Theorem List
Mathematics for Computing, CS/SE 2DM3, Fall 2020

Table of Contents

1 Inequality

Inequality is defined as negation of equality. 

Declaration: _≠_ : t → t → 𝔹

Axiom “Definition of ≠”: x ≠ y  ≡  ¬ (x = y)

It is convenient to have irreflexivity of inequality available in two (equivalent) shapes: 

Theorem “Irreflexivity of ≠”: ¬ (x ≠ x)

Theorem “Irreflexivity of ≠”: x ≠ x  ≡  false

Inequality is symmetric (but, unlike equality, not transitive): 

Theorem “Symmetry of ≠”:  x ≠ y  ≡  y ≠ x

2 Equational Theory of Integers   Exercise_2

Here we develop that part of LADM's “Theory of Integers” that only requires equational reasoning on the integers only, with no other logical symbols besides =, not even ≡. 

Declaration: _+_ : ℤ → ℤ → ℤ
Declaration: _·_ : ℤ → ℤ → ℤ

Axiom (15.1) (15.1a) “Associativity of +”: (a + b) + c = a + (b + c)
Axiom (15.1) (15.1b) “Associativity of ·”: (a · b) · c = a · (b · c)
Axiom (15.2) (15.2a) “Symmetry of +”: a + b = b + a
Axiom (15.2) (15.2b) “Symmetry of ·”: a · b = b · a

Axiom (15.3) “Additive identity” “Identity of +”: 0 + a = a
Axiom (15.4) “Multiplicative identity” “Identity of ·”: 1 · a = a
Axiom (15.5) “Distributivity” “Distributivity of · over +”: a · (b + c) = a · b + a · c
Axiom (15.9) “Zero of ·”: a · 0 = 0

Declaration: -_ : ℤ → ℤ
Declaration: _-_ : ℤ → ℤ → ℤ

Axiom (15.13) “Unary minus”: a + (- a) = 0
Axiom (15.14) “Subtraction”: a - b = a + (- b)


Theorem (15.17) “Self-inverse of unary minus”:
   - (- a) = a

Theorem (15.18) “Fixpoint of unary minus”: - 0 = 0

Theorem (15.20): - a = (- 1) · a

Theorem (15.19) “Distributivity of unary minus over +”:
    - (a + b) = (- a) + (- b)

Theorem (15.21): (- a) · b = a · (- b)

Theorem (15.22): a · (- b) = - (a · b)

Theorem (15.23): (- a) · (- b) = a · b

Theorem (15.24) “Right-identity of -”: a - 0 = a

Theorem (15.25): (a - b) + (c - d) = (a + c) - (b + d)

Theorem (15.26): (a - b) - (c - d) = (a + d) - (b + c)

Theorem (15.27): (a - b) · (c - d) = (a · c + b · d) - (a · d + b · c)

Theorem (15.29) “Distributivity of · over -”:
    (a - b) · c = a · c - b · c

3 Propositional Calculus

3.1 Conjunction   Exercise 3_3

Declaration: _∧_ : 𝔹 → 𝔹 → 𝔹

Axiom (3.35) “Golden rule”: p ∧ q ≡ p ≡ q ≡ p ∨ q

Theorem (3.36) “Symmetry of ∧”: p ∧ q ≡ q ∧ p

Theorem (3.37) “Associativity of ∧”: (p ∧ q) ∧ r ≡ p ∧ (q ∧ r)

Theorem (3.38) “Idempotency of ∧”: p ∧ p ≡ p

Theorem (3.39) “Identity of ∧”: p ∧ true ≡ p

Theorem (3.40) “Zero of ∧”: p ∧ false ≡ false

Theorem (3.41) “Distributivity of ∧ over ∧”: p ∧ (q ∧ r) ≡ (p ∧ q) ∧ (p ∧ r)

Theorem (3.42) “Contradiction”: p ∧ ¬ p ≡ false

Theorem (3.43) (3.43a) “Absorption”: p ∧ (p ∨ q) ≡ p

Theorem (3.43) (3.43b) “Absorption”: p ∨ (p ∧ q) ≡ p

Theorem (3.44) (3.44a) “Absorption”: p ∧ (¬ p ∨ q) ≡ p ∧ q

Theorem (3.44) (3.44b) “Absorption”: p ∨ (¬ p ∧ q) ≡ p ∨ q

Theorem (3.44) (3.44c) “Absorption”: ¬ p ∧ (p ∨ q) ≡ ¬ p ∧ q

Theorem (3.44) (3.44d) “Absorption”: ¬ p ∨ (p ∧ q) ≡ ¬ p ∨ q

Theorem (3.45) “Distributivity of ∨ over ∧”: p ∨ (q ∧ r) ≡ (p ∨ q) ∧ (p ∨ r)

Theorem (3.46) “Distributivity of ∧ over ∨”: p ∧ (q ∨ r) ≡ (p ∧ q) ∨ (p ∧ r)

Theorem (3.47) (3.47a) “De Morgan”: ¬(p ∧ q) ≡ ¬ p ∨ ¬ q

Theorem (3.47) (3.47b) “De Morgan”: ¬(p ∨ q) ≡ ¬ p ∧ ¬ q

Theorem (3.48): p ∧ q ≡ p ∧ ¬ q ≡ ¬ p

Theorem (3.49) “Semi-distributivity of ∧ over ≡”: p ∧ (q ≡ r) ≡ p ∧ q ≡ p ∧ r ≡ p

Theorem (3.50) “Strong Modus Ponens”: p ∧ (q ≡ p) ≡ p ∧ q

Theorem (3.51) “Replacement”: (p ≡ q) ∧ (r ≡ p) ≡ (p ≡ q) ∧ (r ≡ q)

Theorem (3.52) “Alternative definition of ≡”: p ≡ q ≡ (p ∧ q) ∨ (¬ p ∧ ¬ q)

Theorem (3.53) “Exclusive or” “Alternative definition of ≢”:
  (p ≢ q) ≡ (¬ p ∧ q) ∨ (p ∧ ¬ q)

Theorem (3.55): (p ∧ q) ∧ r ≡ p ≡ q ≡ r ≡ p ∨ q ≡ q ∨ r ≡ r ∨ p ≡ p ∨ q ∨ r

3.2 Disjunction   Exercise_3_2 Homework_5_2

Declaration: _∨_ : 𝔹 → 𝔹 → 𝔹

Axiom (3.24) “Symmetry of ∨”: p ∨ q ≡ q ∨ p

Axiom (3.25) “Associativity of ∨”: (p ∨ q) ∨ r ≡ p ∨ (q ∨ r)

Axiom (3.26) “Idempotency of ∨”: p ∨ p ≡ p

Axiom (3.27) “Distributivity of ∨ over ≡”: p ∨ (q ≡ r) ≡ p ∨ q ≡ p ∨ r

Axiom (3.28) “Excluded Middle” “LEM”: p ∨ ¬ p

Theorem (3.29) “Zero of ∨”: p ∨ true ≡ true

Theorem (3.30) “Identity of ∨”: p ∨ false ≡ p

Theorem (3.31) “Distributivity of ∨ over ∨”: p ∨ (q ∨ r) ≡ (p ∨ q) ∨ (p ∨ r)

Theorem (3.32): p ∨ q ≡ p ∨ ¬ q ≡ p

3.3 Formalising “Knights and Knaves” Puzzles   Exercise_3_1

Raymond Smullyan posed many puzzles about an island that has two kinds of inhabitants:

  • knights, who always tell the truth, and
  • knaves, who always lie.

You encounter two people A and B.

The above paragraph contains information that is common to all scenarios below.

We are careful to postulate as axioms only statements that apply in all scenarios.

We declare a special type for the inhabitants of that island: 

Declaration: Inhabitant : Type
Declaration: _is-knight, _is-knave : Inhabitant → 𝔹

We then encode the two kinds of inhabitants as two unary Boolean-valued predicate operators, written in postfix syntax, and given higher precedence than logical negation, so we can write ¬ X is-knight with the same meaning as ¬ (X is-knight):

Obviously the “two kinds of inhabitants” are intended to be exhaustive; we formalise that as an inequivalence, and derive alternative formualations that well be useful for reasoning below: 

Axiom “Knights and knaves”: X is-knight ≢ X is-knave

Lemma “Knights and knaves”: X is-knight ≡ ¬ X is-knave

Lemma “Knights and knaves”: X is-knave ≡ ¬ X is-knight

The puzzles are all presented as stories contining as key ingredients that some inhabitant X makes some statement s; if we formalise that statement s into proposition p, then we formalist that whole ingredient as: 

    X says-🙶 p 🙷

