Loop while proving a theorem

Question

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

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

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

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_1reduction is the one step beta reduction of lambda calculus, and beta_reduction is its reflexive, transitive closure)

Answer 1

You are stuck because inversion on H is not enough. Instead, you would need a kind of induction on H to provide you with the needed hypothesis in the transitive case, to allow you to conclude. However, since H's type is an inductive predicate, induction on it is tricky. Indeed, if you use the usual induction H., Coq will lose all informations about the indices in H's type, and especially the Var x one. This will make your proof attempts fail.

Instead, what you can use is rely on the dependent induction tactic (you will need to Require Import Program.Equality to have access to this tactic). This tactic automatically handles the kind of induction on inductive predicates where the indices are not variables. Here you could start your proof with intros e n H. dependent induction H. and the rest should be easy.

In general, when you define inductive predicates (such as beta_reduction) over inductive datatypes (such as expression), and you want to use hypothesis using those inductive predicates (here H), doing induction directly on the predicate (using dependent induction) as we did here is very powerful. In particular, it specializes which constructors of your datatype can appear in the inductive hypothesis, thus in a way performs a kind of induction on the datatype at the same time.

Answer 2

@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.