test: proving properties of mutually defined functions

tests/lean/run/mutualDefThms.lean

@@ -0,0 +1,59 @@
+inductive Foo where
+  | text : String → Foo
+  | element : List Foo → Foo
+
+namespace Foo
+
+mutual
+  def textLengthList : List Foo → Nat
+    | [] => 0
+    | f::fs => textLength f + textLengthList fs
+
+  def textLength : Foo → Nat
+    | text s => s.length
+    | element children => textLengthList children
+end
+
+def concat (f₁ f₂ : Foo) : Foo :=
+  Foo.element [f₁, f₂]
+
+theorem textLength_concat (f₁ f₂ : Foo) : textLength (concat f₁ f₂) = textLength f₁ + textLength f₂ := by
+  simp [concat, textLength, textLengthList]
+
+mutual
+  def flatList : List Foo → List String
+    | [] => []
+    | f :: fs => flat f ++ flatList fs
+
+  def flat : Foo → List String
+    | text s => [s]
+    | element children => flatList children
+end
+
+def listStringLen (xs : List String) : Nat :=
+  xs.foldl (init := 0) fun sum s => sum + s.length
+
+theorem foldl_init (s : Nat) (xs : List String) :  (xs.foldl (init := s) fun sum s => sum + s.length) = s + (xs.foldl (init := 0) fun sum s => sum + s.length) := by
+  induction xs generalizing s with
+  | nil => simp [List.foldl]
+  | cons x xs ih => simp [List.foldl, ih x.length, ih (s + x.length)]; simp_arith
+
+theorem listStringLen_append (xs ys : List String) : listStringLen (xs ++ ys) = listStringLen xs + listStringLen ys := by
+  simp [listStringLen]
+  induction xs with
+  | nil => simp [List.foldl]
+  | cons x xs ih => simp [List.foldl, foldl_init x.length, ih]; simp_arith
+
+mutual
+  theorem listStringLen_flat (f : Foo) : listStringLen (flat f) = textLength f := by
+    match f with
+    | text s => simp [flat, textLength, listStringLen, List.foldl]
+    | element cs => simp [textLength, flat, listStringLen_flatList cs]
+
+  theorem listStringLen_flatList (cs : List Foo) : listStringLen (flatList cs) = textLengthList cs := by
+    match cs with
+    | [] => simp
+    | f :: fs => simp [flatList, textLengthList, listStringLen_append, listStringLen_flatList fs, listStringLen_flat f]
+end
+
+end Foo