Computing Finset sort of Finset range

Stream: new members

[Andy Jiang]

Hi, I would like to prove the result that Finset sort of Finset range is List.range. But I'm unsure how to start

import Mathlib
theorem finset_sorted_range {k : ℕ} (i : Fin k) :
  (Finset.sort (. ≤ .) (Finset.range k)) = List.range k := by
  sorry

Like do I have to use the mergesort definition. Or is there some theorem in Mathlib that two lists are the same if they are both sorted, nodup and have the same Finset?

[Yaël Dillies]

Weirdly enough, the lemma for Finset.sort is missing, but we do have docs#List.mergeSort_eq_self

[Andy Jiang]

so am I stuck having to prove it from the definitions of mergesort?

[Andy Jiang]

it's a bit confusing to me that there's no characterizations proven for Finset sort? How is it used in other places? do they prove things using mergesort definition?

[Ruben Van de Velde]

Maybe this helps break it down:

import Mathlib

theorem bar (s t : List ℕ) (h : List.Perm s t) (hs : List.Sorted (· ≤ ·) s) (ht : List.Sorted (· ≤ ·) t) : s = t := by
  apply List.eq_of_perm_of_sorted h hs ht

#check List.sorted_cons
theorem foo {α : Type uu} {r : α → α → Prop} {a : α} {l : List α} :
    List.Sorted r (l ++ [a]) ↔ (∀ b ∈ l, r b a) ∧ List.Sorted r l := by
  sorry

theorem Finset.sort_insert (s : Finset ℕ) (x : ℕ) (h : ∀ y ∈ s, y ≤ x) (hx : x ∉ s) :
    Finset.sort (· ≤ ·) (insert x s) = Finset.sort (· ≤ ·) s ++ [x] := by
  rw [←Finset.cons_eq_insert]
  swap; exact hx
  apply bar
  swap
  exact sort_sorted _ _
  swap
  rw [foo]
  constructor
  · intro b hb
    simp at hb
    apply h _ hb
  exact sort_sorted _ _
  apply (Finset.sort_perm_toList _ _).trans
  apply (Finset.toList_cons hx).trans
  apply List.Perm.trans _ (List.perm_append_singleton _ _).symm
  rw [List.perm_cons]
  apply (Finset.sort_perm_toList _ _).symm


theorem finset_sorted_range {k : ℕ} :
    (Finset.sort (. ≤ .) (Finset.range k)) = List.range k := by
  induction k with
  | zero => simp
  | succ n ih =>
  rw [@Finset.range_succ]
  rw [List.range_succ]
  rw [← ih]
  rw [Finset.sort_insert]
  intro y
  simpa using le_of_lt
  simp

[Ruben Van de Velde]

Also apparently missing: the reverse of a sorted list is sorted in the other direction

[Andy Jiang]

Ah thank you! right I forgot that List.eq_of_perm_of_sorted allows proofs to reduce to showing perm--which then can be done with Finset.sort_perm_toList. Will try to finish the proof from here and reply with the full code after.

[Andy Jiang]

Below is a completed file

import Mathlib

theorem bar {α : Type u_1} (r : α → α → Prop) [DecidableEq α]
    [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r]
    (s t : List α) (h : List.Perm s t) (hs : List.Sorted r s) (ht : List.Sorted r t) : s = t := by
  apply List.eq_of_perm_of_sorted h hs ht

theorem list_pairwise_join_iff {α : Type*} {r : α → α → Prop} {l1 l2 : List α}:
    (l1++l2).Pairwise r ↔ (l1.Pairwise r) ∧ (l2.Pairwise r) ∧ (∀ {x y : α} (_ : x ∈ l1) (_: y ∈ l2), (r x y)) := by
  match l1 with
  | [] => simp
  | x :: xs =>
    simp [List.Pairwise]
    let h := @list_pairwise_join_iff α r xs l2
    simp_rw [h]
    --pure tautology from here
    apply Iff.intro
    intro ⟨h1,h2,h3,h4⟩
    apply And.intro
    apply And.intro
    exact (λ {u : α} (h : u ∈ xs) => h1 u (Or.inl h))
    exact h2
    apply And.intro
    exact h3
    intro u v
    intro h5
    cases h5 with
    | inl h5a => rw [h5a];exact (λ (h : v ∈ l2) => h1 v (Or.inr h))
    | inr h5b => exact (λ (h : v ∈ l2) => h4 h5b h)
    intro ⟨⟨g1,g2⟩,g3,g4⟩
    apply And.intro
    intro u
    intro g5
    cases g5 with
    | inl g6a => exact g1 u g6a;
    | inr g6b => exact g4 (Or.inl (refl x)) g6b
    apply And.intro
    exact g2
    apply And.intro
    exact g3
    exact (λ {u v : α} (h : u ∈ xs)(g : v ∈ l2) => g4 (Or.inr h) g)

