Lean.ToExpr Rat

Stream: Is there code for X?

[Eric Wieser]

Aaron Liu said:

deriving instance Lean.ToExpr for Rat

I'm surprised that this isn't somewhere in mathlib already

[Eric Wieser]

Though I guess there's the question of whether it should use a / b or OfScientific

[Aaron Liu]

Eric Wieser said:

Though I guess there's the question of whether it should use a / b or OfScientific

How would you use OfScientific?

[Eric Wieser]

Only when b is of the form $2^x5^y$ I guess

[Aaron Liu]

that sounds like it will cause some people debugging hell later

[Eric Wieser]

You mean to say that people care about other primes too?

[Eric Wieser]

You're right though, / is the reasonable choice

[Aaron Liu]

Is this a reasonable implementation?

import Batteries.Data.Rat.Basic
import Lean.ToExpr

open Lean

instance : ToExpr Rat where
  toTypeExpr := .const ``Rat []
  toExpr q :=
    let lit r := mkApp3 (.const ``OfNat.ofNat [levelZero]) (.const ``Rat [])
      (mkRawNatLit r) (.app (.const ``Rat.instOfNat []) (mkRawNatLit r))
    let numAbs := lit q.num.natAbs
    let num :=
      if q.num ≥ 0 then numAbs else
        mkApp3 (.const ``Neg.neg [levelZero]) (.const ``Rat []) (.const ``Rat.instNeg []) numAbs
    if q.den = 1 then num else
      let den := lit q.den
      mkApp6 (.const ``HDiv.hDiv [levelZero, levelZero, levelZero])
        (.const ``Rat []) (.const ``Rat []) (.const ``Rat [])
        (mkApp2 (.const ``instHDiv [levelZero]) (.const ``Rat []) (.const ``Rat.instDiv []))
        num den

[Eric Wieser]

I think we already have most of an instance inside norm_num

[Eric Wieser]

I guess the other question is whether we want (-a) / b or -(a/b)

[Aaron Liu]

(-a) / b pretty prints as -a / b, and -(a/b) pretty prints as -(a / b)

[Andrew Yang]

the normal form in norm_num is also (-a) / b

[Eric Wieser]

Neither of docs#neg_div or docs#neg_div' are simp though, interestingly

[Eric Wieser]

Andrew Yang said:

the normal form in norm_num is also (-a) / b

Nice evidence that the toExpr function almost already exists!

[Eric Wieser]

This is the closest I got when I needed it quickly before:

-- hack, this should be constructed inline
def mkRatQ (q : ℚ) : MetaM Q(ℝ) := do
  have m'n : Q(ℕ) := mkRawIntLit q.num
  have m'd : Q(ℕ) := mkRawNatLit q.den
  have r : Result q(0 : ℝ) := .isRat' q(inferInstance) q (m'n) (m'd) q(sorry)
  let ⟨(m' : Q(ℝ)), hm', _⟩ ← r.toSimpResult
  return m'

[Eric Wieser]

Where the relevant code is here

[Notification Bot]

16 messages were moved here from #new members > Unexpected token when deriving instance by Eric Wieser.

[Mario Carneiro]

Eric Wieser said:

Where the relevant code is here

This seems to contradict the claim that the normal form in norm_num is (-a) / b

[Mario Carneiro]

I can clearly see -(a / b) there

[Mario Carneiro]

and a test like example : -1 / (2:Rat) = sorry := by norm_num normalizes to -(1 / 2)

[Kyle Miller]

The pp.numericTypes option assumes that rational numbers are of the form HDiv.hDiv (nat <|> Neg.neg nat) nat for what it's worth.

[Eric Wieser]

I think that's the right behavior for printing whatever the norm_num-normal form is, to avoid printing (-(a / b) : Rat)