<commit_before>/-
Copyright (c) 2016 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/
import data.list.perm

/-!
# Sorting algorithms on lists

In this file we define `list.sorted r l` to be an alias for `pairwise r l`. This alias is preferred
in the case that `r` is a `<` or `≤`-like relation. Then we define two sorting algorithms:
`list.insertion_sort` and `list.merge_sort`, and prove their correctness.
-/

open list.perm

universe uu

namespace list

/-!
### The predicate `list.sorted`
-/

section sorted

variables {α : Type uu} {r : α → α → Prop}

/-- `sorted r l` is the same as `pairwise r l`, preferred in the case that `r`
  is a `<` or `≤`-like relation (transitive and antisymmetric or asymmetric) -/
def sorted := @pairwise

instance decidable_sorted [decidable_rel r] (l : list α) : decidable (sorted r l) :=
list.decidable_pairwise _

@[simp] theorem sorted_nil : sorted r [] := pairwise.nil

theorem sorted_of_sorted_cons {a : α} {l : list α} : sorted r (a :: l) → sorted r l :=
pairwise_of_pairwise_cons

theorem sorted.tail {r : α → α → Prop} {l : list α} (h : sorted r l) : sorted r l.tail :=
h.tail

theorem rel_of_sorted_cons {a : α} {l : list α} : sorted r (a :: l) →
  ∀ b ∈ l, r a b :=
rel_of_pairwise_cons

@[simp] theorem sorted_cons {a : α} {l : list α} :
  sorted r (a :: l) ↔ (∀ b ∈ l, r a b) ∧ sorted r l :=
pairwise_cons

protected theorem sorted.nodup {r : α → α → Prop} [is_irrefl α r] {l : list α} (h : sorted r l) :
  nodup l :=
h.nodup

theorem eq_of_perm_of_sorted [is_antisymm α r]
  {l₁ l₂ : list α} (p : l₁ ~ l₂) (s₁ : sorted r l₁) (s₂ : sorted r l₂) : l₁ = l₂ :=
begin
  induction s₁ with a l₁ h₁ s₁ IH generalizing l₂,
  { exact p.nil_eq },
  { have : a ∈ l₂ := p.subset (mem_cons_self _ _),
    rcases mem_split this with ⟨u₂, v₂, rfl⟩,
    have p' := (perm_cons a).1 (p.trans perm_middle),
    have := IH p' (pairwise_of_sublist (by simp) s₂), subst l₁,
    change a::u₂ ++ v₂ = u₂ ++ ([a] ++ v₂), rw ← append_assoc, congr,
    have : ∀ (x : α) (h : x ∈ u₂), x = a := λ x m,
      antisymm ((pairwise_append.1 s₂).2.2 _ m a (mem_cons_self _ _))
        (h₁ _ (by simp [m])),
    rw [(@eq_repeat _ a (length u₂ + 1) (a::u₂)).2,
        (@eq_repeat _ a (length u₂ + 1) (u₂++[a])).2];
    split; simp [iff_true_intro this, or_comm] }
end

@[simp] theorem sorted_singleton (a : α) : sorted r [a] := pairwise_singleton _ _
<commit_msg>feat(data/list/sort): subperm sorted implies sublist (#10892)<commit_after>/-
Copyright (c) 2016 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/
import data.list.perm

/-!
# Sorting algorithms on lists

In this file we define `list.sorted r l` to be an alias for `pairwise r l`. This alias is preferred
in the case that `r` is a `<` or `≤`-like relation. Then we define two sorting algorithms:
`list.insertion_sort` and `list.merge_sort`, and prove their correctness.
-/

open list.perm

universe uu

namespace list

/-!
### The predicate `list.sorted`
-/

section sorted

variables {α : Type uu} {r : α → α → Prop}

/-- `sorted r l` is the same as `pairwise r l`, preferred in the case that `r`
  is a `<` or `≤`-like relation (transitive and antisymmetric or asymmetric) -/
def sorted := @pairwise

instance decidable_sorted [decidable_rel r] (l : list α) : decidable (sorted r l) :=
list.decidable_pairwise _

@[simp] theorem sorted_nil : sorted r [] := pairwise.nil

theorem sorted_of_sorted_cons {a : α} {l : list α} : sorted r (a :: l) → sorted r l :=
pairwise_of_pairwise_cons

theorem sorted.tail {r : α → α → Prop} {l : list α} (h : sorted r l) : sorted r l.tail :=
h.tail

theorem rel_of_sorted_cons {a : α} {l : list α} : sorted r (a :: l) →
  ∀ b ∈ l, r a b :=
rel_of_pairwise_cons

@[simp] theorem sorted_cons {a : α} {l : list α} :
  sorted r (a :: l) ↔ (∀ b ∈ l, r a b) ∧ sorted r l :=
pairwise_cons

protected theorem sorted.nodup {r : α → α → Prop} [is_irrefl α r] {l : list α} (h : sorted r l) :
  nodup l :=
h.nodup

theorem eq_of_perm_of_sorted [is_antisymm α r]
  {l₁ l₂ : list α} (p : l₁ ~ l₂) (s₁ : sorted r l₁) (s₂ : sorted r l₂) : l₁ = l₂ :=
begin
  induction s₁ with a l₁ h₁ s₁ IH generalizing l₂,
  { exact p.nil_eq },
  { have : a ∈ l₂ := p.subset (mem_cons_self _ _),
    rcases mem_split this with ⟨u₂, v₂, rfl⟩,
    have p' := (perm_cons a).1 (p.trans perm_middle),
    have := IH p' (pairwise_of_sublist (by simp) s₂), subst l₁,
    change a::u₂ ++ v₂ = u₂ ++ ([a] ++ v₂), rw ← append_assoc, congr,
    have : ∀ (x : α) (h : x ∈ u₂), x = a := λ x m,
      antisymm ((pairwise_append.1 s₂).2.2 _ m a (mem_cons_self _ _))
        (h₁ _ (by simp [m])),
    rw [(@eq_repeat _ a (length u₂ + 1) (a::u₂)).2,
        (@eq_repeat _ a (length u₂ + 1) (u₂++[a])).2];
    split; simp [iff_true_intro this, or_comm] }
end

theorem sublist_of_subperm_of_sorted [is_antisymm α r]
  {l₁ l₂ : list α} (p : l₁ <+~ l₂) (s₁ : l₁.sorted r) (s₂ : l₂.sorted r) : l₁ <+ l₂ :=
let ⟨_, h, h'⟩ := p in by rwa ←list.eq_of_perm_of_sorted h (list.pairwise_of_sublist h' s₂) s₁

@[simp] theorem sorted_singleton (a : α) : sorted r [a] := pairwise_singleton _ _

{'fraction_non_alphanumeric': 0.1447063369397218, 'fraction_numerical': 0.006375579598145286, 'mean_word_length': 3.229575163398693, 'pattern_counts': {'":': 0, '<': 13, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1038320', 'n_tokens_mistral': 2187, 'n_tokens_neox': 2166, 'n_words': 767}