Implement blocking of propositional conditions

Author: marcusrossel

Lean/Egg/Core/Blocks.lean

@@ -1,13 +1,14 @@
 import Egg.Core.Source
 import Egg.Core.Normalize
-import Lean
-open Lean
+
+open Lean Meta
 
 namespace Egg
 
 abbrev Block := Expr
 
-def Block.from (expr : Expr) (cfg : Config.Normalization) : MetaM Block :=
+def Block.from? (expr : Expr) (cfg : Config.Normalization) : MetaM (Option Block) := do
+  unless (← inferType expr).isProp do return none
   normalize expr cfg
 
 abbrev Blocks := Array Block

Lean/Egg/Tactic/Basic.lean

@@ -4,6 +4,7 @@ import Egg.Tactic.Config.Option
 import Egg.Tactic.Config.Modifier
 import Egg.Tactic.Goal
 import Egg.Tactic.Guides
+import Egg.Tactic.Blocks
 import Egg.Tactic.Rewrite.Rules.Gen.Basic
 import Egg.Core.Gen.Guides
 import Egg.Tactic.Trace
@@ -41,8 +42,8 @@ open Config.Modifier (egg_cfg_mod)
 syntax egg_baskets := ("+" noWs ident)*
 
 protected partial def eval
-    (mod : TSyntax ``egg_cfg_mod) (args : TSyntax `egg_args)
-    (guides : Option (TSyntax `egg_guides)) (baskets : TSyntax `Egg.egg_baskets)
+    (mod : TSyntax ``egg_cfg_mod) (args : TSyntax `egg_args) (guides : Option (TSyntax `egg_guides))
+    (blocks : Option (TSyntax `egg_blocks)) (baskets : TSyntax `Egg.egg_baskets)
     (calcifyTk? : Option Syntax := none) : TacticM Unit := do
   let save ← saveState
   try core catch err => restoreState save; throw err
@@ -57,6 +58,7 @@ where
     let goal ← Goal.gen goal
     goal.id.withContext do
       let guides := (← guides.mapM Guides.parseGuides).getD #[]
+      let blocks ← getBlocks blocks cfg
       -- We increase the mvar context depth, so that ambient mvars aren't unified during rewrite
       -- generation proof and reconstruction. Note that this also means that we can't assign the
       -- `goal` mvar inside of this `do`-block .
@@ -67,7 +69,7 @@ where
             let rws := rules.entries.map (·.rw)
             guides := guides ++ (← genDerivedGuides goal.toCongr rws)
         withTraceNode `egg.guides (fun _ => return "Guides") do guides.trace `egg.guides
-        runEqSat goal rules guides cfg
+        runEqSat goal rules guides blocks cfg
       match res with
       | some (proof, proofTime, result) =>
         if cfg.reporting then
@@ -79,9 +81,9 @@ where
         if let some tk := calcifyTk? then calcify tk proof goal.intros.unzip.snd
       | none => goal.id.admit
   runEqSat
-      (goal : Goal) (rules : Rewrite.Rules) (guides : Guides) (cfg : Config) :
+      (goal : Goal) (rules : Rewrite.Rules) (guides : Guides) (blocks : Blocks) (cfg : Config) :
       TacticM <| Option (AbstractMVarsResult × Nat × Request.Result) := do
-    let req ← Request.encoding goal.toCongr rules guides #[] cfg
+    let req ← Request.encoding goal.toCongr rules guides blocks cfg
     withTraceNode `egg.encoded (fun _ => return "Encoded") do req.trace `egg.encoded
     if let .beforeEqSat := cfg.exitPoint then return none
     let result ← req.run cfg.explLengthLimit (onEqSatFailure cfg)
@@ -92,7 +94,7 @@ where
     | .proof prf =>
       let proofTime := (← IO.monoMsNow) - beforeProof
       return some (prf, proofTime, result)
-    | .retryWithShapes => runEqSat goal rules guides { cfg with shapes := true }
+    | .retryWithShapes => runEqSat goal rules guides blocks { cfg with shapes := true }
   onEqSatFailure (cfg : Config) (report : Request.Result.Report) : Request.Failure → MetaM MessageData
     | .backend msg? => do
       let mut msg := msg?
@@ -105,17 +107,21 @@ where
       let msg := s!"egg found an explanation exceeding the length limit ({len} vs {cfg.explLengthLimit})\nYou can increase this limit using 'set_option egg.explLengthLimit <num>'.\n"
       unless cfg.reporting do return msg
       return msg ++ formatReport cfg.flattenReports report
+  getBlocks (stx? : Option <| TSyntax `egg_blocks) (cfg : Config) : TacticM Blocks := do
+    let some stx := stx? | return #[]
+    unless cfg.subgoals do logWarningAt stx "conditions are only blocked when `egg.subgoals` is `true`"
+    Blocks.parseBlocks cfg.toNormalization stx
 
