qsort.lean

import init data.list data.nat
open nat list eq.ops

lemma filter_length_bound {p : nat → Prop} [h : decidable_pred p] : ∀ {xs : list nat}, length (filter p xs) ≤ length xs
| [] := by simp
| (x::xs) := match decidable.em (p x) with
  | (or.inl px) := calc
    length (filter p (x::xs)) = length (x :: filter p xs) : !filter_cons_of_pos px ▸ rfl
    ... = length (filter p xs) + 1 : by simp
    ... ≤ length xs + 1 : add_le_add_right !filter_length_bound 1
    ... ≤ length (x::xs) : by simp
  | (or.inr npx) := calc
    length (filter p (x::xs)) = length (filter p xs) : !filter_cons_of_neg npx ▸ rfl
    ... ≤ length xs : !filter_length_bound
    ... ≤ length xs + 1 : !le_add_right
    ... ≤ length (x::xs) : by simp
  end

lemma length_cons {x n : nat} {xs : list nat} : length (x :: xs) ≤ n + 1 → length xs ≤ n := λp, calc
  length xs = length (x :: xs) - 1 : by simp
  ... ≤ n + 1 - 1 : nat.sub_le_sub_right p 1
  ... ≤ n : by simp

definition qsort' : ∀ (n : nat) (xs : list nat), length xs ≤ n → list nat
| n [] p := []
| 0 (x::xs) p := absurd (eq_nil_of_length_eq_zero (eq_zero_of_le_zero p)) !cons_ne_nil
| (n+1) (x::xs) p :=
  qsort' n (filter (λt, t ≤ x) xs) (le.trans !filter_length_bound (!length_cons p)) ++ [x] ++
  qsort' n (filter (λt, x < t) xs) (le.trans !filter_length_bound (!length_cons p))

definition qsort : list nat → list nat := λxs, qsort' (length xs) xs (le.nat_refl _)

definition is_sorted : list nat → Prop
| [] := true
| [a] := true
| (a::b::xs) := a ≤ b ∧ is_sorted (b::xs)

lemma is_sorted.nil_iff : is_sorted [] ↔ true := iff.rfl
lemma is_sorted.nil : is_sorted [] := iff.mpr is_sorted.nil_iff trivial
lemma is_sorted.singleton_iff {a : nat} : is_sorted [a] ↔ true := iff.rfl
lemma is_sorted.singleton {a : nat} : is_sorted [a] := iff.mpr is_sorted.singleton_iff trivial
lemma is_sorted.step_iff {a b : nat} {xs : list nat} : is_sorted (a::b::xs) ↔ a ≤ b ∧ is_sorted (b::xs) := iff.rfl
lemma is_sorted.step {a b : nat} {xs : list nat} : is_sorted (a::b::xs) → a ≤ b ∧ is_sorted (b::xs) := iff.mpr is_sorted.step_iff

definition occs : nat → list nat → nat
| a [] := 0
| a (x::xs) := if a = x then 1 + occs a xs else occs a xs

lemma occs.nil {a} : occs a [] = 0 := rfl
lemma occs.if_pos {a x xs} : a = x → occs a (x::xs) = 1 + occs a xs := by intros; rewrite [↑occs, if_pos a_1]
lemma occs.if_neg {a x xs} : a ≠ x → occs a (x::xs) = occs a xs := by intros; rewrite [↑occs, if_neg a_1]

definition is_perm : list nat → list nat → Prop
| xs ys := ∀ a, occs a xs = occs a ys

infix ~ := is_perm

theorem is_perm.refl [refl] : ∀ (l : list nat), l ~ l := λl a, rfl
theorem is_perm.symm [symm] : ∀ {l₁ l₂ : list nat}, l₁ ~ l₂ → l₂ ~ l₁ := λl₁ l₂ l₁₂ a, by rewrite (l₁₂ a)
theorem is_perm.trans [trans] : ∀ {l₁ l₂ l₃ : list nat}, is_perm l₁ l₂ → is_perm l₂ l₃ → is_perm l₁ l₃ := λl₁ l₂ l₃ l₁₂ l₂₃ a, l₁₂ a ⬝ l₂₃ a

