From 116e7ff82e88ed66cfb9b4918f5843257da9db5a Mon Sep 17 00:00:00 2001 From: Jakob von Raumer Date: Mon, 1 Dec 2014 14:49:27 -0500 Subject: [PATCH] feat(library/hott) port Jeremy's group file to use path equality --- library/hott/algebra/binary.lean | 75 ++++ library/hott/algebra/group.lean | 567 +++++++++++++++++++++++++++++ library/hott/algebra/relation.lean | 122 +++++++ 3 files changed, 764 insertions(+) create mode 100644 library/hott/algebra/binary.lean create mode 100644 library/hott/algebra/group.lean create mode 100644 library/hott/algebra/relation.lean diff --git a/library/hott/algebra/binary.lean b/library/hott/algebra/binary.lean new file mode 100644 index 0000000000..65fb6df596 --- /dev/null +++ b/library/hott/algebra/binary.lean @@ -0,0 +1,75 @@ +/- +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: algebra.binary +Authors: Leonardo de Moura, Jeremy Avigad + +General properties of binary operations. +-/ + +import hott.path +open path + +namespace path_binary + section + variable {A : Type} + variables (op₁ : A → A → A) (inv : A → A) (one : A) + + notation [local] a * b := op₁ a b + notation [local] a ⁻¹ := inv a + notation [local] 1 := one + + definition commutative := ∀a b, a*b ≈ b*a + definition associative := ∀a b c, (a*b)*c ≈ a*(b*c) + definition left_identity := ∀a, 1 * a ≈ a + definition right_identity := ∀a, a * 1 ≈ a + definition left_inverse := ∀a, a⁻¹ * a ≈ 1 + definition right_inverse := ∀a, a * a⁻¹ ≈ 1 + definition left_cancelative := ∀a b c, a * b ≈ a * c → b ≈ c + definition right_cancelative := ∀a b c, a * b ≈ c * b → a ≈ c + + definition inv_op_cancel_left := ∀a b, a⁻¹ * (a * b) ≈ b + definition op_inv_cancel_left := ∀a b, a * (a⁻¹ * b) ≈ b + definition inv_op_cancel_right := ∀a b, a * b⁻¹ * b ≈ a + definition op_inv_cancel_right := ∀a b, a * b * b⁻¹ ≈ a + + variable (op₂ : A → A → A) + + notation [local] a + b := op₂ a b + + definition left_distributive := ∀a b c, a * (b + c) ≈ a * b + a * c + definition right_distributive := ∀a b c, (a + b) * c ≈ a * c + b * c + end + + context + variable {A : Type} + variable {f : A → A → A} + variable H_comm : commutative f + variable H_assoc : associative f + infixl `*` := f + theorem left_comm : ∀a b c, a*(b*c) ≈ b*(a*c) := + take a b c, calc + a*(b*c) ≈ (a*b)*c : H_assoc + ... ≈ (b*a)*c : H_comm + ... ≈ b*(a*c) : H_assoc + + theorem right_comm : ∀a b c, (a*b)*c ≈ (a*c)*b := + take a b c, calc + (a*b)*c ≈ a*(b*c) : H_assoc + ... ≈ a*(c*b) : H_comm + ... ≈ (a*c)*b : H_assoc + end + + context + variable {A : Type} + variable {f : A → A → A} + variable H_assoc : associative f + infixl `*` := f + theorem assoc4helper (a b c d) : (a*b)*(c*d) ≈ a*((b*c)*d) := + calc + (a*b)*(c*d) ≈ a*(b*(c*d)) : H_assoc + ... ≈ a*((b*c)*d) : H_assoc + end + +end path_binary diff --git a/library/hott/algebra/group.lean b/library/hott/algebra/group.lean new file mode 100644 index 0000000000..50872c0a47 --- /dev/null +++ b/library/hott/algebra/group.lean @@ -0,0 +1,567 @@ +/- +Copyright (c) 2014 Jeremy Avigad. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: algebra.group +Authors: Jeremy Avigad, Leonardo de Moura + +Various multiplicative and additive structures. Partially modeled on Isabelle's library. +-/ + +import hott.path hott.trunc data.unit data.sigma data.prod +import hott.algebra.binary + +open path truncation path_binary -- note: ⁻¹ will be overloaded + +namespace path_algebra + +variable {A : Type} + +/- overloaded symbols -/ +structure has_mul [class] (A : Type) := +(mul : A → A → A) + +structure has_add [class] (A : Type) := +(add : A → A → A) + +structure has_one [class] (A : Type) := +(one : A) + +structure has_zero [class] (A : Type) := +(zero : A) + +structure has_inv [class] (A : Type) := +(inv : A → A) + +structure has_neg [class] (A : Type) := +(neg : A → A) + +infixl `*` := has_mul.mul +infixl `+` := has_add.add +postfix `⁻¹` := has_inv.inv +prefix `-` := has_neg.neg +notation 1 := !has_one.one +notation 0 := !has_zero.zero + + +/- semigroup -/ + +structure semigroup [class] (A : Type) extends has_mul A := +(carrier_hset : is_hset A) +(mul_assoc : ∀a b c, mul (mul a b) c ≈ mul a (mul b c)) + +theorem mul_assoc [s : semigroup A] (a b c : A) : a * b * c ≈ a * (b * c) := +!semigroup.mul_assoc + +structure comm_semigroup [class] (A : Type) extends semigroup A := +(mul_comm : ∀a b, mul a b ≈ mul b a) + +theorem mul_comm [s : comm_semigroup A] (a b : A) : a * b ≈ b * a := +!comm_semigroup.mul_comm + +theorem mul_left_comm [s : comm_semigroup A] (a b c : A) : a * (b * c) ≈ b * (a * c) := +path_binary.left_comm (@mul_comm A s) (@mul_assoc A s) a b c + +theorem mul_right_comm [s : comm_semigroup A] (a b c : A) : (a * b) * c ≈ (a * c) * b := +path_binary.right_comm (@mul_comm A s) (@mul_assoc A s) a b c + +structure left_cancel_semigroup [class] (A : Type) extends semigroup A := +(mul_left_cancel : ∀a b c, mul a b ≈ mul a c → b ≈ c) + +theorem mul_left_cancel [s : left_cancel_semigroup A] {a b c : A} : + a * b ≈ a * c → b ≈ c := +!left_cancel_semigroup.mul_left_cancel + +structure right_cancel_semigroup [class] (A : Type) extends semigroup A := +(mul_right_cancel : ∀a b c, mul a b ≈ mul c b → a ≈ c) + +theorem mul_right_cancel [s : right_cancel_semigroup A] {a b c : A} : + a * b ≈ c * b → a ≈ c := +!right_cancel_semigroup.mul_right_cancel + + +/- additive semigroup -/ + +structure add_semigroup [class] (A : Type) extends has_add A := +(add_assoc : ∀a b c, add (add a b) c ≈ add a (add b c)) + +theorem add_assoc [s : add_semigroup A] (a b c : A) : a + b + c ≈ a + (b + c) := +!add_semigroup.add_assoc + +structure add_comm_semigroup [class] (A : Type) extends add_semigroup A := +(add_comm : ∀a b, add a b ≈ add b a) + +theorem add_comm [s : add_comm_semigroup A] (a b : A) : a + b ≈ b + a := +!add_comm_semigroup.add_comm + +theorem add_left_comm [s : add_comm_semigroup A] (a b c : A) : + a + (b + c) ≈ b + (a + c) := +path_binary.left_comm (@add_comm A s) (@add_assoc A s) a b c + +theorem add_right_comm [s : add_comm_semigroup A] (a b c : A) : (a + b) + c ≈ (a + c) + b := +path_binary.right_comm (@add_comm A s) (@add_assoc A s) a b c + +structure add_left_cancel_semigroup [class] (A : Type) extends add_semigroup A := +(add_left_cancel : ∀a b c, add a b ≈ add a c → b ≈ c) + +theorem add_left_cancel [s : add_left_cancel_semigroup A] {a b c : A} : + a + b ≈ a + c → b ≈ c := +!add_left_cancel_semigroup.add_left_cancel + +structure add_right_cancel_semigroup [class] (A : Type) extends add_semigroup A := +(add_right_cancel : ∀a b c, add a b ≈ add c b → a ≈ c) + +theorem add_right_cancel [s : add_right_cancel_semigroup A] {a b c : A} : + a + b ≈ c + b → a ≈ c := +!add_right_cancel_semigroup.add_right_cancel + +/- monoid -/ + +structure monoid [class] (A : Type) extends semigroup A, has_one A := +(mul_left_id : ∀a, mul one a ≈ a) (mul_right_id : ∀a, mul a one ≈ a) + +theorem mul_left_id [s : monoid A] (a : A) : 1 * a ≈ a := !monoid.mul_left_id + +theorem mul_right_id [s : monoid A] (a : A) : a * 1 ≈ a := !monoid.mul_right_id + +structure comm_monoid [class] (A : Type) extends monoid A, comm_semigroup A + + +/- additive monoid -/ + +structure add_monoid [class] (A : Type) extends add_semigroup A, has_zero A := +(add_left_id : ∀a, add zero a ≈ a) (add_right_id : ∀a, add a zero ≈ a) + +theorem add_left_id [s : add_monoid A] (a : A) : 0 + a ≈ a := !add_monoid.add_left_id + +theorem add_right_id [s : add_monoid A] (a : A) : a + 0 ≈ a := !add_monoid.add_right_id + +structure add_comm_monoid [class] (A : Type) extends add_monoid A, add_comm_semigroup A + + + +/- group -/ + +structure group [class] (A : Type) extends monoid A, has_inv A := +(mul_left_inv : ∀a, mul (inv a) a ≈ one) + +-- Note: with more work, we could derive the axiom mul_left_id + +section group + + variable [s : group A] + include s + + theorem mul_left_inv (a : A) : a⁻¹ * a ≈ 1 := !group.mul_left_inv + + theorem inv_mul_cancel_left (a b : A) : a⁻¹ * (a * b) ≈ b := + calc + a⁻¹ * (a * b) ≈ a⁻¹ * a * b : mul_assoc + ... ≈ 1 * b : mul_left_inv + ... ≈ b : mul_left_id + + theorem inv_mul_cancel_right (a b : A) : a * b⁻¹ * b ≈ a := + calc + a * b⁻¹ * b ≈ a * (b⁻¹ * b) : mul_assoc + ... ≈ a * 1 : mul_left_inv + ... ≈ a : mul_right_id + + theorem inv_unique {a b : A} (H : a * b ≈ 1) : a⁻¹ ≈ b := + calc + a⁻¹ ≈ a⁻¹ * 1 : mul_right_id + ... ≈ a⁻¹ * (a * b) : H + ... ≈ b : inv_mul_cancel_left + + theorem inv_one : 1⁻¹ ≈ 1 := inv_unique (mul_left_id 1) + + theorem inv_inv (a : A) : (a⁻¹)⁻¹ ≈ a := inv_unique (mul_left_inv a) + + theorem inv_inj {a b : A} (H : a⁻¹ ≈ b⁻¹) : a ≈ b := + calc + a ≈ (a⁻¹)⁻¹ : inv_inv + ... ≈ b : inv_unique (H⁻¹ ▹ (mul_left_inv _)) + + --theorem inv_eq_inv_iff_eq (a b : A) : a⁻¹ ≈ b⁻¹ ↔ a ≈ b := + --iff.intro (assume H, inv_inj H) (assume H, congr_arg _ H) + + --theorem inv_eq_one_iff_eq_one (a b : A) : a⁻¹ ≈ 1 ↔ a ≈ 1 := + --inv_one ▹ !inv_eq_inv_iff_eq + + theorem eq_inv_imp_eq_inv {a b : A} (H : a ≈ b⁻¹) : b ≈ a⁻¹ := + H⁻¹ ▹ (inv_inv b)⁻¹ + + --theorem eq_inv_iff_eq_inv (a b : A) : a ≈ b⁻¹ ↔ b ≈ a⁻¹ := + --iff.intro !eq_inv_imp_eq_inv !eq_inv_imp_eq_inv + + theorem mul_right_inv (a : A) : a * a⁻¹ ≈ 1 := + calc + a * a⁻¹ ≈ (a⁻¹)⁻¹ * a⁻¹ : inv_inv + ... ≈ 1 : mul_left_inv + + theorem mul_inv_cancel_left (a b : A) : a * (a⁻¹ * b) ≈ b := + calc + a * (a⁻¹ * b) ≈ a * a⁻¹ * b : mul_assoc + ... ≈ 1 * b : mul_right_inv + ... ≈ b : mul_left_id + + theorem mul_inv_cancel_right (a b : A) : a * b * b⁻¹ ≈ a := + calc + a * b * b⁻¹ ≈ a * (b * b⁻¹) : mul_assoc + ... ≈ a * 1 : mul_right_inv + ... ≈ a : mul_right_id + + theorem inv_mul (a b : A) : (a * b)⁻¹ ≈ b⁻¹ * a⁻¹ := + inv_unique + (calc + a * b * (b⁻¹ * a⁻¹) ≈ a * (b * (b⁻¹ * a⁻¹)) : mul_assoc + ... ≈ a * a⁻¹ : mul_inv_cancel_left + ... ≈ 1 : mul_right_inv) + + theorem mul_inv_eq_one_imp_eq {a b : A} (H : a * b⁻¹ ≈ 1) : a ≈ b := + calc + a ≈ a * b⁻¹ * b : inv_mul_cancel_right + ... ≈ 1 * b : H + ... ≈ b : mul_left_id + + -- TODO: better names for the next eight theorems? (Also for additive ones.) + theorem mul_eq_imp_eq_mul_inv {a b c : A} (H : a * b ≈ c) : a ≈ c * b⁻¹ := + H ▹ !mul_inv_cancel_right⁻¹ + + theorem mul_eq_imp_eq_inv_mul {a b c : A} (H : a * b ≈ c) : b ≈ a⁻¹ * c := + H ▹ !inv_mul_cancel_left⁻¹ + + theorem eq_mul_imp_inv_mul_eq {a b c : A} (H : a ≈ b * c) : b⁻¹ * a ≈ c := + H⁻¹ ▹ !inv_mul_cancel_left + + theorem eq_mul_imp_mul_inv_eq {a b c : A} (H : a ≈ b * c) : a * c⁻¹ ≈ b := + H⁻¹ ▹ !mul_inv_cancel_right + + theorem mul_inv_eq_imp_eq_mul {a b c : A} (H : a * b⁻¹ ≈ c) : a ≈ c * b := + !inv_inv ▹ (mul_eq_imp_eq_mul_inv H) + + theorem inv_mul_eq_imp_eq_mul {a b c : A} (H : a⁻¹ * b ≈ c) : b ≈ a * c := + !inv_inv ▹ (mul_eq_imp_eq_inv_mul H) + + theorem eq_inv_mul_imp_mul_eq {a b c : A} (H : a ≈ b⁻¹ * c) : b * a ≈ c := + !inv_inv ▹ (eq_mul_imp_inv_mul_eq H) + + theorem eq_mul_inv_imp_mul_eq {a b c : A} (H : a ≈ b * c⁻¹) : a * c ≈ b := + !inv_inv ▹ (eq_mul_imp_mul_inv_eq H) + + --theorem mul_eq_iff_eq_inv_mul (a b c : A) : a * b ≈ c ↔ b ≈ a⁻¹ * c := + --iff.intro mul_eq_imp_eq_inv_mul eq_inv_mul_imp_mul_eq + + --theorem mul_eq_iff_eq_mul_inv (a b c : A) : a * b ≈ c ↔ a ≈ c * b⁻¹ := + --iff.intro mul_eq_imp_eq_mul_inv eq_mul_inv_imp_mul_eq + + definition group.to_left_cancel_semigroup [instance] : left_cancel_semigroup A := + left_cancel_semigroup.mk (@group.mul A s) (@group.carrier_hset A s) (@group.mul_assoc A s) + (take a b c, + assume H : a * b ≈ a * c, + calc + b ≈ a⁻¹ * (a * b) : inv_mul_cancel_left + ... ≈ a⁻¹ * (a * c) : H + ... ≈ c : inv_mul_cancel_left) + + definition group.to_right_cancel_semigroup [instance] : right_cancel_semigroup A := + right_cancel_semigroup.mk (@group.mul A s) (@group.carrier_hset A s) (@group.mul_assoc A s) + (take a b c, + assume H : a * b ≈ c * b, + calc + a ≈ (a * b) * b⁻¹ : mul_inv_cancel_right + ... ≈ (c * b) * b⁻¹ : H + ... ≈ c : mul_inv_cancel_right) + +end group + +structure comm_group [class] (A : Type) extends group A, comm_monoid A + + +/- additive group -/ + +structure add_group [class] (A : Type) extends add_monoid A, has_neg A := +(add_left_inv : ∀a, add (neg a) a ≈ zero) + +section add_group + + variables [s : add_group A] + include s + + theorem add_left_inv (a : A) : -a + a ≈ 0 := !add_group.add_left_inv + + theorem neg_add_cancel_left (a b : A) : -a + (a + b) ≈ b := + calc + -a + (a + b) ≈ -a + a + b : add_assoc + ... ≈ 0 + b : add_left_inv + ... ≈ b : add_left_id + + theorem neg_add_cancel_right (a b : A) : a + -b + b ≈ a := + calc + a + -b + b ≈ a + (-b + b) : add_assoc + ... ≈ a + 0 : add_left_inv + ... ≈ a : add_right_id + + theorem neg_unique {a b : A} (H : a + b ≈ 0) : -a ≈ b := + calc + -a ≈ -a + 0 : add_right_id + ... ≈ -a + (a + b) : H + ... ≈ b : neg_add_cancel_left + + theorem neg_zero : -0 ≈ 0 := neg_unique (add_left_id 0) + + theorem neg_neg (a : A) : -(-a) ≈ a := neg_unique (add_left_inv a) + + theorem neg_inj {a b : A} (H : -a ≈ -b) : a ≈ b := + calc + a ≈ -(-a) : neg_neg + ... ≈ b : neg_unique (H⁻¹ ▹ (add_left_inv _)) + + --theorem neg_eq_neg_iff_eq (a b : A) : -a ≈ -b ↔ a ≈ b := + --iff.intro (assume H, neg_inj H) (assume H, congr_arg _ H) + + --theorem neg_eq_zero_iff_eq_zero (a b : A) : -a ≈ 0 ↔ a ≈ 0 := + --neg_zero ▹ !neg_eq_neg_iff_eq + + theorem eq_neg_imp_eq_neg {a b : A} (H : a ≈ -b) : b ≈ -a := + H⁻¹ ▹ (neg_neg b)⁻¹ + + --theorem eq_neg_iff_eq_neg (a b : A) : a ≈ -b ↔ b ≈ -a := + --iff.intro !eq_neg_imp_eq_neg !eq_neg_imp_eq_neg + + theorem add_right_inv (a : A) : a + -a ≈ 0 := + calc + a + -a ≈ -(-a) + -a : neg_neg + ... ≈ 0 : add_left_inv + + theorem add_neg_cancel_left (a b : A) : a + (-a + b) ≈ b := + calc + a + (-a + b) ≈ a + -a + b : add_assoc + ... ≈ 0 + b : add_right_inv + ... ≈ b : add_left_id + + theorem add_neg_cancel_right (a b : A) : a + b + -b ≈ a := + calc + a + b + -b ≈ a + (b + -b) : add_assoc + ... ≈ a + 0 : add_right_inv + ... ≈ a : add_right_id + + theorem neg_add (a b : A) : -(a + b) ≈ -b + -a := + neg_unique + (calc + a + b + (-b + -a) ≈ a + (b + (-b + -a)) : add_assoc + ... ≈ a + -a : add_neg_cancel_left + ... ≈ 0 : add_right_inv) + + theorem add_eq_imp_eq_add_neg {a b c : A} (H : a + b ≈ c) : a ≈ c + -b := + H ▹ !add_neg_cancel_right⁻¹ + + theorem add_eq_imp_eq_neg_add {a b c : A} (H : a + b ≈ c) : b ≈ -a + c := + H ▹ !neg_add_cancel_left⁻¹ + + theorem eq_add_imp_neg_add_eq {a b c : A} (H : a ≈ b + c) : -b + a ≈ c := + H⁻¹ ▹ !neg_add_cancel_left + + theorem eq_add_imp_add_neg_eq {a b c : A} (H : a ≈ b + c) : a + -c ≈ b := + H⁻¹ ▹ !add_neg_cancel_right + + theorem add_neg_eq_imp_eq_add {a b c : A} (H : a + -b ≈ c) : a ≈ c + b := + !neg_neg ▹ (add_eq_imp_eq_add_neg H) + + theorem neg_add_eq_imp_eq_add {a b c : A} (H : -a + b ≈ c) : b ≈ a + c := + !neg_neg ▹ (add_eq_imp_eq_neg_add H) + + theorem eq_neg_add_imp_add_eq {a b c : A} (H : a ≈ -b + c) : b + a ≈ c := + !neg_neg ▹ (eq_add_imp_neg_add_eq H) + + theorem eq_add_neg_imp_add_eq {a b c : A} (H : a ≈ b + -c) : a + c ≈ b := + !neg_neg ▹ (eq_add_imp_add_neg_eq H) + + --theorem add_eq_iff_eq_neg_add (a b c : A) : a + b ≈ c ↔ b ≈ -a + c := + --iff.intro add_eq_imp_eq_neg_add eq_neg_add_imp_add_eq + + --theorem add_eq_iff_eq_add_neg (a b c : A) : a + b ≈ c ↔ a ≈ c + -b := + --iff.intro add_eq_imp_eq_add_neg eq_add_neg_imp_add_eq + + definition add_group.to_left_cancel_semigroup [instance] : + add_left_cancel_semigroup A := + add_left_cancel_semigroup.mk (@add_group.add A s) (@add_group.add_assoc A s) + (take a b c, + assume H : a + b ≈ a + c, + calc + b ≈ -a + (a + b) : neg_add_cancel_left + ... ≈ -a + (a + c) : H + ... ≈ c : neg_add_cancel_left) + + definition add_group.to_add_right_cancel_semigroup [instance] : + add_right_cancel_semigroup A := + add_right_cancel_semigroup.mk (@add_group.add A s) (@add_group.add_assoc A s) + (take a b c, + assume H : a + b ≈ c + b, + calc + a ≈ (a + b) + -b : add_neg_cancel_right + ... ≈ (c + b) + -b : H + ... ≈ c : add_neg_cancel_right) + + /- minus -/ + + -- TODO: derive corresponding facts for div in a field + definition minus (a b : A) : A := a + -b + + infix `-` := minus + + theorem minus_self (a : A) : a - a ≈ 0 := !add_right_inv + + theorem minus_add_cancel (a b : A) : a - b + b ≈ a := !neg_add_cancel_right + + theorem add_minus_cancel (a b : A) : a + b - b ≈ a := !add_neg_cancel_right + + theorem minus_eq_zero_imp_eq {a b : A} (H : a - b ≈ 0) : a ≈ b := + calc + a ≈ (a - b) + b : minus_add_cancel + ... ≈ 0 + b : H + ... ≈ b : add_left_id + + --theorem eq_iff_minus_eq_zero (a b : A) : a ≈ b ↔ a - b ≈ 0 := + --iff.intro (assume H, H ▹ !minus_self) (assume H, minus_eq_zero_imp_eq H) + + theorem zero_minus (a : A) : 0 - a ≈ -a := !add_left_id + + theorem minus_zero (a : A) : a - 0 ≈ a := (neg_zero⁻¹) ▹ !add_right_id + + theorem minus_neg_eq_add (a b : A) : a - (-b) ≈ a + b := !neg_neg⁻¹ ▹ idp + + theorem neg_minus_eq (a b : A) : -(a - b) ≈ b - a := + neg_unique + (calc + a - b + (b - a) ≈ a - b + b - a : add_assoc + ... ≈ a - a : minus_add_cancel + ... ≈ 0 : minus_self) + + theorem add_minus_eq (a b c : A) : a + (b - c) ≈ a + b - c := !add_assoc⁻¹ + + theorem minus_add_eq_minus_swap (a b c : A) : a - (b + c) ≈ a - c - b := + calc + a - (b + c) ≈ a + (-c - b) : neg_add + ... ≈ a - c - b : add_assoc + + --theorem minus_eq_iff_eq_add (a b c : A) : a - b ≈ c ↔ a ≈ c + b := + --iff.intro (assume H, add_neg_eq_imp_eq_add H) (assume H, eq_add_imp_add_neg_eq H) + + --theorem eq_minus_iff_add_eq (a b c : A) : a ≈ b - c ↔ a + c ≈ b := + --iff.intro (assume H, eq_add_neg_imp_add_eq H) (assume H, add_eq_imp_eq_add_neg H) + + --theorem minus_eq_minus_iff {a b c d : A} (H : a - b ≈ c - d) : a ≈ b ↔ c ≈ d := + --calc + -- a ≈ b ↔ a - b ≈ 0 : eq_iff_minus_eq_zero + -- ... ↔ c - d ≈ 0 : H ▹ !iff.refl + -- ... ↔ c ≈ d : iff.symm (eq_iff_minus_eq_zero c d) + +end add_group + +structure add_comm_group [class] (A : Type) extends add_group A, add_comm_monoid A + +section add_comm_group + +variable [s : add_comm_group A] +include s + + theorem minus_add_eq (a b c : A) : a - (b + c) ≈ a - b - c := + !add_comm ▹ !minus_add_eq_minus_swap + + theorem neg_add_eq_minus (a b : A) : -a + b ≈ b - a := !add_comm + + theorem neg_add_distrib (a b : A) : -(a + b) ≈ -a + -b := !add_comm ▹ !neg_add + + theorem minus_add_right_comm (a b c : A) : a - b + c ≈ a + c - b := !add_right_comm + + theorem minus_minus_eq (a b c : A) : a - b - c ≈ a - (b + c) := + calc + a - b - c ≈ a + (-b + -c) : add_assoc + ... ≈ a + -(b + c) : neg_add_distrib + ... ≈ a - (b + c) : idp + + theorem add_minus_cancel_left (a b c : A) : (c + a) - (c + b) ≈ a - b := + calc + (c + a) - (c + b) ≈ c + a - c - b : minus_add_eq + ... ≈ a + c - c - b : add_comm a c + ... ≈ a - b : add_minus_cancel + + +end add_comm_group + + +/- bundled structures -/ + +structure Semigroup := +(carrier : Type) (struct : semigroup carrier) + +coercion Semigroup.carrier +instance Semigroup.struct + +structure CommSemigroup := +(carrier : Type) (struct : comm_semigroup carrier) + +coercion CommSemigroup.carrier +instance CommSemigroup.struct + +structure Monoid := +(carrier : Type) (struct : monoid carrier) + +coercion Monoid.carrier +instance Monoid.struct + +structure CommMonoid := +(carrier : Type) (struct : comm_monoid carrier) + +coercion CommMonoid.carrier +instance CommMonoid.struct + +structure Group := +(carrier : Type) (struct : group carrier) + +coercion Group.carrier +instance Group.struct + +structure CommGroup := +(carrier : Type) (struct : comm_group carrier) + +coercion CommGroup.carrier +instance CommGroup.struct + +structure AddSemigroup := +(carrier : Type) (struct : add_semigroup carrier) + +coercion AddSemigroup.carrier +instance AddSemigroup.struct + +structure AddCommSemigroup := +(carrier : Type) (struct : add_comm_semigroup carrier) + +coercion AddCommSemigroup.carrier +instance AddCommSemigroup.struct + +structure AddMonoid := +(carrier : Type) (struct : add_monoid carrier) + +coercion AddMonoid.carrier +instance AddMonoid.struct + +structure AddCommMonoid := +(carrier : Type) (struct : add_comm_monoid carrier) + +coercion AddCommMonoid.carrier +instance AddCommMonoid.struct + +structure AddGroup := +(carrier : Type) (struct : add_group carrier) + +coercion AddGroup.carrier +instance AddGroup.struct + +structure AddCommGroup := +(carrier : Type) (struct : add_comm_group carrier) + +coercion AddCommGroup.carrier +instance AddCommGroup.struct + +end path_algebra diff --git a/library/hott/algebra/relation.lean b/library/hott/algebra/relation.lean new file mode 100644 index 0000000000..ead65fef15 --- /dev/null +++ b/library/hott/algebra/relation.lean @@ -0,0 +1,122 @@ +/- +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: algebra.relation +Author: Jeremy Avigad + +General properties of relations, and classes for equivalence relations and congruences. +-/ + +namespace relation + +/- properties of binary relations -/ + +section + variables {T : Type} (R : T → T → Type) + + definition reflexive : Type := Πx, R x x + definition symmetric : Type := Π⦃x y⦄, R x y → R y x + definition transitive : Type := Π⦃x y z⦄, R x y → R y z → R x z +end + + +/- classes for equivalence relations -/ + +structure is_reflexive [class] {T : Type} (R : T → T → Type) := (refl : reflexive R) +structure is_symmetric [class] {T : Type} (R : T → T → Type) := (symm : symmetric R) +structure is_transitive [class] {T : Type} (R : T → T → Type) := (trans : transitive R) + +structure is_equivalence [class] {T : Type} (R : T → T → Type) +extends is_reflexive R, is_symmetric R, is_transitive R + +-- partial equivalence relation +structure is_PER {T : Type} (R : T → T → Type) extends is_symmetric R, is_transitive R + +-- Generic notation. For example, is_refl R is the reflexivity of R, if that can be +-- inferred by type class inference +section + variables {T : Type} (R : T → T → Type) + definition rel_refl [C : is_reflexive R] := is_reflexive.refl R + definition rel_symm [C : is_symmetric R] := is_symmetric.symm R + definition rel_trans [C : is_transitive R] := is_transitive.trans R +end + + +/- classes for unary and binary congruences with respect to arbitrary relations -/ + +structure is_congruence [class] + {T1 : Type} (R1 : T1 → T1 → Type) + {T2 : Type} (R2 : T2 → T2 → Type) + (f : T1 → T2) := +(congr : Π{x y}, R1 x y → R2 (f x) (f y)) + +structure is_congruence2 [class] + {T1 : Type} (R1 : T1 → T1 → Type) + {T2 : Type} (R2 : T2 → T2 → Type) + {T3 : Type} (R3 : T3 → T3 → Type) + (f : T1 → T2 → T3) := +(congr2 : Π{x1 y1 : T1} {x2 y2 : T2}, R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2)) + +namespace is_congruence + + -- makes the type class explicit + definition app {T1 : Type} {R1 : T1 → T1 → Type} {T2 : Type} {R2 : T2 → T2 → Type} + {f : T1 → T2} (C : is_congruence R1 R2 f) ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) := + is_congruence.rec (λu, u) C x y + + definition app2 {T1 : Type} {R1 : T1 → T1 → Type} {T2 : Type} {R2 : T2 → T2 → Type} + {T3 : Type} {R3 : T3 → T3 → Type} + {f : T1 → T2 → T3} (C : is_congruence2 R1 R2 R3 f) ⦃x1 y1 : T1⦄ ⦃x2 y2 : T2⦄ : + R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2) := + is_congruence2.rec (λu, u) C x1 y1 x2 y2 + + /- tools to build instances -/ + + theorem compose + {T2 : Type} {R2 : T2 → T2 → Type} + {T3 : Type} {R3 : T3 → T3 → Type} + {g : T2 → T3} (C2 : is_congruence R2 R3 g) + ⦃T1 : Type⦄ {R1 : T1 → T1 → Type} + {f : T1 → T2} (C1 : is_congruence R1 R2 f) : + is_congruence R1 R3 (λx, g (f x)) := + is_congruence.mk (λx1 x2 H, app C2 (app C1 H)) + + theorem compose21 + {T2 : Type} {R2 : T2 → T2 → Type} + {T3 : Type} {R3 : T3 → T3 → Type} + {T4 : Type} {R4 : T4 → T4 → Type} + {g : T2 → T3 → T4} (C3 : is_congruence2 R2 R3 R4 g) + ⦃T1 : Type⦄ {R1 : T1 → T1 → Type} + {f1 : T1 → T2} (C1 : is_congruence R1 R2 f1) + {f2 : T1 → T3} (C2 : is_congruence R1 R3 f2) : + is_congruence R1 R4 (λx, g (f1 x) (f2 x)) := + is_congruence.mk (λx1 x2 H, app2 C3 (app C1 H) (app C2 H)) + + theorem const {T2 : Type} (R2 : T2 → T2 → Type) (H : relation.reflexive R2) + ⦃T1 : Type⦄ (R1 : T1 → T1 → Prop) (c : T2) : + is_congruence R1 R2 (λu : T1, c) := + is_congruence.mk (λx y H1, H c) + +end is_congruence + +theorem congruence_const [instance] {T2 : Type} (R2 : T2 → T2 → Type) + [C : is_reflexive R2] ⦃T1 : Type⦄ (R1 : T1 → T1 → Prop) (c : T2) : + is_congruence R1 R2 (λu : T1, c) := +is_congruence.const R2 (is_reflexive.refl R2) R1 c + +theorem congruence_trivial [instance] {T : Type} (R : T → T → Type) : + is_congruence R R (λu, u) := +is_congruence.mk (λx y H, H) + + +/- relations that can be coerced to functions / implications-/ + +structure mp_like [class] (R : Type → Type → Type) := +(app : Π{a b : Type}, R a b → (a → b)) + +definition rel_mp (R : Type → Type → Type) [C : mp_like R] {a b : Type} (H : R a b) := +mp_like.app H + + +end relation