commit 55177fdde1b807b42418f2d3be76a117af5a5200
parent fc069dce718c31e7bea098053be45b3e4005f9de
Author: Alex Balgavy <alex@balgavy.eu>
Date: Wed, 9 Dec 2020 23:07:14 +0100
Update logical verification notes
Diffstat:
3 files changed, 131 insertions(+), 0 deletions(-)
diff --git a/content/logical-verification/Basic mathematical structures.md b/content/logical-verification/Basic mathematical structures.md
@@ -0,0 +1,50 @@
++++
+title = 'Basic mathematical structures'
++++
+# Basic mathematical structures
+## Type classes
+
+Different structures:
+1. semigroups: satisfy `x * (y * z) = (x * y) * z`
+2. monoids: satisfy 1 above and `x * 1 = x ∧ 1 * x = x`
+3. groups: satisfy 1 and 2 above, and `x * x⁻¹ = 1 ∧ x⁻¹ * x = 1`
+
+These are type classes in Lean.
+
+We can define our own type, integers modulo 2, and register it as an additive group:
+
+```lean
+inductive my_int : Type
+| zero
+| one
+
+def my_int.add : my_int → my_int → my_int
+| my_int.zero a := a
+| a my_int.zero := a
+| my_int.one my_int.one := my_int.zero
+
+@[instance] def my_int.add_group : add_group my_int :=
+{ add := my_int.add,
+ add_assoc :=
+ by intros a b c; cases' a; cases' b; cases' c; refl,
+ zero := my_int.zero,
+ zero_add := by intro a; cases' a; refl,
+ add_zero := by intro a; cases' a; refl,
+ neg := λa, a,
+ add_left_neg := by intro a; cases' a; refl }
+```
+
+## Lists, multisets, finite sets
+For finite collections of elements, available structures:
+- list: order and duplicates matter
+- multiset: only duplicates matter
+- finsets: neither order nor duplicates matter
+
+`dec_trivial` is a lemma you can use for trivial decidable goals (i.e. if there are no variables in the expression).
+
+## Order type classes
+For example `(Ν, ≤)` or `(set Ν, ⊆)`.
+
+- preorder: reflexivity (`x ≤ x`), transitivity (`x ≤ y → y ≤ z → x ≤ z`)
+- partial order: preorder with antisymmetry (`x ≤ y → y ≤ x → x = y`)
+- linear order: partial order with `x ≤ y ∨ y ≤ x`
diff --git a/content/logical-verification/Rational and real numbers.md b/content/logical-verification/Rational and real numbers.md
@@ -0,0 +1,79 @@
++++
+title = 'Rational and real numbers'
++++
+# Rational and real numbers
+## Rational numbers
+Rational numbers are fractions.
+As integers are naturals with a minus operator, rationals are integers with a division operator.
+
+```lean
+structure fraction :=
+(num : Ζ)
+(denom : Ζ)
+(denom_ne_zero : denom ≠ 0)
+```
+
+You can then define equivalence on a fraction:
+
+```lean
+@[instance] def fraction.setoid : setoid fraction :=
+{ r := λa b : fraction, num a * denom b = num b * denom a,
+ iseqv := /- proof -/ }
+
+lemma fraction.setoid_iff (a b : fraction) :
+ a ≈ b ↔ num a * denom b = num b * denom a :=
+by refl
+```
+
+Then define rationals based on the setoid:
+
+```lean
+def rat : Type := quotient fraction.setoid
+
+@[instance] def has_zero : has_zero rat :=
+{ zero := ⟦0⟧ }
+
+@[instance] def has_one : has_one rat :=
+{ one := ⟦1⟧ }
+
+@[instance] def has_add : has_add rat :=
+{ add :=
+ quotient.lift₂ (λa b : fraction, ⟦a + b ⟧)
+ by /- proof -/ }
+```
+
+Could also use a subtype of `fraction`, but then more complicated function definitions are needed.
+
+## Real numbers
+Some sequences seem to converge, but don't converge to a rational number. For example √2.
+The reals are rationals with a limit.
+
+A sequence of rational numbers is Cauchy if for a nonzero `x`, there is an `n ∈ Ν`, such that for all `m ≥ n`, we have `|a_n - a_m| < x`.
+
+```lean
+def is_cau_seq (f : Ν → Q) : Prop :=
+∀x > 0, ∃n, ∀m ≥ n, abs (f n - f m) < x
+
+def cau_seq : Type :=
+{f : N → Q // is_cau_seq f}
+
+-- two sequences represent same real number when their difference converges to zero
+@[instance] def cau_seq.setoid : setoid cau_seq :=
+{ r := λf g : cau_seq, ∀x > 0, ∃n, ∀m ≥ n, abs (seq_of f m - seq_of g m) < x,
+ iseqv := by /- proof -/ }
+
+def real : Type := quotient cau_seq.setoid
+namespace real
+
+@[instance] def has_zero : has_zero real :=
+{ zero := ⟦cau_seq.const 0⟧ }
+
+@[instance] def has_one : has_one real :=
+{ one := ⟦cau_seq.const 1⟧ }
+
+@[instance] def has_add : has_add real :=
+{ add := quotient.lift₂ (λ a h : cau_seq, ⟦a + b ⟧)
+ by /- proof -/ }
+end real
+```
+
diff --git a/content/logical-verification/_index.md b/content/logical-verification/_index.md
@@ -18,3 +18,5 @@ There is a [Git repository](https://github.com/blanchette/logical_verification_2
- [Hoare logic](hoare-logic/)
- [Denotational semantics](denotational-semantics/)
- [Logical foundations of mathematics](logical-foundations-of-mathematics/)
+- [Basic mathematical structures](basic-mathematical-structures/)
+- [Rational and real numbers](rational-and-real-numbers/)
