Theory "sorting"

Signature

Definitions

PERM_DEF

⊢ ∀L1 L2. PERM L1 L2 ⇔ ∀x. FILTER ($= x) L1 = FILTER ($= x) L2

SORTS_DEF

⊢ ∀f R. SORTS f R ⇔ ∀l. PERM l (f R l) ∧ SORTED R (f R l)

PART_DEF

⊢ (∀P l1 l2. PART P [] l1 l2 = (l1,l2)) ∧
  ∀P h rst l1 l2.
      PART P (h::rst) l1 l2 = if P h then PART P rst (h::l1) l2
      else PART P rst l1 (h::l2)

PARTITION_DEF

⊢ ∀P l. PARTITION P l = PART P l [] []

PERM_SINGLE_SWAP_DEF

⊢ ∀l1 l2.
      PERM_SINGLE_SWAP l1 l2 ⇔
      ∃x1 x2 x3. l1 = x1 ++ x2 ++ x3 ∧ l2 = x1 ++ x3 ++ x2

STABLE_DEF

⊢ ∀sort r.
      STABLE sort r ⇔
      SORTS sort r ∧
      ∀p. (∀x y. p x ∧ p y ⇒ r x y) ⇒ ∀l. FILTER p l = FILTER p (sort r l)

PART3_DEF

