From e22d2f6cb1f23ea2e00cd1c7b2d768fa1370469a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 23 Sep 2020 18:18:08 -0700
Subject: [PATCH] test: new tests for structural recursion

@Kha The structural recursion is working :)
It is so much more powerful than the one in Lean3.
I added examples with `let rec`, nested and multiple
`match`-expressions.
I will keep testing and adding missing features tomorrow, and
will hopefully start porting stdlib to new frontend before the end of
the week.
---
 tests/lean/run/structuralRec1.lean | 36 ++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)

diff --git a/tests/lean/run/structuralRec1.lean b/tests/lean/run/structuralRec1.lean
index e1639f7384..743536237d 100644
--- a/tests/lean/run/structuralRec1.lean
+++ b/tests/lean/run/structuralRec1.lean
@@ -18,3 +18,39 @@ rfl
 
 theorem ex5 {α β} (f : α → β) : map f [] = [] :=
 rfl
+
+def map2 {α β} (f : α → β) (as : List α) : List β :=
+let rec loop : List α → List β
+ | []    => []
+ | a::as => f a :: loop as;
+loop as
+
+theorem ex6 {α β} (f : α → β) (a : α) (as : List α) : map2 f (a::as) = (f a) :: map2 f as :=
+rfl
+
+def foo (xs : List Nat) : List Nat :=
+match xs with
+| []    => []
+| x::xs =>
+  let y := 2 * x;
+  match xs with
+  | []    => []
+  | x::xs => (y + x) :: foo xs
+
+#eval foo [1, 2, 3, 4]
+
+theorem fooEq (x y : Nat) (xs : List Nat) : foo (x::y::xs) = (2*x + y) :: foo xs :=
+rfl
+
+def bla (x : Nat) (ys : List Nat) : List Nat :=
+if x % 2 == 0 then
+  match ys with
+  | []    => []
+  | y::ys => (y + x/2) :: bla (x/2) ys
+else
+  match ys with
+  | []    => []
+  | y::ys => (y + x/2 + 1) :: bla (x/2) ys
+
+theorem blaEq (y : Nat) (ys : List Nat) : bla 4 (y::ys) = (y+2) :: bla 2 ys :=
+rfl