scope of std

Stream: batteries

[Yury G. Kudryashov]

What is going to be the border between Std and Mathlib? I understand that lemmas about List, Nat, Int, and Rat` that don't need extra dependencies can go to Std. What about

• Order hierarchy, specifically
  • Preorder, PartialOrder, LinearOrder?
  • OrderBot, OrderTop?
  • Lattice, SemilatticeSup, SemilatticeInf?
• Function.Injective, Function.Surjective, Function.Bijective, Function.Involutive?
• Equiv, Function.Embedding? (if yes, then please wait till we decide about #2202)
• algebraic hierarchy? (I guess, "no", at least for now)

[Mario Carneiro]

My not-very-well thought out gut response to these:

• Preorder, PartialOrder, LinearOrder: yes, likely with changes though so it is not yet clear whether it would be suitable for mathlib
• OrderBot, OrderTop, Lattice, SemilatticeSup, SemilatticeInf: probably not unless some additional reasons for having them show up, esp. due to use in data structures
• Function.Injective, Function.Surjective, Function.Bijective, Function.Involutive: These are basic vocabulary definitions, I don't see any reason not to have them
• Equiv: I would say 'yes' but it comes with pretty huge implications in terms of lemmas about it, it may require some finess
• Function.Embedding: probably also yes, although the name is not great
• algebraic hierarchy: I think we might need a separate repo just for this. The churn rate is too high to make it suitable for std

[Joe Hendrix]

I'd like to have folds and sums over data structures so a Monoid in terms of append/empty and SumMonoid would be useful concepts to have. Commutative versions could also be useful for folds over unordered data structures.

I'm not sure they should match Mathlib's though. I'd want to better understand the utility of npow/nsmul and would want to get consensus since stability is really important.

[Joe Hendrix]

With regards to the other classes, I'd like to see algorithms/data structure needs drive their introducing. e.g., graph algorithms for orders, abstract interpretation tactics for lattice operations.

[François G. Dorais]

Joe Hendrix said:

I'd like to have folds and sums over data structures so a Monoid in terms of append/empty and SumMonoid would be useful concepts to have. Commutative versions could also be useful for folds over unordered data structures.

I'm not sure they should match Mathlib's though. I'd want to better understand the utility of npow/nsmul and would want to get consensus since stability is really important.

I think we need ad-hoc monoid classes that are not attached to specific operations and notations.

[Patrick Massot]

Joe Hendrix said:

I'd want to better understand the utility of npow/nsmul and would want to get consensus since stability is really important.

Did you read Chapter 7 of #mil about that?

[Joe Hendrix]

Did you read Chapter 7 of #mil about that?

I have not, but read through it now. Thanks.

[Joe Hendrix]

François G. Dorais said:

I think we need ad-hoc monoid classes that are not attached to specific operations and notations.

As in include the operations in the signature? That seems reasonable for fold. We could just restrict its use in Std to types where the parameters for that instance are clear (e.g, List/Array/etc).

[Yury G. Kudryashov]

It would be nice to have generic lemmas about unspecified operations and simp being able to apply it to specific operations (e.g., tagged with an attribute) like */+/∪. Probably, this will need yet another change to simp core because these lemmas won't have head symbols anymore.

[Joe Hendrix]

Could you share an example?

[Yury G. Kudryashov]

E.g., 1 * a = a, where 1 is a neutral element for *.

[Yury G. Kudryashov]

Or a + (-a) = 0, where - is the negation for +.

[Yury G. Kudryashov]

OTOH, to_additive etc work for now.

[Joe Hendrix]

There is some work on a more precise discrimination tree in std4#394, but I don't think that addresses this use case though. I think this would need to key on the type class constraint and require changes to the Key type. I'd like to do additional work on simp (e.g., rewriting modulo) later in the year, but other things currently take priority.

[Yury G. Kudryashov]

I don't think that this has high priority. For now, we use tactic like to_additive to generate versions of lemmas for different operations.

[François G. Dorais]

Mario Carneiro said:

• algebraic hierarchy: I think we might need a separate repo just for this. The churn rate is too high to make it suitable for std

Yes, a separate repo is a better idea. I, for example and probably others, are experimenting with algebraic hierarchies based on different ideas from Mathlib's. It would be a huge setback if these experiments weren't able to use Std to implement complex decision algorithms, for example.

[Kevin Buzzard]

Out of interest, what do you not like about mathlib's way of setting it all up? I guess mathlib itself can be regarded as evidence that it works...

[Joe Hendrix]

I think there are a few things:

1. Standard should be performant. I'd at least want a repeated squaring approach (e.g, mathlib#8885).
2. There's complexity in how to deal with the diamond issue and desire for extensions (e.g., a PosNat version for Semigroup.

I'm leaning towards introducing a version where the operations are unbundled for use with folding over structures. That wouldn't conflict with the Mathlib and an analogue for SMul doesn't make sense there so the diamond issue is avoided.

[Johan Commelin]

Before splitting the algebraic hierarchy into a separate repo, I would like to see evidence for projects that want to depend on the algebraic hierarchy but do not want to depend on mathlib

[Mario Carneiro]

I think there is a fairly large number of projects that want to depend on "mathlib lite", i.e. tactics like linarith, some finite sets, maybe enough for doing basic combinatorics but not other things like topology and analysis (except insofar as those things are dependencies of the other things). I estimate somewhere in the range of 400 files being relevant here assuming a good job is done of import pruning

[Mario Carneiro]

The trouble is that mathlib has really not grown in a direction such that one can cleanly cleave that off without pulling closer to 1500 files (which is still better than the 4000 files you get today)

[Yury G. Kudryashov]

Mario Carneiro said:

• Function.Injective, Function.Surjective, Function.Bijective, Function.Involutive: These are basic vocabulary definitions, I don't see any reason not to have them

I'm going to PR these to std. I have 2 questions:

• what would be a good file for (a) definitions; (b) theorems?
• what name should I put in the "Author:" field? The first 3 definitions are not mine.

[Mario Carneiro]

This should be migrating a file from mathlib (ish), you should copy the author info from there

[Mario Carneiro]

I think we can move Std.Logic to Std.Logic.Basic and add this as Std.Logic.Function

[Yury G. Kudryashov]

Should it be Std.Logic.Function.Defs and Std.Logic.Function.Lemmas or just 1 file?

[Mario Carneiro]

for now, just Std.Logic.Function, these are pretty abstract definitions

[Yury G. Kudryashov]

I'll make a PR. If there will be too many lemmas, then we can always move them to a new file.

[Mario Carneiro]

in std there is a split between Basic and Lemmas roughly equivalent to Defs / Basic in mathlib, but Basic files are normally for executable functions

[Mario Carneiro]

I think we can make an exception for Std.Logic which will be all lemmas and noncomputable defs more or less

[Mario Carneiro]

back in the day there wasn't too much in the way of theorems directly about those four definitions but I'm sure it's grown since then...

[Mario Carneiro]

I'm wondering if we can or should forgo the other auxiliary definitions like LeftInverse and HasLeftInverse

[Mario Carneiro]

I've never really felt that they pulled their weight, you can just inline them into the few statements using them

[Yury G. Kudryashov]

Do we need HasLeftInverse? In classical logic, it's just Injective.

[Mario Carneiro]

std is, let's say, constructive-aware

[Mario Carneiro]

but like I said I don't think we really need the definition regardless

[Yury G. Kudryashov]

There are 2 ways to write LeftInverse: f ∘ g = id and ∀ x, f (g x) = x.

[Mario Carneiro]

in lemma statements I would opt for the second one

[Mario Carneiro]

which IIRC is also how LeftInverse is defined

[Yury G. Kudryashov]

Mario Carneiro said:

std is, let's say, constructive-aware

Do you care about computable definitions, or constructive proofs as well?

[Mario Carneiro]

both, although I'm not pushing very hard for constructive proofs ATM

[Mario Carneiro]

Actually the situation with computable definitions is more complex, because std wants computable definitions to actually be efficient

[Yury G. Kudryashov]

BTW, do you plan to write some automation for enforcing constructive proofs on a specific set of theorems?

[François G. Dorais]

@Kevin Buzzard It's not that I don't like Mathlib's way, I'm just exploring other ways.

[Mario Carneiro]

I have some automation for that, but I never committed it

[Yury G. Kudryashov]

If you care about some thoerems in Mathlib not using classical reasoning, then probably you should commit this automation.

[Mario Carneiro]

(it was a bit depressing to trace everything back to split and then be dashed against the rocks of lean4#2414)

[Yury G. Kudryashov]

Note: I don't care about constructivist reasoning but I'm ready to tolerate it in some parts of Mathlib if this will improve chances of you and a few other people who care about it not leaving the project.

[Yury G. Kudryashov]

What should I do about attribute [eqns _]? Delete them and leave it for Mathlib?

[Mario Carneiro]

yes, looks like you can set that from other files just fine so it should be okay to do so

[Mario Carneiro]

what declaration is using that?

[Yury G. Kudryashov]

flip and comp

[Mario Carneiro]

those aren't even defined in std, so it should be fine

[Mario Carneiro]

We can look into upstreaming eqns too, it looks fairly reasonable

[Yury G. Kudryashov]

I want to keep this PR small.

[Yury G. Kudryashov]

We can upstream more later.

[Johan Commelin]

Btw, here is ForbiddenAxioms, which I think was mostly written by Mario at some point.

import Std.Tactic.Lint
import LeanCond.PrintNum

namespace Lean

open Elab Command

private def forbiddenAxioms (bad : List Name) : CommandElabM Unit := do
  let env ← getEnv
  let decls ← liftCoreM Std.Tactic.Lint.getDeclsInCurrModule
  decls.forM fun n ↦
    let axs := ((((CollectAxioms.collect n).run env).run {}).2).axioms.toList
    let l := bad.filter fun a ↦ a ∈ axs
    if l.isEmpty then pure ()
    else logError m!"'{n}' depends on: {l}"

open private printAxiomsOf from Lean.Elab.Print
elab tk:"#forbiddenAxioms " ids:ident* : command => withRef tk do
  let ns ← ids.mapM resolveGlobalConstNoOverloadWithInfo
  withRef tk <| forbiddenAxioms ns.toList

private def explainForbiddenAxioms (n : Name) (bad : List Name) : CommandElabM Unit := do
  let env ← getEnv
  match env.find? n with
  | none => throwError "unknown constant '{n}'"
  | some ci =>
  match ci.value? with
  | none => throwError "constant '{n}' has no value"
  | some e => do
  let deps := e.getUsedConstants
  deps.forM fun d ↦
    let axs := ((((CollectAxioms.collect d).run env).run {}).2).axioms.toList
    let l := bad.filter fun a ↦ a ∈ axs
    if l.isEmpty then pure ()
    else logError m!"'{d}' depends on: {l}"

open private printAxiomsOf from Lean.Elab.Print
elab tk:"#explainForbiddenAxioms " ids:ident* : command => withRef tk do
  let ns ← ids.mapM resolveGlobalConstNoOverloadWithInfo
  match ns.toList with
  | [] => throwError "no constant given"
  | n::ns => withRef tk <| explainForbiddenAxioms n ns

end Lean

[Johan Commelin]

I don't know if Std would want something like this.

Usage: put #forbiddenAxioms Classical.choice at the bottom of a file, and it will ensure that all the decls in that file are constructive.

[Yury G. Kudryashov]

IMHO, it should be per-declaration.

[Johan Commelin]

Makes sense

[Johan Commelin]

#explainForbiddenAxioms will tell you which decls in the proof of theorem X are causing it to be non-constructive

[Mario Carneiro]

oh yeah, that's my uncommitted tactic alright

[Mario Carneiro]

the reason it scans everything in the file is because I was using it to check all definitions for reasonable use of classical axioms. For a permanent attribute it would of course be per-declaration

[Mario Carneiro]

when you have a file like Std.Data.Nat.Lemmas with a bazillion little lemmas you don't want to have to write each declaration out separately

[Mario Carneiro]

(my previous workflow was to grep for theorem and then multi-edit my way to a long list of #print axioms lines, but you still have to then delete the ones which turn up empty (which isn't immediately obvious because #print axioms always produces output) and you still have to figure out which constant reference is "to blame" in each case)

[Patrick Massot]

Johan Commelin said:

Before splitting the algebraic hierarchy into a separate repo, I would like to see evidence for projects that want to depend on the algebraic hierarchy but do not want to depend on mathlib

I definitely see a use case for having real numbers + tactics: 1st year undergrad teaching.

[Patrick Massot]

To be clear: the fact that the hard-drive requirement of my 1st year undergrad course got multiplied by 10 in the Lean 4 upgrade is a serious issue.

[Kevin Buzzard]

I am about to find out this week whether this is an issue for my students; this time last year I was still teaching in Lean 3.

[Yury G. Kudryashov]

I think that instead of having separate repos we should have a tool that deletes all files not imported by a given list of files. Then you put the remaining files in a separate repo and use it for your course.

[Yury G. Kudryashov]

Or lake should download oleans on the fly so that the students won't have to download unneeded files.

[Mario Carneiro]

I will keep hoping that we can get lake to do this automatically

[Mario Carneiro]

Note that you can already lake exe cache get Mathlib.Data.Real.Basic if you want

[Mario Carneiro]

but lake will clone the whole repo, so you always get all the sources regardless

[Yury G. Kudryashov]

Mario Carneiro said:

My not-very-well thought out gut response to these:

• Preorder, PartialOrder, LinearOrder: yes, likely with changes though so it is not yet clear whether it would be suitable for mathlib

What changes would you expect in Preorder/PartialOrder?

[Mario Carneiro]

lean4#1777

[Mario Carneiro]

that is mainly about LinearOrder though

[Mario Carneiro]

for the simpler classes the main thing is that we may want a lawless and/or decidable version of the class

[Yury G. Kudryashov]

Lawless: docs#LE and docs#LT

[Mario Carneiro]

in most programming languages PartialOrd or equivalent implies the existence of a function which decides LE/LT

[Yury G. Kudryashov]

Decidable: docs#DecidableRel

[Mario Carneiro]

that's four classes though just for decidable le/lt

[Mario Carneiro]

and we definitely want to avoid the current situation where some stuff asks for le and other stuff uses lt

[Yury G. Kudryashov]

I will think whether we can make it useful both for Mathlib and programming.

[Mario Carneiro]

having one canonical ordering class (or a hierarchy of them) is important for this

[Mario Carneiro]

(programming applications also have a use for the lawful ordering class, e.g. docs#Std.TransCmp which is used in RBMap)

[Martin Dvořák]

I would love to see left and right in Std4.

[Kim Morrison]

@Martin Dvořák, they have been for a while. import Std.Tactic.LeftRight.