Cannot Find `Real.add`

Stream: mathlib4

[Kaiyu Yang]

The code below gives me the error unknown constant 'Real.add', but Real.add is defined here. Did I miss something? Thanks!

import Mathlib.Data.Real.Basic

#check Real.add

[Kyle Miller]

It's marked private, which means you're not allowed to reference it outside that module.

[Kaiyu Yang]

But the code below works. I thought marking something with private just means we need to use its fully qualified name for accessing it.

namespace Foo

private def bar := 1

end Foo

#eval Foo.bar

[Kyle Miller]

protected is for fully qualified names.

I guess I don't know the exact semantics of private, but definitely outside the module you can't refer to it anymore. In your example you're still in the same module. (A module isn't a namespace.)

[Kyle Miller]

If you want to circumvent the fact that the designers of Real made Real.add private, you can indirectly refer to it using Real.instAddReal.1, since it's the field inside the Add Real instance. But you're supposed to use + instead of Real.add.

[Kyle Miller]

#xy-ing, why do you need to refer to Real.add?

[Kaiyu Yang]

Ah, I see. I'll try the workaround. Thanks

why do you need to refer to Real.add?

I'm writing some metaprogramming code to translate Lean expressions of real numbers to SMT queries.

[Eric Wieser]

Why not match against HAdd.hAdd? (aka +)

[Kaiyu Yang]

I guess maybe in my use case I just need to use `Real.add instead of ``Real.add.

[Kaiyu Yang]

Why not match against HAdd.hAdd? (aka +)

I'll also try that. Thanks!

[Kyle Miller]

Kaiyu Yang said:

I guess maybe in my use case I just need to use `Real.add instead of ``Real.add.

I don't think that would work -- I believe the way private works is that it gets a name that's not a normal identifier, so you can't refer to it.

[Eric Wieser]

Kaiyu Yang said:

Why not match against HAdd.hAdd? (aka +)

I'll also try that. Thanks!

Better yet would be to use Qq, as let ~q($a + $b) := e

[Kyle Miller]

In particular, x + y is @HAdd.hAdd ℝ ℝ ℝ (@instHAdd ℝ Real.instAddReal) x y, so you can look for @HAdd.hAdd _ _ _ (@instHAdd _ Real.instAddReal) x y (each _ is implied by Real.instAddReal)

[Kyle Miller]

(Eric's Qq suggestion could work too. We sent our messages at the exact same time.)

[Kaiyu Yang]

I'll try them. Thank you both!

[Kyle Miller]

Here's a matcher for real addition. It's not as nice looking as a Qq implementation, and it's less resistant to any changes to the library, but here it is in case it's helpful.

import Mathlib.Data.Real.Basic

open Lean

/-- Given `x + y` of Reals, returns `(x, y)`. Otherwise returns `none`. -/
def Lean.Expr.realAdd? (e : Expr) : Option (Expr × Expr) := do
  guard <| e.isAppOfArity ``HAdd.hAdd 6
  let inst := e.appFn!.appFn!.appArg!
  guard <| inst.isAppOfArity ``instHAdd 2
  guard <| inst.appArg!.isConstOf ``Real.instAddReal
  return (e.appFn!.appArg!, e.appArg!)

open Elab Term in
elab "test" t:term : command => Elab.Command.runTermElabM fun _ => do
  let e ← withSynthesize <| Elab.Term.elabTerm t none
  let e ← instantiateMVars e
  logInfo m!"e = {e}"
  let r := e.realAdd?
  logInfo m!"Got {r}"

test (1 + 2 : ℕ) -- Got none
test (1 + 2 : ℝ) -- Got some ((1, 2))

[Scott Morrison]

I would recommend avoiding using Qq for pattern matching. That part of the Qq implementation is pretty spicy (exciting macros, unclear performance), and we're still thinking about its future.

[Scott Morrison]

Kyle's solution is great.

[Eric Wieser]

Kyle's solution has a pretty major flaw; it matches instances syntactically rather than up to defeq

[Eric Wieser]

So if you have @AddMonoid.toAdd Real.instAddMonoid instead of Real.instAddReal then it doesn't work

[Eric Wieser]

(No offence meant Kyle; your code is fine, but it demonstrates just how easy it is to fall into that instance trap when not using Qq if even a metaproramming expert makes that mistake)

[Kyle Miller]

I'm offended ;-)

[Eric Wieser]

Though I will admit that Qq is not playing ball at all here

[Kyle Miller]

This seems to work, but I can't be sure it's correct:

import Mathlib.Data.Real.Basic

open Lean Meta Qq

/-- Given `x + y` of Reals, returns `(x, y)`. Otherwise returns `none`. -/
def Lean.Expr.realAdd? (e : Expr) : MetaM (Option (Q(ℝ) × Q(ℝ))) := do
  unless ← isDefEq (← inferType e) (.const ``Real []) do
    return none
  have e : Q(ℝ) := e
  let ~q(($x + $y : ℝ)) := e | return none
  return some (x, y)

open Elab Term in
elab "test" t:term : command => Elab.Command.runTermElabM fun _ => do
  let e ← withSynthesize <| Elab.Term.elabTerm t none
  let e ← instantiateMVars e
  logInfo m!"e = {e}"
  let r ← e.realAdd?
  logInfo m!"Got {r}"

test (1 + 2 : ℕ) -- Got none
test (1 + 2 : ℝ) -- Got some ((1, 2))

[Kyle Miller]

I looked at the generated code and it seems like it's doing the right thing.

[Eric Wieser]

Here's my version:

/-- Given `x + y` of Reals, returns `(x, y)`. Otherwise fail. -/
def Lean.Expr.realAdd? (e : Expr) : MetaM (Expr × Expr) := do
  let ⟨Level.succ Level.zero, (t : Q(Type 0)), (e : Q($t))⟩ ← inferTypeQ e | failure
  let ~q(ℝ) := t | failure
  let ~q($a + $b) := e | failure
  pure (a, b)

[Eric Wieser]

It's a shame Qq doesn't let that be combined into a single pattern match

[Eric Wieser]

This looks like a #mwe of the Qq bug:

def foo (e : Nat × Q(Nat)) : MetaM Unit := do
  let .mk u (~q(1)) := e | failure
  return

[Eric Wieser]

It was a one-character fix: quote4#26

[Eric Wieser]

With that change, you can write

/-- Given `x + y` of Reals, returns `(x, y)`. Otherwise returns `none`. -/
def Lean.Expr.realAdd? (e : Expr) : MetaM (Option (Q(ℝ) × Q(ℝ))) := do
  let ⟨Level.succ Level.zero, ~q(ℝ), ~q($a + $b)⟩ ← inferTypeQ e | return none
  return some (a, b)

[Scott Morrison]

#8415 is the Mathlib bump for this.

[Eric Wieser]

quote4#21 is a bit too spicy for me

[Eric Wieser]

lean4#2880 makes it so you can write 1 instead of Level.succ Level.zero there