coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club] Strengthening the definitional equality on types?, Benjamin Pierce
- Re: [Coq-Club] Strengthening the definitional equality on types?, Adam Chlipala
- Re: [Coq-Club] Strengthening the definitional equality on types?, Arnaud Spiwack
- Re: [Coq-Club] Strengthening the definitional equality on types?, Arnaud Spiwack
- Re: [Coq-Club] Strengthening the definitional equality on types?, AUGER Cedric
- Re: [Coq-Club] Strengthening the definitional equality on types?, Stefan Monnier
- Re: [Coq-Club] Strengthening the definitional equality on types?, Conor McBride
- Re: [Coq-Club] Strengthening the definitional equality on types?, Hugo Herbelin
Archive powered by MhonArc 2.6.16.