From 9b9dd4d4ec0d29e4ab883d76990309aeffc2ca29 Mon Sep 17 00:00:00 2001
From: Siddhartha Gadgil <siddhartha.gadgil@gmail.com>
Date: Mon, 9 Sep 2024 09:02:58 +0530
Subject: [PATCH] negation code (before video)

---
 MetaExamples/Negate.lean | 35 +++++++++++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)
 create mode 100644 MetaExamples/Negate.lean

diff --git a/MetaExamples/Negate.lean b/MetaExamples/Negate.lean
new file mode 100644
index 0000000..7ab565b
--- /dev/null
+++ b/MetaExamples/Negate.lean
@@ -0,0 +1,35 @@
+import Lean
+import MetaExamples.Basic
+open Lean Meta Elab Term
+
+partial def negate (e: Expr) : MetaM Expr := do
+  match e with
+  | .forallE name domain body bi => do
+    if ← isProp domain then
+      let negBody ← negate body
+      mkAppM ``And #[domain, negBody]
+    else
+    let negFn ←
+      withLocalDecl name bi domain fun x => do
+        let negBody ← negate (body.instantiate1 x)
+        mkLambdaFVars #[x] negBody
+    mkAppM ``Exists #[negFn]
+  | _ =>
+    match e.app2? ``Exists with
+    | some (_, .lam name domain body bi) => do
+      withLocalDecl name bi domain fun x => do
+        let negBody ← negate (body.instantiate1 x)
+        mkForallFVars #[x] negBody
+    | _ => mkAppM ``Not #[e]
+
+elab "negate#" t:term : term => do
+  let p ← elabType t
+  negate p
+
+#check negate# (∀n: Nat, n > 0 →  n ≠ n + 1)
+#check negate# (∃n: Nat, 2 * n > n + 1)
+#check fun (f: Nat → Nat) => negate# (∀ k : Nat, ∃ n: Nat, ∀ m: Nat, m > n → f m > k)
+
+#check Not
+
+#expr [∃ n:Nat, 2 * n > n + 1]