Fix enum index mismatch for StopReason

Fix the `Condition.Kind` for propositional type classes

Lean/Egg/Core/Gen/GoalTcSpecs.lean

@@ -7,7 +7,7 @@ namespace Egg
 /-
 For goal type specialization, we consider the following shapes of goals and rewrites:
 
-(1) . ~ .       where . is not a proposition
+(1) . = .       where . is not a proposition
 (2) (_ = _) ~ . where . is a proposition (necessarily)
 (3) . ~ (_ = _) where . is a proposition (necessarily)
 

Lean/Egg/Core/Premise/Rewrites.lean

@@ -29,10 +29,11 @@ def Kind.isTcInst : Kind → Bool
   | tcInst => true
 
 def Kind.forType? (ty : Expr) : MetaM (Option Kind) := do
-  if ← Meta.isProp ty then
-    return some .proof
-  else if (← Meta.isClass? ty).isSome then
+  -- Since type classes can also be propositions, we do the type class check first.
+  if (← Meta.isClass? ty).isSome then
     return some .tcInst
+  else if ← Meta.isProp ty then
+    return some .proof
   else
     return none
 

Lean/Egg/Tests/Groups.lean

@@ -23,7 +23,6 @@ macro "group" mod:egg_cfg_mod guides:(egg_guides)? : tactic => `(tactic|
   egg $mod [mul_assoc, one_mul, mul_one, inv_mul_self, mul_inv_self] $[$guides]?
 )
 
-set_option trace.egg true in
 theorem inv_mul_cancel_left : a⁻¹ * (a * b) = b := by group
 
 theorem mul_inv_cancel_left : a * (a⁻¹ * b) = b := by group

Lean/Egg/Tests/Inst Erasure.lean

@@ -5,6 +5,8 @@ info: [egg.encoded] Encoded
   [egg.encoded] Goal
     [egg.encoded] LHS: (app (app (app (app (app (app (const "HAdd.hAdd" 0 0 0) (const "Nat")) (const "Nat")) (const "Nat")) (inst (app (app (app (const "HAdd" 0 0 0) (const "Nat")) (const "Nat")) (const "Nat")))) (fvar 65)) (fvar 65))
     [egg.encoded] RHS: (app (app (app (app (app (app (const "HAdd.hAdd" 0 0 0) (const "Nat")) (const "Nat")) (const "Nat")) (inst (app (app (app (const "HAdd" 0 0 0) (const "Nat")) (const "Nat")) (const "Nat")))) (fvar 65)) (fvar 65))
+  [egg.encoded] Guides
+    [egg.encoded] (= (app (app (app (app (app (app (const "HAdd.hAdd" 0 0 0) (const "Nat")) (const "Nat")) (const "Nat")) (inst (app (app (app (const "HAdd" 0 0 0) (const "Nat")) (const "Nat")) (const "Nat")))) (fvar 65)) (fvar 65)) (app (app (app (app (app (app (const "HAdd.hAdd" 0 0 0) (const "Nat")) (const "Nat")) (const "Nat")) (inst (app (app (app (const "HAdd" 0 0 0) (const "Nat")) (const "Nat")) (const "Nat")))) (fvar 65)) (fvar 65)))
 -/
 #guard_msgs(info) in
 set_option trace.egg.encoded true in

Lean/Egg/Tests/Math/Math/Group.lean

@@ -23,8 +23,8 @@ theorem inv_inv : a⁻¹⁻¹ = a := by
   egg! calc _ = a⁻¹⁻¹ * (a⁻¹ * a)
             _ = _
 
-theorem inv_mul'' : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by
-  egg! using a⁻¹ * (a * b) * (a * b)⁻¹
+theorem inv_mul' : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by
+  egg! using b⁻¹ * a⁻¹ * (a * b) * (a * b)⁻¹
 
 theorem inv_inv' : a⁻¹⁻¹ = a := by
   egg! using a⁻¹ * a

Lean/Egg/Tests/Math/Math/Lie.lean

@@ -1,6 +1,9 @@
 import Mathlib.Algebra.Lie.Basic
 import Egg
 
+set_option egg.timeLimit 10
+set_option egg.genNestedSplits false
+
 universe u v w w₁ w₂
 
 variable {R : Type u} {L : Type v} {M : Type w} {N : Type w₁}
@@ -9,6 +12,11 @@ variable [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M]
 variable [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N]
 variable (t : R) (x y z : L) (m n : M)
 
+variable {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁}
+variable [LieRing L₁] [LieAlgebra R L₁]
+variable [LieRing L₂] [LieAlgebra R L₂]
+variable [LieRing L₃] [LieAlgebra R L₃]
+
 example : ⁅-x, m⁆ = -⁅x, m⁆ := by
   rw [← sub_eq_zero, sub_neg_eq_add, ← add_lie]
   simp only [neg_add_cancel, zero_lie]
@@ -24,10 +32,7 @@ example : ⁅x, m - n⁆ = ⁅x, m⁆ - ⁅x, n⁆ := by
   simp only [sub_eq_add_neg, lie_add, lie_neg]
 
 example : ⁅-x, m⁆ - -⁅x, m⁆ = 0 := by
-  egg [neg_add_cancel, zero_lie, sub_neg_eq_add, add_lie]
-
-set_option egg.timeLimit 10
-set_option egg.genNestedSplits false
+  egg [sub_eq_zero, neg_lie]
 
 example : ⁅-x, m⁆ = -⁅x, m⁆ := by
   egg [neg_add_cancel, zero_lie, sub_eq_zero, sub_neg_eq_add, add_lie]
@@ -40,3 +45,21 @@ example : ⁅x - y, m⁆ = ⁅x, m⁆ - ⁅y, m⁆ := by
 
 example : ⁅x, m - n⁆ = ⁅x, m⁆ - ⁅x, n⁆ := by
   egg [sub_eq_add_neg, lie_add, lie_neg]
+
+-- lie_skew
+example : -⁅y, x⁆ = ⁅x, y⁆ := by
+  egg [neg_eq_iff_add_eq_zero, lie_add, add_lie, lie_self, zero_add, add_zero] using ⁅x + y, x⁆ + ⁅x + y, y⁆
+
+namespace LieHom
+
+-- inverse
+example (f : L₁ →ₗ⁅R⁆ L₂) (g : L₂ → L₁) (h₁ : Function.LeftInverse g f)
+    (h₂ : Function.RightInverse g f) : L₂ →ₗ⁅R⁆ L₁ :=
+  { LinearMap.inverse f.toLinearMap g h₁ h₂ with
+    map_lie' := by
+      intros x y
+      egg calc [h₂ x, h₂ y, map_lie, h₁ _]
+        g ⁅x, y⁆ = g ⁅f (g x), f (g y)⁆
+        _ = g (f ⁅g x, g y⁆)
+        _ = ⁅g x, g y⁆
+  }

Lean/Egg/Tests/Math/Math/PushNeg.lean

@@ -12,6 +12,8 @@ attribute [egg] not_exists
 
 -- TODO: Changing this `=` to a `↔` exposes the problem of instantiating erased equivalences with
 --       `Eq`, instead of distinguishing between `Eq` and `Iff`.
+--       Andrés Idea: During proof reconstruction, if defeq with `Eq` fails, try replacing it with
+--       `Iff`.
 example : ¬¬(p = p) := by
   egg!
 

Lean/Egg/Tests/Math/Math/Rotman.lean

@@ -41,7 +41,9 @@ theorem proposition_1_15 {n r : Nat} (h : n ≥ r) : n.choose r = (n !) / (r ! *
     calc (n + 1).choose r
       _ = (n !) / ((r - 1)! * (n - r + 1)!) + (n !) / (r ! * (n - r)!) := by egg [proposition_1_14, hi, h₁, h₂, h₃]
       _ = _ := Nat.cast_inj.mp <| by
-        egg calc [toReal, fromReal, add_comm, sub_add_cancel, sub_add_eq_add_sub, mul_one, mul_comm, mul_assoc, mul_div_mul_left, _root_.div_mul_div_comm, _root_.add_div, div_mul_eq_div_mul_one_div, left_distrib, Real.Gamma_add_one, h₄, h₅, h₆]
+        egg calc [toReal, fromReal, add_comm, sub_add_cancel, sub_add_eq_add_sub, mul_one, mul_comm,
+                  mul_assoc, mul_div_mul_left, _root_.div_mul_div_comm, _root_.add_div,
+                  div_mul_eq_div_mul_one_div, left_distrib, Real.Gamma_add_one, h₄, h₅, h₆]
           ↑((n !) / ((r - 1)! * (n - r + 1)!) + (n !) / (r ! * (n - r)!))
           _ = (n﹗ / ((r - 1)﹗ * (n - r + 1)﹗) + n﹗ / (r ﹗ * (n - r)﹗))
           _ = n﹗ / ((r - 1)﹗ * (n - r)﹗) * (1 / (n - r + 1) + 1 / r)

Lean/Egg/Tests/Shapes Rerun.lean

@@ -5,18 +5,18 @@ import Egg
 -- shown when setting `exitPoint := some .beforeProof`.
 
 /--
-error: egg failed to build proof step 2: unification failure for LHS of rewrite #0:
+error: egg failed to build proof step 0: unification failure for LHS of rewrite #0:
 
-  HAdd.hAdd
+  Nat.add
 vs
-  ?m.257
+  ?m.240
 in
-  HAdd.hAdd
+  Nat.add
 and
   ()
 
 • Types: ⏎
-  ?m.257: Unit
+  ?m.240: Unit
 
 • Read Only Or Synthetic Opaque MVars: []
 -/

Lean/Egg/Tests/Shapes.lean

@@ -7,6 +7,8 @@ info: [egg.encoded] Encoded
   [egg.encoded] Goal
     [egg.encoded] LHS: (◇ * (const "Bool.true"))
     [egg.encoded] RHS: (◇ * (const "Bool.true"))
+  [egg.encoded] Guides
+    [egg.encoded] (◇ * (= (◇ * (const "Bool.true")) (◇ * (const "Bool.true"))))
 -/
 #guard_msgs in
 set_option trace.egg.encoded true in

Rust/Egg/src/lib.rs

@@ -146,9 +146,9 @@ impl CRewritesArray {
 pub fn u8_from_stop_reason(r: StopReason) -> (u8, String) {
     match r {
         StopReason::Saturated         => (0, "".to_string()),
-        StopReason::IterationLimit(_) => (1, "".to_string()),
-        StopReason::NodeLimit(_)      => (2, "".to_string()),
-        StopReason::TimeLimit(_)      => (3, "".to_string()),
+        StopReason::TimeLimit(_)      => (1, "".to_string()),
+        StopReason::IterationLimit(_) => (2, "".to_string()),
+        StopReason::NodeLimit(_)      => (3, "".to_string()),
         StopReason::Other(msg)        => (4, msg),
     }
 }