List.Sorted.cons

Stream: Is there code for X?

[Violeta Hernández]

If a :: l is sorted under a transitive relation r and r b a, then b :: a :: l is sorted too.

[Violeta Hernández]

Do we have this?

[Violeta Hernández]

Here's a quick proof I cooked up. No idea why rintro refuses to name my assumption.

import Mathlib.Data.List.Sort

theorem List.Sorted.cons {r : α → α → Prop} [IsTrans α r] {l : List α} {a b : α}
    (ha : Sorted r (a :: l)) (h : r b a) : Sorted r (b :: a :: l) := by
  refine List.pairwise_cons.2 ⟨?_, ha⟩
  rintro c (_ | _)
  · exact h
  · apply trans h
    apply rel_of_sorted_cons ha
    assumption

[Ruben Van de Velde]

The one where you put an underscore?

[Violeta Hernández]

Yeah, even if I put variable names in there they don't show up on the second goal

[Ruben Van de Velde]

Huh. I'd look, but I'm on my phone and it's not a mwe

[Violeta Hernández]

Oh, let me fix that real quick

[Eric Wieser]

Golfed a little:

theorem List.Sorted.cons {r : α → α → Prop} [IsTrans α r] {l : List α} {a b : α}
    (ha : Sorted r (a :: l)) (h : r b a) : Sorted r (b :: a :: l) :=
  Pairwise.cons (forall_mem_cons.2 ⟨h, fun _ hx => _root_.trans h <| rel_of_sorted_cons ha _ hx⟩) ha

[Ruben Van de Velde]

import Mathlib.Data.List.Sort

theorem List.Sorted.cons {r : α → α → Prop} [IsTrans α r] {l : List α} {a b : α}
    (ha : Sorted r (a :: l)) (h : r b a) : Sorted r (b :: a :: l) := by
  refine List.pairwise_cons.2 ⟨?_, ha⟩
  simp only [mem_cons]
  rintro c (rfl | hc)
  · exact h
  · apply trans h
    apply rel_of_sorted_cons ha
    apply hc

Looks like it probably has to do with the definition of Mem

[Violeta Hernández]

Forgot to link the PR, #15914

[Violeta Hernández]

Speaking of lemmas about lists, do we have this? If Sorted (<) l and StrictMono f, then Sorted (<) (l.map f)

[Eric Wieser]

theorem List.Sorted.map {α β} {l : List α} (f : α → β) {ra : α → α → Prop} (rb : β → β → Prop)
    (hf : ∀ a ∈ l, ∀ b ∈ l, ra a b → rb (f a) (f b)) (h : l.Sorted ra) :
    (l.map f).Sorted rb :=
  match l with
  | [] => by simp
  | x :: xs => by
    simp only [List.sorted_cons, List.map, List.mem_map, forall_exists_index, and_imp,
      forall_apply_eq_imp_iff₂] at h ⊢
    simp_rw [List.forall_mem_cons] at hf
    exact ⟨fun a ha => hf.1.2 _ ha (h.1 _ ha), h.2.map _ _ <| fun a ha b hb => (hf.2 _ ha).2 _ hb⟩

[Eric Wieser]

Oh, I guess this is just a stronger version of docs#List.Pairwise.map

[Giacomo Stevanato]

Here's a simplier proof of List.Sorted.cons using List.Chain:

import Mathlib.Data.List.Sort
import Mathlib.Data.List.Chain

theorem List.Sorted.cons {r : α → α → Prop} [IsTrans α r] {l : List α} {a b : α}
    (ha : Sorted r (a :: l)) (h : r b a) : Sorted r (b :: a :: l) := by
  rw [Sorted, ←List.chain_iff_pairwise] at *
  exact List.Chain.cons h ha

[Violeta Hernández]

Can we do this in reverse? That is, use List.Sorted.cons to golf List.Chain.cons?

[Giacomo Stevanato]

No, because List.Chain.cons is a constructor

[Giacomo Stevanato]

You might be able to use List.Sorted.cons to prove List.chain_iff_pairwise though

[Giacomo Stevanato]

Now that I think about it though, shouldn't this be List.Pairwise.cons instead of List.Sorted.cons?

[Giacomo Stevanato]

Nevermind, List.Pairwise.cons as a name is already taken, though it could be List.Pairwise.trans_cons or something like that.