Is there a computable way to get a Rat out of AddCircle?

Stream: Is there code for X?

[suhr]

I need a function that extracts a value of type Rat (in the range of [0; 1)) from a value of type AddCircle (1 : Rat). I tried to do the following:

abbrev PClass := AddCircle (1 : Rat)
def PClass.rat (x: AddCircle (1 : Rat)): Rat := (AddCircle.liftIco 1 0 id) x

But I get the following error:

failed to compile definition, compiler IR check failed at `rat`. Error: depends on declaration 'AddCircle.liftIco', which has no executable code; consider marking definition as 'noncomputable'

Is there a computable way to get a value out of AddCircle (1 : Rat)?

[Aaron Liu]

noncomputability is coming from docs#toIcoDiv where it extracts a kind of "floor" from the Archimedean hypothesis using choice

[Yury G. Kudryashov]

You can define your own function, then prove that it's equal to the noncomputable version.

[Yury G. Kudryashov]

Let me write a definition.

[Yury G. Kudryashov]

import Mathlib

variable {R : Type*} [Ring R] [LinearOrder R] [FloorRing R] [IsStrictOrderedRing R]

protected def AddCircle.fract (x : AddCircle (1 : R)) : R :=
  Quotient.liftOn' x Int.fract fun a b ↦ by
    rw [QuotientAddGroup.leftRel_apply, AddSubgroup.mem_zmultiples_iff]
    rintro ⟨k, hk⟩
    obtain rfl : b = a + k := by linear_combination (norm := {simp; abel}) -hk
    rw [Int.fract_add_intCast]

@[simp]
theorem AddCircle.fract_coe (x : R) : AddCircle.fract x = Int.fract x := rfl

theorem AddCircle.fract_eq_liftIco [Archimedean R] (x : AddCircle (1 : R)) : x.fract = liftIco (1 : R) 0 id x := by
  rcases QuotientAddGroup.mk_surjective x with ⟨x, rfl⟩
  symm
  suffices ∃ z : ℤ, x = Int.fract x + z by
    simpa [liftIco, equivIco, toIcoMod_eq_iff, Int.fract_lt_one]
  use ⌊x⌋
  simp