The extra-fat quotation marks in _says-🙶_🙷 are obtained by typing \``` respectively \'''. 

Precedence 140 for:  _says-🙶_🙷
Declaration: _says-🙶_🙷 : Inhabitant → 𝔹 → 𝔹

The definitions of knights and knaves are the easily formalised: 

Axiom “Knighthood”: X says-🙶 p 🙷 ≡ X is-knight ≡ p
Axiom “Knavehood”:  X says-🙶 p 🙷 ≡ X is-knave  ≡ ¬ p

Finally, we formalise the statement “You encounter two people A and B”, making explicit the assumptions that these “people” are inhabitants of this island. 

Declaration: A, B : Inhabitant

3.4 Leibniz's Rule as an Axiom, Replacement Theorems   Exercise 5_1 Homework 7_2

Theorem “Definition of ≡”:  (p ≡ q) = (p = q)

Axiom (3.83) “Leibniz”: e = f ⇒ E[z ≔ e] = E[z ≔ f]

Theorem (3.84) (3.84a) “Replacement”:
    (e = f) ∧ E[z ≔ e] ≡ (e = f) ∧ E[z ≔ f]

Theorem (3.84) (3.84b) “Replacement”:
    (e = f) ⇒ E[z ≔ e] ≡ (e = f) ⇒ E[z ≔ f]

Theorem (3.84) (3.84c) “Replacement”:
    q ∧ (e = f) ⇒ E[z ≔ e] ≡ q ∧ (e = f) ⇒ E[z ≔ f]

Theorem (3.85) (3.85a) “Replace by `true`”: p ⇒ E[z ≔ p] ≡ p ⇒ E[z ≔ true]

Theorem (3.85) (3.85b) “Replace by `true`”: q ∧ p ⇒ E[z ≔ p] ≡ q ∧ p ⇒ E[z ≔ true]

Theorem (3.85c) “Replace by `false`”: ¬ p ⇒ E[z ≔ p] ≡ ¬ p ⇒ E[z ≔ false]

Theorem (3.86) (3.86a) “Replace by `false`”: E[z ≔ p] ⇒ p ≡ E[z ≔ false] ⇒ p

Theorem (3.86) (3.86b) “Replace by `false`”: E[z ≔ p] ⇒ p ∨ q ≡ E[z ≔ false] ⇒ p ∨ q

Theorem (3.87) “Replace by `true`”: p ∧ E[z ≔ p] ≡ p ∧ E[z ≔ true]

Theorem (3.88) “Replace by `false`”: p ∨ E[z ≔ p] ≡ p ∨ E[z ≔ false]

Theorem (3.89) “Shannon”: E[z ≔ p] ≡ (p ∧ E[z ≔ true]) ∨ (¬ p ∧ E[z ≔ false])


Axiom (3.83) “Leibniz”: e = f  ⇒  E[z ≔ e] = E[z ≔ f]

Theorem (3.84) (3.84a) “Replacement”:
    (e = f) ∧ E[z ≔ e]  ≡  (e = f) ∧ E[z ≔ f]

Lemma “Replacement in equality with addition”:
    a = b + c ∧ c = d  ≡  a = b + d ∧ c = d

3.5 Implication   Exercise 4_1  Homework 7_1

Declaration: _⇒_ : 𝔹 → 𝔹 → 𝔹

Declaration: _⇐_ : 𝔹 → 𝔹 → 𝔹

Axiom (3.57) “Definition of ⇒”: p ⇒ q ≡ p ∨ q ≡ q

Axiom (3.58) “Consequence” “Definition of ⇐”: p ⇐ q ≡ q ⇒ p

Theorem (3.59) “Definition of ⇒”: p ⇒ q ≡ ¬ p ∨ q

Theorem (3.60) “Definition of ⇒”: p ⇒ q ≡ p ∧ q ≡ p

Theorem (3.61) “Contrapositive”: p ⇒ q ≡ ¬ q ⇒ ¬ p

Theorem (3.62): p ⇒ (q ≡ r) ≡ p ∧ q ≡ p ∧ r

Theorem (3.63) “Distributivity of ⇒ over ≡”: p ⇒ (q ≡ r) ≡ p ⇒ q ≡ p ⇒ r

Theorem (3.64): p ⇒ (q ⇒ r) ≡ (p ⇒ q) ⇒ (p ⇒ r)

Theorem (3.65) “Shunting”: p ∧ q ⇒ r ≡ p ⇒ (q ⇒ r)

Theorem (3.66): p ∧ (p ⇒ q) ≡ p ∧ q

Theorem (3.67): p ∧ (q ⇒ p) ≡ p

Theorem (3.68): p ∨ (p ⇒ q) ≡ true

Theorem (3.69): p ∨ (q ⇒ p) ≡ q ⇒ p

Theorem (3.70): p ∨ q ⇒ p ∧ q ≡ p ≡ q

Theorem (3.71) “Reflexivity of ⇒”: (p ⇒ p) ≡ true

Theorem (3.72) “Right zero of ⇒”: (p ⇒ true) ≡ true

Theorem (3.73) “Left identity of ⇒”: (true ⇒ p) ≡ p

Theorem (3.74) “Definition of ¬ from ⇒”: (p ⇒ false) ≡ ¬ p

Theorem (3.75) “ex falso quodlibet”: (false ⇒ p) ≡ true

Theorem (3.76) (3.76a) “Weakening” “Strengthening”: p ⇒ p ∨ q

Theorem (3.76) (3.76a) “Weakening” “Strengthening”: p ⇒ p ∨ q

Theorem (3.76) (3.76b) “Weakening” “Strengthening”: p ∧ q ⇒ p

Theorem (3.76) (3.76c) “Weakening” “Strengthening”: p ∧ q ⇒ p ∨ q

Theorem (3.76) (3.76d) “Weakening” “Strengthening”: p ∨ (q ∧ r) ⇒ p ∨ q

Theorem (3.76) (3.76e) “Weakening” “Strengthening”: p ∧ q ⇒ p ∧ (q ∨ r)

Theorem (3.77) “Modus ponens”: p ∧ (p ⇒ q) ⇒ q

Theorem (3.78): (p ⇒ r) ∧ (q ⇒ r) ≡ (p ∨ q ⇒ r)

Theorem (3.79): (p ⇒ r) ∧ (¬ p ⇒ r) ≡ r

Theorem (3.80) “Mutual implication”: (p ⇒ q) ∧ (q ⇒ p) ≡ p ≡ q

Theorem (3.81) “Antisymmetry of ⇒”: (p ⇒ q) ∧ (q ⇒ p) ≡ (p ≡ q)

Theorem (3.82) (3.82a) “Transitivity of ⇒”: (p ⇒ q) ∧ (q ⇒ r) ⇒ (p ⇒ r)

Theorem (3.82) (3.82b) “Transitivity of ⇒”: (p ≡ q) ∧ (q ⇒ r) ⇒ (p ⇒ r)

Theorem (3.82) (3.82c) “Transitivity of ⇒”: (p ⇒ q) ∧ (q ≡ r) ⇒ (p ⇒ r)

Theorem (3.59) “Material implication”: p ⇒ q ≡ ¬ p ∨ q

Theorem (3.65) “Shunting”: p ∧ q ⇒ r ≡ p ⇒ (q ⇒ r)

Theorem (3.66) “Strong modus ponens”: p ∧ (p ⇒ q) ≡ p ∧ q

Theorem (3.67) “Even if”: p ∧ (q ⇒ p) ≡ p

Theorem (3.71) “Reflexivity of ⇒”: p ⇒ p

Theorem “Indirect reflexivity of ⇒”: (p ≡ q) ⇒ (p ⇒ q)

Theorem (3.80) “Mutual implication”: (p ⇒ q) ∧ (q ⇒ p) ≡ p ≡ q

Theorem (3.81) “Antisymmetry of ⇒”: (p ⇒ q) ∧ (q ⇒ p) ⇒ (p ≡ q)

Theorem (3.82) (3.82a) “Transitivity of ⇒”: (p ⇒ q) ∧ (q ⇒ r) ⇒ (p ⇒ r)

Theorem (3.82) (3.82b) “Transitivity of ⇒”: (p ≡ q) ∧ (q ⇒ r) ⇒ (p ⇒ r)

Theorem “Antitonicity of ¬”:  (p ⇒ q) ⇒ (¬ q ⇒ ¬ p)

Theorem “Left-monotonicity of ∨”: (p ⇒ q) ⇒ ((p ∨ r) ⇒ (q ∨ r))

Theorem “Left-monotonicity of ∧”: (p ⇒ q) ⇒ ((p ∧ r) ⇒ (q ∧ r))

Theorem “Left-antitonicity of ⇒”: (p ⇒ q) ⇒ ((q ⇒ r) ⇒ (p ⇒ r))

Theorem “Right-monotonicity of ⇒”: (p ⇒ q) ⇒ ((r ⇒ p) ⇒ (r ⇒ q))

3.6 Conditionals   Homework 9_2

Declaration: if_then_else_fi : 𝔹 → t → t → t

Axiom “if true”:   if true  then x else y fi  =  x
Axiom “if false”:  if false then x else y fi  =  y

Theorem “`if` to ∨”:
    P[z ≔ if b then x else y fi]
  ≡ (b ∧ P[z ≔ x]) ∨ (¬ b ∧ P[z ≔ y])

Theorem “if swap”:
      if   b then x else y fi
   =  if ¬ b then y else x fi

Theorem “if then=true”: if R then true else P fi   ≡  R ∨ P

Theorem “if else=false”: if R then P else false fi   ≡  R ∧ P

4 Abstract Algebra: Magmas, Monoids, and Groups   Assignment 1

4.1 Basics

Theorem “A Boolean expression not equal to true is equal to false”:
   (p ≢ true) ≡ (p ≡ false)

Declaration: even : ℤ → 𝔹

Axiom “Even distributes over +”: even (x + y) ≡ even x ≡ even y
Axiom “Even of 2”: even 2
Axiom “Even of 1 ---not!”: ¬ even 1

Declaration: black : ℤ → ℤ → 𝔹

Axiom “Definition of black”:  black i j ≡ even i ≡ even j

Theorem “Bishops stay on the same colour”:
    black (i + k) (j + k) ≡ black i j

Theorem “Knights always change colours”: black (i + 2) (j + 1) ≢ black i j

4.2 Recalling Magmas

Declaration: τ : Type
Declaration: _⊕_ : τ → τ → τ

Axiom “Associativity of ⊕”: (x ⊕ y) ⊕ z = x ⊕ (y ⊕ z)

Theorem “Associativity of ≢”:
     ((p ≢ q) ≢ r) = (p ≢ (q ≢ r))

4.3 Monoid Madness

Declaration: Id : τ
Axiom “Left-identity of ⊕”: x = Id ⊕ x

Theorem “Left-identity of ≢”: (false ≢ p) ≡ p

Axiom “Symmetry of ⊕”:  x ⊕ y = y ⊕ x

Theorem “Symmetry of ≢”:  (p ≢ q) ≡ (q ≢ p)

Theorem “Right-identity of ⊕”:  x = x ⊕ Id

4.4 “Everyone break into Groups!”

Precedence 210 for: inv_
Declaration: inv_ : τ → τ
Axiom “Left-inverses”: inv x ⊕ x = Id

Theorem “Right-inverses”: x ⊕ inv x = Id

Theorem “Left-inverses for ≢”: (p ≢ p) = false

Precedence 190 for: _⊝_   -- entered with `\o-` and `\ominus`.
Declaration: _⊝_ : τ → τ → τ

Axiom “Definition of ⊝”: x ⊝ y = x ⊕ inv y

Theorem “Mutual associativity of ⊕ and ⊝”:
    x ⊕ (y ⊝ z) = (x ⊕ y) ⊝ z

Theorem “Right-identity of inverse”: x ⊝ Id = x

Theorem “Self-cancellation of inverse”: x ⊝ x = Id

Theorem “Inverse of composition” “Subtraction of sum”:
    x ⊝ (y ⊕ z) = (x ⊝ z) ⊝ y

4.5 Relative Undoability: Uniqueness of ／Binary Inverses＼

Declaration: _／_ : τ → τ → τ
Declaration: _＼_ : τ → τ → τ

Axiom “Under”: x ⊕ y = z  ≡  y = x ＼ z
Axiom “Over”:  x ⊕ y = z  ≡  x = z ／ y

Theorem “Under with ⊕ in the numerator”:    y = x ＼ (x ⊕ y)

Theorem “⊕ then Under”:                     x ⊕ (x ＼ z) = z

Theorem “Over with ⊕ in the numerator”:     x = (x ⊕ y) ／ y

Theorem “Over then ⊕”:                      (z ／ y) ⊕ y = z

Theorem “Fractions”: a ＼ b  =  b ／ a

Declaration: _%-of_ : ℤ → ℤ → ℤ
Declaration: _div_ : ℤ → ℤ → ℤ

Axiom “Definition of percentage”: x %-of y  =  (x div 100) · y
Axiom “Into the numerator”: (x div z) · y = (x · y) div z

Theorem “Percentages commute”: a %-of b  =  b %-of a

4.6 “Swap or Paws” —Take II

Lemma “Irreflexivity of ≢”: (p ≢ p) = false

Lemma “xor swap”:
     x = X ∧ y = Y
     ⇒⁅  x := x ≢ y  ⍮
         y := x ≢ y  ⍮
         x := x ≢ y
     ⁆
     x = Y ∧ y = X

Wap: Xor Swap without the xor!! 

Lemma “wap”:
     x = X ∧ y = Y
     ⇒⁅  x := x ≡ y  ⍮
         y := x ≡ y  ⍮
         x := x ≡ y
     ⁆
     x = Y ∧ y = X

5 Inductively Defined Types

5.1 Inductive Theory of the Natural Numbers   Exercise 4_2

Here we develop an theory of the natural numbers based on induction over 0 and the successor operator suc_. 

Theorem “Successor”: suc n = n + 1

Theorem “Associativity of +”: (a + b) + c = a + (b + c)

Declaration: _·_ : ℕ → ℕ → ℕ

Axiom “Definition of · for 0”: 0 · n = 0
Axiom “Definition of · for `suc`”: (suc m) · n = n + m · n

Theorem “Left-identity of ·”: 1 · n = n

Theorem “Right-zero of ·”: m · 0 = 0

Theorem “Multiplying the successor”: m · (suc n) = m + m · n

Theorem “Symmetry of ·”: m · n = n · m

Theorem “Distributivity of · over +”: (k + m) · n = k · n + m · n

Theorem “Associativity of ·”: (k · m) · n = k · (m · n)

5.2 Predecessors in the Inductive Theory of the Natural Numbers   Homework 8_5

Corollary “Identity of +”: 0 + a = a

Corollary “Identity of ·”: 1 · a = a

Corollary “Zero of ·”: 0 · a = 0

Theorem “Successor is non-decreasing”: a ≤ suc a

Theorem “Successor is increasing”: a < suc a

We define the predecessor function pred on natural numbers, and since it has to be defined for all natural numbers, we let it map 0 to 0: 

Declaration: pred : ℕ → ℕ
Axiom “Predecessor of zero”:       pred 0       = 0
Axiom “Predecessor of successor”:  pred (suc n) = n

Corresponding to the “Successor” theorem suc n = n + 1, we also have a “Predecessor” theorem: 

Theorem “Predecessor”:  pred n = n - 1

Theorem “Predecessor is non-increasing”: pred a ≤ a

Theorem “Predecessor of non-zero”:
    n ≠ 0  ≡  suc (pred n) = n

Theorem “Monotonicity of predecessor”: a ≤ b ⇒ pred a ≤ pred b

Theorem “Non-<-monotonicity of predecessor”:
    ¬ (a < b ⇒ pred a < pred b)[a, b ≔ ? , ? ]

Theorem “<-Monotonicity of predecessor”:
    suc a < b ⇒ pred (suc a) < pred b

5.3 Inductive Theory of Sequences   Exercise_9_1 Homework_14

Here we develop a theory of sequences following LADM chapter 13. 

Sequences formalised via the new type constructor `Seq`

      Declaration: Seq : Type → Type

Producing types Seq A of finite sequences with elements of type A, and Seq A is introduced as an inductive type with the following constructors: 

      Declaration: 𝜖  : Seq A
      Declaration: _◃_ : A → Seq A → Seq A

𝜖 (type \emptySeq or \eps) stands for the empty sequence.

For an element x : A and a sequence xs : Seq a, the sequence x ◃ xs has x as its first element, also called head, and xs as its tail. For the symbol ◃, type \cons.

The binary operator ◃ associates to the right.

Corresponding to “Zero is not successor” on the natural numbers, here we have: 

Axiom (13.3) “Cons is not empty”: x ◃ xs ≠ 𝜖

The axiom corresponding to “Cancellation of successor” on the natural number then rounds off the characterisation of sequence equality as being equality of construction from `𝜖` and `◃`: 

Axiom (13.4) “Cancellation of ◃”:
   x ◃ xs = y ◃ ys  ≡  x = y ∧ xs = ys

The induction principle for sequences implemented in By induction proofs is the following: 

       P[xs ≔ 𝜖]
    ⇒  (∀ xs : Seq A ❙ P • (∀ x : A • P[xs ≔ x ◃ xs]))
    ⇒  (∀ xs : Seq A • P)

An induction proof for either just `P`, or for `∀ xs : Seq A • P` (it works the same for both goal statements), therefore takes the following shape: 

    By induction on `xs : Seq A`:
      Base case:

         ⟪ Proof for `P[xs ≔ 𝜖]` ⟫

      Induction step:

         ⟪ Proof for `∀ x : A • P[xs ≔ x ◃ xs]` ⟫

           ⟪ using: Induction hypothesis `P` ⟫

Be careful to introduce a fresh variable instead of x for proving theorems that mention x! 

Theorem (13.6) “Cons decomposition”:
   ∀ xs : Seq A • xs = 𝜖  ∨  (∃ y • ∃ ys • xs = y ◃ ys)

Theorem (13.7) “Tail is different”:
    ∀ xs : Seq A • ∀ x : A • x ◃ xs ≠ xs

Theorem (13.7) “Tail is different”:
    x ◃ xs ≠ xs

5.3.1 Membership

Declaration: _∈_ : A → Seq A → 𝔹

Axiom (13.10) “Membership in 𝜖”:     x ∈ 𝜖         ≡  false
Axiom (13.11) “Membership in ◃”:    x ∈ (y ◃ ys)  ≡  x = y   ∨  x ∈ ys

Theorem (13.16) “Membership in ▹”:
    x ∈ (ys ▹ z)  ≡  x ∈ ys ∨ x = z

Theorem (13.21) “Membership in ⌢”:
    x ∈ ys ⌢ zs  ≡  x ∈ ys ∨ x ∈ zs

5.3.2 Mapping a Function over a Sequence

Declaration: map : (A → B) → Seq A → Seq B

For example: map factorial [3, 0, 5] = [6, 1, 120]. 

Axiom “Definition of `map` for 𝜖”:   map f 𝜖 = 𝜖
Axiom “Definition of `map` for ◃”:   map f (x ◃ xs) = f x ◃ map f xs

Theorem “Definition of `map` for ▹”:
    map f (xs ▹ x) = map f xs ▹ f x

Theorem “Distributivity of `map` over ⌢”:
    map f (xs ⌢ ys) = map f xs ⌢ map f ys

5.3.3 Theorems to those of ℕ

Axiom (13.3) “Cons is not empty”: x ◃ xs ≠ 𝜖

Theorem “Cons is not empty”: x ◃ xs = 𝜖  ≡  false

Axiom (13.4) “Cancellation of ◃”:
   x ◃ xs = y ◃ ys  ≡  x = y ∧ xs = ys

5.3.4 Snoc

Declaration: _▹_ : Seq A → A → Seq A

Axiom (13.12) “Definition of ▹ for 𝜖”:         𝜖 ▹ a = a ◃ 𝜖
Axiom (13.13) “Definition of ▹ for ◃”:   (a ◃ s) ▹ b = a ◃ (s ▹ b)

Fact (H12.1): (2 ◃ 5 ◃ 3 ◃ 𝜖) ▹ 7  = 2 ◃ 5 ◃ 3 ◃ 7 ◃ 𝜖

Theorem (13.14) “Snoc is not empty”:  xs ▹ x ≠ 𝜖

Corollary “Snoc is not empty”:  xs ▹ x = 𝜖  ≡  false

5.3.5 Catenation

Declaration: _⌢_ : Seq A → Seq A → Seq A

Axiom (13.17)
      “Left-identity of ⌢”
      “Definition of ⌢ for 𝜖”:             𝜖 ⌢ ys = ys
Axiom (13.18)
      “Mutual associativity of ◃ with ⌢”
      “Definition of ⌢ for ◃”:      (x ◃ xs) ⌢ ys = x ◃ (xs ⌢ ys)

Fact (H12.2):  (2 ◃ 7 ◃ 5 ◃ 𝜖) ⌢ (1 ◃ 9 ◃ 𝜖) = 2 ◃ 7 ◃ 5 ◃ 1 ◃ 9 ◃ 𝜖

Theorem (13.19) “Right-identity of ⌢”:
    xs ⌢ 𝜖 = xs

Theorem (13.20) “Associativity of ⌢”:
    (xs ⌢ ys) ⌢ zs = xs ⌢ (ys ⌢ zs)

Theorem (13.23) “Empty concatenation”:
    xs ⌢ ys = 𝜖  ≡  xs = 𝜖 ∧ ys = 𝜖

5.3.6 Reverse

Declaration: reverse : Seq A → Seq A
Axiom “Definition of `reverse` for 𝜖”:  reverse 𝜖 = 𝜖
Axiom “Definition of `reverse` for ◃”:  reverse (x ◃ xs) = reverse xs ▹ x

Theorem “cat-snoc”:
    (us ⌢ vs) ▹ w = us ⌢ (vs ▹ w)

Theorem “Reverse of ⌢”:
   reverse (xs ⌢ ys) = reverse ys ⌢ reverse xs

We introduce the `head` and `tail` functions that extract the constituents of non-empty sequences: 

Declaration: head : Seq A → A
Declaration: tail : Seq A → Seq A

Note that the following axioms leave head 𝜖 and tail 𝜖 undefined — nothing interesting can be proven about these expressions. (Only boring things like head 𝜖 = head 𝜖…) 

Axiom “Definition of `head`”: head (x ◃ xs) = x
Axiom “Definition of `tail`”: tail (x ◃ xs) = xs

Theorem “Non-empty-sequence extensionality”:
    xs ≠ 𝜖 ⇒ xs = head xs ◃ tail xs

Theorem “snoc-cat”:
    (us ▹ v) ⌢ vs = us ⌢ (v ◃ vs)

5.4 Binary Trees   Exercise 12

As a simple graph, a relation may have the peculiar property of each node having at most two outgoing edges and no node is isolated (“forever alone”); such graphs are known as binary trees.

Since every node points to at most two other nodes, we can represent such relations inductively —as we did with ℕatural numbers, sequences, and paths.

We use symbols for the tree constructors that are intended to somewhat reflect the kind of downwards-growing tree drawing you see below:

  • ◬ — type: \emptytree or \t0
  • ◿ — type: \lbranch
  • ◺ — type: \rbranch

A nonempty tree (l ◿ x ◺ r) consists of a node carrying value x and branching to the left subtree l and the right subtree r: 

Declaration: Tree : Type → Type
Declaration:          ◬   : Tree A
Declaration:        _◿_◺_ : Tree A → A → Tree A → Tree A

Declaration: example : Tree ℕ
Axiom “Definition of `example`”:
  t1 = ((◬ ◿ 2 ◺ ◬) ◿ 3 ◺ (◬ ◿ 5 ◺ ◬))
       ◿ 7 ◺
       (◬ ◿ 10 ◺ (◬ ◿ 11 ◺ ◬))

Declaration: ｢_｣ : A → Tree A  --- \lsingleton and \rsingleton
Axiom “Singleton tree”: ｢ x ｣ = ◬ ◿ x ◺ ◬

Fact “Alternative definition of `example`”:
  t1 = (｢ 2 ｣ ◿ 3 ◺ ｢ 5 ｣)
       ◿ 7 ◺
       (◬ ◿ 10 ◺ ｢ 11 ｣)

Read l ◿ x ◺ r as “ node x has two child trees, the left l and the right r ”.

(The notation is also suggestive of how such trees are actually implemented: A non-empty tree is a value x and a pointer to the right child and a pointer to the left child!)

As with sequences, and other inductive data types, we can define operations on an inductive data type by considering the possible ways to form elements of this type.

E.g., We define the operator `_˘` to stand for the mirroring function on trees — via an inductive definition that covers all possible shapes of the argument tree: 

Declaration: _˘ : Tree A → Tree A
Axiom “Mirror”: ◬ ˘  = ◬
Axiom “Mirror”: (l ◿ x ◺ r) ˘  =  (r ˘) ◿ x ◺ (l ˘)

Theorem “Mirroring singleton trees”: ｢ x ｣ ˘ = ｢ x ｣  -- Singleton trees are fixpoints of mirroring:

To show a property P is true for all trees one needs to check that it is true for the simplest tree ◬ and that if it is true for existing trees, then the way to make new trees preserves the truth of P; i.e., if P holds for l and r hold, then it needs to hold also for (l ◿ x ◺ r) should also be true: 

Axiom “Tree induction”:
     P[t ≔ ◬]
  ∧  ( ∀ l, r : Tree A; x : A
       • P[t ≔ l] ∧ P[t ≔ r]  ⇒  P[t ≔ l ◿ x ◺ r]
     )
  ⇒  (∀ t : Tree A • P)

Using this induction principle for our trees, we can prove that the above mirroring operation is an involution, just like reverse for sequences and converse for relations: 

Theorem “Self-inverse of tree mirror”: ∀ t : Tree A • (t ˘) ˘ = t
Proof:
  Using “Tree induction”:
    Subproof for `◬ ˘ ˘ = ◬`: By “Mirror”
    Subproof for `∀ l, r : Tree A; x : A
         • (l ˘) ˘ = l ∧ (r ˘) ˘ = r
         ⇒ (l ◿ x ◺ r)˘ ˘ = (l ◿ x ◺ r)`:
       For any `l, r, x`:
         Assuming “IHL” `(l ˘) ˘ = l`,
                  “IHR” `(r ˘) ˘ = r`:
             (l ◿ x ◺ r) ˘ ˘
           =⟨ “Mirror” ⟩
             (l ˘ ˘) ◿ x ◺ (r ˘ ˘)
           =⟨ Assumptions “IHL” and “IHR” ⟩
             l ◿ x ◺ r

Declaration: size : Tree A → ℕ
Axiom “Tree size”: size ◬  = 0
Axiom “Tree size”: size (l ◿ x ◺ r)  =  size l + 1 + size r

Lemma “Singleton tree size”: size ｢ x ｣ = 1
Theorem “Size of mirrored tree”:
    ∀ t : Tree A • size (t ˘) = size t  --   Mirroring preserves size:

Similar to the map function you have seen on sequences, we also define a map function on tree, which creates a copy with “updated” elements: 

Declaration: map : (A → B) → Tree A → Tree B
Axiom “Tree map”: map f ◬ = ◬
Axiom “Tree map”: map f (l ◿ x ◺ r) = (map f l) ◿ (f x) ◺ (map f r)
Theorem “Size of mapped tree”:
    ∀ t •  size (map f t) = size t -- map preserver tree size:

5.4.1 Tree Traversals — Seqentialising the Nodes

We define the three standard ways to sequentialise the tree elements while for each node keeping all elements of the left subtree before the elements of the right subtree (remember the names!): 

Declaration: preOrder, inOrder, postOrder : Tree A → Seq A

Axiom “Definition of `preOrder`”:
     preOrder ◬ = 𝜖
  ∧  preOrder (l ◿ x ◺ r) = x ◃ preOrder l ⌢ preOrder r

Lemma “Singleton `preOrder`”: preOrder ｢ x ｣ = x ◃ 𝜖

Fact: preOrder example = 7 ◃ 3 ◃ 2 ◃ 5 ◃ 10 ◃ 11 ◃ 𝜖

Axiom “Definition of `inOrder`”:
     inOrder ◬ = 𝜖
  ∧  inOrder (l ◿ x ◺ r) = inOrder l ⌢ x ◃ inOrder r

Lemma “Singleton `inOrder`”: inOrder ｢ x ｣ = x ◃ 𝜖

Fact: inOrder example = 2 ◃ 3 ◃ 5 ◃ 7 ◃ 10 ◃ 11 ◃ 𝜖

Axiom “Definition of `postOrder`”:
     postOrder ◬ = 𝜖
  ∧  postOrder (l ◿ x ◺ r) = postOrder l ⌢ postOrder r ▹ x

Lemma “Singleton `postOrder`”: postOrder ｢ x ｣ = x ◃ 𝜖

Fact: postOrder example = 2 ◃ 5 ◃ 3 ◃ 11 ◃ 10 ◃ 7 ◃ 𝜖

Theorem “map commutes with inOrder”:
   ∀ f : A → B • ∀ t : Tree a
   • map f (inOrder t) = inOrder (map f t)

Note that in the theorem statement of “map commutes with inOrder”, the first map is the one from the theory of sequences, while the second map is the one from the current notebook.

6 Order Theory   Assignment_2

6.1 Introduction and Uniqueness of Bottoms

Usually we have a collection τ of things that we are working with and are they ordered by relationship _⊑_.

For example:

  1. People standing in a line are ordered by their position in the line.
    • For any two people, one will always be in-front of the other.
    • Such orders are called ‘linear’ — since they are like a line.
    • For instance, the natural numbers order by size, ≤, are linearly ordered.
  2. People in a city may be ordered by the floor level they live on.
    • People in different buildings, homes, are ‘incomparable’: Neither is ‘above’ the other.
    • Such orders are not linear.
    • For instance, members of a (business) hierarchy are only above their juniors and are not above their colleagues, and so are not linearly ordered. Likewise for ‘trees’ and ‘graphs’.

  3. The Booleans are ordered by implication, ⇒.

    This relationship is completely determined by the requirement that “ false ⇒ true ”; i.e., false is smaller-than true.

    Indeed, the collection of things that satisfy false is smaller than the collection of things that satisfy true, since the empty collection is smaller than the collection comprising everything.

Relationship:

Order Tree (hierarchy)
Linear order List (flattened tree)

We can formalise this situation as follows. (Where ⊑ is entered with \sqleq or \[=.) 

Conjunctional: _⊑_

Declaration: τ : Type
Declaration: _⊑_ : τ → τ → 𝔹

Axiom “Reflexivity of ⊑”: a ⊑ a
Axiom “Transitivity of ⊑”: a ⊑ b  ∧  b ⊑ c  ⇒  a ⊑ c
Axiom “Antisymmetry of ⊑”: a ⊑ b  ∧  b ⊑ a  ⇒  a = b

Theorem “Indirect reflexivity of ⊑”:  a = b  ⇒  a ⊑ b

Theorem “Mutual ⊑”: a ⊑ b  ∧  b ⊑ a  ≡  a = b

Theorem “Conjunctional Practice α”: a ⊑ a ⊑ b  ≡  a ⊑ b

Theorem “Conjunctional Practice β”
   “Sandwhich theorem”:
   a ⊑ b ⊑ a  ≡  a = b

Theorem “Conjunctional Practice γ”
        “Chaining”:
   a ⊑ b ⊑ c  ⇒  a ⊑ c

Declaration: ⊥₁, ⊥₂ : τ

Axiom “First bottom”:  ⊥₁ ⊑ a
Axiom “Second bottom”: ⊥₂ ⊑ a

Theorem “Bottoms are unique”: ⊥₁ = ⊥₂

Declaration: ⊥ : τ
Axiom “Bottom of ⊑”: ⊥ ⊑ a

6.2 Uniqueness of Tops

Declaration: ⊤₁, ⊤₂ : τ
Axiom “First top”: a ⊑ ⊤₁
Axiom “Second top”: b ⊑ ⊤₂

Theorem “Tops are unique”: ⊤₁ = ⊤₂

Declaration: ⊤ : τ
Axiom “Top is greatest element”: a ⊑ ⊤

Theorem “Top is maximal”: ⊤ ⊑ a ≡ a = ⊤

6.3 Divisibility

We can order the naturals by their size, as is usual, but we can also order them by how they factor into each other.

Say a | b precisely when b is a multiple of a; i.e., b = q · a for some integer q.

Be careful:

\(\frac{n}{m}\), n / m real division a number
n ÷ m integer division a number
m ∣ n divisibility relation a proposition 
Declaration: _|_ : ℕ → ℕ → 𝔹
Explanation: d | m ≔ “`d` divides `m`”
Explanation: d | m ≔ “`d` is a divisor of `m`”
Explanation: d | m ≔ “`m` is a multiple of `d`”

Axiom “Reflexitivity of |”: m | m
Axiom “Antisymmetry of |”: m | n  ∧  n | m  ⇒  n = m
Axiom “Transitivity of |”: m | n  ∧  n | k  ⇒  m | k

Theorem “Mutual divisibility” “Mutual |”:  m | n  ∧  n | m  ≡  n = m

Axiom “Divisibility of multiples”: m | (q · m)

Theorem “Top of |” “Greatest value of |”: m | 0

Theorem “Bottom of |” “Least element of |”: 1 | m

Theorem “Top of |” “Greatest value of |” “Top is maximal”:
   0 | n  ≡  n = 0

Theorem “Bottom of |” “Least element of |” “Bottom is minimal”:
  m | 1  ≡  m = 1

Axiom “Invariance of Divisibility under semi-linear combinations”:
   k | x  ∧  k | y  ≡  k | (x + a · y) ∧ k | y

Theorem “Invariance of Divisibility under semi-linear combinations”:
  k | y ⇒ (k | (x + a · y) ≡ k | x)

Theorem “|-Weakening” “|-Strengthening”:
  m | n  ⇒  m | (q · n)

Theorem “Divisibility of sums”: a | b  ∧  a | c  ⇒  a | (b + c)

Theorem “Divisiblity of linear combinations”:
  a | b  ∧  a | c  ⇒  a | (b · x + c · y)

Theorem “Sufficient Case Analysis for |”: a | b  ∨  a | c  ⇒  a | (b · c)

6.4 Meets and joins: Generalising Minima and Maxima

We have seen that _⊑_ : τ → τ → 𝔹 generalises all of

  • _≤_ : ℕ → ℕ → 𝔹
  • _∣_ : ℕ → ℕ → 𝔹
  • _⇒_ : 𝔹 → 𝔹 → 𝔹.

Let us turn to seeing what generalises

  • _↓_ : ℕ → ℕ → ℕ
  • _∧_ : 𝔹 → 𝔹 → 𝔹
  • gcd (greatest common divisor) operation

The generalision will be an operation _⊓_ : τ → τ → τ that will be the greatest lower bound of its arguments —it is where two elements “meet”.

Enter ⊓ using \meet. 

Precedence 100 for: _⊓_
Declaration: _⊓_ : τ → τ → τ

Axiom “Characterisation of ⊓”:
   c ⊑ a  ∧  c ⊑ b  ≡  c  ⊑  a ⊓ b

Theorem “Weakening for ⊓”: a ⊓ b  ⊑  a

Theorem “Weakening for ⊓”: a ⊓ b  ⊑  b

Theorem “Left-Monotonicity of ⊓”: a ⊑ b  ⇒  a ⊓ c ⊑ b ⊓ c

Theorem “Idempotency of ⊓”: a ⊓ a  =  a

Theorem “Induced definition of inclusion”: a ⊑ b  ≡  a ⊓ b = a

Precedence 100 for: _⊔_
Declaration: _⊔_ : τ → τ → τ

Axiom “Characterisation of ⊔”:
  a ⊑ c  ∧  b ⊑ c  ≡  a ⊔ b  ⊑  c

Theorem “Weakening for ⊔”: a  ⊑  a ⊔ b

Theorem (3.76l) “Weakening for ⊔”: b  ⊑  a ⊔ b

Theorem “Idempotency of ⊔”:  a ⊔ a = a

Theorem “Induced definition of inclusion”: a ⊑ b  ≡ a ⊔ b = b

Theorem “Absorption” “Squeeze Law” “Sandwich Theorem”: a ⊓ (b ⊔ a) = a

Theorem “Absorption” “Squeeze Law” “Sandwich Theorem”: a ⊔ (b ⊓ a) = a

Theorem “Weakening from ⊓ to ⊔” “Strengthening from ⊔ to ⊓”:
    a ⊓ b  ⊑  a ⊔ b

Theorem “Symmetry of ⊓”: a ⊓ b = b ⊓ a

Theorem “Symmetry of ⊔”: a ⊔ b = b ⊔ a

Theorem “Golden rule for ⊓ and ⊔”: b ⊓ a = a  ≡   b = a ⊔ b

Theorem “Golden rule for ⊓ and ⊔”: b ⊓ a = a ⊔ b  ≡   a = b

Theorem “Indirect zero of ⊔”:
  a ⊔ ⊤ ⊑ c  ≡  ⊤ ⊑ c

6.5 Order on Integers   Exercise 7_3

Theorem “Cancellation of unary minus”: - a = - b  ≡  a = b

Declaration: _<_ , _≤_ , _>_ , _≥_ : ℤ → ℤ → 𝔹

Axiom (15.36) “Less”, “Definition of <”: a < b ≡ pos (b - a)
Axiom (15.37) “Greater”, “Definition of >”: a > b ≡ pos (a - b)
Axiom (15.38) “At most” “Definition of ≤”: a ≤ b ≡ a < b ∨ a = b
Axiom (15.39) “At least” “Definition of ≥”: a ≥ b ≡ a > b ∨ a = b

Theorem “Irreflexivity of <”: ¬ (a < a)

Theorem “Irreflexivity of <”: a = b ⇒ ¬ (a < b)

Theorem “Irreflexivity of <”: a < b ⇒ ¬ (a = b)

Theorem “Irreflexivity of <”: ¬ (a < b ∧ a = b)

Theorem “Converse of <”: a > b ≡ b < a

Theorem “Converse of ≤”: a ≥ b ≡ b ≤ a

Theorem “Irreflexivity of >”: ¬ (a > a)

Theorem (15.40) “Positive elements”: pos b ≡ 0 < b

Theorem (15.41) (15.41a) “Transitivity” “Transitivity of <”:
   a < b  ∧  b < c  ⇒  a < c

Theorem (15.41) (15.41b) “Transitivity” “Transitivity of ≤ with <”:
   a ≤ b  ∧  b < c  ⇒  a < c

Theorem (15.41) (15.41c) “Transitivity” “Transitivity of < with ≤”:
   a < b  ∧  b ≤ c  ⇒  a < c

Theorem (15.41) (15.41d) “Transitivity” “Transitivity of ≤”:
   a ≤ b  ∧  b ≤ c  ⇒  a ≤ c

Theorem “Transitivity of ≤”:
   a ≤ b  ⇒  b ≤ c  ⇒  a ≤ c

Theorem “Transitivity of >”:
   a > b  ∧  b > c  ⇒  a > c

Theorem (15.42) “<-Isotonicity of +”:
   a < b  ≡  a + d < b + d

Theorem “<-Monotonicity of +”:
   a < b  ⇒  a + d < b + d

Theorem “<-Monotonicity of +”:
   a < b ⇒ c < d ⇒ a + c < b + d

Theorem “≤-Isotonicity of +”:
   a ≤ b  ≡  a + d ≤ b + d

Theorem “≤-Monotonicity of +”:
   a ≤ b  ⇒  a + d ≤ b + d

Theorem “Asymmetry of <”: ¬ (a < b  ∧  b < a)

Theorem (15.44A) “Trichotomy — A”:
    a < b  ≡  a = b  ≡  a > b

Theorem (15.44B) “Trichotomy — B”:
    ¬ (a < b  ∧  a = b  ∧  a > b)

Theorem (15.44) “Trichotomy”:
    (a < b  ≡  a = b  ≡  a > b) ∧
    ¬ (a < b  ∧  a = b  ∧  a > b)

6.6 Positivity of Integers   Exercise 7_1 7_2

Following the “Ordered Domains” section of LADM Chapter 15 “A Theory of Integers”, we introduce the positivity predicate pos axiomatically. 

Theorem (15.7) “Cancellation of ·”: c ≠ 0 ⇒ (c · a = c · b  ≡  a = b)
Theorem (15.8) “Cancellation of +”:          a + b = a + c  ≡  b = c
Theorem “Non-zero multiplication”: a ≠ 0 ⇒ b ≠ 0 ⇒ a · b ≠ 0

Declaration: pos : ℤ → 𝔹

Axiom (15.30) “Positivity under +”: pos a ∧ pos b ⇒ pos (a + b)
Axiom (15.31) “Positivity under ·”: pos a ∧ pos b ⇒ pos (a · b)
Axiom (15.32) “Non-positivity of 0”: ¬ pos 0
Axiom (15.33) “Positivity under unary minus”: b ≠ 0 ⇒ (pos b ≡ ¬ pos (- b))

Theorem (15.33b) “Positivity under unary minus”: b ≠ 0 ⇒ (pos (- b) ≡ ¬ pos b)

Theorem (15.33c) “Positivity under unary minus”: (pos (- b) ≡ pos b) ⇒ b = 0

Theorem “Positive implies non-zero”: pos a ⇒ a ≠ 0

Theorem (15.34) “Positivity of squares”: b ≠ 0 ⇒ pos (b · b)

Corollary “Positivity of 1”: pos 1

Theorem “Positivity”: pos a ≡ a ≠ 0 ∧ ¬ pos (- a)

Theorem (15.35) “Positivity under positive ·”: pos a ⇒ (pos b ≡ pos (a · b))

6.7 Mixed Monotonicity   Exercise 8_2 8_3

Theorem “Multiplying by 2”: 2 · x = x + x

Theorem “Multiplying by 3”: 3 · x = x + x + x

Theorem “Left-antitonicity of ⇒”: (p ⇒ q) ⇒ ((q ⇒ r) ⇒ (p ⇒ r))

Theorem “Right-monotonicity of ⇒”: (p ⇒ q) ⇒ ((r ⇒ p) ⇒ (r ⇒ q))

Theorem  “Left-antitonicity of <”: (p ≤ q) ⇒ ((q < r) ⇒ (p < r))

Theorem “Right-monotonicity of <”: (p ≤ q) ⇒ ((r < p) ⇒ (r < q))

Theorem  “Left-antitonicity of ≤”: (p ≤ q) ⇒ ((q ≤ r) ⇒ (p ≤ r))

Theorem “Right-monotonicity of ≤”: (p ≤ q) ⇒ ((r ≤ p) ⇒ (r ≤ q))

Theorem  “Weak left-antitonicity of <”: (p < q) ⇒ ((q < r) ⇒ (p < r))

Theorem “Weak right-monotonicity of <”: (p < q) ⇒ ((r < p) ⇒ (r < q))

6.8 “Indirect Equality” on Integers   Exercise 8_1

Following the “Ordered Domains” secion of LADM Chapter 15 “A Theory of Integers”, we provide the usual ordering relations on the integers and some of their properties. 

Theorem (15.47) “Indirect Equality” “Indirect Equality from below”:
  a = b  ≡  (∀ z • z ≤ a  ≡  z ≤ b)

Theorem “Indirect Equality” “Indirect Equality from above”:
  a = b  ≡  (∀ z • a ≤ z  ≡  b ≤ z)

Declaration: _↓_ : ℤ → ℤ → ℤ
Declaration: _↑_ : ℤ → ℤ → ℤ

Axiom (15.53) (15.53a) “Definition of ↓”:
   z ≤ x ↓ y  ≡  z ≤ x ∧ z ≤ y

Axiom (15.53) (15.53b) “Definition of ↑”:
   x ↑ y ≤ z ≡  x ≤ z ∧ y ≤ z

Theorem (15.54) “Symmetry of ↓”:  x ↓ y = y ↓ x

Theorem (15.54) “Symmetry of ↑”:  x ↑ y = y ↑ x

Theorem (15.55) “Associativity of ↓”: (x ↓ y) ↓ z = x ↓ (y ↓ z)

Theorem (15.55) “Associativity of ↑”: (x ↑ y) ↑ z = x ↑ (y ↑ z)

Theorem (15.56) “Idempotency of ↓”: x ↓ x = x

Theorem (15.56) “Idempotency of ↑”:  x ↑ x = x

Theorem (15.57) “Minimum is lower bound”: x ↓ y ≤ x  ∧  x ↓ y ≤ y

Theorem (15.57) “Maximum is upper bound”: x ≤ x ↑ y  ∧  y ≤ x ↑ y

Theorem (15.58) “At most via minimum”: x ≤ y  ≡  x ↓ y = x

Theorem (15.58) “At most via maximum”: x ≤ y  ≡  x ↑ y = y

7 Quantification

7.1 Universal ∀

Axiom “Leibniz for ∀ range”:
    (∀ x • R₁ ≡ R₂) ⇒ ((∀ x ❙ R₁ • P) ≡ (∀ x ❙ R₂ • P))

Axiom “Leibniz for ∀ body”:
    (∀ x • R ⇒ (P₁ ≡ P₂)) ⇒ ((∀ x ❙ R • P₁) ≡ (∀ x ❙ R • P₂))

Axiom (8.11) “Substitution” “Substitution into ∀”:
   (∀ x ❙ R • P)[y ≔ F] ≡ ∀ x ❙ R[y ≔ F] • P[y ≔ F]

Axiom (8.13) “Empty range for ∀”:
  (∀ x ❙ false • P)  ≡  true

Axiom (8.14) “One-point rule for ∀”:
  (∀ x ❙ x = E • P)  ≡  P[x ≔ E]

Axiom (8.15) “Distributivity of ∀ over ∧”:
  (∀ x ❙ R • P) ∧ (∀ x ❙ R • Q) ≡ (∀ x ❙ R • P ∧ Q)

Axiom (8.17) “Range split for ∀”:
     (∀ x ❙ R ∨ S  • P)  ∧  (∀ x ❙ R ∧ S  • P)
   ≡ (∀ x ❙ R      • P)  ∧  (∀ x ❙ S      • P)

Axiom (8.20) “Nesting for ∀”:
    (∀ x, y ❙ R ∧ S • P)
  ≡ (∀ x ❙ R • (∀ y ❙ S • P))

Theorem “Replacement in ∀”:
    (∀ y ❙ R ∧ e = f • P[x ≔ e])
  ≡ (∀ y ❙ R ∧ e = f • P[x ≔ f])

Axiom (8.20a) “Dummy list permutation for ∀”:
   (∀ x, y ❙ R • P) ≡ (∀ y, x ❙ R • P)

Theorem (8.19) “Interchange of dummies for ∀”:
    (∀ x ❙ R • (∀ y ❙ S • P))
  ≡ (∀ y ❙ S • (∀ x ❙ R • P))

Axiom (9.2) “Trading for ∀”:
   (∀ x ❙ R • P) ≡ (∀ x • R ⇒ P)

Theorem (9.3) (9.3a) “Trading for ∀”:
   (∀ x ❙ R • P) ≡ (∀ x • ¬ R ∨ P)

Theorem (9.3) (9.3b) “Trading for ∀”:
   (∀ x ❙ R • P) ≡ (∀ x • R ∧ P ≡ R)

Theorem (9.3) (9.3b) “Trading for ∀”:
   (∀ x ❙ R • P) ≡ (∀ x • R ∧ P ≡ R)

Theorem (9.3) (9.3c) “Trading for ∀”:
   (∀ x ❙ R • P) ≡ (∀ x • R ∨ P ≡ P)

Theorem (9.4) (9.4a) “Trading for ∀”:
   (∀ x ❙ Q ∧ R • P) ≡ (∀ x ❙ Q • R ⇒ P)

Theorem (9.4) (9.4b) “Trading for ∀”:
   (∀ x ❙ Q ∧ R • P) ≡ (∀ x ❙ Q • ¬ R ∨ P)

Theorem (9.4) (9.4c) “Trading for ∀”:
   (∀ x ❙ Q ∧ R • P) ≡ (∀ x ❙ Q • R ∧ P ≡ R)

Theorem (9.4) (9.4d) “Trading for ∀”:
   (∀ x ❙ Q ∧ R • P) ≡ (∀ x ❙ Q • R ∨ P ≡ P)

Theorem “Leibniz for ∀ body”:
    (∀ x ❙ R • P₁ ≡ P₂) ⇒ ((∀ x ❙ R • P₁) ≡ (∀ x ❙ R • P₂))

Theorem (8.18) “Range split for ∀”:
     (∀ x ❙ R ∨ S  • P)
   ≡ (∀ x ❙ R      • P)
   ∧ (∀ x ❙ S      • P)

Axiom (9.5) “Distributivity of ∨ over ∀”:
    P ∨ (∀ x ❙ R • Q) ≡ (∀ x ❙ R • P ∨ Q)

Theorem (9.6): P ∨ (∀ x • ¬ R) ≡ (∀ x ❙ R • P)

Theorem “Distributivity of ⇒ over ∀”: P ⇒ (∀ x ❙ R • Q) ≡ (∀ x ❙ R • P ⇒ Q)

Theorem (9.7) “Distributivity of ∧ over ∀”:
    ¬(∀ x • ¬ R)  ⇒  (P ∧ (∀ x ❙ R • Q)  ≡  (∀ x ❙ R • P ∧ Q))

Theorem (9.8) “True ∀ body”: (∀ x ❙ R • true)

Theorem “Introducing fresh ∀”: P ⇒ (∀ x ❙ R • P)

Theorem (9.9) “Sub-distributivity of ∀ over ≡”:
   (∀ x ❙ R • P ≡ Q)
   ⇒ ((∀ x ❙ R • P) ≡ (∀ x ❙ R • Q))

Theorem (9.10) “Range weakening for ∀” “Range strengthening for ∀”:
    (∀ x ❙ Q ∨ R • P) ⇒ (∀ x ❙ Q • P)

Theorem (9.11) “Body weakening for ∀” “Body strengthening for ∀”:
    (∀ x ❙ R • P ∧ Q) ⇒ (∀ x ❙ R • P)

Theorem (9.12) “Monotonicity of ∀” “Body monotonicity of ∀”:
    (∀ x ❙ R • Q ⇒ P) ⇒ ((∀ x ❙ R • Q) ⇒ (∀ x ❙ R • P))

7.2 Sum Σ

Axiom “Leibniz for ∑ range”:
    (∀ x • R₁ ≡ R₂) ⇒ (∑ x ❙ R₁ • E) = (∑ x ❙ R₂ • E)

Axiom “Leibniz for ∑ body”:
    (∀ x • R ⇒ E₁ = E₂) ⇒ (∑ x ❙ R • E₁) = (∑ x ❙ R • E₂)

Axiom (8.13) “Empty range for ∑”:
  (∑ x ❙ false • E)  =  0

Axiom (8.14) “One-point rule for ∑”:
  (∑ x ❙ x = D • E)  =  E[x ≔ D]

Axiom (8.15) “Distributivity of ∑ over +”:
  (∑ x ❙ R • E₁ + E₂) = (∑ x ❙ R • E₁) + (∑ x ❙ R • E₂)

Axiom (8.17) “Range split for ∑” “Range split”:
     (∑ x ❙ Q ∨ R  • E)  +  (∑ x ❙ Q ∧ R  • E)
   = (∑ x ❙ Q      • E)  +  (∑ x ❙ R      • E)

Theorem (8.16) “Disjoint range split for ∑”:
   (∀ x • Q ∧ R ≡ false) ⇒
   ((∑ x ❙ Q ∨ R • E) = (∑ x ❙ Q • E) + (∑ x ❙ R • E))

Axiom (8.20) “Nesting for ∑”:
    (∑ x ❙ Q • (∑ y ❙ R • E))
  = (∑ x, y ❙ Q ∧ R • E)

Theorem “Replacement in ∑”:
    (∑ x ❙ R ∧ e = f • E[y ≔ e])
  = (∑ x ❙ R ∧ e = f • E[y ≔ f])

Axiom (8.20a) “Dummy list permutation for ∑”:
   (∑ x, y ❙ R • E) = (∑ y, x ❙ R • E)

Theorem (8.19) “Interchange of dummies”:
    (∑ x ❙ Q • (∑ y ❙ R • P))
  = (∑ y ❙ R • (∑ x ❙ Q • P))

Axiom (8.21) “Dummy renaming for ∑”, “α-conversion”:
  (∑ x ❙ R • E) = (∑ y ❙ R[x ≔ y] • E[x ≔ y])

Axiom “Distributivity of · over ∑”:
    a · (∑ x ❙ R • E) = (∑ x ❙ R • a · E)

Theorem “Zero ∑ body”: (∑ x ❙ R • 0) = 0

Theorem “Constant range conjunction in ∑”:
    (∑ x ❙ P ∧ R • F) = if P then (∑ x ❙ R • F) else 0 fi

Theorem “Conditional one-point rule for ∑”:
  (∑ x ❙ P ∧ x = E • F) = if P[x ≔ E] then F[x ≔ E] else 0 fi

7.3 Sum Quantification for ℕ   Exercise 6_5

Theorem “Split off term” “Split off term at top”:
    (∑ i : ℕ ❙ i < suc n • E) = (∑ i : ℕ ❙ i < n • E) + E[i ≔ n]

Theorem “Split off term” “Split off term at top”:
    m ≤ n ⇒
    (∑ i ❙ m ≤ i < suc n • E) = (∑ i ❙ m ≤ i < n • E) + E[i ≔ n]

Theorem “Split off term at top using ≤”:
    (∑ i ❙ i ≤ suc n • E) = (∑ i ❙ i ≤ n • E) + E[i ≔ suc n]

Theorem “Odd-number sum”:
    (∑ i : ℕ ❙ i < n • suc i + i) = n · n

Theorem “Sum the numbers”:
    2 · (∑ i ❙ i ≤ n • i) = n · suc n

7.4 Quantification Proofs: Monotonicity of Sum Quantification in ℕ   Homework 12

Theorem “Addition is non-decreasing”: a ≤ a + b

Theorem “Range weakening for ∑”:
     (∑ x ❙ Q • E) ≤ (∑ x ❙ Q ∨ R • E)

Theorem “Range weakening for ∑”:
    (∑ x ❙ Q ∧ R • E) ≤ (∑ x ❙ R • E)

Theorem “Range-monotonicity of ∑”:
     (∀ x • Q ⇒ R) ⇒ ((∑ x ❙ Q • E) ≤ (∑ x ❙ R • E))

Theorem “Body increasing for ∑”:
    (∑ x ❙ R • E) ≤ (∑ x ❙ R • D + E)

Theorem “Cancellation of monus”:  b ≤ a  ⇒  (a - b) + b = a

Theorem “Body-monotonicity of ∑”:
    (∀ x ❙ R • D ≤ E) ⇒ ((∑ x ❙ R • D) ≤ (∑ x ❙ R • E))

7.5 Practice with Universal and Existential Quantification in the setting of ℕ   Homework 11_2

Theorem “Unboundedness of ℕ”: ∀ n : ℕ • ∃ m : ℕ • n < m

Theorem “Unboundedness of ℕ”: ∀ n : ℕ • ∃ m : ℕ • n < m

Theorem “Addition does not associate mutually with monus”:
  ¬ (∀ k : ℕ • ∀ m : ℕ • ∀ n : ℕ • k + (m - n) = (k + m) - n)

8 Reverse Correctness Presentation   Homework_5_1

In lecture and in the homework, we have stressed that assignment command calculations should ‘begin at the bottom’ and work up; as such, it is more ‘natural’ to begin our calculation with the ‘bottom part’ at the top and work our way down to the other part.

To do so, we use the ‘flipped around’ assignment connective: 

    Axiom “Definition of ⁅_⁆⇐”:   Q ⁅ C ⁆⇐ P  ≡  P ⇒⁅ C ⁆ Q

This is similar to the arithmetic ordering: 

    y ≥ x  ≡  x ≤ y

It is the same thing, but the order has been flipped to make writing our calculations the same way we actually think of them: With the post-condition first, then eventually obtaining the pre-condition.

Here is a demonstration… 

     Lemma “Demo”: x + y = 13    ⇒⁅ x := x + 7 ⁆   x + y = 20
     Proof:
         x + y = 20
       ⁅ x := x + 7 ⁆⇐ ⟨ “Assignment” ⟩
         (x + y = 20)[x ≔ x + 7]
       ≡⟨ Substitution ⟩
         x + 7 + y = 20
       ≡⟨ Fact `20 = 13 + 7` ⟩
         x + 7 + y = 13 + 7
       ≡⟨ “Cancellation of +” ⟩
         x + y = 13

This ‘flipped around’ notation is only superficial, and so it also applies to sequential commands, as follows. 

     Lemma “Demo”:  j + k = S
                   ⇒⁅ j  := j + 1⍮ k := k + 1 ⁆
                    j + k = S + 2
     Proof:
         j + k = S + 2
       ⁅ k := k + 1 ⁆⇐⟨ “Assignment” ⟩
         (j + k = S + 2)[k ≔ k + 1]
       ≡⟨ Substitution ⟩
          j + k + 1 = S + 2
       ⁅ j := j + 1 ⁆⇐⟨ “Assignment” ⟩
         (j + k + 1 = S + 2)[j ≔ j + 1]
       ≡⟨ Substitution — and sym & assoc of + ⟩
         j + k + 1 + 1 = S + 2
       ≡⟨ Fact `1 + 1 = 2` ⟩
         j + k + 2 = S + 2
       ≡⟨ “Cancellation of +” ⟩
         j + k = S

Note that the seqence of the assignment in the proof is “along the ⇐ arrows”, that is, if you are reading and/or writing top-down, you encounter the last assignment first! 

Lemma “Set”: true ⇒⁅ p := q ⁆ (p ≡ q)

Lemma “Increment”: x = 0  ⇒⁅ x := x + q ⁆   x = q

Lemma “Stay Simple”:   q = a · c
                      ⇒⁅ q := q + c · c ⍮ a := a + c  ⁆
                       q = a · c

Lemma “Square Suc”: (n + 1) · (n + 1) = n · n + 2 · n + 1

Lemma “Stay squared”:   s = n · n
                      ⇒⁅ s := s + 2 · n + 1⍮ n := n + 1 ⁆
                        s = n · n

9 Residuals   Assignment 3

9.1 Implication is “division” for the Booleans … !?

Declaration: _÷_ : ℕ → ℕ → ℕ   ╍╍╍  \div
Axiom “Characterisation of ÷”:  k · m ≤ n  ≡  k ≤ n ÷ m

Theorem “Sub-cancellation of ÷”:  (a ÷ b) · b ≤ a

Theorem “Characterisation of ⇐”:  (k ∧ m) ⇒ n  ≡  k ⇒ (n ⇐ m)

Theorem “Characterisation of ⇒”:  (k ∧ m) ⇒ n  ≡  k ⇒ (m ⇒ n)

Theorem “Sub-cancellation of ⇐”:  (a ⇐ b) ∧ b   ⇒   a

Declaration: _／_ : τ → τ → τ  ╍╍╍  “over”, \over
Declaration: _＼_ : τ → τ → τ  ╍╍╍  “under”, \under
Declaration: _⨾_ : τ → τ → τ   ╍╍╍  “and then”, \;;
Declaration: Id : τ           ╍╍╍   “identity”

Axiom “Associativity of ⨾”:  (x ⨾ y) ⨾ z  =  x ⨾ (y ⨾ z)
Axiom “Left-identity of ⨾”:  Id ⨾ x = x
Axiom “Right-Identity of ⨾”: x ⨾ Id = x

Axiom “Characterisation of ／”:  a ⨾ b ⊑ c  ≡  a ⊑ c ／ b
Axiom “Characterisation of ＼”:  a ⨾ b ⊑ c  ≡  b ⊑ a ＼ c

Theorem “Cancellation of ／”: (a ／ b) ⨾ b ⊑ a

Theorem “Cancellation of ＼”: a ⨾ (a ＼ b) ⊑ b

9.2 Enriched Indirect Reasoning

Theorem “Enriched indirect equality” “Indirect equality”:
   P[z ≔ x] ∧ P[z ≔ y]
   ⇒  ((∀ z ❙ P • z ⊑ x ≡ z ⊑ y)  ≡  x = y)

Theorem  “Indirect equality”: (∀ z • z ⊑ x ≡ z ⊑ y)  ≡  x = y

Theorem  “Indirect equality”: (∀ z • z ≤ x ≡ z ≤ y)  ≡  x = y

Theorem  “Indirect equality”: (∀ z • z ⇒ x  ≡  z ⇒ y)  ≡  x = y

Theorem “Dividing a division”: (a ÷ b) ÷ c  =  a ÷ (c · b)

Theorem “Dividing a division”: ((a ⇐ b) ⇐ c)  =  (a ⇐ (c ∧ b))

Theorem “Dividing a division”: (a ／ b) ／ c  =  a ／ (c ⨾ b)

Theorem “Dividing a division”: a ＼ (b ＼ c)  =  (b ⨾ a) ＼ c

Theorem “Archimedian Property”: ∀ m • ∀ n • ∃ k •  m · k  ≤  n

9.3 A meaning of “groups” ⊕, ⨾, ˘, ⁻¹; “lattices” ⊑, ⊓, ⊔; “residuals” ╱, ╲

Before continuing, you may have seen ⊑ as a placeholder (metavariable, abstraction) of notions of order that you may come to see later in your CS studies, such as at-most ≤, divisibility ∣, set-inclusion ⊆, structure-inclusion (graphs, etc), program-refinement, propositional strength ⇒.

We can make the following “interpretation”:

Symbol Clothes Interpretation
𝓍 Putting on the article of clothing 𝓍
x ˘, or x⁻¹ Taking off the article of clothing 𝓍 ⟦ Maybe you see _˘ in A4. ⟧
𝓍 ⨾ 𝓎 (“⊕”) Wearing clothes 𝓍 “and then” wearing 𝓎 —e.g., socks then shoes
𝓎 ⁻¹ ⨾ 𝓍 ⁻¹ “Taking off” clothes” 𝓎 and then “taking off” 𝓍 —e.g., shoes off then socks off
𝓍 ⊑ 𝓎 The articles of clothes 𝓍 “can be found among” the pile of clothes 𝓎
𝓍 ⊓ 𝓎 The accessories needed for “both” kinds of clothes 𝓍 and 𝓎
𝓍 ⊔ 𝓎 Possible accessories, clothes, that go well with clothes 𝓍 “or” clothes 𝓎
𝓍 ╱ 𝓎 Wear as much clothes as possible “and-then” wear 𝓎, so the wardrobe is in the pile of clothes 𝓍
𝓍 ╲ 𝓎 Wear 𝓍 “first and-then” wear as much clothes as possible, so the wardrobe is in the pile of clothes 𝓎

9.4 Monotonicity and Strengthening Proofs

Theorem “Cancellation of ／”: (a ／ b) ⨾ b ⊑ a

Theorem “Cancellation of ＼”: a ⨾ (a ＼ b) ⊑ b

Theorem “Cancellation by ／” “Right-division of multiples”: a ⊑ (a ⨾ b) ／ b

Theorem “Cancellation by ＼” “Left-division of multiples”: b ⊑ a ＼ (a ⨾ b)

Theorem “Monotonicity of ⨾”: a ⊑ a′ ⇒ a ⨾ b ⊑ a′ ⨾ b

Theorem “Monotonicity of ⨾”: b ⊑ b′ ⇒ a ⨾ b ⊑ a ⨾ b′

Theorem “Monotonicity of ⨾”: a ⊑ a′ ∧ b ⊑ b′ ⇒ a ⨾ b ⊑ a′ ⨾ b′

Theorem “Numerator monotonicity”: a ⊑ a′ ⇒  a ／ b ⊑ a′ ／ b

Theorem “Numerator monotonicity”: b ⊑ b′ ⇒  a ＼ b ⊑ a ＼ b′

Theorem “Denominator antitonicity”: b′ ⊑ b ⇒  a ／ b ⊑ a ／ b′

Theorem “Denominator antitonicity”: a′ ⊑ a ⇒  a ＼ b ⊑ a′ ＼ b

10 Set Theory   Homework_15

Set theory is based on the membership relation _∈_ (type \in).

In typed set theory, we also have, for each type t, a separate type set t for sets with elements of type t.

A membership relationship “x ∈ S” then only makes sense of an x of type t if S is of type set t. This is formalised by giving _∈_ the type t → set t → 𝔹, where t is a type variable (as in the typing of equality, _=_ : t → t → 𝔹): 

Declaration: set : Type → Type

Declaration: 𝐔 : set t

Declaration: _∈_ : t → set t → 𝔹
Explanation: e ∈ S ≔ “`e` is an element of `S`.”
Explanation: e ∈ S ≔ “item `e` is an element of the set `S`.”

Axiom (11.4) “Set extensionality”:
   S = T  ≡  (∀ e  •  e ∈ S  ≡  e ∈ T)

10.1 Inclusion

Declaration: _⊆_ : set t → set t → 𝔹

Axiom (11.13) “Subset” “Definition of ⊆” “Set inclusion”:
   S ⊆ T  ≡  (∀ e ❙ e ∈ S • e ∈ T)

Corollary “Subset” “Definition of ⊆” “Set inclusion”:
   S ⊆ T  ≡  (∀ e • e ∈ S ⇒ e ∈ T)

Theorem “Subset membership” “Casting”:
    X ⊆ Y ⇒ x ∈ X ⇒ x ∈ Y

Theorem (11.59) “Transitivity of ⊆”: X ⊆ Y ⇒ Y ⊆ Z ⇒ X ⊆ Z

Theorem (11.58) “Reflexivity of ⊆”: X ⊆ X

Theorem (11.57) “Antisymmetry of ⊆”: X ⊆ Y ⇒ Y ⊆ X ⇒ X = Y

Theorem (11.57) “Antisymmetry of ⊆”: X ⊆ Y ⇒ Y ⊆ X ⇒ X = Y

Theorem (11.57) “Antisymmetry of ⊆”: X ⊆ Y ⇒ Y ⊆ X ⇒ X = Y

10.2 Complement

The complement of a set S, written ~ S, is the collection of elements that are not in S. 

Declaration: ~_ : set t → set t

Axiom “Complement”: e ∈ ~ S  ≡ ¬ (e ∈ S)

Theorem (11.19) “Self-inverse of complement”: ~ (~ S) = S

Theorem “Lower ~ connection for ⊆”:
    ~ X ⊆ Y  ≡  ~ Y ⊆ X

Theorem “Upper ~ connection for ⊆”:
    X ⊆ ~ Y  ≡  Y ⊆ ~ X

10.3 Union and Intersection

Declaration: _∪_ , _∩_ : set t → set t → set t

Axiom “Union”:          e ∈ S ∪ T  ≡  e ∈ S  ∨  e ∈ T
Axiom “Intersection”:   e ∈ S ∩ T  ≡  e ∈ S  ∧  e ∈ T

Theorem (11.45) “Inclusion via ∪”:  S ⊆ T  ≡  S ∪ T = T

10.4 Pairs and Cartesian Products

The pair consisting of the two constituents `b` and `c`, in that order, is written `⟨ b , c ⟩`.

Pairs are equal exactly if their respective constituents are equal: 

Axiom (14.2) “Pair equality”: ⟨ b, c ⟩ =  ⟨ b', c' ⟩  ≡  b = b' ∧ c = c'

If `t` and `u` are types, the type of pairs with first constituent in `t` and second constituent in `u` is written `❰ t, u ❱`. (You type `\<!` for `❰` and `\>!` for `❱`, but you will probably not need these a lot.)

The pair projections for pairs with any constituent types: 

Declaration: fst : ❰ t , u ❱ → t
Declaration: snd : ❰ t , u ❱ → u

Axiom “Definition of `fst`”: fst ⟨ x, y ⟩ = x
Axiom “Definition of `snd`”: snd ⟨ x, y ⟩ = y

Axiom “Pair equality”: p = q  ≡  fst p = fst q  ∧  snd p = snd q

We use `_×_` for Cartesian product of sets only, not for types: 

Declaration: _×_ : set t → set u → set ❰ t , u ❱

Axiom “Membership in ×”:
  p ∈ S × T  ≡  fst p ∈ S ∧ snd p ∈ T

Theorem (14.4) “Membership in ×”:
    ⟨ x , y ⟩ ∈ S × T  ≡  x ∈ S ∧ y ∈ T

Theorem “Pair extensionality”: p = ⟨ fst p , snd p ⟩

Theorem (14.5) “Membership in swapped ×”:
    ⟨ x , y ⟩ ∈ S × T  ≡  ⟨ y , x ⟩ ∈ T × S

Theorem (14.6) “Empty factor in ×”:
    S = {}  ⇒  S × T = {}

Declaration: swap-× : ❰ t, u ❱ → ❰ u, t ❱
Axiom “Definition of `swap-×`”: swap-× ⟨ x, y ⟩ = ⟨ y, x ⟩

Theorem “fst after swap-×”: fst (swap-× p) = snd p

Theorem “snd after swap-×”: snd (swap-× p) = fst p

11 Relations

11.1 Relations via Set Theory   Homework 17

11.1.1 Domain and Range

Declaration:  Dom : (A ↔ B) → set A
Declaration:  Ran : (A ↔ B) → set B

Axiom “Membership in `Dom`”:
  x ∈ Dom R  ≡  ∃ y • x ⦗ R ⦘ y

Axiom “Membership in `Ran`”:
  y ∈ Ran R  ≡  ∃ x • x ⦗ R ⦘ y

Theorem “Domain of union”: Dom (R ∪ S) = Dom R ∪ Dom S

Theorem “Domain of intersection”: Dom (R ∩ S) ⊆ Dom R ∩ Dom S

11.1.2 Relation Converse

Declaration: _˘ : (A ↔ B) → (B ↔ A)

Axiom “Relation converse” “Relationship via ˘”:
    y ⦗ R ˘ ⦘ x  ≡  x ⦗ R ⦘ y

Theorem “Self-inverse of ˘”:   R ˘ ˘  =  R

Theorem “Monotonicity of ˘”: R ⊆ S      ⇒  R ˘ ⊆ S ˘

Theorem “Isotonicity of ˘”: R ⊆ S   ≡   R ˘ ⊆ S ˘

Theorem “Domain of converse”: Dom (R ˘) = Ran R

Theorem “Converse of ∩”:     (R ∩ S) ˘  =  R ˘ ∩ S ˘

11.1.3 Relation Composition

Declaration: _⨾_ : (A ↔ B) → (B ↔ C) → (A ↔ C)

Axiom “Relation composition”:
    a ⦗ R ⨾ S ⦘ c  ≡  ∃ b • a ⦗ R ⦘ b ∧ b ⦗ S ⦘ c

Theorem “Converse of ⨾”:    (R ⨾ S) ˘    =  S ˘ ⨾ R ˘

11.1.4 Polymorphic Identity

The only new item introduced in this section is the polymorphic identity relation Id.

Similar to how equality _=_ can be used at type A → A → 𝔹 for any type A, this new Id can be used at type A ↔ A at any type A: 

Declaration: Id : A ↔ A

The lecture slides present Id as abbreviation for 𝕀 𝐔.

(Remember that the blackboard-bold I symbol 𝕀 is obtained by typing \II, two upper-case i letters as in identity.)

Where this is used at type A ↔ A, it has also been written informally on the lecture slides as 𝕀 ⌞ A ⌟, using the convention that ⌞ A ⌟ stands for 𝐔 : set A. 

Axiom “Definition of `Id` via 𝕀”: Id = 𝕀 𝐔

With that, the direct correspondence between `Id` and `_=_` is easy to derive, and does not need to mention the type (that is, the “`A`” mentioned so far): 

Theorem “Identity relation” “Relationship via `Id`”:
    x ⦗ Id ⦘ y  ≡  x = y

Theorem “Converse of `Id`”: Id ˘        =  Id

Theorem “Left-identity of ⨾” “Identity of ⨾”:
    Id ⨾ R = R

Theorem “Right-identity of ⨾” “Identity of ⨾”:
    R ⨾ Id = R

11.1.5 Reflexivity

We define the reflexivity predicate for relations using the predicate-logic formulation: 

Declaration: reflexive : A ↔ A  →  𝔹
Axiom “Definition of reflexivity”:  reflexive R  ≡  ∀ x • x ⦗ R ⦘ x

Theorem “`Id` is reflexive”: reflexive Id

Theorem “Reflexivity”:  reflexive R  ≡  Id ⊆ R

Theorem “Composition of reflexive relations”:
  reflexive R ⇒ reflexive S ⇒ reflexive (R ⨾ S)

Theorem “Converse of reflexive relations”:
  reflexive R ⇒ reflexive (R ˘)

Theorem “Converse reflects reflectivity”:
  reflexive (R ˘) ⇒ reflexive R

11.1.6 Transitivity

We define the transitivity predicate for relations using the predicate-logic formulation: 

Declaration: transitive : A ↔ A  →  𝔹
Axiom “Definition of transitivity”:
    transitive R   ≡  ∀ x • ∀ y • ∀ z •
                        x ⦗ R ⦘ y ⦗ R ⦘ z  ⇒  x ⦗ R ⦘ z

Theorem “Converse of transitive relations”:
    transitive R ⇒ transitive (R ˘)

11.2 Relations via Set Theory I: Properties of the Basic Operators   Exercise 10_1

Theorem “Converse of {}”:     {} ˘  =  {}

Theorem “Converse of ∪”:     (R ∪ S) ˘  =  R ˘ ∪ S ˘

Theorem “Distributivity of ⨾ over ∪ to the right”
        “Distributivity of ⨾ over ∪”:
    Q ⨾ (R ∪ S)  =  Q ⨾ R  ∪  Q ⨾ S

Theorem “Sub-distributivity of ⨾ over ∩ to the right”
        “Sub-distributivity of ⨾ over ∩”:
     Q ⨾ (R ∩ S)  ⊆  Q ⨾ R  ∩  Q ⨾ S

Theorem “Associativity of ⨾”: (Q ⨾ R) ⨾ S = Q ⨾ (R ⨾ S)

Theorem “Monotonicity of ⨾ in first argument” “Monotonicity of ⨾”:
    Q ⊆ R  ⇒  Q ⨾ S ⊆ R ⨾ S

Theorem “Monotonicity of ⨾ in second argument” “Monotonicity of ⨾”:
    R ⊆ S  ⇒  Q ⨾ R ⊆ Q ⨾ S

Theorem “Characterisation of ∩”:
    Q ⊆ R ∩ S   ≡   Q ⊆ R  ∧ Q ⊆ (S : A ↔ B)

The modal rule can be seen as a kind of over-approximation of multiplicative inverse with respect to composition “~⨾~”.

In a field, for example in ℝ, if a has an inverse a⁻¹ (that is, if a · a⁻¹ = 1, which requires a ≠ 0), then you have: 

      a · b + c  =  a · (b + a⁻¹ · c)

Relation converse in general does not produce inverses, but still an “over-approximation to an inverse”, since the equation above turns into a relation inclusion: 

Theorem “Modal rule”:    (Q ⨾ R) ∩ S ⊆ Q ⨾ (R ∩ Q ˘ ⨾ S)

Theorem “Modal rule”:    (Q ⨾ R) ∩ S ⊆ (Q ∩ S ⨾ R ˘) ⨾ R

Theorem “Restricted identity property for 𝕀-Dom”:
     𝕀 (Dom R) ⨾ R = R

11.3 Relations via Set Theory II: Properties of the Basic Operators   Exercise 10_2

Declaration: P : Type
Explanation: P ≔ “Type of persons”

  We declare relations `C` and `B` with the following meanings:

  - `p ⦗ C ⦘ q` means “`p` called `q` (by phone)”
  - `p ⦗ B ⦘ q` means “`p` is a brother of `q`”

Declaration: C : P ↔ P
Declaration: B : P ↔ P

Declaration: Helen, Aos, Jun, Obama, Shirley, Alex, Jim, Jane : P

### Relationship to Predicate Logic

  From the following relationship statements,
  calculate “readable” predicate logic statements:

Calculation:
    Aos ⦗ C ⨾ B ⦘ Jun

Calculation:
    Aos ⦗ ~ (C ⨾ ~ B) ⦘ Jun

Calculation:
    Aos ⦗ ~ (~ C ⨾ B) ⦘ Jun

Calculation:
    Aos ⦗ ~ ((C ∩ ~ (B ⨾ C ˘)) ⨾ ~ B) ⦘ Jun

Calculation:
    (B ⨾ ({ Jun } × 𝐔)) ∩ (C ⨾ C ˘)  ⊆  Id

### Formalise Relation-Algebraically

Axiom “Helen called somebody who called her”: ?

Axiom “Aos called everybody who called a brother of Jun”: ?

Axiom “Aos hasn't called anybody who has called Jun”: ?

11.4 Relations via Set Theory: Counterexamples for Non-Properties of the Basic Operators   Exercise 10_3

Lemma “Membership in two-element set enumeration”: x ∈ {x, y}
Lemma “Membership in set enumeration”: x ∈ {u ❙ u = x ∨ R}

Theorem “Non-Isotonicity of ⨾ in first argument”:
    ¬(∀ Q : 𝔹 ↔ 𝔹 • ∀ R : 𝔹 ↔ 𝔹 • ∀ S : 𝔹 ↔ 𝔹
      • Q ⨾ S ⊆ R ⨾ S  ⇒  Q ⊆ R)

Theorem “Non-distributivity of ⨾ over ∩ to the right”:
    ¬ (∀ Q : 𝔹 ↔ 𝔹 • ∀ R : 𝔹 ↔ 𝔹 • ∀ S : 𝔹 ↔ 𝔹 • Q ⨾ R  ∩  Q ⨾ S  ⊆  Q ⨾ (R ∩ S))

11.5 Relations via Set Theory: Heterogeneous Relation Properties, starting from Relation-Algebraic Formulations   Homework 18

Theorem “Monotonicity of ∪”: A₁ ⊆ A₂ ⇒ (A₁ ∪ B) ⊆ (A₂ ∪ B)

Theorem “Monotonicity of ∪”: A₁ ⊆ A₂ ⇒ B₁ ⊆ B₂ ⇒ (A₁ ∪ B₁) ⊆ (A₂ ∪ B₂)

Theorem “Distributivity of ⨾ over ∪ to the left”
        “Distributivity of ⨾ over ∪”:
    (Q ∪ R) ⨾ S  =  Q ⨾ S  ∪  R ⨾ S

11.5.1 Univalence

A relation is univalent iff it relates each argument with at most one result. 

Declaration: is-univalent : A ↔ B  →  𝔹
Axiom “Definition of univalence”:    is-univalent R   ≡  R ˘ ⨾ R ⊆ Id

Theorem “Univalence of composition”:
     is-univalent R ⇒ is-univalent S ⇒ is-univalent (R ⨾ S)

Theorem “Univalence”:
      is-univalent R
   ≡  ∀ b₁ • ∀ b₂ • ∀ a • a ⦗ R ⦘ b₁ ∧ a ⦗ R ⦘ b₂ ⇒ b₁ = b₂

11.5.2 Totality

A relation is total if it relates each argument with at least one result. 

Declaration: is-total : A ↔ B  →  𝔹
Axiom “Definition of totality”:      is-total R       ≡  Id ⊆ R ⨾ R ˘

Theorem “Totality of union”:
    is-total R ⇒ is-total S ⇒ is-total (R ∪ S)

Theorem “Totality”: is-total R  ≡  ∀ a • ∃ b • a ⦗ R ⦘ b

Theorem “Domain of total relations”:   is-total R  ≡  𝐔 ⊆ Dom R

Theorem “Domain of total relations”:  is-total R  ≡  Dom R = 𝐔

11.5.3 Injectivity

Declaration: is-injective : A ↔ B  →  𝔹

Axiom “Definition of injectivity”:
    is-injective R    ≡   R ⨾ R ˘  ⊆  Id

Injectivity is dual (with respect to the direction of composition) to univalence, so the dualisation operator “`_˘`” (converse) converts between the two: 

Theorem “Injectivity of converse”:
    is-injective (R ˘) ≡  is-univalent R

Theorem “Univalence of converse”:
    is-univalent (R ˘)  ≡  is-injective R

Theorem “Injectivity”:
       is-injective R
    ≡  ∀ a₁ • ∀ a₂ • ∀ b • a₁ ⦗ R ⦘ b ∧ a₂ ⦗ R ⦘ b ⇒ a₁ = a₂

11.5.4 Surjectivity

Declaration: is-surjective : A ↔ B  →  𝔹

Axiom “Definition of surjectivity”:
    is-surjective R    ≡   Id  ⊆  R ˘ ⨾ R

Theorem “Totality of converse”:
    is-total (R ˘)  ≡  is-surjective R

Theorem “Surjectivity”:
    is-surjective R  ≡  (∀ b • (∃ a • a ⦗ R ⦘ b))

11.6 Cartesian Products and Relations

Lemma “Relationship via ×”: x ⦗ S × T ⦘ y  ≡  x ∈ S ∧ y ∈ T

Theorem (14.8) “Distributivity of × over ∪”:
    S × (T ∪ U) = (S × T) ∪ (S × U)

Theorem (14.8) “Distributivity of × over ∪”:
    (S ∪ T) × U = (S × U) ∪ (T × U)

Theorem (14.9) “Distributivity of × over ∩”:
    S × (T ∩ U) = (S × T) ∩ (S × U)

Theorem (14.9) “Distributivity of × over ∩”:
    (S ∩ T) × U = (S × U) ∩ (T × U)

Theorem “Non-empty sets”: S ≠ {} ≡ (∃ x • x ∈ S)

Theorem (14.7i): S ≠ {} ⇒ T ≠ {} ⇒ S × T = T × S ⇒ S = T

Theorem (14.7ii): T ≠ {} ⇒ S × T = T × S ⇒ S ⊆ T

Theorem (14.13): S ≠ {}  ⇒  S × T ⊆ S × U  ⇒  T ⊆ U

11.7 Abstract Relation Algebra: Inclusion, Composition, Converse, and Intersection   Exercise 11_1 11_2 12_2 12_3

The type constructor _↔_ for relation types is obtained by typing \rel, and has higher precedence than the function type constructor _→_. 

Declaration: _↔_ : Type → Type → Type

11.7.1 Inclusion

Declaration: _⊆_ : A ↔ B → A ↔ B → 𝔹
Axiom “Reflexivity of ⊆”: R ⊆ R
Lemma “Reflexivity of ⊆”: R = S  ⇒  R ⊆ S
Axiom “Transitivity of ⊆”: Q ⊆ R ⇒ R ⊆ S ⇒ Q ⊆ S
Axiom “Antisymmetry of ⊆”: R ⊆ S ⇒ S ⊆ R ⇒ R = S
Theorem “Transitivity of ⊆”: Q ⊆ R ∧ R ⊆ S ⇒ Q ⊆ S
Lemma “Flipped Transitivity of ⊆”: R ⊆ S ⇒ Q ⊆ R ⇒ Q ⊆ S

Theorem “Mutual inclusion”: R = S  ≡  R ⊆ S  ∧ S ⊆ R
Theorem “Indirect Relation Equality”
        “Indirect Relation Equality from below”:
    Q = R  ≡  (∀ S • S ⊆ Q  ≡  S ⊆ R)
Theorem “Indirect Relation Inclusion”
        “Indirect Relation Inclusion from above”:
    Q ⊆ R  ≡  (∀ S • R ⊆ S  ⇒  Q ⊆ S)

Declaration: _⊇_ : A ↔ B → A ↔ B → 𝔹
Axiom “Opposite inclusion”: R ⊇ S  ≡  S ⊆ R

11.7.2 Composition

Declaration: _⨾_ : A ↔ B → B ↔ C → A ↔ C
Axiom “Associativity of ⨾”: (Q ⨾ R) ⨾ S = Q ⨾ (R ⨾ S)
Axiom “Monotonicity of ⨾”:  P ⊆ Q  ⇒  R ⊆ S  ⇒  P ⨾ R ⊆ Q ⨾ S
Theorem “Monotonicity of ⨾”:  Q ⊆ R  ⇒  Q ⨾ S ⊆ R ⨾ S
Theorem “Monotonicity of ⨾”:  R ⊆ S  ⇒  Q ⨾ R ⊆ Q ⨾ S

Declaration: Id : A ↔ A
Axiom “Identity of ⨾”: Id ⨾ R = R
Axiom “Identity of ⨾”: R ⨾ Id = R

11.7.3 Converse

Declaration: _˘ : (A ↔ B) → (B ↔ A)
Axiom “Self-inverse of ˘”: R ˘ ˘  =  R
Lemma “Cancellation of ˘”:  R ˘ = S ˘  ≡  R = S
Axiom “Monotonicity of ˘”: R ⊆ S      ⇒  R ˘ ⊆ S ˘
Theorem “Isotonicity of ˘”:  R ⊆ S  ≡  R ˘ ⊆ S ˘
Axiom “Converse of `Id`”:  Id ˘        =  Id
Axiom “Converse of ⨾”:     (R ⨾ S) ˘    =  S ˘ ⨾ R ˘

11.7.4 Intersection

Declaration: _∩_ : A ↔ B → A ↔ B → A ↔ B

Axiom “Characterisation of ∩”  : Q ⊆ R ∩ S   ≡   Q ⊆ R  ∧ Q ⊆ S

Theorem “Weakening for ∩”      : Q ∩ R ⊆ Q  ∧  Q ∩ R ⊆ R
Theorem “Symmetry of ∩”        : Q ∩ R  ⊆  R ∩ Q
Corollary “Symmetry of ∩”      : Q ∩ R  =  R ∩ Q
Theorem “Associativity of ∩”   : (Q ∩ R) ∩ S  ⊆  Q ∩ (R ∩ S)
Corollary “Associativity of ∩” : (Q ∩ R) ∩ S  =  Q ∩ (R ∩ S)
Theorem “Idempotency of ∩”     : R ∩ R = R
Theorem “Monotonicity of ∩”    : Q ⊆ R  ⇒  Q ∩ S ⊆ R ∩ S

Theorem “Inclusion via ∩”      : Q ⊆ R  ≡  Q ∩ R = Q

Theorem “Converse of ∩”        :     (R ∩ S) ˘  ⊆  R ˘ ∩ S ˘
Theorem “Converse of ∩”        :     (R ∩ S) ˘  =  R ˘ ∩ S ˘

Theorem “Sub-distributivity of ⨾ over ∩”:
    Q ⨾ (R ∩ S)  ⊆  Q ⨾ R  ∩  Q ⨾ S

11.7.5 Heterogeneous Properties

Declaration: reflexive : A ↔ A  →  𝔹
Declaration: symmetric : A ↔ A  →  𝔹
Declaration: transitive, idempotent : A ↔ A  →  𝔹
Declaration: equivalence, preorder : A ↔ A  →  𝔹
Declaration: antisymmetric, order : A ↔ A  →  𝔹

Axiom “Definition of reflexivity”:    reflexive R      ≡  Id ⊆ R
Axiom “Definition of symmetry”:       symmetric R      ≡  R ˘ ⊆ R
Axiom “Definition of transitivity”:   transitive R     ≡  R ⨾ R ⊆ R
Axiom “Definition of idempotency”:    idempotent R     ≡  R ⨾ R = R
Axiom “Definition of equivalence”:    equivalence R    ≡  reflexive R
                                                          ∧ symmetric R
                                                          ∧ transitive R
Axiom “Definition of preorder”:       preorder R       ≡  reflexive R
                                                          ∧ transitive R
Axiom “Definition of antisymmetry”:   antisymmetric R  ≡  R ∩ R ˘ ⊆ Id
Axiom “Definition of ordering”:       order R          ≡  reflexive R
                                                          ∧ antisymmetric R
                                                          ∧ transitive R

Theorem “Reflexivity of converse”  :    reflexive R ≡ reflexive (R ˘)
Theorem “Reflexivity of ⨾”         :    reflexive R ⇒ reflexive S ⇒ reflexive (R ⨾ S)

Lemma “Definition of symmetry”     :    symmetric R   ≡   R ˘ = R
Theorem “Symmetry of converse”     :    symmetric R ≡ symmetric (R ˘)

Theorem “Antisymmetry of converse” :  antisymmetric R  ≡  antisymmetric (R ˘)

Theorem “Converse of an order”     :  order E  ≡  order (E ˘)

11.7.6 Dedekind and Modal Rules

Axiom “Dedekind rule”:    (Q ⨾ R) ∩ S ⊆ (Q ∩ S ⨾ R ˘) ⨾ (R ∩ Q ˘ ⨾ S)
Theorem “Modal rule”:     (Q ⨾ R) ∩ S ⊆ (Q ∩ S ⨾ R ˘) ⨾ R
Theorem “Modal rule”:     (Q ⨾ R) ∩ S ⊆ Q ⨾ (R ∩ Q ˘ ⨾ S)

One simple consequence of any modal rule is the following theorem (also known as “co-difunctionality”); the name “Hesitation” is intended to suggest that whenever you can make a step forward to some place, you can also first make a step forward, then one back, and finally another one forward to the same place (due to the implicit assumption that the place you started from is still available for the backwards step after the first step forward). 

Theorem “Hesitation”: R ⊆ R ⨾ R ˘ ⨾ R

A transitive and symmetric relations is also called a partial equivalence relation (PER), where the word “partial” again really just means “not necessarily total”, which in the case of PERs would be understood more naturally as “not necessarily reflexive”.

This is justified by the fact that equivalence relations are total due to reflexivity. 

Theorem “PER factoring”:    symmetric Q ⇒ transitive Q ⇒  Q ⨾ R ∩ Q = Q ⨾ (R ∩ Q)
Theorem “Reflexive implies total”:    reflexive R  ⇒  total R
Theorem “Idempotency from symmetric and transitive”:    symmetric R ⇒ transitive R ⇒ idempotent R

Theorem “Right-distributivity of ⨾ with univalent over ∩”:
    univalent F  ⇒  F ⨾ (R ∩ S) = F ⨾ R ∩ F ⨾ S

Theorem “Swapping mapping across ⊆”:
    mapping F  ⇒  (R ⨾ F ⊆ S  ≡  R ⊆ S ⨾ F ˘)

11.7.7 Powers and Reflexive-transitive Closure

Associating to the right: _**_
Declaration: _**_ :  (A ↔ A)  →  ℕ  →  (A ↔ A)

Axiom “Definition of **”:  R ** 0    =  Id
Axiom “Definition of **”:  R ** suc i  =  R ⨾ R ** i

Theorem “Right-identity of **”: R ** 1 = R
Theorem “Addition in **”: R ** (i + j) = R ** i ⨾ R ** j

Declaration: _* : A ↔ A  →  A ↔ A
Axiom “Definition of `_*`”:    R * = (⋃ i : ℕ • R ** i)

Theorem “Characterisation of `_*`: Expanding”:  R ⊆ R *
Theorem “Characterisation of `_*`: Reflexivity”:  reflexive (R *)
Theorem “Characterisation of `_*`: Transitivity”:  transitive (R *)
Theorem “Characterisation of `_*`: Expansion of powers”:
    R ⊆ S  ⇒  reflexive S  ⇒  transitive S  ⇒ R ** i ⊆ S
Theorem “Characterisation of `_*`: Minimality”:
    R ⊆ S  ⇒  reflexive S  ⇒  transitive S  ⇒ R * ⊆ S

11.8 Operators Combining Sets and Relations   Homework 19

Associating to the right: _◁_ , _⩤_
Associating to the left: _▷_ , _⩥_

Theorem “Converse of ×”:  (A × B) ˘ = B × A

11.8.1 Domain and Range Restrictions

  - type “`\drestr`” for “`◁`” --- “domain restriction”,
  - type “`\ndrestr`” for “`⩤`” --- “negated domain restriction”, “domain antirestriction”,
  - type “`\rrestr`” for “`▷`” --- “range restriction”,
  - type “`\nrrestr`” for “`⩥`” --- “negated range restriction”, “range antirestriction”.

Declaration: _◁_ , _⩤_ : set t₁ → (t₁ ↔ t₂) → (t₁ ↔ t₂)
Declaration: _▷_ , _⩥_ : (t₁ ↔ t₂) → set t₂ → (t₁ ↔ t₂)

Axiom “Definition of ◁”:  A ◁ R = R ∩ (A × 𝐔)
Axiom “Definition of ▷”:  R ▷ B = R ∩ (𝐔 × B)
Axiom “Definition of ⩤”:  A ⩤ R = R ∩ (~ A × 𝐔)
Axiom “Definition of ⩥”:  R ⩥ B = R ∩ (𝐔 × ~ B)

Lemma “Definition of ⩤ via ◁”:   A ⩤ R  =  ~ A ◁ R
Lemma “Definition of ⩥ via ▷”:   R ⩥ B  =  R ▷ ~ B
Theorem “Distributivity of ◁ over set intersection”:  (A ∩ B) ◁ R = (A ◁ R) ∩ (B ◁ R)
Theorem “Distributivity of ◁ over relation union”:    A ◁ (R ∪ S) = (A ◁ R) ∪ (A ◁ S)
Theorem “Definition of ▷ via ◁”:  R ▷ B  =  (B ◁ R ˘) ˘
Theorem “Definition of ◁ via ▷”:  A ◁ R  =  (R ˘ ▷ A) ˘
Theorem “Distributivity of ▷ over set intersection”:    R ▷ (B ∩ C) = (R ▷ B) ∩ (R ▷ C)
Theorem “Distributivity of ▷ over relation union”:    (R ∪ S) ▷ B = (R ▷ B) ∪ (S ▷ B)
Theorem “Range of ◁”: Ran (R ▷ B) = Ran R ∩ B
Theorem “Relationship via ◁” “Domain restriction”:    x ⦗ A ◁ R ⦘ y  ≡  x ∈ A ∧ x ⦗ R ⦘ y
Theorem “Relationship via ▷” “Range restriction”:    x ⦗ R ▷ B ⦘ y  ≡  x ⦗ R ⦘ y ∈ B
Theorem “Relationship via ⩤” “Domain antirestriction”:    x ⦗ A ⩤ R ⦘ y  ≡  ¬ (x ∈ A) ∧ x ⦗ R ⦘ y
Theorem “Domain restriction by `Dom`”:  Dom S ◁ S = S
Theorem “Domain restriction via ⨾”:    A ◁ R = 𝕀 A ⨾ R
Theorem “Range restriction via ⨾”:    R ▷ B = R ⨾ 𝕀 B
Theorem “Switching ▷ and ◁ in ⨾”:    (R ▷ B) ⨾ S  =  R ⨾ (B ◁ S)
Theorem “Mutual associativity of ⨾ with ▷”:    (R ⨾ S) ▷ C  =  R ⨾ (S ▷ C)

11.8.2 Relational Image

Declaration: _⦇_⦈ : (t₁ ↔ t₂) → set t₁ → set t₂

Axiom “Definition of ⦇_⦈”: R ⦇ A ⦈ = Ran (A ◁ R)

Theorem “Relational image”:  y ∈ R ⦇ A ⦈  ≡  (∃ x ❙ x ∈ A • x ⦗ R ⦘ y)

11.8.3 Relation Override

Declaration: _⊕_ : (t₁ ↔ t₂) → (t₁ ↔ t₂) → (t₁ ↔ t₂)

Axiom “Definition of ⊕”:   R ⊕ S  =  (Dom S ⩤ R) ∪ S

Theorem “Relation override”:
    x ⦗ R ⊕ S ⦘ y  ≡  if x ∈ Dom S then x ⦗ S ⦘ y else x ⦗ R ⦘ y fi

Author: Musa Al-hassy and Wolfram Kahl

Created: 2020-12-15 Tue 08:12

Validate