## Stream: new members

### Topic: Simplify let ... in ... in hypothesis

#### Henning Dieterichs (Dec 04 2020 at 10:28):

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 (Dec 04 2020 at 10:52):

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 (Dec 04 2020 at 10:53):

I assume in your real example z depends on x?

yes

#### Reid Barton (Dec 04 2020 at 10:55):

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

#### Mario Carneiro (Dec 04 2020 at 11:52):

generalize

#### Eric Wieser (Dec 04 2020 at 11:54):

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

no

#### Mario Carneiro (Dec 04 2020 at 11:55):

it's a first time though

#### Henning Dieterichs (Dec 04 2020 at 12:03):

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.

#mwe ?

#### Reid Barton (Dec 04 2020 at 12:08):

oh right that makes sense

#### Reid Barton (Dec 04 2020 at 12:09):

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

#### Mario Carneiro (Dec 04 2020 at 12:16):

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 (Dec 04 2020 at 12:17):

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 (Dec 04 2020 at 12:20):

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 (Dec 04 2020 at 12:21):

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 (Dec 04 2020 at 12:21):

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

#### Eric Wieser (Dec 04 2020 at 12:22):

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

#### Reid Barton (Dec 04 2020 at 12:22):

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

#### Mario Carneiro (Dec 04 2020 at 12:22):

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

#### Eric Wieser (Dec 04 2020 at 12:22):

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

#### Henning Dieterichs (Dec 04 2020 at 12:24):

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 (Dec 04 2020 at 12:47):

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 (Dec 04 2020 at 12:49):

 change _ = g _ at h, also works

Last updated: May 16 2021 at 05:21 UTC