Theory comparison

⊢ ∀cmp cmp2 f.
    equiv_inj cmp cmp2 f ⇔
    ∀k1 k2. cmp2 (f k1) (f k2) = Equal ⇒ cmp k1 k2 = Equal

⊢ ∀cmp.
    good_cmp cmp ⇔
    (∀x. cmp x x = Equal) ∧ (∀x y. cmp x y = Equal ⇒ cmp y x = Equal) ∧
    (∀x y. cmp x y = Greater ⇔ cmp y x = Less) ∧
    (∀x y z. cmp x y = Equal ∧ cmp y z = Less ⇒ cmp x z = Less) ∧
    (∀x y z. cmp x y = Less ∧ cmp y z = Equal ⇒ cmp x z = Less) ∧
    (∀x y z. cmp x y = Equal ∧ cmp y z = Equal ⇒ cmp x z = Equal) ∧
    ∀x y z. cmp x y = Less ∧ cmp y z = Less ⇒ cmp x z = Less

⊢ ∀cmp cmp2 f.
    resp_equiv2 cmp cmp2 f ⇔
    ∀k1 k2. cmp k1 k2 = Equal ⇒ cmp2 (f k1) (f k2) = Equal

⊢ ∀cmp f. resp_equiv cmp f ⇔ ∀k1 k2 v. cmp k1 k2 = Equal ⇒ f k1 v = f k2 v

⊢ ∀c. TotOrd c ⇒ TO_inv c = CURRY (invert ∘ UNCURRY c)

⊢ ∀R. irreflexive R ⇒
      TO_of_LinearOrder (LLEX R) = list_cmp (TO_of_LinearOrder R)

⊢ ∀c. TotOrd c ⇒ TotOrd (list_cmp c)

⊢ ∀cmp. TotOrd cmp ⇒ good_cmp cmp

⊢ ∀cmp f.
    (∀x y. cmp x y = Equal ⇒ x = y) ⇒
    resp_equiv cmp f ∧ ∀cmp2. good_cmp cmp2 ⇒ resp_equiv2 cmp cmp2 f

⊢ ∀x y. bool_cmp x y = Equal ⇔ (x ⇔ y)

⊢ bool_cmp T T = Equal ∧ bool_cmp F F = Equal ∧ bool_cmp T F = Greater ∧
  bool_cmp F T = Less

⊢ good_cmp bool_cmp

⊢ ∀x y. char_cmp x y = Equal ⇔ x = y

⊢ char_cmp = charOrd

⊢ ∀c1 c2. char_cmp c1 c2 = num_cmp (ORD c1) (ORD c2)

⊢ good_cmp char_cmp

⊢ (Less ≠ Equal ∧ Less ≠ Greater ∧ Equal ≠ Greater) ∧
  ((∀v0 v1 v2. (case Less of Less => v0 | Equal => v1 | Greater => v2) = v0) ∧
   (∀v0 v1 v2.
      (case Equal of Less => v0 | Equal => v1 | Greater => v2) = v1) ∧
   ∀v0 v1 v2.
     (case Greater of Less => v0 | Equal => v1 | Greater => v2) = v2) ∧
  (∀a. a = Less ∨ a = Equal ∨ a = Greater) ∧
  ∀cmp.
    good_cmp cmp ⇔
    (∀x. cmp x x = Equal) ∧ (∀x y. cmp x y = Equal ⇒ cmp y x = Equal) ∧
    (∀x y. cmp x y = Greater ⇔ cmp y x = Less) ∧
    (∀x y z. cmp x y = Equal ∧ cmp y z = Less ⇒ cmp x z = Less) ∧
    (∀x y z. cmp x y = Less ∧ cmp y z = Equal ⇒ cmp x z = Less) ∧
    (∀x y z. cmp x y = Equal ∧ cmp y z = Equal ⇒ cmp x z = Equal) ∧
    ∀x y z. cmp x y = Less ∧ cmp y z = Less ⇒ cmp x z = Less

⊢ ∀cmp.
    good_cmp cmp ⇒
    irreflexive (λk k'. cmp k k' = Less) ∧
    transitive (λk k'. cmp k k' = Less)

⊢ ∀cmp. good_cmp cmp ⇒ transitive (λk k'. cmp k k' = Less)

⊢ ∀cmp.
    good_cmp cmp ⇔
    (∀x. cmp x x = Equal) ∧
    ∀x y z.
      (cmp x y = Greater ⇔ cmp y x = Less) ∧
      (cmp x y = Less ∧ cmp y z = Equal ⇒ cmp x z = Less) ∧
      (cmp x y = Less ∧ cmp y z = Less ⇒ cmp x z = Less)

