progress on fail_if_no_progress

Stream: mathlib4

[Thomas Murrills]

I'm (finally!) taking a look again at #3757. :) I've revamped what I think the config ought to look like in the spirit of providing all knobs you might want, in part informed by what I think a generic configurable equality assertion ought to look like—though I'm doing this "by hand" instead of attempting to actually produce something general, since it's probably more important to get it working first and then take care of the general case, rather than the other way around! (Though I would like to address the general case here at some point! I have some ideas if anyone's curious.)

In part, I'm trying to make it more natural to write your own bespoke FailIfNoProgress.Config instance by propagating defaults down from global settings, as per #lean4 > Inheriting defaults from parent structures .

I need to tweak and fill out the actual implementation to match the new configs, but this should be mostly mechanical; then more docstrings are needed, which is again straightforward. I'd also like to rewrite some of the code in that PR, as it looks quite a bit worse now than it did then...though I'm told that's a common experience :)

[Thomas Murrills]

I'll ask a couple miscellaneous questions in this thread as I try to finish it up! @Scott Morrison and @Alex J. Best, I hope to have it cleaned up enough to be commentable-on (comment-on-able?) in a day or two if you're interested (though my current circumstances are a bit volatile when it comes to being sure of such a thing); or, if there are obvious tasks either of you would like to address there, please feel free. :)

Here's one such misc. question: I have functions zip?, zipM?, zipWith?, zipWithM?, zipWithFold?, and zipWithFoldM? which return none if the lengths of the lists don't match. The relevance here is that we ought to check that the lengths of two lists (of e.g. goals or hypotheses) which we're comparing match before we actually start comparing the elements. Besides the fact that I think a couple of them weren't implemented correctly back then (oops!), (1) do these exist somewhere and (2) if not, where should they go? They seem more general than fail_if_no_progress.

[Scott Morrison]

I doubt these exist. It's not obvious to me that an Option valued version of zip is the right answer here, however.

Why not just separately compare the lengths, before ever looking at the zip? If the length don't match we can just terminate, as clearly the goal has changed by any of the standards.
We're just comparing things like lists of hypotheses here, so there is no performance issue to worry about.

If there were a reason for a richer version of zip, maybe something like zipWithLeftovers : List α → List β → List (α × β) × List α × List β (possibly an ⊕ at the end there?) would be the right answer. You can match on it to detect whether the lists had different lengths. I don't like the Option valued alternative because it is throwing away some but not all of the additional information available beyond zip, and it seems overly specific.

[Kyle Miller]

Related are docs#List.zipWithLeft and docs#List.zipWithRight (and docs#List.zipLeft and docs#zipRight). List.zipWithLeftovers and a corresponding List.zipLeftovers seem like they'd be a nice addition (modulo the names, since With implies there's a function being mapped over the zipping, and List.zipLeftovers isn't so descriptive on its own)

[Scott Morrison]

zipAndTail(s)?

[Thomas Murrills]

plus, zipLeftovers implies the existence of zipRightovers :)

[Thomas Murrills]

also it’s a moot point, but just curious, what did you mean by throwing away some but not all of the information available beyond zip? Wouldn’t we be throwing it all away?

[Yakov Pechersky]

In python, it's called zip_longest

[Scott Morrison]

Thomas Murrills said:

also it’s a moot point, but just curious, what did you mean by throwing away some but not all of the information available beyond zip? Wouldn’t we be throwing it all away?

zipwithTail : List α → List β → List (α × β) × (List α ⊕ List β) is (EDIT: err, not quite...) an isomorphism from the inputs to the output. zip throws away "everything" except the List (α × β) part, while your zip? throws away everything except whether one of the two tails is non-empty. The fact that there are several intermediate options between zipWithTail and zip besides zip? made me dubious that any of them were generally useful.

[Thomas Murrills]

Ok, #3757 essentially passes CI, besides a build-trivial refactor passes CI and is out for review! A couple finishing review questions that I can think of right now:

[Thomas Murrills]

