16

我正在使用 Coq Proof Assistant 来实现（小型）编程语言的模型（扩展了 Bruno De Fraine、Erik Ernst、Mario Sü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.

extendsJava 中的类扩展机制在哪里，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)

using丢弃有关和的induction H.所有信息。案件变成uvst_refl

u : cname
v : cname
fsv : flds
t : typ
H0 : fields v fsv
============================
 exists fs : flds, fields u (fsv ++ fs)

如您所见，与 中的构造函数相关的信息u以及与中的构造函数相关的信息都丢失了。更糟糕的是，由于这个 Coq 无法看到这一点，并且在这种情况下实际上必须是相同的。vtypHtuv

当inversion在 Coq 上使用该策略时，H成功地看到了这一点u并且v是相同的。然而，这种策略在这里并不适用，因为我需要induction生成的归纳假设来证明st_trans和st_extends案例。

有没有一种策略可以结合最好的inversion和induction生成归纳假设并推导等式，而不会破坏有关构造函数中包含的内容的信息？或者，有没有办法手动获取我需要的信息？info inversion H并且info induction H两者都表明许多转换是自动应用的（尤其是使用inversion）。这些使我在构建的同时尝试了该change策略let ... in，但没有任何进展。

4

3 回答 3

15

当您需要对具有依赖类型 ( ) 且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 模式由内置 tactic 执行。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.
于 2010-12-23T21:06:33.787 回答
7

我遇到了类似的问题，Coq 8.3 的“依赖归纳”策略处理了事务。

于 2011-02-04T15:04:13.007 回答
3

我确信 CPDT 对这个问题有一些评论，但它在哪里并不完全清楚。以下是一些链接：

  1. http://adam.chlipala.net/cpdt/html/Cpdt.Predicates.html “隐式相等的谓词”部分显示了 Coq“丢失信息”的最简单的情况（在破坏，而不是归纳）。还解释了为什么会丢失此信息：当您破坏应用于不是自由变量的参数的类型时，这些类型首先会被自由变量替换（这就是 Coq 丢失信息的原因。）

  2. http://adam.chlipala.net/cpdt/html/Cpdt.Universes.html “避免公理的方法”部分展示了一些避免公理 K 的技巧，包括 Gilles 描述的“等式技巧”。搜索“使用基于等式的通用技巧来支持对类型族的非变量参数的归纳”

我认为这种现象与依赖模式匹配密切相关。

于 2016-05-01T06:00:32.077 回答