类型上的模式匹配，以便在 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 的情况还是有其他方法可以区分这种情况？

我在谷歌上搜索了很多，但不幸的是，我大多是偶然发现了有关依赖模式匹配的帖子。

我还尝试用 Scheme Equality for ext 生成一个（布尔）方案，但由于类型参数的原因，这没有成功。

Answer 1

What I'd like to do is somehow distinguish between the cases where the existential type is actually same and where it's not.

这是不可能的，因为 Coq 的逻辑与表示同构类型相等的单价公理兼容。所以尽管 (unit * unit) 和 unit 在句法上是不同的，但 Coq 的逻辑无法区分它们。

一个可能的 work-around 是为您感兴趣的类型创建一个代码数据类型，并将其存储为一个存在项。像这样：

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）会给你更多的表达能力。

类型上的模式匹配，以便在 Coq 中实现存在类型构造函数的相等性

Pattern-match on type in order to implement equality for existentially typed constructor in Coq

coq