test: well-founded recursion example

see #860

tests/lean/run/860.lean

@@ -0,0 +1,37 @@
+def evenq (n: Nat) : Bool := Nat.mod n 2 = 0
+
+theorem Nat.add_sub_self (a b : Nat) : (a + b) - b = a := by
+  induction b with
+  | zero => rfl
+  | succ n ih =>
+    show (a + n).succ - n.succ = a
+    rw [Nat.succ_sub_succ, ih]
+
+private theorem pack_loop_terminates : (n : Nat) → n / 2 < n.succ
+  | 0   => by decide
+  | 1   => by decide
+  | n+2 => by
+    rw [Nat.div_eq]
+    split
+    . rw [Nat.add_sub_self]
+      have := pack_loop_terminates n
+      calc n/2 + 1 < Nat.succ n + 1   := Nat.add_le_add_right this 1
+             _     < Nat.succ (n + 2) := Nat.succ_lt_succ (Nat.succ_lt_succ (Nat.lt_succ_self _))
+    . apply Nat.zero_lt_succ
+
+def pack (n: Nat) : List Nat :=
+  let rec loop (n : Nat) (acc : Nat) (accs: List Nat) : List Nat :=
+    let next (n: Nat) := n / 2;
+    match n with
+    | Nat.zero => List.cons acc accs
+    | n+1 => match evenq n with
+      | true => loop (next n) 0 (List.cons acc accs)
+      | false => loop (next n) (acc+1) accs
+  loop n 0 []
+termination_by
+  invImage (fun ⟨n, _, _⟩ => n) Nat.lt_wfRel
+decreasing_by
+  simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel]
+  apply pack_loop_terminates
+
+#eval pack 27