Theorem List
Mathematics for Computing, CS/SE 2DM3, Fall 2020
Table of Contents
- 1. Inequality
- 2. Equational Theory of Integers Exercise_2
- 3. Propositional Calculus
- 3.1. Conjunction Exercise 3_3
- 3.2. Disjunction Exercise_3_2 Homework_5_2
- 3.3. Formalising “Knights and Knaves” Puzzles Exercise_3_1
- 3.4. Leibniz's Rule as an Axiom, Replacement Theorems Exercise 5_1 Homework 7_2
- 3.5. Implication Exercise 4_1 Homework 7_1
- 3.6. Conditionals Homework 9_2
- 4. Abstract Algebra: Magmas, Monoids, and Groups Assignment 1
- 5. Inductively Defined Types
- 5.1. Inductive Theory of the Natural Numbers Exercise 4_2
- 5.2. Predecessors in the Inductive Theory of the Natural Numbers Homework 8_5
- 5.3. Inductive Theory of Sequences Exercise_9_1 Homework_14
- 5.4. Binary Trees Exercise 12
- 6. Order Theory Assignment_2
- 6.1. Introduction and Uniqueness of Bottoms
- 6.2. Uniqueness of Tops
- 6.3. Divisibility
- 6.4. Meets and joins: Generalising Minima and Maxima
- 6.5. Order on Integers Exercise 7_3
- 6.6. Positivity of Integers Exercise 7_1 7_2
- 6.7. Mixed Monotonicity Exercise 8_2 8_3
- 6.8. “Indirect Equality” on Integers Exercise 8_1
- 7. Quantification
- 8. Reverse Correctness Presentation Homework_5_1
- 9. Residuals Assignment 3
- 10. Set Theory Homework_15
- 11. Relations
- 11.1. Relations via Set Theory Homework 17
- 11.2. Relations via Set Theory I: Properties of the Basic Operators Exercise 10_1
- 11.3. Relations via Set Theory II: Properties of the Basic Operators Exercise 10_2
- 11.4. Relations via Set Theory: Counterexamples for Non-Properties of the Basic Operators Exercise 10_3
- 11.5. Relations via Set Theory: Heterogeneous Relation Properties, starting from Relation-Algebraic Formulations Homework 18
- 11.6. Cartesian Products and Relations
- 11.7. Abstract Relation Algebra: Inclusion, Composition, Converse, and Intersection Exercise 11_1 11_2 12_2 12_3
- 11.8. Operators Combining Sets and Relations Homework 19
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.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:
- 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.
- 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’.
The Booleans are ordered by implication,
⇒
.This relationship is completely determined by the requirement that “
false ⇒ true
”; i.e.,false
is smaller-thantrue
.Indeed, the collection of things that satisfy
false
is smaller than the collection of things that satisfytrue
, 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