feat(library/binary, library/relation): introduce general properties for binary operations and relations

library/algebra/binary.lean

@@ -1,16 +1,45 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Leonardo de Moura
+/-
+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 logic.eq
 open eq.ops
 
 namespace binary
-  context
+  section
     variable {A : Type}
-    variable f : A → A → A
-    infixl `*` := f
-    definition commutative := ∀{a b}, a*b = b*a
-    definition associative := ∀{a b c}, (a*b)*c = a*(b*c)
+    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
@@ -21,15 +50,15 @@ namespace binary
     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}
+      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⁻¹
+        ...   = a*(c*b) : H_comm
+        ...   = (a*c)*b : H_assoc
   end
 
   context
@@ -40,8 +69,7 @@ namespace binary
     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⁻¹}
+              ... = a*((b*c)*d) : H_assoc
   end
 
-
 end binary

library/algebra/category/basic.lean

@@ -29,7 +29,7 @@ namespace category
   definition id [reducible] : Π {a : ob}, hom a a := rec (λ hom compose id assoc idr idl, id) C
   definition ID [reducible] (a : ob) : hom a a := id
 
-  infixr `∘`:60 := compose
+  infixr `∘` := compose
   infixl `⟶`:25 := hom -- input ⟶ using \--> (this is a different arrow than \-> (→))
 
   variables {h : hom c d} {g : hom b c} {f : hom a b} {i : hom a a}
@@ -61,7 +61,7 @@ namespace category
   definition Mk {ob} (C) : Category := Category.mk ob C
   definition MK (a b c d e f g) : Category := Category.mk a (category.mk b c d e f g)
 
-  definition objects [coercion] [reducible] (C : Category) : Type 
+  definition objects [coercion] [reducible] (C : Category) : Type
   := Category.rec (fun c s, c) C
 
   definition category_instance [instance] [coercion] [reducible] (C : Category) : category (objects C)

library/algebra/category/morphism.lean

@@ -54,7 +54,7 @@ namespace morphism
   calc
     g = g ∘ id : symm !id_right
      ... = g ∘ f ∘ g' : {symm Hr}
-     ... = (g ∘ f) ∘ g' : !assoc
+     ... = (g ∘ f) ∘ g' : sorry -- !assoc
      ... = id ∘ g' : {Hl}
      ... = g' : !id_left
 

library/algebra/relation.lean

@@ -1,22 +1,24 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Jeremy Avigad
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 
--- algebra.relation
--- ==============
+Module: algebra.relation
+Author: Jeremy Avigad
+
+General properties of relations, and classes for equivalence relations and congruences.
+-/
 
 import logic.prop
 
-
--- General properties of relations
--- -------------------------------
-
 namespace relation
 
-definition reflexive {T : Type} (R : T → T → Type) : Type := ∀x, R x x
-definition symmetric {T : Type} (R : T → T → Type) : Type := ∀⦃x y⦄, R x y → R y x
-definition transitive {T : Type} (R : T → T → Type) : Type := ∀⦃x y z⦄, R x y → R y z → R x z
+  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
 
 inductive is_reflexive [class] {T : Type} (R : T → T → Type) : Prop :=
 mk : reflexive R → is_reflexive R

library/general_notation.lean

@@ -35,7 +35,7 @@ reserve infix `≠`:50
 reserve infix `≈`:50
 reserve infix `∼`:50
 
-reserve infix `∘`:60      -- input with \comp
+reserve infixr `∘`:60      -- input with \comp
 reserve postfix `⁻¹`:100  --input with \sy or \-1 or \inv
 reserve infixl `⬝`:75
 reserve infixr `▸`:75