Retrieving lost names

Stream: lean4

[Bolton Bailey]

I am working on translating the tactic from my SNARK project into lean4. The tactic repeatedly splits hypotheses of the form a * b = 0 into a = 0 \or b = 0 and simplifies. The trouble is, I keep overwriting the name found_zero so when the tactic doesn't close the goal, it leaves a bunch of hypotheses with inaccessible names.

Is there some tactic that just assigns all the inaccessible names in the environment an arbitrary name so that I can work with them again?

import Lean.Elab.Tactic
import Mathlib

syntax "integral_domain_tactic" : tactic

macro_rules
| `(tactic| integral_domain_tactic) =>
  `(tactic|
      trace "Call to integral_domain_tactic";
      trace_state;
      -- Factor statements of the form a * b = 0 into a = 0 ∨ b = 0
      -- Note that this also eliminates True and False hypotheses
      simp_all (config := {decide := false, failIfUnchanged := false}) only [
            -- Basic arithmetic simplifications
            add_zero, zero_add, mul_zero, zero_mul, mul_one, one_mul,
            -- Simplifications for true and false
            false_or, or_false, true_or, or_true, not_true, not_false_iff,
            eq_self_iff_true, Ne.def, one_ne_zero, mul_ne_zero_iff,
            -- Key arithmetic simplification for integral domains: a * b = 0 ↔ a = 0 ∨ b = 0
            mul_eq_zero];
      first
        -- If we are done, halt
        | done
        -- If we have a hypothesis of the form a * b = 0, split into a = 0 ∨ b = 0, and recurse
        | --try clear found_zero
          try rename' found_zero => found_zero_prev
          try rename' found_zero_prev => found_zero_prev_prev
          cases' ‹_ ∨ _› with found_zero found_zero
          all_goals integral_domain_tactic
        -- If we cannot split, we skip, leaving the goal unsolved for the user to resolve
        | skip
   )


section test

-- Per the docs: "To obtain an integral domain use [CommRing α] [IsDomain α]"
variable {F R : Type} [Field F] [CommRing R] [IsDomain R]


-- If the tactic can't solve the goal, it should leave the cases it found
example (a b c d e : F)
    (h1 : a * c = 0) (h2 : b * d = 0) (h3 : a * d + b * c = e) :
    a * d = e + 1 ∨ b * c = e + 1 := by
  integral_domain_tactic

The test here results in the state with a case looking like

case inl.inl
FR: Type
inst✝²: Field F
inst✝¹: CommRing R
inst✝: IsDomain R
abcde: F
h3: e = 0
found_zero✝¹: b = 0
found_zero✝: a = 0
⊢ False

[Mario Carneiro]

The usual technique used here is to have the tactic accept a list of binderIdent which allows the user to name these variables as they wish

[Mario Carneiro]

It is considered bad practice for a tactic to produce hypotheses with accessible names unless the user wrote them

[Bolton Bailey]

Right, that definitely seems to be the case in the examples I am seeing in mathlib.

The trouble is, I don't necessarily expect to know how many hypotheses will be split, so I wouldn't know what length of a list to provide. I would really be ok if the split Ors were just named after the hypotheses they split, but I'm not sure how to do that either.

[Bolton Bailey]

In the example above, for instance, I could get 4 cases, and it would be cool if the a = 0 and c = 0 hypotheses were always named h1 and the b = 0 and d = 0 were always named h2. That seems like a capability that would only be applicable to casing on disjunctions, though.

[Mario Carneiro]

The idea is that you just have a list and pull things from the list whenever you need a name

[Bolton Bailey]

And I guess I just call the tactic once with a bunch of random names, and then play with the list until the length is right and the names look reasonable?

[Mario Carneiro]

yeah pretty much

[Mario Carneiro]

Have you ever used the induction' e with ... tactic?

[Mario Carneiro]

you just hunt around with names and underscores until you have the right names in the right places

[Bolton Bailey]

I mean the code I provided above uses cases' it's just getting lost in the recursive call somehow.

[Mario Carneiro]

well you aren't actually passing in names from the caller there, that's why

[Mario Carneiro]

although it would be tricky to split a list of names properly in a macro tactic

[Bolton Bailey]

(Basically this code is all adapted from a tactic in lean3 from over a year ago, I recall you helped me with it a lot, but I think things work a little differently in lean 3 compared to lean 4)