Extracting left-hand side from an equality

Stream: new members

[Kevin Cheung]

If I have something like h : a + b + c = 0, is there syntax to refer to the left-hand side a + b + c? I want to be able to do something like let g := (the left-side of the equality in h).

[Kevin Buzzard]

Can you un-xy? Why do you want to give the left hand side of the equality a name?

[Kevin Cheung]

Because I am going to refer to the left-hand side many times (not exactly this expression here) but don't want to retype the whole thing. (In my case, the left-hand side is very long.)

[Matt Diamond]

You know, there was a great trick for this in Lean 3, where you could do something like this:

-- Lean 3 code

import data.nat.basic

example (a b c d e : nat) (h : a + b + c + d + e = 0) : false :=
begin
  let foo := _,
  change foo = 0 at h,
  sorry,
end

[Matt Diamond]

I don't know if it works in Lean 4 though

[Kyle Miller]

Here's something we could have:

import Mathlib.Lean.Expr.Basic

open Lean Meta

elab "lhs%" t:term : term => do
  let e ← Elab.Term.elabTerm t none
  if let some (_, lhs, _, _rhs) := (← inferType e).sides? then
    return lhs
  else
    throwError m!"Not an equality, iff, or HEq:{indentD e}"

elab "rhs%" t:term : term => do
  let e ← Elab.Term.elabTerm t none
  if let some (_, _lhs, _, rhs) := (← inferType e).sides? then
    return rhs
  else
    throwError m!"Not an equality, iff, or HEq:{indentD e}"

example {a b c : Nat} (h : a + b + c = 0) : False := by
  let g := lhs% h
  /-
  g : Nat := a + b + c
  -/

[Kyle Miller]

@Matt Diamond I tried a few tricks, but couldn't get that to work.

[Matt Diamond]

That's unfortunate... it was pretty useful for handling unwieldy expressions

[Matt Diamond]

it would be cool if the change tactic automatically created variables for you if they don't already exist

[Matt Diamond]

@Kevin Cheung Are you familiar with the set tactic? You could use that to define a new variable and it should automatically update any hypotheses that match the definition. The only downside is that you'll need to write out the expression (but only once).

import Mathlib

example (a b c d e : ℕ) (h : a + b * c - d + e = 0) : False := by
  set foo := a + b * c - d + e -- h's type is now `foo = 0`
  sorry

[Jireh Loreaux]

I think @Gareth Ma was working on a setm tactic for this a while back, with advice from @Thomas Murrills. There's probably a PR around somewhere.

[Gareth Ma]

Hi yes… my real life got busy and I couldn’t do any Lean the past weeks

[Gareth Ma]

I can find it, it’s somewhere

[Gareth Ma]

https://github.com/leanprover-community/mathlib4/pull/7890

[Gareth Ma]

I don’t remember exactly what’s missing, but it must be something I didn’t understand, otherwise I would’ve implemented it lol

[Kyle Miller]

@Matt Diamond I hacked your idea together

example {a b c : Nat} (h : a + b + c = 0) : False := by
  change x = _ at h
  /-
  a b c : ℕ
  x : ℕ := a + b + c
  h : x = 0
  ⊢ False
  -/

code

import Mathlib.Tactic

open Lean Elab Term

open Meta in
def withReverted
    {m : Type → Type} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] [MonadInfoTree m]
    {α : Type} (mvarId : MVarId) (fvarIds : Array FVarId)
    (k : MVarId → Array FVarId → m (α × MVarId))
    (clearAuxDeclsInsteadOfRevert := false) : m (α × Array FVarId × MVarId) := do
  let (xs, mvarId) ← mvarId.revert fvarIds true clearAuxDeclsInsteadOfRevert
  let (r, mvarId) ← k mvarId xs
  let (ys, mvarId) ← mvarId.introNP xs.size
  mvarId.withContext do
    for x in xs, y in ys do
      pushInfoLeaf (.ofFVarAliasInfo { id := y, baseId := x, userName := ← y.getUserName })
  return (r, ys, mvarId)

partial def withAutoBoundLet {α : Type _} (k : TermElabM α) : TermElabM α := do
  withReader (fun ctx => { ctx with autoBoundImplicit := true, autoBoundImplicits := {} }) do
    let rec loop (s : SavedState) : TermElabM α := do
      try
        k
      catch
        | ex => match isAutoBoundImplicitLocalException? ex with
          | some n =>
            -- Restore state, declare `n`, and try again
            s.restore
            let val ← Meta.mkFreshExprMVar none
            Meta.withLetDecl n (← Meta.inferType val) val fun x =>
              withReader (fun ctx => { ctx with autoBoundImplicits := ctx.autoBoundImplicits.push x } ) do
                loop (← saveState)
          | none   => throw ex
    loop (← saveState)

