在使用归纳法时保留信息吗？ [英] Keeping information when using induction?

问题描述

我正在使用Coq Proof Assistant来实现（小型）编程语言的模型（扩展了Bruno De Fraine，Erik Ernst和MarioSüdholt的Featherweight Java实现）。使用归纳策略时不断出现的一件事是如何保留类型构造函数中包装的信息。

I am using the Coq Proof Assistant to implement a model of a (small) programming language (extending an implementation of Featherweight Java by Bruno De Fraine, Erik Ernst, Mario Südholt). One thing that keeps coming up when using the induction tactic is how to preserve the information wrapped in type constructors.

我有一个子类型Prop，实现为

I have a sub typing Prop implemented as

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 是类扩展机制，例如 typ 代表两种可用的类型，

where extends is the class extension mechanism as seen in Java, and typ represents the two different kinds of types available,

Inductive typ : Set :=
| c_typ : cname -> typ
| r_typ : rname -> typ.

我想保留类型信息的示例是使用假设

An example of where I would like type information to be preserved is when using the induction tactic on a hypothesis like

H: sub_type (c_typ u) (c_typ v)

例如in

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)

使用归纳H。丢弃有关 u 和 v 的所有信息。 st_refl 的情况变为

using induction H. discards all information about u and v. The st_refl case becomes

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

如您所见，信息 u 和 v 与 typ H 中的c $ c>构造函数丢失了，从而丢失了 t 。更糟糕的是，由于此Coq无法看到 u 和 v 实际上必须在

As you can see the information that u and v are related to the typ constructors in H, and thus to t, is lost. What is worse is that due to this Coq is unable to see that u and v must in fact be the same in this case.

在 H inversion 策略时> Coq成功地看到 u 和 v 是相同的。但是，该策略不适用于此处，因为我需要归纳假设，即归纳生成的证明 st_trans 和 st_extends 例。

When using the inversion tactic on H Coq succeeds in seeing that u and v are the same. That tactic is not applicable here however, as I need the induction hypotheses that induction generates to prove the st_trans and st_extends cases.

是否有一种策略结合了反转和归纳既可以生成归纳假设并得出相等性，又不会破坏有关构造函数中包装内容的信息？另外，有没有办法手动导出我需要的信息？ info倒置H 和 info归纳H 都表明很多转换都是自动应用的（尤其是倒置）。这些使我尝试了 change 策略以及 let ... in 构造，但是没有任何进展。

Is there a tactic that combines the best of inversion and induction to both generate induction hypotheses and derive equalities without destroying information about what is wrapped in the constructors? Alternatively, is there a way to manually derive the information I need? info inversion H and info induction H both show that a lot of transformations are applied automatically (especially with inversion). These have led me to experiment with the change tactic along with let ... in construction, but without any progress.

推荐答案

当您需要对具有从属类型（ sub_type （c_typ u）（c_typ v）），其参数具有特定的结构（ c_typ u ）。有一个通用的技巧，就是有选择地将结构化参数重写为变量，以保持环境中的相等性。

This is a general problem when you need to induct over a hypothesis with a dependent type (sub_type (c_typ u) (c_typ v)) whose parameters have a particular structure (c_typ u). There is a general trick, which is to selectively rewrite the structured parameter to a variable, keeping the equality in the environment.

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模式由内置策略执行在* goal_occurences * 中将 term 记为 ident 。

Since Coq 8.2, this common set-assert-clearbody pattern is performed by the built-in 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.

---

奖金小费（根据经验，这是一个虽然我不记得详细信息）：当您在类型系统上进行相当语法的推理时（当您进行这类机械证明时，情况经常如此），将输入判断保持在设置。考虑将派生作为您要推理的对象。我记得在某些情况下，在类型导数上引入等式很方便，这在 Prop 中并不总是与类型导数一起使用。

---

Bonus tip (from experience, but it's been a while so I don't remember the details): when you're doing fairly syntactic reasoning on type systems (which tends to be the case when you do these kinds of mechanical proofs), it can be convenient to keep typing judgements in Set. Think of typing derivations as objects you're reasoning about. I remember cases where it was convenient to introduce equalities on typing derivation, which doesn't always work with typing derivations in Prop.

与您的 Problem.v 一起，这是反思性案例的证明。对于传递性，我怀疑您的归纳假设不够充分。这可能是简化问题方式的副产品，尽管可传递性通常确实需要令人惊讶地涉及归纳假设或引理。

With your Problem.v, here's a proof of the reflexivity case. For transitivity, I suspect your induction hypothesis isn't strong enough. This may be a byproduct of the way you simplified the problem, though transitivity often does require surprisingly involved induction hypotheses or lemmas.

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.

这篇关于在使用归纳法时保留信息吗？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！