Mercurial > cpdt > repo

comparison src/Match.v @ 302:7b38729be069

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tweak mark-up to support coqdoc 8.3
author Adam Chlipala <adam@chlipala.net>
date Mon, 17 Jan 2011 15:12:30 -0500
parents f4768d5a75eb
children d5787b70cf48
comparison
equal deleted inserted replaced
301:f4768d5a75eb 302:7b38729be069
127 Lemma f_f_f' : forall x, f (f (f x)) = f x. 127 Lemma f_f_f' : forall x, f (f (f x)) = f x.
128 intros; autorewrite with my_db. 128 intros; autorewrite with my_db.
129 (** [[ 129 (** [[
130 ============================ 130 ============================
131 g (g (g x)) = g x 131 g (g (g x)) = g x
132 ]] *) 132 ]]
133 *)
133 134
134 Abort. 135 Abort.
135 136
136 (** Our new hint was used to rewrite the goal into a form where the old hint could no longer be applied. This %``%#"#non-monotonicity#"#%''% of rewrite hints contrasts with the situation for [auto], where new hints may slow down proof search but can never %``%#"#break#"#%''% old proofs. The key difference is that [auto] either solves a goal or makes no changes to it, while [autorewrite] may change goals without solving them. The situation for [eauto] is slightly more complicated, as changes to hint databases may change the proof found for a particular goal, and that proof may influence the settings of unification variables that appear elsewhere in the proof state. *) 137 (** Our new hint was used to rewrite the goal into a form where the old hint could no longer be applied. This %``%#"#non-monotonicity#"#%''% of rewrite hints contrasts with the situation for [auto], where new hints may slow down proof search but can never %``%#"#break#"#%''% old proofs. The key difference is that [auto] either solves a goal or makes no changes to it, while [autorewrite] may change goals without solving them. The situation for [eauto] is slightly more complicated, as changes to hint databases may change the proof found for a particular goal, and that proof may influence the settings of unification variables that appear elsewhere in the proof state. *)
137 138
156 P x 157 P x
157 subgoal 3 is: 158 subgoal 3 is:
158 P (f x) 159 P (f x)
159 subgoal 4 is: 160 subgoal 4 is:
160 P (f x) 161 P (f x)
161 ]] *) 162 ]]
163 *)
162 164
163 Abort. 165 Abort.
164 166
165 (** The inappropriate rule fired the same three times as before, even though we know we will not be able to prove the premises. *) 167 (** The inappropriate rule fired the same three times as before, even though we know we will not be able to prove the premises. *)
166 168
412 H0 : Q x 414 H0 : Q x
413 H3 : R x 415 H3 : R x
414 H4 : S x 416 H4 : S x
415 ============================ 417 ============================
416 S x 418 S x
417 ]] *) 419 ]]
420 *)
418 421
419 assumption. 422 assumption.
420 Qed. 423 Qed.
421 (* end thide *) 424 (* end thide *)
422 End firstorder. 425 End firstorder.
477 match goal with 480 match goal with
478 | [ |- forall x, ?P ] => trivial 481 | [ |- forall x, ?P ] => trivial
479 end. 482 end.
480 483
481 User error: No matching clauses for match goal 484 User error: No matching clauses for match goal
482 ]] *) 485 ]]
486 *)
483 487
484 Abort. 488 Abort.
485 (* end thide *) 489 (* end thide *)
486 490
487 (** The problem is that unification variables may not contain locally-bound variables. In this case, [?P] would need to be bound to [x = x], which contains the local quantified variable [x]. By using a wildcard in the earlier version, we avoided this restriction. To understand why this applies to the [completer] tactics, recall that, in Coq, implication is shorthand for degenerate universal quantification where the quantified variable is not used. Nonetheless, in an Ltac pattern, Coq is happy to match a wildcard implication against a universal quantification. 491 (** The problem is that unification variables may not contain locally-bound variables. In this case, [?P] would need to be bound to [x = x], which contains the local quantified variable [x]. By using a wildcard in the earlier version, we avoided this restriction. To understand why this applies to the [completer] tactics, recall that, in Coq, implication is shorthand for degenerate universal quantification where the quantified variable is not used. Nonetheless, in an Ltac pattern, Coq is happy to match a wildcard implication against a universal quantification.
567 pose n. 571 pose n.
568 (** [[ 572 (** [[
569 n := 3 : nat 573 n := 3 : nat
570 ============================ 574 ============================
571 False 575 False
572 ]] *) 576 ]]
577 *)
573 578
574 Abort. 579 Abort.
575 (* end thide *) 580 (* end thide *)
576 581
577 (* EX: Write a list map function in Ltac. *) 582 (* EX: Write a list map function in Ltac. *)
599 pose ls. 604 pose ls.
600 (** [[ 605 (** [[
601 l := (1, 1) :: (2, 2) :: (3, 3) :: nil : list (nat * nat) 606 l := (1, 1) :: (2, 2) :: (3, 3) :: nil : list (nat * nat)
602 ============================ 607 ============================
603 False 608 False
604 ]] *) 609 ]]
610 *)
605 611
606 Abort. 612 Abort.
607 (* end thide *) 613 (* end thide *)
608 614
609 615
848 (and_True_conc 854 (and_True_conc
849 (ex_conc (fun x0 : nat => P x0) x 855 (ex_conc (fun x0 : nat => P x0) x
850 (Match (P:=P x) (imp_True (P:=True)))))))) 856 (Match (P:=P x) (imp_True (P:=True))))))))
851 : forall (P : nat -> Prop) (Q : Prop), 857 : forall (P : nat -> Prop) (Q : Prop),
852 (exists x : nat, P x /\ Q) --> Q /\ (exists x : nat, P x) 858 (exists x : nat, P x /\ Q) --> Q /\ (exists x : nat, P x)
853 ]] *) 859 ]]
860 *)
854 861
855 862
856 (** * Creating Unification Variables *) 863 (** * Creating Unification Variables *)
857 864
858 (** A final useful ingredient in tactic crafting is the ability to allocate new unification variables explicitly. Tactics like [eauto] introduce unification variable internally to support flexible proof search. While [eauto] and its relatives do %\textit{%#<i>#backward#</i>#%}% reasoning, we often want to do similar %\textit{%#<i>#forward#</i>#%}% reasoning, where unification variables can be useful for similar reasons. 865 (** A final useful ingredient in tactic crafting is the ability to allocate new unification variables explicitly. Tactics like [eauto] introduce unification variable internally to support flexible proof search. While [eauto] and its relatives do %\textit{%#<i>#backward#</i>#%}% reasoning, we often want to do similar %\textit{%#<i>#forward#</i>#%}% reasoning, where unification variables can be useful for similar reasons.