使用归纳法时保留信息？

发布于 2024-10-08 19:46:31 字数 1848 浏览 3 评论 0原文

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

我有一个子类型 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.

我在其中的一个示例希望保留类型信息是在对诸如

H: sub_type (c_typ u) (c_typ v)

E.g. 的假设使用归纳策略时。使用

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 情况变为

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

如您所见，u 和 v 与 typ 构造函数相关的信息如下： code>H 以及 t 都丢失了。更糟糕的是，由于这个原因，Coq 无法看到在这种情况下 u 和 v 实际上一定是相同的。

当在 H 上使用inversion策略时，Coq 成功地发现 u 和 v 是相同的。然而，这种策略在这里并不适用，因为我需要 induction 生成的归纳假设来证明 st_trans 和 st_extends 情况。

是否有一种策略可以结合反演和归纳的优点来生成归纳假设并导出等式，而不破坏有关构造函数中包含的内容的信息？或者，有没有办法手动获取我需要的信息？ 信息反演 H 和 信息归纳 H 都表明许多转换是自动应用的（尤其是反演）。这些导致我尝试使用 change 策略以及 let ... in 构造，但没有任何进展。

原文

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.

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.

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)

E.g. 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)

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)

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.

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.

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.

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

半枫 2024-10-15 19:46:31

当您需要归纳具有依赖类型 (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_occurrences* 执行。

这是使用这种策略证明的一个愚蠢的引理。

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.

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" *).

Since Coq 8.2, this common set-assert-clearbody pattern is performed by the built-in tactic remember term as ident in *goal_occurences*.

Here's a silly lemma proved using this tactic.

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.

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.

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.

回复收藏 0 原文

凉宸 2024-10-15 19:46:31

我遇到了类似的问题，Coq 8.3 的“依赖归纳”策略解决了这个问题。

回复收藏 0 原文

过度放纵 2024-10-15 19:46:31

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

http://adam.chlipala.net/cpdt /html/Cpdt.Predicates.html “具有隐式相等的谓词”部分显示了 Coq“丢失信息”（在析构上，而不是在归纳上）的最简单的情况。它还解释了为什么会丢失此信息：当您破坏应用于非自由变量的参数的类型时，这些类型首先会被替换为自由变量（这就是 Coq 丢失信息的原因。）
http://adam.chlipala.net/cpdt/html/Cpdt.Universes.html “避免公理的方法”部分展示了一些避免公理 K 的技巧，包括 Gilles 描述的“等式技巧”。搜索“使用基于等式的常见技巧来支持对类型族的非变量参数进行归纳”

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

回复收藏 0 原文

~没有更多了~