• I introduce the obvious instance for BEq MetavarKind by hand. Is there a better way of doing this? Or a better location? (Should I or someone else even PR lean4 so that inductive MetavarKind is deriving ... DecidableEq?)

[Thomas Murrills]

• The last three commits refactor the comparison machinery to a new file, since it seemed a bit crowded in FailIfNoProgress.lean, and the content could serve an independent purpose. That is, it seems like a single "functional unit" not specific to fail_if_no_progress, and imo makes the files and logic cleaner if it's an import. But, it's only used in fail_if_no_progress at the moment, so I'm not sure if it should really be split off. Yea or nay? (I can simply revert if nay.)

[Jannis Limperg]

I really like the gist of this PR, and I agree that the comparison functions are more widely applicable and should live in their own files. I have two questions about the functionality:

• Would it be possible to get a mode which ignores changes to FVarIds? That is, fvars at the same position in the context with the same type should be considered the same, even if they have different FVarIds. Rationale: FVarIds are an implementation detail and only affect the respective goal. Use case: a tactic which uses the revert-intro trick, but then ends up not doing anything between revert and intro, changes all the FVarIds but has not made progress.
• Would it be possible to get a mode which checks whether mvars occurring in the goal are the same, even if they have different MVarIds? The difficulty with this is that we still want to ensure that if an mvar appears multiple times in the same goal, its equivalent in the other goal also occurs in the same positions. Not sure if this is relevant for fail_if_no_progress; if not, it probably shouldn't be part of this PR.

[Thomas Murrills]

Nice! :)

• Yes, it is! The basic version of this is the default—this is checkFVarId := false in LocalDeclComparisonConfig. However, this doesn't do the analogous thing you're suggesting for MVarIds, i.e. consider equivalent FVarIds to be equivalent when they appear in subsequent expressions. And on that note:
• Hmm—I'd definitely be interested in doing this (and likewise for FVarIds), and I think it is relevant to fail_if_no_progress! But it might be worth splitting it into a separate PR, as it breaks the (current) modularity of the implementation and would probably be worthy of review by itself. That would probably necessitate keeping track of the MVarIds and FVarIds that were taken to be equivalent, and then replacing them in each type expression we encountered when we compare them.

This sort of flow would also be more efficient! Currently, we check each component against each other component in sequence, when we really ought to defer all the potentially-expensive isDefEq checks until the end, to see if the easier-to-check properties are sufficient for distinguishing our two states. But being able to defer checks would complicate the types of the comparison functions (or have us introduce primed versions of each comparison def which could defer checks). Or maybe we could just pass all the equivalence info from previous hypotheses/goals as arguments to the comparison functions without changing the return types—that would be less efficient, but probably easier and cleaner type-wise. (Or maybe there's an implementation involving Task, which I don't know anything about yet, but the name sounds possibly relevant.)

[Jannis Limperg]

I dug up my implementation. It's more lengthy than I thought... (In fact, it doesn't quite fit into a Zulip message.)

import Std.Lean.Meta.SavedState

open Lean Lean.Meta

namespace Aesop

-- TODO caching -- but maybe the ptrEq optimisation is enough

namespace EqualUpToIdsM

structure Context where
  commonMCtx : MetavarContext
  mctx₁ : MetavarContext
  mctx₂ : MetavarContext

structure State where
  equalMVarIds : HashMap MVarId MVarId := {}
  equalLMVarIds : HashMap LMVarId LMVarId := {}
  equalFVarIds : HashMap FVarId FVarId := {}

end EqualUpToIdsM


abbrev EqualUpToIdsM :=
  ReaderT EqualUpToIdsM.Context $ StateRefT EqualUpToIdsM.State MetaM

-- Make the compiler generate specialized `pure`/`bind` so we do not have to optimize through the
-- whole monad stack at every use site. May eventually be covered by `deriving`.
@[inline, always_inline]
instance : Monad EqualUpToIdsM :=
  { inferInstanceAs (Monad EqualUpToIdsM) with }

