bounded forall implicitness

Stream: general

[Patrick Massot]

I just came across this question asked by Mario three years ago. Each time we write ∀ x ∈ a, ... we really mean ∀ {x : X}, x ∈ a → ... rather than ∀ (x : X), x ∈ a → .... Is this something we should now change (I guess it used to be locked in core)?

[Johan Commelin]

That would be really nice... it would also be a major refactor (-;

[Gabriel Ebner]

You could also write ∀ {x ∈ a}, if you want both arguments to be implicit.

[Gabriel Ebner]

More seriously, it is a single line in parser.cpp that would need to be changed.

[Gabriel Ebner]

Personally, I don't like this style though. It messes error-reporting up too much when you write term-mode proofs.

[Patrick Massot]

Do you have an example of messing up? Note that I don't have a strong opinion here, I only stumbled on this old question by @Mario Carneiro

[Gabriel Ebner]

Something like the following. Note that neither of the two underscores has an error message:

lemma foo : ∀ {ε}, ε > 0 → ¬ ε < 0 := sorry
example : false := foo _ _

This used to be a much bigger problem because without the error messages you had no idea what to fill in for the underscores. This has actually improved recently, now you can at least see a goal if you move over the underscore: ⊢ ⁇ > 0.

[Gabriel Ebner]

Another advantage of explicit arguments is that you can more easily provide the proof via a tactic, like foo x (by simp).

[Patrick Massot]

Ok, we probably won't start a giant refactor if it could then bite us.

[Mario Carneiro]

(Actually, it isn't my question. You probably attributed it to me because I made the initial mathlib commit, but it dates back to library_dev and was asked by Jeremy.)

[Patrick Massot]

Oh I see. I should be careful with git blame from that time.

[Kevin Buzzard]

So this is some question about Lean 2 maybe?

[Mario Carneiro]

no, library_dev is still lean 3

[Mario Carneiro]

it was written from scratch, more or less

[Mario Carneiro]

I don't think there are any files that were actually recognizably ported from lean 2, except maybe something like algebra.group

[Mario Carneiro]

as for the question at hand, I think it would be better to default to ∀ {{ε}}, ε > 0 → ...