Require Import ssrmatching ssreflect.

Section MinimalLogic.

(* we assume two types A and B in our context *)
Variables A B : Type.


(* we can define our first lambda term in this context: the identity on A *)

Definition identA (x : A) := x.

(* ask the type of identA *)
About identA.

(* print the body (definition) of identA *)
Print identA.

(* Remember the type of identA *)
About identA.

(* What if we see this arrow as an "implication" arrow *)
Lemma tautoA : A -> A.
Proof.
move=> x.
exact: x.
Show Proof.
Qed.

(* identA and tautoA are the same lambda terms (with same type) *)
Print tautoA.
Print identA.

(***)

(* Parentheses associate on the right *)
Lemma modus_ponens : (A -> B) -> A -> B.
Proof.
move=> hAB hA.
(* the proof proceeds backward *)
apply: hAB.
apply: hA.
Show Proof.
Qed.

Print modus_ponens.

(***)

(* let us enrich our context with some elements of type A*)

Variables a b c : A.

(* We  dispose of a 'primitive' equality predicate *)
Lemma test_eqA : a = b -> c = b -> a = c.
Proof.
move=> eab ebc.
(* Equality is substitutive: we can rewrite with these hypotheses *)
rewrite eab.
rewrite ebc.
(* We conclude by reflexivity of equality *)
Check (eq_refl b).
exact: (eq_refl b).
Qed.

(***)

(* Terms (identA a) and a are convertible *)

Lemma identAa : identA a = a.
Proof.
Check (eq_refl a).
exact: (eq_refl a).
Show Proof.
Qed.

(* Let us close the section. *)
End MinimalLogic.

(* the type of tautoA has been abstracted over A *)
About tautoA.

(* same for idA *)
About identA.

(* same for test_eqA *)
About test_eqA.

(***)

Section DependentTypes.

(* Consider a type A and two families of types B and C, *)
(* indexed by the inhabitants of A *)
Variable A : Type.

Variables B C : A -> Type.

(* Supppose that every type in the family B is inhabited *)
Hypothesis hB : forall a : A, B a.

Hypothesis hC : forall a, B a -> C a.

Lemma pC : forall a : A, C a.
Proof.
move=> a.
apply: hC.
apply: hB.
Qed.

Print pC.

(* A more sophisticated family of types, with two indexes *)
Variable D : forall a : A, B a -> Type.

Hypothesis hD : forall a, forall b : B a, D a b.

End DependentTypes.

(***)

(* Basic functional programming with enumerated types*)

(* enumerated type *)
Inductive color : Type :=
 |blue : color
 |green : color
 |magenta : color
 |yellow : color.

About color_rect.
(* Print color_rect. *)

(* A program defined by pattern matching *)
Definition complementary_color (c : color) : color :=
  match c with
    |blue => magenta
    |green => yellow
    |magenta => blue
    |yellow => green
  end.

About complementary_color.

Eval compute in complementary_color magenta.

Eval compute in complementary_color green.

(* A proof by case analysis and computation of an equality statement *)
Lemma complementary_color_is_involutive (c : color) :
  complementary_color (complementary_color c) = c.
Proof.
case: c.
- compute. apply: eq_refl.
- compute. apply: eq_refl.
- compute. apply: eq_refl.
- compute. apply: eq_refl.
Qed.

(* Observe the universal quantification *)
About complementary_color_is_involutive.

(* We could shorten the script by applying the same tactics to all subgoals. *)

(* Distinct labell are distinct objects *)
Lemma ex_falso : forall T : Type, blue = magenta -> T.
Proof.
move=> T h.
discriminate.
Qed.

(* We will work in a different namespace because we are re-defining things *)
(* that are already available in the libraries we automatically loaded. *)
Module InductiveDatatypesExamples.

Inductive bool : Type :=  true : bool | false : bool.

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

About negb.

Eval compute in negb true.

(* A proof by case analysis *)
Lemma negbK (b : bool) : negb (negb b) = b.
Proof.
(* we use ; to apply the same tactic to every generated subgoal *)
case: b; compute; apply: eq_refl. 
Qed.

(* Boolean conjunction *)
Definition andb (b1 : bool) (b2:bool) : bool :=
  match b1 with
  | true => b2
  | false => false
  end.

About andb.

Eval compute in andb false true.

(* Computation provides some proofs 'for free' *)
(* We use a different strategy than compute, called simpl *)
Lemma andTb (b : bool) : andb true b = b.
Proof. simpl. apply: eq_refl. Qed.

Lemma andFb (b : bool) : andb false b = false.
Proof. simpl. apply: eq_refl. Qed.

(* For the converse lemmas we need a case analysis *)
Lemma andbT (b : bool) : andb b true = b.
Proof. case: b; apply: eq_refl. Qed.

Lemma andbF (b : bool) : andb b false = false.
Proof. case: b; apply: eq_refl. Qed.


