(** 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.