theorem foo {α : Type*} {r : α → α → Prop} {a : α} {l : List α} :
    List.Sorted r (l ++ [a]) ↔ (∀ b ∈ l, r b a) ∧ List.Sorted r l := by
  unfold List.Sorted
  rw [list_pairwise_join_iff]
  --tautology + a ∈ [a] from here on
  apply Iff.intro
  intro ⟨h1,_,h3⟩
  apply And.intro
  intro u h4
  exact h3 h4 (List.mem_singleton.mpr (refl _))
  exact h1
  intro ⟨g1,g2⟩
  apply And.intro
  exact g2
  apply And.intro
  simp [List.Pairwise]
  intro u v g3 g4
  rw [List.mem_singleton] at g4
  rw [g4]
  exact g1 u g3

theorem Finset.sort_insert {α : Type u_1} (r : α → α → Prop) [DecidableEq α]
    [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] (s : Finset α)
    (x : α) (h : ∀ y ∈ s, r y x) (hx : x ∉ s) :
    Finset.sort (r) (insert x s) = Finset.sort r s ++ [x] := by
  rw [←Finset.cons_eq_insert]
  swap; exact hx
  apply bar r
  swap
  exact sort_sorted _ _
  swap
  rw [foo]
  constructor
  · intro b hb
    simp at hb
    apply h _ hb
  exact sort_sorted _ _
  apply (Finset.sort_perm_toList _ _).trans
  apply (Finset.toList_cons hx).trans
  apply List.Perm.trans _ (List.perm_append_singleton _ _).symm
  rw [List.perm_cons]
  apply (Finset.sort_perm_toList _ _).symm


theorem finset_sorted_range {k : ℕ} :
    (Finset.sort (. ≤ .) (Finset.range k)) = List.range k := by
  induction k with
  | zero => simp
  | succ n ih =>
  rw [@Finset.range_succ]
  rw [List.range_succ]
  rw [← ih]
  rw [Finset.sort_insert]
  intro y
  simpa using le_of_lt
  simp

[Andy Jiang]

I've also collected a bunch of for me useful List 'theorems' below. If people are interested I can try to improve it to make it includ-able in Mathlib? But I really don't know what the requirements are
cont'd from above

theorem filter_sorted {α : Type u_1} (r : α → α → Prop)
    [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] (f : α → Bool)
    (l : List α) (h : List.Sorted r l) :
    List.Sorted r (List.filter f l) := by
  match l with
  | [] => simp
  | x :: xs =>
    unfold List.filter
    cases (f x)
    simp
    exact filter_sorted r f xs (List.Sorted.of_cons h)
    simp
    apply And.intro
    intro b hb
    have hb2 : b ∈ xs := List.mem_of_mem_filter hb
    simp [List.Sorted] at h
    let ⟨h1,_⟩ := h
    exact h1 b hb2
    exact filter_sorted r f xs (List.Sorted.of_cons h)


theorem filter_nodup {α : Type u_1} [DecidableEq α] (f : α → Bool)
    (l : List α) (h : List.Nodup l) :
    List.Nodup (List.filter f l) := by
  match l with
  | [] => simp
  | x :: xs =>
    unfold List.filter
    cases (f x)
    simp
    exact filter_nodup f xs (List.Nodup.of_cons h)
    simp
    apply And.intro
    intro h2
    simp at h
    have : x ∈ xs := List.mem_of_mem_filter h2
    tauto
    exact filter_nodup f xs (List.Nodup.of_cons h)

theorem list_filter_to_finset {α : Type*} [DecidableEq α] (l : List α) (f : α → Bool):
    List.toFinset (List.filter f l) = Finset.filter (λ x => f x) (List.toFinset l) := by
  match l with
  | [] => simp
  | x :: xs =>
    rw [List.toFinset_cons]
    unfold List.filter
    rw [Finset.filter_insert]
    cases (f x)
    simp
    exact list_filter_to_finset xs f
    simp
    rw [list_filter_to_finset xs f]

theorem finset_filter_sort_commute {α : Type u_1} [DecidableEq α] (r : α → α → Prop)
    [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] (f : α → Prop) [DecidablePred f]
    (s : Finset α) :
    Finset.sort r (Finset.filter (λ x => f x) s) = List.filter f (Finset.sort r s) := by
  have h1: List.Sorted r (Finset.sort r (Finset.filter (fun x => f x) s)) := by simp
  have h2: List.Sorted r (List.filter f (Finset.sort r s)) := by
    apply filter_sorted r f (Finset.sort r s)
    exact Finset.sort_sorted r s
  apply List.eq_of_perm_of_sorted _ h1 h2
  apply List.perm_of_nodup_nodup_toFinset_eq
  exact Finset.sort_nodup r (Finset.filter f s)
  apply filter_nodup
  exact Finset.sort_nodup r s
  rw [Finset.sort_toFinset]
  rw [list_filter_to_finset]
  simp

