Correct the definitional of visible mvars

marcusrossel · Dec 18, 2024 · 11ff29b · 11ff29b
1 parent 47aad5b
commit 11ff29b
Show file tree

Hide file tree

Showing 8 changed files with 71 additions and 53 deletions.
diff --git a/Lean/Egg/Core/MVars/Basic.lean b/Lean/Egg/Core/MVars/Basic.lean
@@ -9,8 +9,8 @@ open Std (HashMap HashSet)
 namespace Egg.MVars
 
 /-
-1. An mvar is `inTarget` if it appears explicitly in the given expression. For example, this holds
-   for `?m` in `f (?m + 1)`.
+1. An mvar is `unconditionallyVisible` if it appears explicitly in the given expression, but not in
+   a type class instance or proof term. For example, this holds for `?m` in `f (?m + 1)`.
 2. An mvar `isTcInst` if its type is a type class. For example, this holds for `?i` in
    `@Add Nat ?i`.
 3. An mvar is `inTcInstTerm` if it appears explicitly in a term whose type is a type class. For
@@ -33,11 +33,11 @@ the erasure configuration. The visibility property is used for the following:
 * To determine whether a given condition of a conditional rewrite is unbounded.
 
 Other use cases of properties are:
-* To determine which mvars are conditions of a rewrite, we also need to use Properties 3 and 5.
+* To determine which mvars are conditions of a rewrite, we also need to use Properties 1, 3 and 5.
 * Type class specialization needs Property 2.
 -/
 inductive Property where
-  | inTarget
+  | unconditionallyVisible
   | isTcInst
   | inTcInstTerm
   | inErasedTcInst
@@ -49,19 +49,17 @@ abbrev Properties := HashSet Property
 
 namespace Properties
 
-def containsErased (ps : Properties) : Bool :=
-  ps.any fun
-    | .inErasedProof | .inErasedTcInst => true
-    | _                                => false
-
 def isVisible (ps : Properties) (cfg : Config.Erasure) : Bool :=
-  let tcInstErasureVisibility := ps.contains .inErasedTcInst && cfg.eraseTCInstances
-  let proofErasureVisibility  := ps.contains .inErasedProof  && cfg.eraseProofs
-  let basicVisibility :=
-    ps.contains .inTarget
-    && !(ps.contains .inProofTerm  && cfg.eraseProofs)
-    && !(ps.contains .inTcInstTerm && cfg.eraseTCInstances)
-  basicVisibility || tcInstErasureVisibility || proofErasureVisibility
+  ps.contains .unconditionallyVisible
+  || (ps.contains .inTcInstTerm   && !cfg.eraseTCInstances)
+  || (ps.contains .inErasedTcInst && cfg.eraseTCInstances)
+  || (ps.contains .inProofTerm    && !cfg.eraseProofs)
+  || (ps.contains .inErasedProof  && cfg.eraseProofs)
+
+def inTarget (ps : Properties) : Bool :=
+  ps.contains .unconditionallyVisible
+  || ps.contains .inProofTerm
+  || ps.contains .inTcInstTerm
 
 def insertIf (ps : Properties) (condition : Bool) (p : Property) : Properties :=
   if condition then ps.insert p else ps
@@ -87,7 +85,7 @@ def tcInsts (mvars : MVars) : MVarIdSet :=
 
 def inTarget (mvars : MVars) : MVarIdSet :=
   mvars.expr.fold (init := ∅) fun result m ps =>
-    if ps.contains .inTarget then result.insert m else result
+    if ps.inTarget then result.insert m else result
 
 def insertExpr (mvars : MVars) (m : MVarId) (ps : Properties) : MVars :=
   { mvars with expr := mvars.expr.alter m (ps.union <| ·.getD ∅) }

diff --git a/Lean/Egg/Core/MVars/Collect.lean b/Lean/Egg/Core/MVars/Collect.lean
@@ -35,13 +35,13 @@ private def collectMVar (mvar : MVarId) : CollectionM Unit := do
   modify fun s =>
     let ps := s.active
       |>.insertIf isTcInst .isTcInst
