implicit of equality or iff

Stream: metaprogramming / tactics

[Arthur Paulino]

Skimming through some issues I was able to find #1924
Is the sixth item still wanted?

If a lemma is an iff or equality, then check that every variable that appears on both sides is implicit. (requested by Patrick Massot )

[Patrick Massot]

I think it would at least be interesting to see what is flagged and whether we indeed (almost) always want to follow that rule

[Patrick Massot]

It's clearly pretty low priority. But if you are interested in this as a meta-programming exercise then it could be nice

[Arthur Paulino]

Yeah that's exactly it, I've been seeking a motivated application to learn about meta-programming and this scenario doesn't look too hard. Let's see where I can get to

[Patrick Massot]

Nice! Don't forget there are several resources listed on https://leanprover-community.github.io/learn.html#metaprogramming-and-tactic-writing

[Patrick Massot]

and add https://arxiv.org/abs/2004.03673 for the specific topic of linters

[Arthur Paulino]

I'm almost there! The only thing missing is a function to get all variable names present in an expr. Any hints? I couldn't find anything that does this :pray:

[Alex J. Best]

How to do what you want depends a bit on how you did things so far. Will the exprs you are looking at be open or closed at this point? What method did you use to remove the forall / pi binders to leave you with an expr with an iff as the head term?

[Alex J. Best]

There are functions like docs#expr.list_local_consts, you could also use docs#expr.occurs to check things one by one

[Arthur Paulino]

So far I've got here:

import tactic.lint.basic

private def is_explicit : binder_info → bool
| binder_info.default := tt
| _                   := ff

private meta def unravel_explicits_pi : expr → list name → (list name) × expr
| (expr.pi n i _ e) l := unravel_explicits_pi e (if is_explicit i then l.concat n else l)
| e                 l := (l, e)

private meta def split_eq_iff (e : expr) : option (expr × expr) :=
match e.is_eq with
| some e' := e'
| none    :=
  match e.is_iff with
  | some e' := e'
  | none    := none
  end
end

private meta def get_vars (e : expr) : list name := []

private meta def explicit_vars_of_eq_iff (d : declaration) : tactic (option string) := do
  let (ns, e) := unravel_explicits_pi d.type [],
  match split_eq_iff e with
  | none          := return none
  | some (el, er) := do
    let l := ns.map (λ n, (n ∈ get_vars el) && (n ∈ get_vars er)),
    let has_expl := l.foldl (λ acc b, acc || b) ff,
    return $
    if has_expl then "Varibles used on both sides of equalities or iff's must be implicit."
    else none
  end

[Arthur Paulino]

My plan is:

1. Recursively eat up `pi` expressions and accumulate the names of
the default binders (explicit variables). This is done by
`unravel_explicits_pi`

2 . Check if the remaining expression is an equality or an iff. If either
is the case, extract their respective leftmost and rightmost expressions.
This is done by `split_eq_iff`

3. Check if any name in the list of explicit variables names is both in the
right and left sides of the eq or iff

4. If that's so, return a message

5 Return `none` otherwise

[Arthur Paulino]

aaah, got it! I had to use variables' de-Bruijin indexes instead of their names

[Arthur Paulino]

#11606

[Patrick Massot]

Did you run it on mathlib?

[Arthur Paulino]

Nope, I don't have the resources for that. I was testing with a few dummy lemmas on the same file.
I pushed to GitHub though. Let's see the results of the CI run :eyes:

[Arthur Paulino]

(deleted)

[Arthur Paulino]

(deleted)

[Arthur Paulino]

Okay I think I understood what's wrong. The de-Bruijn index is counted in reverse order. So in the lemma

lemma hi {a b : ℕ} (h : a = b + 1) : a = a := rfl

a, b and h have indexes equal to 2, 1 and 0 respectively. Can someone confirm this hypothesis?

[Alex J. Best]

Yes, whenever you open a binder the "original" de Bruijn indexes are incremented by one and then the variable just opened becomes var 0

[Arthur Paulino]

@Alex J. Best lint_mathlib.lean doesn't run on my machine because of the import all line :(

