Rename defeq options

Lean/Egg/Core/Config.lean

@@ -25,13 +25,16 @@ structure Gen where
   genTcProjRws  := true
   genTcSpecRws  := true
   genGoalTcSpec := true
-  genNatLitRws  := true
-  genEtaRw      := true
-  genBetaRw     := true
-  genLevelRws   := true
   explosion     := false
   deriving BEq
 
+structure DefEq where
+  natLit    := true
+  eta       := true
+  etaExpand := false
+  beta      := true
+  levels    := true
+
 structure Backend where
   blockInvalidMatches := true
   shiftCapturedBVars  := true -- This option implies `blockInvalidMatches`.
@@ -58,7 +61,7 @@ structure Debug where
   vizPath   := (none : Option String)
   deriving BEq
 
-structure _root_.Egg.Config extends Encoding, Gen, Backend, Debug where
+structure _root_.Egg.Config extends Encoding, DefEq, Gen, Backend, Debug where
   retryWithShapes := true
   explLengthLimit := 1000
 
@@ -70,5 +73,5 @@ instance : Coe Encoding Normalization where
 instance : Coe Config Encoding where
   coe := toEncoding
 
-instance : Coe Config Gen where
-  coe := toGen
+instance : Coe Config DefEq where
+  coe := toDefEq

Lean/Egg/Core/Request/Basic.lean

@@ -15,10 +15,10 @@ protected structure Config where
   timeLimit            : Nat
   nodeLimit            : Nat
   iterLimit            : Nat
-  genNatLitRws         : Bool
-  genEtaRw             : Bool
-  genBetaRw            : Bool
-  genLevelRws          : Bool
+  natLit         : Bool
+  eta             : Bool
+  beta            : Bool
+  levels          : Bool
   shapes               : Bool
   blockInvalidMatches  : Bool
   shiftCapturedBVars   : Bool
@@ -32,10 +32,10 @@ instance : Coe Config Request.Config where
     timeLimit            := cfg.timeLimit
     nodeLimit            := cfg.nodeLimit
     iterLimit            := cfg.iterLimit
-    genNatLitRws         := cfg.genNatLitRws
-    genEtaRw             := cfg.genEtaRw
-    genBetaRw            := cfg.genBetaRw
-    genLevelRws          := cfg.genLevelRws
+    natLit         := cfg.natLit
+    eta             := cfg.eta
+    beta            := cfg.beta
+    levels          := cfg.levels
     shapes               := cfg.shapes
     blockInvalidMatches  := cfg.blockInvalidMatches
     shiftCapturedBVars   := cfg.shiftCapturedBVars

Lean/Egg/Tactic/Config/Modifier.lean

@@ -16,10 +16,10 @@ structure Modifier where
   genTcProjRws        : Option Bool            := none
   genTcSpecRws        : Option Bool            := none
   genGoalTcSpec       : Option Bool            := none
-  genNatLitRws        : Option Bool            := none
-  genEtaRw            : Option Bool            := none
-  genBetaRw           : Option Bool            := none
-  genLevelRws         : Option Bool            := none
+  natLit              : Option Bool            := none
+  eta                 : Option Bool            := none
+  beta                : Option Bool            := none
+  levels              : Option Bool            := none
   explosion           : Option Bool            := none
   blockInvalidMatches : Option Bool            := none
   shiftCapturedBVars  : Option Bool            := none
@@ -47,10 +47,10 @@ def modify (cfg : Config) (mod : Modifier) : Config where
   genTcProjRws        := mod.genTcProjRws.getD cfg.genTcProjRws
   genTcSpecRws        := mod.genTcSpecRws.getD cfg.genTcSpecRws
   genGoalTcSpec       := mod.genGoalTcSpec.getD cfg.genGoalTcSpec
