coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] how to make Coq to recognize that two inductive definitions are equal.
chronological Thread
- From: Adam Chlipala <adam AT chlipala.net>
- To: Vladimir Voevodsky <vladimir AT ias.edu>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] how to make Coq to recognize that two inductive definitions are equal.
- Date: Wed, 17 Feb 2010 12:08:03 -0500
Vladimir Voevodsky wrote:
Inductive total2 (T:Type) (P:T -> Type) := tpair: forall t:T, forall x: P t,
total2 T P.
Inductive total2' (T:Type) (P:T -> Type) := tpair': forall t:T, forall x: P
t, total2' T P.
Definition pr21 (T:Type) (P:T -> Type) (z: total2 T P) : T :=
match z with
tpair t x => t
end.
Lemma a (T:Type)(P:T->Type)(z: total2' T P) : pr21 T P z.
Coq does not understand the lemma saying that z has to be of type total2 T P.
However, total2 T P and total2' T P are equal (up to alpha equivalence) as
the terms of the calculus of construction and the membership in one is the
same as in another. How can I point it out to Coq?
You can write conversion functions between them, and you can even get these functions applied automatically as coercions. I don't think there's any way to prove that these types are equal in the sense of [=], though. The standard model shows that it would be OK to add that as an axiom, as long as you don't have some other especially exotic (and contradictory) axiom around.
- [Coq-Club] hint database pollution, Damien Pous
- Re: [Coq-Club] hint database pollution,
Pierre Letouzey
- Re: [Coq-Club] hint database pollution, Damien Pous
- [Coq-Club] how to make Coq to recognize that two inductive definitions are equal.,
Vladimir Voevodsky
- Re: [Coq-Club] how to make Coq to recognize that two inductive definitions are equal., Adam Chlipala
- Re: [Coq-Club] hint database pollution,
Pierre Letouzey
Archive powered by MhonArc 2.6.16.