substitute for `include/omit`?

Stream: lean4

[Damiano Testa]

In the process of porting a file that used include/omit, I found that it would have been useful to have some form of include/omit. I ended up creating sections with the appropriate assumptions, but it was a little tedious.

Below is an example of why this might be wanted.

class one (A : Type) where h : A → A
class two (A : Type) where h : A → A

instance [one A] : Neg A where neg := one.h
instance [two A] : Neg A where neg := two.h

variable {X} {a : X} [one X]

variable [two X]
example : one.h a = - a := rfl  -- comment `variable [two X]` to toggle which one of these
example : two.h a = - a := rfl  -- two examples works and which one fails

theorem which_one? : - a = - a := rfl
#check which_one?    --  Can I control which of `one A` or `two A` is used here?
                     --  Is it inevitably the last-defined instance?

(For completeness, the PR is !4#4293, but it is not easy to single out where the issue above arises.)

[Kevin Buzzard]

I think the party line is "you are not supposed to be in a situation where you need to control that". You want to control typeclass inference?

[Damiano Testa]

I would have preferred not to, but there were two different divs in the context and it was hard to get Lean to figure out which one was the correct one, until I sectioned it.

[Damiano Testa]

(At least, I think that this was the issue: what I know is that it got solved by the section.)

[Damiano Testa]

Anyway, this is a file defining the field of rational functions in one variable: it is quite possible that once the definitions are in, the no-longer-needed omit/include will indeed not be needed!

[Damiano Testa]

A small update on this issue and a potential warning.

While Yuri was porting FieldTheory.Laurent, he ran into issues that the typeclass assumptions of some of the lemmas in FieldTheory.RatFunc were not correct.

I take full responsibility for the mistakes! The reason that I did not realize this, while the PR was in progress, was that I blindly assumed that Lean would cherry-pick the correct typeclass assumptions that were available in context, just as they were intended to be selected. Of course, this was overly naïve on my part!

However, unlike autoImplicit, I do not know how to disable this self-selection of the relevant assumptions (maybe it is in fact impossible). The warning is: if in mathlib3 you felt inclined to avoid introducing sections and preferred to use include/omit, reconsider using sections in Mathlib4!

[Jireh Loreaux]

I think the recommended way to deal with this in Lean 4 is to explicitly include the typeclass arguments in the lemmas in question. But, can you provide an example of one of the offending lemmas? More context is always helpful.

[Eric Wieser]

There was another Zulip thread about thisl perhaps it should be linked here

[Damiano Testa]

Jireh, I tried (and failed) for quite a while to come up with a good example of a theorem with "fuzzy" assumptions and where Lean selects an unwanted subset. Right now, I think that the most solid confirmation is that !4#4512 fails, since "somewhere" in !4#4293 the wrong typeclass was selected. The relevant issue is #4513.
(And the first step towards a solution is, hopefully, #19133.)

[Jireh Loreaux]

Aha, in that case it seems the sectioning really is the correct approach.

[Jireh Loreaux]

I would advocate for never having "fuzzy" assumptions.

[Jireh Loreaux]

Even from a source code readability standpoint that seems hard to parse.

[Damiano Testa]

Jireh, I agree. In this case, I got lazy and decided to port directly instead of section-in-mathlib3-and-then-port. I was warning that the fast way might be the one that starts with sectioning!

[Damiano Testa]

In case people are interested, I decided to write the small tactic prune, similar to the clear... family.

prune clears, very conservatively, all hypotheses that are not "connected" to the goal.

import Std.Data.List.Basic

namespace Lean.Elab.Tactic

open Meta

def revertVarsOnce : TacticM (Array FVarId × List LocalDecl × MVarId) := focus do
  let ctx := (← getLCtx).decls.toList.reduceOption
  let gMVar := ← getMainGoal
  let goal := ← getMainTarget
  let foundDecls := (ctx.map fun x =>
    if x.toExpr.occurs goal then some x else none).reduceOption
  let fvarIdFound := (foundDecls.map Lean.LocalDecl.fvarId).toArray
  let (fvs, newGoal) := ← gMVar.revert fvarIdFound
  setGoals [newGoal]
  pure (fvs, ctx, newGoal)

partial
def revertLoop : TacticM (List LocalDecl × MVarId) := focus do
  let (fvars, ctx, newGoal) := ← revertVarsOnce
  if fvars.size == 0 then pure (ctx, newGoal) else revertLoop

def pruneTac : TacticM Unit := focus do
  let dcls := (← getLCtx).decls.toList.reduceOption
  dbg_trace dcls.length
  let goal := ← getMainGoal
  let newGoal ← goal.tryClearMany (dcls.map LocalDecl.fvarId).toArray
  setGoals [newGoal]
  let nms := (← getMainTarget).getForallBinderNames
  let (_newfvs, rGoal) := ← introNCore newGoal nms.length [] True True
  setGoals [rGoal]

elab "prune" : tactic => do
  let _ := ← revertLoop
  pruneTac

end Lean.Elab.Tactic

universe u
variable {α : Type u} [Add α] [Add α] {e f : α} {a b _d : Nat} {_h : e ≠ f} (h₁ : a = b) {c : Int}

example : a + 5 = c ∨ True := by
  prune
  /- goal state:
  b a: Nat
  h₁: a = b
  c: Int
  ⊢ Int.ofNat a + 5 = c ∨ True
  -/
  exact Or.inr trivial

/-- Lots of duplication of variables, since they are included *again*! -/
example {α : Type u} [Add α] [OfNat α 0] {e f : α} {a b _d : Nat} {_h : e ≠ f} (_h₁ : a = b)
  {_c : Int} : e + f = e ∨ True := by
  /- goal state:
  α✝: Type u
  inst✝³ inst✝²: Add α✝
  e✝ f✝: α✝
  a✝ b✝ _d✝: Nat
  _h✝: e✝ ≠ f✝
  h₁: a✝ = b✝
  c: Int
  α: Type u
  inst✝¹: Add α
  inst✝: OfNat α 0
  e f: α
  a b _d: Nat
  _h: e ≠ f
  _h₁: a = b
  _c: Int
  ⊢ e + f = e ∨ True
  -/
  prune
  /- goal state:
  α: Type u
  inst✝¹: Add α
  inst✝: OfNat α 0
  ef: α
  _h: e ≠ f
  ⊢ e + f = e ∨ True
  -/
  exact Or.inr trivial

[Jannis Limperg]

I believe the check via goal.find? may miss dependencies when the target contains an mvar. In that case, any fvar in the context of the mvar is a possible dependency of the target. Also, I believe you could use collectFVars instead of looping over the expression multiple times.

[Damiano Testa]

Jannis, thank you for the suggestions! I did not know collectFVars -- I'll look into it!
Wrt metavariables in the target, I had simply thought of applying this tactic in a situation where there were no meta-variables...

[Damiano Testa]

Still, this highlighted an issue, I think:

example (a : Nat) : ∃ n, n = 0 := by
  constructor
  /-
  2 goals
  case h
  a: ℕ
  ⊢ ?w = 0
  case w
  a: ℕ
  ⊢ ℕ
  -/
  prune
  /-
  1 goal
  case h
  a: ℕ
  ⊢ ?w = 0
  -/

One goal disappears, since I forgot to get the goals before and then reassign them later, I think.

However, a remains in context, so this should be fine, right?

[Damiano Testa]

focusing the two defs fixed the "disappearing" goal and is also something that I had intended anyway!

I will look into collectFVars, but not today, since it is getting late!

Thank you for your comments, though!

[Damiano Testa]

I opened !4#5062, containing a small modification of the tactic above.

I ended up preferring to use the recursive approach anyway and gave the option to "step in" at any stage of the process. This gives finer control of how many variables you want to keep: prune 0 only keeps the strictly necessary ones, while prune <large> (which is the same as prune), keeps conservatively all hypotheses that are "recursively visible" from the main goal.