test: expand f91 test

Author: nomeata

tests/lean/run/partial_fixpoint_f91.lean

@@ -4,6 +4,31 @@ def f91 (n : Nat) : Option Nat :=
     else f91 (n + 11) >>= f91
 partial_fixpoint
 
+section partial_correctness
+
+-- #check f91.partial_correctness
+
+theorem f91_partial_spec (n r : Nat) :
+    f91 n = some r → r = if n > 100 then n - 10 else 91 := by
+  apply f91.partial_correctness
+  intro f91 ih n r h
+  split at *
+  · simp_all
+  · simp only [Option.bind_eq_bind, Option.bind_eq_some] at h
+    obtain ⟨r', hr1, hr2⟩ := h
+    replace hr1 := ih _ _ hr1
+    replace hr2 := ih _ _ hr2
+    clear ih
+    subst hr1
+    subst hr2
+    split
+    · simp; omega
+    · simp
+
+end partial_correctness
+
+section total_correctness
+
 theorem f91_spec_high (n : Nat) (h : 100 < n) : f91 n =  some (n - 10) := by
   unfold f91; simp [*]
 
@@ -21,7 +46,10 @@ theorem f91_spec_low (n : Nat) (h₂ : n ≤ 100) : f91 n = some 91 := by
     · simp [*, f91]
     · exact f91_spec_low (n + 1) (by omega)
 
-theorem f91_spec (n : Nat) : f91 n =  some (if n ≤ 100 then 91 else n - 10) := by
+theorem f91_spec (n : Nat) :
+    f91 n = some (if n ≤ 100 then 91 else n - 10) := by
   by_cases h100 : n ≤ 100
   · simp [f91_spec_low, *]
   · simp [f91_spec_high, Nat.lt_of_not_le ‹_›, *]
+
+end total_correctness