TL/Coq tutorial — french version: https://gist.github.com/erikmd/ce3f4152f4156128848e64e98aacfc92

tutorial.v

(* Coq syntax reminder: comments are written between (* and *). *)

(*******************************)
(* Tutorial (Course/TP) of Coq *)
(*******************************)

(* See also these course materials (teaching unit ILU3, L3 CS, UPS, in French):

   https://pfitaxel.github.io/ilu3-coq-alectryon/

   Only reading the first 2 Courses (not the 3rd) would be useful for TL
 *)

(* This tutorial is in the form of a .v file to complete.

   You can code your answers interactively with Coq
   by editing the .v file in Emacs+ProofGeneral = the environment recommended
   for TL's TPs (https://github.com/erikmd/tapfa-init.el)
 *)

(* Do not hesitate to ask your supervisor for any questions. *)

(* Summary of the main Emacs shortcuts : do C-f1 (Ctrl+F1) or M-f1 (Alt+F1)

   The ProofGeneral shortcuts all start with C-c (Ctrl+C).
   In particular to evaluate phrases in Emacs+ProofGeneral :
   go to the cursor by doing "C-c RET" (<=> Ctrl+C Entrée)
   or "C-c C-RET"

   Pro Tips:
   - If you've just written a Coq sentence, you can also quickly press
     "." twice (in this case, no need for "C-c RET")
   - To go to the end of the zone validated by Coq, press "C-c C-."
   - To move one step forward or backward, press "C-c C-n" or "C-c C-u"
   - You can also use the Emacs toolbar, which can be displayed using
     the menu (?) -> Show / hide the tool-bar.
 *)

(* Plan :
   1. TYPES AND EXPRESSIONS PART
   1.1. First, a little bit of (functional!) programming
   1.2. A quick reminder about higher-order functions
   1.3. A little more programming; some data structures
   1.4. First proofs "by hand", in propositional logic
   2. ASSISTED-PROOF PART
   2.1. Back to propositional logic
   2.2. Predicate calculus (with quantifiers)
   2.3. Back to Booleans and integers
   2.4. Forward reasoning, Cuts
   2.5. Proofs on lists
 *)

(****************************)
(*                          *)
(* 1. TYPES AND EXPRESSIONS *)
(*                          *)
(****************************)

(*********************************************************)
(* 1.1. First, a little bit of (functional!) programming *)
(*********************************************************)

