Persisting hypotheses across tactics

Stream: metaprogramming / tactics

[Damiano Testa]

This is not a well-defined question, but I hope that it is specific enough that maybe it can receive some useful comments.

For the purpose of this question, you can limit the set of existing tactics to just simp, rw and have.

When looking at a proof in the infoview, you get the impression that (most) tactics preserve almost all the context and typically modify one location (or an explicit subset of locations in the case of tac at loc1 ... locn).

From this perspective, it seems straightforward to "track" locations, e.g. persisting the ones on which simp acted at some point during the proof.

While this heuristic idea is "visually" correct, there are several issues with it:

• the name of the location can become inaccessible (e.g. have h : ... makes a previous h change its username);
• the fvarid of a local declaraction can change (e.g. rw at h substitutes h with a new local declaration with the same username, but different fvarid);
• in the presence of several concurrent goals, the actual metavariables change name after most tactics act on them.

Thus, tracking in practice a location is very tricky.

My question is: is there some API around this?

[Damiano Testa]

My motivation comes from trying to write a version of the "non-terminal simp" linter that would flag non-robust proofs.

[Jannis Limperg]

Tracking lctx changes is a very annoying problem for which I haven't found a good solution yet. There are two approaches:

• Identify hyps by user name. But as you say, this is not guaranteed to be unique or stable. However, if you work with a predetermined set of tactics (which you probably don't), then this can be a good option.
• Identify hyps by unique name (FVarId). But as you say, these change all the time:
  • When the type or value of a hyp is changed in a non-defeq way, the FVarId must change, even if the hyp retains the same user name and users would probably view it as "the same hyp, only modified".
  • Otherwise (even when nothing happens to the hyp), the FVarId may still change. revert-based tactics do this a lot. In cases like these, the MetaM tactic sometimes returns a docs#Lean.Meta.FVarSubst which maps old FVarIds to new FVarIds. But not all MetaM tactics report such substitutions, and when you operate at elaborator level and above, you're probably out of luck entirely.

So yeah, it's tricky. :(

[Damiano Testa]

Ok, thank you for confirming that I am not reinventing some tools that already exist.

I'm going to record both the FVarId and the username and first scan the local contexts for the FVarId and fall back on the username if that fails.

[Kyle Miller]

Tactics are supposed to record a ofFVarAliasInfo in the info trees to connect up fvars

[Kyle Miller]

That tracking is used for the unused variable linter and the "find references" editor feature for example.

[Damiano Testa]

docs#Lean.Elab.Info.ofFVarAliasInfo
docs#Lean.Elab.FVarAliasInfo

[Damiano Testa]

Thanks, Kyle! I'll experiment with this!

[Damiano Testa]

Kyle, I tried your suggestion, but trying this on a few "random" proofs, I could find Info with the following constructors:

CommandInfo
CompletionInfo
MacroExpansionInfo
TacticInfo
TermInfo
OptionInfo
FieldInfo

This means that

UserWidgetInfo
CustomInfo
FVarAliasInfo
FieldRedeclInfo
OmissionInfo

appear very rarely (and actually never in the sample of files that I scanned).

[Mario Carneiro]

What proofs did you look at? Obviously the info nodes that appear depend on the proof

[Damiano Testa]

I opened a few random files (Data.Int.Lemmas, LinearAlgebra.Determinant, RingTheory.Algebra.Flat according to my VSCode history) and I collected all the Infos that I could see in those proofs.

[Damiano Testa]

In particular, I could find no appearance of FVarAliasInfo, that I hoped would help with "persisting" hypotheses, as per Kyle's comment above.

[Mario Carneiro]

you should look at proofs that involve fvar changing, of course. That description is a bit generic, it's hard to tell if you actually saw something. For example proofs by induction on List will surely have this behvior

[Damiano Testa]

Ok, but the reason for looking for them was to help with persisting hypotheses, so the fact that they did not show up in those files makes me think that FVarAliasInfo will not actually be useful for this purpose.

[Kyle Miller]

Maybe in each of those files, incidentally the fvarId is always preserved across all tactics?

[Damiano Testa]

I doubt it, since I'm pretty sure that there were rws.

[Damiano Testa]

Indeed, here is a rw in the determinant file.

And a rw at here.

[Kyle Miller]

docs#Lean.Elab.Tactic.rewriteLocalDecl uses docs#Lean.MVarId.replaceLocalDecl, which creates a docs#Lean.Meta.AssertAfterResult that contains the fvarsubst, but that's never registered as alias info, and, curiously, that never seems to lead to an accidental "unused variable" linter error.

[Kyle Miller]

It does keep "go to definition" from working on the variable afterwards.

But... maybe it's not the "same" variable after a rewrite, so perhaps it makes no sense to register an alias.

[Damiano Testa]

Ok, thank you for investigating! For my application, I definitely want to consider the "new" local fvar after a rw at or simp at as "the same" as the one before the tactic. Indeed, the idea is precisely to catch uses of a tactic like rw after a tactic like simp, but only when acting on "the same" hypothesis. Thus, I want to flag

  simp at h
  rw [] at h

but not

  simp at h
  rw [] at h'

(assuming that the arguments to rw do not involve h and that h and h' are really different!)

[Damiano Testa]

Maybe I can simply record the FVarIds after tactics like simp and match them to the FVarIds before tactics like rw and forget about actually evolving/tracking them. However, I worry that, when the "context MVar" changes, these FVarIds are not preserved.