假设我的数据类型还存在一个存在量化组件的小问题。这次我想定义两个类型的值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，但是由于类型参数的原因，该方案未成功。
我想做的是以某种方式区分存在类型实际上是相同的情况和不存在的情况之间的区别。
这是不可能的，因为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。其他更强大的语言（例如，配备归纳递归的语言）将为您提供更多的表达能力。
本文收集自互联网，转载请注明来源。
如有侵权，请联系 [email protected] 删除。
我来说两句