Mercurial > cpdt > repo

comparison src/Match.v @ 465:4320c1a967c2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Spell check
author Adam Chlipala <adam@chlipala.net>
date Wed, 29 Aug 2012 18:26:26 -0400
parents 38549f152568
children 1fd4109f7b31
comparison
equal deleted inserted replaced
464:e53d051681b0 465:4320c1a967c2
671 (Q --> P x /\ R) 671 (Q --> P x /\ R)
672 -> (Q --> ex P /\ R). 672 -> (Q --> ex P /\ R).
673 imp. 673 imp.
674 Qed. 674 Qed.
675 675
676 (** We will also want a "base case" lemma for finishing proofs where cancelation has removed every constituent of the conclusion. *) 676 (** We will also want a "base case" lemma for finishing proofs where cancellation has removed every constituent of the conclusion. *)
677 677
678 Theorem imp_True : forall P, 678 Theorem imp_True : forall P,
679 P --> True. 679 P --> True.
680 imp. 680 imp.
681 Qed. 681 Qed.
749 749
750 (** * Creating Unification Variables *) 750 (** * Creating Unification Variables *)
751 751
752 (** A final useful ingredient in tactic crafting is the ability to allocate new unification variables explicitly. Tactics like [eauto] introduce unification variables internally to support flexible proof search. While [eauto] and its relatives do _backward_ reasoning, we often want to do similar _forward_ reasoning, where unification variables can be useful for similar reasons. 752 (** A final useful ingredient in tactic crafting is the ability to allocate new unification variables explicitly. Tactics like [eauto] introduce unification variables internally to support flexible proof search. While [eauto] and its relatives do _backward_ reasoning, we often want to do similar _forward_ reasoning, where unification variables can be useful for similar reasons.
753 753
754 For example, we can write a tactic that instantiates the quantifiers of a universally quantified hypothesis. The tactic should not need to know what the appropriate instantiantiations are; rather, we want these choices filled with placeholders. We hope that, when we apply the specialized hypothesis later, syntactic unification will determine concrete values. 754 For example, we can write a tactic that instantiates the quantifiers of a universally quantified hypothesis. The tactic should not need to know what the appropriate instantiations are; rather, we want these choices filled with placeholders. We hope that, when we apply the specialized hypothesis later, syntactic unification will determine concrete values.
755 755
756 Before we are ready to write a tactic, we can try out its ingredients one at a time. *) 756 Before we are ready to write a tactic, we can try out its ingredients one at a time. *)
757 757
758 Theorem t5 : (forall x : nat, S x > x) -> 2 > 1. 758 Theorem t5 : (forall x : nat, S x > x) -> 2 > 1.
759 intros. 759 intros.