Mercurial > cpdt > repo

comparison src/Tactics.v @ 183:02569049397b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Closure conversion defined
author Adam Chlipala <adamc@hcoop.net>
date Sun, 16 Nov 2008 14:01:33 -0500
parents 8f3fc56b90d4
children 699fd70c04a7
comparison
equal deleted inserted replaced
182:24b99e025fe8 183:02569049397b
70 | [ H : Some _ = Some _ |- _ ] => injection H; clear H 70 | [ H : Some _ = Some _ |- _ ] => injection H; clear H
71 end. 71 end.
72 72
73 Ltac rewriteHyp := 73 Ltac rewriteHyp :=
74 match goal with 74 match goal with
75 | [ H : _ |- _ ] => rewrite H 75 | [ H : _ |- _ ] => rewrite H; auto; [idtac]
76 end. 76 end.
77 77
78 Ltac rewriterP := repeat (rewriteHyp; autorewrite with cpdt in *). 78 Ltac rewriterP := repeat (rewriteHyp; autorewrite with cpdt in *).
79 79
80 Ltac rewriter := autorewrite with cpdt in *; rewriterP. 80 Ltac rewriter := autorewrite with cpdt in *; rewriterP.
120 | [ H : done _ |- _ ] => clear H 120 | [ H : done _ |- _ ] => clear H
121 end. 121 end.
122 122
123 Ltac crush' lemmas invOne := 123 Ltac crush' lemmas invOne :=
124 let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence 124 let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence
125 in (sintuition; rewriter; 125 in (sintuition;
126 match lemmas with 126 autorewrite with cpdt in *;
127 | false => idtac 127 repeat (match goal with
128 | _ => repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L)); 128 | [ H : _ |- _ ] => (rewrite H; [])
129 repeat (simplHyp invOne; intuition)); un_done 129 || (rewrite H; [ | solve [ crush' lemmas invOne ] ])
130 end; sintuition; try omega; try (elimtype False; omega)). 130 end; autorewrite with cpdt in *);
131 match lemmas with
132 | false => idtac
133 | _ => repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));
134 repeat (simplHyp invOne; intuition)); un_done
135 end; sintuition; try omega; try (elimtype False; omega)).
131 136
132 Ltac crush := crush' false fail. 137 Ltac crush := crush' false fail.
133 138
134 Theorem dep_destruct : forall (T : Type) (T' : T -> Type) x (v : T' x) (P : T' x -> Prop), 139 Theorem dep_destruct : forall (T : Type) (T' : T -> Type) x (v : T' x) (P : T' x -> Prop),
135 (forall x' (v' : T' x') (Heq : x' = x), P (match Heq in (_ = x) return (T' x) with 140 (forall x' (v' : T' x') (Heq : x' = x), P (match Heq in (_ = x) return (T' x) with