coq syntax of theorem implication

Question

I follow this tutorial : https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html
Section 'Proof by Rewritting' :
The code

Theorem plus_id_example : forall n m : nat,
  n = m =>
  n + n = m + m.

Produces the error :
Syntax error: '.' expected after [vernac:gallina] (in [vernac_aux]).
I don't get what am I doing wrong ?
Also, what is the best place to get documentation ? I mean, beginner-friendly documentation.

SCappella SCappella · Accepted Answer · 2019-03-15T18:40:14

To use the text as it's written on the page you linked, you need to import some notations. In particular, ∀ and → don't exist by default. To import these notations use Require Import Utf8.

Require Import Utf8.

Theorem plus_id_example : ∀n m:nat,
  n = m →
  n + n = m + m.

The ASCII equivalents of these notations are forall for ∀ (as you figured out) and -> for →. If you have the notations imported, you can see what they stand for using Locate. Locate "→". will have output

Notation
"x → y" := forall _ : x, y : type_scope
(default interpretation)

Of course, this doesn't give us ->, since -> is itself a notation for the same thing. Coq will display that notation by default, so if you input

Theorem plus_id_example : forall n m : nat,
  forall _ : n = m,
  n + n = m + m.

(without Utf8 imported), the output is

1 subgoal
______________________________________(1/1)
forall n m : nat, n = m -> n + n = m + m

which uses the -> notation.

coq syntax of theorem implication

1 Answers