Way to use `set` without having to copy-paste expression?

Stream: new members

[Jakub Nowak]

Is it possible to do the same, but without having to mention some_long_and_complicated_expr? E.g., by selecting it with conv => lhs.

import Mathlib

opaque some_long_and_complicated_expr : Nat

example : some_long_and_complicated_expr = 0 := by
  set p := some_long_and_complicated_expr

[Aaron Liu]

import Mathlib

opaque some_long_and_complicated_expr : Nat

example : some_long_and_complicated_expr = 0 := by
  refine let p := _; (?_ : p = _)

[Jakub Nowak]

Is there a way to do let instead of set?

import Mathlib

opaque some_long_and_complicated_expr : Nat

example : some_long_and_complicated_expr = 0 := by
  let p := some_long_and_complicated_expr

[Jakub Nowak]

I guess I can just unfold p.

[Aaron Liu]

import Mathlib

opaque some_long_and_complicated_expr : Nat

example : some_long_and_complicated_expr = 0 := by
  refine let p := _; (?_ : zeta% p = _)

[Jakub Nowak]

Is that idiomatic? I could find any use of that pattern in mathlib.

[Aaron Liu]

no idea

[Aaron Liu]

but it works

[Aaron Liu]

I don't really know a better way

[Robin Arnez]

I would've first thought about

show ?a = 0
let p := ?a

[Aaron Liu]

then you end up with a named metavariable

[Aaron Liu]

so it doesn't work for example if there's already something called ?a

[Aaron Liu]

and you also can't ever use the name ?a again in that proof

[Aaron Liu]

or maybe in the by block? I don't really know how this works

[Ruben Van de Velde]

import Mathlib

opaque some_long_and_complicated_expr : Nat

example : some_long_and_complicated_expr = 0 := by
  set p := _
  change p = 0
  sorry

seems to work

[Ruben Van de Velde]

Does it work robustly? I haven't a clue

[Aaron Liu]

I wonder if we can get like an expression language? to manipulate expressions

[Jakub Nowak]

@Aaron Liu Isn't that conv? Maybe we could have a conv tactic that does set/let on current conv goal? Something like

conv
  lhs
  set p

[Aaron Liu]

not really

[Aaron Liu]

conv has to prove the new expression is equal to the original

[Ruben Van de Velde]

I think a tactic like foo ?p = ?x + ?y would be cool

[Jakub Nowak]

Unfortunately all mentioned ways require repeating names of functions and don't work well with dot notation.

import Mathlib

opaque some_long_and_complicated_expr : Nat
opaque Nat.some_long_function_name : Nat → Prop

example : some_long_and_complicated_expr.some_long_function_name := by
  set p := _
  change Nat.some_long_function_name p

[Aaron Liu]

import Mathlib

opaque some_long_and_complicated_expr : Nat
opaque Nat.some_long_function_name : Nat → Prop

example : some_long_and_complicated_expr.some_long_function_name := by
  set p := _
  conv =>
    enter [1]
    change p
  guard_target =ₛ p.some_long_function_name
  sorry

[Matt Diamond]

you can also use change with metavariables before the set statement (e.g. change ?x = ?y; set x := ?x; set y := ?y) but I'm guessing that runs into the same drawbacks as the other approaches (with the additional drawback that Lean complains about the change tactic not accomplishing anything)

[Bbbbbbbbba]

Is there a way discussed here that works for reducing duplication in the declaration of the statement to prove? (In plain words, what if some_long_and_complicated_expr appears within the statement many times?)

[Jakub Nowak]

Exactly the same should work, because set replaces all occurrences of an expression. It doesn't work for you?
Nvm, it indeed doesn't work with set p := _; conv approach.

[Jakub Nowak]

It works with change if you repeat p:

import Mathlib

opaque some_long_and_complicated_expr : Nat

example : some_long_and_complicated_expr = some_long_and_complicated_expr + 1 := by
  set p := some_long_and_complicated_expr
  guard_target =ₛ p = p + 1

example : some_long_and_complicated_expr = some_long_and_complicated_expr + 1 := by
  set p := _
  change p = p + 1
  guard_target =ₛ p = p + 1

example : some_long_and_complicated_expr = some_long_and_complicated_expr + 1 := by
  set p := _
  conv =>
    lhs
    change p
  guard_target =ₛ p = some_long_and_complicated_expr + 1

Anyone understands why the last one doesn't work, and whether we could fix this? Tbh, I don't even understand why it even works in the first place, specifically why it only works with set, but not let or have.

[Aaron Liu]

It's because set does replacement when you run the tactic and not at any time after

[Aaron Liu]

Jakub Nowak said:

Tbh, I don't even understand why it even works in the first place, specifically why it only works with set, but not let or have.

Maybe a metavariables thing?

[Jakub Nowak]

This works:

import Mathlib

opaque some_long_and_complicated_expr : Nat

example : some_long_and_complicated_expr = some_long_and_complicated_expr + 1 := by
  set p' := _
  conv =>
    lhs
    change p'
  unfold p'
  set p := zeta% p'
  clear p'

[Jakub Nowak]

Is there a tactic that combines unfold, set, and clear?