15. Collatz & Sorting

28/11/22

set_option pp.structure_projections false
variables {A B C : Type}
open nat

def leb : ℕ → ℕ → bool
| 0 n := tt
| (succ n) 0 := ff
| (succ m) (succ n) := leb m n

theorem leb_ok : ∀ m n : ℕ, m ≤ n ↔ leb m n = tt :=
begin
  sorry,
end

def ins : ℕ → list ℕ → list ℕ 
| n [] := [n]
| n (m :: ms) :=
  if (leb n m) then n :: m :: ms
  else m :: (ins n ms)


def sort : list ℕ → list ℕ 
| [] := []
| (n :: ns) := ins n (sort ns)

#eval (sort [ 5,3,2,4,1])

-- sort sorts
-- Sorted : list ℕ → Prop


inductive Le_list : ℕ → list ℕ → Prop
| le_nil : ∀ n : ℕ, Le_list n []
| le_cons : ∀ m n : ℕ, ∀ ns : list ℕ , m ≤ n → Le_list m ns → Le_list m (n :: ns)

inductive Sorted : list ℕ → Prop
| sorted_nil : Sorted []
| sorted_cons : ∀ ms : list ℕ, ∀ n : ℕ, Le_list n ms → Sorted ms → Sorted (n :: ms)

open Sorted
open Le_list

example : Sorted [3,6,8] :=
begin
  apply sorted_cons,
  apply le_cons,
  sorry,
  apply le_cons,
  sorry,
  apply le_nil,
  apply sorted_cons,
  apply le_cons,
  sorry,
  apply le_nil,
  apply sorted_cons,
  apply le_nil,
  apply sorted_nil,
end

example : ¬Sorted [8,6,3] :=
begin
  assume h,
  cases h with _ _ h1 h2,
  cases h1 with _ _ _ _ h3,
  sorry,

end

open list

lemma sgl_sorted : ∀ n : ℕ, Sorted [n] :=
begin
  assume n,
  apply sorted_cons,
  apply le_nil,
  apply sorted_nil,
end

lemma ins_le_lem : ∀ m n : ℕ, ∀ ms : list ℕ, Le_list n ms → n ≤ m → Le_list n (ins m ms) :=
begin
  sorry,
end


lemma ins_lem : ∀ ns : list ℕ, ∀ n : ℕ, Sorted ns → Sorted (ins n ns) :=
begin
  assume ns n sns,
  induction ns with n' ns' ih,
  dsimp[ins],
  apply sgl_sorted,
  dsimp[ins],
  cases eq : (leb n n'),
  simp,
  cases sns with _ _ h2 h3,
  apply sorted_cons,
  apply ins_le_lem,
  exact h2,
  sorry,
  apply ih,
  exact h3,
  simp,
  apply sorted_cons,
  apply le_cons,
  sorry,
  cases sns with _ _ h2 h3,
  sorry,
  sorry,
end



theorem sort_sorts : ∀ ns : list ℕ , Sorted (sort ns) :=
begin
  assume ns,
  induction ns with n ns' ih,
  dsimp [sort],
  apply sorted_nil,
  dsimp [sort],
  apply ins_lem,
  exact ih,
end