-- * Case study -- Let's formalize some stuff about presenting groups (or monoids) by -- generators and relations open import Logic hiding (left; right) open import Nat -- ---------------------------------------------------------------------- -- * Words -- Let X = {a, b, c} be a set of _generators_. -- -- Words in X are things like ε, a • b, a • (b • a), (c • a) • (ε • b) -- Type \bub = •, \cib = ●, \cdot = ·, \buw = ◦, \ciw = ○ data Word (X : Set) : Set where gen : X -> Word X ε : Word X _•_ : Word X -> Word X -> Word X infixr 7 _•_ module Example1 where data Gen : Set where a : Gen b : Gen c : Gen example-word : Word Gen example-word = (gen a • gen b) • (ε • gen a) -- (a • b) • (ε • a) -- Example of generators and relations. -- -- The symmetry group of an equilateral triangle (see lecture notes) -- ---------------------------------------------------------------------- -- * Relations -- A relation is just a pair of words. data Relation (X : Set) : Set where _===_ : Word X -> Word X -> Relation X infix 6 _===_ module Example2 where open Example1 my-relation : Relation Gen my-relation = (gen a • gen b) • (ε • gen a) === gen a • (gen b • gen a) my-relation2 : Relation Gen my-relation2 = gen a • gen b === gen b • gen a -- ---------------------------------------------------------------------- -- * Context -- Definition: a context is a set of relations. -- -- If X is a set (of generators), then we want Context X to be the -- set of sets of relations over X. -- -- In math notation, Context X = P(Relation X), where "P" denotes the powerset. Context : Set -> Set₁ Context X = Relation X -> Set -- The empty context. ∅ : ∀ {X} -> Context X ∅ R = False -- Notation: it is convenient to write R ∈ Γ if the relation R is in Γ. _∈_ : ∀ {X} -> Relation X -> Context X -> Set R ∈ Γ = Γ R infix 5 _∈_ -- ---------------------------------------------------------------------- -- * Reasoning about relations infix 5 _⊢_ -- When does a relation R follow from a set of relations Γ? -- -- We will write Γ ⊢ R to mean "the relations in Γ imply the relation R". data _⊢_ {X : Set} (Γ : Context X) : Relation X -> Set where -- What's assumed is true. axiom : ∀ {R} -> R ∈ Γ -> Γ ⊢ R -- === is an equivalence relation. refl : ∀ {w} -> Γ ⊢ w === w symm : ∀ {w v} -> Γ ⊢ w === v -> Γ ⊢ v === w trans : ∀ {w v u} -> Γ ⊢ w === v -> Γ ⊢ v === u -> Γ ⊢ w === u -- === is a congruence. cong : ∀ {w w' v v'} -> Γ ⊢ w === w' -> Γ ⊢ v === v' -> Γ ⊢ w • v === w' • v' -- The laws of monoids. assoc : ∀ {w v u} -> Γ ⊢ (w • v) • u === w • (v • u) left-unit : ∀ {w} -> Γ ⊢ ε • w === w right-unit : ∀ {w} -> Γ ⊢ w • ε === w -- ---------------------------------------------------------------------- -- * Some syntactic sugar for reasoning in monoids open import Equality as Eq using (_==_) infix 2 equational_ infixl 1 by-equals infixl 4 _reversed infixl 3 left_ infixl 3 right_ equational_ : ∀ {X : Set} {Γ : Context X} -> (w : Word X) -> Γ ⊢ w === w equational_ w = refl by-equals : ∀ {X : Set} {Γ : Context X} {w v : Word X} -> Γ ⊢ w === v -> (u : Word X) -> Γ ⊢ v === u -> Γ ⊢ w === u by-equals E u reason = trans E reason syntax by-equals E u reason = E by reason equals u _reversed : ∀ {X : Set} {Γ : Context X} {w v : Word X} -> Γ ⊢ w === v -> Γ ⊢ v === w _reversed = symm left_ : ∀ {X : Set} {Γ : Context X} {w v u : Word X} -> Γ ⊢ w === v -> Γ ⊢ w • u === v • u left_ E = cong E refl right_ : ∀ {X : Set} {Γ : Context X} {w v u : Word X} -> Γ ⊢ w === v -> Γ ⊢ u • w === u • v right_ E = cong refl E -- A version of reflexivity that can be used as an introduction rule. refl' : ∀ {X : Set} {Γ : Context X} {w v : Word X} -> w == v -> Γ ⊢ w === v refl' Eq.refl = refl -- A synonym for refl, so that we can say "by definition". definition : ∀ {X : Set} {Γ : Context X} {w} -> Γ ⊢ w === w definition = refl -- ---------------------------------------------------------------------- -- * Lemmas about monoids -- For convenience, define powers of words. We'll write w ^ n -- for w raised to the nth power. _^_ : ∀ {Z} -> Word Z -> ℕ -> Word Z w ^ 0 = ε w ^ succ n = w • (w ^ n) infix 8 _^_ module Example3 where open Example1 my-power : Word Gen my-power = gen a ^ 10 module Monoid-Lemmas {X : Set} {Γ : Context X} where -- Left units are unique. left-unit-unique : {w : Word X} -> (∀ v -> Γ ⊢ w • v === v) -> Γ ⊢ w === ε left-unit-unique {w} hyp = trans claim2 claim1 where claim1 : Γ ⊢ w • ε === ε claim1 = hyp ε claim2 : Γ ⊢ w === w • ε claim2 = symm right-unit -- Right units are unique. right-unit-unique : {w : Word X} -> (∀ v -> Γ ⊢ v • w === v) -> Γ ⊢ w === ε right-unit-unique {w} hyp = equational w by symm left-unit equals ε • w by hyp ε equals ε -- Congruence for powers. cong-power : {w v : Word X} (n : ℕ) -> Γ ⊢ w === v -> Γ ⊢ w ^ n === v ^ n cong-power zero hyp = refl cong-power (succ n) hyp = cong hyp (cong-power n hyp) -- ---------------------------------------------------------------------- -- * A tactic for associativity -- Strategy: to check if two words are equal up to associativity and -- unit laws, convert each word to a list of generators, and then use -- "refl" to check if the lists are equal. data List (A : Set) : Set where nil : List A cons : A -> List A -> List A _++_ : {A : Set} -> List A -> List A -> List A nil ++ ys = ys cons x xs ++ ys = cons x (xs ++ ys) module Tactic-Assoc {X : Set} {Γ : Context X} where list-of-word : Word X -> List X list-of-word (gen x) = cons x nil list-of-word ε = nil list-of-word (w • v) = list-of-word w ++ list-of-word v word-of-list : List X -> Word X word-of-list nil = ε word-of-list (cons x xs) = gen x • word-of-list xs lemma-concat : ∀ (xs ys : List X) -> Γ ⊢ word-of-list (xs ++ ys) === word-of-list xs • word-of-list ys lemma-concat nil ys = symm left-unit lemma-concat (cons x xs) ys = equational gen x • word-of-list (xs ++ ys) by right (lemma-concat xs ys) equals gen x • (word-of-list xs • word-of-list ys) by symm assoc equals (gen x • word-of-list xs) • word-of-list ys -- Every word w is relationally equal to its canonical form, defined -- as word-of-list (list-of-word w). lemma-list-of-word : (w : Word X) -> Γ ⊢ word-of-list (list-of-word w) === w lemma-list-of-word (gen x) = right-unit lemma-list-of-word ε = refl lemma-list-of-word (w • v) = equational word-of-list (list-of-word (w • v)) by definition equals word-of-list (list-of-word w ++ list-of-word v) by lemma-concat (list-of-word w) (list-of-word v) equals word-of-list (list-of-word w) • word-of-list (list-of-word v) by cong (lemma-list-of-word w) (lemma-list-of-word v) equals w • v general-assoc : {w v : Word X} -> list-of-word w == list-of-word v -> Γ ⊢ w === v general-assoc {w} {v} hyp = equational w by symm (lemma-list-of-word w) equals word-of-list (list-of-word w) by refl' (Eq.context word-of-list hyp) equals word-of-list (list-of-word v) by lemma-list-of-word v equals v module Example4 where open Example1 open Tactic-Assoc x : list-of-word {Gen} {∅} example-word == cons a (cons b (cons a nil)) x = Eq.refl example-word2 : Word Gen example-word2 = gen a • (ε • (gen b • gen a)) lemma-example : ∅ ⊢ example-word === example-word2 lemma-example = equational (gen a • gen b) • (ε • gen a) by general-assoc Eq.refl equals gen a • (ε • (gen b • gen a)) -- ---------------------------------------------------------------------- -- * Group Grouplike : {X : Set} -> (Γ : Context X) -> Set Grouplike {X} Γ = ∀ (x : X) -> ∃ λ (w : Word X) -> Γ ⊢ w • gen x === ε module Group-Lemmas (X : Set) (Γ : Context X) (group-like : Grouplike Γ) where open Tactic-Assoc infix 8 _⁻¹ _⁻¹ : Word X -> Word X (gen x) ⁻¹ = fst (group-like x) ε ⁻¹ = ε (u • v) ⁻¹ = v ⁻¹ • u ⁻¹ left-inverse : {g : Word X} -> Γ ⊢ g ⁻¹ • g === ε left-inverse {gen x} = snd (group-like x) left-inverse {ε} = left-unit left-inverse {g • h} = equational (h ⁻¹ • g ⁻¹) • (g • h) by assoc equals h ⁻¹ • (g ⁻¹ • (g • h)) by right (symm assoc) equals h ⁻¹ • ((g ⁻¹ • g) • h) by right (left left-inverse) equals h ⁻¹ • (ε • h) by right left-unit equals h ⁻¹ • h by left-inverse equals ε