(* CS3234, Martin Henz and Aquinas Hobor *) (* Quiz A on induction in Coq *) (* 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. Require Import Omega. Inductive Nat : Type := | Zero : Nat | Succ : Nat -> Nat. Inductive Tree : Type := | Leaf : Tree | Node : Tree -> Tree -> Tree. Fixpoint encode(n : Nat) : Tree := match n with | Zero => Leaf | Succ n' => Node Leaf (encode n') end. Fixpoint decode(t : Tree) : Nat := match t with | Leaf => Zero | Node t1 t2 => Succ (decode t2) end. (* 10 marks *) Lemma decode_encode: forall n, decode(encode n) = n. Proof. admit. Qed. (* 10 marks *) Lemma encode_decode: exists t, ~encode(decode t) = t. Proof. admit. Qed. Definition isEncoded (t : Tree) : Prop := exists n, t = encode n. (* Hint: the inversion tactic is your friend. *) (* 10 marks *) Lemma encode_decode2: forall t, isEncoded t -> encode(decode t) = t. Proof. admit. Qed.