def list_truncate_tail {α : Type*} (l : List α) (b: Fin (l.length+1)) : List α :=
  match l with
  | [] => []
  | x :: xs =>
    match b with
    |⟨Nat.zero,_⟩ => []
    |⟨Nat.succ n,h⟩ => (x :: (list_truncate_tail xs ⟨n,by
      simp [List.length] at h
      omega
    ⟩))


theorem list_truncate_tail_zero {α : Type*} (l : List α) :
    list_truncate_tail l 0 = [] := by
  match l with
    | [] => rfl
    | x :: xs =>
      simp [list_truncate_tail]
      rfl

theorem list_truncate_tail_length {α : Type*} (l : List α) (b: Fin (l.length+1)) :
List.length (list_truncate_tail l b) = b := by
  match l with
  | [] => simp [list_truncate_tail]
  | x :: xs =>
    simp [list_truncate_tail]
    match b with
    |⟨Nat.zero,_⟩ => simp
    |⟨Nat.succ n,h⟩ =>
      simp
      exact list_truncate_tail_length xs ⟨n,by exact Nat.succ_lt_succ_iff.mp h⟩


def list_truncate_head {α : Type*} (l : List α) (a: Fin (l.length+1)) : List α :=
  match l with
  | [] => []
  | x :: xs =>
    match a with
    |⟨Nat.zero,_⟩ => x::xs
    |⟨Nat.succ n,h⟩ => list_truncate_head xs ⟨n,by
      simp [List.length] at h
      exact Nat.succ_lt_succ_iff.mp h
    ⟩

theorem list_filter_eval_false {α : Type*} {l : List α}{f : α → Prop}[DecidablePred f]
    (h : (∀ (a : α),(a ∈ l) → ¬ (f a))) : List.filter f l = []:= by
  match l with
  |[] => simp
  |x :: xs =>
    simp [List.filter]
    rw [Bool.decide_false]
    simp
    apply list_filter_eval_false
    intro x_1 h_1
    simp at h
    tauto
    have h_2 : x ∈ (x :: xs) := by simp
    exact h x h_2

theorem list_filter_eval_true {α : Type*} {l : List α}{f : α → Prop}[DecidablePred f]
    (h : (∀ (a : α),(a ∈ l) → (f a))) :List.filter f l = l := by
  match l with
  |[] => simp
  |x :: xs =>
    simp [List.filter]
    rw [Bool.decide_true]
    simp
    apply list_filter_eval_true
    intro x_1 h_1
    simp at h
    tauto
    have h_2 : x ∈ (x :: xs) := by simp
    exact h x h_2

theorem list_get_mem {α : Type*} (l : List α)(i : Fin (l.length)): l.get i ∈ l:= by
  match l with
  |[] =>
    let h := i.isLt
    simp at h
  |x :: xs =>
    match i with
    |⟨Nat.zero,_⟩ => simp
    |⟨Nat.succ n,h⟩ =>
    simp
    apply Or.inr
    apply (@list_get_mem α xs ⟨n,by simp [List.length] at h;omega⟩)

theorem sorted_list_le_entry_lemma {α : Type*} [DecidableEq α] (r : α → α → Prop)
    [DecidableRel r] [hr : IsRefl α r] [IsTrans α r] [has : IsAntisymm α r] [IsTotal α r] (l : List α)
    (h : 0 < l.length)(g : List.Sorted r l)(g2 : List.Nodup l):
    List.filter (λ u => r u (List.get l ⟨0,h⟩)) l = list_truncate_tail l ⟨1, Nat.lt_add_of_pos_left h⟩ := by
  match l with
  |[] => unfold list_truncate_tail;simp
  |x :: xs =>
    unfold list_truncate_tail
    simp
    rw [list_truncate_tail_zero]
    simp [List.filter]
    have : Decidable.decide (r x x) = true := by
      let l := hr.refl x
      apply Bool.decide_true
      exact l
    simp_rw [this]
    have h1: List.filter (fun x_1 => decide (r x_1 x)) xs = [] := by
      rw [List.sorted_cons] at g
      let g1:= g.left
      apply list_filter_eval_false
      intro x_2 h_2
      intro h3
      have h4:= has.antisymm x_2 x h3 (g1 x_2 h_2)
      simp at g2
      rw [h4] at h_2
      tauto
    simp
    exact h1

