aesop and bv_decide

Stream: lean4

[Jakob von Raumer]

I'm getting an error (kernel) unknown constant 'foo._expr_def_1' in this snippet:

lemma foo (a b : BitVec 128 × BitVec 128) (ρ : BitVec 128 × BitVec 128) :
    (∃ (ref3 ref4 ref5 ref6 : BitVec 128), (ref4.uaddOverflow ref6 ∧ ref3.uaddOverflow ref5 ∧
      ((ref4 + ref6).uaddOverflow 1#128))) → ρ = a + b := by
  aesop (add safe [(by bv_decide)])

Not sure if it's a bug in aesop or in bv_decide? @Henrik Böving @Jannis Limperg

[Henrik Böving]

bv_decide does create a definition with this name as an auxiliary constant but I don't understand why it should disappear again.

[Henrik Böving]

So I would expect it's in fact a combi bug^^

[Sebastian Ullrich]

Could be the environment replay, is it new in 4.19?

[Jakob von Raumer]

Yes it is

[Jakob von Raumer]

In a similar vein, I'm getting a (kernel) application type mismatch in an case where I'm using aesop (add safe [(by omega)])

[Jakob von Raumer]

Oh an bv_decide started leaving .lrat crumbs around

[Bhavik Mehta]

Jakob von Raumer said:

In a similar vein, I'm getting a (kernel) application type mismatch in an case where I'm using aesop (add safe [(by omega)])

There was previous discussion on this in #nightly-testing, putting omega in aesop doesn't currently work :(

[Jannis Limperg]

What's the current status of this replay/Aesop issue? I assume it's about replay not picking up auxiliary declarations generated by tactics. Is there a plan to fix this or do I need to work around it in Aesop (which would probably entail going back to the previous hack)?

[Kim Morrison]

I think you're the only user of replay at this point, besides lean4checker, so there's no plan to work on it (but conversely, if you want to propose changes that wouldn't break lean4checker, we can probably merge them).

[Jannis Limperg]

Okay. I hope I'll find time to look into it soon. The current situation, where a bunch of tactics are just broken in Aesop, is very suboptimal.

[Sebastian Ullrich]

A MWE (i.e. calling replay directly) would also be helpful!

[Jakob von Raumer]

(by grind) also causes errors (kernel) constant has already been declared '_grind._proof_8', not sure if they're also because of replay or just due to grinds name generation

[Sebastian Ullrich]

Ah, that indeed is a separate issue that suggests Aesop needs to manage the mkAuxLemma state to prevent such duplicate names

[Jannis Limperg]

I looked into this issue and the situation seems to be as follows (cc @Kim Morrison @Sebastian Ullrich):

• replay is innocent (except for some possible latent bugs below).
• The issue is with Term.mkAuxNameand mkAuxLemma. Both of these are used to register auxiliary constants that are then used in the main constructions of, e.g., bv_decide, grind and omega. The constants are generally named according to a scheme like <decl>._proof_<n>, where <decl> is the theorem we're currently proving and n is a counter that's used to ensure no name clashes.
• The auxiliary declarations are public (they can be referenced, e.g. with #check <decl>._proof_<n>), but unhygienic in the sense that their names are presumably considered unstable implementation details.
• In the context of Aesop, this is problematic because tactics can run in different branches of the search tree, so they don't see auxiliary declarations added by other tactics, leading to name clashes. E.g. one invocation of omega adds an auxiliary declaration <decl>._proof_0; another invocation of omega runs on a sibling branch and also adds <decl>._proof_0; once the branches are combined into the final proof, we get a name clash.
• This conceptual issue has been present basically forever, but is now surfacing because auxiliary declarations are increasingly used in core tactics.

Possible solutions:

• Names of auxiliary lemmas become private and globally unique. This would anyway be better from a hygiene perspective, but maybe there are issues with this that I'm not seeing.
• The environment allows me to 'reserve' names that Term.mkAuxName will then consider used. This would allow me to reserve names that were added on sibling branches. However, branches would become coupled, blocking any future attempt to parallelise Aesop. (For mkAuxLemma, I should be able to implement this solution with the existing API.)
• The environment allows me to register a 'branch name' that becomes part of the auxiliary names generated by Term.mkAuxName and mkAuxLemma. So the generated name would be something like <decl>._branch_<m>._proof_<n>.

Some possible latent bugs of replay that turned up during the investigation:

• In the Lean version I was looking at yesterday, setting the option Lean.Elab.async := false would prevent constants from showing up in asyncConsts, so replay would not pick them up. But this seems to have already changed on master.
• replayConsts only supports definition and theorem constants. I guess this is fine for leanchecker, but for the Aesop use case there's no conceptual reason to prevent tactics from adding axioms or inductives.

[Sebastian Ullrich]

Oh so the kernel error was from aux theorems with colliding names?

[Jannis Limperg]

Ah no, that seems to be a different bug. Investigating...

[Jannis Limperg]

@Sebastian Ullrich the bv_decide error does seem to be related to replay. MWE:

import Lean

open Lean Lean.Meta Lean.Elab.Tactic in
elab "replay" ts:tacticSeq : tactic => do
  let initEnv ← getEnv
  evalTactic ts
  let finalState ← saveState
  setEnv $ ← initEnv.replayConsts initEnv finalState.term.meta.core.env

-- (kernel) unknown constant 'test._expr_def_1'
theorem test
    (x y : BitVec 128) (h : y = x) : x = y := by
  replay bv_decide

[Sebastian Ullrich]

@Jannis Limperg Thanks, that was helpful! #8157

[Jannis Limperg]

Thank you! (lean4#8157)

[Jannis Limperg]

Does the core team have an opinion on the suggested solutions for the name clash issue? My preference is no. 3 (or the radical no. 1). I can make an RFC and/or talk to Leo about it on Thursday.

[Sebastian Ullrich]

I'm assuming we'll want a NameGenerator but I haven't asked others yet