Mercurial > cpdt > repo

comparison src/Tactics.v @ 200:df289eb8ef76

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Small fixes while reading student solutions
author Adam Chlipala <adamc@hcoop.net>
date Fri, 02 Jan 2009 08:57:25 -0500
parents 699fd70c04a7
children cbf2f74a5130
comparison
equal deleted inserted replaced
199:cadeb49dc1ef 200:df289eb8ef76
135 repeat (simplHyp invOne; intuition)); un_done 135 repeat (simplHyp invOne; intuition)); un_done
136 end; sintuition; rewriter; sintuition; try omega; try (elimtype False; omega)). 136 end; sintuition; rewriter; sintuition; try omega; try (elimtype False; omega)).
137 137
138 Ltac crush := crush' false fail. 138 Ltac crush := crush' false fail.
139 139
140 Theorem dep_destruct : forall (T : Type) (T' : T -> Type) x (v : T' x) (P : T' x -> Prop), 140 Theorem dep_destruct : forall (T : Type) (T' : T -> Type) x (v : T' x) (P : T' x -> Type),
141 (forall x' (v' : T' x') (Heq : x' = x), P (match Heq in (_ = x) return (T' x) with 141 (forall x' (v' : T' x') (Heq : x' = x), P (match Heq in (_ = x) return (T' x) with
142 | refl_equal => v' 142 | refl_equal => v'
143 end)) 143 end))
144 -> P v. 144 -> P v.
145 intros. 145 intros.
146 generalize (H _ v (refl_equal _)); trivial. 146 generalize (X _ v (refl_equal _)); trivial.
147 Qed. 147 Qed.
148 148
149 Ltac dep_destruct E := 149 Ltac dep_destruct E :=
150 let doit A := 150 let doit A :=
151 let T := type of A in 151 let T := type of A in