definition is_sorted.cons : ∀ {a} {xs}, is_sorted xs → (∀b, b ∈ xs → a ≤ b) → is_sorted (a::xs)
| a [] sxs p := is_sorted.singleton
| a (x::xs) sxs p := and.intro (p x !mem_cons) sxs

lemma lem6_3 {a : nat} : ∀ {xs ys : list nat}, is_sorted xs ∧ is_sorted ys ∧ (∀b, b ∈ xs → b ≤ a) ∧ (∀b, b ∈ ys → a ≤ b) → is_sorted (xs ++ [a] ++ ys)
| [] [] _ := !is_sorted.singleton
| [] (y::ys) (and.intro _ (and.intro sys (and.intro _ pys))) := iff.mpr is_sorted.step_iff (and.intro (pys y !mem_cons) sys)
| [x] ys (and.intro _ (and.intro sys (and.intro pyx pys))) := is_sorted.cons (is_sorted.cons sys pys) (λb bin, or.elim
  (eq_or_mem_of_mem_cons bin)
  (λba, by rewrite ba; apply (pyx x !mem_cons)) (λbinys, calc
    x ≤ a : pyx _ !mem_cons
    ... ≤ b : pys b binys))
| (x₁::x₂::xs) ys (and.intro sxs (and.intro sys (and.intro pxs pys))) :=
  iff.mpr is_sorted.step_iff (and.intro (and.left sxs)
    (@lem6_3 (x₂::xs) ys (and.intro (and.right sxs) (and.intro sys (and.intro (λb bin, pxs b (!mem_cons_of_mem bin)) pys)))))

lemma lem6_2_6 : ∀ {a : nat} {xs : list nat}, a ∈ xs ↔ occs a xs > 0
| a [] := iff.intro (λain, absurd ain !not_mem_nil) (λnp, by rewrite occs.nil at np; apply lt.irrefl 0; assumption)
| a (x::xs) := iff.intro
  (λain, match decidable.em (a = x) with
    | (or.inl ax) := by rewrite [occs.if_pos ax]; apply (add_pos_left zero_lt_one)
    | (or.inr nax) := calc
      occs a (x::xs) = occs a xs : occs.if_neg nax
      ... > 0 : iff.elim_left lem6_2_6 (begin
        rewrite mem_cons_iff at ain, cases ain,
          contradiction,
          assumption
        end)
    end)
  (λpo, match decidable.em (a = x) with
    | (or.inl ax) := ax ▸ !mem_cons
    | (or.inr nax) :=
      begin
        rewrite mem_cons_iff,
        right, rewrite [↑occs at po, if_neg nax at po],
        rewrite lem6_2_6, assumption
      end
    end)

lemma lem6_2_7 : ∀ {xs ys : list nat}, is_perm xs ys → ∀x, x ∈ xs ↔ x ∈ ys := λxs ys ip x, calc
  x ∈ xs ↔ occs x xs > 0 : !lem6_2_6
  ... ↔ occs x ys > 0 : by rewrite (ip x)
  ... ↔ x ∈ ys : !lem6_2_6

lemma lem6_2_2 {x y : nat} : x ≤ y ∨ x > y :=
  or.elim (@nat.le_total x y) or.inl (λyx, match decidable.em (x = y) with
    | or.inl xy := or.inl (by rewrite xy)
    | or.inr nxy := or.inr (nat.lt_of_le_and_ne yx (ne.symm nxy))
    end)

lemma lem6_2_3 : ∀ {x y : nat}, ¬ (x ≤ y ∧ x > y) := proof
  take x y p,
  have h : y < y, from calc
    y < x : and.right p
    ... ≤ y : and.left p,
  show false, from lt.irrefl _ h
qed

lemma nat_ord_exm : ∀ {x y : nat}, (x ≤ y ∧ ¬ (y < x)) ∨ (y < x ∧ ¬ (x ≤ y)) := λx y, or.elim (@lem6_2_2 x y)
  (λxy, or.inl (and.intro xy (by intro; apply (@lem6_2_3 x y); simp)))
  (λxy, or.inr (and.intro xy (by intro; apply (@lem6_2_3 x y); simp)))