(* Boolean disjunction *)
(* In fact we can collect arguments which have the same type inside the same*)
(* parentheses *)
Definition orb (b1 b2 : bool) : bool :=
  match b1 with
  | true => true
  | false => b2
  end.

About orb. 

Eval compute in orb false true.

(* Computation provides some proofs 'for free' *)
Lemma orTb (b : bool) : orb true b = true.
Proof. simpl. apply: eq_refl. Qed.

Lemma orFb (b : bool) : orb false b = b.
Proof. simpl. apply: eq_refl. Qed.

(* For the converse we need a case analysis *)
Lemma orbF (b : bool) : orb b false = b.
Proof. case: b; apply: eq_refl. Qed.


Lemma negb_andb (b1 b2 : bool) : negb (andb b1 b2) = orb (negb b1) (negb b2).
Proof.
case: b1.
(* computation happens because of the definition of orb by case on its first*)
(* argument *)
- compute. apply: eq_refl.
(* simpl: this other computation strategy make progress only if a constructor is available *)
- simpl. apply: eq_refl.
Qed.

Lemma negb_orb (b1 b2 : bool) : negb (orb b1 b2) = andb (negb b1) (negb b2).
Proof.
case: b1.
(* computation happens because of the definition of orb by case on its first*)
(* argument *)
- compute. apply: eq_refl.
(* simpl: this other computation strategy make progress only if a constructor is available *)
- simpl. apply: eq_refl.
Qed.


(* We can use both arguments of the function for our case analysis *)
Definition addb (b1 b2 : bool) :=
  match b1, b2 with
    |true, false => true
    |false, true => true
    |_, _ => false
  end.

(* An other way of defining this function *)
Definition xorb (b : bool) : bool -> bool :=
  match b with
    |true => negb
    |false => (fun x => x)
  end.

Lemma xorb_addb (b1 b2 : bool) : xorb b1 b2 = addb b1 b2.
Proof.
case: b1; case b2; compute; apply: eq_refl.
Qed.

Lemma xorTb (b : bool) : xorb true b = negb b.
Proof. apply: refl_equal. Qed.

Lemma xorbT (b : bool) : xorb b true = negb b.
Proof. case: b; apply: refl_equal. Qed.

Lemma xorFb (b : bool) : xorb false b = b.
Proof. apply: refl_equal. Qed.

Lemma xorbF (b : bool) : xorb b false = b.
Proof. case: b; apply: refl_equal. Qed.

(* Even with more variables, proofs boil down to checking truth tables. *)
Lemma xorbA (b1 b2 b3 : bool) : xorb b1 (xorb b2 b3) = xorb (xorb b1 b2) b3.
Proof. case: b1; case: b2; case: b3; apply: refl_equal. Qed.

(***)

(* Recursive datatypes *)

Inductive nat : Type :=  O : nat | S : nat -> nat.

About nat_rect.

Definition two := S (S O).

Definition three := S two.

Definition four := S three.

(* We can define functions by pattern matching as previously *)
Definition not_zero (n : nat) : bool :=
  match n with
    |O => false
    |S _ => true
  end.

(* We can define recursive functions *)
Fixpoint odd (n : nat) : bool :=
  match n with
    |O => false
    |S m => negb (odd m)
  end.

About odd.

Eval compute in odd four.

Eval compute in odd three.
      
(* A recursive function with two arguments (the first is decreasing *)
Fixpoint add (n m : nat) : nat :=
  match n with
    |O => m
    |S k => S (add k m)
  end.

Eval compute in add two three.

(* Computation provides some proofs 'for free' *)
Lemma addSn (n m : nat) : add (S n) m = S (add n m).
Proof. simpl. apply: eq_refl. Qed.

(* We can also do proofs by recursion *)
Lemma addnS (n m : nat) : add n (S m) = S (add n m).
Proof.
elim: n => [|n ihn] //=.
rewrite ihn. apply: eq_refl.
Qed.

(* Again: this one is for free: *)
Lemma add0n (n : nat) : add O n = n.
Proof. apply: eq_refl. Qed.

(* But this one requires an induction *)
Lemma addn0 (n : nat) : add n O = n.
Proof. elim: n => //= n ->. apply: eq_refl. Qed.

(* The commutativity of addition *)
Lemma addC (n m : nat) : add n m = add m n.
Proof.
elim: n => [|n /= ->] //=.
- rewrite addn0. apply: eq_refl.
- rewrite addnS. apply: eq_refl.
Qed.

(* Let us prove things about the odd predicate *)
(* Boolean equivalence is equality *)
Lemma odd_add (n m : nat) : odd (add n m) = xorb (odd n) (odd m).
Proof.
elim: n => [|n ihn]; simpl.
- apply: eq_refl.
- rewrite ihn -xorTb xorbA. simpl. apply: eq_refl.
Qed.


End InductiveDatatypesExamples.