Need help understanding ring_nf

Stream: new members

[Kevin Cheung]

I think I am lacking understanding on how Floats and Real work in Mathlib. In particular, I have a hard time seeing how ring_nf works for foo but not bar in the following:

import Mathlib.Tactic

theorem foo : (0.27 : ℝ) = 27 / 100 := by ring_nf
theorem bar : 0.27 = 27 / 100 := by ring_nf -- why doesn't this work?

How can one find out how Lean interpreted the constants 0.27 and 27 / 100 in bar? I suppose Lean automatically treats 27 / 100 as ℝ in foo. Is that right? Also, is bar actually provable? Any help is greatly appreciated.

[Aaron Liu]

Float is not a docs#CommSemiring, so ring_nf will not work.

[Kevin Cheung]

So, in bar, Lean is treating everything as Float? In this case, is it provable?

[Aaron Liu]

I don't think it is provable, since floats are opaque.

[Kevin Cheung]

It's impossible to prove statements involving floats? For example, the following is unprovable?

example : 0.2 > 0.1 := by sorry

[Walter Moreira]

Kevin Cheung said:

...
How can one find out how Lean interpreted the constants 0.27 and 27 / 100 in bar?
...

For future situations, if you mouse over the term 0.27 in the Lean Infoview, you'll see the way that Lean interprets the literal:

@OfScientific.ofScientific Float instOfScientificFloat 27 true 2 : Float

Does anyone know the programmatic way to obtain what the Infoview is showing? I browsed the metaprogramming book but couldn't find it.

[Aaron Liu]

What do you mean by programmatic?

[Aaron Liu]

Kevin Cheung said:

It's impossible to prove statements involving floats? For example, the following is unprovable?

example : 0.2 > 0.1 := by sorry

This seems to be unprovable.

example : 0.2 > 0.1 := by
  unfold GT.gt LT.lt instLTFloat Float.lt
  unfold OfScientific.ofScientific
  unfold instOfScientificFloat
  show
    FloatSpec.lt
      floatSpec
      (Float.val (Float.ofScientific (nat_lit 1) true (nat_lit 1)))
      (Float.val (Float.ofScientific (nat_lit 2) true (nat_lit 1)))
  -- no further reduction is possible
  sorry

-- `1`, `2`, and `true` are fully reduced terms

-- `floatSpec` and `Float.ofScientific` are opaque constants with no definition

-- `FloatSpec.lt` is a projection coming from the type `FloatSpec`

/--
info: structure FloatSpec : Type 1
number of parameters: 0
fields:
  FloatSpec.float : Type
  FloatSpec.val : self.float
  FloatSpec.lt : self.float → self.float → Prop
  FloatSpec.le : self.float → self.float → Prop
  FloatSpec.decLt : DecidableRel self.lt
  FloatSpec.decLe : DecidableRel self.le
constructor:
  FloatSpec.mk (float : Type) (val : float) (lt le : float → float → Prop) (decLt : DecidableRel lt)
    (decLe : DecidableRel le) : FloatSpec
-/
#guard_msgs in
#print FloatSpec

-- `Float.val` is a projection coming from the type `Float`

/--
info: structure Float : Type
number of parameters: 0
fields:
  Float.val : floatSpec.float
constructor:
  Float.mk (val : floatSpec.float) : Float
-/
#guard_msgs in
#print Float

-- however,
example : 0.2 > 0.1 := by native_decide
-- '_example' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool]

[Vlad Tsyrklevich]

Walter Moreira said:

Does anyone know the programmatic way to obtain what the Infoview is showing?

#check 0.27 ?

[Walter Moreira]

Aaron Liu said:

What do you mean by programmatic?

