6
\$\begingroup\$

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.
\$\endgroup\$
6
\$\begingroup\$

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.
\$\endgroup\$
  • 1
    \$\begingroup\$ Since the proof can be finished with several rewrites, it's usually a sign that we can do it using the congruence tactic: ... unfold compose; congruence. \$\endgroup\$ – Anton Trunov Sep 5 '17 at 13:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.