Coq 证明陷入循环

问题描述

编辑：这是一个新手错误。我错过了 beta_equivalence (Var x) (Application (Abstraction 0) Var x) 的案例。请参考这个问题：

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

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

这些是表达式和 beta_equivalence 的定义


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

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

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

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

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

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

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

1 subgoal
n,y : expression
H0 : beta_equivalence (Var n) (Var x)
H1 : y = Var x
H2 : x0 = Var n
______________________________________(1/1)
Var n = Var x

这正是我开始的。如果我在 H 或 H0 上应用反转，它将再次打开相同的 4 个案例。我是 coq 的新手，可能会犯一个新手错误。任何帮助将不胜感激。

解决方法

暂无找到可以解决该程序问题的有效方法，小编努力寻找整理中！

如果你已经找到好的解决方法，欢迎将解决方案带上本链接一起发送给小编。

小编邮箱:dio#foxmail.com (将#修改为@）

coq lambda-calculus proof