(* Midterm solutions in Coq *) (* Preparation for Coq Quiz *) (* 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 *) Tactic Notation "LEM" constr(a) := destruct (classic a). 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. (* Coq Exercise *) (* The following material is for your practice at using predicate logic in Coq. I have done some of the problems, and you should do the others, learning from my examples if you like. *) Parameter term : Type. (* To fully appreciate the proof below, write the proof first in text-based table form. *) Lemma Q8: forall (P Q: term -> Prop), forall x, (forall x, (P x -> ~ Q x)) -> Q x -> ~ P x. Proof. intros. assert (P x -> ~ Q x). apply H. intro. assert (~ Q x). apply H1. apply H2. unfold not in H3. apply H3. trivial. Qed. Lemma Q9: forall (P Q: term -> Prop), (exists x, forall y, P y -> Q x) -> (~ exists x, ~ exists y, P x -> Q y). Proof. intros. intro. destruct H0 as [x0 Hx0]. unfold not in Hx0. apply Hx0. destruct H as [y0 Hy0]. exists y0. apply Hy0. Qed. Lemma Q10: forall (P Q: term -> Prop), (exists x, forall y, P y -> Q x) -> exists x, P x -> Q x. Proof. intros. destruct H as [x0 Hx0]. exists x0. spec Hx0 x0. apply Hx0. Qed.