From 25e78cf4cb68146c9285950af933458151770ddb Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 17 Jan 2006 17:17:32 +0000 Subject: [PATCH] An embryonic kernel of the algebraic library. Useful only to profile the universes :-) --- helm/matita/library/algebra/groups.ma | 16 ++++++ helm/matita/library/algebra/monoids.ma | 62 +++++++++++++++++++++++ helm/matita/library/algebra/semigroups.ma | 43 ++++++++++++++++ 3 files changed, 121 insertions(+) create mode 100644 helm/matita/library/algebra/groups.ma create mode 100644 helm/matita/library/algebra/monoids.ma create mode 100644 helm/matita/library/algebra/semigroups.ma diff --git a/helm/matita/library/algebra/groups.ma b/helm/matita/library/algebra/groups.ma new file mode 100644 index 000000000..6eb0054c2 --- /dev/null +++ b/helm/matita/library/algebra/groups.ma @@ -0,0 +1,16 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/algebra/groups/". + diff --git a/helm/matita/library/algebra/monoids.ma b/helm/matita/library/algebra/monoids.ma new file mode 100644 index 000000000..782da09d7 --- /dev/null +++ b/helm/matita/library/algebra/monoids.ma @@ -0,0 +1,62 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/algebra/monoids/". + +include "algebra/semigroups.ma". + +record isMonoid (SS:SemiGroup) (e:SS) : Prop ≝ + { e_is_left_unit: is_left_unit SS e; + e_is_right_unit: is_right_unit SS e + }. + +record Monoid : Type ≝ + { semigroup: SemiGroup; + e: semigroup; + properties: isMonoid ? e + }. + +coercion cic:/matita/algebra/monoids/semigroup.con. + +definition is_left_inverse ≝ + λM:Monoid. let op ≝ op M in let e ≝ e M in + λopp: M → M. + ∀x:M. op (opp x) x = e. + +definition is_right_inverse ≝ + λM:Monoid. let op ≝ op M in let e ≝ e M in + λopp: M → M. + ∀x:M. op x (opp x) = e. + +theorem is_left_inverse_to_is_right_inverse_to_eq: + ∀M:Monoid. ∀oppL,oppR. + is_left_inverse M oppL → is_right_inverse M oppR → + ∀x:M. oppL x = oppR x. + intros; + letin op ≝ (op M); + letin e ≝ (e M); + generalize in match (H x); intro; + change in H2 with (op (oppL x) x = e); + generalize in match (eq_f ? ? (λy. op y (oppR x)) ? ? H2); + simplify; fold simplify op; + intro; clear H2; + generalize in match (properties (semigroup M)); intro; + unfold isSemiGroup in H2; unfold associative in H2; + rewrite > H2 in H3; clear H2; + rewrite > H1 in H3; + rewrite > (e_is_left_unit ? ? (properties M)) in H3; + rewrite > (e_is_right_unit ? ? (properties M)) in H3; + assumption. +qed. + diff --git a/helm/matita/library/algebra/semigroups.ma b/helm/matita/library/algebra/semigroups.ma new file mode 100644 index 000000000..bea3ae584 --- /dev/null +++ b/helm/matita/library/algebra/semigroups.ma @@ -0,0 +1,43 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/algebra/semigroups". + +include "higher_order_defs/functions.ma". + +definition isSemiGroup ≝ + λC:Type. λop: C → C → C.associative C op. + +record SemiGroup : Type ≝ + { carrier: Type; + op: carrier → carrier → carrier; + properties: isSemiGroup carrier op + }. + +coercion cic:/matita/algebra/semigroups/carrier.con. + +definition is_left_unit ≝ + λS:SemiGroup. λe:S. ∀x:S. op S e x = x. + +definition is_right_unit ≝ + λS:SemiGroup. λe:S. ∀x:S. op S x e = x. + +theorem is_left_unit_to_is_right_unit_to_eq: + ∀S:SemiGroup. ∀e1,e2:S. + is_left_unit ? e1 → is_right_unit ? e2 → e1=e2. + intros; + rewrite < (H e2); + rewrite < (H1 e1) in \vdash (? ? % ?); + reflexivity. +qed. \ No newline at end of file -- 2.39.2