# Zulip Chat Archive

## 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`

?

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

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?

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

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`

.

#### Kevin Buzzard (Dec 04 2020 at 12:05):

#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