lemma lem6_2_8 {a : nat} : ∀ {xs ys : list nat}, occs a (xs ++ ys) = occs a xs + occs a ys
| [] ys := calc
  occs a ([] ++ ys) = occs a ys : rfl
  ... = 0 + occs a ys : by simp
  ... = occs a [] + occs a ys : occs.nil
| (x::xs) ys := match decidable.em (a = x) with
  | (or.inl ax) := calc
  occs a (x :: xs ++ ys) = 1 + occs a (xs ++ ys) : occs.if_pos ax
  ... = 1 + occs a xs + occs a ys : by rewrite lem6_2_8; simp
  ... = occs a (x::xs) + occs a ys : occs.if_pos ax
  | (or.inr nax) := calc
  occs a (x :: xs ++ ys) = occs a (xs ++ ys) : occs.if_neg nax
  ... = occs a xs + occs a ys : lem6_2_8
  ... = occs a (x::xs) + occs a ys : occs.if_neg nax
  end

lemma lem6_2_9 : ∀ {xs ys zs : list nat} {a : nat}, is_perm (xs ++ ys) zs → is_perm (xs ++ [a] ++ ys) (a :: zs)
| [] ys zs a := λyz c, calc
  occs c (nil ++ a :: ys) = occs c ([a] ++ ys) : rfl
  ... = occs c [a] + occs c ys : lem6_2_8
  ... = occs c [a] + occs c zs : yz c ▸ rfl
  ... = occs c (a :: zs) : lem6_2_8
| (x::xs) ys zs a := λxyz c, calc
    occs c (x :: xs ++ [a] ++ ys) = occs c (x :: xs ++ [a]) + occs c ys : !lem6_2_8
    ... = occs c (x :: xs) + occs c [a] + occs c ys : !lem6_2_8
    ... = occs c [a] + (occs c (x :: xs) + occs c ys) : by simp
    ... = occs c [a] + occs c ((x :: xs) ++ ys) : eq.symm !lem6_2_8
    ... = occs c [a] + occs c zs : xyz c ▸ rfl
    ... = occs c (a :: zs) : !lem6_2_8

lemma lem6_2_11 : ∀ {xs : list nat} {x : nat}, is_perm xs (filter (λt, t ≤ x) xs ++ filter (λt, x < t) xs)
| [] x := λa, rfl
| (x::xs) y := λa, eq.symm (calc
  occs a (filter (λ (t : ℕ), t ≤ y) (x :: xs) ++ filter (λ (t : ℕ), y < t) (x :: xs))
  = occs a [x] + occs a (filter (λ (t : ℕ), t ≤ y) xs ++ filter (λ (t : ℕ), y < t) xs) : match @nat_ord_exm x y with
    | (or.inl (and.intro xy nyx)) := calc
      occs a (filter (λ (a : ℕ), a ≤ y) (x :: xs) ++ filter (λ (a : ℕ), y < a) (x :: xs))
      = occs a (x :: filter (λ (a : ℕ), a ≤ y) xs ++ filter (λ (a : ℕ), y < a) (x :: xs)) : @filter_cons_of_pos nat _ _ x xs xy
      ... = occs a (x :: filter (λ (a : ℕ), a ≤ y) xs ++ filter (λ (a : ℕ), y < a) xs) : @filter_cons_of_neg nat _ _ x xs nyx
      ... = occs a [x] + occs a (filter (λ (a : ℕ), a ≤ y) xs ++ filter (λ (a : ℕ), y < a) xs) : lem6_2_8
    | (or.inr (and.intro xy nyx)) := calc
      occs a (filter (λ (a : ℕ), a ≤ y) (x :: xs) ++ filter (λ (a : ℕ), y < a) (x :: xs))
      = occs a (filter (λ (a : ℕ), a ≤ y) xs ++ filter (λ (a : ℕ), y < a) (x :: xs)) : @filter_cons_of_neg nat _ _ x xs nyx
      ... = occs a (filter (λ (a : ℕ), a ≤ y) xs ++ (x :: filter (λ (a : ℕ), y < a) xs)) : @filter_cons_of_pos nat _ _ x xs xy
      ... = occs a (filter (λ (a : ℕ), a ≤ y) xs) + occs a ([x] ++ filter (λ (a : ℕ), y < a) xs) : lem6_2_8
      ... = occs a (filter (λ (a : ℕ), a ≤ y) xs) + (occs a [x] + occs a (filter (λ (a : ℕ), y < a) xs)) : lem6_2_8
      ... = occs a [x] + (occs a (filter (λ (a : ℕ), a ≤ y) xs) + occs a (filter (λ (a : ℕ), y < a) xs)) : nat.add_left_comm _ _ _
      ... = occs a [x] + occs a (filter (λ (a : ℕ), a ≤ y) xs ++ filter (λ (a : ℕ), y < a) xs) : lem6_2_8
    end
  ... = occs a [x] + occs a xs : lem6_2_11 a
  ... = occs a (x :: xs) : lem6_2_8)

