assert! in recursive functions

Stream: lean4

[Joachim Breitner]

TIL that assert!, when used in a recursive function, can help lean find a termination argument, e.g. in

def allSplits (s : Nat) (P : Nat → Nat → Bool) : Bool :=
  (List.range (s+1)).all fun s' => P s' (s-s')

def allPartitions (s: Nat) (P : List Nat → Bool) :=
  match s with
  | 0 =>
    P []
  | s+1 =>
    allSplits s fun s1 s2 =>
      assert! s1 + s2 = s
      allPartitions s1 fun xs =>
        allPartitions s2 fun ys =>
          P (xs ++ ys)

This makes sense when one thinks about it (and may actually be genuinely useful and still allow verification later), but I did not expect it.

[Joachim Breitner]

This can sometimes probably even work as a more convenient alternative to adding subtypes to the result just for termination checking (for non-empty result types, else you can't assert! easily), that defers discharging these conditions until after the function is defined.

[François G. Dorais]

How about a realize_assertions tactic to make the behavior explicit and extendible?

[Joachim Breitner]

Sorry, I don't quite follow, can you elaborate?

[Mario Carneiro]

it would be great if there was a assert! h : cond form