Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Strengthening the definitional equality on types?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Strengthening the definitional equality on types?


chronological Thread 
  • From: Adam Chlipala <adamc AT hcoop.net>
  • To: Benjamin Pierce <bcpierce AT cis.upenn.edu>
  • Cc: coq-club AT pauillac.inria.fr, Martin Hofmann <mhofmann AT TCS.IFI.LMU.DE>
  • Subject: Re: [Coq-Club] Strengthening the definitional equality on types?
  • Date: Tue, 04 Aug 2009 17:34:39 -0400
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Benjamin Pierce wrote:
Suppose one wanted to define isomorphisms in the following slightly unusual fashion:

Inductive Dir : Set := R | L.
Definition swap (d:Dir) := match d with R => L | L => R end.

Module Type Iso.
Parameter S : Dir -> Set.
Parameter f : forall d, S d -> S (swap d).
Axiom isoAx : forall d x, f (swap d) (f d x) = x.
End Iso.

Instead of two separate functions, two axioms, and two sets, we index everything by a direction. This means we can write definitions of composition of isomorphisms, juxtaposition, etc. and prove their properties very compactly (saving 50% of the typing each time).

Unfortunately, this definition doesn't typecheck: the term

f (swap d) (f d x)

has type S (swap (swap d)), not S d, which is the type of x. Of course, swap (swap d) is provably equal to d for every d, but not convertible.

You can restate the type of [isoAx] like this:

Axiom isoAx : forall d x, f (swap d) (f d x)
= match d return S d -> S (swap (swap d)) with
| R => fun x => x
| L => fun x => x
end x.

It's hard to say whether the details of your development will go more smoothly with this, with [JMeq], or with something else.





Archive powered by MhonArc 2.6.16.

Top of Page