证明定理时循环 [英] Loop while proving a theorem

问题描述

在用Debruijn指数形式化Lambda演算并在Coq中进行替换之后，我试图证明以下定理.

I am trying to prove the following theorem after formalizing lambda calculus with Debruijn indices and substitution in Coq.

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

这些是表达和减少beta的定义

and these are the definitions for expression and beta reduction

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.

在试图证明该定理时，我陷入了一个循环.

I am stuck in a loop while trying to prove this theorem.

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

应用这些步骤之后，这些就是我要使用的假设和子目标

After applying these steps, these are the hypothesis and subgoals I've to work with

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"解决第一个子目标.战术和第二子目标通过反射性".但是，当我到达第三个子目标时，这就是我剩下的

I can solve the first subgoal by "inversion H0" tactic and second subgoal by "reflexivity". However when I reach the third subgoal, this is what I am left with

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.

This is exactly what I started with. I will have to prove that y can only take the value of Var x for H0 to be provable.

(beta_1减少是lambda演算的一步beta减少，beta_reduction是其反射性，传递性封闭)

(beta_1reduction is the one step beta reduction of lambda calculus, and beta_reduction is its reflexive, transitive closure)

推荐答案

@Meven的答案很好地解释了错误所在，并提供了一个很好的解决方案.如果您想在没有依赖性归纳策略的情况下执行此操作，则可以自己记住丢失的信息.

@Meven's answer is a good explanation of what is wrong and gives a good solution. If you want to do it without the dependent induction tactic, you can remember the lost information yourself.

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.

这篇关于证明定理时循环的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！