theorem thm6_4 : ∀ {m : nat} {xs : list nat} (p : length xs ≤ m), is_sorted (qsort' m xs p) ∧ is_perm xs (qsort' m xs p)
| 0 [] p := and.intro is_sorted.nil (λa, rfl)
| 0 (x::xs) p := absurd (eq_zero_of_le_zero p) (by simp)
| (m+1) [] p := and.intro is_sorted.nil (λa, rfl)
| (m+1) (x::xs) p := and.intro
  (proof
    let l₁ := qsort' m (filter (λt, t ≤ x) xs) (le.trans !filter_length_bound (!length_cons p)) in
    let l₂ := qsort' m (filter (λt, x < t) xs) (le.trans !filter_length_bound (!length_cons p)) in
    
    have isl₁ : (is_sorted l₁), from and.left (thm6_4 _),
    have isl₂ : (is_sorted l₂), from and.left (thm6_4 _),
    have ipl₁ : is_perm (filter (λt, t ≤ x) xs) l₁, from and.right (thm6_4 _),
    have ipl₂ : is_perm (filter (λt, x < t) xs) l₂, from and.right (thm6_4 _),
    have prl₁ : ∀(b : ℕ), b ∈ l₁ → b ≤ x, from (λb bin, of_mem_filter (iff.elim_right (!lem6_2_7 ipl₁ _) bin)),
    have prl₂ : ∀(b : ℕ), b ∈ l₂ → x < b, from (λb bin, of_mem_filter (iff.elim_right (!lem6_2_7 ipl₂ _) bin)),
    show (is_sorted (qsort' (m+1) (x::xs) p)),
      from lem6_3 (and.intro isl₁ (and.intro isl₂ (and.intro prl₁ (λb bin, le_of_lt_or_eq (or.inl (prl₂ b bin))))))
  qed)
  (proof
    let l₁ := qsort' m (filter (λt, t ≤ x) xs) (le.trans !filter_length_bound (!length_cons p)) in
    let l₂ := qsort' m (filter (λt, x < t) xs) (le.trans !filter_length_bound (!length_cons p)) in
    have ipl₁ : is_perm (filter (λt, t ≤ x) xs) l₁, from and.right (thm6_4 _),
    have ipl₂ : is_perm (filter (λt, x < t) xs) l₂, from and.right (thm6_4 _),

    show (is_perm (x::xs) (l₁ ++ [x] ++ l₂)), from λc, eq.symm (calc
      occs c (l₁ ++ [x] ++ l₂) = occs c l₁ + occs c [x] + occs c l₂ : lem6_2_8 ▸ rfl ⬝ lem6_2_8 ▸ rfl
      ... = occs c [x] + (occs c l₁ + occs c l₂) : by simp
      ... = occs c [x] + (occs c (filter (λt, t ≤ x) xs) + occs c (filter (λt, x < t) xs)) : ipl₁ c ▸ rfl ⬝ ipl₂ c ▸ rfl
      ... = occs c [x] + (occs c (filter (λt, t ≤ x) xs ++ filter (λt, x < t) xs)) : lem6_2_8
      ... = occs c [x] + occs c xs : lem6_2_11
      ... = occs c (x :: xs) : lem6_2_8)
  qed)

corollary cor6_5 : ∀ {xs : list nat}, is_sorted (qsort xs) ∧ is_perm xs (qsort xs) := λxs, thm6_4 _