michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/algebra/binary): define right_commutative and left_commutative

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-09 10:54:28 -07:00
parent 8522fbec4b
commit d5176ebae5
3 changed files with 40 additions and 30 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

36
library/algebra/binary.lean
View file

@ -20,41 +20,45 @@ namespace binary
local notation a ⁻¹ := inv a
local notation 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 commutative [reducible] := ∀a b, a * b = b * a
definition associative [reducible] := ∀a b c, (a * b) * c = a * (b * c)
definition left_identity [reducible] := ∀a, 1 * a = a
definition right_identity [reducible] := ∀a, a * 1 = a
definition left_inverse [reducible] := ∀a, a⁻¹ * a = 1
definition right_inverse [reducible] := ∀a, a * a⁻¹ = 1
definition left_cancelative [reducible] := ∀a b c, a * b = a * c → b = c
definition right_cancelative [reducible] := ∀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
definition inv_op_cancel_left [reducible] := ∀a b, a⁻¹ * (a * b) = b
definition op_inv_cancel_left [reducible] := ∀a b, a * (a⁻¹ * b) = b
definition inv_op_cancel_right [reducible] := ∀a b, a * b⁻¹ * b = a
definition op_inv_cancel_right [reducible] := ∀a b, a * b * b⁻¹ = a
variable (op₂ : A → A → A)
local notation 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
definition left_distributive [reducible] := ∀a b c, a * (b + c) = a * b + a * c
definition right_distributive [reducible] := ∀a b c, (a + b) * c = a * c + b * c
definition right_commutative [reducible] {B : Type} (f : B → A → B) := ∀ b a₁ a₂, f (f b a₁) a₂ = f (f b a₂) a₁
definition left_commutative [reducible] {B : Type} (f : A → B → B) := ∀ a₁ a₂ b, f a₁ (f a₂ b) = f a₂ (f a₁ b)
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) :=
theorem left_comm : left_commutative f :=
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 :=
theorem right_comm : right_commutative f :=
take a b c, calc
(a*b)*c = a*(b*c) : H_assoc
... = a*(c*b) : H_comm

6
library/algebra/function.lean
View file

@ -14,6 +14,12 @@ variables {A : Type} {B : Type} {C : Type} {D : Type} {E : Type}
definition compose [reducible] (f : B → C) (g : A → B) : A → C :=
λx, f (g x)
definition compose_right [reducible] (f : B → B → B) (g : A → B) : B → A → B :=
λ b a, f b (g a)
definition compose_left [reducible] (f : B → B → B) (g : A → B) : A → B → B :=
λ a b, f (g a) b
definition id [reducible] (a : A) : A :=
a

28
library/data/list/perm.lean
View file

@ -467,27 +467,27 @@ assume p : l₁++(a::l₂) ~ l₃++(a::l₄),
section foldl
variables {f : B → A → B} {l₁ l₂ : list A}
variable rcomm : ∀ b a₁ a₂, f (f b a₁) a₂ = f (f b a₂) a₁
variable rcomm : right_commutative f
include rcomm
theorem foldl_eq_of_perm : l₁ ~ l₂ → ∀ a, foldl f a l₁ = foldl f a l₂ :=
theorem foldl_eq_of_perm : l₁ ~ l₂ → ∀ b, foldl f b l₁ = foldl f b l₂ :=
assume p, perm_induction_on p
(λ a, by rewrite *foldl_nil)
(λ x t₁ t₂ p r a, calc
foldl f a (x::t₁) = foldl f (f a x) t₁ : foldl_cons
... = foldl f (f a x) t₂ : r (f a x)
... = foldl f a (x::t₂) : foldl_cons)
(λ x y t₁ t₂ p r a, calc
foldl f a (y :: x :: t₁) = foldl f (f (f a y) x) t₁ : by rewrite foldl_cons
... = foldl f (f (f a x) y) t₁ : by rewrite rcomm
... = foldl f (f (f a x) y) t₂ : r (f (f a x) y)
... = foldl f a (x :: y :: t₂) : by rewrite foldl_cons)
(λ t₁ t₂ t₃ p₁ p₂ r₁ r₂ a, eq.trans (r₁ a) (r₂ a))
(λ b, by rewrite *foldl_nil)
(λ x t₁ t₂ p r b, calc
foldl f b (x::t₁) = foldl f (f b x) t₁ : foldl_cons
... = foldl f (f b x) t₂ : r (f b x)
... = foldl f b (x::t₂) : foldl_cons)
(λ x y t₁ t₂ p r b, calc
foldl f b (y :: x :: t₁) = foldl f (f (f b y) x) t₁ : by rewrite foldl_cons
... = foldl f (f (f b x) y) t₁ : by rewrite rcomm
... = foldl f (f (f b x) y) t₂ : r (f (f b x) y)
... = foldl f b (x :: y :: t₂) : by rewrite foldl_cons)
(λ t₁ t₂ t₃ p₁ p₂ r₁ r₂ b, eq.trans (r₁ b) (r₂ b))
end foldl
section foldr
variables {f : A → B → B} {l₁ l₂ : list A}
variable lcomm : ∀ a₁ a₂ b, f a₁ (f a₂ b) = f a₂ (f a₁ b)
variable lcomm : left_commutative f
include lcomm
theorem foldr_eq_of_perm : l₁ ~ l₂ → ∀ b, foldr f b l₁ = foldr f b l₂ :=