noncomputable checker is too pesimistic

Stream: lean4

[Tomas Skrivan]

I would like to write code like this:

def foo {K} [IsROrC K] (x : K) := (∂ x':=x, (x'*x' + x')) rewrite_by symdiff

where (∂ x':=x, (x'*x' + x')) differentiates the expression w.r.t. to x' and evaluates it in x. The x:term rewrite_by c:conv rewrites x with tactic c. The above definition simplifies to def foo {K} [IsROrC K] (x : K) := 1 + x * 2, but I really want to write it down in the original form.

Afterwards I really want to evaluate foo on floats. My idea is to create fake instance IsROrC Float and call foo (1.0 : Float). Unfortunately, this does not work as the instance IsROrC Float has to be marked noncomputable because it uses reals. My hope that it would work because foo is not using any of the noncomputable parts of IsROrC.

Here is mwe demonstrating the problem where Foo simulates the class IsROrC

class Foo (α : Type _) extends Add α where
  norm : α → Nat

noncomputable
instance instFooNat : Foo Nat where
  norm := fun a => Classical.arbitrary Nat

def foo [Foo α] (x y : α) := x + y  -- here I require `Foo` as it might be required for some rewrites

#eval foo 1 2 -- fails as it depends on noncomputable `instFooNat` however `foo` is not using the noncomputable `Foo.norm`

Any ideas how to deal/sidestep this?

[Eric Wieser]

Use unsafe instead of noncomputable

[Eric Wieser]

Can you make a slightly less minimal example that uses Real but not IsROrC?

[Eric Wieser]

If your problem really is the norm, I would expect the following to be computable:

def norm (f : Float) : ℝ := (f.abs.toRat : ℝ)

(assuming we have Float.abs and Float.toRat)

[Tomas Skrivan]

The norm is not the issue, I will try to create a different mwe

[Tomas Skrivan]

I started dissecting IsROrC and the problem disappeared ... and I don't have to mark the instance isROrC Float as noncomputable anymore. I will have to investigate more what is going on.

[Mac Malone]

@Tomas Skrivan Note that you can get your original example to work by marking the instance macro_inline:

class Foo (α : Type _) extends Add α where
  norm : α → Nat

@[macro_inline] noncomputable
instance instFooNat : Foo Nat where
  norm := fun a => Classical.arbitrary Nat

def foo [Foo α] (x y : α) := x + y

#eval foo 1 2 -- 3

[Mac Malone]

This will result in the structure being unpacked before the noncomputable checker kicks in.

[Tomas Skrivan]

Cool, I haven't thought of using that. I managed to solve the issue differently but I will keep this in mind for the future.