⊢ ∀cmp. good_cmp cmp ⇒ transitive (λ(k,v) (k',v'). cmp k k' = Less)

⊢ ∀c. TotOrd c ⇒ list_cmp c = ListOrd (TO c)

⊢ ∀cmp x y.
    (∀x y. cmp x y = Equal ⇔ x = y) ⇒ (list_cmp cmp x y = Equal ⇔ x = y)

⊢ ∀cmp l1 l2 cmp' l1' l2'.
    l1 = l1' ∧ l2 = l2' ∧
    (∀x x'. MEM x l1' ∧ MEM x' l2' ⇒ cmp x x' = cmp' x x') ⇒
    list_cmp cmp l1 l2 = list_cmp cmp' l1' l2'

⊢ ∀cmp l1 l2.
    list_cmp cmp l1 l2 = Equal ⇔ LIST_REL (λx y. cmp x y = Equal) l1 l2

⊢ ∀cmp. good_cmp cmp ⇒ good_cmp (list_cmp cmp)

⊢ ∀x y. num_cmp x y = Equal ⇔ x = y

⊢ ∀n1 n2.
    num_cmp n1 n2 =
    if n1 = n2 then Equal else if n1 < n2 then Less else Greater

⊢ good_cmp num_cmp

⊢ num_cmp = numOrd

⊢ ∀c. option_cmp2 c = TO_inv (option_cmp (TO_inv c))

⊢ ∀cmp x y.
    (∀x y. cmp x y = Equal ⇔ x = y) ⇒ (option_cmp2 cmp x y = Equal ⇔ x = y)

⊢ ∀cmp v1 v2 cmp' v1' v2'.
    v1 = v1' ∧ v2 = v2' ∧
    (∀x x'. v1' = SOME x ∧ v2' = SOME x' ⇒ cmp x x' = cmp' x x') ⇒
    option_cmp2 cmp v1 v2 = option_cmp2 cmp' v1' v2'

⊢ option_cmp2 cmp NONE NONE = Equal ∧
  option_cmp2 cmp NONE (SOME x') = Greater ∧
  option_cmp2 cmp (SOME x) NONE = Less ∧
  option_cmp2 cmp (SOME x) (SOME y) = cmp x y

⊢ ∀cmp. good_cmp cmp ⇒ good_cmp (option_cmp2 cmp)

⊢ ∀P. (∀cmp. P cmp NONE NONE) ∧ (∀cmp x. P cmp NONE (SOME x)) ∧
      (∀cmp x. P cmp (SOME x) NONE) ∧ (∀cmp x y. P cmp (SOME x) (SOME y)) ⇒
      ∀v v1 v2. P v v1 v2

⊢ ∀cmp x y.
    (∀x y. cmp x y = Equal ⇔ x = y) ⇒ (option_cmp cmp x y = Equal ⇔ x = y)

⊢ ∀cmp v1 v2 cmp' v1' v2'.
    v1 = v1' ∧ v2 = v2' ∧
    (∀x x'. v1' = SOME x ∧ v2' = SOME x' ⇒ cmp x x' = cmp' x x') ⇒
    option_cmp cmp v1 v2 = option_cmp cmp' v1' v2'

⊢ option_cmp c NONE NONE = Equal ∧ option_cmp c NONE (SOME v0) = Less ∧
  option_cmp c (SOME v3) NONE = Greater ∧
  option_cmp c (SOME v1) (SOME v2) = c v1 v2

⊢ ∀cmp. good_cmp cmp ⇒ good_cmp (option_cmp cmp)

⊢ ∀cmp1 cmp2 x y.
    (∀x y. cmp1 x y = Equal ⇔ x = y) ∧ (∀x y. cmp2 x y = Equal ⇔ x = y) ⇒
    (pair_cmp cmp1 cmp2 x y = Equal ⇔ x = y)

⊢ ∀cmp1 cmp2 v1 v2 cmp1' cmp2' v1' v2'.
    v1 = v1' ∧ v2 = v2' ∧
    (∀a b c d. v1' = (a,b) ∧ v2' = (c,d) ⇒ cmp1 a c = cmp1' a c) ∧
    (∀a b c d. v1' = (a,b) ∧ v2' = (c,d) ⇒ cmp2 b d = cmp2' b d) ⇒
    pair_cmp cmp1 cmp2 v1 v2 = pair_cmp cmp1' cmp2' v1' v2'

⊢ pair_cmp c1 c2 x y =
  case c1 (FST x) (FST y) of
    Less => Less
  | Equal => c2 (SND x) (SND y)
  | Greater => Greater

⊢ ∀cmp1 cmp2. good_cmp cmp1 ∧ good_cmp cmp2 ⇒ good_cmp (pair_cmp cmp1 cmp2)

⊢ ∀R V. TotOrd R ∧ TotOrd V ⇒ pair_cmp R V = R lexTO V

⊢ ∀x y. string_cmp x y = Equal ⇔ x = y

⊢ string_cmp = list_cmp char_cmp

⊢ good_cmp string_cmp

⊢ string_cmp = apto stringto