coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adamc AT cs.berkeley.edu>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club]Automatic derivation of dependent inversion principle?
- Date: Thu, 06 Jul 2006 11:43:11 -0700
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Is there any way that I can get Coq to derive automatically the dependent inversion principle 'tm_invert_true' below?
Inductive tm : bool -> Set :=
| t : tm true
| f : tm false.
Lemma tm_invert_true' : forall (P : tm true -> Prop),
P t
-> forall t e,
(match t return (tm t -> Prop) with
| true => P
| _ => fun _ => True
end) e.
destruct e; trivial.
Qed.
Lemma tm_invert_true : forall (P : tm true -> Prop),
P t
-> forall e, P e.
intros.
generalize (tm_invert_true' P); intuition.
generalize (H1 true); trivial.
Qed.
Goal (forall (e1 e2 : tm true),
match e1 with
| t => e2
| _ => t
end = e2).
inversion e1 using tm_invert_true; trivial.
- [Coq-Club]Automatic derivation of dependent inversion principle?, Adam Chlipala
Archive powered by MhonArc 2.6.16.