Coq proof that type isomorphism relationship is transitive

Question

The following code is in Coq, a proof assistant by INRIA implemented in OCaml.

I'm defining two types as being isomorphic when there exists two functions f : s -> t and g : t -> s such that, for all x, f (g x) = x. The function compose is just a helper function to make it easier to write terms in my typeclass.

I'm trying to prove that the isomorphism relation that I'm defining is transitive.

My proof is kind of ugly, I'm using inversion twice to get a whole bunch of terms "in scope".

Here's all the stuff that I introduce:

1 subgoal
A : Type
B : Type
C : Type
X : Isomorphism A B
X' : Isomorphism B C
from0 : A -> B
to0 : B -> A
from_to0 : forall x : B, from0 (to0 x) = x
to_from0 : forall x : A, to0 (from0 x) = x
from1 : B -> C
to1 : C -> B
from_to1 : forall x : C, from1 (to1 x) = x
to_from1 : forall x : B, to1 (from1 x) = x
______________________________________(1/1)
Isomorphism A C

Then I'm using refine with two holes _ in order to introduce two further goals:

refine({|
  from := compose from1 from0;
  to := compose to0 to1;
  from_to := _;
  to_from := _
|}).

I'm constructing from and to explicitly, and allowing from_to and to_from to become goals, like this:

______________________________________(1/2)
forall x : C, compose from1 from0 (compose to0 to1 x) = x
______________________________________(2/2)
forall x : A, compose to0 to1 (compose from1 from0 x) = x

And then for each of those cases I unfold to get rid of compose, and then get rid of adjacent froms and tos by rewriting.

This whole thing seems more complicated than it needs to be. Is there a more direct way to show that Isomorphism A B -> Isomorphism B C -> Isomorphism A C is inhabited?

Here is the complete source code for reference:

Class Isomorphism A B :=
  {
    from: A -> B;
    to: B -> A;
    from_to x: from (to x) = x;
    to_from x: to (from x) = x
  }.


Definition compose {T T' T''} (f : T' -> T'') (g : T -> T') (x : T) : T'' :=
  f (g x).


Definition trans { A B C }: Isomorphism A B -> Isomorphism B C -> Isomorphism A C.
intros X X'.
inversion X.
inversion X'.
refine({|
  from := compose from1 from0;
  to := compose to0 to1;
  from_to := _;
  to_from := _
|}).
{
  intros.
  unfold compose.
  rewrite -> from_to0.
  rewrite -> from_to1.
  reflexivity.
}
{
  intros.
  unfold compose.
  rewrite -> to_from1.
  rewrite -> to_from0.
  reflexivity.
}
Qed.

Answer 1

You can make the proof a lot shorter by giving a constructor for the class Isomorphism and by destructing your arguments instead of inverting them:

Class Isomorphism A B :=
  MkIsomorphism {
    from: A -> B;
    to: B -> A;
    from_to x: from (to x) = x;
    to_from x: to (from x) = x
  }.


Definition compose {A B C} (f : B -> C) (g : A -> B) (x : A) : C
  := f (g x).

Definition trans {A B C} :
  Isomorphism A B -> Isomorphism B C -> Isomorphism A C.
Proof.
intros [AtoB BtoA AtoBtoA BtoAtoB] [BtoC CtoB BtoCtoB CtoBtoC].
apply MkIsomorphism
  with (from := compose BtoC AtoB)
       (to   := compose BtoA CtoB);
intro x; unfold compose.
 - rewrite AtoBtoA, BtoCtoB; reflexivity.
 - rewrite CtoBtoC, BtoAtoB; reflexivity.
Defined.