问题描述
在用 Coq 中的 Debruijn 索引和替换形式化 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,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 是它的自反、传递闭包）
解决方法
您卡住了，因为 H 上的反演是不够的。相反，您需要对 H 进行某种归纳，以在传递情况下为您提供所需的假设，以便您得出结论。
但是，由于 H 的类型是归纳谓词，因此对其进行归纳是很棘手的。事实上，如果你使用通常的 induction H.，Coq 将丢失所有关于 H 类型索引的信息，尤其是 Var x 类型。这将使您的证明尝试失败。
相反，您可以使用的是依赖 dependent induction 策略（您需要 Require Import Program.Equality 才能使用此策略）。这种策略会自动处理对索引不是变量的归纳谓词的归纳。在这里，您可以从 intros e n H. dependent induction H. 开始您的证明，其余的应该很容易。
通常，当您在归纳数据类型（例如 beta_reduction）上定义归纳谓词（例如 expression），并且您希望使用这些归纳谓词（此处为 H )，直接在谓词上进行归纳（使用 dependent induction），就像我们在这里所做的那样非常强大。特别是，它专门指定了你的数据类型的哪些构造函数可以出现在归纳假设中，从而在某种程度上同时对数据类型进行了一种归纳。
@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.