-      |>.insertIf (!s.active.containsErased) .inTarget
+      |>.insertIf s.active.isEmpty .unconditionallyVisible
     { s with mvars := s.mvars.insertExpr mvar ps }
 
 private def collectLMVar (lmvar : LMVarId) : CollectionM Unit := do
   if (← amb).lvl.contains lmvar then return
   modify fun s =>
-    let ps := s.active.insertIf (!s.active.containsErased) .inTarget
+    let ps := s.active.insertIf s.active.isEmpty .unconditionallyVisible
     { s with mvars := s.mvars.insertLevel lmvar ps }
 
 private def collectLevel (lvl : Level) : CollectionM Unit := do

diff --git a/Lean/Egg/Tactic/Trace.lean b/Lean/Egg/Tactic/Trace.lean
@@ -51,12 +51,12 @@ nonrec def formatReport
     (if rep.rwStats.isEmpty then "" else s!"\nrw stats:\n{rep.rwStats}")
 
 def MVars.Property.toMessageData : MVars.Property → MessageData
-  | .inTarget       => m!".inTarget"
-  | .isTcInst       => m!".isTcInst"
-  | .inTcInstTerm   => m!".inTcInstTerm"
-  | .inErasedTcInst => m!".inErasedTcInst"
-  | .inProofTerm    => m!".inProofTerm"
-  | .inErasedProof  => m!".inErasedProof"
+  | .unconditionallyVisible => m!".unconditionallyVisible"
+  | .isTcInst               => m!".isTcInst"
+  | .inTcInstTerm           => m!".inTcInstTerm"
+  | .inErasedTcInst         => m!".inErasedTcInst"
+  | .inProofTerm            => m!".inProofTerm"
+  | .inErasedProof          => m!".inErasedProof"
 
 def MVars.Properties.toMessageData (ps : MVars.Properties) : MessageData :=
   ps.toList.map Property.toMessageData

diff --git a/Lean/Egg/Tests/Conditional.lean b/Lean/Egg/Tests/Conditional.lean
@@ -79,9 +79,9 @@ info: [egg.rewrites] Rewrites
     [egg.rewrites] #0(∅): h
       [egg.rewrites] ?l₁ = ?l₂
       [egg.rewrites] LHS MVars
-          [?l₁: [.inTarget]]
+          [?l₁: [.unconditionallyVisible]]
       [egg.rewrites] RHS MVars
-          [?l₂: [.inTarget]]
+          [?l₂: [.unconditionallyVisible]]
   [egg.rewrites] Tagged (0)
   [egg.rewrites] Builtin (0)
   [egg.rewrites] Derived (0)

diff --git a/Lean/Egg/Tests/Explosion.lean b/Lean/Egg/Tests/Explosion.lean
@@ -55,9 +55,9 @@ info: [egg.rewrites] Rewrites
     [egg.rewrites] #0(⇔): h
       [egg.rewrites] f ?x ?y = f ?y ?x
       [egg.rewrites] LHS MVars
-          [?y: [.inTarget], ?x: [.inTarget]]
+          [?y: [.unconditionallyVisible], ?x: [.unconditionallyVisible]]
       [egg.rewrites] RHS MVars
-          [?y: [.inTarget], ?x: [.inTarget]]
+          [?y: [.unconditionallyVisible], ?x: [.unconditionallyVisible]]
   [egg.rewrites] Tagged (0)
   [egg.rewrites] Builtin (0)
   [egg.rewrites] Derived (0)
@@ -77,9 +77,9 @@ info: [egg.rewrites] Rewrites
     [egg.rewrites] #0(⇔): h
       [egg.rewrites] f ?x ?y = f ?y ?x
       [egg.rewrites] LHS MVars
-          [?x: [.inTarget], ?y: [.inTarget]]
+          [?x: [.unconditionallyVisible], ?y: [.unconditionallyVisible]]
       [egg.rewrites] RHS MVars
