证明定理时循环

Question

在使用 Debruijn 索引和 Coq 中的替换形式化 lambda 演算之后，我试图证明以下定理。

Theorem atom_equality : forall e : expression , forall x : nat,
  (beta_reduction (Var x) e) -> (e = Var x).

这些是表达式和​​β减少的定义

Inductive expression : Type :=
  | Var (n : nat)
  | Abstraction (e : expression)
  | Application (e1 : expression) (e2 : expression).
.
.

Inductive beta_reduction : expression -> expression -> Prop :=
  | beta_1step (x y : expression) : beta_1reduction x y -> beta_reduction x y
  | beta_reflexivity (x : expression) :  beta_reduction x x 
  | beta_transitivity (x y z : expression) : beta_reduction x y -> beta_reduction y z -> beta_reduction x z.

我在试图证明这个定理时陷入了一个循环。

Proof.
intro e. induction e.
  - intros. inversion H.

应用这些步骤后，这些是我必须使用的假设和子目标

3 subgoals
n, x : nat
H : beta_reduction (Var x) (Var n)
x0, y : expression
H0 : beta_1reduction (Var x) (Var n)
H1 : x0 = Var x
H2 : y = Var n
______________________________________(1/3)
Var n = Var x
______________________________________(2/3)
Var n = Var n
______________________________________(3/3)
Var n = Var x

我可以通过“反转 H0”策略解决第一个子目标，通过“反身”策略解决第二个子目标。但是当我达到第三个子目标时，这就是我剩下的

1 subgoal
n, x : nat
H : beta_reduction (Var x) (Var n)
x0, y, z : expression
H0 : beta_reduction (Var x) y
H1 : beta_reduction y (Var n)
H2 : x0 = Var x
H3 : z = Var n
______________________________________(1/1)
Var n = Var x

这正是我开始的。我必须证明 y 只能取 Var x 的值才能证明 H0。

（beta_1reduction是lambda演算的一步beta归约，beta_reduction是它的自反传递闭包）

Answer 1

你被卡住了，因为H 的反转还不够。相反，您需要对H 进行一种归纳，以在传递情况下为您提供所需的假设，以便您得出结论。 然而，由于H 的类型是一个归纳谓词，因此对其进行归纳是很棘手的。事实上，如果你使用通常的induction H.，Coq 将丢失所有关于H 类型索引的信息，尤其是Var x 类型。这将使您的证明尝试失败。

相反，您可以使用dependent induction 策略（您需要Require Import Program.Equality 才能使用此策略）。这种策略会自动处理索引不是变量的归纳谓词的那种归纳。在这里你可以用intros e n H. dependent induction H. 开始你的证明，其余的应该很容易。

一般来说，当您在归纳数据类型（例如 expression）上定义归纳谓词（例如 beta_reduction），并且您想使用这些归纳谓词（此处为 H）使用假设时，直接对我们在这里所做的谓词（使用dependent induction）非常强大。特别是，它专门指定了您的数据类型的哪些构造函数可以出现在归纳假设中，从而在某种程度上同时对数据类型执行一种归纳。

Answer 2

@Meven 的回答很好地解释了问题所在，并提供了很好的解决方案。如果您不想使用dependent induction 策略，您可以自己remember 丢失的信息。

Proof.
  (beta_reduction (Var x) e) -> (e = Var x).
  intros e x H.
  remember (Var x) as q eqn:Hq.
  induction H; rewrite Hq in *. 
  - inversion H.
  - reflexivity.
  - rewrite IHbeta_reduction1 in IHbeta_reduction2.
    apply IHbeta_reduction2.
    reflexivity.
    reflexivity.
Qed.