Fails to unfold function definition

Stream: general

[Aaron Bies]

Hi, does anyone know how I can unfold the definition of evals_to in the example below?

I expected either refl or rw to complete the proof, both fail and hint doesn't help me either

inductive term
  | const : ℕ → term
  | var : ℕ → term
  --| add : term → term → term
  --| mul : term → term → term
  -- ...

def evals_to : ℕ → (ℕ → term) → term → ℕ → Prop
  | _ _ (term.const c) y := c = y
  | (n + 1) env (term.var x) y := evals_to n env (env x) y
  -- ...
  | _ _ _ _ := false

example : evals_to 100 (λ _, term.const 0) (term.const 5) 5 :=
by rw evals_to -- works, completes the goal

example : ∀ (n : ℕ) (env : ℕ → term), evals_to n env (term.const 5) 5 :=
begin
  intros n env,
  rw evals_to, -- fails
end

[Yaël Dillies]

You have to do cases n first. Oh wait, not sure

[Aaron Bies]

wait yes that works

example : ∀ (n : ℕ) (env : ℕ → term), evals_to n (env) (term.const 5) 5 :=
begin
  intros n env,
  cases n;
  rw evals_to,
end

[Aaron Bies]

...but why?

[Eric Wieser]

delta evals_to might work too

[Yaël Dillies]

That's because you defined evals_to by pattern-matching, so the equations are written in terms of the patterns. Namely there must be one for evals_to 0 env (term.const c) y and one for evals_to (n + 1) env (term.const c) y, and apparently Lean isn't smart enough to notice it can unify them.

[Eric Wieser]

Have a look at #print prefix evals_to.equations to see what equations lean generated

[Aaron Bies]

Oh yeah, it did generate _eqn_1 and _eqn_3 for the first case

evals_to.equations._eqn_1 : ∀ (_x : ℕ → term) (c y : ℕ), evals_to 0 _x (term.const c) y = (c = y)
evals_to.equations._eqn_2 : ∀ (_x : ℕ → term) (ᾰ _x_1 : ℕ), evals_to 0 _x (term.var ᾰ) _x_1 = false
evals_to.equations._eqn_3 : ∀ (n : ℕ) (_x : ℕ → term) (c y : ℕ), evals_to n.succ _x (term.const c) y = (c = y)
evals_to.equations._eqn_4 : ∀ (n : ℕ) (env : ℕ → term) (x y : ℕ), evals_to (n + 1) env (term.var x) y = evals_to n env (env x) y

[Aaron Bies]

Welp, time to wrap some things in cases n; { ... }!

[Aaron Bies]

Thank you for clearing that up!