Zulip Chat Archive

Stream: general

Topic: Picky bsupr


Yaël Dillies (May 10 2021 at 21:06):

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 (May 11 2021 at 06:49):

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 (May 11 2021 at 06:54):

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 (May 11 2021 at 06:58):

Should the mono tactic be able help here in principle?

Yaël Dillies (May 11 2021 at 07:09):

Oh. What's this?

Yaël Dillies (May 11 2021 at 08:09):

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 (May 11 2021 at 08:10):

(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 (May 11 2021 at 09:05):

The commented out code is junk?

Eric Wieser (May 11 2021 at 09:12):

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 (May 11 2021 at 09:15):

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

Eric Wieser (May 11 2021 at 09:18):

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 (May 11 2021 at 09:18):

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

Yaël Dillies (May 11 2021 at 09:21):

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 (May 11 2021 at 09:22):

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

Eric Wieser (May 11 2021 at 09:24):

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

Eric Wieser (May 11 2021 at 09:26):

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

Eric Wieser (May 11 2021 at 09:26):

Maybe we should

Yaël Dillies (May 11 2021 at 09:54):

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 (May 11 2021 at 09:58):

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

Eric Wieser (May 11 2021 at 10:00):

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 (May 11 2021 at 11:05):

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

Yaël Dillies (May 12 2021 at 07:06):

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


Last updated: Dec 20 2023 at 11:08 UTC