use bug

Stream: mathlib4

[Patrick Massot]

Trying to write exercises for #mil, I wrote the following code that has several issues.

import Mathlib.RingTheory.Ideal.Operations

open BigOperators

example {R : Type*} [CommRing R] {I J : Ideal R} {x : R} :
    x ∈ I * J ↔ ∃ (n : ℕ) (a b : Fin n → R), (∀ i, a i ∈ I ∧ b i ∈ J) ∧ ∑ i, a i * b i = x := by
  constructor
  · intro hx
    let P : R → Prop := fun x ↦  ∃ n, ∃ a b : Fin n → R, (∀ (i : Fin n), a i ∈ I ∧ b i ∈ J) ∧
      ∑ i : Fin n, a i * b i = x
    apply Submodule.smul_induction_on (p := P) hx
    intro a ha b hb
    existsi 1
    use fun _ ↦ a, fun _ ↦ b
    constructor
    tauto
    simp
    rintro x y ⟨n, a, b, hab, rfl⟩ ⟨m, c, d, hcd, rfl⟩
    existsi n + m
    use Fin.addCases a c
    use Fin.addCases b d
    constructor
    · intros i
      constructor
      · induction i using Fin.addCases
        next i =>  simpa using (hab i).1
        next i =>  simpa using (hcd i).1
      · induction i using Fin.addCases
        next i =>  simpa using (hab i).2
        next i =>  simpa using (hcd i).2
    · simp [Fin.sum_univ_add]
  · rintro ⟨n, a, b, h, rfl⟩
    apply Ideal.sum_mem
    intro i _
    apply Submodule.mul_mem_mul  (h i).1 (h i).2

First I could sweat we add that kind of lemma somewhere but couldn't find it. Then the two calls to existsi cannot be replaced by use without a weird error unknown free variable '_uniq.259659' (that seem to be a fashionable error message those days). Then I'd like to use apply Submodule.smul_induction_on without defining P first. Then I couldn't find Fin.addCases using Loogle, what would be a good request? Then how to find the correct syntax to use induction using Fin.addCases with the | syntax instead of next?. And finally the brand new aesop powers from @Jireh Loreaux do not seem to be able to replace the last three lines. Short version: nothing worked smoothly in this proof.

[Scott Morrison]

What are the new aesop powers? See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60aesop.60.20for.20.60SetLike.60/near/397741320

[Jireh Loreaux]

@Patrick Massot as for aesop, it's just missing attributes. I'm going to have a follow-up PR where I add the attributes more widely as I try to golf these sorts of things across the library. I'll try to collect a list of lemmas that need it, so if you run across any just let me know. In this case, I think the attribute to add is:

attribute [aesop safe apply (rule_sets [SetLike])]
  sum_mem
  Submodule.mul_mem_mul

[Jireh Loreaux]

This is the | syntax for induction using Fin.addCases, but admittedly I had to go-to-def to see what the names were. I don't think we have a code action for this yet, and I'm not sufficiently experienced with metaprogramming yet to write it.

      · induction i using Fin.addCases with
        | left i =>  simpa using (hab i).1
        | right i =>  simpa using (hcd i).1

[Jireh Loreaux]

I don't have a really good suggestion for searching for Fin.addCases unless you know or can guess Case would be in the name. Then ...
@loogle "Cases", FIn (?a + ?b)

[loogle]

:exclamation: unknown identifier 'FIn'
Did you mean "Cases", MLList.fin (?a + ?b) or something else?

[Jireh Loreaux]

@loogle "Cases", Fin (?a + ?b)

[loogle]

:search: Fin.addCases, Fin.lastCases, and 12 more

[Jireh Loreaux]

but that's probably too much cheating.

[Jireh Loreaux]

i'm not really sure what's going on with the use versus existsi, but the variable it's complaining about it P, which you can see by using this quick tactic I used to show the FVarId associated to a local declaration.

open Lean Meta Elab Tactic

