complete_lattice and has_sup

Stream: mathlib4

[Patrick Massot]

As can be seen elsewhere, I wanted to open a PR to start working on order.complete_lattice. And the very first line is tricky. I'm sure this has been discussed but I can't find it. In Lean 3 we had docs#has_sup and docs#has_Sup. How do we translate those?

[Patrick Massot]

I've found https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/sup.2FSup but it was inconclusive. Now is the time to decide something.

[Yaël Dillies]

We just decided to keep the Lean 3 capitalisation for Icc and friends. Should we do the same for sup and Sup?

[Yaël Dillies]

Also, wait until you get to file#probability/independence :grinning_face_with_smiling_eyes:

[Ruben Van de Velde]

Oh no. SUP?

[Yaël Dillies]

That doesn't work for lemma names, because it would get turned back into sup

[Kevin Buzzard]

SupCat

[Adam Topaz]

what if has_sup becomes BinarySup and has_Sup becomes Sup?

[Adam Topaz]

That matches e.g. docs#category_theory.limits.has_binary_products and docs#category_theory.limits.has_products

[Yaël Dillies]

So you want to write binarySup_binarySup_binarySup_comm for docs#sup_sup_sup_comm?

[Adam Topaz]

that lemma has a ridiculous name anyway

[Yaël Dillies]

Thanks! I named it

[Mario Carneiro]

This is about the name of the class not the notation though

[Mario Carneiro]

e.g. the name of the class for \in is Membership

[Mario Carneiro]

but the operator is called mem

[Mario Carneiro]

I don't think a longer name is much of a problem here since it will be rarely used

[Mario Carneiro]

I think binary sup (the operator) should be called sup and I hope that's not under discussion

[Patrick Massot]

Oops, I manage to split this conversation into two threads because I wanted to connect with the older discussion.

[Mario Carneiro]

let's keep this one on the name of the notation classes

[Mario Carneiro]

although I suppose that it depends somewhat on the name of the operations

[Reid Barton]

I actually find sup for the binary operation the most confusing one

[Reid Barton]

in part because it's not the terminology I'm used to, e.g., nlab

A poset that has all finite joins is a join-semilattice [= semilattice_sup + has_bot]. A poset that has all suprema is a suplattice [= complete_semilattice_Sup].

[Eric Wieser]

The other thread is here

[Patrick Massot]

We now settled on names for those functions. I started to update the file. But it would be nice to have help from mathport. Indeed mathport decided to rename all Sup to sup and it doesn't help at all with search and replace to enforce the new names. Can we somehow tell mathport to try again with the chosen sup supₛ supᵢ inf infₛ infᵢ as well as the corresponding class names (see mathlib4#1053).

[Kevin Buzzard]

Can you get the oneshot feature to work?

[Kevin Buzzard]

https://github.com/leanprover-community/mathport/blob/master/Oneshot/README.md

[Patrick Massot]

I'll try that later today

[Eric Wieser]

If you already have a port of a file, you should be able to get git to help you here, by setting up your history as

old-mathport-output ------ your-partial-port
     \
      \------- new-mathport-output

and then merging the heads

[Scott Morrison]

I did some more by hand, pushing hopefully complete fixes up to line 465. But I'm going to stop for the night (possibly even the whole weekend...)

[Patrick Massot]

I did a mathport oneshot pass and pushed

[Patrick Massot]

I did a big renaming and cleanup pass. The file now starts to make sense. I'm releasing the lock on this PR.

[Scott Morrison]

Awesome! I did a little more, and we're getting closer.

[Scott Morrison]

Okay, it compiles now, and I fixed a bunch of names involving Sup.

[Scott Morrison]

There is some linting to do, if someone wants to look at that.

[Patrick Massot]

The complete lattice file is almost linted but there are two remaining errors about a simp lemma not being able to simplify its left-hand side.

@[simp]
theorem supᵢ_infᵢ_ge_nat_add (f : ℕ → α) (k : ℕ) : (⨆ n, ⨅ i ≥ n, f (i + k)) = ⨆ n, ⨅ i ≥ n, f i :=
  by
  have hf : Monotone fun n => ⨅ i ≥ n, f i := fun n m h => binfᵢ_mono fun i => h.trans
  rw [← Monotone.supᵢ_nat_add hf k]
  · simp_rw [infᵢ_ge_eq_infᵢ_nat_add, ← Nat.add_assoc]

Note that, right after this lemma (where the linter already complains), you can try

example (f : ℕ → α) (k : ℕ) : (⨆ n, ⨅ i ≥ n, f (i + k)) = ⨆ n, ⨅ i ≥ n, f i := by
   simp

and it works. The version with simp only [supᵢ_infᵢ_ge_nat_add] also works. The only weird thing is that simp? reports simp only [not_le, supᵢ_infᵢ_ge_nat_add]. And simp only [not_le] doesn't seem to do anything.

[Patrick Massot]

@Gabriel Ebner do you understand what is going with the simp linter in this example?

[Patrick Massot]

This is in mathlib4#1053

[Gabriel Ebner]

This is a hard nut to crack. I can't really tell what's going on here either. Weirdly enough, if I call simpNF.test directly then the linter passes. It's only when run via #lint that it complains. :shrug:

[Gabriel Ebner]

Either way, supᵢ_infᵢ_ge_nat_add should not be marked simp, the subterm ?f (i + ?k) produces an ugly higher-order unification problem.

[Scott Morrison]

Okay, I've removed the simp there, and left a link to this thread. I'll merge this PR soon! Thanks all for the work on this one. On to data.list.basic. :-)

[Eric Wieser]

Is the use of ge instead of le causing the issue?

[Kevin Buzzard]

It doesn't seem to be. Interestingly, Patrick's example is

(⨆ n, ⨅ i ≥ n, f (i + k)) = ⨆ n, ⨅ i ≥ n, f i

and Chris' example here is

(⋃ n, ⋂ i ≥ n, f (i + k)) = ⋃ n, ⋂ i ≥ n, f i

which are, erm, kind of similar.

[Kevin Buzzard]

I've recorded the issue here but clearly the short term solution is just to remove the simp and move on.