(* Additional Exercises 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 ExistsForall: forall (P : term -> term -> Prop), (exists y, forall x, P x y) -> (forall x, exists y, P x y). Proof. intro. intro. intro x0. destruct H as [y0 Hy0_fact]. exists y0. spec Hy0_fact x0. apply Hy0_fact. Qed.