-  genNatLitRws        := mod.genNatLitRws.getD cfg.genNatLitRws
-  genEtaRw            := mod.genEtaRw.getD cfg.genEtaRw
-  genBetaRw           := mod.genBetaRw.getD cfg.genBetaRw
-  genLevelRws         := mod.genLevelRws.getD cfg.genLevelRws
+  natLit              := mod.natLit.getD cfg.natLit
+  eta                 := mod.eta.getD cfg.eta
+  beta                := mod.beta.getD cfg.beta
+  levels              := mod.levels.getD cfg.levels
   explosion           := mod.explosion.getD cfg.explosion
   blockInvalidMatches := mod.blockInvalidMatches.getD cfg.blockInvalidMatches
   shiftCapturedBVars  := mod.shiftCapturedBVars.getD cfg.shiftCapturedBVars

Lean/Egg/Tactic/Config/Option.lean

@@ -49,10 +49,10 @@ register_egg_options
   genTcProjRws
   genTcSpecRws
   genGoalTcSpec
-  genNatLitRws
-  genEtaRw
-  genBetaRw
-  genLevelRws
+  natLit
+  eta
+  beta
+  levels
   explosion
   blockInvalidMatches
   shiftCapturedBVars "Note: Setting this to `true` also enables `egg.blockInvalidMatches`."

Lean/Egg/Tactic/Premises/Gen.lean

@@ -17,7 +17,7 @@ namespace Egg.Premises
 
 private def tracePremises
     (basic : WithSyntax Rewrites) (tagged builtins tc ex pruned : Rewrites)