syntax (name := fvar_id) "fvar_id" ident : tactic
elab "fvar_id" h:ident : tactic => withMainContext do
  (← getMainGoal).withContext do
  for ldecl in (← getLCtx) do
    if ldecl.userName == h.getId then
      logInfo m!"{ldecl.userName} : {ldecl.type} has FVarId : {ldecl.fvarId.name}"

[Patrick Massot]

@Jireh Loreaux Thank you very much for your answer.

[Patrick Massot]

To everyone, here is a somewhat minimized version of the use bug:

import Mathlib.RingTheory.Ideal.Operations

example {R : Type*} [CommRing R] {I J : Ideal R} {x : R} (hx : x ∈ I • J) :
      ∃ n: ℕ, True := by
   let P : R → Prop := fun x ↦ ∃ n : ℕ, True
   apply Submodule.smul_induction_on (p := P) hx
   intro a ha b hb
   use' 1

[Patrick Massot]

The first idea, which to wrap more stuff into withMainContext is not enough:

import Mathlib.RingTheory.Ideal.Operations

namespace Mathlib.Tactic
open Lean Meta Elab Tactic

/-- Run the `useLoop` on the main goal then discharge remaining explicit `Prop` arguments. -/
def runUse' (eager : Bool) (discharger : TacticM Unit) (args : List Term) : TacticM Unit :=
withMainContext do
  let egoals ← focus do
    let (egoals, acc, insts) ← useLoop eager (← getGoals) args [] []
    -- Try synthesizing instance arguments
    for inst in insts do
      if !(← inst.isAssigned) then
        discard <| observing? do inst.assign (← synthInstance (← inst.getType))
    -- Set the goals.
    setGoals (egoals ++ acc)
    pruneSolvedGoals
    pure egoals
  -- Run the discharger on non-assigned proposition metavariables
  -- (`trivial` uses `assumption`, which isn't great for non-propositions)
  for g in egoals do
    if !(← g.isAssigned) then
      if ← isProp (← g.getType) then
        trace[tactic.use] "running discharger on {g}"
        discard <| run g discharger

elab (name := useSyntax')
    "use'" discharger?:(Parser.Tactic.discharger)? ppSpace args:term,+ : tactic => do
  runUse false (← mkUseDischarger discharger?) args.getElems.toList

end Mathlib.Tactic

[Kyle Miller]

@Patrick Massot I think I found the use bug, but I haven't tested the fix yet

[Patrick Massot]

I can test it if you want.

[Patrick Massot]

What would be the fix?

[Kyle Miller]

I'll push a branch in a moment

[Kyle Miller]

@Patrick Massot Here's a WIP branch with a few fixes: #7827

[Patrick Massot]

Nice. I can see some pattern here.

[Kyle Miller]

@Patrick Massot It looks like at least one of these fixes addressed the problem! Do you think it would be hard to minimize the example so that it can go into the tests/Use file and not need any more imports? I'm guessing the key is that P is let-bound.

[Patrick Massot]

Naive minimization didn't work, but I'll try some more.

[Jireh Loreaux]

Kyle, I thought that as well, but letI didn't make the problem go away, which I would have expected it to do.

[Kyle Miller]

Yeah, got it:

example : let P : Nat → Prop := fun x => ∃ n : Nat, True; P 1 := by
  intro P
  use 1

[Kevin Buzzard]

Nice!

[Kyle Miller]

You need a step like intro at the beginning to make sure you have a new local context before the offending tactic, since otherwise you might accidentally be inside a local context that hides the problem.

[Patrick Massot]

I wasn't fast enough. And mine is more complicated

example : ∀ _n : Nat, ∃ _k : Nat, True := by
  let P : Nat → Prop := fun _n ↦ ∃ _k : Nat, True
  apply Nat.rec (motive := P)
  -- use 1
  existsi 1
  trivial
  intro n _
  existsi 1
  trivial

[Patrick Massot]

I delegated the PR, let's wait for CI.