Add freshman's dream to test cases

Lean/Egg/Tests/Freshman.lean

@@ -0,0 +1,61 @@
+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_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
+
+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_one, pow_two, pow_three, char_two] $[$base]? $[$guides]?
+)
+
+variable [CharTwoRing α]
+
+theorem freshmans_dream (x y : α) : (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
+  char_two_ring
+
+theorem freshmans_dream₃ (x y : α) : (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)       := by char_two_ring
+   _ = (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 : α) : (x + y) ^ 3 = x ^ 3 + x * y ^ 2 + x ^ 2 * y + y ^ 3 := by
+  char_two_ring

Lean/Egg/Tests/Groups.lean

@@ -1,25 +1,18 @@
 import Egg
-import Lean
 
-class Group (α) where
-  zero          : α
-  neg           : α → α
-  add           : α → α → α
-  add_assoc     : ∀ a b c, add (add a b) c = add a (add b c)
-  zero_add      : ∀ a, add zero a = a
-  add_zero      : ∀ a, add a zero = a
-  add_left_neg  : ∀ a, add (neg a) a = zero
-  add_right_neg : ∀ a, add a (neg a) = zero
+class Zero (α) where zero : α
+instance [Zero α] : OfNat α 0 where ofNat := Zero.zero
 
-open Group
-
-instance [Group α] : Neg α where neg := neg
-instance [Group α] : Add α where add := add
-instance [Group α] : OfNat α 0 where ofNat := zero
+class Group (α) extends Zero α, Neg α, Add α where
+  add_assoc     (a b c : α) : (a + b) + c = a + (b + c)
+  zero_add      (a : α)     : 0 + a = a
+  add_zero      (a : α)     : a + 0 = a
+  add_left_neg  (a : α)     : -a + a = 0
+  add_right_neg (a : α)     : a + -a = 0
 
 variable [Group G] {a b : G}
 
-open Egg.Guides Egg.Config.Modifier in
+open Group Egg.Guides Egg.Config.Modifier in
 macro "group" mod:egg_cfg_mod base:(egg_base)? guides:(egg_guides)? : tactic => `(tactic|
   egg $mod [add_assoc, zero_add, add_zero, add_left_neg, add_right_neg] $[$base]? $[$guides]?
 )