Zulip Chat Archive

Stream: lean4

Topic: Generalizing let statement


Jad Ghalayini (Jun 29 2022 at 13:49):

I have some code of the form

let x := some complicated expr;
y

and would like to pattern match on the value of x. Is there a nice shorthand to use generalize or some other tactic for this, as I'm struggling to just get it to match the LHS of the let-statement

Jad Ghalayini (Jun 29 2022 at 13:49):

Note that y depends on x here

Alexander Bentkamp (Jun 29 2022 at 14:49):

Can you give a concrete example? Do you mean something like this?

example : let x := 0; x + 5 = 5 := by
  intro x
  generalize h : x = x'
  cases x'
  · exact Nat.zero_add 5
  · exact Nat.noConfusion h

Jad Ghalayini (Jun 29 2022 at 14:52):

I didn't know you could use intro that way; but I was thinking more

(let x := 0; ...) = y

Alexander Bentkamp (Jun 29 2022 at 15:02):

Ok, so like this?

example : (let x := 42; x + 5) = 47 := by
  generalize h : 42 = x'
  show x' + 5 = 47
  sorry

I don't know any way to avoid repeating the "complicated expr" (in my example 42). Is that what you are asking?

Jad Ghalayini (Jun 29 2022 at 15:03):

@Alexander Bentkamp yep; in this case it's this massive abomination post-simp

Sebastian Ullrich (Jun 29 2022 at 15:06):

Do you know about simp (config := { zeta := false })?

Jad Ghalayini (Jun 29 2022 at 21:43):

@Sebastian Ullrich no; but it didn't help; the LHS of the let-statement is obtained by dsimp which for some reason doesn't seem to zeta-expand anyways

Leonardo de Moura (Jul 01 2022 at 13:44):

dsimp which for some reason doesn't seem to zeta-expand anyways

I fixed this issue https://github.com/leanprover/lean4/commit/a639eb185cab63adac2616486c2239a796b7b066

@Jad Ghalayini Could you please post a #mwe?


Last updated: Dec 20 2023 at 11:08 UTC