Tauto infinite loop

Stream: metaprogramming / tactics

[Sam Ezeh]

https://github.com/leanprover-community/mathlib4/issues/10590

Would this issue be suitable for me to begin contributing to Mathlib's meta-library? What would an acceptable solution look like? I've written a fix that tags hypotheses with a hashset so we don't visit them twice, would this be an acceptable approach or is there a better way of doing this?

[Sam Ezeh]

The diff looks like this

diff --git a/Mathlib/Tactic/Tauto.lean b/Mathlib/Tactic/Tauto.lean
index a61841c23a..cb5062d8a7 100644
--- a/Mathlib/Tactic/Tauto.lean
+++ b/Mathlib/Tactic/Tauto.lean
@@ -111,12 +111,15 @@ partial def distribNotAux (fvars : List Expr) (g : MVarId) : MetaM MVarId :=
 Tries to apply de-Morgan-like rules on all hypotheses.
 Always succeeds, regardless of whether any progress was actually made.
 -/
-def distribNot : TacticM Unit := withMainContext do
-  let mut fvars := []
+def distribNot (visited : ST.Ref IO.RealWorld (HashSet FVarId)) : TacticM Unit := withMainContext do
+  let mut fvarIds := []
   for h in ← getLCtx do
+    if (← visited.get).contains h.fvarId then
+      continue
     if !h.isImplementationDetail then
-      fvars := mkFVar h.fvarId :: fvars
-  liftMetaTactic' (distribNotAux fvars)
+      fvarIds := h.fvarId :: fvarIds
+  liftMetaTactic' (distribNotAux (fvarIds.map mkFVar))
+  visited.modify (λ s ↦ s.insertMany fvarIds)

 /-- Config for the `tauto` tactic. Currently empty. TODO: add `closer` option. -/
 structure Config
@@ -158,11 +161,12 @@ duplicated work.
 def tautoCore : TacticM Unit := do
   _ ← tryTactic (evalTactic (← `(tactic| contradiction)))
   _ ← tryTactic (evalTactic (← `(tactic| assumption)))
