相关疑难解决方法(0)

我正在使用Coq Proof Assistant来实现(小)编程语言的模型(扩展由Bruno De Fraine,Erik Ernst,MarioSüdholt执行的Featherweight Java).使用induction策略时不断出现的一件事是如何保存包含在类型构造函数中的信息.

我有一个子类型Prop实现为

Inductive sub_type : typ -> typ -> Prop :=
| st_refl : forall t, sub_type t t
| st_trans : forall t1 t2 t3, sub_type t1 t2 -> sub_type t2 t3 -> sub_type t1 t3
| st_extends : forall C D,
    extends C D ->
    sub_type (c_typ C) (c_typ D).

Hint Constructors sub_type.

extends在Java中看到的类扩展机制在哪里,它typ表示可用的两种不同类型,

Inductive typ : Set :=
| c_typ : cname -> typ
| r_typ …