Eliminate Option from total function result types

[tothtamas28]

Related

• A shallow embedding of K definitions into Lean 4 #4552 (section Totality)
• Generate function definitions #4727

If a K function symbol production is marked total, the corresponding Lean definition should not have Option as its result type.

The key to this is generating theorem stubs that can be used to show absurdity of certain cases.

For the main def, it should be proved that alt least one of the rules apply. For a rule def, each application of a non-total function induces an obligation to prove definedness.

Motivating example:

def div (x y : Nat) : Option Nat := ...

theorem div_x_2_ne_none (x : Nat) : div x 2 ≠ none := sorry

def halve (x : Nat) : Nat :=
  match h0 : div x 2 with
  | some res => res
  | none => absurd h0 (div_x_2_ne_none x)