The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Here is a rather elegant solution suggested to me by Benjamin Werner (it seems to go down to George Gonthier, he will correct me if I'm wrong).

The essence of the idea is to add a pinch of dynamic typechecking which we then prove cannot fail. It is a bit disapointing in that we statically check a dynamic check that will have to be performed. But this seems rather minimalistic. Here is your piece of file transformed this way (with a few not-so-helpful comments) :

Require Import Program.

(* We shall proceed to equalise more type through *dynamic* type conversion
    which will always reduce to the identity. *)

(* Type of coercions, "IsntEq" means that coercion failed, 
    "IsEq c" is a successful condition. We will see to prevent "IsntEq" to bother us"*)
Inductive eqopt {A:Type} (F:A->Type) (i j:A) :=
  | IsntEq
  | IsEq (c:F i -> F j) 
.
Implicit Arguments IsntEq [ [A] [F] [i] [j] ].
Implicit Arguments IsEq [ [A] [F] [i] [j] ].
Definition id {A} (x:A) := x.

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

(* This defines a coercion at type [Dir], in fact any type with decidable equality
    can be given such a coercion. *)
Definition equalise_dir (F:Dir -> Type) (d1 d2:Dir) : eqopt F d1 d2 :=
  match d1 , d2 with
  | R , R => IsEq id
  | L , L => IsEq id
  | _ , _ => IsntEq
  end.

(* The fundamental lemma meaning that the coercion is always the identity *)
Lemma equalise_dir_same : forall F d, equalise_dir F d d = IsEq id.
  intros F []; easy.
Qed.

(* The magic function encapsulating the dynamic type cast. We provide
    a proof that it cannot fail. *)
Program Definition swapf {S : Dir -> Type} (f:forall d, S d -> S (swap d)) : forall d, S (swap d) -> S d :=
  fun d x => match equalise_dir S (swap (swap d)) d with
  | IsntEq => !
  | IsEq c => c (f (swap d) x)
  end.
Next Obligation.
  destruct d; easy.
Qed.

Module Type Iso.
  Parameter S : Dir -> Type.
  Parameter f : forall d, S d -> S (swap d).

  Axiom isoAx : forall d x, swapf f d (f d x) = x.
End Iso.

2009/8/4 Benjamin Pierce <bcpierce AT cis.upenn.edu>

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