+  let visited ← ST.mkRef .empty
   iterateUntilFailure do
     let gs ← getUnsolvedGoals
     allGoals (
       liftMetaTactic (fun m => do pure [(← m.intros!).2]) <;>
-      distribNot <;>
+      distribNot visited <;>
       liftMetaTactic (casesMatching casesMatcher (recursive := true) (throwOnNoMatch := false)) <;>
       (do _ ← tryTactic (evalTactic (← `(tactic| contradiction)))) <;>
       (do _ ← tryTactic (evalTactic (← `(tactic| refine or_iff_not_imp_left.mpr ?_)))) <;>

[David Renshaw]

Thanks for looking into this!

[David Renshaw]

My initial reaction is: it would be nice to avoid the need for ref cells.

[David Renshaw]

Here's a more narrow "fix", that just bails when replace does not get rid of the old hypothesis:

diff --git a/Mathlib/Tactic/Tauto.lean b/Mathlib/Tactic/Tauto.lean
index a61841c23a..9e6e61e026 100644
--- a/Mathlib/Tactic/Tauto.lean
+++ b/Mathlib/Tactic/Tauto.lean
@@ -25,7 +25,13 @@ def distribNotOnceAt (hypFVar : Expr) (g : MVarId) : MetaM AssertAfterResult :=
   let .fvar fvarId := hypFVar | throwError "not fvar {hypFVar}"
   let h ← fvarId.getDecl
   let e : Q(Prop) ← (do guard <| ← Meta.isProp h.type; pure h.type)
-  let replace (p : Expr) := g.replace h.fvarId p
+  let replace (p : Expr) : MetaM AssertAfterResult := do
+     let result ← g.replace h.fvarId p
+     result.mvarId.withContext do
+     if (← getLCtx).contains h.fvarId
+     then throwError "'replace' did not remove the existing hypothesis"
+     pure result
+
   match e with
   | ~q(¬ ($a : Prop) = $b) => do
     let h' : Q(¬$a = $b) := h.toExpr

[David Renshaw]

On the other hand, with your fix, tauto can probably prove more things than with my fix. (EDIT: or maybe not? see my later comments below)

[David Renshaw]

Added a comment on the issue: https://github.com/leanprover-community/mathlib4/issues/10590#issuecomment-2028196263

[David Renshaw]

My initial reaction is: it would be nice to avoid the need for ref cells.

I believe it's possible for fvars to be shared among multiple subgoals being operated on by the allGoals combinator, and I think that we typically want distribNot to act on all of the hypotheses of these subgoals. So it seems potentially problematic to share the visited HashSet among them.

[Sam Ezeh]

David Renshaw said:

My initial reaction is: it would be nice to avoid the need for ref cells.

I believe it's possible for fvars to be shared among multiple subgoals being operated on by the allGoals combinator, and I think that we typically want distribNot to act on all of the hypotheses of these subgoals. So it seems potentially problematic to share the visited HashSet among them.

Oh I see! I had a look at the comment on GitHub and I agree, there is no point in sharing the visited hash set. I was also worried about introducing a regression but as you noted, mathlib3 simply failed on that case anyway so that's not an issue.

[Sam Ezeh]

Should I submit a PR with your solution?

[David Renshaw]

Sounds good to me!

[Sam Ezeh]

Using this example

import Mathlib.Data.Part

open Part

theorem mem_restrict (p : Prop) (o : Part α) (h : p → o.Dom) (a : α) :
    a ∈ restrict p o h ↔ p ∧ a ∈ o := by
  dsimp [restrict, mem_eq]
  tauto

I get the following error when using the new tauto

/-
  don't know how to synthesize placeholder
  context:

  α: Type u_1
  p: Prop
  o: Part α
  h: p → o.Dom
  a: α
  em✝: (a : Prop) → Decidable a
  ⊢ (∃ (h_1 : p), o.get _ = a) ↔ p ∧ ∃ (h : o.Dom), o.get h = a
  -/

This really confused me because I would've expected it to act as any other error and iterateUntilFailure continues to succeed and I don't understand how throwing an error in replace causes issues with synthesis. After poking around at the code I was able to get the synthesis issue by throwing an error in replace but it only occurs when I also call g.replace. I tried the trySynthInstanceQ and working by cases on the Option type it returns but the tauto' tactic still fails with the same synthesis issue. What's going on here?

[Sam Ezeh]

Another thing is that CI still passed despite this, would it be worth adding a test case for this somewhere? If so, how would I go about doing this in Mathlib?

[Sam Ezeh]

So this diff is enough to cause it

diff --git a/Mathlib/Tactic/Tauto.lean b/Mathlib/Tactic/Tauto.lean
index a61841c23a..19d211fdd7 100644
--- a/Mathlib/Tactic/Tauto.lean
+++ b/Mathlib/Tactic/Tauto.lean
@@ -25,7 +25,10 @@ def distribNotOnceAt (hypFVar : Expr) (g : MVarId) : MetaM AssertAfterResult :=
   let .fvar fvarId := hypFVar | throwError "not fvar {hypFVar}"
   let h ← fvarId.getDecl
   let e : Q(Prop) ← (do guard <| ← Meta.isProp h.type; pure h.type)
-  let replace (p : Expr) := g.replace h.fvarId p
+  let replace (p : Expr) := do
+    let _ ← g.replace h.fvarId p
+    throwError "always fails"
+
   match e with
   | ~q(¬ ($a : Prop) = $b) => do
     let h' : Q(¬$a = $b) := h.toExpr

[David Renshaw]

Huh, weird.
This seems to fix it:

diff --git a/Mathlib/Tactic/Tauto.lean b/Mathlib/Tactic/Tauto.lean
index 9e6e61e026..2fa55ba8d9 100644
--- a/Mathlib/Tactic/Tauto.lean
+++ b/Mathlib/Tactic/Tauto.lean
@@ -26,10 +26,13 @@ def distribNotOnceAt (hypFVar : Expr) (g : MVarId) : MetaM AssertAfterResult :=
   let h ← fvarId.getDecl
   let e : Q(Prop) ← (do guard <| ← Meta.isProp h.type; pure h.type)
   let replace (p : Expr) : MetaM AssertAfterResult := do
+     let s ← saveState
      let result ← g.replace h.fvarId p
      result.mvarId.withContext do
      if (← getLCtx).contains h.fvarId
-     then throwError "'replace' did not remove the existing hypothesis"
+     then
+       s.restore
+       throwError "'replace' did not remove the existing hypothesis"
      pure result

   match e with

[David Renshaw]

... but I don't yet have a good understanding of why the explicit save/restore is needed. I had thought that the exception handling would take care of the necessary rollback.

[David Renshaw]

I made a little example program to test my understanding:

import Lean

open Lean Meta Elab.Tactic

syntax (name := foo) "foo" : tactic

elab_rules : tactic
| `(tactic| foo) => do
  let g ← getMainGoal
  try
    g.assign (mkNatLit 1)
    throwError "oops!"
  catch _ =>
    if ←g.isAssigned
    then throwError "oh no!"
    g.assign (mkNatLit 2)
  pure ()

def x : Nat := by foo

#print x
-- 2

[David Renshaw]

and that works like I expected -- the throwError rolls back the g.assign

[David Renshaw]

so I still don't understand why the saveState and s.restore seem to be needed in the proposed tauto fix.

[Thomas Murrills]

I think the issue is with liftMetaTactic:

import Lean

open Lean Meta Elab.Tactic

syntax (name := foo) "foo" : tactic

elab_rules : tactic
| `(tactic| foo) => liftMetaTactic fun g => do
  try
    g.assign (mkNatLit 1)
    throwError "oops!"
  catch _ =>
    if ← g.isAssigned then throwError "oh no!"
    g.assign (mkNatLit 2)
  pure []

def x : Nat := by foo -- oh no!

#print x
-- 1

I wonder if this is related to lean4#3001 (though I haven’t checked that that instance is actually relevant here).

[David Renshaw]

Ah, good find.

[David Renshaw]

@Thomas Murrills do you agree that this seems like a bug?

[Thomas Murrills]

Absolutely!

[Thomas Murrills]

Actually, this seems like a problem with theMetaM tryCatch instance somehow.

import Lean

open Lean Meta Elab.Tactic

def x : MVarId → MetaM Unit
| g => do
  try
    g.assign (mkNatLit 1)
    throwError "oops!"
  catch _ =>
    if ← g.isAssigned then throwError "oh no!"
    g.assign (mkNatLit 2)

#eval show MetaM _ from do -- oh no!
  let a ← mkFreshExprMVar (Expr.const ``Nat [])
  x a.mvarId!

[Thomas Murrills]

(no liftM in sight)

[David Renshaw]

trying to unravel this MonadExcept / MonadExceptOf stack of instances has me like :face_with_spiral_eyes:

[Thomas Murrills]

Ooh, take a look at #general > try, salvage, catch ; that’s not directly useful per se, but involved unraveling that stack!

[Thomas Murrills]

It goes all the way down to EStateM under EIO.

[Thomas Murrills]

I think there’s a special tryCatch for TacticM and CoreM, but iirc the rest are in terms of monad transformers.

[David Renshaw]

is it possible that the special TacticM is specifically adding the save/restore behavior, and MetaM is not getting it (perhaps even intentionally)?

[Thomas Murrills]

Yes, I think it’s quite possible that the “right” behavior is from the special TacticM restore used in its tryCatch. But I would doubt it’s intentional…

[Thomas Murrills]

I’m suspicious of the MonadExceptOf instance for StateRefT' in Init.Control.StateRef, as MetaM uses a StateRefT' to store the MetavarContext…

[David Renshaw]

where is StateRefT defined? When I jump to definition it takes me to StateRefT'.

[David Renshaw]

oh.. it's a macro (unclear where it's defined, but maybe not important)

