## Mercurial > cpdt > repo

### diff src/Match.v @ 488:31258618ef73

Find changesets by keywords (author, files, the commit message), revision
number or hash, or revset expression.

Incorporate feedback from Nathan Collins

author | Adam Chlipala <adam@chlipala.net> |
---|---|

date | Tue, 08 Jan 2013 14:38:56 -0500 |

parents | 5025a401ad9e |

children | 49f3b2d70302 |

line wrap: on

line diff

--- a/src/Match.v Mon Jan 07 15:23:16 2013 -0500 +++ b/src/Match.v Tue Jan 08 14:38:56 2013 -0500 @@ -582,13 +582,13 @@ imp. Qed. -Theorem assoc_prem1 : forall P Q R S, +Theorem pick_prem1 : forall P Q R S, (P /\ (Q /\ R) --> S) -> ((P /\ Q) /\ R --> S). imp. Qed. -Theorem assoc_prem2 : forall P Q R S, +Theorem pick_prem2 : forall P Q R S, (Q /\ (P /\ R) --> S) -> ((P /\ Q) /\ R --> S). imp. @@ -600,13 +600,13 @@ imp. Qed. -Theorem assoc_conc1 : forall P Q R S, +Theorem pick_conc1 : forall P Q R S, (S --> P /\ (Q /\ R)) -> (S --> (P /\ Q) /\ R). imp. Qed. -Theorem assoc_conc2 : forall P Q R S, +Theorem pick_conc2 : forall P Q R S, (S --> Q /\ (P /\ R)) -> (S --> (P /\ Q) /\ R). imp. @@ -626,8 +626,8 @@ || (apply and_True_prem; tac) || match P with | ?P1 /\ ?P2 => - (apply assoc_prem1; search P1) - || (apply assoc_prem2; search P2) + (apply pick_prem1; search P1) + || (apply pick_prem2; search P2) end in match goal with | [ |- ?P /\ _ --> _ ] => search P @@ -637,7 +637,7 @@ (** To understand how [search_prem] works, we turn first to the final [match]. If the premise begins with a conjunction, we call the [search] procedure on each of the conjuncts, or only the first conjunct, if that already yields a case where [tac] does not fail. The call [search P] expects and maintains the invariant that the premise is of the form [P /\ Q] for some [Q]. We pass [P] explicitly as a kind of decreasing induction measure, to avoid looping forever when [tac] always fails. The second [match] case calls a commutativity lemma to realize this invariant, before passing control to [search]. The final [match] case tries applying [tac] directly and then, if that fails, changes the form of the goal by adding an extraneous [True] conjunct and calls [tac] again. The %\index{tactics!progress}%[progress] tactical fails when its argument tactic succeeds without changing the current subgoal. - The [search] function itself tries the same tricks as in the last case of the final [match]. Additionally, if neither works, it checks if [P] is a conjunction. If so, it calls itself recursively on each conjunct, first applying associativity lemmas to maintain the goal-form invariant. + The [search] function itself tries the same tricks as in the last case of the final [match], using the [||] operator as a shorthand for trying one tactic and then, if the first fails, trying another. Additionally, if neither works, it checks if [P] is a conjunction. If so, it calls itself recursively on each conjunct, first applying associativity lemmas to maintain the goal-form invariant. We will also want a dual function [search_conc], which does tree search through an [imp] conclusion. *) @@ -647,8 +647,8 @@ || (apply and_True_conc; tac) || match P with | ?P1 /\ ?P2 => - (apply assoc_conc1; search P1) - || (apply assoc_conc2; search P2) + (apply pick_conc1; search P1) + || (apply pick_conc2; search P2) end in match goal with | [ |- _ --> ?P /\ _ ] => search P @@ -718,7 +718,7 @@ (** %\vspace{-.15in}% [[ t2 = fun P Q : Prop => -comm_prem (assoc_prem1 (assoc_prem2 (False_prem (P:=P /\ P /\ Q) (P /\ Q)))) +comm_prem (pick_prem1 (pick_prem2 (False_prem (P:=P /\ P /\ Q) (P /\ Q)))) : forall P Q : Prop, Q /\ (P /\ False) /\ P --> P /\ Q ]] @@ -750,7 +750,7 @@ and_True_prem (ex_prem (P:=fun x : nat => P x /\ Q) (fun x : nat => - assoc_prem2 + pick_prem2 (Match (P:=Q) (and_True_conc (ex_conc (fun x0 : nat => P x0) x