Set Implicit Arguments. Require Import LibTactics. (* ********************************************************************** *) (** ** Definitions used in demos *) Variables H1 H2 H3 H4 H5 H6 : Prop. Variables P1 P2 P3 : nat -> Prop. (* ********************************************************************** *) (** ** Notation *) Lemma demo_exist : exists x1 x2 x3, x1 = x2 /\ x2 = x3 /\ x3 = 0. Proof. (* dup N makes N copies of the current goal, which is useful for demos *) dup 6. (* N-ary existentials are displayed in a packed way, and they can be instantiated at once *) exists 0 0 0. auto. (* [exists~ 0 0 0] is the same as [exists 0 0 0] followed with auto *) exists~ 0 0 0. (* if a wild-card is provided, an existential variable is introduced *) exists __ 0 __. skip. (* if a double wild-card is provided, as many existential as possible are introduced *) exists 0 ___. (* a shorthand for [exists __ __ __] is [exists___ 3] *) exists___ 3. skip. (* [exists___] without arguments is the same as [exists __ ... __]. Contrary to [exists ___], it does not unfold definitions. *) exists___. skip. Admitted. (* ********************************************************************** *) (** ** Assertions, cuts, contradiction *) Lemma demo_false_1 : forall (n:nat), (forall m, m = n -> False) -> H1. Proof. intros n P. dup 5. (* [false_goal] replaces the current goal by [False] *) false. eapply P. reflexivity. (* [false E] proves the goal if [E] has type [False] *) false (P n (refl_equal n)). (* [false E] is in fact the same as [false; apply E] *) false P. reflexivity. (* [false*] is short for [false; eauto] *) false*. (* [false] also tries and call [congruence] *) lets: (P n). false. Qed. Lemma demo_false_2 : 0 = 1 -> 1 = 2. Proof. intros. dup 3. (* [contradiction] does not cover [discriminate] *) try contradiction. skip. discriminate. (* while [false] covers [contradiction] and [discriminate] *) false. Qed. Lemma demo_false_3 : (forall b, b = false) -> False. Proof. introv H. dup. (* [false E] is able to use [forwards E] to exhibit a contradiction. *) false (>> H true). (* syntax [false E1 .. EN] is also available *) false H true. Qed. Lemma demo_tryfalse : forall n, S n = 1 -> n = 0. Proof. intros. dup 2. (* often in a case analysis, several subcases are absurd. example: *) destruct n. auto. false. (* [tryfalse] removes all the subcases solved by [false] *) destruct n; tryfalse. auto. Qed. Lemma demo_asserts_cuts : True. Proof. dup 7. (* here is another syntax for assert *) asserts U: H2. skip. skip. (* that allows for intro-patterns *) asserts [U V]: (H2 /\ H3). skip. skip. (* the intro-pattern [U [V W]] may be simply written U V W *) asserts U V W: (H2 /\ H3 /\ H4). skip. skip. (* this is also convenient for existentials *) asserts x y E F: (exists x y, S x = y /\ x > 0). skip. skip. (* if no pattern is provided, a fresh name is generated *) asserts: (H2 /\ H3). skip. skip. (* [asserts~] calls [auto] only on the asserted proposition. *) asserts~ U: (0 = 0). skip. (* [cuts] is like [asserts] except it swaps subgoals *) cuts U V: (H2 /\ H3). skip. skip. Qed. (* ********************************************************************** *) (** ** Assumptions *) Lemma demo_lets : (H1 -> H2 -> H3 /\ H4) -> (H1 -> H2) -> H1 -> H3. Proof. intros P Q R. (* [lets] is a tactic for naming a term *) lets U: (Q R). (* [lets] can decompose terms with a patterns *) lets [V W]: (P R U). (* again, the syntax for conjunctions applies *) lets V1 W1: (P R U). (* [lets] without an intro-pattern generates a fresh name *) lets: (P R). (* [lets] on an existing hypothesis makes a copy of it *) lets U': U. skip. Qed. (* ********************************************************************** *) (** * Apply *) Definition Dup x := x + x. Lemma demo_applys : forall P : (nat -> nat) -> nat -> Prop, (forall f, P f (f 0)) -> P Dup 0. Proof. intros. dup 4. (* while apply is able to do some unification *) apply (H Dup). (* since CoqV8.2, apply is able to do this unfolding *) apply H. (* before, one had to use [refine] *) refine (H _). (* [applys H] is simply [refine (H _ ... _)] with enough many underscores *) applys H. Qed. Lemma demo_applys_to : (H1 -> H2 -> H3 /\ H4) -> (H1 -> H2) -> H1 -> H3. Proof. introv P Q R. dup. (* [applys_to R] is used to apply a lemma to [R] and name R the result *) applys_to R Q. skip. (* another example *) applys_to R P. skip. Qed. (* ********************************************************************** *) (** * Introduction *) Section IntrovTest. Variables P1 P2 P3 : nat -> Prop. Lemma demo_introv_1 : forall a b, P1 a -> P2 b -> forall c d, P3 c -> P1 d -> c = b. Proof. dup 4. (* [introv] introduces all the variables which are not hypotheses, more precisely all the variables used dependently. *) introv. (* if there is no more head variables, and no definition can be unfolded at head of the goal, it does not do anything *) introv. skip. (* [introv A] introduces all variables, then does [intros A] *) introv A. introv B. introv. intros C D. skip. (* [introv] may take several arguments, as illustrated below *) introv A B. introv. skip. introv A B C D. skip. Qed. Definition Same (x y : nat) := True -> x = y. Definition Sym (x:nat) := forall y, x = y -> Same y x. Lemma demo_introv_2 : forall a, Sym a. Proof. dup 4. (* [introv] introduces a variable but no subsequent definition *) introv. (* [introv] unfolds definition if no variable is visible *) introv. skip. (* [introv E] unfolds definitions until finding an hypothesis *) introv E. introv F. skip. (* [introv E F] unfolds several definitions if needed *) introv E F. skip. (* [introv] may unfold definition without any introduction *) introv E. introv. skip. Qed. Lemma demo_introv_3 : forall a, a = 0 -> Sym a. Proof. dup 5. (* more examples *) (* introduces [a] only *) introv. skip. (* introduces [a = 0] *) introv E. skip. (* introduces [a = 0] and [a = y] *) introv E F. skip. (* introduces [a = 0] and [a = y] and [True] *) introv E F G. skip. (* introduction of more names fails *) try (introv E F G H). skip. Qed. Definition TestSym := (forall a, a = 0 -> Sym a). Lemma demo_introv_4 : TestSym. Proof. dup 2. (* same as before, except the goal itself is a definition *) (* introduces [a] only *) introv. skip. (* introduces [a = 0] *) introv E. skip. Qed. Lemma demo_introv_5 : forall a, a = 0 -> ~ Sym a. Proof. dup 2. (* playing with negation *) (* introduces [a = 0] *) introv E. skip. (* introduces [a = 0] and [Sym a] *) introv E F. skip. Qed. (* Iterated unfolding to get hypotheses *) Definition AllSameAs (x:nat) := forall y, Same y x. Definition AllSame := forall x, AllSameAs x. Lemma demo_introv_6 : AllSame. Proof. dup 2. (* introduces only [x], then only [y] *) introv. introv. skip. (* introduces [x] and [y] and [True] *) introv E. skip. Qed. Definition AllSameAgain := AllSame. Lemma demo_introv_7 : AllSameAgain. Proof. dup 2. (* introduces only [x], then only [y] *) introv. introv. skip. (* introduces [x] and [y] and [True] *) introv E. skip. Qed. Lemma demo_introv_8 : forall a (c:nat) b, P1 a -> P2 b -> True. Proof. (* notice that variables which are not used dependently are treated as hypotheses, e.g. variable [c] below. This might not be the desired behaviour, but that's all I'm able to implement in Ltac. *) introv c E F. skip. Qed. Definition IMP P A (x y : A) := P -> x = y. Lemma demo_intros_all : (forall a b, P1 a -> P2 b -> IMP H1 a b) /\ (forall a b, a = 0 -> b = 1 -> ~ (a = b)). Proof. split. (* [intros_all] introduces as many arguments as possible *) intros_all. skip. intros_all. skip. Qed. (* An example showing that [intro] is not very-well specified with respect to beta-reduction, explaining why [introv] isn't doing better. *) Definition testing f := forall (x:nat), f x -> True. Lemma demo_introv_what_to_do : testing (fun a => a = 0). Proof. dup. intro. skip. (* does beta-reduce f *) hnf. intro. skip. (* does not beta-reduce f *) Qed. End IntrovTest. (* ********************************************************************** *) (** * Generalization, naming *) Lemma demo_gen_and_generalizes : forall P Q : nat -> nat -> nat -> Prop, forall a b c, P a b c -> Q a a a -> P b b c -> True. Proof. intros. dup 3. (* [gen] generalizes an hypothesis and clears it *) gen H. skip. (* it generalizes all the dependencies of a variable *) gen a. skip. (* it also works for several variables at once *) gen b c. skip. Qed. Inductive ind : nat -> Prop := | ind_0 : ind 0 | ind_S : forall n, ind n -> ind (S n) | ind_SS : forall n, ind n -> ind (S (S n)) | ind_P : forall (A:Type) (P:A->Prop) (f:A->nat) (a:A), ind (f a) -> P a -> ind (S (f a)). Lemma demo_sets_and_set_eq_and_sets_eq : forall n, ind (3 + n) -> ind (7 + n) -> ind (7 + n). Proof. introv M1 M2. dup 9. (* [sets] introduces a name and performs the substitution *) sets a: (3+n). skip. sets b: (7+n). skip. (* [set_eq] introduces an equality *) set_eq a Ha: (7+n). skip. (* [sets_eq] introduces an equality and substitutes *) sets_eq a Ha: (7+n). skip. (* the name of the hypothesis can be generated *) sets_eq a: (7+n). skip. (* the name of the variable can also be generated *) sets_eq: (7+n). skip. (* [set_eq in H] performs the substitution in [H] *) set_eq a: (7+n) in M2. skip. (* [set_eq in |-] performs no substitution *) set_eq a: (7+n) in |-. skip. (* [set_eq <-] generates the equality [7+n=a] *) sets_eq <- a: (7+n). skip. Qed. Lemma demo_sets_let_and_sets_eq_let : forall n1 n2 : nat, (let x := n1 + n2 in x = x) -> (let y := n2 + n1 in let z := y + y in z = z) -> (let t := n1 + n1 in t = t). Proof. intros n1 n2 M1 M2. dup 3. (* [sets_let x] introduces a local definition for a let; note that, due to a limitation of Coq, only one local binding can be named! *) sets_let a. sets_let b. sets_let c. auto. (* the hypothesis where to look can be specified *) sets_let a in M1. auto. (* [sets_eq_let] introduces explicit equalities like [sets_eq] *) sets_eq_let a. sets_eq_let b. sets_eq_let c. auto. Qed. (* ********************************************************************** *) (** * Unfolding *) Definition Id A (x:A) := x. Lemma demo_unfolds_folds : forall a b, a = Id(b) -> Dup a = 0 -> Dup b = Id(0+0). Proof. intros. dup 2. (* [unfolds] is same as [unfold in *] *) unfolds Dup. skip. (* [unfolds] can take several arguments *) unfolds Id,Dup. subst b. (* [folds] is same as [fold in *]. *) folds (Dup a). skip. Qed. Definition Twice (P:Prop) := True -> P /\ P. Lemma demo_unfolds_head_definition : forall P:Prop, (True -> P) -> Twice P -> Twice P. Proof. introv A B. (* [unfolds] without arguments unfolds the head definition *) unfolds. (* it also applies to an hypothesis *) unfolds in B. skip. Qed. (* ********************************************************************** *) (** * Simplification *) Lemma demo_simpls_and_unsimpl : forall a b, Dup a = (1+1) -> Dup b = Id(0+0). Proof. intros. (* [simpls] is same as [simpl in *] *) simpls. (* [unsimpl] can be used to undo a simplification *) unsimpl (0+0). unsimpl (2+0) in H. skip. Qed. (* ********************************************************************** *) (** * Substitution *) Lemma demo_substs_1 : forall a b c d e : nat, a = b -> b = c -> d = e -> e = d -> P1 d -> P2 a -> P3 c. Proof. introv P Q R U V. dup 2. (* [subst] does not work with circular equalities *) try subst. skip. (* [substs] does work however *) substs. skip. Qed. Lemma demo_substs_2 : forall x y (f:nat->nat), x = f x -> y = x -> y = f x. Proof. intros. (* [subst] does not work *) try subst. (* [substs] does work *) substs. assumption. Qed. Lemma subst_hyp_demo : forall (x y x' y' z z' : nat) (P:nat->Prop), (x,y,z) = (x',y',z') -> P x -> P x' -> P y -> P y' -> P z -> P z' -> z = z'. Proof. introv H. intros. subst_hyp_base H. auto. Qed. (* ********************************************************************** *) (** * Rewriting *) Lemma demo_rewrites : (forall n m, m + n = n + m) -> 3 + 4 = 7. Proof. introv H. dup. (* [rewrites] support the [rm] identity tag to remove hypothesis *) rewrites (rm H). skip. (* [rewrites] can take arguments like [forwards] -- see further *) rewrites (>> H __ 3). skip. Qed. Lemma demo_rewrites_at : forall x y z, x = y + y -> x + x = z -> z + z = x + x + x + x. Proof. introv E H. dup. (* [rewrite] rewrites in all similar occurences *) rewrite E. skip. (* [rewrites at] can be used to control the target of rewrite *) rewrites E at 2. rewrites E at 2 in H. rewrites <- H at 2. skip. Qed. Lemma demo_rewrite_all : (forall n, n + 0 = 0 + n) -> (3 + 0) + 0 = 5 + 0. Proof. intros E. (* [rewrite_all] is same as [repeat rewrite] *) rewrite_all E. skip. Qed. Lemma demo_asserts_and_cuts_rewrite : forall n, 0 < n < 2 -> P1 1 -> P1 n. Proof. introv Lt H. dup 2. (* [asserts_rewrite] rewrites and generates a proof obligation *) asserts_rewrite (n = 1). skip. skip. (* same for [cuts_rewrite], except the subgoals are swapped *) cuts_rewrite (n = 1). skip. skip. Qed. Lemma demo_replaces : forall a b, a = b + b -> a + a + a = 3 * a. Proof. intros. dup 3. (* [replaces] replaces all occurences (the equality subgoal is first) *) replaces a with 3. skip. skip. (* [replaces at] replaces at a given occurence *) replaces a at 2 with 5. skip. skip. (* [replaces] and [replaces at] works in hypotheses *) replaces b at 2 with 4 in H. skip. skip. Qed. Lemma demo_pi_rewrite : forall (P:Prop) (X:P->nat) (p1 p2:P), X p1 + X p2 = X p2 + X p1. Proof. (* [pi_rewrite E] replaces any proposition [E] with an evar of the same type. This is very useful when working with terms that are unifiable modulo proof irrelevance *) intros. pi_rewrite p1. reflexivity. Qed. (* ********************************************************************** *) (** * Inversions *) Inductive even_shift : nat -> nat -> Prop := | even_0 : even_shift 0 2 | even_SS : forall n m, even_shift n m -> even_shift (S (S n)) (S (S m)). Lemma demo_invert : even_shift 4 8 -> False. Proof. intros P. dup 12. (* [inversion] generates a lot of ugly stuff *) inversion P. inversion H7. inversion H10. (* [inversions H] is short for [inversion H; subst; clear H] *) inversions P. inversions H7. inversions H8. (* [invert] is same as [inversion H; clear H] except that it generalizes the generated hypotheses so that they can be named manually using intros or introv *) invert P. introv P' EQ1 EQ2. skip. (* [invert as] can be used to name the generated hypotheses directly, in the [introv] fashion *) invert P as P' EQ1 EQ2. skip. (* [inverts] does the same as [inversion; clear], then it substitutes all the generated equalities (and only these fresh equalities, not the older ones) *) inverts P. inverts H7. inverts H8. (* it is /sometimes/ possible to name the resulting hypotheses *) inverts P as P'. inverts P' as P''. inverts P''. (* it is even possible to reuse the same name *) inverts P as P. inverts P as P. inverts P. (* [invert as] without arguments leaves the hypotheses that have been generated in the goal *) inverts P as. introv P'. skip. (* one may add the keyword [keep] in order to keep the inverted hypothesis *) invert keep P. intros. skip. inverts keep P as P' EQ1 EQ2. skip. inverts keep P as. introv P'. skip. (* [lets_inverts] need to be used to invert expressions that are not simply the name of an hypothesis *) lets_inverts (conj P P) as H1 H2. skip. Qed. Inductive Behave : Type := | Behave_intro : forall (A:Type) (F:A->nat) (P:A->Prop), Behave. Inductive behave : nat -> Behave -> Prop := | behave_intro : forall (A:Type) (F:A->nat) (P:A->Prop) V, P V -> behave (F V) (@Behave_intro A F P). Lemma demo_dependent_invert : behave 4 (Behave_intro (fun x:nat => x) (fun x:nat => x <> 3)) -> False. Proof. intros H. dup 3. (* [inversion] can generate some dependently-typed equalities *) inversion H. (* look at H9 and H10 *) skip. (* [inverts] carries out all the substitution properly *) inverts H. skip. (* again, it is possible to name the new hypotheses *) inverts H as R1 R2 R3. skip. Qed. Lemma demo_inject_and_injects : forall a b c, (a,b,c) = (1,2,3) -> b = 2. Proof. introv EQ. dup 5. (* [injection] generates some equalities in the goal *) injection EQ. skip. (* [inject] does the same *) inject EQ. skip. (* but it is also able to name these hypotheses *) inject EQ as EQ1 EQ2 EQ3. skip. (* and [injects] can substitute these hypotheses *) injects EQ. skip. (* it also works if the equalities are in the other direction *) symmetry in EQ. injects EQ. skip. Qed. (* ********************************************************************** *) (** * Case_if *) Lemma demo_case_if : forall b c :bool, (if b then true else true) = false -> (if c then true else true) = true. Proof. intros. dup 4. case_if. auto. auto. case_if as P. auto. auto. case_if in H. case_if in H as P. Qed. (* ********************************************************************** *) (** * F_equal *) Lemma demo_fequals_1 : forall a b c d, b = d -> d = 2 -> a = 1 -> (a,b,c) = (1,2,3). Proof. intros. dup 3. (* [f_equal] is not really clever on tuples *) f_equal. f_equal. skip. skip. skip. (* while [fequal] works better *) fequal. skip. skip. skip. (* even more useful, [fequals] tries to discharge the easy subgoals using [reflexivity] and [congruence] *) fequals. skip. Qed. Lemma demo_fequals_2 : forall f a b c d, b = d -> d = 2 -> a = 1 -> f a b c = f 1 2 3 :> nat. Proof. intros. dup 2. (* [fequal] and [fequals] also work for functions, of course *) fequal. skip. skip. skip. fequals. skip. Qed. (** [fequals] supports proof irrelevance *) Lemma demo_fequal_post : forall (P:Prop) (X:P->nat) (p1 p2:P), X p1 = X p2. Proof. intros. fequals. Qed. (* ********************************************************************** *) (** * Induction *) Inductive natequal : nat -> nat -> Prop := | natequal_O : natequal 0 0 | natequal_S : forall n, natequal n n -> natequal (S n) (S n). induction H. skip. skip. (* but [inductions], based on [dependent induction], does work. *) inductions H gen n m p. skip. skip. Qed. Lemma demo_inductions' : forall n m, natequal (n + m) 0 -> n = 0. Proof. intros. dup. (* same *) induction H. skip. skip. (* correct version *) inductions H gen n m. skip. Qed. *) (* ********************************************************************** *) (** ** N-ary splitting and branching *) Definition test_split_1 := H1 /\ H2 /\ H3. Definition test_split_2 := H4 /\ H5 /\ H6 /\ test_split_1. Definition test_split_3 := test_split_2. Lemma demo_splits : test_split_3. Proof. dup 5. (* spliting a bunch of conjunction is a pain *) split. skip. split. skip. split. skip. split. skip. skip. (* [splits_all] is short for [repeat split] *) splits_all. skip. skip. skip. skip. skip. skip. (* but it is sometimes too aggressive. *) (* [splits N] splits a conjunction in N parts *) splits 4. skip. skip. skip. skip. splits 3. skip. skip. skip. (* [splits] is able to guess the appropriate arity *) splits. skip. skip. skip. splits. skip. skip. skip. Qed. Lemma demo_branch : 1 = 2 \/ 2 = 3 \/ 3 = 4 \/ 4 = 4 \/ 4 = 5 \/ 5 = 6. Proof. dup 6. (* [branch K of N] is used to select a branch of a disjunction *) branch 1 of 6. skip. branch 4 of 6. auto. branch 6 of 6. skip. (* [branch] can usually guess the appopriate arity *) branch 1. skip. branch 4. auto. branch 6. skip. Qed. Lemma demo_destructs : 1 = 2 /\ (2 = 3 /\ 3 = 4) /\ 4 = 5 -> True. Proof. intros H. destructs H. skip. Qed. (* ********************************************************************** *) (** * Hide, clears, sorts *) Parameter lemma_hide : forall n, n + 0 = n. Lemma demo_hide_hyps : forall x:nat, x + 0 = x. Proof. intros. (* Any term admits the type [Something] *) generalize (lemma_hide : Something). intros H. generalize (lemma_hide : Something). intros H'. (* [show_hyp H] unfolds the definition of [Something] *) show_hyp H. (* [hide_hyp H] reveals the definition of [Something] *) hide_hyp H. (* [show_hyps] and [hide_hyps] apply to all hypotheses of sort Prop *) show_hyps. hide_hyps. (* Hidden terms remain convertible with their original value *) hnf in H. apply H'. Qed. Lemma demo_hide_def : forall x:nat, let y := x + x in let z := y in y + 0 = y. Proof. intros. (* [hide_def x] hides the body of a definition *) hide_def y. hide_def z. (* [show_def x] reveals the body of a definition *) show_def y. show_def z. (* [hide_defs] and [show_defs] applies to all definitions *) hide_defs. show_defs. (* [show_def] can be used to unfold [Something] in the goal *) hide_def y. unfold y. show_def. Admitted. Lemma demo_hide_generic : forall x:nat, let y := x + x + x + x in let z := y in y + 0 = y. Proof. intros. generalize (lemma_hide). intros H. (* [hide]/[show] work both for definition and hypotheses *) hide H. hide y. show H. show y. (* [hide_all]/[show_all] hide everything *) hide_all. show_all. (* Observe that substitution of hidden terms may require several unfolding. *) hide_all. subst y. show_def z. show_def z. (* The tactic [show_all] reveals everything at once *) show_all. hide_all. apply H. Qed. Lemma demo_hide_term : forall x, x + x + x = 3. Proof. intros. (* using [hide_term E] and [show_term] *) hide_term (x+x+x). show_term. (* typically used in a pattern matching *) match goal with |- ?T = _ => hide_term T end. Admitted. Lemma demo_clears : forall (x y z : nat) (A B : Prop), (x > 0) -> (x <> y) -> (A <-> B) -> True. Proof. introv z Pos Neq Iff. dup 5. (* [clears] is like [clear] except it clears all dependencies *) clears y. skip. clears x. skip. clears x y. skip. clears Neq A. skip. (* [clears] without arguments clears only unused variables (which are not propositions) *) clears. skip. Qed. Lemma demo_sort : forall n : nat, n > 0 -> forall P Q : Prop, (P <-> Q) -> forall m : nat, m <> n -> forall K : nat -> Prop, K n -> forall p, K (m+p) -> True. Proof. intros. (* [sort] puts all the proposition at the bottom of the context *) sort. skip. Qed. (* ********************************************************************** *) (** * Skip *) Lemma demo_skip : forall n m p : nat, n > m -> m >= p -> n > p. Proof. intros. dup 6. (* [skip H: E] is used to admit a new fact *) skip R1: (m = m). skip. skip R1 R2: (m = m /\ n > m+1). skip. skip q Q: (exists q, q > p). skip. skip: (m <> n). skip. (* [skip_rewrite E] is used to admit a fact E and rewrite it *) skip_rewrite (m = n) in H0. skip. (* [skip_induction] is used to do an induction and cheat on the induction hypothesis, by having it as strong as the initial goal *) dup. induction p. skip. skip. skip_induction p. skip. skip. Qed. Lemma demo_skip_with_existential : False. Proof. dup. (* [skip'] is the alternative implementation of [skip], which forbits [Qed] to be written at the end of the proof *) skip'. skip'. Admitted. (* ********************************************************************** *) (** ** Advanced instantiation *) (* Note: the use of "instantiation modes" is described in the overview file and described in full details in the source file LibTactics.v *) Lemma demo_lets_of : forall (x y : nat) (A B : Prop), (x > 0) -> (x <> y) -> (A <-> B) -> (forall n, n > 0 -> forall m, n <> m -> exists k, k <> m) -> (forall n : nat, n > 0 -> forall P Q : Prop, (P <-> Q) -> forall m : nat, n <> m -> forall K : nat -> Prop, K n -> forall p, K (m+p) -> True) -> True. Proof. introv Pos Neq Iff L M. (* [lets] is used to instantiate a lemma [M] on arguments *) lets P: M Iff. eauto. clear P. lets P: (>> M Neq). eauto. eauto. clear P. lets P: (>> M __ y). eauto. eauto. clear P. lets P: (>> M x __ B). eauto. instantiate (1:=A) in P. clear P. (* [Hnts] keyword can be omitted *) lets P: (>> M __ y Neq). eauto. eauto. clear P. (* The syntax [>>] is not required for less than 5 arguments. *) lets P: M Pos A B Neq. eauto. clear P. (* A triple underscore indicates to instantiate all remaining *) lets k K: (>> L Pos ___). eauto. clears k. lets k K: (>> L ___). eauto. eauto. clears k. (* [forwards I: (>> E E1 .. EN)] is short for [lets I: (>> E E1 .. EN ___)] *) forwards R: L. eauto. eauto. clear R. forwards R: L Pos. eauto. clear R. forwards k K: L. eauto. eauto. clears k. forwards [k K]: L Pos y. eauto. clears k. forwards k K: (>> L x y). eauto. eauto. clears k. lets k K: (>> L Neq). eauto. clears k. auto. Qed. Lemma demo_forwards_1 : forall x : nat, x > 1 -> (forall z, z > 1 -> exists y, z < 2 /\ z <> y) -> True. Proof. introv Le H. dup 4. (* [forwards] is used to instantiate a lemma entirely, generating one subgoal for each hypothesis and one existential variable for each universally quantified variable *) forwards Q: H. eauto. skip. (* an introduction-pattern can be used to decompose the result *) forwards [y [R1 R2]]: H. eauto. skip. (* and [forwards] can also be used without introduction pattern *) forwards: H. eauto. skip. (* [forwards] does nothing on an hypothesis without quantifiers *) forwards: Le. skip. Qed. Lemma demo_forwards_2 : (forall x y : nat, x = y -> x <= y) -> forall a b : nat, a <= a. Proof. intros. dup. (* some more examples *) forwards K: (H a). reflexivity. apply K. forwards* K: (H a). Qed. Lemma demo_applys_specializes : forall (x y : nat) (A B : Prop), (x > 0) -> (x <> y) -> (A <-> B) -> (forall n : nat, n > 0 -> forall P Q : Prop, (P <-> Q) -> forall m : nat, m <> n -> True) -> True. Proof. introv Pos Neq Iff M. dup 17. (* [applys] is used to apply an instantiated lemma. *) applys (>> M Pos). eauto. eauto. applys (>> M A B). eauto. eauto. eauto. applys (>> M Pos Iff). eauto. applys (>> M Iff). eauto. eauto. applys (>> M x Iff). eauto. eauto. applys M x Iff. eauto. eauto. (* [specializes] is used to instantiate an hypothesis in-place *) specializes M (>> 3). auto. specializes M (>> 3 A B). auto. auto. specializes M (>> A __ __). eauto. eauto. auto. specializes M (>> Pos Iff 2). eauto. auto. (* A triple underscore indicates to instantiate all remaining *) specializes M (>> Pos ___). eauto. eauto. auto. specializes M (>> __ B ___). eauto. eauto. eauto. auto. specializes M __. specializes M __. eauto. auto. (* [specializes] can be used as [forwards in] thanks to [___] *) specializes M ___. eauto. eauto. eauto. auto. (* In those tactics, one can apply the constant [rm] to any subterm to request the argument of [rm] to be removed from the context. *) applys (>> M (rm Pos) Iff). (* [Pos] is gone here *) eauto. (* In fact, [rm] can be applied in depth inside terms *) specializes M (>> (proj1 (conj (rm Pos) Neq))). (* [Pos] is gone *) auto. Qed. (** Similar demos, showing how head definitions are unfolded *) Definition mydef := forall (n m : nat), n = m -> False. Lemma demo_specializes_definition : forall (i:nat), mydef -> i <> i. Proof. introv H. dup 6. (** specializes one by one *) specializes H i. specializes H i. specializes H (refl_equal i). false. (** specializes all arguments *) specializes H i i (refl_equal i). false. (** specializes skipping some arguments *) specializes H (refl_equal i). false. (** forwards all arguments *) forwards: H. apply (refl_equal i). false. (** forwards on one arguments *) forwards M: H i. reflexivity. false. (** build using lets *) lets: (>> H (refl_equal i)). false. Qed. (** Unfolding occurs recursively *) Definition outerdef := mydef. Lemma demo_specializes_definition_2 : forall (i:nat), outerdef -> i <> i. Proof. introv H. dup 6. (** specializes one by one *) specializes H i. specializes H i. specializes H (refl_equal i). false. (** specializes all arguments *) specializes H i i (refl_equal i). false. (** specializes skipping some arguments *) specializes H (refl_equal i). false. (** forwards all arguments *) forwards: H. apply (refl_equal i). false. (** forwards on one arguments *) forwards M: H i. reflexivity. false. (** build using lets *) lets: (>> H (refl_equal i)). false. Qed. (** On the other hand, definitions that are not at head position are not unfolded *) Definition nesteddef := forall (n:nat), mydef. Lemma demo_specializes_definition_3 : forall (i:nat), nesteddef -> outerdef. Proof. intros i H. dup 4. (** forwards does not instantiate [mydef] from [H] *) forwards K: H i. skip. (** ... unless explicitely visible *) unfold nesteddef, mydef in H. forwards K: H i. apply (refl_equal i). false. (** yet, it should be possible to instantiate arguments inside [mydef] if providing explicit arguments *) lets K: (>> H i i). skip. lets K: (>> H i (refl_equal i)). skip. Qed. (* ********************************************************************** *) (** ** Introduction of equalities to enable [apply] to work *) Lemma demo_ereplace_working : forall (P:nat->nat->Prop) x y, (forall n, P n n) -> (x > 0 -> x = y) -> (x > 0) -> P x y. Proof. introv H E L. dup 3. (* here, the hypothesis [P n n] cannot be applied directly *) try apply H. (* however, we really want to be able to apply it *) eapply equates_2. apply H. auto. (* this is particularly useful for automation *) eapply equates_2; eauto. (* the tactic [equates] inputs the position where evars should be introduced in place of arguments; the indices are to be counted from the right. *) equates 2. skip. skip. Admitted. Lemma demo_equates_non_dep : forall (P:nat->nat->nat->Prop) x y z, P x y z. Proof. intros. dup 5. equates 1. skip. skip. equates 2. skip. skip. equates 3. skip. skip. (* multiple [equates] are allowed *) equates 1 2. skip. skip. skip. equates (>> 1 2). skip. skip. skip. Admitted. Lemma demo_equates_dep : forall (P:nat->forall A, A->Prop) x (T:Type) z, P x T z. Proof. intros. dup 3. equates 1. skip. skip. (* replacement of dependent hypotheses is not allowed *) try equates 2. equates 3. skip. skip. equates 1 3. skip. skip. skip. Admitted. (* ********************************************************************** *) (** ** Induction on height of a derivation *) Section IndHeight. (** Lambda calculus *) Inductive trm : Type := | trm_var : nat -> trm | trm_abs : nat -> trm -> trm | trm_app : trm -> trm -> trm. Parameter subst : nat -> trm -> trm -> trm. (** Original big-step reduction judgment *) Inductive bigred : trm -> trm -> Prop := | bigred_val : forall v, bigred v v | bigred_abs : forall x t, bigred (trm_abs x t) (trm_abs x t) | bigred_app : forall t1 t2 x t3 v2 v, bigred t1 (trm_abs x t3) -> bigred t2 v2 -> bigred (subst x v2 t3) v -> bigred (trm_app t1 t2) v. (** Same judgment, with an index to bound the height *) Inductive bigredh : nat -> trm -> trm -> Prop := | bigredh_val : forall n v, bigredh (S n) v v | bigredh_abs : forall n x t, bigredh (S n) (trm_abs x t) (trm_abs x t) | bigredh_app : forall n t1 t2 x t3 v2 v, bigredh n t1 (trm_abs x t3) -> bigredh n t2 v2 -> bigredh n (subst x v2 t3) v -> bigredh (S n) (trm_app t1 t2) v. Require Import Omega. Hint Extern 1 ((_ < _)%nat) => omega. Hint Constructors bigred bigredh. Lemma bigredh_lt : forall n n' t v, bigredh n t v -> (n < n')%nat -> bigredh n' t v. Proof. introv H. gen n'. induction H; introv L; (destruct n' as [|n']; [ false; omega | auto* ]). Qed. Lemma bigredh_bigred : forall n t v, (* optional *) bigredh n t v -> bigred t v. Proof. introv H. induction* H. Qed. Lemma bigred_bigredh : forall t v, bigred t v -> exists n, bigredh n t v. Proof. hint bigredh_lt. introv H. induction H; try induct_height. Qed. (** After exploiting this last lemma, it is possible to perform an induction on the height of a derivation by doing [induction n]. *) End IndHeight. |