[David Renshaw]

The EST monad does not implement try/catch backtracking:

import Lean

open Lean Meta Elab.Tactic Elab.Command
#eval show MetaM Unit from do
  let x := runEST (ε := String) fun σ ↦ do
    let r : ST.Ref σ Nat ← ST.mkRef 0
    try
      r.set 1
      throw "boom"
    catch _ =>
      dbg_trace ←r.get   -- prints "1"
      r.set 2
  dbg_trace x
  pure ()

[David Renshaw]

... and that seems reasonable to me.

[David Renshaw]

I suppose that the reason I expect MetaM try/catch to backtrack the Meta state is that TacticM does it, and TacticM is "just" a wrapper of MetaM.

[Thomas Murrills]

I’d expect it to backtrack even here—but I don’t necessarily know what other languages do with ST. In general I’d expect try/catch to always backtrack, or at the very least to have consistent behavior across monads.

[Thomas Murrills]

I think either

1. we should fix these Ref-related tryCatch instances so that they backtrack (like everything else)
2. we should ensure that all of Lean’s nongeneric monads (MetaM, TermElabM, etc.) backtrack under tryCatch (and ideally MonadControl)

[Mario Carneiro]

Thomas Murrills said:

I’d expect it to backtrack even here—but I don’t necessarily know what other languages do with ST. In general I’d expect try/catch to always backtrack, or at the very least to have consistent behavior across monads.

