feat: expose that panic α = default

[digama0]

For reasoning about code that contains panic!, I think the least bad option (other than removing panic entirely) is to just make it visible to the kernel that panic evaluates to default (which is true if we ignore the side effect of tracing to stderr). This is similar to the dbgTrace function which has a side effect but is not opaque to the kernel and instead has a definition which just shows what happens after the side effect.

[leodemoura]

For reasoning about code that contains panic!,

Could you please provide some use-cases?

[digama0]

For example, a theorem I would like to prove is:

theorem head!_eq_head? [Inhabited α] : ∀ l : List α, head! l = (head? l).get!

but it's not true in the nil case, because the two sides reduce to

panicCore (mkPanicMessageWithDecl "Init.Data.List.BasicAux" "List.head!" 31 12 "empty list") =
panicCore (mkPanicMessageWithDecl "Init.Data.Option.BasicAux" "Option.get!" 16 14 "value is none")

and the two string expressions are not equal even after reduction.

On the other hand,

theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD default

is provable, because the panic in this function is performed in a slightly different way which does not use an opaque.