protected def EqualUpToIdsM.run (x : EqualUpToIdsM α)
    (commonMCtx mctx₁ mctx₂ : MetavarContext) :
    MetaM α :=
  (·.fst) <$> (x { commonMCtx, mctx₁, mctx₂ }).run {}

namespace Unsafe

mutual
  unsafe def levelsEqualUpToIdsCore (l₁ l₂ : Level) : EqualUpToIdsM Bool :=
    if ptrEq l₁ l₂ then
      return true
    else
      levelsEqualUpToIdsCore' l₁ l₂

  unsafe def levelsEqualUpToIdsCore' : Level → Level → EqualUpToIdsM Bool
    | .zero, .zero => return true
    | .succ l₁, .succ l₂ => levelsEqualUpToIdsCore l₁ l₂
    | .max l₁ m₁, .max l₂ m₂ =>
      levelsEqualUpToIdsCore l₁ l₂ <&&> levelsEqualUpToIdsCore m₁ m₂
    | .imax l₁ m₁, .imax l₂ m₂ =>
      levelsEqualUpToIdsCore l₁ l₂ <&&> levelsEqualUpToIdsCore m₁ m₂
    | .param n₁, .param n₂ => return n₁ == n₂
    | (.mvar m₁), l₂ => compareMVar (swap := false) m₁ l₂
    | l₁, (.mvar m₂) => compareMVar (swap := true)  m₂ l₁
    | _, _ => return false
  where
    @[inline, always_inline]
    go (swap : Bool) (l₁ l₂ : Level) : EqualUpToIdsM Bool :=
      if swap then
        levelsEqualUpToIdsCore l₂ l₁
      else
        levelsEqualUpToIdsCore l₁ l₂

    @[inline, always_inline]
    checkMVarEquality (m₁ m₂ : LMVarId) : EqualUpToIdsM Bool := do
      let commonMCtx := (← read).commonMCtx
      if commonMCtx.lDepth.contains m₁ || commonMCtx.lDepth.contains m₂ then
        return m₁ == m₂
      if let some m₂' := (← get).equalLMVarIds.find? m₁ then
        return m₂' == m₂
      else
        modify λ s => { s with equalLMVarIds := s.equalLMVarIds.insert m₁ m₂ }
        return true

    @[specialize]
    compareMVar (swap : Bool) (m₁ : LMVarId) (l₂ : Level) :
        EqualUpToIdsM Bool := do
      if let some l₁ ← getLevelMVarAssignment? m₁ then
        go swap l₁ l₂
      else if let .mvar m₂ := l₂ then
        if let some l₂ ← getLevelMVarAssignment? m₂ then
          go swap (.mvar m₁) l₂
        else if swap then
          checkMVarEquality m₂ m₁
        else
          checkMVarEquality m₁ m₂
      else
        return false
end

end Unsafe

@[implemented_by Unsafe.levelsEqualUpToIdsCore]
opaque levelsEqualUpToIdsCore (l₁ l₂ : Level) : EqualUpToIdsM Bool

private def namesEqualUpToMacroScopes (n₁ n₂ : Name) : Bool :=
  n₁.hasMacroScopes == n₂.hasMacroScopes &&
  n₁.eraseMacroScopes == n₂.eraseMacroScopes

private def lctxDecls (lctx : LocalContext) : Array LocalDecl :=
  lctx.foldl (init := Array.mkEmpty lctx.numIndices) λ decls d => decls.push d

structure GoalContext where
  mdecl₁ : MetavarDecl
  mdecl₂ : MetavarDecl
  equalFVarIds : HashMap FVarId FVarId := {}

namespace Unsafe

