underdefined computable definitions

Stream: lean4

[Jakob von Raumer]

Maybe that's a silly question: But is there a good way to write a definition that evaluates to just any value and let's me prove nothing about it? Something like a Classical.choice that evaluates or a completely intransparent Inhabited?

[nrs]

The unsafe keyword might be worth looking at. Just prepend your function definition with it (unsafe def myfunc ...)

[nrs]

It is viral however and anything that calls it will need to be tagged unsafe. The partial keyword is an alternative that is opaque and can be used as a proof that the function's type is inhabited (and nothing else)

[Henrik Böving]

Jakob von Raumer said:

Maybe that's a silly question: But is there a good way to write a definition that evaluates to just any value and let's me prove nothing about it? Something like a Classical.choice that evaluates or a completely intransparent Inhabited?

opaque foo (a : Type) [Inhabited a] : a := default ? Though this will of course still respect refl

[François G. Dorais]

You don't need := default.

[Henrik Böving]

Might be that it gets this by itself yeah, I'm not on a machine

[Jakob von Raumer]

Ah thanks, that's maybe what I'm looking for (except for the respecting refl part)

[Kyle Miller]

One trick here is that you can add multiple arguments to foo, one per variable in your local context for the definition you're making, so that you can have it return different opaque values for different function inputs. Worth thinking about if you want to make sure you can prove even less about it.

[Kyle Miller]

Example:

opaque divZero (a : Nat) : Nat

def safeDiv (a b : Nat) : Nat :=
  if b = 0 then divZero a else a / b

[Kyle Miller]

example : safeDiv 2 0 = safeDiv 3 0 := rfl -- fails

[François G. Dorais]

Be careful though:

example : safeDiv 2 0 = safeDiv 3 0 := by native_decide

The compiler can see through the opaque definition.