Picky bsupr

Stream: general

[Yaël Dillies]

I've been having problems with bsupr several times now, but I had put that on the account on me being unfamiliar with the API. Far from me was the idea that binfi is actually better behaved! But here's a code snippet testifying:

import order.complete_lattice

variables {α : Type*} [complete_lattice α] {f : α → α} [monotone f]

def fixed_points_complete_lattice :
complete_lattice {x // x = f x} :=
{ sup := λ ⟨x, hx⟩ ⟨y, hy⟩, ,
  le := (≤),
  le_refl := le_refl,
  le_trans := λ x y z, le_trans,
  le_antisymm := λ x y, le_antisymm,
  le_sup_left := _,
  le_sup_right := _,
  sup_le := _,
  inf := _,
  inf_le_left := _,
  inf_le_right := _,
  le_inf := _,
  top := ⟨(⨆ (x : α) (hx : x ≤ f x), x), begin
    let u := ⨆ (x : α) (hx : x ≤ f x), x,
    have h : u ≤ f u := bsupr_le (λ x hx, hx.trans (‹monotone f› (le_bsupr x hx))),
    refine h.antisymm _,
    apply le_bsupr_of_le _,--exact le_bsupr (f u) (‹monotone f› h), weirdly doesn't work
    exact ‹monotone f› h,
    exact le_refl _,
   end⟩,
  le_top := _,
  bot := ⟨(⨅ (x : α) (hx : f x ≤ x), x), begin
    let u := ⨅ (x : α) (hx : f x ≤ x), x,
    have h : f u ≤ u := le_binfi (λ x hx, le_trans (‹monotone f› (binfi_le x hx)) hx),
    refine (h.antisymm _).symm,
    exact binfi_le (f u) (‹monotone f› h),--and this works!!!
   end⟩,
  bot_le := _,
  Sup := _,
  le_Sup := _,
  Sup_le := _,
  Inf := _,
  Inf_le := _,
  le_Inf := _ }

le_bsupr doesn't match while in the same situation with dual order le_binfi matches. I'm baffled.

[Yaël Dillies]

In general, dealing with supr/infi nested more than two times is a pain. I've since filled in the Sup field, and several times I had to use le_binfi, intro two variables, use le_infi, intro a variable, prove the stuff. I would want instead to do something like use le_bbinfi, intro three variables, prove the stuff. And of course generally I would want to use le_b...binfi, intro n variables, prove the stuff. Unless I'm wrong, we currently have no lemma/tactic that would make this process smoother.

[Yaël Dillies]

For example, try proving this lemma that is not supposed to be hard:

import order.complete_lattice

variables {α : Type*} [complete_lattice α] {f : α → α} [monotone f]

lemma mwe (s: set {x // x = f x}) :
  f (⨅ (x : α) (hx : f x ≤ x) (hxs : ∀ y ∈ s, ↑y ≤ x), x) ≤
  ⨅ (x : α) (hx : f x ≤ x) (hxs : ∀ y ∈ s, ↑y ≤ x), x :=

Here's my proof, to guide you

lemma mwe (s: set {x // x = f x}) :
  f (⨅ (x : α) (hx : f x ≤ x) (hxs : ∀ y ∈ s, ↑y ≤ x), x) ≤
  ⨅ (x : α) (hx : f x ≤ x) (hxs : ∀ y ∈ s, ↑y ≤ x), x :=
begin
  refine le_binfi (λ x hx, le_infi (λ hxs, le_trans (‹monotone f› _) hx)),
  apply binfi_le_of_le,
  { exact hx },
  exact infi_le _ hxs,
end

[Johan Commelin]

Should the mono tactic be able help here in principle?

[Yaël Dillies]

Oh. What's this?

[Yaël Dillies]

Okay, here's the battleground: https://github.com/leanprover-community/mathlib/blob/knaster-tarski/src/order/knaster_tarski.lean
It's all done, but every single proof is golfable because of the "bbsupr/bbinfi". Have fun!

[Yaël Dillies]

(yeah, I just read the statement and Knaster–Tarski yesterday on Wikipedia and thought "Oh, that would be fun to do in Lean!", hence I did)

[Eric Wieser]

The commented out code is junk?

[Eric Wieser]

It's not short, but I found your mwe very easy to prove going one step at a time:

lemma mwe  (hf : monotone f) (s: set {x // x = f x}) :
  f (⨅ (x : α) (hx : f x ≤ x) (hxs : ∀ y ∈ s, ↑y ≤ x), x) ≤
  ⨅ (x : α) (hx : f x ≤ x) (hxs : ∀ y ∈ s, ↑y ≤ x), x :=
begin
  apply hf.map_infi_le.trans _,
  apply infi_le_infi,
  intro i,
  apply hf.map_infi_le.trans _,
  apply infi_le_infi,
  intro hi,
  apply hf.map_infi_le.trans _,
  apply infi_le_infi,
  intro hx,
  exact hi,
end

[Eric Wieser]

This does feel like something mono ought to be able to help withh

[Eric Wieser]

tagging docs#monotone.map_infi_le with [mono] gives an error, presumably because the ≤ in the hypothesis is hidden under a binder

[Yaël Dillies]

Yeah, the commented code was my attempt with using complete_lattice directly.

[Yaël Dillies]

There's this general theme about supr and infi that makes me think a tactic designed specifically for them would be beneficial. Here I want inequalities about them, but earlier I wanted a \in \Inter to be transformed into nested \forall.

[Yaël Dillies]

But maybe I'm lacking overview and the mono tactic you're talking about generalizes the tactic I want.

[Eric Wieser]

I assume docs#set.mem_Inter exists and handles your desire for a forall?

[Eric Wieser]

mem is kinda special here; we have no typeclasses for how it interacts with lattice structures as far as I know

[Eric Wieser]

Maybe we should

[Yaël Dillies]

Yeah but then I have the same problem as here. One nested Inter can be dealt with mem_Inter. Two nested Inters can be dealt with mem_bInter (actually not even that, because mem_bInter only picks up the case \Inter (x : \a) (hx : x \in S) and not \Inter (x : \a) (hx : p x) where p is a general predicate). But three nested Inters can only be dealt with mem_Inter + mem_bInter, mem_bInter + mem_Inter or mem_Inter + mem_Inter + mem_Inter. There has to be a better way.

[Eric Wieser]

simp only [mem_Inter] should clean them all up, right?

[Eric Wieser]

example (x : α) (y : ℕ → ℕ → ℕ → set α) : x ∈ ⋂ i j k, y i j k :=
begin
  simp only [set.mem_Inter],
  intros i j k,
  sorry -- `x ∈ y i j k` : oops my goal wasn't true
end

[Yaël Dillies]

Oh, maybe the tactic I want is simp only :sweat_smile:

[Yaël Dillies]

I'm PRing #7589 because I really can't see how to get a cleaner code.