mutual
  unsafe def localDeclsEqualUpToIdsCore :
      LocalDecl → LocalDecl → ReaderT GoalContext EqualUpToIdsM Bool
    | .cdecl _ _ userName₁ type₁ bi₁ kind₁,
      .cdecl _ _ userName₂ type₂ bi₂ kind₂ =>
      pure (namesEqualUpToMacroScopes userName₁ userName₂ &&
            bi₁ == bi₂ && kind₁ == kind₂) <&&>
      exprsEqualUpToIdsCore type₁ type₂
    | .ldecl _ _ userName₁ type₁ v₁ _ kind₁,
      .ldecl _ _ userName₂ type₂ v₂ _ kind₂ =>
      pure (namesEqualUpToMacroScopes userName₁ userName₂ &&
            kind₁ == kind₂) <&&>
      exprsEqualUpToIdsCore type₁ type₂ <&&>
      exprsEqualUpToIdsCore v₁ v₂
    | _, _ => return false

  unsafe def exprsEqualUpToIdsCore (e₁ e₂ : Expr) :
      ReaderT GoalContext EqualUpToIdsM Bool := do
    if ptrEq e₁ e₂ then
      return true
    else
      exprsEqualUpToIdsCore' e₁ e₂

  unsafe def exprsEqualUpToIdsCore' :
      Expr → Expr → ReaderT GoalContext EqualUpToIdsM Bool
    | .bvar i, .bvar j => return i == j
    | .fvar fvarId₁, .fvar fvarId₂ =>
      return (← read).equalFVarIds.find? fvarId₁ == some fvarId₂
    | .sort u, .sort v => levelsEqualUpToIdsCore u v
    | .const decl₁ lvls₁, .const decl₂ lvls₂ =>
      return decl₁ == decl₂ && lvls₁ == lvls₂
    | .app f₁ x₁, .app f₂ x₂ =>
      exprsEqualUpToIdsCore f₁ f₂ <&&> exprsEqualUpToIdsCore x₁ x₂
    | .lam n₁ t₁ e₁ bi₁, .lam n₂ t₂ e₂ bi₂ =>
      pure (n₁ == n₂ && bi₁ == bi₂) <&&>
      exprsEqualUpToIdsCore t₁ t₂ <&&>
      exprsEqualUpToIdsCore e₁ e₂
    | .forallE n₁ t₁ e₁ bi₁, .forallE n₂ t₂ e₂ bi₂ =>
      pure (n₁ == n₂ && bi₁ == bi₂) <&&>
      exprsEqualUpToIdsCore t₁ t₂ <&&>
      exprsEqualUpToIdsCore e₁ e₂
    | .letE n₁ t₁ v₁ e₁ _, .letE n₂ t₂ v₂ e₂ _ =>
      pure (n₁ == n₂) <&&>
      exprsEqualUpToIdsCore t₁ t₂ <&&>
      exprsEqualUpToIdsCore v₁ v₂ <&&>
      exprsEqualUpToIdsCore e₁ e₂
    | .lit l₁, .lit l₂ => return l₁ == l₂
    | .mdata _ e₁, e₂ => exprsEqualUpToIdsCore e₁ e₂
    | e₁, .mdata _ e₂ => exprsEqualUpToIdsCore e₁ e₂
    | .proj n₁ i₁ e₁, .proj n₂ i₂ e₂ =>
      pure (n₁ == n₂ && i₁ == i₂) <&&> exprsEqualUpToIdsCore e₁ e₂
    | .mvar m₁, e₂ => compareMVar (swap := false) m₁ e₂
    | e₁, .mvar m₂ => compareMVar (swap := true)  m₂ e₁
    | _, _ => return false
  where
    @[inline, always_inline]
    go (swap : Bool) (e₁ e₂ : Expr) : ReaderT GoalContext EqualUpToIdsM Bool :=
      if swap then
        exprsEqualUpToIdsCore e₂ e₁
      else
        exprsEqualUpToIdsCore e₁ e₂

    @[inline, always_inline]
    checkMVarEquality (m₁ m₂ : MVarId) : EqualUpToIdsM Bool := do
      let commonMCtx := (← read).commonMCtx
      if commonMCtx.decls.contains m₁ || commonMCtx.decls.contains m₂ then
        return m₁ == m₂
      else if let some m₂' := (← get).equalMVarIds.find? m₁ then
        return m₂' == m₂
      else if ← mvarIdsEqualUpToIdsCore m₁ m₂ then
        modify λ s => { s with equalMVarIds := s.equalMVarIds.insert m₁ m₂ }
        return true
      else
        return false

    @[specialize]
    compareMVar (swap : Bool) (m₁ : MVarId) (e₂ : Expr) :
        ReaderT GoalContext EqualUpToIdsM Bool := do
      if let some e₁ ← getExprMVarAssignment? m₁ then
        go swap e₁ e₂
      else if let .mvar m₂ := e₂ then
        if let some e₂ ← getExprMVarAssignment? m₂ then
          go swap (.mvar m₁) e₂
        else if swap then
          checkMVarEquality m₂ m₁
        else
          checkMVarEquality m₁ m₂
      else
        return false

  unsafe def mvarIdsEqualUpToIdsCore (mvarId₁ mvarId₂ : MVarId) :
      EqualUpToIdsM Bool := do
    let gctx ← read
    let (some mdecl₁) := gctx.mctx₁.decls.find? mvarId₁ | throwError
      "unknown metavariable '?{mvarId₁.name}'"
    let (some mdecl₂) := gctx.mctx₂.decls.find? mvarId₂ | throwError
      "unknown metavariable '?{mvarId₂.name}'"
    let decls₁ := lctxDecls mdecl₁.lctx
    let decls₂ := lctxDecls mdecl₂.lctx
    if decls₁.size != decls₂.size then
      return false

    let mut gctx : GoalContext := { mdecl₁, mdecl₂ }
    for ldecl₁ in decls₁, ldecl₂ in decls₂ do
      if ! (← localDeclsEqualUpToIdsCore ldecl₁ ldecl₂ |>.run gctx) then
        return false
      else
        let equalFVarIds := gctx.equalFVarIds.insert ldecl₁.fvarId ldecl₂.fvarId
        gctx := { gctx with equalFVarIds }
    exprsEqualUpToIdsCore mdecl₁.type mdecl₂.type |>.run gctx
