biSup_inf_le

Stream: Is there code for X?

[Patrick Massot]

I can’t find.

lemma biSup_inf_le {α β : Type*} [CompleteLattice β] (f : α → β) (s : Set α) (b : β) :
    ⨆ a ∈ s, (f a ⊓ b) ≤ (⨆ a ∈ s, f a) ⊓ b :=
  iSup₂_le fun _ ha ↦ inf_le_inf_right b (le_biSup f ha)

where is it hidden?

[Bhavik Mehta]

It looks to me like this is missing, the closest I can find is docs#iSup_inf_le_sSup_inf which is a less general version of your lemma and docs#iSup₂_inf_eq which has stronger typeclass assumptions.

[Eric Wieser]

@Jovan Gerbscheid, do you know why this doesn't work?

import Mathlib

-- we should have this lemma too
lemma iSup_inf_le {α : Sort*} {β : Type*} [CompleteLattice β] (f : α → β) (b : β) :
    ⨆ a, (f a ⊓ b) ≤ (⨆ a, f a) ⊓ b :=
  iSup_le fun _ => inf_le_inf_right _ (le_iSup f _)

lemma biSup_inf_le {α β : Type*} [CompleteLattice β] (f : α → β) (s : Set α) (b : β) :
    ⨆ a ∈ s, (f a ⊓ b) ≤ (⨆ a ∈ s, f a) ⊓ b := by
  -- extracted into a `have` to exonerate any elaboration issues
  have := fun a : α => iSup_inf_le (f := fun h : a ∈ s => f a) (b := b)
  -- doesn't match
  grw [this]

which fails with

Tactic `grewrite` failed: did not find instance of the pattern in the target expression
  ⨆ (_ : ?a ∈ s), f ?a ⊓ b

α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
f : α → β
s : Set α
b : β
this : ∀ (a : α), ⨆ (_ : a ∈ s), f a ⊓ b ≤ (⨆ (_ : a ∈ s), f a) ⊓ b
⊢ ⨆ a ∈ s, f a ⊓ b ≤ (⨆ a ∈ s, f a) ⊓ b

(recall that ⨆ a ∈ s, f a is the delaboration of ⨆ a, ⨆ h : a ∈ s, f a)

[Aaron Liu]

bound variables

[Aaron Liu]

remember ⨆ a, ⨆ h : a ∈ s, f a is actually iSup fun a => ⨆ h : a ∈ s, f a

[Eric Wieser]

Does grw not support bound variables?

[Aaron Liu]

to match rw which also doesn't support bound variables

[Eric Wieser]

I guess

lemma biSup_inf_le {α β : Type*} [CompleteLattice β] (f : α → β) (s : Set α) (b : β) :
    ⨆ a ∈ s, (f a ⊓ b) ≤ (⨆ a ∈ s, f a) ⊓ b := by
  grw [← iSup_inf_le]
  gcongr
  grw [← iSup_inf_le]

works

[Aaron Liu]

it says in the module docstring about this here

TODO:

The algorithm used to implement grw uses the same method as rw to determine where to rewrite.
This means that we can get ill-typed results. Moreover, it doesn't detect which occurrences
can be rewritten by gcongr and which can't. It also means we cannot rewrite bound variables.

A better algorithm would be similar to simp only, where we recursively enter the subexpression
using gcongr lemmas. This is tricky due to the many different gcongr for each pattern.

With the current implementation, we can instead use nth_grw.

[Eric Wieser]

I don't understand the last remark, nth_grw is of no help here as far as I can tell

[Jovan Gerbscheid]

nth_grw helps if grw doesn't find the right position.

[Eric Wieser]

But I guess doesn't help if the "right" position is under a binder?

[Jovan Gerbscheid]

Indeed

[Patrick Massot]

I created #34812 about those lemmas.