Deriving insertion sort by proof

InsertionSort.lean

/-
 - Definition of insertion sort.
 - Copyright Siva Somayyajula, 2017
 -/

namespace list

universe u
variable {α : Type u}

-- Permutation equivalence of lists
protected def equiv (l₁ l₂ : list α) := l₁ ⊆ l₂ ∧ l₂ ⊆ l₁
infix ` ≃ `:50 := list.equiv

-- Permutation equivalence is an equivalence relation
@[refl, simp] lemma equiv.refl (l : list α) : l ≃ l :=
⟨by simp, by simp⟩

@[symm] lemma equiv.symm {l₁ l₂ : list α} : l₁ ≃ l₂ → l₂ ≃ l₁ :=
and.symm

@[trans] lemma equiv.trans {l₁ l₂ l₃ : list α} : l₁ ≃ l₂ → l₂ ≃ l₃ → l₁ ≃ l₃
| ⟨x, y⟩ ⟨z, w⟩ := ⟨subset.trans x z, subset.trans w y⟩

-- Permutation equivalence is invariant under cons
lemma cons_equiv_cons {l₁ l₂} (a : α) : l₁ ≃ l₂ → a :: l₁ ≃ a :: l₂
| ⟨x, y⟩ := ⟨cons_subset_cons a x, cons_subset_cons a y⟩

-- The subset relation is invariant under permutation
lemma cons_subset_comm {a b : α} {l₁ l₂} :
  l₁ ⊆ l₂ → a :: b :: l₁ ⊆ b :: a :: l₂ :=
λ h _ m, match m with
| or.inl is_a           := or.inr (or.inl is_a)
| or.inr (or.inl is_b)  := or.inl is_b
| or.inr (or.inr in_l₁) := or.inr (or.inr (h in_l₁))
end

-- Permutation equivalence is, naturally, invariant under permutation
lemma cons_equiv_comm {a b : α} {l₁ l₂} :
  l₁ ≃ l₂ → a :: b :: l₁ ≃ b :: a :: l₂
| ⟨x, y⟩ := ⟨cons_subset_comm x, cons_subset_comm y⟩

-- A list is sorted iff it is a chain under some ordering
def sorted [has_le α] : list α → Prop
| (a :: b :: t) := a ≤ b ∧ sorted (b :: t)
| _             := true

-- The tail of any sorted list is sorted
lemma sorted_tl [has_le α] {h : α} {t} : sorted (h :: t) → sorted t :=
λ s, by {cases t, trivial, exact s.right}

-- A list sorted by a weak order means its head is its least element
lemma sorted_least_elem [weak_order α] {h : α} {t} :
  sorted (h :: t) → ∀ {a}, a ∈ t → h ≤ a :=
begin
  -- By induction, we repeatedly apply transitivity
  intros s _ m,
  induction t with h' t' ih generalizing h,
    exact absurd m (not_mem_nil a),
    cases m with is_h' in_t',
      rw is_h', exact s.left,
      exact le_trans s.left (ih in_t' s.right)
end

-- Given a sorted list, consing an element preserves sorting if it is the least element
lemma sorted_cons [has_le α] {h : α} {t} :
  sorted t → (∀ {a}, a ∈ t → h ≤ a) → sorted (h :: t) :=
begin
  intros _ f,
  cases t,
    trivial,
    apply and.intro,
    exact f (or.inl (by refl)),
    assumption
end

-- One can insert an element into a list sorted by a linear weak order and keep it sorted
def insert_le [decidable_linear_order α] (a : α) (l₁) :
  sorted l₁ → {l₂ // a :: l₁ ≃ l₂ ∧ sorted l₂} :=
begin
  intro s₁,
  induction l₁ with h t₁ ih,
    existsi ([a]), simp,
    by_cases a ≤ h with hleq,
      -- If a ≤ h, then a :: h :: t₁ is the result
      existsi a :: h :: t₁, exact ⟨by refl, hleq, s₁⟩,
      -- Else, insert a by recursion
      cases ih (sorted_tl s₁) with t₂ p, cases p with e s₂,
      existsi h :: t₂, apply and.intro,
      calc
        a :: h :: t₁ ≃ h :: a :: t₁ : cons_equiv_comm (by refl)
                 ... ≃ h :: t₂      : cons_equiv_cons h e,
      -- Show that h :: t₂ is sorted by noting h is its least element
      exact sorted_cons s₂ (λ _ m,
      match e.right m with
      | or.inl is_a  := by {rw is_a, exact le_of_not_le hleq}
      | or.inr in_t₁ := sorted_least_elem s₁ in_t₁
      end)
end

-- For any list, there always exists an equivalent list sorted by a linear weak order
-- This is precisely insertion sort
def insertion_sort [decidable_linear_order α] (l₁ : list α) :
  {l₂ // l₁ ≃ l₂ ∧ sorted l₂} :=
begin
  induction l₁ with h t₁ ih,
    -- Nil is always sorted
    existsi nil, simp,
    -- If the tail is sorted, then insert the head while preserving order
    cases ih with t₂ ih, cases ih with e s,
    cases (insert_le h t₂ s) with l₂ pf, cases pf with _ _,
    existsi l₂, apply and.intro,
    calc
      h :: t₁ ≃ h :: t₂ : cons_equiv_cons h e
          ... ≃ l₂      : by assumption,
    assumption
end

end list