Module minimal_Gallina_introduction.

Variable x : Prop.
Variables A B : Prop.
Variable t2 : Prop.

Check A -> B : Prop.
(* NB: holds thanks to the rule Prod-Prop *)

Check (fun y => y -> y) : Prop -> Prop.
Definition t1_oops := fun y => y -> y.
Check t1_oops.
Definition t1 := fun y : Prop => y -> y.
Check t1.
Check t1 A : Prop.

Check (Prop -> Prop) -> B.
(* NB: Prop -> Prop has type a sort -> ok *)
Fail Check (fun y : Prop => y -> y) -> B.
(* NB: (fun y : Prop => y -> y) has type Prop -> Prop, which is not a sort -> NG *)

End minimal_Gallina_introduction.

From Ssreflect Require Import ssreflect.

Module propositions_as_types_example.

Lemma hilbertS (A B C : Prop) :
  (A -> B -> C) -> (A -> B) -> A -> C.
Show Proof.
move=> H1.
Show Proof. (* observe the effect of move=> on the proof-term *)
move=> H2.
move=> H3.
Show Proof.
cut B. (* NB: this is a traditional Coq tactic, seldom used in practice but corresponds well to modus ponens *)
Show Proof.
cut A.
Show Proof.
assumption.
assumption.
Show Proof.
cut A.
assumption.
assumption.
Show Proof.
Qed.

Definition hilbertS_proof :=
  fun (A B C : Prop) (H1 : A -> B -> C) (H2 : A -> B) (H3 : A) =>
    (fun H : B => (fun H0 : A => H1 H0) H3 H) ((fun H : A => H2 H) H3).

Lemma hilbertS_direct_proof (A B C : Prop) :
  (A -> B -> C) -> (A -> B) -> A -> C.
exact (hilbertS_proof A B C).
Qed.

Lemma hilbertS_in_practice (A B C : Prop) :
  (A -> B -> C) -> (A -> B) -> A -> C.
move=> H1.
move=> H2.
move=> H3.
apply H1.
exact H3.
apply H2.
exact H3.
Show Proof.
Qed.

Definition hilbertS_in_practice_proof :=
  fun (A B C : Prop) (H1 : A -> B -> C) (H2 : A -> B) (H3 : A) =>
    H1 H3 (H2 H3).

Goal hilbertS_proof = hilbertS_in_practice_proof.
reflexivity.
Qed.

End propositions_as_types_example.

Module move_and_apply_tactics.

Lemma modus_ponens : forall P Q : Prop, (P -> Q) -> P -> Q.
Show Proof.
move=> P.
Show Proof.
move: P.
Show Proof.
move=> P Q PQ p.
apply: PQ.
done.
Qed.

Goal forall P Q : Prop, (forall R : Prop, R -> Q) -> P -> Q.
Proof.
move=> P Q rq p.
Fail apply rq.
apply: rq p.
(*
compare with:
refine (rq _ _).
exact p.
*)
Qed.

(* a note an unification *)
Variable A : Prop.
Variable op : A -> A -> A.
Local Notation "a + b" := (op a b). (* left associative *)
Hypothesis opA : forall a b c, a + (b + c) = a + b + c.
Variable lt : A -> A -> Prop.
Local Notation "a < b" := (lt a b).
Hypothesis lt_addr : forall m n p, m < n -> m < n + p.

Goal forall a b c d,
  a < b ->
  a < b + c + d.
move=> a b c d.
Fail apply lt_addr.
(* Error: Impossible to unify "b + c" with "b". *)
(* match m<->a, n<->b, p<->d and thus b + c<->n !!! *)
rewrite -opA.
apply lt_addr.
Qed.

Goal False.
evar (x : nat).
have : (2 + x = 4 + 5)%nat.
  rewrite /x.
  apply refl_equal.
rewrite /= in x *.
Abort.

End move_and_apply_tactics.

Lemma exo0 : forall P : Prop, P -> P.
Proof.
Abort.

Lemma exo1 : forall P Q : Prop, P -> (P -> Q) -> Q.
Proof.
Abort.

Lemma exo2 : forall P : Prop, (P -> P) -> P -> P.
Proof.
(* NB: pove using the modus ponens lemma *)
Abort.

