monotone functions from finset

Stream: Is there code for X?

[Heather Macbeth]

I couldn't find in mathlib the following characterization of monotone functions with domain a Finset, anyone recognize it?

import Mathlib.Data.Finset.Basic

open Finset

example {α β : Type _} [DecidableEq α] [Preorder β] (f : Finset α → β) :
    Monotone f ↔ ∀ s : Finset α, ∀ i, f s ≤ f (insert i s) := by
  refine ⟨fun h s i ↦ ?_, fun h ↦ ?_⟩
  · exact h (Finset.subset_insert i s)
  · intro s
    suffices : ∀ t, f s ≤ f (s ∪ t)
    · intro v huv
      calc f s ≤ f (s ∪ (v \ s)) := this _
        _ = f v := by rw [union_sdiff_of_subset huv]
    intro t
    induction' t using Finset.induction with i t _hit ih
    · simp
    · calc f s ≤ f (s ∪ t) := ih
        _ ≤ f (insert i (s ∪ t)) := h _ _
        _ = f (s ∪ (insert i t)) := by rw [Finset.union_insert]

[Eric Wieser]

I think it should follow from some result about docs#Covby ?

[Anatole Dedecker]

I don't see why it would, because this really only true because you can get to any finset by a finite sequence of insertion. For example the result is false for Set (take f s = 1 if s is finite and f s = 0 otherwise)

[Anatole Dedecker]

The mathematical result is that the order on Finset is the smallest order relation such that s ⊆ insert i s, but I don't think we have that nor a good way to use it.

[Eric Wieser]

I think the version I want is

import Mathlib.Data.Finset.Basic
import Mathlib.Order.Cover
import Mathlib.Order.LocallyFinite

open Finset

lemma monotone_iff_forall_covby {α β : Type*} [Preorder α] [LocallyFiniteOrder α] [Preorder β] (f : α → β) :
    Monotone f ↔ ∀ a b : α, a ⋖ b → f a ≤ f b := by
  refine ⟨fun hf a b h ↦ ?_, fun h ↦ ?_⟩
  · exact hf h.le
  · intro a b h
    -- iterate over a chain between `a` and `b`
    sorry

[Anatole Dedecker]

Oh okay with LocallyFiniteOrder that would work

[Eric Wieser]

Where the other two missing pieces are:

lemma Finset.covby_cons {α} {a : α} {s : Finset α} (h : a ∉ s) : s ⋖ cons a s h :=
  ⟨Finset.ssubset_cons h, fun t (hst : s ⊂ t) (hts : t ⊂ _) => sorry⟩

lemma Finset.covby_iff_eq_cons {s t : Finset α} : s ⋖ t ↔ ∃ a h, t = cons a s h :=
  ⟨fun h => sorry, fun ⟨a, h, h'⟩ => h' ▸ Finset.covby_cons h⟩

[Heather Macbeth]

By the way, while using my brand new lemma, I realised that the more convenient version is to put an extra condition i ∉ s on the index:

theorem Finset.monotone_iff {α β : Type _} [Preorder β] (f : Finset α → β) :
    Monotone f ↔ ∀ s : Finset α, ∀ {i} (hi : i ∉ s), f s ≤ f (insert i s) := by

[Jireh Loreaux]

Just to be clear, that makes it exactly (up to propositional equality) Covby.

[Anatole Dedecker]

Eric Wieser said:

I think the version I want is

import Mathlib.Data.Finset.Basic
import Mathlib.Order.Cover
import Mathlib.Order.LocallyFinite

open Finset

lemma monotone_iff_forall_covby {α β : Type*} [Preorder α] [LocallyFiniteOrder α] [Preorder β] (f : α → β) :
    Monotone f ↔ ∀ a b : α, a ⋖ b → f a ≤ f b := by
  refine ⟨fun hf a b h ↦ ?_, fun h ↦ ?_⟩
  · exact hf h.le
  · intro a b h
    -- iterate over a chain between `a` and `b`
    sorry

I claim that the right way to prove this is to start with:

import Mathlib.Data.Finset.Basic
import Mathlib.Order.Cover
import Mathlib.Order.LocallyFinite

open Finset

lemma foo {α : Type*} [Preorder α] [LocallyFiniteOrder α] (x y : α) :
    x ≤ y ↔ Relation.ReflTransGen (· ⋖ ·) x y := by
  sorry

[Anatole Dedecker]

Then things like docs#Relation.ReflTransGen.lift should get the monotonicity result

[Anatole Dedecker]

Note that we have docs#List.relationReflTransGen_of_exists_chain

[Eric Wieser]

Heather Macbeth said:

By the way, while using my brand new lemma, I realised that the more convenient version is to put an extra condition i ∉ s on the index

At that point you may as well use cons instead of insert, which also saves you from needing [DecidableEq α]

[Yaël Dillies]

btw I have a big PR with a bunch of relevant lemmas

[Anatole Dedecker]

What a surprise!

[Jireh Loreaux]

But Yaël, the key question is: is it Lean 3 or Lean 4? :smiley:

[Jireh Loreaux]

