Generalising lemma for instances

Stream: mathlib4

[Gareth Ma]

Hi, I have the following proof right now that doesn't work. However, if you replace all the α with ℚ then it works. My idea is that if alpha can be casted to Q then the proof should still work

instance {α : Type*} [OrderedRing α] [Coe α ℚ] : ∀ (z : α) (a : ℕ), Decidable (a ≤ ⌊(z : ℝ)⌋₊) := by
  intro z a
  by_cases hz : 0 ≤ z
  · have : ⌊(z : ℝ)⌋₊ = ⌊(z : ℚ)⌋₊ := by
      zify
      rw [cast_floor_eq_int_floor, cast_floor_eq_int_floor, Rat.floor_cast] <;> norm_cast
      /- Need to prove 0 ≤ Coe.coe z from 0 ≤ z -/
    rw [this]
    apply decLe
  · rw [floor_eq_zero.mpr (by norm_cast ; linarith)]
    /- Need to prove Coe.coe z < 1 from ¬0 ≤ z -/
    apply decLe

What should the correct instances be? For example, this proof should work for Nat and Int because they can be casted to rationals in this natural way

[Gareth Ma]

(The proof is long because I want it to be computable)

[Timo Carlin-Burns]

for #mwe I had to add

import Mathlib

open Nat

[Gareth Ma]

Ah my bad

[Gareth Ma]

After thinking a bit, maybe it's not really possible, since the Coe instance / coercion in general doesn't have any guarantee

[Timo Carlin-Burns]

import Mathlib

open Nat

instance {α : Type*} [Coe α ℚ] : ∀ (z : α) (a : ℕ), Decidable (a ≤ ⌊(z : ℝ)⌋₊) := by
  intro z a
  by_cases hz : 0 ≤ (z : ℚ) -- changed from `0 ≤ z`
  · have : ⌊(z : ℝ)⌋₊ = ⌊(z : ℚ)⌋₊ := by
      zify
      rw [cast_floor_eq_int_floor, cast_floor_eq_int_floor, Rat.floor_cast] <;> norm_cast
    rw [this]
    apply decLe
  · rw [floor_eq_zero.mpr (by norm_cast ; linarith)]
    apply decLe

[Timo Carlin-Burns]

You don't even need an [OrderedRing α] assumption

[Timo Carlin-Burns]

(z : ℝ) in your goal is really (↑(↑z : ℚ) : ℝ), and since you've proven the result for all ℚ, you've also proven it for (↑z : ℚ)

[Gareth Ma]

Hmm I will try it out

[Gareth Ma]

Thanks!

[Gareth Ma]

Oops, just came back. It doesn't work as I wanted (as intended) since it's noncomputable:

import Mathlib

open Nat in
theorem inst1 {α : Type*} [Coe α ℚ] : ∀ (z : α) (a : ℕ), Decidable (a ≤ ⌊(z : ℝ)⌋₊) := by
  intro z a
  by_cases hz : 0 ≤ (z : ℚ) -- changed from `0 ≤ z`
  · have : ⌊(z : ℝ)⌋₊ = ⌊(z : ℚ)⌋₊ := by
      zify
      rw [cast_floor_eq_int_floor, cast_floor_eq_int_floor, Rat.floor_cast] <;> norm_cast
    rw [this]
    apply decLe
  · rw [floor_eq_zero.mpr (by norm_cast ; linarith)]
    apply decLe

instance : Coe ℕ ℚ := ⟨fun a ↦ (a : ℚ)⟩
instance : Coe ℤ ℚ := ⟨fun a ↦ (a : ℚ)⟩

def f {α : Type} [Coe α ℚ] (z : α) (a : ℕ) := a ≤ ⌊(z : ℝ)⌋₊

/- failed to compile definition, consider marking it as 'noncomputable' because it depends on
'inst1', and it does not have executable code -/
instance (z : ℤ) (a : ℕ) : Decidable (f z a) := by
  unfold f
  exact inst1 _ _

/- Both of these are noncomputable now -/
#eval (3 : ℕ) ≤ ⌊((5 : ℤ) : ℝ)⌋₊
#eval f (3 : ℤ) 1

[Gareth Ma]

Unfortunately I don't think it's avoidable, so for now I have just replaced alpha with three different theorems for N Z and Q :)

[Gareth Ma]

Gareth Ma said:

After thinking a bit, maybe it's not really possible, since the Coe instance / coercion in general doesn't have any guarantee

Thinking back to this, what I want is an order-preserving embedding ("mathematically") instead of a type-theoretic Coe, if that makes sense

[Gareth Ma]

In other words, something that can prove $(0 \leq (z : \alpha)) \implies (0 \leq (z : \mathbb{Q}))$

[Brendan Seamas Murphy]

I think you want an order embedding (ie reflecting and preserving) so that you can conclude Coe.coe z < 1 from ¬(0 <= z)

[Gareth Ma]

Yes exactly! Does that exist in Mathlib?

[Brendan Seamas Murphy]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Hom/Basic.html#OrderEmbedding

[Gareth Ma]

Thanks, let me try it

[Eric Wieser]

Why not:

import Mathlib

open Nat

instance {α : Type*} [Coe α ℚ] : ∀ (z : α) (a : ℕ), Decidable (a ≤ ⌊(z : ℝ)⌋₊) := by
  infer_instance

[Gareth Ma]

It immediately says it's noncomputable

[Gareth Ma]

Again the point of the long proof is for it to be computable, otherwise I think something like decLe works immediately

[Eric Wieser]

I recommend first proving

import Mathlib

open Nat

theorem aux {α : Type*} [Coe α ℚ]  (z : α) (a : ℕ) :
  (a ≤ ⌊(z : ℝ)⌋₊) ↔ a ≤ (z : ℚ)

[Eric Wieser]

You almost never want to write a complex decidable instance, just write a lemma that converts the statement into sometime already Decidable and use docs#decidable_of_iff

[Gareth Ma]

I will do that instead :)

[Gareth Ma]

Thanks everyone

[Gareth Ma]

Okay I just isolated the decidability statements into a new file, then copy and paste it a billion times (more like 12) :) It's probably still a better approach then whatever I was attempting above though hahah