The Coq mailing list

[AUGER Cedric <sedrikov AT gmail.com>]

What about the following code?
+ it type checks
+ it is semantically exactly what you wanted
+ it has same signature for parameters
- it is awful when unfolding/defining
- it implies destruction on d to get the equality (even if it is more 
convenient to type:
  destruct d; apply isoAx
    than
  destruct d; [apply isoAxL | apply isoAxR]
   , it is less convenient than typing
  apply isoAxL)

 Module Type Iso.
   Parameter S : Dir -> Set.
   Parameter f : forall d, S d -> S (swap d).
   Axiom isoAx : forall d x, match d as d0 return S (swap (swap d0)) -> 
S d0 -> Prop with
    | R => fun x y => x = y
    | L => fun x y => x = y
    end (f (swap d) (f d x)) x.
 End Iso.

or this code:
+ it type checks
+ it is semantically exactly what you wanted
+ it has same signature for parameters
- it is awful to cast whenever required

 Module Type Iso.
   Parameter S : Dir -> Set.
   Parameter f : forall d, S d -> S (swap d).
   Definition cast : forall d, S (swap (swap d)) -> S d :=
      fun d => match d as d0 returns S (swap (swap d0)) -> S d0 with
        | L => fun x => x
        | R => fun x => x
      end.(* identity type-casted *)
   Axiom isoAx : forall d x, cast _ (f (swap d) (f d x)) = x.
 End Iso.


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.
>
> What to do?  We've seen the discussion of John Major equality in 
> CoqArt... is this our only hope, or is there a lighter way?
>
> Thanks!
>
>     - Benjamin Pierce and Martin Hofmann
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club