Why doesn't this work for ℝ?

Stream: mathlib4

[Markus Schmaus]

I'm looking into formalizing the notion that a Float approximates a real number.

For some reason the following code works for ℚ, but for some reason it throws an error for ℝ.

import Mathlib

inductive IsApproxℚ : Float → ℚ → Prop :=
  | ofNat (base : ℕ) : IsApproxℚ (Float.ofNat base) base

example : IsApproxℚ (Float.ofNat 1) 1 := by
  apply IsApproxℚ.ofNat

inductive IsApproxℝ : Float → ℝ → Prop :=
  | ofNat (base : ℕ) : IsApproxℝ (Float.ofNat base) base

example : IsApproxℝ (Float.ofNat 1) 1 := by
  apply IsApproxℝ.ofNat

Why is that? Can I make this work somehow?

[Markus Schmaus]

Here is the error message:

tactic 'apply' failed, failed to unify
  IsApproxℝ (Float.ofNat ?base) ↑?base
with
  IsApproxℝ (Float.ofNat 1) 1
⊢ IsApproxℝ (Float.ofNat 1) 1

[Damiano Testa]

If you try

  convert IsApproxℝ.ofNat 1

instead of apply, you will see what is the issue that Lean is facing. Essentially, you need to provide a proof that one 1 is equal to another 1!

[Markus Schmaus]

That's very useful. This results in two goals, one that 1 = ↑1 and another that ℝ is inhabited. Curiously, for 2 it's only necessary to show that ℝ is inhabited. Why is this only necessary for ℝ, but not for ℚ?

import Mathlib

inductive IsApproxℝ : Float → ℝ → Prop :=
  | ofNat (base : ℕ) {exact : ℝ} : IsApproxℝ (Float.ofNat base) base

example : IsApproxℝ (Float.ofNat 1) 1 := by
  convert IsApproxℝ.ofNat 1
  simp only [Nat.cast_one]
  exact Inhabited.default

example : IsApproxℝ (Float.ofNat 2) 2 := by
  convert IsApproxℝ.ofNat 2
  exact Inhabited.default

[Kevin Buzzard]

Probably because in the case of the rationals the proof is rfl and in the case of the reals it's not. Your apply proof only works assuming that the two 1's are equal by definition, so whether it works in practice all depends on the underlying definitions of things, which is sort of random.