Zulip Chat Archive

Stream: new members

Topic: Simplify `let ... in ...` in hypothesis


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Dec 04 2020 at 10:53):

I assume in your real example z depends on x?

view this post on Zulip Henning Dieterichs (Dec 04 2020 at 10:53):

yes

view this post on Zulip Reid Barton (Dec 04 2020 at 10:55):

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

view this post on Zulip Mario Carneiro (Dec 04 2020 at 11:52):

generalize

view this post on Zulip Eric Wieser (Dec 04 2020 at 11:54):

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

view this post on Zulip Mario Carneiro (Dec 04 2020 at 11:55):

no

view this post on Zulip Mario Carneiro (Dec 04 2020 at 11:55):

it's a first time though

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Dec 04 2020 at 12:05):

#mwe ?

view this post on Zulip Reid Barton (Dec 04 2020 at 12:08):

oh right that makes sense

view this post on Zulip Reid Barton (Dec 04 2020 at 12:09):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 04 2020 at 12:21):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Dec 04 2020 at 12:22):

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

view this post on Zulip Mario Carneiro (Dec 04 2020 at 12:22):

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

view this post on Zulip Eric Wieser (Dec 04 2020 at 12:22):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Dec 04 2020 at 12:49):

change _ = g _ at h, also works


Last updated: May 16 2021 at 05:21 UTC