1

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

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.

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

谢谢您的帮助。

4

1 回答 1

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是相等的，这需要在某些时候证明两个术语f1和f2类型eq x (inrb tt) -> A是相等的。

问题是 的元素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.
于 2017-08-07T12:38:36.153 回答