Option.get!

Stream: lean4

[Horatiu Cheval]

Is it possible to prove the following statement?

example {α : Type _} [Inhabited α] : (none.get! : α) = Inhabited.default := by sorry

I tried all sorts of versions of simp but I didn't succeed. Or is it the case that panic! (which appears in the definition of Option.get!) should only be used for programming and not theorem proving, and that if I want to prove theorems I should use something like

def Option.get!! {α : Type _} [Inhabited α] : Option α → α
| some x => x
| none => Inhabited.default

instead?

[Henrik Böving]

If you want to prove for example this:

example : (panic! "Hello") = (0 : Nat)

you can get two levels deep into the panic implementation:

example : (panic! "Hello") = (0 : Nat) := by
  simp only [panicWithPosWithDecl]
  simp only [panic]

however panicCore (which will show up in the proof goal at this point) is declared as a constant in Prelude.lean:

@[neverExtract, extern "lean_panic_fn"]
constant panicCore {α : Type u} [Inhabited α] (msg : String) : α

and constants can not be unwrapped by design since they are opaque. So yes you can in fact not prove anything about the return value of panic!, merely that it will return something of the desired type.

I'd say if you really need something that returns Inhabited.default in case of a none you could use Option.getD Inhabited.default

[Marc Huisinga]

panic! ultimately refers to panicCore in Init/Prelude.lean, which is a constant and hence cannot be unfolded, so it shouldn't be possible to prove anything about it. Ideally, in proofs, you ensure that the panic! case never occurs via preconditions (it shouldn't occur at runtime either after all!).

[Horatiu Cheval]

I see, thank you both. It makes sense, in my case, the none case can definitely happen so I will go with the getD version.

[Marcus Rossel]

Do you know why panic! is a "proper" function instead of a partial def?
I find it kind of counterintuitive that an "error out at runtime" construct can be used within the mathematically sound part of Lean.
Is it so that we can write functions that use things like get! without having to show that it is safe within the function definition (but still can prove later that it's actually safe, by proving that the panic case can never occur)?

[Marc Huisinga]

Marcus Rossel said:

Do you know why panic! is a "proper" function instead of a partial def?
I find it kind of counterintuitive that an "error out at runtime" construct can be used within the mathematically sound part of Lean.
Is it so that we can write functions that use things like get! without having to show that it is safe within the function definition (but still can prove later that it's actually safe, by proving that the panic case can never occur)?

It's not a proper function, it's a constant. Partial functions are also just unsafe functions hidden behind a constant. (cf https://leanprover.github.io/lean4/doc/lean3changes.html#the-meta-keyword)

[Horatiu Cheval]

I was under the impression that a partial def still doesn't compromise soundness, because it requires the target type to be inhabited, is that right?