--note that if you put l[i] in the definition here it will not pattern match
theorem sorted_list_le_entry {α : Type*} [DecidableEq α] (r : α → α → Prop)
    [DecidableRel r] [hr : IsRefl α r] [IsTrans α r] [has:IsAntisymm α r] [IsTotal α r]
    (l : List α) (i : Fin l.length)(g : List.Sorted r l)(g2 : List.Nodup l):
    List.filter (r . (l.get i)) l =
      list_truncate_tail l (⟨i.val+1,by let h := i.isLt;exact Nat.add_lt_add_right h 1⟩) := by
  match l with
    |[] => simp;unfold list_truncate_tail;rfl
    |t :: ts =>
      match i with
      |⟨Nat.zero,h⟩ =>
        apply sorted_list_le_entry_lemma
        exact g
        exact g2
      |⟨Nat.succ n,h⟩ =>
        simp
        simp [List.filter]
        let nindex : Fin (ts.length) := ⟨n,by simp [List.length] at h;omega⟩
        have : r t (ts[nindex]) := by
          simp [List.Sorted] at g
          apply g.left
          apply list_get_mem
        rw [Bool.decide_true]
        simp
        simp [list_truncate_tail]
        swap
        exact this
        apply sorted_list_le_entry
        rw [List.sorted_cons] at g
        exact g.right
        rw [List.nodup_cons] at g2
        exact g2.right

theorem list_sort_characterization{α : Type*} [DecidableEq α] (r : α → α → Prop)
    [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] (l : List α) (h : List.Sorted r l)
    (g : List.Nodup l):
    ∀ (i : Fin (l.length)), List.length (List.filter (r . (List.get l i)) l) = (i+1) := by
  intro i
  rw [sorted_list_le_entry]
  apply list_truncate_tail_length
  exact h
  exact g

theorem list_whose_finset_is_singleton {α : Type} [DecidableEq α] (lst : List α) (x : α)
    (h : lst.toFinset ⊆ {x}) : lst = List.replicate lst.length x := by
  match lst with
  | [] => simp
  | y::ys =>
    have h₁ : y = x := by
      have : y ∈ (y::ys).toFinset := by
        rw [List.mem_toFinset]; simp
      have : y ∈ {x} := by exact h this
      simp at this
      exact this
    have h₂ : ys.toFinset ⊆ {x} := by
      simp at h
      rw [← h]
      exact Finset.subset_insert y ys.toFinset
    have ih : ys = List.replicate ys.length x := list_whose_finset_is_singleton ys x h₂
    rw [h₁, ih]
    simp

theorem list_map_toFinset {α : Type u_1} {β : Type u_2} {f : α ↪ β} [DecidableEq α] [DecidableEq β] {s : List α} :
  Finset.map f (List.toFinset s) = List.toFinset (List.map (↑f) s) := by
  match s with
  | [] => simp
  | y::ys =>
    simp
    rw [list_map_toFinset]

theorem sort_monotone_map {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β]
 (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r]
  (s : β → β → Prop) [DecidableRel s] [IsTrans β s] [IsAntisymm β s] [IsTotal β s]
    (f : α ↪ β) (preserve_lt : {x : α} → {y : α} → (h : r x y) → (s (f x) (f y)))
    (fst : Finset α): Finset.sort s (Finset.map f fst) = List.map f (Finset.sort r fst) := by
  let lst := Finset.sort r fst
  have lst_sorted : List.Sorted r lst := Finset.sort_sorted r fst
  have RHS_sorted : List.Sorted s (List.map f lst) := by
    apply List.pairwise_map.mpr
    unfold List.Sorted at lst_sorted
    exact List.Pairwise.imp preserve_lt lst_sorted
  have LHS_nodup : List.Nodup (Finset.sort s (Finset.map f fst)) := Finset.sort_nodup s (Finset.map f fst)
  have RHS_nodup : List.Nodup (List.map f (Finset.sort r fst)) := by
    apply List.Nodup.map
    exact Function.Embedding.injective f
    exact Finset.sort_nodup r fst
  have h₂ : (Finset.sort s (Finset.map f fst)).toFinset = (List.map f (Finset.sort r fst)).toFinset := by
    simp
    rw [← list_map_toFinset]
    simp
  have LHS_sorted : List.Sorted s (Finset.sort s (Finset.map f fst)) :=  Finset.sort_sorted s (Finset.map f fst)

  rw [List.toFinset_eq_iff_perm_dedup] at h₂
  rw [List.Nodup.dedup] at h₂
  rw [List.Nodup.dedup] at h₂
  exact List.eq_of_perm_of_sorted h₂ LHS_sorted RHS_sorted
  tauto
  tauto

[Ruben Van de Velde]

Skimming quickly, those seem useful if they don't exist yet. The proofs need a bit of work to be a little less verbose and more maintainable, but you could already create a pull request on mathlib. You'd need push access if you don't have it yet

[Andy Jiang]

OK thanks I'll try to simplify the proofs a little and try to do a pull request