⊢ (∀R h. PART3 R h [] = ([],[],[])) ∧
  ∀R h hd tl.
      PART3 R h (hd::tl) =
      if R h hd ∧ R hd h then (I ## (CONS hd ## I)) (PART3 R h tl)
      else if R hd h then (CONS hd ## (I ## I)) (PART3 R h tl)
      else (I ## (I ## CONS hd)) (PART3 R h tl)

Theorems

PERM_REFL

⊢ ∀L. PERM L L

PERM_INTRO

⊢ ∀x y. x = y ⇒ PERM x y

PERM_transitive

⊢ transitive PERM

PERM_TRANS

⊢ ∀x y z. PERM x y ∧ PERM y z ⇒ PERM x z

PERM_SYM

⊢ ∀l1 l2. PERM l1 l2 ⇔ PERM l2 l1

PERM_CONG

⊢ ∀L1 L2 L3 L4. PERM L1 L3 ∧ PERM L2 L4 ⇒ PERM (L1 ++ L2) (L3 ++ L4)

PERM_MONO

⊢ ∀l1 l2 x. PERM l1 l2 ⇒ PERM (x::l1) (x::l2)

PERM_CONS_IFF

⊢ ∀x l2 l1. PERM (x::l1) (x::l2) ⇔ PERM l1 l2

PERM_NIL

⊢ ∀L. (PERM L [] ⇔ L = []) ∧ (PERM [] L ⇔ L = [])

PERM_SING

⊢ (PERM L [x] ⇔ L = [x]) ∧ (PERM [x] L ⇔ L = [x])

PERM_CONS_EQ_APPEND

⊢ ∀L h. PERM (h::t) L ⇔ ∃M N. L = M ++ h::N ∧ PERM t (M ++ N)

PERM_APPEND

⊢ ∀l1 l2. PERM (l1 ++ l2) (l2 ++ l1)

CONS_PERM

⊢ ∀x L M N. PERM L (M ++ N) ⇒ PERM (x::L) (M ++ x::N)

APPEND_PERM_SYM

⊢ ∀A B C. PERM (A ++ B) C ⇒ PERM (B ++ A) C

PERM_SPLIT_IF

⊢ ∀P Q l. EVERY (λx. P x ⇔ ¬Q x) l ⇒ PERM l (FILTER P l ++ FILTER Q l)

PERM_SPLIT

⊢ ∀P l. PERM l (FILTER P l ++ FILTER ($~ ∘ P) l)

FILTER_EQ_REP

⊢ FILTER ($= x) l = REPLICATE (LENGTH (FILTER ($= x) l)) x

FILTER_EQ_LENGTHS_EQ

⊢ LENGTH (FILTER ($= x) l1) = LENGTH (FILTER ($= x) l2) ⇒
  FILTER ($= x) l1 = FILTER ($= x) l2

PERM_alt

⊢ ∀L1 L2.
      PERM L1 L2 ⇔ ∀x. LENGTH (FILTER ($= x) L1) = LENGTH (FILTER ($= x) L2)

PERM_IND

⊢ ∀P.
      P [] [] ∧ (∀x l1 l2. P l1 l2 ⇒ P (x::l1) (x::l2)) ∧
      (∀x y l1 l2. P l1 l2 ⇒ P (x::y::l1) (y::x::l2)) ∧
      (∀l1 l2 l3. P l1 l2 ∧ P l2 l3 ⇒ P l1 l3) ⇒
      ∀l1 l2. PERM l1 l2 ⇒ P l1 l2

PERM_SWAP_AT_FRONT

⊢ PERM (x::y::l1) (y::x::l2) ⇔ PERM l1 l2

PERM_SWAP_L_AT_FRONT

⊢ ∀x y. PERM (x ++ y ++ l1) (y ++ x ++ l2) ⇔ PERM l1 l2

PERM_STRONG_IND

⊢ ∀P.
      P [] [] ∧ (∀x l1 l2. PERM l1 l2 ∧ P l1 l2 ⇒ P (x::l1) (x::l2)) ∧
      (∀x y l1 l2. PERM l1 l2 ∧ P l1 l2 ⇒ P (x::y::l1) (y::x::l2)) ∧
      (∀l1 l2 l3. PERM l1 l2 ∧ P l1 l2 ∧ PERM l2 l3 ∧ P l2 l3 ⇒ P l1 l3) ⇒
      ∀l1 l2. PERM l1 l2 ⇒ P l1 l2

PERM_LENGTH

⊢ ∀l1 l2. PERM l1 l2 ⇒ LENGTH l1 = LENGTH l2

PERM_MEM_EQ

⊢ ∀l1 l2. PERM l1 l2 ⇒ ∀x. MEM x l1 ⇔ MEM x l2

PERM_LIST_TO_SET

⊢ ∀l1 l2. PERM l1 l2 ⇒ LIST_TO_SET l1 = LIST_TO_SET l2

SORTED_IND

⊢ ∀P.
      (∀R. P R []) ∧ (∀R x. P R [x]) ∧
      (∀R x y rst. P R (y::rst) ⇒ P R (x::y::rst)) ⇒
      ∀v v1. P v v1

SORTED_DEF

⊢ (∀R. SORTED R [] ⇔ T) ∧ (∀x R. SORTED R [x] ⇔ T) ∧
  ∀y x rst R. SORTED R (x::y::rst) ⇔ R x y ∧ SORTED R (y::rst)

SORTED_EQ

⊢ ∀R L x. transitive R ⇒ (SORTED R (x::L) ⇔ SORTED R L ∧ ∀y. MEM y L ⇒ R x y)

SORTED_APPEND

⊢ ∀R L1 L2.
      transitive R ∧ SORTED R L1 ∧ SORTED R L2 ∧
      (∀x y. MEM x L1 ∧ MEM y L2 ⇒ R x y) ⇒
      SORTED R (L1 ++ L2)

PART_LENGTH

⊢ ∀P L l1 l2 p q.
      (p,q) = PART P L l1 l2 ⇒
      LENGTH L + LENGTH l1 + LENGTH l2 = LENGTH p + LENGTH q

PART_LENGTH_LEM

⊢ ∀P L l1 l2 p q.
      (p,q) = PART P L l1 l2 ⇒
      LENGTH p ≤ LENGTH L + LENGTH l1 + LENGTH l2 ∧
      LENGTH q ≤ LENGTH L + LENGTH l1 + LENGTH l2

PARTs_HAVE_PROP

⊢ ∀P L A B l1 l2.
      (A,B) = PART P L l1 l2 ∧ (∀x. MEM x l1 ⇒ P x) ∧ (∀x. MEM x l2 ⇒ ¬P x) ⇒
      (∀z. MEM z A ⇒ P z) ∧ ∀z. MEM z B ⇒ ¬P z

PART_MEM

⊢ ∀P L a1 a2 l1 l2.
      (a1,a2) = PART P L l1 l2 ⇒
      ∀x. MEM x (L ++ (l1 ++ l2)) ⇔ MEM x (a1 ++ a2)

QSORT_IND

⊢ ∀P.
      (∀ord. P ord []) ∧
      (∀ord h t.
           (∀l1 l2. (l1,l2) = PARTITION (λy. ord y h) t ⇒ P ord l2) ∧
           (∀l1 l2. (l1,l2) = PARTITION (λy. ord y h) t ⇒ P ord l1) ⇒
           P ord (h::t)) ⇒
      ∀v v1. P v v1

QSORT_DEF

⊢ (∀ord. QSORT ord [] = []) ∧
  ∀t ord h.
      QSORT ord (h::t) =
      (let
         (l1,l2) = PARTITION (λy. ord y h) t
       in
         QSORT ord l1 ++ [h] ++ QSORT ord l2)

QSORT_MEM

⊢ ∀R L x. MEM x (QSORT R L) ⇔ MEM x L

QSORT_PERM

⊢ ∀R L. PERM L (QSORT R L)

QSORT_SORTED

⊢ ∀R L. transitive R ∧ total R ⇒ SORTED R (QSORT R L)

QSORT_SORTS

⊢ ∀R. transitive R ∧ total R ⇒ SORTS QSORT R

PERM_APPEND_IFF

⊢ (∀l l1 l2. PERM (l ++ l1) (l ++ l2) ⇔ PERM l1 l2) ∧
  ∀l l1 l2. PERM (l1 ++ l) (l2 ++ l) ⇔ PERM l1 l2

PERM_SINGLE_SWAP_SYM

⊢ ∀l1 l2. PERM_SINGLE_SWAP l1 l2 ⇔ PERM_SINGLE_SWAP l2 l1

PERM_SINGLE_SWAP_I

⊢ PERM_SINGLE_SWAP (x1 ++ x2 ++ x3) (x1 ++ x3 ++ x2)

PERM_SINGLE_SWAP_APPEND

⊢ PERM_SINGLE_SWAP (x2 ++ x3) (x3 ++ x2)

PERM_SINGLE_SWAP_REFL

⊢ ∀l. PERM_SINGLE_SWAP l l

PERM_SINGLE_SWAP_CONS

⊢ PERM_SINGLE_SWAP M N ⇒ PERM_SINGLE_SWAP (x::M) (x::N)

PERM_SINGLE_SWAP_TC_CONS

⊢ ∀M N. PERM_SINGLE_SWAP⁺ M N ⇒ PERM_SINGLE_SWAP⁺ (x::M) (x::N)

PERM_TC

⊢ PERM = PERM_SINGLE_SWAP⁺

PERM_RTC

⊢ PERM = PERM_SINGLE_SWAP^*

PERM_EQC

⊢ PERM = PERM_SINGLE_SWAP^=

PERM_lifts_transitive_relations

⊢ ∀f Q.
      (∀x1 x2 x3. Q (f (x1 ++ x2 ++ x3)) (f (x1 ++ x3 ++ x2))) ∧ transitive Q ⇒
      ∀x y. PERM x y ⇒ Q (f x) (f y)

PERM_lifts_equalities

⊢ ∀f.
      (∀x1 x2 x3. f (x1 ++ x2 ++ x3) = f (x1 ++ x3 ++ x2)) ⇒
      ∀x y. PERM x y ⇒ f x = f y

PERM_lifts_invariants

⊢ ∀P.
      (∀x1 x2 x3. P (x1 ++ x2 ++ x3) ⇒ P (x1 ++ x3 ++ x2)) ⇒
      ∀x y. P x ∧ PERM x y ⇒ P y

PERM_lifts_monotonicities

⊢ ∀f.
      (∀x1 x2 x3.
           ∃x1' x2' x3'.
               f (x1 ++ x2 ++ x3) = x1' ++ x2' ++ x3' ∧
               f (x1 ++ x3 ++ x2) = x1' ++ x3' ++ x2') ⇒
      ∀x y. PERM x y ⇒ PERM (f x) (f y)

PERM_EQUIVALENCE

⊢ equivalence PERM

PERM_EQUIVALENCE_ALT_DEF

⊢ ∀x y. PERM x y ⇔ PERM x = PERM y

ALL_DISTINCT_PERM

⊢ ∀l1 l2. PERM l1 l2 ⇒ (ALL_DISTINCT l1 ⇔ ALL_DISTINCT l2)

PERM_ALL_DISTINCT

⊢ ∀l1 l2.
      ALL_DISTINCT l1 ∧ ALL_DISTINCT l2 ∧ (∀x. MEM x l1 ⇔ MEM x l2) ⇒
      PERM l1 l2

ALL_DISTINCT_PERM_LIST_TO_SET_TO_LIST

⊢ ∀ls. ALL_DISTINCT ls ⇔ PERM ls (SET_TO_LIST (LIST_TO_SET ls))

PERM_MAP

⊢ ∀f l1 l2. PERM l1 l2 ⇒ PERM (MAP f l1) (MAP f l2)

PERM_SUM

⊢ ∀l1 l2. PERM l1 l2 ⇒ SUM l1 = SUM l2

PERM_FILTER

⊢ ∀P l1 l2. PERM l1 l2 ⇒ PERM (FILTER P l1) (FILTER P l2)

PERM_REVERSE

⊢ PERM ls (REVERSE ls)

PERM_REVERSE_EQ

⊢ (PERM (REVERSE l1) l2 ⇔ PERM l1 l2) ∧ (PERM l1 (REVERSE l2) ⇔ PERM l1 l2)

FOLDR_PERM

⊢ ∀f l1 l2 e. ASSOC f ∧ COMM f ⇒ PERM l1 l2 ⇒ FOLDR f e l1 = FOLDR f e l2

PERM_SET_TO_LIST_count_COUNT_LIST

⊢ PERM (SET_TO_LIST (count n)) (COUNT_LIST n)

SUM_IMAGE_count_SUM_GENLIST

⊢ ∑ f (count n) = SUM (GENLIST f n)

SUM_IMAGE_count_MULT

⊢ (∀m. m < n ⇒ g m = ∑ (λx. f (x + k * m)) (count k)) ⇒
  ∑ f (count (k * n)) = ∑ g (count n)

sum_of_sums

⊢ ∑ (λm. ∑ (f m) (count a)) (count b) =
  ∑ (λm. f (m DIV a) (m MOD a)) (count (a * b))

SORTED_NIL

⊢ ∀R. SORTED R []

SORTED_SING

⊢ ∀R x. SORTED R [x]

SORTED_TL

⊢ SORTED R (x::xs) ⇒ SORTED R xs

SORTED_EL_SUC

⊢ ∀R ls. SORTED R ls ⇔ ∀n. SUC n < LENGTH ls ⇒ R (EL n ls) (EL (SUC n) ls)

SORTED_EL_LESS

⊢ ∀R.
      transitive R ⇒
      ∀ls. SORTED R ls ⇔ ∀m n. m < n ∧ n < LENGTH ls ⇒ R (EL m ls) (EL n ls)

SORTED_APPEND_IFF

⊢ ∀R L1 L2.
      SORTED R (L1 ++ L2) ⇔
      SORTED R L1 ∧ SORTED R L2 ∧ (L1 = [] ∨ L2 = [] ∨ R (LAST L1) (HD L2))

MEM_PERM

⊢ ∀l1 l2. PERM l1 l2 ⇒ ∀a. MEM a l1 ⇔ MEM a l2

SORTED_PERM_EQ

⊢ ∀R.
      transitive R ∧ antisymmetric R ⇒
      ∀l1 l2. SORTED R l1 ∧ SORTED R l2 ∧ PERM l1 l2 ⇒ l1 = l2

QSORT_eq_if_PERM

⊢ ∀R.
      total R ∧ transitive R ∧ antisymmetric R ⇒
      ∀l1 l2. QSORT R l1 = QSORT R l2 ⇔ PERM l1 l2

SORTED_FILTER

⊢ ∀R ls P. transitive R ∧ SORTED R ls ⇒ SORTED R (FILTER P ls)

ALL_DISTINCT_SORTED_WEAKEN

⊢ ∀R R' ls.
      (∀x y. MEM x ls ∧ MEM y ls ∧ x ≠ y ⇒ (R x y ⇔ R' x y)) ∧
      ALL_DISTINCT ls ∧ SORTED R ls ⇒
      SORTED R' ls

PERM_FUN_APPEND_C

⊢ ∀l1 l1' l2 l2'.
      PERM l1 = PERM l1' ⇒
      PERM l2 = PERM l2' ⇒
      PERM (l1 ++ l2) = PERM (l1' ++ l2')

PERM_FUN_CONS

⊢ ∀x l1 l1'. PERM l1 = PERM l1' ⇒ PERM (x::l1) = PERM (x::l1')

PERM_FUN_APPEND_CONS

⊢ ∀x l1 l2. PERM (l1 ++ x::l2) = PERM (x::l1 ++ l2)

PERM_FUN_SWAP_AT_FRONT

⊢ ∀x y l. PERM (x::y::l) = PERM (y::x::l)

PERM_FUN_CONS_11_SWAP_AT_FRONT

⊢ ∀y l1 x l2. PERM l1 = PERM (x::l2) ⇒ PERM (y::l1) = PERM (x::y::l2)

PERM_FUN_CONS_11_APPEND

⊢ ∀y l1 l2 l3. PERM l1 = PERM (l2 ++ l3) ⇒ PERM (y::l1) = PERM (l2 ++ y::l3)

PERM_FUN_CONS_APPEND_1

⊢ ∀l l1 x l2. PERM l1 = PERM (x::l2) ⇒ PERM (l1 ++ l) = PERM (x::(l2 ++ l))

PERM_FUN_CONS_APPEND_2

⊢ ∀l l1 x l2. PERM l1 = PERM (x::l2) ⇒ PERM (l ++ l1) = PERM (x::(l ++ l2))

PERM_FUN_APPEND_APPEND_1

⊢ ∀l1 l2 l3 l4.
      PERM l1 = PERM (l2 ++ l3) ⇒ PERM (l1 ++ l4) = PERM (l2 ++ (l3 ++ l4))

PERM_FUN_APPEND_APPEND_2

⊢ ∀l1 l2 l3 l4.
      PERM l1 = PERM (l2 ++ l3) ⇒ PERM (l4 ++ l1) = PERM (l2 ++ (l4 ++ l3))

PERM_FUN_APPEND

⊢ ∀l1 l2. PERM (l1 ++ l2) = PERM (l2 ++ l1)

PERM_FUN_CONS_IFF

⊢ ∀x l1 l2. PERM l1 = PERM l2 ⇒ PERM (x::l1) = PERM (x::l2)

PERM_FUN_APPEND_IFF

⊢ ∀l l1 l2. PERM l1 = PERM l2 ⇒ PERM (l ++ l1) = PERM (l ++ l2)

PERM_FUN_CONG

⊢ ∀l1 l1' l2 l2'.
      PERM l1 = PERM l1' ⇒ PERM l2 = PERM l2' ⇒ (PERM l1 l2 ⇔ PERM l1' l2')

PERM_CONG_2

⊢ ∀l1 l1' l2 l2'. PERM l1 l1' ⇒ PERM l2 l2' ⇒ (PERM l1 l2 ⇔ PERM l1' l2')

PERM_CONG_APPEND_IFF

⊢ ∀l l1 l1' l2 l2'.
      PERM l1 (l ++ l1') ⇒ PERM l2 (l ++ l2') ⇒ (PERM l1 l2 ⇔ PERM l1' l2')

PERM_FUN_SPLIT

⊢ ∀l l1 l1' l2. PERM l (l1 ++ l2) ⇒ PERM l1' l1 ⇒ PERM l (l1' ++ l2)

PERM_REWR

⊢ ∀l r l1 l2. PERM l r ⇒ (PERM (l ++ l1) l2 ⇔ PERM (r ++ l1) l2)

PART3_FILTER

⊢ ∀tl hd.
      PART3 R hd tl =
      (FILTER (λx. R x hd ∧ ¬R hd x) tl,FILTER (λx. R x hd ∧ R hd x) tl,
       FILTER (λx. ¬R x hd) tl)

QSORT3_IND

⊢ ∀P.
      (∀R. P R []) ∧
      (∀R hd tl.
           (∀lo eq hi. (lo,eq,hi) = PART3 R hd tl ⇒ P R hi) ∧
           (∀lo eq hi. (lo,eq,hi) = PART3 R hd tl ⇒ P R lo) ⇒
           P R (hd::tl)) ⇒
      ∀v v1. P v v1

QSORT3_DEF

⊢ (∀R. QSORT3 R [] = []) ∧
  ∀tl hd R.
      QSORT3 R (hd::tl) =
      (let (lo,eq,hi) = PART3 R hd tl in QSORT3 R lo ++ hd::eq ++ QSORT3 R hi)

PERM3

⊢ ∀x a a' b b' c c'.
      (PERM a a' ∧ PERM b b' ∧ PERM c c') ∧ PERM x (a ++ b ++ c) ⇒
      PERM x (a' ++ b' ++ c')

PERM3_FILTER

⊢ ∀l h.
      PERM l
        (FILTER (λx. R x h ∧ ¬R h x) l ++ FILTER (λx. R x h ∧ R h x) l ++
         FILTER (λx. ¬R x h) l)

PERM_QSORT3

⊢ ∀l R. PERM l (QSORT3 R l)

SORTED_EQ_PART

⊢ ∀l R. transitive R ⇒ SORTED R (FILTER (λx. R x hd ∧ R hd x) l)

QSORT3_SORTS

⊢ ∀R. transitive R ∧ total R ⇒ SORTS QSORT3 R

QSORT3_SPLIT

⊢ ∀R.
      transitive R ∧ total R ⇒
      ∀l e.
          QSORT3 R l =
          QSORT3 R (FILTER (λx. R x e ∧ ¬R e x) l) ++
          FILTER (λx. R x e ∧ R e x) l ++ QSORT3 R (FILTER (λx. ¬R x e) l)

QSORT3_STABLE

⊢ ∀R. transitive R ∧ total R ⇒ STABLE QSORT3 R

QSORT3_MEM

⊢ ∀R L x. MEM x (QSORT3 R L) ⇔ MEM x L

QSORT3_SORTED

⊢ ∀R L. transitive R ∧ total R ⇒ SORTED R (QSORT3 R L)

sorted_count_list

⊢ ∀n. SORTED $<= (COUNT_LIST n)

sorted_map

⊢ ∀R f l. transitive R ⇒ (SORTED R (MAP f l) ⇔ SORTED (inv_image R f) l)

sorted_perm_count_list

⊢ ∀y f l n.
      SORTED (inv_image $<= f) l ∧ PERM (MAP f l) (COUNT_LIST n) ⇒
      MAP f l = COUNT_LIST n

SORTED_weaken

⊢ ∀R R' ls.
      SORTED R ls ∧ (∀x y. MEM x ls ∧ MEM y ls ∧ R x y ⇒ R' x y) ⇒
      SORTED R' ls

less_sorted_eq

⊢ ∀L x. SORTED $< (x::L) ⇔ SORTED $< L ∧ ∀y. MEM y L ⇒ x < y

SORTED_GENLIST_PLUS

⊢ ∀n k. SORTED $< (GENLIST ($+ k) n)

SORTED_ALL_DISTINCT

⊢ irreflexive R ∧ transitive R ⇒ ∀ls. SORTED R ls ⇒ ALL_DISTINCT ls

sorted_filter

⊢ ∀R ls. transitive R ⇒ SORTED R ls ⇒ SORTED R (FILTER P ls)