(* Coq Homework on Propositional Logic in Coq *) (* CS3234, Martin Henz and Aquinas Hobor *) (* A little black magic to make sure that "*" is the product constructor on types instead of the multiplication operator on nat. *) Open Local Scope type_scope. (* Some useful tactics *) Tactic Notation "spec" hyp(H) := match type of H with ?a -> _ => let H1 := fresh in (assert (H1: a); [|generalize (H H1); clear H H1; intro H]) end. Tactic Notation "spec" hyp(H) constr(a) := (generalize (H a); clear H; intro H). Tactic Notation "spec" hyp(H) constr(a) constr(b) := (generalize (H a b); clear H; intro H). Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) := (generalize (H a b c); clear H; intro H). Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) constr(d) := (generalize (H a b c d); clear H; intro H). Tactic Notation "spec" hyp(H) constr(a) constr(b) constr(c) constr(d) constr(e) := (generalize (H a b c d e); clear H; intro H). Ltac remembertac2 x a := let x := fresh x in let H := fresh "Heq" x in (set (x:=a) in *; assert (H: a=x) by reflexivity; clearbody x). Tactic Notation "cases" constr(a) := let x := fresh in (remembertac2 x a; destruct x). Require ClassicalFacts. (* no axioms in this line *) Require Export Coq.Logic.ClassicalChoice. (* Axioms dependent_unique_choice, relational_choice *) Axiom dep_extensionality: forall (A: Type) (B: A -> Type) (f g : forall x: A, B x), (forall x, f x = g x) -> f = g. Implicit Arguments dep_extensionality. Axiom prop_ext: ClassicalFacts.prop_extensionality. Implicit Arguments prop_ext. Inductive Num : Type := | Zero : Num | Succ : Num -> Num. Definition Atom : Type := Num. Definition p_0 : Atom := Zero. Definition p_1 : Atom := Succ Zero. Definition p_2 : Atom := Succ (Succ Zero). Record Bool : Type := | T : Bool | F : Bool. Definition Valuation : Type := Atom -> Bool. Definition exampleValuation : Valuation := fun a : Atom => match a with | Zero => T (* p_0 *) | Succ Zero => F (* p_1 *) | Succ (Succ Zero) => T (* p_2 *) | _ => F (* all other *) end. Inductive PropFormula : Type := | propTop : PropFormula | propBot : PropFormula | propAtom : Atom -> PropFormula | propNeg : PropFormula -> PropFormula | propConj : PropFormula -> PropFormula -> PropFormula | propDisj : PropFormula -> PropFormula -> PropFormula | propImpl : PropFormula -> PropFormula -> PropFormula. Definition exampleFormula : PropFormula := propDisj (propNeg (propAtom p_2)) (propImpl (propConj (propAtom p_1) propTop) propBot). Fixpoint eval (f : PropFormula) (v : Valuation) : Bool := match f with | propTop => T | propBot => F | propAtom a => v(a) | propNeg f1 => match (eval f1 v) with | F => T | T => F end | propConj f1 f2 => match (eval f1 v, eval f2 v) with | (F, F) => F | (F, T) => F | (T, F) => F | (T, T) => T end | propDisj f1 f2 => match (eval f1 v, eval f2 v) with | (F, F) => F | (F, T) => T | (T, F) => T | (T, T) => T end | propImpl f1 f2 => match (eval f1 v, eval f2 v) with | (F, F) => T | (F, T) => T | (T, F) => F | (T, T) => T end end. Goal (eval exampleFormula exampleValuation) = T. reflexivity. Qed. Module Type PROP_PROOF_RULES. Section RULES. Variable v : Valuation. Definition holds (f : PropFormula) : Prop := eval f v = T. Axiom Top_I : holds propTop. Axiom Conj_I : forall f1 f2, holds f1 -> holds f2 -> holds (propConj f1 f2). Axiom Conj_E1 : forall f1 f2, holds (propConj f1 f2) -> holds f1. Axiom Conj_E2 : forall f1 f2, holds (propConj f1 f2) -> holds f2. Axiom NegNeg_E : forall f, holds (propNeg (propNeg f)) -> holds f. Axiom Impl_I : forall f1 f2, (holds f1 -> holds f2) -> holds (propImpl f1 f2). Axiom Impl_E : forall f1 f2, holds (propImpl f1 f2) -> holds f1 -> holds f2. Axiom Disj_I1 : forall f1 f2, holds f1 -> holds (propDisj f1 f2). Axiom Disj_I2 : forall f1 f2, holds f2 -> holds (propDisj f1 f2). Axiom Disj_E : forall f1 f2 f3, holds (propDisj f1 f2) -> (holds f1 -> holds f3) -> (holds f2 -> holds f3) -> holds f3. Axiom Bot_E : forall f, holds propBot -> holds f. Axiom Neg_E : forall f, holds f -> holds (propNeg f) -> holds propBot. Axiom Neg_I : forall f, (holds f -> holds propBot) -> holds (propNeg f). End RULES. End PROP_PROOF_RULES. (* Coq Quiz A *) Module CoqQuizA(PR : PROP_PROOF_RULES). Import PR. Opaque holds. (* So that you can use LEM if you prefer, I provide a proof here. If you want to use it, use "apply LEM." *) Lemma LEM : forall v F, holds v (propDisj F (propNeg F)). Proof. intros. apply NegNeg_E. apply Neg_I. intro. apply Neg_E with F0. apply NegNeg_E. apply Neg_I. intro. apply Neg_E with (propDisj F0 (propNeg F0)). apply Disj_I2. trivial. trivial. apply Neg_I. intro. apply Neg_E with (propDisj F0 (propNeg F0)). apply Disj_I1. trivial. trivial. Qed. Lemma Problem1A : forall P Q R v, holds v (propImpl (propDisj (propConj P Q) (propConj P R)) (propConj P (propDisj Q R))). Proof. admit. Qed. Lemma Problem2A : forall v P Q R, holds v (propImpl (propImpl P (propNeg Q)) (propImpl (propImpl (propDisj R (propNeg R)) Q) (propNeg P))). Proof. admit. Qed. Lemma Problem3A: forall v P, holds v (propImpl (propNeg (propNeg (propNeg P))) (propImpl P (propImpl P (propNeg P)))). Proof. admit. Qed. End CoqQuizA.