Is it possible to see through opaque?

Stream: lean4

[Geoffrey Irving]

docs#BaseIO.asTask has a simple definition, but is marked opaque, so this proof doesn't work:

import Mathlib

variable {α : Type}

lemma BaseIO.askTask_def (x : BaseIO α) (prio : Task.Priority) :
    BaseIO.asTask prio x = Task.pure <$> x := by
  rfl  -- Does not work, since BaseIO.asTask is opaque

Is there a way to make this proof work, or is opaque indeed impossible to see through (by design)?

[Geoffrey Irving]

Hmm, this documentation makes me guess it's impossible: https://leanprover-community.github.io/mathlib4_docs/Init/Tactics.html#Lean.Parser.Tactic.withUnfoldingAll

[Jon Eugster]

But this simple definition is only a placeholder for typechecking and asTask is implemented by the specified C-function, so when run, these two objects in BaseIO Task give you different Tasks back.

So I'd somehow hope that you wouldn't be able to prove such an equality.

Can I ask you why you'd want to do that?

[Geoffrey Irving]

I want to prove that the pure content of IO.asTask has certain properties, similar to how I’m allowed to prove that Task.spawn has properties even though it is also implemented in C.

[Geoffrey Irving]

Ah, I can dodge this, so I'm not blocked: if I write my own version of BaseIO.asTask that threads the property though via dependent types, I can prove what I need.