在 prod 的 sigma 和不相交的 sum 之间建立同构

Question

我根据不相交和的定义定义了一个布尔归纳类型：

Inductive Boole :=
  | inlb (a: unit)
  | inrb (b: unit).

给定两种类型 A 和 B 我试图证明它们之间的同构

sigT (fun x: Boole => prod ((eq x (inrb tt)) -> A) (eq x (inlb tt) -> B))

和

A + B

我设法证明了同构的一方面

Definition sum_to_sigT {A} {B} (z: A + B) :
  sigT (fun x: Boole => prod ((eq x (inrb tt)) -> A) (eq x (inlb tt) -> B)).
Proof.
case z.
  move=> a.
  exists (inrb tt).
  rewrite //=.
move=> b.
  exists (inlb tt).
  rewrite //=.
Defined.

Lemma eq_inla_inltt (a: unit) : eq (inlb a) (inlb tt).
Proof.
by case a.
Qed.

Lemma eq_inra_inrtt (a: unit) : eq (inrb a) (inrb tt).
Proof.
by case a.
Qed.

Definition sigT_to_sum {A} {B} 
  (w: sigT (fun x: Boole => prod ((eq x (inrb tt)) -> A) (eq x (inlb tt) -> B))) :
  A + B.
Proof.
destruct w.
destruct p.
destruct x.
apply (inr (b (eq_inla_inltt a0))).
apply (inl (a (eq_inra_inrtt b0))).
Defined.

Definition eq_sum_sigT {A} {B} (x: A + B): 
  eq x (sigT_to_sum (sum_to_sigT x)).
Proof.
by case x.
Defined.

但我在证明另一方时遇到了麻烦，主要是因为我无法在以下证明中涉及的不同 x 和 p 之间建立相等性：

Definition eq_sigT_sum {A} {B} 
  (y: sigT (fun x: Boole => prod ((eq x (inrb tt)) -> A) (eq x (inlb tt) -> B))) : eq y (sum_to_sigT (sigT_to_sum y)).
Proof.
case: (sum_to_sigT (sigT_to_sum y)).
  move=> x p.
  destruct y.
  destruct x.
  destruct p.
Defined.

有人知道我如何证明后一个引理吗？

感谢您的帮助。

Answer 1

这听起来很奇怪，但你无法在 Coq 的理论中证明这个结果。

让我们将类型称为sigT (fun x => prod (eq x (inrb tt) -> A) (eq x (inlb tt) -> B)) 简称为T。 T 的任何元素都具有existT x (pair f g) 的形式，其中x : Boole、f : eq x (inrb tt) -> A 和g : eq x (inlb tt) -> B。为了显示您的结果，您需要证明 T 类型的两个表达式相等，这需要在某些时候证明 eq x (inrb tt) -> A 类型的两个术语 f1 和 f2 相等。

问题在于eq x (inrb tt) -> A 的元素是函数：它们将x 和inrb tt 相等的证明作为输入，并产生A 类型的术语作为结果。可悲的是，Coq 中函数相等的概念在大多数情况下都太弱了，无法派上用场。通常在数学中，我们会通过证明它们产生相同的结果来证明两个函数相等，即：

forall f g : A -> B,
  (forall x : A, f x = g x) -> f = g.

这个原则，通常称为功能扩展性，默认情况下在 Coq 中是不可用的。幸运的是，该理论允许我们安全地将其添加为公理，而不会影响理论的合理性。我们甚至可以在标准库中使用它。我在这里提供了一个稍微修改过的结果的证明。 （我冒昧地使用了 ssreflect 库，因为我看到你也在使用它。）

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.

Require Import Coq.Logic.FunctionalExtensionality.

Section Iso.

Variables A B : Type.

Inductive sum' :=
| Sum' x of x = true -> A & x = false -> B.

Definition sum'_of_sum (x : A + B) :=
  match x with
  | inl a =>
    Sum' true
         (fun _ => a)
         (fun e : true = false =>
            match e in _ = c return if c then A else B with
            | erefl => a
            end)
  | inr b =>
    Sum' false
         (fun e =>
            match e in _ = c return if c then A else B with
            | erefl => b
            end)
         (fun _ => b)
  end.

Definition sum_of_sum' (x : sum') : A + B :=
  let: Sum' b f g := x in
  match b return (b = true -> A) -> (b = false -> B) -> A + B with
  | true => fun f _ => inl (f erefl)
  | false => fun _ g => inr (g erefl)
  end f g.

Lemma sum_of_sum'K : cancel sum_of_sum' sum'_of_sum.
Proof.
case=> [[]] /= f g; congr Sum'; apply: functional_extensionality => x //;
by rewrite (eq_axiomK x).
Qed.

End Iso.