try catch generally does not backtrack in lean, this is what MonadBacktrack is for. The reason for this is because backtracking state involves overhead which you don't want to pay unless you know that it will be needed, so doing this by default in all state monads would cause performance issues when using lean's many linear data structures

[Mario Carneiro]

It would be lovely to have some kind of explicit opt in backtracking try/ catch though, rather than having to save and restore the state manually, which is error prone

[David Renshaw]

@Mario Carneiro if I'm working in a monad M, is there an easy way to look up whether try/catch in M will backtrack or not?

[David Renshaw]

I'm trying to do #synth MonadBacktrack TacticM, but it's not working

[Mario Carneiro]

docs#Lean.MonadBacktrack

[Mario Carneiro]

... you know the "instances" list in doc-gen would be a lot nicer if it showed the types rather than the names of the instances

[David Renshaw]

yeah, that gives me a list of instances, but I don't see TacticM in there, so presumably it comes from some monad tranformer instance

[David Renshaw]

oh, wait maybe it is there, just with an enormous obfuscated name

[David Renshaw]

Mario Carneiro said:

docs#Lean.MonadBacktrack

The way we are manually backtracking in mathlib4#11799 is by calling MonadBacktrack.saveState. So I don't see how MonadBacktrack can also be the marker for "this monad automatically backtracks in try/catch".

[Mario Carneiro]

it's not, it's the interface for manually backtracking

[Mario Carneiro]

the marker for "automatically backtracks" AFAIK is nothing because nothing does that

[Mario Carneiro]

...although now that I come to think of it some OrElse instances backtrack

[Mario Carneiro]

it's probably in need of a proper census to find out how inconsistent things actually are

[David Renshaw]

Restating my question: what piece of documentation tells me that TacticM does try/catch backtracking and MetaM does not?

[David Renshaw]

It seems the answer is "none".

[Mario Carneiro]

the answer is "look at the code"

[Mario Carneiro]

aka "none"

[David Renshaw]

and that's really difficult because of the layers of monad transformer indirection!

[Mario Carneiro]

well on the flip side that's good because there are only a few monad transformer primitives to look at

[Mario Carneiro]

Looks like the implementation of tryCatch on EStateM uses tricky typeclass machinery such that it backtracks only if there is a Backtrackable instance available, see src#EStateM.nonBacktrackable

[Mario Carneiro]

TacticM also has a special case MonadExcept instance, but not MonadExceptOf, which means that tryCatch and tryCatchThe behave differently...

[Mario Carneiro]

