Mercurial > cpdt > repo

comparison src/Tactics.v @ 88:cde1351d18bb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Get Coinductive compiling again
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Oct 2008 10:43:54 -0400
parents fd505bcb5632
children 8c7d9b82a4a4
comparison
equal deleted inserted replaced
87:a0b8b550e265 88:cde1351d18bb
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'' tryLemmas lemmas invOne := 114 Ltac crush' 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 match tryLemmas with 117 match lemmas with
118 | true => repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L)); 118 | false => idtac
119 | _ => repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));
119 repeat (simplHyp invOne; intuition)); un_done 120 repeat (simplHyp invOne; intuition)); un_done
120 | _ => idtac
121 end; sintuition; try omega; try (elimtype False; omega)). 121 end; sintuition; try omega; try (elimtype False; omega)).
122 122
123 Ltac crush := crush'' false tt fail. 123 Ltac crush := crush' false fail.
124 Ltac crush' := crush'' true.
125 124
126 Theorem dep_destruct : forall (T : Type) (T' : T -> Type) x (v : T' x) (P : T' x -> Prop), 125 Theorem dep_destruct : forall (T : Type) (T' : T -> Type) x (v : T' x) (P : T' x -> Prop),
127 (forall x' (v' : T' x') (Heq : x' = x), P (match Heq in (_ = x) return (T' x) with 126 (forall x' (v' : T' x') (Heq : x' = x), P (match Heq in (_ = x) return (T' x) with
128 | refl_equal => v' 127 | refl_equal => v'
129 end)) 128 end))