14. Reverse, Definition of Sorted

21/11/22

set_option pp.structure_projections false


/- 
inductive list(A : Type)
| nil : list
-- | cons : A → list → list
| snoc : list → A → list




open list
local notation (name := cons) a :: b := cons a b

1 :: 2 :: 3 :: nil
[1,2,3]
-/

variables {A B C : Type}

/-
def append : list A → list A → list A
| [] bs := bs
| {a :: as} bs := a :: (append as bs)

[1,2] ++ [3,4] = [1,2,3,4]

local notation (name := append) as ++ bs := append as bs
-/


/-
proof is using induction over lists
(list A, ++, [])
commutative monoid?
[1,2]++[3] ≠ [3]++[1,2]
lists are the free monoid
what is the free commutative monoid

multisets, bags
{1,1} ≠ {1}
{1,2,3} = {3,2,1}

forget multisets, back to lists...#check
rev [1,2,3] = [3,2,1]

-/
--snoc [1,2] 3 = [1,2,3]

def snoc : list A → A → list A
| [] a := [a]
| (b :: bs) a := b :: (snoc bs a)

-- rev [1,2,3] = snoc(rev [2,3])
-- snoc [3,2] 1 = [3,2,1]
def rev : list A → list A
| [] := []
| (a :: as) := snoc (rev as) a

#eval (rev [1,2,3])
#eval rev (rev [1,2,3])

open list

lemma revsnoc : ∀ as : list A, ∀ a : A, rev (snoc as a) = a :: rev as :=
begin
  assume as a,
  induction as with b as' ih,
  dsimp[snoc,rev],
  refl,
  dsimp[snoc,rev],
  rw ih,
  dsimp[snoc],
  refl,
end

theorem revrev : ∀ as : list A, rev(rev as) = as :=
begin
  assume as,
  induction as with a as' ih,
  dsimp [rev],
  refl,
  dsimp[rev],
  rw revsnoc,
  rw ih,
end


---

-- sort : list ℕ → list ℕ 
-- sort [5,3,2,2,1] → [1,2,2,3,5]

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)

theorem sort_sorts : ∀ ns : list ℕ , Sorted (sort ns) :=
begin
  sorry,
end