I was too vague. I would like to find a function or command (similar to #print) that shows the term with the the coercions that Lean is applying.

[Kevin Cheung]

Walter Moreira said:

Aaron Liu said:

What do you mean by programmatic?

I was too vague. I would like to find a function or command (similar to #print) that shows the term with the the coercions that Lean is applying.

I have also been trying to find such a command as well to no avail.

[Kevin Cheung]

Looking at native_decide, it seems that it takes computations from outside the trusted kernel. Is this the only way one can deal with proofs involving Float?

[Walter Moreira]

Vlad Tsyrklevich said:

#check 0.27 ?

Yes, that definitely shows Float as the type of the literal. Is it always guaranteed that will be the coercion in an arbitrary expression (like bar above)?

[Aaron Liu]

Walter Moreira said:

Aaron Liu said:

What do you mean by programmatic?

I was too vague. I would like to find a function or command (similar to #print) that shows the term with the the coercions that Lean is applying.

#print is a command. Is that no good? You can also #check.

[Kevin Cheung]

In the following, #check just shows Prop and #print fails

#check (0.27 > 1 / 5)
#print (0.27 > 1 / 5)

[Kevin Cheung]

But one can hover over the numbers in Infoview to see the full picture for #check. So that works.

[Aaron Liu]

Kevin Cheung said:

But one can hover over the numbers in Infoview to see the full picture for #check. So that works.

Yes, that's what I meant. Is this no good?

[Aaron Liu]

Or do you want to print it without having to hover?

[Luigi Massacci]

Kevin Cheung said:

Looking at native_decide, it seems that it takes computations from outside the trusted kernel. Is this the only way one can deal with proofs involving Float?

Broadly speaking yes, because of what was said above about opaqueness. Having said that, are you sure you want to work with floats as opposed to rationals? floats are really nasty to prove anything about even on paper: addition and multiplication are not associative, do not distribute over each other, etc

[Kevin Cheung]

Yes. Print without hovering, if possible.

[Walter Moreira]

Aaron Liu said:

Kevin Cheung said:

But one can hover over the numbers in Infoview to see the full picture for #check. So that works.

Yes, that's what I meant. Is this no good?

We were hoping to get the more informative term: @OfScientific.ofScientific Float instOfScientificFloat 27 true 2 : Float

[Kevin Cheung]

Luigi Massacci said:

Kevin Cheung said:

Looking at native_decide, it seems that it takes computations from outside the trusted kernel. Is this the only way one can deal with proofs involving Float?

Broadly speaking yes, because of what was said above about opaqueness. Having said that, are you sure you want to work with floats as opposed to rationals? floats are really nasty to prove anything about even on paper: addition and multiplication are not associative, do not distribute over each other, etc

I'm not at the point of doing the following but what if I want to prove some properties about numerical algorithms that work with Float? This kind of work is unavoidable, I think, in numerical analysis.

[Luigi Massacci]

I mean, pen and paper correctness proofs for numerical analysis quite often pretend to work with the reals anyway, which is more than fine in most cases

[Luigi Massacci]

(and given how little numerical stuff there is in lean, right now that would already be a solid project, without worrying about verifying the correctness of an actually runnable implementation)

[Luigi Massacci]

also, for actual software, native_decide is not bad at all

[Luigi Massacci]

If you want examples of working with Float though, you can look at SciLean by @Tomas Skrivan

[Tomas Skrivan]

In SciLean, I have a class RealScalar R(extends RCLike R) that says R behaves like a real number and provides all the basic functions like exp, sin etc. Most of the definitions and theorems are then parameterized by this type Rand instance of RealScalar R. When it comes to actually running the programs I just provide inconsistent instance RealScalar Float.

[Aaron Liu]

I was able to write this (it doesn't handle corner cases), still can't find a builtin command to do it.

import Lean

open Lean Elab Command Meta

syntax (name := see) "#see" term : command

@[command_elab see]
def elabShow : CommandElab
  | `(#see%$tk $term) => withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_show do
    -- -- show signature for `#check id`/`#check @id`
    -- if let `($id:ident) := term then
    --   try
    --     for c in (← realizeGlobalConstWithInfos term) do
    --       addCompletionInfo <| .id term id.getId (danglingDot := false) {} none
    --       logInfoAt tk <| .signature c
    --       return
    --   catch _ => pure ()  -- identifier might not be a constant but constant + projection
    let e ← Term.elabTerm term none
    Term.synthesizeSyntheticMVarsNoPostponing (ignoreStuckTC := true)
    -- Users might be testing out buggy elaborators. Let's typecheck before proceeding:
    withRef tk <| Meta.check e
    let e ← Term.levelMVarToParam (← instantiateMVars e)
    if e.isSyntheticSorry then
      return
    let type ← inferType e
    let str : MessageData ← e.withApp fun f xs ↦
      return xs.foldl (fun m n ↦ m ++ m!" {n}") m!"{f}"
    logInfoAt tk <| str ++ m!" : {type}"
  | _ => throwUnsupportedSyntax

/--
info: @OfScientific.ofScientific Float instOfScientificFloat 27 true 2 : Float
-/
#guard_msgs in
#see 0.27

I did find that norm_num has a command form #norm_num

[Tomas Skrivan]

I would recommend formalizing numerical algorithms something like this. Example for Lagrange interpolating polynomial:

import Mathlib

open Filter Set

-- specification over reals
def lagrangeInterpolSpec (n : ℕ) (f : ℝ → ℝ) (x : ℝ) : ℝ := sorry

-- executable program
def lagrangeInterpol {R} [Add R] [Mul R] [Zero R] [One R] (n : ℕ) (f : R → R) (x : R) : R := sorry

-- exacutable program satisfies the spec
theorem lagrangeInterpol_spec (n : ℕ) (f : ℝ → ℝ) (x : ℝ) :
  lagrangeInterpol n f x = lagrangeInterpolSpec n f x := sorry

-- Lagrange interpolating polynom is actually converging to the function under some assumptions
theorem lagrangeInterpolSpec_limit (f : ℝ → ℝ) (hf : ContDiff ℝ ⊤ f) (x : ℝ) :
  ∀ x ∈ Icc 0 1, f x = lim ((⊤ : Filter ℕ).map (lagrangeInterpolSpec · f x)) := sorry

[Kevin Cheung]

Aaron Liu said:

I was able to write this (it doesn't handle corner cases), still can't find a builtin command to do it.

import Lean

open Lean Elab Command Meta

syntax (name := see) "#see" term : command

@[command_elab see]
def elabShow : CommandElab
  | `(#see%$tk $term) => withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_show do
    -- -- show signature for `#check id`/`#check @id`
    -- if let `($id:ident) := term then
    --   try
    --     for c in (← realizeGlobalConstWithInfos term) do
    --       addCompletionInfo <| .id term id.getId (danglingDot := false) {} none
    --       logInfoAt tk <| .signature c
    --       return
    --   catch _ => pure ()  -- identifier might not be a constant but constant + projection
    let e ← Term.elabTerm term none
    Term.synthesizeSyntheticMVarsNoPostponing (ignoreStuckTC := true)
    -- Users might be testing out buggy elaborators. Let's typecheck before proceeding:
    withRef tk <| Meta.check e
    let e ← Term.levelMVarToParam (← instantiateMVars e)
    if e.isSyntheticSorry then
      return
    let type ← inferType e
    let str : MessageData ← e.withApp fun f xs ↦
      return xs.foldl (fun m n ↦ m ++ m!" {n}") m!"{f}"
    logInfoAt tk <| str ++ m!" : {type}"
  | _ => throwUnsupportedSyntax

/--
info: @OfScientific.ofScientific Float instOfScientificFloat 27 true 2 : Float
-/
#guard_msgs in
#see 0.27

I did find that norm_num has a command form #norm_num

I don't quite understand why without #guard_msgs, #see 0.27 would produce an error. I'm not very familiar with metaprogramming so pardon my ignorance.

[Aaron Liu]

If you comment out #guard_msgs, the docComment gets attached to #see, which is illegal.

[Kevin Cheung]

I see. I guess I don't quite know how docComment works.