在 Coq 中表示非不相交联合的方法是什么？

Question

在 Coq 中，

A+B

是类型

A

和

B

的不相交总和。

有没有办法引入两种类型的（可能）不相交的总和？ 例如，如果可能

A

=

B

怎么办？

我在网上找不到任何关于这个的信息，但也许我只是以错误的方式思考这个问题

Answer 1

一般情况下你不能。 Coq 就是所谓的内涵类型理论；这意味着每个术语都会告诉你它是什么类型，所以没有办法拥有两种不同类型的东西。 Disjoint union 是你要做的最好的事情。这是一个重要课程的一个方面：类型不是集合，它们在重要方面的行为不同。

当然，您可能会遇到可以针对特定情况建立工会的情况。但这将是一种只适用于那种情况的特殊类型。

Answer 2

你的意思是这样的吗？

    Require Import List.
    Import ListNotations. 
    Section AB.
      Variables (A B: Type). 
      Let AB := (A + B)%type.
    
      Definition list_inl (l: list A) : list AB :=
        map (fun a  : A   => inl a) l. 
    
      Definition list_inr (l: list B) : list AB :=
        map (fun b  : B   => inr b) l. 
    
      (* heterogeneous append *)
    
      Definition app' (l: list A)(l' : list B) :=
        list_inl l ++ list_inr l'. 
    
      Fixpoint list_pi1 (l: list AB) : list A :=
       match l with
         | nil => nil
         | inl x::tl  => x:: list_pi1 tl
         | _ :: tl => list_pi1 tl
      end.
    
    End AB.

更技术性的方法是 Adam Chlipala 的“异构列表” （http://adam.chlipala.net/cpdt/cpdt.pdf 第 169 页）。