16. Permutation

02/12/22

Permutation - If the output contains the same element in a different order Perm [1,2,3] [1,3,2] is true Perm [1,2] [1] is false Perm [1,1] [1] is false

/- Lecture 17, IFR (COMP2009,2022-23) -/
set_option pp.structure_projections false

open nat
open list

-- ble and ≤

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

#reduce (ble 4 7)

-- ins-sort

def ins : ℕ → list ℕ → list ℕ 
| a [] := [a]
| a (b :: bs) := if ble a b then a :: b :: bs else b::(ins a bs)

#reduce ins 6 [2, 3, 3, 8]

def sort : list ℕ → list ℕ  
| [] := []
| (a :: as) := ins a (sort as)

#reduce (sort [6,3,8,2,3])

/-
theorem sort_sorts : ∀ ns : list ℕ,
  Sorted (sort ns) 
-/

variable {A : Type}

inductive Insert : A → list A → list A → Prop
| ins_hd : ∀ m : A, ∀ ms : list A, 
      Insert m ms (m :: ms)
| ins_tl :  ∀ m n : A, ∀ ms ns : list A,
      Insert n ms ns 
      → Insert n (m :: ms) (m :: ns)

open Insert

inductive Perm : list A → list A → Prop
| perm_nil : Perm [] []
| perm_cons : ∀ ms ns ns' : list A, ∀ m : A,
            Perm ms ns 
            → Insert m ns ns' 
            → Perm (m :: ms) ns' 

open Perm

example : Perm [1,2,3] [3,2,1] :=
begin
  apply perm_cons,
  apply perm_cons,
  apply perm_cons,
  apply perm_nil,
  apply ins_hd,
  apply ins_tl,
  apply ins_hd,
  apply ins_tl,
  apply ins_tl,
  apply ins_hd,
end

theorem refl_perm : ∀ as : list A,
  Perm as as :=
begin
  assume as,
  induction as with a as' ih,
  apply perm_nil,
  apply perm_cons,
  apply ih,
  apply ins_hd,
end

example : ∀ as bs : list A,
  Perm as bs → Perm bs as :=
sorry

example : ∀ as bs cs : list A,
  Perm as bs → Perm bs cs → Perm as cs :=
sorry

-- Perm is an equivalence relation
-- if equality of A is decidable
-- then Perm {A} is decidable.

def is_perm : list ℕ → list ℕ → bool
:= sorry

theorem is_perm_ok : ∀ ms ns : list ℕ,
  Perm ms ns ↔ is_perm ms ns = tt :=
sorry

lemma ins_perm : ∀ n :ℕ, ∀ ns : list ℕ,
  Insert n ns (ins n ns) :=
begin
  assume n ns,
  induction ns with n' ns' ih,
  dsimp [ins],
  apply ins_hd,
  dsimp [ins],
  cases (ble n n'),
  simp,
  apply ins_tl,
  apply ih,
  simp,
  apply ins_hd,
end

theorem perm_sort : ∀ ns : list ℕ,
  Perm ns (sort ns) :=
begin
  assume ns,
  induction ns with n ns' ih,
  apply perm_nil,
  dsimp [sort],
  apply perm_cons,
  apply ih,
  apply ins_perm,
end