-elab "egg " baskets:egg_baskets mod:egg_cfg_mod args:egg_args guides:(egg_guides)? : tactic =>
-  Egg.eval mod args guides baskets
+elab "egg " baskets:egg_baskets mod:egg_cfg_mod args:egg_args guides:(egg_guides)? blocks:(egg_blocks)? : tactic =>
+  Egg.eval mod args guides blocks baskets
 
 -- WORKAROUND: This fixes `Tests/EndOfInput *`.
 macro "egg " baskets:egg_baskets mod:egg_cfg_mod : tactic =>
   `(tactic| egg $baskets $mod:egg_cfg_mod)
 
 -- The syntax `egg?` calls calcify after running egg.
-elab tk:"egg? " baskets:egg_baskets mod:egg_cfg_mod args:egg_args guides:(egg_guides)? : tactic =>
-  Egg.eval mod args guides baskets (calcifyTk? := tk)
+elab tk:"egg? " baskets:egg_baskets mod:egg_cfg_mod args:egg_args guides:(egg_guides)? blocks:(egg_blocks)? : tactic =>
+  Egg.eval mod args guides blocks baskets (calcifyTk? := tk)
 
 -- WORKAROUND: This fixes a problem analogous to `Tests/EndOfInput *` for `egg?`.
 macro "egg? " baskets:egg_baskets mod:egg_cfg_mod : tactic =>

Lean/Egg/Tactic/Blocks.lean

@@ -0,0 +1,20 @@
+import Egg.Core.Blocks
+import Lean
+open Lean Elab Tactic
+
+namespace Egg.Blocks
+
+declare_syntax_cat egg_blocks
+syntax " blocking " (term,*) : egg_blocks
+
+def parseBlocks (cfg : Config.Normalization) : TSyntax `egg_blocks → TacticM Blocks
+  | `(egg_blocks|blocking $bs,*) => do
+    let mut blocks : Blocks := #[]
+    for b in bs.getElems do
+      let e ← Tactic.elabTerm b none
+      -- See `parseGuides` for an explanation of this.
+      if e.hasSorry then continue
+      let some block ← Block.from? e cfg | throwErrorAt b "blocking terms must be propositions"
+      blocks := blocks.push block
+    return blocks
+  | _ => unreachable!

Lean/Egg/Tactic/Calc.lean

@@ -23,7 +23,7 @@ syntax egg_calc_step := ppIndent(colGe term (&" with " egg_cfg_mod egg_args)? (e
 
 structure Step where
   mod    : TSyntax ``egg_cfg_mod
-  args  : TSyntax `egg_args
+  args   : TSyntax `egg_args
   guides : Option (TSyntax `egg_guides)
 deriving Inhabited
 
@@ -65,11 +65,11 @@ def parseRawSteps : (TSyntax ``egg_calc_steps) → TacticM RawSteps
       $tail]*) => return { head := ← parseRawStep head, tail := ← tail.mapM parseRawStep }
   | _ => throwUnsupportedSyntax
 
-syntax &"egg " egg_baskets &" calc " egg_args egg_calc_steps : tactic
+syntax &"egg " egg_baskets &" calc " egg_args egg_calc_steps (egg_blocks)? : tactic
 
 def eval
     (baskets : TSyntax `Egg.egg_baskets) (args : TSyntax `egg_args)
-    (steps : TSyntax ``egg_calc_steps) : TacticM Unit := do
+    (steps : TSyntax ``egg_calc_steps) (blocks : Option <| TSyntax `egg_blocks) : TacticM Unit := do
   withMainContext do
     let rawSteps ← parseRawSteps steps
     let goalType ← getMainTarget
@@ -112,7 +112,7 @@ where
     throwError "'egg calc' failed to infer goal type"
   stepToEgg (step : Step) : TacticM (TSyntax `tactic) := do
     let allPrems ← appendArgs step.args args
-    `(tactic| egg $baskets $step.mod:egg_cfg_mod $allPrems $[$step.guides]?)
+    `(tactic| egg $baskets $step.mod:egg_cfg_mod $allPrems $[$step.guides]? $[$blocks]?)
   dedupSubgoals (subgoals : List MVarId) : MetaM (List MVarId) := do
     let mut result := []
     for subgoal in subgoals do
@@ -164,5 +164,5 @@ where
       lastRhs := rhs
     return result
 
-elab "egg " baskets:egg_baskets " calc " args:egg_args steps:egg_calc_steps : tactic =>
-  eval baskets args steps
+elab "egg " baskets:egg_baskets " calc " args:egg_args steps:egg_calc_steps blocks:(egg_blocks)?: tactic =>
+  eval baskets args steps blocks

Lean/Egg/Tests/Blocking.lean

@@ -0,0 +1,49 @@
+import Egg
+
+/-- warning: conditions are only blocked when `egg.subgoals` is `true` -/
+#guard_msgs in
+example : True := by
+  egg blocking True
+
+/-- error: blocking terms must be propositions -/
+#guard_msgs in
+example : True := by
+  egg blocking 0
+
+set_option egg.subgoals true
+
+example : True := by
+  egg blocking True
+
+variable {P : Prop}
+
+/--
+error: unsolved goals
+P : Prop
+h : P → False
+⊢ P
+-/
+#guard_msgs in
+example (h : P → False) : False := by
+  egg [h]
+
+/-- error: egg failed to prove the goal (saturated) -/
+#guard_msgs in
+example (h : P → False) : False := by
+  egg [h] blocking P
+
+/--
+error: unsolved goals
+P Q : Prop
+hq : Q
+h₁ : P → False
+h₂ : Q → False
+⊢ P
+-/
+#guard_msgs in
+example {Q : Prop} (hq : Q) (h₁ : P → False) (h₂ : Q → False) : False := by
+  egg [h₁, h₂]
+
+example {Q : Prop} (hq : Q) (_h₁ : P → False) (h₂ : Q → False) : False := by
+  egg [_h₁, h₂] blocking P
+  exact hq