(* 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.