(* Let's define the function which, to n, associates n + 1. *)

(* In OCaml, we would have written:

   let f = fun n -> n + 1;;
 *)

(* In Coq, we write:

   Definition f := fun n => n + 1.

what ProofGeneral will display with colors
and/or replace fun with a lambda: *)

Definition f := fun n => n + 1.

(* In math, we would write:

   f : N ⟶ N
       n ↦ n+1

   "↦" ("\mapsto" in LaTeX) will be written "fun … => …" en Coq.

   The part "N ⟶ N" also exists in Coq and is called the "type" of the function.

   Here Coq has automatically inferred it, we can display it with : *)

Check f.

(* We could also have given it explicitly *)
Definition f2 : nat -> nat := fun n => n + 1.

(* Unlike OCaml, it is impossible to define in Coq two
   functions (or types) having the same name in the same file;
   thus, this helps to avoid confusion. *)
Fail Definition f2 := fun n => n + 2.
(* The "Fail" command checks that the following sentence gives an error,
   ignore this one and continue anyway.
   This command therefore essentially has a "documentation" purpose. *)

(* Generally, "t : T" reads «t is of type T».
   We can put such “type annotations” almost everywhere and
   t is not necessarily a function. *)
Definition f3 := fun (n : nat) => n + 1.

(* Other syntax: to avoid having to write fun, we can also
   write the argument name after the function name, before ":="
   (and this is what we will do from now on). *)
Definition f4 n := n + 1.

(* The syntax changes but it is exactly the same function, like the
   Print command shows. *)
Print f4.
Print f.  (* same result *)

(* As with any programming language, functions can be evaluated *)
Eval compute in f 2.
(* Just like in OCaml, we could write "f(2)", but the parentheses
   are of no use if there is no subexpression to group together;
   so we generally just use a space : "f 2" *)

(* We can also ask the type of f 2 *)
Check f 2.
(* Of course, the term must be well typified. This fails : *)
Check f f.
(* Comment out the previous line (or add the "Fail" command in front)
   to be able to continue *)

(******************************************************)
(* 1.2. A quick reminder about higher-order functions *)
(******************************************************)

(* As in OCaml, you can define curried functions
(i.e. taking two or more arguments) : *)
Definition g x y := x + 2 * y.

(*equivalent syntaxes*)
Definition g2 := fun x y => x + 2 * y.
Definition g3 := fun x => (fun y => x + 2 * y).

(*Let's look at the type of g*)
Check g.
(* we obtain «nat -> nat -> nat» which read «nat -> (nat -> nat)»
   i.e. the function g is a function with one argument (x), which
   returns a function taking an argument (y) and returning x+2y. *)
Check g 1.

(* for the evaluation, we can therefore write *)
Eval compute in (g 1) 3.
(*or more simply*)
Eval compute in g 1 3.

(* We can also define "functionals", i.e. functions taking functions
   as arguments: *)
Definition repeat_twice f (x : nat) := f (f x).

Check repeat_twice.
(* repeat_twice *)
(*      : (nat -> nat) -> nat -> nat *)

Print f.
Eval compute in repeat_twice f 2.

(********************************************************)
(* 1.3. A little more programming; some data structures *)
(********************************************************)

(* one of the simplest types: booleans *)
Check true.
Check false.

(* Booleans are defined in the Coq standard library
as a user type with 2 constructors:

a boolean is either true or false (and nothing else) *)
Print bool.

(* true and false are thus constructors. Note in passing that it
there is no constraint on the “case” of constructors in Coq:
no need for them to start with a capital letter. *)

(*we can examine the value of a boolean with a match*)

Definition et a b :=
  match a with
  | true => b
  | false => false
  end.

(* Writing "if b then ct else cf" is just syntactic sugar
for the match above and it is the simplified writing by default: *)

Print et.

(* But you can switch to “low-level display” mode to deactivate
this simplified writing: *)

Set Printing All.

Print et.

Unset Printing All.

Eval compute in et true false.

Eval compute in et true true.

(*Similarly to OCaml, we are obliged to define all cases, but
   “non-exhaustive pattern-matching” is an error, not a warning
   (comment to continue) *)
Definition et_non_exhaustif a b :=
  match a with
  | true => b
  end.

(* The standard Coq library provides notations "&&", "||"
associated with the definitions "andb" (identical to our definition "and"
so in the following we will use "andb" rather than "et"), "orb",
and "negb": *)

Check andb false true.
Check orb false true.
Check negb false.
Eval compute in negb false.

(* A possible invocation to have lighter notations: *)
Open Scope bool_scope.

Check andb false true.
Check orb false true.

(* a slightly more complex type: natural numbers.

They are defined in the Coq standard library as a type
user to 2 constructors:

an integer is either O or the successor of an integer. *)
Print nat.

(* Note that the syntax displayed by Coq is equivalent to the following syntax :

Inductive nat :=
  | O
  | S (_ : nat). *)

(*At the time this nat type is defined in the standard library,
   Coq automatically generates the induction principle "nat_ind", which
   naturally coincides with the "proof by induction" scheme,
   which we will see (again) later. *)
Check nat_ind.

(* Note, the representation of integers in this form corresponds
   to a "base 1 representation", that is to say that the integer
   16, even if Coq “reads” and “writes” it in base 10 with the options
   default display, internally it is stored as
   of an inductive expression involving 17 constructors! *)

Set Printing All.
Check 16.
Unset Printing All.
Check 17.

(* Of course, other more compact representations of integers
   natural (in binary…), and relative integers, are available
   in the standard Coq library, but we will not go into more detail
   on this aspect during this tutorial nor in the TL module. *)

(* We recalled previously (“and” function) the syntax of Coq
   to perform filtering (syntax very close to that of OCaml!)

   As for the equivalent of "let rec" in Coq, it involves using
   the “Fixpoint” command.

   On the other hand, we will not use the Coq equivalent of OCaml syntax
   "let rec … in", since in practice this would make the
   proofs of properties of locally defined function... *)

(* Define function "factorielle" of type "nat -> nat".
   Then calculate "factorielle 3".

   Reminder on recursion: you must ensure that your
   recursive function definitions have recursive calls of which
   the main argument is structurally decreasing (to guarantee
   termination. Otherwise, Coq will refuse your definition! *)

(*
Fixpoint factorielle n := (* ... (to complete) *)

Eval compute in (* ... (to complete) *)
 *)

(* Set boolean predicate "pair" of type "nat -> bool".
   Then calculate "pair 6". *)
(*
Fixpoint pair n :=  (* ... (to complete) *)

Eval compute in (* ... (to complete) *)
 *)

(* To conclude on this review of filtering and recursion in Coq
   here is an example of defining a boolean predicate "inf",
   testing if an integer n is smaller than or equal to another integer m.
   Can you explain in your own words each of the branches of the
   match ? (which here corresponds to simultaneous pattern-matching!) *)
Fixpoint inf n m :=
  match n,m with
  | O, _ => true
  | S n1, O => false
  | S n1, S m1 => inf n1 m1
  end.
Check inf.
Eval compute in inf 2 3.
Eval compute in inf 1 0.

(* Remarque : don't confuse "computable" boolean operations
&&, || et negb, with logic connectors /\, \/ et ~, who does not
do not take Booleans as arguments but Propositions : *)

Check 0 = 0.
(* 0 = 0 *)
(*      : Prop *)

Check (0 = 0) /\ (0 = 0).

Check 0 < 1 \/ 0 = 1 \/ 0 > 1.

(* "/\" is thus a notation for and,
   "\/" for or,
   "~" for not *)

Check and (0 = 0) (0 = 0).
Check or (0 < 1) (or (0 = 1) (0 > 1)).

(* Q1. What is a proposition in Coq?
   Q2. how to show that a proposition is true?

Before doing specific exercises to prove propositions
simple in 3 different ways (by hand, semi-automatically
or fully automatic), two quick answers:


R1. A proposition is a logical formula, and in Coq it is
both an object of type Prop, and a data type whose expressions
of this type are the proofs of the formula in question.

This corresponds to the notion of “Curry-Howard correspondence” seen in
course.

For example, we will have (proof that 0=0) : 0 = 0 : Prop

Thus, Prop is a "type of type", just like the keyword Type
seen in course.

There are some semantic differences between Prop and Type that we
we will not go into detail here. (The main idea being that Type matches
to the type of “informative data types” (integers, lists, functions),
Prop corresponds to the type of “purely logical formulas”.)


R2. To show that a proposition P is true, it is a question of exhibiting
a proof, that is to say an expression p which has the right type (p : P).

The purpose of the Coq proof assistant is to facilitate the construction
of these terms of proof (p), then at the time of "Qed.", to verify
automatically that the type of the proof term coincides with the statement
of the formula we want to prove.

Now, exercises! *)

(*******************************************************)
(* 1.4. First proofs "by hand", in propositional logic *)
(*******************************************************)

Section PremieresPreuves.

(*In this section, assume three propositions A, B and C*)
Variables A B C : Prop.

(* a function is a proof: for example, the identity function
   "prove" that A implies A *)
Definition identite : A -> A := fun a => a.

(* prove at least 2 properties among the following properties *)

(*
Definition ex0 : B -> B := (* ... (to complete) *)

Definition ex1 : A -> B -> A := (* ... (to complete) *)

Definition ex2 : A -> B -> B := (* ... (to complete) *)

Definition ex3 : A -> (A -> B) -> B := (* ... (to complete) *)

Definition ex4 : (A -> B) -> (B -> C) -> A -> C := (* ... (to complete) *)

Definition ex5 : (A -> B) -> (A -> B -> C) -> A -> C := (* ... (to complete) *)
 *)

End PremieresPreuves.

(**************************)
(*                        *)
(* 2. ASSISTED-PROOF PART *)
(*                        *)
(**************************)

(************************************)
(* 2.1. Back to propositional logic *)
(************************************)

Section PremieresTactiques.

(*In this section, assume three propositions A, B and C*)
Variables A B C : Prop.

(* We could do all our proofs by writing functions of the
   good guy, as before, but it quickly becomes inhuman; Coq
   therefore offers an interactive mode in which it will help us to
   construct the proofs step by step (hence the name Proof assistant). *)

Lemma ex'0 : B -> B.
(* instead of Lemma, we could use the synonyms Theorem,
Remark, Corollary, Fact, Example *)
Proof.
(*we start an interactive proof*)
(* we now type tactics which will modify the sub-goals to
prove until there's none left *)
intros Hb.
(* our first tactic, we move hypothesis B and give it the name Hb *)
(* Hb has type B ie Hb is a proof of B *)
apply Hb.
(* our second tactic, we use B *)
Qed.
(* Quod Erat Demonstrandum, CQFD in Latin, we record and verify the proof *)

(* in fact, here Coq knows how to prove this automatically *)
Lemma ex'0' : B -> B.
Proof. auto. Qed.

(* redo the previous proofs using the intros and apply tactics *)
Lemma ex'1 : A -> B -> A.
Proof.
(* ... (to complete) *)
Admitted.

Lemma ex'2 : A -> B -> B.
Proof.
(* ... (to complete) *)
Admitted.

(*
  For ex'3, we will notice that the type of the 2nd hypothesis introduced is
  a functional type. It is therefore possible to apply the function on a
  argument of type A to obtain a B.
  Deduce 2 different proofs of ex'3', using the apply tactic
  once or twice.
  Note (doing Print ex'3_Vi) that the constructed term is the same.
*)
Lemma ex'3_V1 : A -> (A -> B) -> B.
Proof.
(* ... (to complete) *)
Admitted.

Lemma ex'3_V2 : A -> (A -> B) -> B.
Proof.
(* ... (to complete) *)
Admitted.

Lemma ex'4 : (A -> B) -> (B -> C) -> A -> C.
Proof.
(* ... (to complete) *)
Admitted.

Lemma ex'5 : (A -> B) -> (A -> B -> C) -> A -> C.
Proof.
(* ... (to complete) *)
Admitted.

(* in the presence of several sub-goals, braces can be used
   to delimit them *)
Lemma ex'5' : (A -> B) -> (A -> B -> C) -> A -> C.
Proof.
intros Hab Habc Ha.
apply Habc.
{ admit. (* ... (to complete) *)
}
admit. (* ... (to complete) *)
Admitted.

(* or delimit the sub-goals with “-” items *)
Lemma ex'5'' : (A -> B) -> (A -> B -> C) -> A -> C.
Proof.
intros Hab Habc Ha.
apply Habc.
- admit. (* ... (to complete) *)
- admit.  (* ... (to complete) *)
Admitted.

(*note: these lemmas are quite simple and the “auto” tactic
   proves all *)
Lemma ex'5''' : (A -> B) -> (A -> B -> C) -> A -> C.
Proof.
auto.
Qed.

(* Consider the conjunction of 2 propositions: A /\ B.
   From A and B, we can prove A /\ B by applying conj.
   Not to be confused with function (andb : bool -> bool -> bool).
*)
Check conj.

Lemma ex6 : A -> B -> A /\ B.
Proof.
intros Ha Hb.
apply conj.
- apply Ha.
- apply Hb.
Qed.

(*the “split” tactic is a synonym for “apply conj”*)
Lemma ex6' : A -> B -> A /\ B.
Proof.
intros Ha Hb.
split. (* 2 subgoals are produced: prove A, prove B *)
- apply Ha. (* 1er sub-goal: we prove A *)
- apply Hb. (* 2eme sub-goal: we prove B *)
Qed.

(* we can destroy A /\ B after having introduced it, with "destruct …"
or "destruct … as [Ha Hb]" *)
Lemma ex7 : A /\ B -> A.
intros Hab. (* Hab is a proof of A/\B *)
destruct Hab as [Ha Hb]. (* Ha is a proof of A, Hb a proof of B *)
apply Ha.
Qed.

(*Prove the following lemma*)
Lemma ex8 : A /\ B -> B /\ A.
Proof.
(* ... (to complete) *)
Admitted.

(* the disjunction (or) is similar: A \/ B.
   From A (resp. B), we have a proof of A \/ B.
   If we have a proof of A or a proof of B,
   we can prove A \/ B by applying or_introl (resp. or_intror) *)
Check or_introl.
Check or_intror.

Lemma ex9 : A -> A \/ B.
Proof.
intros Ha.
apply or_introl.
apply Ha.
Qed.

(* the tactic “left” (resp. right) is a synonym for «apply or_introl» *)
Lemma ex9' : A -> A \/ B.
Proof.
intros Ha.
left.
apply Ha.
Qed.

(* just like A /\ B, we can destroy A \/ B with “destruct …” or
   "destruct … as [Ha | Hb]"
 *)
(* we will note that the destruction of an AND produces 2 hypotheses while
   the destruction of an OR leads to 2 proofs - 1 for each hypothesis
 *)
Lemma ex10 : A \/ B -> (B -> A) -> A.
Proof.
intros Hab.
destruct Hab as [Ha | Hb]. (* creates 2 sub-goals *)
- intros _. (* we do not need the hypothesis introduced, so we ignore it with _ *)
  apply Ha.
- intros Himpl.
  apply Himpl.
  apply Hb.
Qed.

(*Prove the following lemma*)
Lemma ex11 : A \/ B -> B \/ A.
Proof.
(* ... (to complete) *)
Admitted.

End PremieresTactiques.

(*******************************************************)
(* 2.2. Predicate calculus (with quantifiers) *)
(*******************************************************)
Section CalculPredicats.

Variable P Q : nat -> Prop.
Variable R : nat -> nat -> Prop.

(* Prove *)
Lemma ex12 : (forall x, P x) /\ (forall x, Q x) -> (forall x, P x /\ Q x).
Proof. (* use «intros x» and apply *)
(* ... (to complete) *)
Admitted.

(* Prove *)
Lemma ex13 : (forall x, P x) \/ (forall x, Q x) -> (forall x, P x \/ Q x).
Proof.
(* ... (to complete) *)
Admitted.

(* Essayez de prouver (si c'est possible !) *)
Lemma ex14 : (forall x, P x \/ Q x) -> (forall x, P x) \/ (forall x, Q x).
Proof.
(* ... (to complete) *)
Abort.

(* (H: exists x, …) is destroyed with “destruct H as [x Hx]” *)
(* and is proven with the “exists x” tactic: to prove a formula
  exists x, P x, you must provide a value for x and prove that it
  satisfied P*)
Lemma ex15 : (exists x, forall y, R x y) -> (forall y, exists x, R x y).
Proof.
intros Hex.
destruct Hex as [x Hx].
intros y.
exists x.
apply Hx.
Qed.

(* Prove *)
Lemma ex16 : (exists x, P x -> Q x) -> (forall x, P x) -> exists x, Q x.
Proof.
(* ... (to complete) *)
Admitted.

End CalculPredicats.

(**************************************)
(* 2.3. Back to Booleans and integers *)
(**************************************)

Open Scope bool_scope.

(* Booleans allow to do proofs by "brute force" (enumeration of all cases) : *)
Lemma negneg : forall b, negb (negb b) = b.
Proof.
intros b.
destruct b. (* generates a goal for each possible value of b *)
- easy. (* a bit more powerful than "reflexivity" *)
- easy.
Qed.

(* Prove *)
Lemma and_commutatif : forall a b, a && b = b && a.
Proof.
(* ... (to complete) *)
Admitted.

(* consider integer addition defined in the Coq library by :

Fixpoint plus n m :=
  match n with
  | 0 => m
  | S p => S (plus p m)
  end.

We will thus note that
  - (plus 0 m) reduces to m
  - (plus (S n) m) reduces to S (plus n m).
However (plus n 0) des not reduce.
 *)

(* the "simpl" tactic is used to simplify terms *)
Lemma plus0n : forall n, plus 0 n = n.
Proof.
intros n.
simpl.
reflexivity.
Qed.

(* but one can also directly write *)
Lemma plus0n' : forall n, plus 0 n = n.
Proof.
reflexivity. (* since the 2 terms are identical after reduction *)
Qed.

(* it doesn't work the other way around *)
Lemma plusn0 : forall n, plus n 0 = n.
Proof.
intros n.
simpl. (* does nothing *)
(* in fact, plus is defined recursively on its first argument,
in this case n, which is any natural number (we don't know if it is
of the form O or S n'), so we can't calculate anything *)
Abort.

(* We will proceed by recurrence on n using the induction tactic *)
Lemma plusn0 : forall n, plus n 0 = n.
Proof.
(* no need to do "intros n" beforehand! *)
induction n.
- (* simpl. useless *) reflexivity. (* basic cases *)
- simpl. (* useful for showing the term we want to rewrite *)
  rewrite IHn. (* hypothèse de récurrence *)
  (* rewrite can be used with any equality *)
  (* if need be, we could use the equality from right to left by doing
     rewrite <-IHn *)
  easy.
Qed.

(* Prove *)
Lemma plus1n : forall n, plus 1 n = S n.
Proof.
(* ... (to complete) *)
Admitted.

(* Prove *)
Lemma plusSn : forall n m, S (plus n m) = plus n (S m).
Proof.
(* ... (to complete) *)
Admitted.

(* Prove (a bit harder, don't hesitate to use the previous lemmas) *)
Lemma plus_commutatif : forall n m, plus n m = plus m n.
Proof.
(* ... (to complete) *)
Admitted.

(* you can also use the operators +,* which are just notations *)
Lemma plus_commutatif_bis : forall n m, n + m = m + n.
Proof.
apply plus_commutatif.
Qed.

From Coq Require Import Lia. (* Linear Integer Aritmetic:
automatic proof of linear properties on integers *)

Lemma plus_commutatif' : forall n m, n + m = m + n.
Proof.
intros n m.
lia. (* it's automatic! *)
Qed.
(* lia supports sum, product by a constant, comparisons *)

(********************************)
(* 2.4. Forward reasoning, Cuts *)
(********************************)

(* So far, proofs have been made by modifying the goal until it becomes
trivial or it reduces to a known lemma.

We often do the opposite when writing a proof on paper:
we start from the hypotheses and modify them to reach the conclusion.
This is known as the "forward" style of reasoning.

This often involves making what is known as a cut:
the proof is paused to prove an intermediate result which is then used.

This can be done using an intermediate lemma (like the "plusSn" lemma
in the proof of "plus_commutatif" above) but sometimes you have to copy
all the hypotheses and leave a lemma lying around, perhaps too specialized
to be really reusable.

The tactic
"assert (nom : propriété)." provides a lighter alternative. *)

Lemma plus_commutatif'' : forall n m, plus n m = plus m n.
Proof.
induction n.
- intros m.
  rewrite plusn0.
  easy.
- assert (HplusSn : forall m, S (plus m n) = plus m (S n)).
  { induction m.
    - easy.
    - simpl.
      rewrite IHm.
      easy.
  } (* we now have HplusSn in our hypotheses *)
  intros m.
  simpl.
  rewrite IHn.
  rewrite HplusSn.
  easy.
Qed.

(************************)
(* 2.5. Proofs on lists *)
(************************)

Require Import List.
Import ListNotations.
(* les 2 constructors are denoted [] and _::_ like in OCaml *)

(* To be placed at the beginning of the file or
   before the 1st polymorphic definition *)
Set Implicit Arguments.

Fixpoint append T (l1 l2 : list T) : list T := (* T made implicit *)
  match l1 with
    [] => l2
  | x :: r => x :: append r l2 (* the 1st argument T is implicit *)
  end.
Eval compute in append [1;2] [3;4].  (* uses "append", defined above *)
Eval compute in [1;2] ++ [3;4].  (* uses "app" from the standard library *)
(* the concatenation is thus denoted "… @ …" in OCaml, "… ++ …" in Coq *)

(* The induction principle on lists is automatically generated when the
list type is defined. The "most general iterator on lists" has the
following type, and can be related to the induction principle: *)
Check list_ind.

(* Let's prove a correction lemma for the function "app" *)

Lemma app_length :
  forall T (l l' : list T), length (app l l') = length l + length l'.
Proof.
(* ... (to complete, starting with induction l) *)
Admitted.

Print app_length. (* note that the proof term contains "list_ind" *)