From d5176ebae5f257ca7b4b9fe7cacb366ca5f11a63 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 9 Apr 2015 10:54:28 -0700 Subject: [PATCH] refactor(library/algebra/binary): define right_commutative and left_commutative --- library/algebra/binary.lean | 36 +++++++++++++++++++---------------- library/algebra/function.lean | 6 ++++++ library/data/list/perm.lean | 28 +++++++++++++-------------- 3 files changed, 40 insertions(+), 30 deletions(-) diff --git a/library/algebra/binary.lean b/library/algebra/binary.lean index 060a8cb0a..79dd40e1e 100644 --- a/library/algebra/binary.lean +++ b/library/algebra/binary.lean @@ -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 diff --git a/library/algebra/function.lean b/library/algebra/function.lean index 7e9ff6cd9..3d1b8664e 100644 --- a/library/algebra/function.lean +++ b/library/algebra/function.lean @@ -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 diff --git a/library/data/list/perm.lean b/library/data/list/perm.lean index ac4e114d9..43e210505 100644 --- a/library/data/list/perm.lean +++ b/library/data/list/perm.lean @@ -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₂ :=