类型上的模式匹配，以便在 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

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

这是不可能的，因为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中的类型。其他更强大的语言(例如配备归纳递归(会给你更多的表达能力。