-          [?x: [.inTarget], ?y: [.inTarget]]
+          [?x: [.unconditionallyVisible], ?y: [.unconditionallyVisible]]
   [egg.rewrites] Tagged (0)
   [egg.rewrites] Builtin (0)
   [egg.rewrites] Derived (0)
@@ -99,24 +99,24 @@ info: [egg.rewrites] Rewrites
     [egg.rewrites] #0(⇐): h
       [egg.rewrites] f ?x ?x = f ?y ?x
       [egg.rewrites] LHS MVars
-          [?x: [.inTarget]]
+          [?x: [.unconditionallyVisible]]
       [egg.rewrites] RHS MVars
-          [?x: [.inTarget], ?y: [.inTarget]]
+          [?x: [.unconditionallyVisible], ?y: [.unconditionallyVisible]]
   [egg.rewrites] Tagged (0)
   [egg.rewrites] Builtin (0)
   [egg.rewrites] Derived (2)
     [egg.rewrites] #0💥→[3](⇔)
       [egg.rewrites] f ?m.243 ?m.243 = f a ?m.243
       [egg.rewrites] LHS MVars
-          [?m.243: [.inTarget]]
+          [?m.243: [.unconditionallyVisible]]
       [egg.rewrites] RHS MVars
-          [?m.243: [.inTarget]]
+          [?m.243: [.unconditionallyVisible]]
     [egg.rewrites] #0💥→[4](⇔)
       [egg.rewrites] f ?m.252 ?m.252 = f b ?m.252
       [egg.rewrites] LHS MVars
-          [?m.252: [.inTarget]]
+          [?m.252: [.unconditionallyVisible]]
       [egg.rewrites] RHS MVars
-          [?m.252: [.inTarget]]
+          [?m.252: [.unconditionallyVisible]]
   [egg.rewrites] Definitional
   [egg.rewrites] Hypotheses (0)
   [egg.rewrites] Pruned (0)

diff --git a/Lean/Egg/Tests/MVars Properties.lean b/Lean/Egg/Tests/MVars Properties.lean
@@ -12,9 +12,9 @@ info: [egg.rewrites] Rewrites
     [egg.rewrites] #0(⇔): h
       [egg.rewrites] ?x = ?x
       [egg.rewrites] LHS MVars
-          [?x: [.inTarget]]
+          [?x: [.unconditionallyVisible]]
       [egg.rewrites] RHS MVars
-          [?x: [.inTarget]]
+          [?x: [.unconditionallyVisible]]
   [egg.rewrites] Tagged (0)
   [egg.rewrites] Builtin (0)
   [egg.rewrites] Derived (0)
@@ -32,9 +32,9 @@ info: [egg.rewrites] Rewrites
     [egg.rewrites] #0(⇒): h
       [egg.rewrites] f ?x = ?x
       [egg.rewrites] LHS MVars
-          [?x: [.inTarget], ?α: [.inTarget]]
+          [?x: [.unconditionallyVisible], ?α: [.unconditionallyVisible]]
       [egg.rewrites] RHS MVars
-          [?x: [.inTarget]]
+          [?x: [.unconditionallyVisible]]
   [egg.rewrites] Tagged (0)
   [egg.rewrites] Builtin (0)
   [egg.rewrites] Derived (0)
@@ -52,9 +52,9 @@ info: [egg.rewrites] Rewrites
     [egg.rewrites] #0(⇒): h
       [egg.rewrites] ?x + ?x = ?x
       [egg.rewrites] LHS MVars
-          [?x: [.inTarget], ?inst✝: [.inTcInstTerm, .isTcInst, .inTarget]]
+          [?x: [.unconditionallyVisible], ?inst✝: [.inTcInstTerm, .isTcInst]]
       [egg.rewrites] RHS MVars
-          [?x: [.inTarget]]
+          [?x: [.unconditionallyVisible]]
   [egg.rewrites] Tagged (0)
   [egg.rewrites] Builtin (0)
   [egg.rewrites] Derived (0)