end

end Unsafe

@[implemented_by Unsafe.mvarIdsEqualUpToIdsCore]
opaque mvarIdsEqualUpToIdsCore (mvarId₁ mvarId₂ : MVarId) : EqualUpToIdsM Bool

def mvarIdsEqualUpToIds (commonMCtx mctx₁ mctx₂ : MetavarContext)
    (mvarId₁ mvarId₂ : MVarId) : MetaM Bool := do
  mvarIdsEqualUpToIdsCore mvarId₁ mvarId₂ |>.run commonMCtx mctx₁ mctx₂

def tacticStatesEqualUpToIds (commonMCtx mctx₁ mctx₂ : MetavarContext)
    (goals₁ goals₂ : List MVarId) : MetaM Bool := do
  if goals₁.length != goals₂.length then
    return false
  else
    for g₁ in goals₁, g₂ in goals₂ do
      if ! (← mvarIdsEqualUpToIds commonMCtx mctx₁ mctx₂ g₁ g₂) then
        return false
    return true

[Jannis Limperg]

open Lean.Elab.Tactic in
def assertEqualTactics (t₁ t₂ : TacticM Unit) : TacticM Unit := do
  let commonMCtx ← getMCtx
  let (state₁, goals₁) ← runTactic t₁
  let (state₂, goals₂) ← runTactic t₂
  let eq ←
    tacticStatesEqualUpToIds commonMCtx state₁.meta.mctx state₂.meta.mctx
      goals₁ goals₂
  if ! eq then
    throwError "Tactics produced different tactic states.\nTactic 1:{indentD $ ← ppTacticState state₁ goals₁}\nTactic 2:{indentD $ ← ppTacticState state₂ goals₂}"
where
  runTactic (t : TacticM Unit) : TacticM (Meta.SavedState × List MVarId) := do
    let s ← withoutModifyingState do t; saveState
    return (s.term.meta, s.tactic.goals)

  ppTacticState (state : Meta.SavedState) (goals : List MVarId) :
      MetaM MessageData :=
    state.runMetaM' do
      addMessageContext $ .joinSep (goals.map toMessageData) "\n"