open Tactic in
elab_rules : tactic
  | `(tactic| change $newType:term $[$loc:location]?) => do
    withLocation (expandOptLocation (Lean.mkOptionalNode loc))
      (atLocal := fun h => withSynthesize do
        let g ← getMainGoal
        let hTy ← h.getType
        let (mvar, h', g) ← withReverted g #[h] fun g _ => do
          g.withContext <| withAutoBoundLet do
            let auto := (← read).autoBoundImplicits.toArray
            let g ← auto.foldlM (init := g) (fun g fvar => do
              let decl ← fvar.fvarId!.getDecl
              Prod.snd <$> g.let decl.userName decl.value decl.type)
            g.withContext do
            let mvar ← Meta.mkFreshExprMVar none
            let _ ← Term.elabTerm (← `(term | show $newType from $(← Term.exprToSyntax mvar))) hTy
            pure (mvar, g)
        let #[h] := h' | throwError "internal error with fvars"
        g.withContext do
        let g ← g.changeLocalDecl' h (← Meta.inferType mvar)
        replaceMainGoal [g])
      (atTarget := throwError "unimplemented")
      (failed := fun _ => throwError "change tactic failed")

example {a b c : Nat} (h : a + b + c = 0) : False := by
  change x = _ at h
  /-
  a b c : ℕ
  x : ℕ := a + b + c
  h : x = 0
  ⊢ False
  -/

[Kyle Miller]

I'm not sure this is a good default for change, but it's interesting and worth considering as a tactic.

[Matt Diamond]

nice! yeah perhaps it could be a separate tactic

[Matt Diamond]

Gareth's setm seems similar in function, just with slightly different syntax

[Yaël Dillies]

I would have expected the syntax to be change ?x = _ at h

[Eric Wieser]

Or perhaps $x

[Yaël Dillies]

I think it shouldn't be a separate tactic if we manage to make one of Eric's or my syntax work

[Kevin Cheung]

Matt Diamond said:

Kevin Cheung Are you familiar with the set tactic? You could use that to define a new variable and it should automatically update any hypotheses that match the definition. The only downside is that you'll need to write out the expression (but only once).

import Mathlib

example (a b c d e : ℕ) (h : a + b * c - d + e = 0) : False := by
  set foo := a + b * c - d + e -- h's type is now `foo = 0`
  sorry

I didn't know about set, only let and have. This could work. Thanks!

[Kyle Miller]

Yaël Dillies said:

I would have expected the syntax to be change ?x = _ at h

Sure -- my experiment was just to see if I could misuse the autoImplicits mechanism to get this to work. Maybe there will be a tactic one day where it'll be useful to auto-add additional let bindings like this.

[Kyle Miller]

Gareth's setm uses ?x and it seems like a better idea on the grounds that you can predict what the new let bindings will be.

[Kyle Miller]

I just discovered a hack to get the Lean 3 trick @Matt Diamond mentioned to work:

import Mathlib.Data.Nat.Basic

example (a b c d e : ℕ) (h : a + b + c + d + e = 0) : False := by
  let foo : ?_ := ?_
  replace h := (by refine h : foo = 0)
  /-
  a b c d e : ℕ
  foo : ℕ := a + b + c + d + e
  h : foo = 0
  ⊢ False
  -/
  sorry

[Kyle Miller]

Here's a variation on it:

import Mathlib.Data.Nat.Basic

example (a b c d e : ℕ) (h : a + b + c + d + e = 0) : False := by
  let foo : ?_ := ?_
  change type_of% (by refine h : foo = 0) at h
  /-
  a b c d e : ℕ
  foo : ℕ := a + b + c + d + e
  h : foo = 0
  ⊢ False
  -/
  sorry

[Kyle Miller]

There's a chance I just coded change ... at ... wrong and there's a way to get change foo = 0 at h by itself to work here. I think I remember that there was a tradeoff between change foo = 0 at h working and typeclass instance synthesis succeeding for things like numerals.

[Kyle Miller]

Getting change to work for this without breaking hasn't been successful yet. std4#555 is an attempt, but it seems to be choosing the wrong instances in Std.Data.Int.DivMod. I'm not sure why it's picking up on Nat instances rather than unifying with the Int ones if there's nothing that I can see triggering default instances.

[Kevin Cheung]

Kyle Miller said:

I just discovered a hack to get the Lean 3 trick Matt Diamond mentioned to work:

import Mathlib.Data.Nat.Basic

example (a b c d e : ℕ) (h : a + b + c + d + e = 0) : False := by
  let foo : ?_ := ?_
  replace h := (by refine h : foo = 0)
  /-
  a b c d e : ℕ
  foo : ℕ := a + b + c + d + e
  h : foo = 0
  ⊢ False
  -/
  sorry

This is amazing. But it looks like magic to me. What are refine and replace actually doing under the hood?

[Kyle Miller]

The replace tactic is cheating and not actually changing h, but replacing it.

The key trick is that refine has the power to assign to ?_ metavariables at a certain step, and these are normally not assignable. (In std4#555 I tried giving change this power)

[Kevin Cheung]

I see.