我正在使用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 : rname -> typ.
我希望保存类型信息的一个例子是在induction假设上使用策略时
H: sub_type (c_typ u) (c_typ v)
例如
u : cname
v : cname
fsv : flds
H : sub_type (c_typ u) (c_typ v)
H0 : fields v fsv
============================
exists fs : flds, fields u (fsv ++ fs)
使用induction H.丢弃所有关于u和的信息v.的st_refl情况下,成为
u : cname
v : cname
fsv : flds
t : typ
H0 : fields v fsv
============================
exists fs : flds, fields u (fsv ++ fs)
正如你所看到的信息u,并v都与typ在构造函数H,并因此t,将丢失.更糟的是,由于这种勒柯克无法看到,u而v实际上必须在这种情况下是相同的.
当使用Coq inversion上的策略H成功地看到它u并且v是相同的.然而,这种策略在这里并不适用,因为我需要induction产生的归纳假设来证明这些st_trans和st_extends案例.
是否有一种策略结合了最好的inversion和induction同时产生归纳假设并导出均等性而不破坏有关构造函数中包含的内容的信息？或者,有没有办法手动导出我需要的信息？info inversion H并且info induction H两者都表明自动应用了很多变换(特别是有inversion).这些让我尝试了change战术和let ... in建筑,但没有任何进展.
Gil*_*il' 14
当您需要使用sub_type (c_typ u) (c_typ v)其参数具有特定结构(c_typ u)的依赖类型()来引导假设时,这是一个普遍问题.有一个通用技巧,即有选择地将结构化参数重写为变量,保持环境中的相等性.
set (t1 := c_typ u) in H; assert (Eq1 : t1 = c_typ u) by reflexivity; clearbody t1.
set (t2 := c_typ u) in H; assert (Eq2 : t2 = c_typ u) by reflexivity; clearbody t2.
induction H. (*often "; try subst" or "; try rewrite Eq1; try rewrite Eq2" *).
从Coq 8.2开始,这种常见的set-assert-clearbody模式由内置策略执行.remember term as ident in *goal_occurences*
这是一个使用这种策略证明的愚蠢的引理.
Lemma subtype_r_left_equal :
forall r1 t2, sub_type (r_typ r1) t2 -> r_typ r1 = t2.
Proof.
intros.
remember (r_typ r1) as t1 in H.
induction H.
congruence.
solve [firstorder].
discriminate.
Qed.
奖金提示(来自经验,但它已经有一段时间了,所以我不记得细节):当你在类型系统上进行相当的语法推理时(当你做这些机械校样时往往是这种情况),它可以方便地保持打字判断Set.考虑将派生类型作为您推理的对象.我记得在输入派生时引入平等的方便的情况,这并不总是与输入派生有关Prop.
有了你Problem.v,这里是反身性案例的证明.对于传递性,我怀疑你的归纳假设不够强.这可能是您简化问题的方式的副产品,尽管传递性通常需要令人惊讶地涉及诱导假设或引理.
Fact sub_type_fields: forall u v fsv,
sub_type (c_typ u) (c_typ v) -> fields v fsv ->
exists fs, fields u (fsv ++ fs).
Proof.
intros.
remember (c_typ u) as t1 in H.
remember (c_typ v) as t2 in H.
induction H.
(* case st_refl *)
assert (v = u). congruence. subst v t.
exists nil. rewrite <- app_nil_end. assumption.
(* case st_trans *)
subst t1 t3.
(* case st_extends *)
Admitted.