Pulling `let`s to the outside of a statement

Stream: Is there code for X?

[Eric Wieser]

Is there a tactic that can pull let statements to the outermost scope such that they can be introd?

example : (let x := 1 in x) = 1 :=
begin
  change let x := 1 in x = 1,  -- is there a tactic that can do this for me?
  intro,
  -- I want to get `x := 1` in the local context
  sorry,
end

[Mario Carneiro]

no

[Eric Wieser]

A lemma like

lemma apply_let {α : Sort*} {a : α} (β : α → Sort*) (f : Π a, β a) (P : Π {a}, β a → Sort*):
  P (let a' : α := a in f a') = let a' : α := a in P (f a') := rfl

seems not to help, rw can't match it

[Mario Carneiro]

no, and you would be hard-pressed to make that work anyway since f can depend on the defeq a' = a

[Eric Wieser]

Is the defeq not avialable on both the LHS and RHS?

[Eric Wieser]

Is this tactic broken for obvious reasons?

meta def mk_local_lets : expr → tactic (list expr × expr)
| (expr.elet n d v b) := do
  p ← tactic.definev n d v,
  (ps, r) ← mk_local_lets (expr.instantiate_var b p),
  return ((p :: ps), r)
| (expr.app f x) := do
    (fargs, f) ← mk_local_lets f,
    (xargs, x) ← mk_local_lets x,
    pure (fargs ++ xargs, f.app x)
| e := return ([], e)

meta def tactic.interactive.lift_lets : tactic unit :=
do
  (lets, t) ← tactic.target >>= mk_local_lets,
  tactic.change t

[Mario Carneiro]

it doesn't work for binders, but otherwise sure that works

[Eric Wieser]

You mean for the types of binders?

[Eric Wieser]

Or do you more generally mean extracting non-dependent lets?

[Kyle Miller]

@Eric Wieser Here's a Lean 4 version: mathlib4#3893

[Kyle Miller]

Right now it just lifts the lets, but the tactic could also have the additional useful feature to then intro all the lets into the local context (which would be especially useful for lift_lets at h).

[Kyle Miller]

That might also be out of scope for the tactic, and a intro at h might be in order, as suggested at https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20How.20to.20eliminate.20let-statements.20in.20hypothesis/near/357094481

[Kyle Miller]

Though with revert you can do something like intro at h

example (h : let x := 1; x = y) : True := by
  revert h
  lift_lets
  intro x h
  guard_hyp x : Nat := 1
  guard_hyp h :ₛ x = y
  trivial