(* The Curry-Howard Isomorphism      *)
(*   propositional fragment                   *)
(*   Venanzio Capretta, February 2011 *)

(* False is a proposition with no proof,
    it corresponds to the empty set.
*)

Print Empty_set.

Print False.

(* True is a proposition with just one proof,
    it corresponds with the singleton unit set.
*)

Print unit.

Print True.

(* Conjunction is just Cartesian product. *)

Print prod.

Print and.

(* Disjunction is just disjoint sum. *)

Print sum.

Print or.

(* And implication is just the function space: same notation. *)

(* EXAMPLES of programs and corresponding lemmas. *)

Definition composition (X Y Z:Set): (X->Y) -> (Y->Z) -> X -> Z :=
fun f g z => g (f z).

Definition logic_comp (A B C: Prop): (A->B) -> (B->C) -> (A->C) :=
fun h1 h2 h3 => h2 (h1 h3).

Section PropositionalLogic.

Variables (A B C: Prop).

(* Instead of defining a proof-term, we can give a proof using tactics. *)

Lemma logic_composition: (A->B) -> (B->C) -> A -> C.
Proof.
intro h1. (* The tactic "intro" introduces a new assumption. *)
intro h2.
intro h3.
apply h2. (* "apply" uses an assumption to prove the goal. *)
apply h1.
apply h3.
Qed.

Print logic_composition.

Definition tripling (X Y Z:Set): X -> Y -> Z -> X*Y*Z :=
fun x y z => ((x,y),z).

Definition three_conj: A -> B -> C -> A /\ B /\ C :=
fun h1 h2 h3 => conj h1 (conj h2 h3).

Lemma three_conjunction: A -> B -> C -> A /\ B /\ C.
Proof.
intros h1 h2 h3.
split.    (* "split" divides the goal into parts. *)
apply h1.
split.
apply h2.
apply h3.
Qed.

Print three_conjunction.

Definition sum_abs (X Y: Set): (X->Y) -> (X+Y) -> Y :=
fun f u =>
  match u with
    inl x => f x
  | inr y => y
  end.

Definition disj_abs: (A->B) -> (A \/ B) -> B :=
fun h1 h2 =>
  match h2 with
    or_introl a => h1 a
  | or_intror b => b
  end.

Lemma disjunction_absorption: (A->B) -> (A \/ B) -> B.
Proof.
intros h1 h2.
elim h2.  (* "elim" does case analysis on an assumption. *)
exact h1. (* "exact" gives directly the proof of the goal. *)
trivial.  (* "trivial" proves easy goals automatically. *)
Qed.

Print disjunction_absorption.

Lemma or_impl_exchange:
  (A->B)\/(A->C) -> A -> (B\/C).
Proof.
intros h a.
elim h.
intro hab.
left.   (* "left" proves the first part of a disjunction. *)
apply hab.
exact a.
intro hac.
right.  (* "right" proves the second part of a disjunction. *) 
apply hac.
exact a.
Qed.

(* Negation ~A is just A->False. *)

Lemma contropositive: (A -> B) -> (~B -> ~A).
intros hab hnb.
(* red. *)
intro a.
(* red in hnb. *)
apply hnb.
apply hab.
exact a.
Qed.

End PropositionalLogic.