(* transitivity of implication *)
Lemma exo3 P Q R : (P -> Q) -> (Q -> R) -> P -> R.
Proof.
Abort.

Section logical_connectives.

Print True.
Check True.
Check I.

Goal True.
apply: I.
Qed.

Print False.

Goal True -> False.
case.
Show Proof.
Abort.

Check False_ind.

Goal False -> 1 = 0.
move=> p.
exact: (False_ind (1 = 0) p).
Qed.

Print and.
Check conj I I.
Print and_ind.
Print and_rect.

Goal forall P Q, P /\ Q -> Q /\ P.
move=> P Q.
case.
Show Proof.
move=> p q.
split.
exact q.
exact p.
Qed.

Print or.
Print or_ind.

Check (or_intror False I).
About or_intror.
Check (@or_intror False True I).
Check (@or_intror False _ I).
Check (@or_intror _ _ I).
Check (@or_intror _ _ I) :  False \/ True.

Goal forall A B, A \/ B -> B \/ A.
move=> A B.
  case=> [a | b].
  right.
  exact a.
left.
exact b.
Qed.

End logical_connectives.

Lemma exo4 : False \/ True.
Proof.
Abort.

Lemma exo5 : forall A B C : Prop, A /\ B <-> B /\ A.
Proof.
Abort.

Lemma exo6 (A B C : Prop) : A /\ B /\ C ->
  (A /\ B) /\ C.
Proof.
Abort.

Lemma exo7 (A B : Prop) : (A -> B) -> (~B -> ~A).
Proof.
Abort.

Section Set_Prop.

Check nat.

Goal 0 = 1 -> False.
move=> abs.
discriminate.
Qed.

(* case analysis of Prop proofs forbidden on sorts Set and Types *)

Goal (exists n : nat, True) -> nat.
Fail case.
(*  Error: Case analysis on sort Set is not allowed for inductive definition ex *)
Abort.
About ex.

Goal forall A B : Prop, A \/ B -> nat.
move=> A B.
Fail case.
Abort.

(* case analysis of Prop proofs ok on sort Set when only one constructor *)

Goal 0 = 1 -> nat.
move=> abs.
discriminate.
Show Proof.
Qed.

Goal forall n m : nat, n = m /\ n <> m -> nat.
move=> n m.
case => nm nm'.
exact O.
Qed.

Print sum.
Print sumbool.
Print sumor.

(* case analysis of Type proofs ok on any sorts *)

About sig.
Goal {n : nat | True} -> nat.
case.
move=> m _.
exact m.
Qed.

End Set_Prop.

Section product_formation.

(* NB: hierarchy *)
Check Prop.
Check Set.
Set Printing Universes.
Check Type.
Unset Printing Universes.

(* rule Prop <= Set: *)
Variables P0 P1 : Prop.
Check P0 -> P1 : Set.
Check P0 : Set.
(* rule Prop <= Type: *)
Check P0 : Type.
(* NB: rule Set <= Type: *)
Variable S0 : Set.
Check S0 : Type.

(* rule Prod-Prop: *)
Check P1 -> P1 : Prop.
Check (S0 -> P0) : Prop.
Variable T0 : Type.
Check (T0 -> P0) : Prop.

Check (forall x : nat, 0 <= x).
Check (forall x : nat, x = x) : Set.
Check (forall A : Prop, A -> A).
Check (forall P : nat -> Prop, P O -> exists n : nat , P n) : Prop.

(* rule Prod-Set: *)
Check (P0 -> S0) : Set.
Fail Check (P0 -> S0) : Prop.
Variable S1 : Set.
Check (S1 -> S0) : Set.
Fail Check (T0 -> S0) : Set.

Check (nat -> nat).
Fail Check (forall A : Set, A -> A) : Set.

(* rule Prod-Type: *)

Check (Prop -> Prop) : Type.
Check (Set -> Set) : Type.
Check (forall A : Set, A -> A) : Type.
Check (nat -> Prop) : Type.
Check ((Prop -> Prop) -> Prop) : Type.
Check (forall P : nat -> Prop, Prop) : Type.

End product_formation.