Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] how to make Coq to recognize that two inductive definitions are equal.

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.



Archive powered by MhonArc 2.6.16.

Top of Page