How to best recall P ∧ Q → R

Stream: general

[Martin Dvořák]

I have long been wondering about how to best recall P ∧ Q → R theorems.
I want to optimize for readability, believability, and esthetics.

Consider a project that contains main_result at the end of a long and messy implementation.
I want to recall it in a user-facing file that is formally verified as well.
Several options came to my mind.

import Mathlib

def Foo (x : ℕ) : Prop := sorry
def Bar (x y : ℕ) : Prop := sorry
def Baz (x y : ℕ) : Prop := sorry

theorem main_result {x y : ℕ} (hx : Foo x) (hxy : Bar x y) : Baz x y := sorry
-----------------------------------------------------------------------------

recall main_result {x y : ℕ} (hx : Foo x) (hxy : Bar x y) : Baz x y

recall main_result {x y : ℕ} (_ : Foo x) (_ : Bar x y) : Baz x y

recall main_result {x y : ℕ} : Foo x → Bar x y → Baz x y

recall main_result {x y : ℕ} : Foo x → (Bar x y → Baz x y)

example (x y : ℕ) : Foo x ∧ Bar x y → Baz x y :=
  fun ⟨hx, hxy⟩ => main_result hx hxy

example (x y : ℕ) : (Foo x ∧ Bar x y) → Baz x y :=
  fun ⟨hx, hxy⟩ => main_result hx hxy

• The first recall is the most faithful-to-the-implementation option, but it contains unnecessary variable names and makes linter.unusedVariables complain.
• The second recall fixes the disadvantages of the above but it may make the reader wonder what the underscores mean, distracting readers from the message.
• The third recall is probably the most natural way for me to write it; it is also the most consistent way with respect to other recalls in the same file. Unfortunately, many mathematicians are not used to currying and will be left confused.
• The fourth recall carries a lower risk of confusing the readers. Unfortunately, it is somewhat ugly to look at, especially in situations where P and Q are similar. Also, for people who are not used to currying, it may be still difficult to internalize its meaning.
• The examples at the end are perhaps a good way how to eat the cake and have it too — the curried version is better for the implementation (and also for potential downstream projects), so we keep it inside, but it isn't optimal for presentation of our results, hence we present the results in the uncurried way. On the negative side, it is less obvious on the first sight that an existing result is recalled. Also, we need to decide whether it is obvious that ∧ has higher precedence than → or parentheses should be used for clarity.

Which version do you prefer?

[Patrick Massot]

One possibility is to tell the unused variable linter to stop complaining about recall.

[Martin Dvořák]

Yes, I also considered turning off the linter in the "presentation" file.
However, the question remains whether

recall main_result {x y : ℕ} (hx : Foo x) (hxy : Bar x y) : Baz x y

is the best way to recall given result.

[Martin Dvořák]

/poll Which version do you prefer?
the first recall, after suppressing the linter
the first recall, letting the linter complain
the second recall (underscores)
the third recall (chained implication)
the fourth recall (chained implication with redundant parentheses)
the first example (conjunction implies)
the second example (conjunction with redundant parentheses implies)

[Violeta Hernández]

(what does recall do?)

[Kenny Lau]

like a no-op, hopefully

[Martin Dvořák]

Violeta Hernández said:

(what does recall do?)

It allows us to repeat an existing declaration in a way that emits a compile-time error if the recalled declaration isn't definitionally equal to the original declaration.

[Martin Dvořák]

The very fact that such a proficient Lean user as @Violeta Hernández didn't know recall demonstrates that this command is underutilized and not talked about enough in this community.

It is such a pity that recall isn't used more!
Most of the time when I visit a repository downstream of Mathlib, I don't know where to start reading in order to be able to understand and believe the main results, even if the README file vaguely says what the main results are.

I suggest that every project should have a "summary" in the sink file (the file that is usually named the same as the project, lies in the root folder, and imports all other .lean files) that recalls the main results and all nontrivial definitions they depend on (dependencies of the statements, not the proofs). It is very little extra work and a huge advantage for visitors!

[Yaël Dillies]

Martin Dvořák said:

I suggest that every project should have a "summary" in the sink file (the file that is usually named the same as the project, lies in the root folder, and imports all other .lean files) that recalls the main results and all nontrivial definitions they depend on (dependencies of the statements, not the proofs). It is very little extra work

It is in fact a lot of (continuous) extra work because those recall commands would get wiped out every time I run lake exe mk_all to update that file. This happens > 20 times a week

[Yaël Dillies]

If you can think of another standardised place where such recall commands could go, I'd gladly switch

[Mario Carneiro]

maybe don't use mk_all and use globs instead

[Patrick Massot]

I think we should really encourage use of globs. If they don’t work well enough then we should encourage the FRO to fix them instead of writing those mk_all files.

[Yaël Dillies]

I would be the first happy to drop those files, but I manage too many projects simultaneously to be able to take such an approach on an individual basis. What about we switch out mathlib first?

[Martin Dvořák]

Patrick Massot said:

I think we should really encourage use of globs.

Is it https://github.com/madvorak/duality/blob/db8a785db20438eb379d8fe5a423e5e07469a707/lakefile.lean#L12
that you mean?

[Martin Dvořák]

I love using globs!
I have them in most of my projects that don't have a blueprint (and don't have doc-gen either).
Is it possible to have globs with Leanblueprint (in LeanProject-generated projects)?