@Anatole Dedecker I don't think your lemma foo is true unless you assume α is a PartialOrder, because if x ≠ y but x ≤ y and y ≤ x, then Relation.ReflTransGen (· ⋖ ·) x y is false because there is no strictly increasing chain from x to y.

[Anatole Dedecker]

Ah right. That problem doesn’t arise if we use docs#Wcovby though, right? But restricting to partial orders is probably fine anyway

[Jireh Loreaux]

Let the golfing begin, I am totally unfamiliar with this end of the library:

import Mathlib.Data.Finset.LocallyFinite
import Mathlib.Order.Cover
import Mathlib.Order.LocallyFinite

open Finset

lemma foo {α : Type*} [Preorder α] [LocallyFiniteOrder α] (x y : α) :
    x ≤ y ↔ Relation.ReflTransGen (· ⩿ ·) x y := by
  refine ⟨?_, fun h ↦ ?_⟩
  · suffices ∀ n : ℕ, ∀ x y : α,
        x ≤ y → (Icc x y).card = n → Relation.ReflTransGen (· ⩿ ·) x y by
      exact fun a ↦ this (card (Icc x y)) x y a rfl
    intro n
    induction n using Nat.strong_induction_on with
    | @h n hn =>
      match n with
      | 0 => exact fun x y hx h ↦ (Icc_eq_empty_iff.mp (by simpa using h) hx).elim
      | 1 =>
        intro x y hxy h
        rw [card_eq_one] at h
        obtain ⟨a, ha⟩ := h
        have hx := mem_singleton.mp <| ha ▸ left_mem_Icc.mpr hxy
        have hy := mem_singleton.mp <| ha ▸ right_mem_Icc.mpr hxy
        substs hx hy
        rfl
      | k + 2 =>
        intro x y hxy h
        have : (Ico x y).card < k + 2 := h ▸ (card_lt_card <|
          ⟨Ico_subset_Icc_self, not_subset.mpr ⟨y, ⟨right_mem_Icc.mpr hxy, right_not_mem_Ico⟩⟩⟩)
        by_cases hxy' : y ≤ x
        · exact Relation.ReflTransGen.single
            ⟨hxy, fun c hxc hcy ↦ lt_irrefl c <| (hcy.trans_le hxy').trans hxc⟩
        · have h_non : (Ico x y).Nonempty := ⟨x, mem_Ico.mpr ⟨le_rfl, lt_of_le_not_le hxy hxy'⟩⟩
          obtain ⟨z, z_mem, hz⟩ := (Ico x y).exists_maximal h_non
          have z_card : (Icc x z).card < k + 2 := calc
            (Icc x z).card ≤ (Ico x y).card :=
              card_le_of_subset fun w hw ↦ Icc_subset_Ico_right (mem_Ico.mp z_mem).2 hw
            _              < k + 2 := this
          have h₁ := hn (Icc x z).card z_card x z (mem_Ico.mp z_mem).1 rfl
          have h₂ : z ⩿ y := by
            refine ⟨(mem_Ico.mp z_mem).2.le, fun c hzc hcy ↦ hz c ?_ hzc⟩
            exact mem_Ico.mpr <| ⟨(mem_Ico.mp z_mem).1.trans hzc.le, hcy⟩
          exact Relation.ReflTransGen.tail h₁ h₂
  · induction h with
    | refl => rfl
    | tail _ h₁ h₂ => exact h₂.trans h₁.le

[Jireh Loreaux]

One place I feel like there should be obvious room for improvement: I did strong induction on the cardinality of Finset.Icc x y, but it would have been nicer if I could have used some sort of direct induction principle; I couldn't see how to make things like docs#Finset.induction_on apply in this situation though.

[Anatole Dedecker]

I think you really have to use cardinality here though, because you don’t know how much you decrease the cardinality at each step, so you have to use some kind of well-foundedness. Probably you could also use well foundedness of \subset on Finset, but I can’t think of anything else

[Jireh Loreaux]

Yes, the well-foundedness of ⊆ on Finset was the kind of thing I was thinking, but I guess it's not too important.

[Jireh Loreaux]

@Heather Macbeth I've added a bit more below, but I haven't yet added the glue that connects covby to insert for Finset. If you would like to clean it up and PR it, that's fine, but if you want me to I can probably do it sometime this weekend.

import Mathlib.Data.Finset.LocallyFinite
import Mathlib.Order.Cover
import Mathlib.Order.LocallyFinite

open Finset

variable {α β : Type*}

lemma le_iff_reflTransGen_wcovby [Preorder α] [LocallyFiniteOrder α] {x y : α} :
    x ≤ y ↔ Relation.ReflTransGen (· ⩿ ·) x y := by
  refine ⟨fun hxy ↦ ?_, fun h ↦ ?_⟩
  · suffices ∀ n : ℕ, (Icc x y).card = n → Relation.ReflTransGen (· ⩿ ·) x y by
      exact this (card (Icc x y)) rfl
    intro n
    induction n using Nat.strong_induction_on generalizing x y with
    | @h n hn =>
      match n with
      | 0 => exact fun h ↦ (Icc_eq_empty_iff.mp (by simpa using h) hxy).elim
      | 1 =>
        intro h
        rw [card_eq_one] at h
        obtain ⟨a, ha⟩ := h
        have hx := mem_singleton.mp <| ha ▸ left_mem_Icc.mpr hxy
        have hy := mem_singleton.mp <| ha ▸ right_mem_Icc.mpr hxy
        substs hx hy
        rfl
      | k + 2 =>
        intro h
        have : (Ico x y).card < k + 2 := h ▸ (card_lt_card <|
          ⟨Ico_subset_Icc_self, not_subset.mpr ⟨y, ⟨right_mem_Icc.mpr hxy, right_not_mem_Ico⟩⟩⟩)
        by_cases hxy' : y ≤ x
        · exact Relation.ReflTransGen.single
            ⟨hxy, fun c hxc hcy ↦ lt_irrefl c <| (hcy.trans_le hxy').trans hxc⟩
        · have h_non : (Ico x y).Nonempty := ⟨x, mem_Ico.mpr ⟨le_rfl, lt_of_le_not_le hxy hxy'⟩⟩
          obtain ⟨z, z_mem, hz⟩ := (Ico x y).exists_maximal h_non
          have z_card : (Icc x z).card < k + 2 := calc
            (Icc x z).card ≤ (Ico x y).card :=
              card_le_of_subset fun w hw ↦ Icc_subset_Ico_right (mem_Ico.mp z_mem).2 hw
            _              < k + 2 := this
          have h₁ := hn (Icc x z).card z_card (mem_Ico.mp z_mem).1 rfl
          have h₂ : z ⩿ y := by
            refine ⟨(mem_Ico.mp z_mem).2.le, fun c hzc hcy ↦ hz c ?_ hzc⟩
            exact mem_Ico.mpr <| ⟨(mem_Ico.mp z_mem).1.trans hzc.le, hcy⟩
          exact Relation.ReflTransGen.tail h₁ h₂
  · induction h with
    | refl => rfl
    | tail _ h₁ h₂ => exact h₂.trans h₁.le

lemma monotone_iff_forall_wcovby [Preorder α] [LocallyFiniteOrder α] [Preorder β]
    (f : α → β) : Monotone f ↔ ∀ a b : α, a ⩿ b → f a ≤ f b := by
  refine ⟨fun hf _ _ h ↦ hf h.le, fun h a b hab ↦ ?_⟩
  simpa [Relation.reflTransGen_eq_self (r := ((· : β) ≤ ·)) IsRefl.reflexive transitive_le]
    using Relation.ReflTransGen.lift f h <| le_iff_reflTransGen_wcovby.mp hab

open Relation

lemma Relation.ReflTransGen.reflGen {r : α → α → Prop} :
    ReflTransGen (ReflGen r) = ReflTransGen r := by
  refine le_antisymm (fun x y h ↦ ?_) ?_
  · simpa [refl_trans_gen_idem] using ReflTransGen.mono (fun _ _ ↦ ReflGen.to_reflTransGen) h
  · exact fun _ _ ↦ ReflTransGen.mono fun _ _ ↦ ReflGen.single

lemma Relation.ReflGen_eq {r : α → α → Prop} : ReflGen r = fun x y ↦ x = y ∨ r x y := by
  ext x y
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · induction h with
    | refl => exact Or.inl rfl
    | single hx => exact Or.inr hx
  · rcases h with ⟨rfl, h⟩
    · exact ReflGen.refl
    · exact ReflGen.single <| by assumption

lemma reflTransGen_wcovby_eq_reflTransGen_covby [PartialOrder α] :
    ReflTransGen ((· : α) ⩿ ·) = ReflTransGen (· ⋖ ·) := by
  simp_rw [wcovby_iff_eq_or_covby, ←ReflGen_eq, ReflTransGen.reflGen]

lemma le_iff_reflTransGen_covby [PartialOrder α] [LocallyFiniteOrder α] {x y : α} :
    x ≤ y ↔ Relation.ReflTransGen (· ⋖ ·) x y := by
  rw [le_iff_reflTransGen_wcovby, reflTransGen_wcovby_eq_reflTransGen_covby]

lemma monotone_iff_forall_covby [PartialOrder α] [LocallyFiniteOrder α] [Preorder β]
    (f : α → β) : Monotone f ↔ ∀ a b : α, a ⋖ b → f a ≤ f b := by
  refine ⟨fun hf _ _ h ↦ hf h.le, fun h a b hab ↦ ?_⟩
  simpa [Relation.reflTransGen_eq_self (r := ((· : β) ≤ ·)) IsRefl.reflexive transitive_le]
    using Relation.ReflTransGen.lift f h <| le_iff_reflTransGen_covby.mp hab

[Heather Macbeth]

@Jireh Loreaux Thank you for this nice lemma! I won't get to PR'ing it this weekend, but if you also don't I will put it on my to-do list.

[Jireh Loreaux]

@Heather Macbeth, @Eric Wieser, @Anatole Dedecker : #6709

[Yaël Dillies]

Jireh Loreaux said:

But Yaël, the key question is: is it Lean 3 or Lean 4? :smiley:

Currently Lean 3, haven't had time to port anything in the past month.