Mercurial > cpdt > repo

comparison src/Tactics.v @ 297:b441010125d4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Everything compiles in Coq 8.3pl1
author Adam Chlipala <adam@chlipala.net>
date Fri, 14 Jan 2011 14:39:12 -0500
parents de53c8bcfa8d
children
comparison
equal deleted inserted replaced
296:559ec7328410 297:b441010125d4
1 (* Copyright (c) 2008, Adam Chlipala 1 (* Copyright (c) 2008-2011, Adam Chlipala
2 * 2 *
3 * This work is licensed under a 3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
124 Ltac un_done := 124 Ltac un_done :=
125 repeat match goal with 125 repeat match goal with
126 | [ H : done _ |- _ ] => clear H 126 | [ H : done _ |- _ ] => clear H
127 end. 127 end.
128 128
129 Require Import JMeq.
130
129 Ltac crush' lemmas invOne := 131 Ltac crush' lemmas invOne :=
130 let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence in 132 let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence in
131 let rewriter := autorewrite with cpdt in *; 133 let rewriter := autorewrite with cpdt in *;
132 repeat (match goal with 134 repeat (match goal with
133 | [ H : _ |- _ ] => (rewrite H; []) 135 | [ H : ?P |- _ ] =>
134 || (rewrite H; [ | solve [ crush' lemmas invOne ] ]) 136 match P with
135 || (rewrite H; [ | solve [ crush' lemmas invOne ] | solve [ crush' lemmas invOne ] ]) 137 | context[JMeq] => fail 1
138 | _ => (rewrite H; [])
139 || (rewrite H; [ | solve [ crush' lemmas invOne ] ])
140 || (rewrite H; [ | solve [ crush' lemmas invOne ] | solve [ crush' lemmas invOne ] ])
141 end
136 end; autorewrite with cpdt in *) 142 end; autorewrite with cpdt in *)
137 in (sintuition; rewriter; 143 in (sintuition; rewriter;
138 match lemmas with 144 match lemmas with
139 | false => idtac 145 | false => idtac
140 | _ => repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L)); 146 | _ => repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));