Mercurial > cpdt > repo
comparison src/Tactics.v @ 80:506a06118014
Try arithmetic contradiction
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 04 Oct 2008 14:58:00 -0400 |
parents | b52204928c7d |
children | 522436ed6688 |
comparison
equal
deleted
inserted
replaced
79:6c2607211cee | 80:506a06118014 |
---|---|
110 Ltac crush' lemmas invOne := | 110 Ltac crush' lemmas invOne := |
111 let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence | 111 let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence |
112 in (sintuition; rewriter; | 112 in (sintuition; rewriter; |
113 repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L)); | 113 repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L)); |
114 repeat (simplHyp invOne; intuition)); | 114 repeat (simplHyp invOne; intuition)); |
115 un_done; sintuition; try omega). | 115 un_done; sintuition; try omega; try (elimtype False; omega)). |
116 | 116 |
117 Ltac crush := crush' tt fail. | 117 Ltac crush := crush' tt fail. |