open Lean.Elab.Tactic in
elab &"assert_equal_tactics "
    " { " ts₁:tacticSeq " } " " { " ts₂:tacticSeq " } " : tactic => do
  assertEqualTactics (evalTactic ts₁) (evalTactic ts₂)

example : True := by
  assert_equal_tactics { trivial } { trivial }
  trivial

example : True := by
  assert_equal_tactics { open Classical in trivial } { trivial }
  trivial

example (n m : Nat) : True := by
  fail_if_success assert_equal_tactics { cases n } { cases m }
  trivial

example : 0 < 3 := by
  apply Nat.lt_trans
  assert_equal_tactics { exact Nat.lt_succ_self 0 } { exact Nat.lt_succ_self 0 }
  (case m => exact 1); all_goals decide

example : 0 < 3 := by
  apply Nat.lt_trans
  assert_equal_tactics { apply Nat.lt_trans } { apply Nat.lt_trans }
  (case m => exact 1); all_goals decide

end Aesop

[Thomas Murrills]

Oh nice! :D That seems to use some neat low-level functionality I'm not yet familiar with—e.g., when exactly to use @[inline] or @[always_inline], what @[specialize] means, etc. (I keep meaning to dig a bit deeper on those.)

Would it be useful to pepper in ptrEq throughout the PR'd fail_if_no_progress in the way you've done here, or is that already taken care of by beq/isDefEq?

In the fail_if_no_progress context (which is a bit more general, I suppose) I wonder if it instead makes sense to traverse the expression and e.g. replace mvar1 with mvar2 in e₁ once they've been deemed equivalent, then compare this e₁' with e₂. That way, we get to use isDefEq if we like. Though I'm not sure how to handle different levels in that context...maybe they could be abstracted out into level mvars for isDefEq? For beq, maybe a more specific implementation like the one you have here would be useful. It might also be useful to simply use your implementation as a drop-in replacement for beq when ignoring id's (instead of traversing & replacing)!

[Jannis Limperg]

Thomas Murrills said:

Oh nice! :D That seems to use some neat low-level functionality I'm not yet familiar with—e.g., when exactly to use @[inline] or @[always_inline], what @[specialize] means, etc. (I keep meaning to dig a bit deeper on those.)

I'm mostly cargo-culting this stuff myself; haven't done any measurements. @[specialize] should be analogous to Haskell's {- SPECIALIZE -}, which, for a function with instance argument [C α], generates a specialized version of the function for each instance of C at which the function is used.

Would it be useful to pepper in ptrEq throughout the PR'd fail_if_no_progress in the way you've done here, or is that already taken care of by beq/isDefEq?

The core functions should already be using pointer equality where appropriate.

In the fail_if_no_progress context (which is a bit more general, I suppose) I wonder if it instead makes sense to traverse the expression and e.g. replace mvar1 with mvar2 in e₁ once they've been deemed equivalent, then compare this e₁' with e₂. That way, we get to use isDefEq if we like. Though I'm not sure how to handle different levels in that context...maybe they could be abstracted out into level mvars for isDefEq? For beq, maybe a more specific implementation like the one you have here would be useful. It might also be useful to simply use your implementation as a drop-in replacement for beq when ignoring id's (instead of traversing & replacing)!

For beq, you should probably use my code or something like it. That'll be more efficient than replacing mvars. (Also more complex though.) For isDefEq, I guess replacing mvars is the only practicable way.

[Alex J. Best]

BTW my impression was (though I could be wrong), that in Lean instance arguments were always considered for specialization by the compiler, so for lean it is mostly helpful when you have something higher order, like a function argument, but that isn't a typeclass.

[Jannis Limperg]

@Thomas Murrills I've now tested my equality checking algorithm and of course it turned out to be more than a little buggy. A new version is now in Aesop. This one is used all over the Aesop test suite, so I'm fairly confident that it is mostly correct.