From 3b1178e9bc4a8c7517255beea4d8cd151f1191c5 Mon Sep 17 00:00:00 2001
From: Marcus Rossel <marcusrossel@icloud.com>
Date: Tue, 16 Apr 2024 11:36:31 +0200
Subject: [PATCH] Add a version of freshman's dream with a sensible def of pow

---
 Lean/Egg/Tests/Freshman Pow.lean | 59 ++++++++++++++++++++++++++++++++
 Lean/Egg/Tests/Freshman.lean     | 11 +++---
 2 files changed, 64 insertions(+), 6 deletions(-)
 create mode 100644 Lean/Egg/Tests/Freshman Pow.lean

diff --git a/Lean/Egg/Tests/Freshman Pow.lean b/Lean/Egg/Tests/Freshman Pow.lean
new file mode 100644
index 0000000..e43f581
--- /dev/null
+++ b/Lean/Egg/Tests/Freshman Pow.lean	
@@ -0,0 +1,59 @@
+import Egg
+
+class Inv (α) where inv : α → α
+postfix:max "⁻¹" => Inv.inv
+
+class Zero (α) where zero : α
+instance [Zero α] : OfNat α 0 where ofNat := Zero.zero
+
+class One (α) where one : α
+instance [One α] : OfNat α 1 where ofNat := One.one
+
+class Ring (α) extends Zero α, One α, Add α, Sub α, Mul α, Div α, Pow α Nat, Inv α, Neg α where
+  comm_add  (a b : α)   : a + b = b + a
+  comm_mul  (a b : α)   : a * b = b * a
+  add_assoc (a b c : α) : a + (b + c) = (a + b) + c
+  mul_assoc (a b c : α) : a * (b * c) = (a * b) * c
+  sub_canon (a b : α)   : a - b = a + -b
+  neg_add   (a : α)     : a + -a = 0
+  div_canon (a b : α)   : a / b = a * b⁻¹
+  zero_add  (a : α)     : a + 0 = a
+  zero_mul  (a : α)     : a * 0 = 0
+  one_mul   (a : α)     : a * 1 = a
+  distrib   (a b c : α) : a * (b + c)  = (a * b) + (a * c)
+  pow_zero  (a : α)     : a ^ 0 = 1
+  pow_succ  (a : α)     : a ^ (n + 1) = a * (a ^ n)
+
+class CharTwoRing (α) extends Ring α where
+  char_two (a : α) : a + a = 0
+
+open Ring CharTwoRing Egg.Guides Egg.Config.Modifier in
+macro "char_two_ring" mod:egg_cfg_mod base:(egg_base)? guides:(egg_guides)? : tactic => `(tactic|
+  egg $mod [comm_add, comm_mul, add_assoc, mul_assoc, sub_canon, neg_add, div_canon, zero_add,
+  zero_mul, one_mul, distrib, pow_zero, pow_succ, char_two, Nat.succ_eq_add_one] $[$base]? $[$guides]?
+)
+
+variable [CharTwoRing α] (x y : α)
+
+theorem freshmans_dream₂ : (x + y) ^ 2 = x ^ 2 + y ^ 2 := by
+   calc (x + y) ^ 2
+    _ = (x + y) * (x + y)             := by char_two_ring
+    _ = x * (x + y) + y * (x + y)     := by char_two_ring
+    -- _ = x ^ 2 + x * y + y * x + y ^ 2
+    _ = x ^ 2 + y ^ 2                 := by char_two_ring
+
+theorem freshmans_dream₂': (x + y) ^ 2 = x ^ 2 + y ^ 2 := by
+  char_two_ring
+
+theorem freshmans_dream₃ : (x + y) ^ 3 = x ^ 3 + x * y ^ 2 + x ^ 2 * y + y ^ 3 := by
+  calc (x + y) ^ 3
+   _ = (x + y) * (x + y) * (x + y)                     := by char_two_ring
+   _ = (x + y) * (x * (x + y) + y * (x + y))           := by char_two_ring
+   -- _ = (x + y) * (x ^ 2 + x * y + y * x + y ^ 2)
+   _ = (x + y) * (x ^ 2 + y ^ 2)                       := by char_two_ring
+   _ = x * (x ^ 2 + y ^ 2) + y * (x ^ 2 + y ^ 2)       := by char_two_ring
+   _ = (x * x ^ 2) + x * y ^ 2 + y * x ^ 2 + y * y ^ 2 := by char_two_ring
+   _ = x ^ 3 + x * y ^ 2 + x ^ 2 * y + y ^ 3           := by char_two_ring
+
+theorem freshmans_dream₃' : (x + y) ^ 3 = x ^ 3 + x * y ^ 2 + x ^ 2 * y + y ^ 3 := by
+  char_two_ring using (x + y) * (x + y)
diff --git a/Lean/Egg/Tests/Freshman.lean b/Lean/Egg/Tests/Freshman.lean
index 82e860a..1acdd80 100644
--- a/Lean/Egg/Tests/Freshman.lean
+++ b/Lean/Egg/Tests/Freshman.lean
@@ -25,7 +25,6 @@ class Ring (α) extends Zero α, One α, Add α, Sub α, Mul α, Div α, Pow α
   pow_one   (a : α)     : a ^ 1 = a
   pow_two   (a : α)     : a ^ 2 = (a ^ 1) * a
   pow_three (a : α)     : a ^ 3 = (a ^ 2) * a
-  -- TODO: Changing the axioms for `^` to be recursive breaks some of the proofs.
 
 class CharTwoRing (α) extends Ring α where
   char_two (a : α) : a + a = 0
@@ -36,19 +35,19 @@ macro "char_two_ring" mod:egg_cfg_mod base:(egg_base)? guides:(egg_guides)? : ta
   zero_mul, one_mul, distrib, pow_zero, pow_one, pow_two, pow_three, char_two] $[$base]? $[$guides]?
 )
 
-variable [CharTwoRing α]
+variable [CharTwoRing α] (x y : α)
 
-theorem freshmans_dream (x y : α) : (x + y) ^ 2 = (x ^ 2) + (y ^ 2) := by
+theorem freshmans_dream : (x + y) ^ 2 = (x ^ 2) + (y ^ 2) := by
   calc (x + y) ^ 2
    _ = (x + y) * (x + y)             := by char_two_ring
    _ = x * (x + y) + y * (x + y)     := by char_two_ring
    _ = x ^ 2 + x * y + y * x + y ^ 2 := by char_two_ring
    _ = x ^ 2 + y ^ 2                 := by char_two_ring
 
-theorem freshmans_dream' (x y : α) : (x + y) ^ 2 = (x ^ 2) + (y ^ 2) := by
+theorem freshmans_dream' : (x + y) ^ 2 = (x ^ 2) + (y ^ 2) := by
   char_two_ring
 
-theorem freshmans_dream₃ (x y : α) : (x + y) ^ 3 = x ^ 3 + x * y ^ 2 + x ^ 2 * y + y ^ 3 := by
+theorem freshmans_dream₃ : (x + y) ^ 3 = x ^ 3 + x * y ^ 2 + x ^ 2 * y + y ^ 3 := by
   calc (x + y) ^ 3
    _ = (x + y) * (x + y) * (x + y)                     := by char_two_ring
    _ = (x + y) * (x * (x + y) + y * (x + y))           := by char_two_ring
@@ -58,5 +57,5 @@ theorem freshmans_dream₃ (x y : α) : (x + y) ^ 3 = x ^ 3 + x * y ^ 2 + x ^ 2
    _ = (x * x ^ 2) + x * y ^ 2 + y * x ^ 2 + y * y ^ 2 := by char_two_ring
    _ = x ^ 3 + x * y ^ 2 + x ^ 2 * y + y ^ 3           := by char_two_ring
 
-theorem freshmans_dream₃' (x y : α) : (x + y) ^ 3 = x ^ 3 + x * y ^ 2 + x ^ 2 * y + y ^ 3 := by
+theorem freshmans_dream₃' : (x + y) ^ 3 = x ^ 3 + x * y ^ 2 + x ^ 2 * y + y ^ 3 := by
   char_two_ring