What is meant by Coq arrow -> in Coq theorem?

Question

I am trying to understand Coq theorem:

Theorem thm0 : UseCl Pos (PredVP (UsePN john_PN) walk_V) ->
               UseCl Pos (PredVP (UsePN john_PN) walk_V).
intro H.
exact H.
Qed.

from https://github.com/GU-CLASP/FraCoq/blob/master/Tutorial.org

What is meant by the arrow symbol ->? As I understand, then Coq uses two arrows https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html : 1) double arrow for defining type constructors and 2) single arrow -> for definint new type. But this theorem is statement, not the type definition. Why there is this arrow? How to understand this statement as a Coq theorem?

Answer 1

The double arrow (=>) is used in Coq to mark pattern-matching branches. For example, we can define boolean negation like this:

Definition negb (b : bool) : bool :=
  match b with
  | true  => false
  | false => true
  end.

The single arrow (->) is used to express two seemingly unrelated concepts:

1. Function types. For instance, nat -> bool is the type of functions from the natural numbers to booleans.

2. Logical implication. This is the use that you see in the statement of your theorem. The statement A -> B means that B holds whenever A does.

In reality, however, this distinction is only superficial: in Coq, proofs of implication and functions are actually the same thing! For Coq, a proof of implication A -> B is, in a precise sense, a function that takes a proof asserting the truth of A and returns a proof asserting the truth of B. If this sounds confusing, do not worry: you can just pretend most of the time that the two uses of the arrow refer to different things, and this will not harm you. The Software Foundations book has a chapter that discusses these issues in more detail.