$ lean -j4 --old --run scripts/lint_mathlib.lean
/home/arthur/workspace/mathlib/scripts/lint_mathlib.lean:1:0: error: file 'all' not found in the search path

[Alex J. Best]

You can run leanproject mk-all to create it

[Arthur Paulino]

Oh that was painless. I was already getting all ready to kill the process if it started taking too much memory :sweat_smile:
Thanks!

[Alex J. Best]

It just creates a file with all possible imports, if you already have oleans for everything else importing it won't be an issue. That's why I recommended to use the --old flag for testing this though, that way you don't need to recompile everything when you only changed a linter

[Arthur Paulino]

Alright @Patrick Massot I think the linter is working nicely now. I ran two experiments, one for iffs and eqs and another one just for iffs (after seeing Eric's hidden comment). Basically, forbidding such explicit variables for eqs and iffs is far too restrictive and ~30k lemmas in 1462 files were flagged. When running it for iffs only, ~3k lemmas were flagged in 566 files.

Here you can find the outputs of that linter alone both cases:
eqs_and_iffs.txt
iffs.txt

[Patrick Massot]

I'm not surprised there many errors. The question is: does "fixing" those make mathlib better? Or does it lead to a lot of underscores? If it makes mathlib better then the bonus question is: who wants to fix 3k lemmas and the resulting breakage?

[Arthur Paulino]

Hm, I'm sure I'm not qualified enough to answer the first question because I don't know the extents of "better" in this case. But if it is the case and someone else joins the party, then I'd have the courage to take the journey with the goal of learning a lot

[Arthur Paulino]

It would be a medium sized project though. Many files changed, but with approximately mechanical complexity

[Kevin Buzzard]

When linters started, mathlib failed a lot of them eg lots of defs didn't have docstrings etc. The defs were marked @nolint and we carried on, and fixed things slowly.

Patrick is right in that it might well be the case that there are times when explicit variables do make things easier.

[Arthur Paulino]

I see. I'm modifying the PR anyways to consider only iffs so it looks ~10 times less scary :smiley:

[Arthur Paulino]

Done. Thanks for the help everyone!

[Alex J. Best]

There were some weird examples recently in the thread "rw + apply instance" (sorry on mobile so can't work out how to copy link, why Zulip why), where making arguments explicit made rw not produce side goals

[Arthur Paulino]

But that's a bug, no?

[Alex J. Best]

Perhaps, it might be more subtle than just an oversight though. It could be an unavoidable consequence of the default elaboration order or something like that, where the "fix" of changing the elaboration algorithm would have many knock on effects elsewhere. Or it could just be a small bug, I have no idea.
Of course it would be great to explore and fix these things if possible, I'm just saying this is the sort of issue we might run into if we actually wanted to make such a change at scale.

[Arthur Paulino]

Ah, then you meant "[...] where making arguments implicit made rw [...]", right?

[Alex J. Best]

I don't think so, in that case we had a lemma than when rewritten with made a side goal that was solvable with apply instance. But rw solved that goal on its own when the lemma signature was changed to make R explicit, so the version with R explicit was somehow better. It is very strange

[Yakov Pechersky]

If someone is rewriting with some foo, where the statement of foo has several variables, and when rewriting, foo is used without providing all the variables:
lemma foo (a b c : X) := ...
rw [foo a]
Then, my understanding is, the rw tactic looks for the first subexpression where foo a matches syntactically for some instantiation of b and c. Those become side goals.
Now consider "rw foo _ b". My understanding is that the new side goal a will be automatically discharged only if b somehow implies a as it is.
If a is instead implicit, we have rw foo b, and this lack of mentioning of a means that it relies on on-site unification, which is simplest to do as leaving a side goal, since the statement might not be valid without having an "a".
Why does switching from implicit to explicit then help with these side goals? I think because implicit arguments are elaborated eagerly while explicit and also {{}} are not. So in that deferred elaboration case, the side goal is formed only after choice of rewrite subexpression, and can thus be discharged.

A theory, I might have a mistaken understanding of the tactic and the interplay of elab and unif.