@@ -65,3 +65,23 @@ info: [egg.rewrites] Rewrites
 #guard_msgs(info) in
 example (h : ∀ [Add α] (x : α), x + x = x) : true = true := by
   egg [h]
+
+/--
+info: [egg.rewrites] Rewrites
+  [egg.rewrites] Basic (1)
+    [egg.rewrites] #0(⇔): h
+      [egg.rewrites] f ?n ⋯ = ?n
+      [egg.rewrites] LHS MVars
+          [?n: [.inErasedProof, .inProofTerm, .unconditionallyVisible]]
+      [egg.rewrites] RHS MVars
+          [?n: [.unconditionallyVisible]]
+  [egg.rewrites] Tagged (0)
+  [egg.rewrites] Builtin (0)
+  [egg.rewrites] Derived (0)
+  [egg.rewrites] Definitional
+  [egg.rewrites] Hypotheses (0)
+  [egg.rewrites] Pruned (0)
+-/
+#guard_msgs(info) in
+example (f : (n : Nat) → (0 < n + 1) → Nat) (h : ∀ n, f n (Nat.zero_lt_succ n) = n) : 0 = 0 := by
+  egg [h]
diff --git a/Lean/Egg/Tests/Prune.lean b/Lean/Egg/Tests/Prune.lean
@@ -40,9 +40,9 @@ info: [egg.rewrites] Rewrites
     [egg.rewrites] #0(⇔): Nat.add_comm
       [egg.rewrites] ?n + ?m = ?m + ?n
       [egg.rewrites] LHS MVars
-          [?m: [.inTarget], ?n: [.inTarget]]
+          [?m: [.unconditionallyVisible], ?n: [.unconditionallyVisible]]
       [egg.rewrites] RHS MVars
-          [?m: [.inTarget], ?n: [.inTarget]]
+          [?m: [.unconditionallyVisible], ?n: [.unconditionallyVisible]]
   [egg.rewrites] Tagged (0)
   [egg.rewrites] Builtin (0)
   [egg.rewrites] Derived (0)
@@ -52,8 +52,8 @@ info: [egg.rewrites] Rewrites
     [egg.rewrites] #1(⇔)
       [egg.rewrites] ?a + ?b = ?b + ?a
       [egg.rewrites] LHS MVars
-          [?b: [.inTarget], ?a: [.inTarget]]
-      [egg.rewrites] RHS MVars [?b: [.inTarget], ?a: [.inTarget]]
+          [?b: [.unconditionallyVisible], ?a: [.unconditionallyVisible]]
+      [egg.rewrites] RHS MVars [?b: [.unconditionallyVisible], ?a: [.unconditionallyVisible]]
 -/
 #guard_msgs in
 set_option linter.unusedVariables false in

diff --git a/Lean/Egg/Tests/Tagged TC Gen.lean b/Lean/Egg/Tests/Tagged TC Gen.lean
@@ -21,13 +21,13 @@ info: [egg.rewrites] Rewrites
     [egg.rewrites] □0(⇔)
       [egg.rewrites] z = z
       [egg.rewrites] LHS MVars
-          [?α: [.inErasedTcInst, .inTarget],
-           ?c: [.inTcInstTerm, .isTcInst, .inTarget],
-           ?u.80: [.inErasedTcInst, .inTarget]]
+          [?α: [.inErasedTcInst, .unconditionallyVisible],
+           ?c: [.inTcInstTerm, .isTcInst],
+           ?u.80: [.inErasedTcInst, .unconditionallyVisible]]
       [egg.rewrites] RHS MVars
-          [?α: [.inErasedTcInst, .inTarget],
-           ?c: [.inTcInstTerm, .isTcInst, .inTarget],
-           ?u.80: [.inErasedTcInst, .inTarget]]
+          [?α: [.inErasedTcInst, .unconditionallyVisible],
+           ?c: [.inTcInstTerm, .isTcInst],
+           ?u.80: [.inErasedTcInst, .unconditionallyVisible]]
   [egg.rewrites] Builtin (0)
   [egg.rewrites] Derived (3)
     [egg.rewrites] □0<⊢>(⇔)