coq - 使用归纳法时保留信息？

Question

我正在使用 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.

哪里 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 ，丢失了。更糟糕的是，由于这个 Coq 无法看到 u和 v在这种情况下实际上必须相同。

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

有没有结合了 inversion最好的战术？和 induction在不破坏构造函数中包装内容的信息的情况下生成归纳假设并导出等式？或者，有没有办法手动获取我需要的信息？ info inversion H和 info induction H两者都表明许多转换是自动应用的(尤其是 inversion )。这些促使我尝试使用 change战术与 let ... in build ，但没有任何进展。

Answer 1

当您需要归纳具有依赖类型 ( 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.