-    (facts : WithSyntax Facts) (cfg : Config.Gen) : TacticM Unit := do
+    (facts : WithSyntax Facts) (cfg : Config.DefEq) : TacticM Unit := do
   let cls := `egg.rewrites
   withTraceNode cls (fun _ => return "Rewrites") do
     withTraceNode cls (fun _ => return m!"Basic ({basic.elems.size})") do basic.elems.trace basic.stxs cls
@@ -28,9 +28,9 @@ private def tracePremises
     withTraceNode cls (fun _ => return m!"Hypotheses ({facts.elems.size})") do
       facts.elems.trace facts.stxs cls
     withTraceNode cls (fun _ => return "Definitional") do
-      if cfg.genBetaRw    then Lean.trace cls fun _ => "β-Reduction"
-      if cfg.genEtaRw     then Lean.trace cls fun _ => "η-Reduction"
-      if cfg.genNatLitRws then Lean.trace cls fun _ => "Natural Number Literals"
+      if cfg.beta    then Lean.trace cls fun _ => "β-Reduction"
+      if cfg.eta     then Lean.trace cls fun _ => "η-Reduction"
+      if cfg.natLit then Lean.trace cls fun _ => "Natural Number Literals"
     withTraceNode cls (fun _ => return m!"Pruned ({pruned.size})") do pruned.trace #[] cls
 
 partial def gen

Lean/Egg/Tactic/Trace.lean

@@ -115,9 +115,9 @@ nonrec def Config.trace (cfg : Config) (cls : Name) : TacticM Unit := do
   withTraceNode cls (fun _ => return "Configuration") do
     trace cls fun _ => m!"{toEmoji cfg.genTcProjRws} Generate Type Class Projection Rewrites"
     trace cls fun _ => m!"{toEmoji cfg.genTcSpecRws} Generate Type Class Specialization Rewrites"
-    trace cls fun _ => m!"{toEmoji cfg.genNatLitRws} Enable Definitional Natural Number Literal Rewrites"
-    trace cls fun _ => m!"{toEmoji cfg.genBetaRw} Enable β-Reduction"
-    trace cls fun _ => m!"{toEmoji cfg.genEtaRw} Enable η-Reduction"
+    trace cls fun _ => m!"{toEmoji cfg.natLit} Enable Definitional Natural Number Literal Rewrites"
+    trace cls fun _ => m!"{toEmoji cfg.beta} Enable β-Reduction"
+    trace cls fun _ => m!"{toEmoji cfg.eta} Enable η-Reduction"
     trace cls fun _ => m!"{toEmoji cfg.blockInvalidMatches} Block Invalid Matches"
     trace cls fun _ => m!"{toEmoji cfg.shiftCapturedBVars} Correct BVar Indices"
     trace cls fun _ => m!"{toEmoji cfg.optimizeExpl} Optimize Explanation Length"

Lean/Egg/Tests/Andrés/Andrés/Basic.lean

@@ -19,8 +19,6 @@ example [Module R S] (q : ℚ≥0) (a : S) : (q : R) • a = q • a := by
     Nat.cast_smul_eq_nsmul
   ]
 
--- TODO: This saturates in slotted? I'm guessing there's something wrong with the saturation
---       condition/progress measure.
 set_option egg.slotted true in
 example [Module R S] (q : ℚ≥0) (a : S) : (q : R) • a = q • a := by
   refine MulAction.injective₀ (G₀ := ℚ≥0) (Nat.cast_ne_zero.2 q.den_pos.ne') ?_

Lean/Egg/Tests/Andrés/lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "31a10a332858d6981dbcf55d54ee51680dd75f18",
+   "rev": "76e9ebe4176d29cb9cc89c669ab9f1ce32b33c3d",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1357f4f49450abb9dfd4783e38219f4ce84f9785",
+   "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5f934891e11d70a1b86e302fdf9cecfc21e8de46",
+   "rev": "45d016d59cf45bcf8493a203e9564cfec5203d9b",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,17 +35,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "baa65c6339a56bd22b7292aa4511c54b3cc7a6af",
+   "rev": "1383e72b40dd62a566896a6e348ffe868801b172",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.43",
+   "inputRev": "v0.0.46",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
+   "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "984d7ee170b75d6b03c0903e0b750ee2c6d1e3fb",
+   "rev": "ac7b989cbf99169509433124ae484318e953d201",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -71,14 +71,24 @@
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "0f1430e6f1193929f13905d450b2a44a54f3927e",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d5ab93e3a3afadaf265a583a92f7e7c47203b540",
+   "rev": "a7fc949f1b05c2a01e01c027fd9f480496a1253e",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.13.0",
+   "inputRev": "v4.14.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/nomeata/lean-calcify",

Lean/Egg/Tests/Andrés/lakefile.toml

@@ -6,7 +6,7 @@ defaultTargets = ["«Andrés»"]
 [[require]]
 name    = "mathlib"
 scope   = "leanprover-community"
-version = "git#v4.13.0"
+version = "git#v4.14.0-rc1"
 
 [[require]]
 name = "egg"

Lean/Egg/Tests/Andrés/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.13.0
+leanprover/lean4:v4.14.0-rc1

Lean/Egg/Tests/BVar Index Correction.lean

@@ -7,7 +7,7 @@ example (h : ∀ x y : Nat, x = y ↔ y = x) : (∀ x y : Nat, x = y) ↔ (∀ a
 -- We have to disable β-reduction as part of normalization, as otherwise `thm₁,₂` are useless, and
 -- disable β-reduction in egg, as this interferes with the test cases.
 set_option egg.betaReduceRws false
-set_option egg.genBetaRw false
+set_option egg.beta false
 
 -- This theorem is only applicable in the forward direction.
 theorem thm₁ : ∀ x y : Nat, (x, y).fst = (fun _ => x) (nat_lit 1) :=

Lean/Egg/Tests/Beta.lean

@@ -1,6 +1,6 @@
 import Egg
 
-set_option egg.genBetaRw true
+set_option egg.beta true
 
 example : (fun x => x) 0 = 0 := by
   egg

Lean/Egg/Tests/Block Invalid Matches.lean

@@ -9,8 +9,8 @@ set_option egg.shiftCapturedBVars false
 -- any way, so we disable them.
 set_option egg.betaReduceRws false
 set_option egg.etaReduceRws false
-set_option egg.genBetaRw false
-set_option egg.genEtaRw false
+set_option egg.beta false
+set_option egg.eta false
 
 -- These tests cover Condition (1) of (in-)valid matches.
 section «Condition 1»

Lean/Egg/Tests/Conditional.lean

@@ -101,9 +101,9 @@ info: [egg.rewrites] Rewrites
 #guard_msgs(info, drop error) in
 set_option egg.genTcProjRws false in
 set_option egg.builtins false in
-set_option egg.genBetaRw false in
-set_option egg.genEtaRw false in
-set_option egg.genNatLitRws false in
+set_option egg.beta false in
+set_option egg.eta false in
+set_option egg.natLit false in
 set_option egg.builtins false in
 example (l₁ l₂ : List Nat) (h : ∀ (α : Type) (l₁ l₂ : List α), l₁ = l₂) : l₁ = l₂ := by
   set_option trace.egg.rewrites true in egg [h]

Lean/Egg/Tests/EraseProofs.lean

@@ -7,8 +7,8 @@ set_option egg.eraseProofs true
 /-- error: egg failed to prove the goal (saturated) -/
 #guard_msgs in
 set_option egg.eraseProofs false in
-set_option egg.genBetaRw false in
-set_option egg.genEtaRw false in
+set_option egg.beta false in
+set_option egg.eta false in
 example (arr : Array α) (i : Nat) (h₁ h₂ : i < arr.size) : arr[i]'h₁ = arr[i]'h₂ := by
   egg
 

Lean/Egg/Tests/Eta.lean

@@ -1,10 +1,10 @@
 import Egg
 
 -- Note: We disable β-reduction as it can also solve many of these cases without η-reduction.
-set_option egg.genEtaRw true
-set_option egg.genBetaRw false
+set_option egg.eta true
+set_option egg.beta false
 
-set_option egg.genEtaRw false in
+set_option egg.eta false in
 /-- error: egg failed to prove the goal (saturated) -/
 #guard_msgs in
 example : (fun x => Nat.succ x) = Nat.succ := by
@@ -44,7 +44,7 @@ example : id (eta 2 Nat.succ Nat) = id Nat.succ := by
 example : (eta 50 Nat.succ Nat) = Nat.succ := by
   egg
 
-set_option egg.genEtaRw false in
+set_option egg.eta false in
 /-- error: egg failed to prove the goal (saturated) -/
 #guard_msgs in
 example (a : Nat) (h : ∀ b : Nat, b.succ.add a = 0) : (10 |> fun x => Nat.succ x).add a = 0 := by

Lean/Egg/Tests/Explosion.lean

@@ -1,11 +1,11 @@
 import Egg
 
-set_option egg.genEtaRw false
-set_option egg.genBetaRw false
+set_option egg.eta false
+set_option egg.beta false
 set_option egg.genTcProjRws false
 set_option egg.genGoalTcSpec false
 set_option egg.builtins false
-set_option egg.genNatLitRws false
+set_option egg.natLit false
 
 set_option egg.explosion true
 

Lean/Egg/Tests/Level Defeq.lean

@@ -3,23 +3,23 @@ import Egg
 -- The only difference between these two and the next two examples is the order of universe levels
 -- in `[]`. That is, the second examples require commutativity of `Level.max`.
 
-set_option egg.genLevelRws false in
+set_option egg.levels false in
 example (f : α → γ) (g : β → δ) : List.map (Prod.map f g) [] = [] := by
   egg [List.map]
 
-set_option egg.genLevelRws true in
+set_option egg.levels true in
 example (f : α → γ) (g : β → δ) : List.map (Prod.map f g) [] = [] := by
   egg [List.map]
 
 variable {α : Type _} {β : Type _} {γ : Type _} {δ : Type _}
 
 /-- error: egg failed to prove the goal (saturated) -/
 #guard_msgs in
-set_option egg.genLevelRws false in
+set_option egg.levels false in
 example (f : α → γ) (g : β → δ) : List.map (Prod.map f g) [] = [] := by
   egg [List.map]
 
-set_option egg.genLevelRws true in
+set_option egg.levels true in
 example (f : α → γ) (g : β → δ) : List.map (Prod.map f g) [] = [] := by
   egg [List.map]
 

Lean/Egg/Tests/NatLit.lean

@@ -2,7 +2,7 @@ import Egg
 
 -- Tests involving conversions between `Nat.zero` and `Nat.succ _` and `.lit (.natVal _)`.
 
-set_option egg.genNatLitRws true
+set_option egg.natLit true
 
 example : 0 = Nat.zero := by
   egg
@@ -66,7 +66,7 @@ example : 12345 % 67890 = 12345 := by
 example : 12345 % 0 = 12345 := by
   egg
 
-set_option egg.genNatLitRws false in
+set_option egg.natLit false in
 set_option egg.natReduceRws false in
 /-- error: egg failed to prove the goal (saturated) -/
 #guard_msgs in