模式匹配的类型为了实现Coq中存在类型的构造函数的相等性

Question

假设我的数据类型与存在量化组件存在一个小问题。这次我想定义何时两个值类型ext相等。

Inductive ext (A: Set) := 
| ext_ : forall (X: Set), option X -> ext A. 

Fail Definition ext_eq (A: Set) (x y: ext A) : Prop := 
    match x with 
    | ext_ _ ox => match y with 
       | ext_ _ oy => (* only when they have the same types *) 
           ox = oy 
       end 
    end. 

我想要做的是以某种方式区分存在类型实际上相同和不存在的情况。这是JMeq的情况还是有其他方式来完成这种情况区分？

我google了很多，但不幸的是我大多偶然发现关于依赖模式匹配的帖子。

我也试着用Scheme Equality for ext生成一个（布尔型）方案，但是由于类型参数，这是不成功的。

Answer 1

我想要做的是以某种方式区分存在类型实际上相同和不存在的情况。

这是不可能的，因为Coq的逻辑与同构类型相等的单一公理相容。因此，即使(unit * unit)和unit在句法上不同，它们也不能通过Coq的逻辑进行区分。

可能的解决方法是为您感兴趣的类型设置一个数据类型的代码并将其存储为存在。事情是这样的：

Inductive Code : Type := 
    | Nat : Code 
    | List : Code -> Code. 

Fixpoint meaning (c : Code) := match c with 
    | Nat  => nat 
    | List c' => list (meaning c') 
end. 

Inductive ext (A: Set) := 
    | ext_ : forall (c: Code), option (meaning c) -> ext A. 

Lemma Code_eq_dec : forall (c d : Code), { c = d } + { c <> d }. 
Proof. 
intros c; induction c; intros d; destruct d. 
- left ; reflexivity. 
- right ; inversion 1. 
- right ; inversion 1. 
- destruct (IHc d). 
    + left ; congruence. 
    + right; inversion 1; contradiction. 
Defined. 

Definition ext_eq (A: Set) (x y: ext A) : Prop. 
refine(
    match x with | @ext_ _ c ox => 
    match y with | @ext_ _ d oy => 
    match Code_eq_dec c d with 
    | left eq => _ 
    | right neq => False 
    end end end). 
subst; exact (ox = oy). 
Defined. 

然而，这显然限制颇多的那种类型，你可以在ext包。其他功能更强大的语言（例如配备Induction-recursion）会给你更多的表现力。