test: perf experiments

tests/playground/seq1.lean

@@ -0,0 +1,31 @@
+abbrev M := ExceptT String $ StateT Nat Id
+
+/- The following instances are not needed, but they speedup the proof -/
+instance : Monad M := inferInstance
+instance : LawfulMonad M := inferInstance
+instance : MonadStateOf Nat M := inferInstance
+instance : Bind M := inferInstance
+instance : Pure M := inferInstance
+
+syntax "bigAdd0Seq! " num : term
+
+macro_rules
+  | `(bigAdd0Seq! $n) =>
+    let n := n.toNat
+    if n == 0 then
+      `(pure ())
+    else
+      `(get >>= fun n => set (0 + n) >>= fun _ => bigAdd0Seq! $(Lean.quote (n - 1)))
+
+@[simp] theorem get_set  : (get >>= fun n => set n) = (pure () : M Unit) :=
+  rfl
+
+set_option maxRecDepth   1000000
+set_option maxHeartbeats 1000000
+
+theorem ex : (bigAdd0Seq! 40 : M Unit) = pure () := by
+  simp
+
+-- set_option pp.explicit true
+-- set_option pp.notation false
+-- #print ex

tests/playground/seq2.lean

@@ -0,0 +1,26 @@
+abbrev M := ExceptT String $ StateT Nat Id
+
+def add (n : Nat) : M Unit :=
+  modify (· + 0)
+
+@[simp] theorem addZero : add (natLit! 0) = pure () :=
+  rfl
+
+syntax "bigAdd0Seq! " num : term
+
+macro_rules
+  | `(bigAdd0Seq! $n) =>
+    let n := n.toNat
+    if n == 0 then
+      `(pure ())
+    else
+      `(add (natLit! 0) >>= fun _ => bigAdd0Seq! $(Lean.quote (n - 1)))
+
+set_option maxRecDepth 10000
+
+theorem ex : bigAdd0Seq! 10 = pure () := by
+  simp
+
+-- set_option pp.explicit true
+-- set_option pp.notation false
+-- #print ex