Mercurial > cpdt > repo

comparison src/Tactics.v @ 86:fd505bcb5632

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of certified regexp matcher
author Adam Chlipala <adamc@hcoop.net>
date Mon, 06 Oct 2008 14:33:11 -0400
parents 3746a2ded8da
children cde1351d18bb
comparison
equal deleted inserted replaced
85:3746a2ded8da 86:fd505bcb5632
109 Ltac un_done := 109 Ltac un_done :=
110 repeat match goal with 110 repeat match goal with
111 | [ H : done _ |- _ ] => clear H 111 | [ H : done _ |- _ ] => clear H
112 end. 112 end.
113 113
114 Ltac crush' lemmas invOne := 114 Ltac crush'' tryLemmas lemmas invOne :=
115 let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence 115 let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence
116 in (sintuition; rewriter; 116 in (sintuition; rewriter;
117 repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L)); 117 match tryLemmas with
118 repeat (simplHyp invOne; intuition)); 118 | true => repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));
119 un_done; sintuition; try omega; try (elimtype False; omega)). 119 repeat (simplHyp invOne; intuition)); un_done
120 | _ => idtac
121 end; sintuition; try omega; try (elimtype False; omega)).
120 122
121 Ltac crush := crush' tt fail. 123 Ltac crush := crush'' false tt fail.
124 Ltac crush' := crush'' true.
122 125
123 Theorem dep_destruct : forall (T : Type) (T' : T -> Type) x (v : T' x) (P : T' x -> Prop), 126 Theorem dep_destruct : forall (T : Type) (T' : T -> Type) x (v : T' x) (P : T' x -> Prop),
124 (forall x' (v' : T' x') (Heq : x' = x), P (match Heq in (_ = x) return (T' x) with 127 (forall x' (v' : T' x') (Heq : x' = x), P (match Heq in (_ = x) return (T' x) with
125 | refl_equal => v' 128 | refl_equal => v'
126 end)) 129 end))