模式匹配的類型爲了實現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）會給你更多的表現力。