(** EqImplIso.v Version 1.1 February 2011 *)
(** runs under V8.3, tested with 8.3pl2 *)
(** Celia Picard with contributions by Ralph Matthes,
I.R.I.T., University of Toulouse and CNRS*)
(** provides a proof that the compositions of two symmetric retypings
are extensionally equal to the identity *)
(** this is code that conforms to the description in the article
"Permutations in Coinductive Graph Representation"
by the authors *)
Section EqImplIso.
Variables A B: Set.
Hypothesis Hyp: A = B.
(* Definition of a function that "retypes" f to type B *)
Definition ii (f:A): B :=
match Hyp in (_= n) return n with refl_equal => f end.
(* Definition of a function that "retypes" g to type A *)
Definition jj (g:B): A :=
match (sym_eq Hyp) in (_= n) return n with refl_equal => g end.
(* Proofs that the two functions defined above are effectively
inverse to each other *)
Lemma iijj (g:B): ii(jj g) = g.
Proof.
unfold ii, jj.
revert g.
rewrite <- Hyp.
reflexivity.
Qed.
Lemma jjii (f:A): jj(ii f) = f.
Proof.
unfold ii, jj.
refine (match Hyp return _ with refl_equal => _ end).
reflexivity.
Qed.
End EqImplIso.