类型同构关系是传递的协q证明

Question

下面的代码是Coq中的，它是INRIA在OCaml中实现的一个验证助手。

当存在两个函数f : s -> t和g : t -> s时，我将两种类型定义为同构，对于所有的x，f (g x) = x。函数compose只是一个帮助函数，可以使在我的类型库中编写术语变得更容易。

我试图证明我定义的同构关系是可传递的。

我的证明有点丑陋，我用了两次反演来得到一整串“范围内”的术语。

以下是我介绍的所有内容：

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

然后，我使用带有两个孔的细化_来介绍两个进一步的目标：

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

我正在显式地构造from和to，并允许from_to和to_from成为目标，如下所示：

______________________________________(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

然后，对每一个案例，我展开，以摆脱写作，然后摆脱相邻的froms和tos重写。

整件事看起来比需要的复杂多了。有没有更直接的方式来显示Isomorphism A B -> Isomorphism B C -> Isomorphism A C有人居住呢？

以下是供参考的完整源代码：

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

您可以通过为类Isomorphism提供一个构造函数，并通过销毁您的参数，而不是将它们反转，从而使证明变得更短：

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.