test: experiment

tests/playground/nnf.lean

@@ -0,0 +1,33 @@
+open Lean
+
+partial def mkBigAnd (n : Nat) (p : Syntax) : MacroM Syntax :=
+  loop 0 n
+where
+  loop (low high : Nat) : MacroM Syntax := do
+    if low == high then
+      `($p[$(quote low)])
+    else
+      let mid := (low + high)/2
+      `($(← loop low mid) ∧ $(← loop (mid + 1) high))
+
+macro "bigAnd! " n:num p:ident : term => mkBigAnd n.toNat p
+
+partial def mkBigOrNot (n : Nat) (p : Syntax) : MacroM Syntax :=
+  loop 0 n
+where
+  loop (low high : Nat) : MacroM Syntax := do
+    if low == high then
+      `(¬ $p[$(quote low)])
+    else
+      let mid := (low + high)/2
+      `($(← loop low mid) ∨ $(← loop (mid + 1) high))
+
+macro "bigOrNot! " n:num p:ident : term => mkBigOrNot n.toNat p
+
+@[simp] axiom not_and (p q : Prop) : (¬ (p ∧ q)) = (¬ p ∨ ¬ q)
+
+theorem ex (p : Array Prop) : (¬ bigAnd! 500 p) = bigOrNot! 500 p := by
+  simp only [not_and]
+  rfl
+
+-- #print ex