Structure with noncomputable rec/accessor?

Stream: lean4

[James Gallicchio]

Is there a way to mark a structure's rec/accessor functions noncomputable after the declaration? I'm doing some FFI stuff, I would like them to be available for reasoning, but noncomputable. My first instinct was to use the attribute command but noncomputable isn't actually an attribute.

[James Gallicchio]

Ended up just making an opaque NonemptyType and introducing the axioms I needed, but I'm still curious if this solution is possible!

[Gabriel Ebner]

Can you post a concrete example of what you're trying to do?

[cognivore]

:eyes:

[James Gallicchio]

Sure -- the reason for the noncomputability is to do with this Uninit type @Mario Carneiro worked out, which is defined as follows:

opaque UninitPointed.{u} (α : Type u) : NonemptyType.{u}
def Uninit.{u} (α : Type u) : Type u := (UninitPointed α).type

namespace Uninit

instance : Nonempty (Uninit α) := (UninitPointed α).property

noncomputable opaque uninit {α} : Uninit α

unsafe def initUnsafe (a : α) : Uninit α := unsafeCast a
@[implementedBy initUnsafe]
opaque init (a : α) : Uninit α

...

def getValueExists (x : Uninit α) (h : ∃ a, x = .init a) : α := ...

So given a value x : Uninit α it is undecidable whether it is init or uninit. But given a proof that ∃ a, x = Uninit.init a the value can be synthesized.

[James Gallicchio]

All that said, an uninitialized value of type Uninit α violates the Lean ABI (in particular, something might call lean_inc or lean_dec on it, which could segfault). So, Uninit α values can only exist if they are contained by some external object that properly handles them

[James Gallicchio]

That's okay for me -- I wanted to use Uninit α to implement arrays that can be partially uninitialized. The uninit values are never actually exposed to the Lean runtime, but are used to define the interface. So I wanted to have something like this:

structure ArrayUninit.{u} (α : Type u) (n : Nat) where
  data : Fin n → Uninit α

But, of course, this is potentially unsafe if data is computable, since then we could actually expose uninitialized values to the runtime.

[James Gallicchio]

So since I couldn't figure out how to do that, instead I wrote a new opaque type that is isomorphic to Fin n → Uninit α. I had to then manually axiomatize the reasoning principles for it, which are equivalent to what would be auto-generated by the structure, modulo rec being noncomputable.