Simplify `let ... in ...` in hypothesis

Stream: new members

[Henning Dieterichs]

How can I deconstruct an hypothesis of the form h: a = let x = y in z x into x: ..., h1: x = y and h2: a = z[x]? I tried cases and simp, both inlined x into y which I want to avoid, as it becomes an unreadable mess.

[Henning Dieterichs]

It seems like this works:

set x = y,
have h1: a = z x := h,

It is a little bit magic though, as have h1 := h does nothing.

[Eric Wieser]

I assume in your real example z depends on x?

[Henning Dieterichs]

yes

[Reid Barton]

I think there's a version of set which doesn't introduce a let binding

[Mario Carneiro]

generalize

[Eric Wieser]

Does generalize avoid the need to write x = y a second time?

[Mario Carneiro]

no

[Mario Carneiro]

it's a first time though

[Henning Dieterichs]

This does not work anymore though:

generalize x_def: y = x,
have h1: a = z x := h,

I.e. I don't know how to get rid of the let in in h with this.
Lean gets rid of it automatically when using set.

[Kevin Buzzard]

#mwe ?

[Reid Barton]

oh right that makes sense

[Reid Barton]

There's also a tactic to clear the let binding part of a hypothesis

[Mario Carneiro]

I wonder if rcases can be modified to capture let bindings. It's a bit tricky because whnf will go right past a let binding

[Henning Dieterichs]

def f (x: nat) := (x, x)
def g (x: nat × nat) := x.fst + x.snd

lemma mwe (x: nat) (h: x = let y := f x in g y): x = 0 :=
begin
    set y := f x,
    have y_def: y = f x, { simp [y] },
    replace h: x = g y := h,

    sorry,
end

Somewhat artificial though. How can I get to the sorry with the same state more elegantly?

[Mario Carneiro]

Actually, perhaps a better interface is some kind of split_lets that will extract let statements in the targeted hyp(s) and introduce new variables like set

[Kevin Buzzard]

import tactic

def f (x: nat) := (x, x)
def g (x: nat × nat) := x.fst + x.snd

lemma mwe (x: nat) (h: x = let y := f x in g y): x = 0 :=
begin
    set y := f x with y_def,
    simp at h,
    sorry,
end

is one less line and also less painful

[Mario Carneiro]

this still doesn't solve the problem of a let under a lambda though

[Eric Wieser]

While not what this thread is about, note that intro will slice off a let from the goal

[Reid Barton]

maybe in Lean 4 we can just reuse the lambda lifting pass

[Mario Carneiro]

actually maybe there is a dsimp option for doing beta reduction but not zeta (let reduction)

[Eric Wieser]

Of course intro at would be silly for the other meanings of intro

[Henning Dieterichs]

Kevin Buzzard said:

import tactic

def f (x: nat) := (x, x)
def g (x: nat × nat) := x.fst + x.snd

lemma mwe (x: nat) (h: x = let y := f x in g y): x = 0 :=
begin
    set y := f x with y_def,
    simp at h,
    sorry,
end

is one less line and also less painful

Thanks! Didn't know about with in set. I thought I should avoid non-goal closing simps though?

[Kevin Buzzard]

For me the whole point of set is the with. You're right -- simp only [y_def] at h, is better for the second line.

[Kevin Buzzard]

change _ = g _ at h, also works