Unfolding into ite?

Stream: lean4

[Ryan Lahfa]

I'm trying to do some simple program verification using Lean 4 and I have this little de Bruijn indexes formalization:

import Lean
open Classical

inductive LambdaTerm where
| var (val : Nat)
| app (fn: LambdaTerm) (arg: LambdaTerm)
| lambda (body: LambdaTerm)

def allFreeVariablesBoundBy (n: Nat) (t: LambdaTerm): Prop :=
  aux n t 0
where
  aux n t depth : Prop := match t with
| LambdaTerm.var (val := m) => m < n + depth
| LambdaTerm.app (fn := fn) (arg := arg) => aux n fn depth ∧ aux n arg depth
| LambdaTerm.lambda (body := fn) => aux n fn (depth + 1)

macro "C[" n:term "](" t:term ")" : term => `(allFreeVariablesBoundBy $n $t)
def isClosedTerm (t: LambdaTerm): Prop := C[0](t)

def substitute (t: LambdaTerm) (index: Nat) (expr: LambdaTerm): LambdaTerm :=
  aux index t 0
where
  aux i t depth : LambdaTerm := match t with
  | LambdaTerm.var (val := m) => if i + depth = m then expr else t
  | LambdaTerm.app fn arg => LambdaTerm.app (aux i fn depth) (aux i arg depth)
  | LambdaTerm.lambda body => LambdaTerm.lambda (aux i body (depth + 1))

theorem substitute.idOnClosed (depth: Nat) (t: LambdaTerm) (ht: C[depth](t)) (index: Nat) (expr: LambdaTerm) (hexpr: isClosedTerm expr): substitute.aux t index expr depth = t :=
by induction t with
| var m => have p: index + depth ≠ m := sorry; admit
| app fn arg h_fn h_arg => admit
| lambda body h_body => admit

In substitute.idOnClosed, I'm trying to reduce the goal to its (if i + depth = m then expr else LambdaTerm.var m) = LambdaTerm.var m form so I can apply ifNeg and rfl, but I'm unable to see how to do it. I also searched here but without any luck.

I tried change which is not implemented, simp, dsimp and other similar things, and re-read the tests/examples provided in the repository.

[Mario Carneiro]

Although change is not implemented, show exists and does the same thing

[Mario Carneiro]

You've done induction on the wrong variable, t and expr are flipped

[Mario Carneiro]

theorem substitute.idOnClosed (depth: Nat) (t: LambdaTerm) (ht: C[depth](t))
  (index: Nat) (expr: LambdaTerm) (hexpr: isClosedTerm expr):
  substitute.aux expr index t depth = t :=
by induction t with
| var m => have p: index + depth ≠ m := sorry; simp [aux, p]
| app fn arg h_fn h_arg => admit
| lambda body h_body => admit

[Ryan Lahfa]

Mario Carneiro said:

theorem substitute.idOnClosed (depth: Nat) (t: LambdaTerm) (ht: C[depth](t))
  (index: Nat) (expr: LambdaTerm) (hexpr: isClosedTerm expr):
  substitute.aux expr index t depth = t :=
by induction t with
| var m => have p: index + depth ≠ m := sorry; simp [aux, p]
| app fn arg h_fn h_arg => admit
| lambda body h_body => admit

Uh! Many thanks!