(* CS3234, Martin Henz and Aquinas Hobor *) (* Quiz B 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. (* Consider the following definition of trees with data at their nodes and leaves. Note we use the built-in nat type so we can use omega. *) Inductive DTree : Type := | DLeaf : nat -> DTree | DNode : nat -> DTree -> DTree -> DTree. (* DTree less than or equal : every nat in this tree is <= n *) Fixpoint DT_lte (dt : DTree) (n : nat) : Prop := match dt with | DLeaf n' => n' <= n | DNode n' dtl dtr => n' <= n /\ DT_lte dtl n /\ DT_lte dtr n end. (* DTree greater than or equal : every nat in this tree is >= n *) Fixpoint DT_gte (dt : DTree) (n : nat) : Prop := match dt with | DLeaf n' => n' >= n | DNode n' dtl dtr => n' >= n /\ DT_gte dtl n /\ DT_gte dtr n end. (* Every nat in the left tree is <= n and every nat in the right tree is >= n *) Fixpoint ordered (dt : DTree) : Prop := match dt with | DLeaf _ => True | DNode n dtl dtr => ordered dtl /\ ordered dtr /\ DT_lte dtl n /\ DT_gte dtr n end. (* Get the rightmost element *) Fixpoint rightmost(dt : DTree) : nat := match dt with | DLeaf n => n | DNode _ _ dtr => rightmost dtr end. (* 10 marks *) Lemma DT_lte_upwards_closed: forall dt n, DT_lte dt n -> forall m, n <= m -> DT_lte dt m. Proof. admit. Qed. (* 10 marks *) Lemma rightmost_ordered_lower: forall t n, ordered t -> DT_gte t n -> n <= rightmost t. Proof. admit. Qed. (* You will want to use the above two lemmas to prove this one; just use, for example, "apply rightmost_ordered_lower", etc. to use them. You might find the "apply ... with ..." construct useful too. *) (* 10 marks *) Lemma rightmost_bounds: forall t, ordered t -> DT_lte t (rightmost t). Proof. admit. Qed.