the monad instance for StateT (src#StateT.instMonadExceptOfStateT) appears to use the state nonlinearly, which seems like a bug, but is also AFAICT the only thing you could write for that instance. It seems like this means StateT will always backtrack everything, even if the state is not backtrackable?

[Mario Carneiro]

by contrast, the monad instance for StateRefT' (src#StateRefT'.instMonadExceptOfStateRefT'), despite using basically the same code, will not backtrack thanks to the magic of IO refs

[Mario Carneiro]

So it looks like the conclusion is:

Does it automatically backtrack on tryCatch?

• StateT: yes
• StateRefT': no
• EStateM: only if the state is Backtrackable. Is it backtrackable?
  • no (why does this class even exist then?)
• TacticM: yes

All of the special case instances except MonadExcept TacticM don't change the backtracking behavior

Does <|> backtrack:

• MetaM: yes
• Parser: it's complicated
• FormatterM / ParenthesizerM: yes
• otherwise: it's the same as try catch, see above

[Mario Carneiro]

in summary, state tracked in StateT generally backtracks, while state in StateRefT' doesn't, and most lean monads store all the state in StateRefT' or EStateM and so most of the state is not automatically backtracked. <|> is more likely to backtrack than try catch. Should this be documented more explicitly? Absolutely.

[Mario Carneiro]

this is an API mismatch between StateT and StateRefT that I had not previously realized

[Thomas Murrills]

This is a massive footgun, right? I’m not sure documentation alone would prevent the footgun from going off. Shouldn’t all try/catch uses behave the same (one way or another) with respect to backtracking, just as a matter of, well, good UX? Otherwise, you need to think about the details of each monad you’re in, and therefore about which lift you use—and a big part of the usefulness of lifts is that you don’t really have to think about them.

Likewise, if you know a monad you’re using has state, now you need to look at the (extrinsic) implementation details of that state to know what your code means, even though the interaction with that state uses the same API (or API which obscures how the state is implemented).

I think (but am ultimately guessing) that many people would expect state to be rewound by try/catch, and that not doing so is a footgun (less so if it were uniformly not rewound, but a footgun nonetheless).

So, my (ideal-world) proposal would be to uniformly backtrack state with try, with an opt-in non-backtracking try variant (try!? or simply do … catch?), for when you’re sure you want to prioritize optimization over intuitive semantics. Since it’s the less intuitive/more finicky thing, my thinking is that it’s better for non-backtracking to be the one to require the deliberate opt-in.

My not-quite-as-ideal-but-still-better-world proposal would be to use backtracking by default in try/catch in all of the major Lean monads—MetaM should work like TacticM and CoreM, etc.

[Mario Carneiro]

Otherwise, you need to think about the details of each monad you’re in, and therefore about which lift you use—and a big part of the usefulness of lifts is that you don’t really have to think about them.

Lifts don't really change things here. What matters is what kind of state it is, i.e. whether the state in the monad is being tracked via the StateT part of your monad transformer stack or a StateRefT part. Lifts will not move state from one slot to another. So I think it's okay that the answer is "it's monad dependent, but the monad author has made choices about what should be persisted and what hasn't, hopefully in a way that makes sense"

[Mario Carneiro]

That is, for a given piece of lean state like the MetavarContext, you can ask whether it is persisted or not in every monad which has one of these things and get a consistent answer. (Spoiler, it is backtracked by <|> and not by try catch.)

[Thomas Murrills]

Hmm, it’s my opinion that you should not have to ask about the implementation details of the state to know the semantics of try/catch. If you want something to behave differently, I think there should be different API.

Also, here, lifts did move state from one slot to another because of TacticM’s custom tryCatch! So, more narrowly, I at least think the core Lean monads should behave consistently with respect to each other.

[Mario Carneiro]

well in any case I can't do much about it

[Mario Carneiro]

take it up with core if you want to fight that battle

[Mario Carneiro]

I can't even imagine how much code would have to be reviewed after a change of that magnitude

[Thomas Murrills]

Haha, yeah, I am just speaking in principle, not at you directly :)

[Thomas Murrills]

When I’ve got a bit of time, I think I’ll ask in #lean4 for opinions on at least the core monad issue, and in the meantime, I’ll see if I can help out with documentation. That would certainly be better than nothing! :)

[Mario Carneiro]

maybe if you add docs you can highlight how inconsistent the behavior is without saying anything directly :)