From: Enrico Tassi Date: Wed, 28 May 2008 11:00:26 +0000 (+0000) Subject: dama restarted X-Git-Tag: make_still_working~5114 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2caf6f16d535477ccccbf4f0ebe47edceeddab78;p=helm.git dama restarted --- diff --git a/helm/software/matita/contribs/dama/dama/Q_is_orded_divisble_group.ma b/helm/software/matita/contribs/dama/dama/Q_is_orded_divisble_group.ma deleted file mode 100644 index a0b646f33..000000000 --- a/helm/software/matita/contribs/dama/dama/Q_is_orded_divisble_group.ma +++ /dev/null @@ -1,276 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - - - -include "Q/q.ma". -include "ordered_divisible_group.ma". - -definition strong_decidable ≝ - λA:Prop.A ∨ ¬ A. - -theorem strong_decidable_to_Not_Not_eq: - ∀T:Type.∀eq: T → T → Prop.∀x,y:T. - strong_decidable (x=y) → ¬x≠y → x=y. - intros; - cases s; - [ assumption - | elim (H H1) - ] -qed. - -definition apartness_of_strong_decidable: - ∀T:Type.(∀x,y:T.strong_decidable (x=y)) → apartness. - intros; - constructor 1; - [ apply T - | apply (λx,y:T.x ≠ y); - | simplify; - intros 2; - apply (H (refl_eq ??)); - | simplify; - intros 4; - apply H; - symmetry; - assumption - | simplify; - intros; - elim (f x z); - [ elim (f z y); - [ elim H; - transitivity z; - assumption - | right; - assumption - ] - | left; - assumption - ] - ] -qed. - -theorem strong_decidable_to_strong_ext: - ∀T:Type.∀sd:∀x,y:T.strong_decidable (x=y). - ∀op:T→T. strong_ext (apartness_of_strong_decidable ? sd) op. - intros 6; - intro; - apply a; - apply eq_f; - assumption; -qed. - -theorem strong_decidable_to_transitive_to_cotransitive: - ∀T:Type.∀le:T→T→Prop.(∀x,y:T.strong_decidable (le x y)) → - transitive ? le → cotransitive ? (λx,y.¬ (le x y)). - intros; - whd; - simplify; - intros; - elim (f x z); - [ elim (f z y); - [ elim H; - apply (t ? z); - assumption - | right; - assumption - ] - | left; - assumption - ] -qed. - -theorem reflexive_to_coreflexive: - ∀T:Type.∀le:T→T→Prop.reflexive ? le → coreflexive ? (λx,y.¬(le x y)). - intros; - unfold; - simplify; - intros 2; - apply H1; - apply H; -qed. - -definition ordered_set_of_strong_decidable: - ∀T:Type.∀le:T→T→Prop.(∀x,y:T.strong_decidable (le x y)) → - transitive ? le → reflexive ? le → excess. - intros; - constructor 1; - [ constructor 1; - [ constructor 1; - [ constructor 1; - [ apply T - | apply (λx,y.¬(le x y)); - | apply reflexive_to_coreflexive; - assumption - | apply strong_decidable_to_transitive_to_cotransitive; - assumption] - no ported to duality - ] -qed. - -definition abelian_group_of_strong_decidable: - ∀T:Type.∀plus:T→T→T.∀zero:T.∀opp:T→T. - (∀x,y:T.strong_decidable (x=y)) → - associative ? plus (eq T) → - commutative ? plus (eq T) → - (∀x:T. plus zero x = x) → - (∀x:T. plus (opp x) x = zero) → - abelian_group. - intros; - constructor 1; - [apply (apartness_of_strong_decidable ? f);] - try assumption; - [ change with (associative ? plus (λx,y:T.¬x≠y)); - simplify; - intros; - intro; - apply H2; - apply a; - | intros 2; - intro; - apply a1; - apply c; - | intro; - intro; - apply a1; - apply H - | intro; - intro; - apply a1; - apply H1 - | intros; - apply strong_decidable_to_strong_ext; - assumption - ] -qed. - -definition left_neutral ≝ λC:Type.λop.λe:C. ∀x:C. op e x = x. -definition left_inverse ≝ λC:Type.λop.λe:C.λinv:C→C. ∀x:C. op (inv x) x = e. - -record nabelian_group : Type ≝ - { ncarr:> Type; - nplus: ncarr → ncarr → ncarr; - nzero: ncarr; - nopp: ncarr → ncarr; - nplus_assoc: associative ? nplus (eq ncarr); - nplus_comm: commutative ? nplus (eq ncarr); - nzero_neutral: left_neutral ? nplus nzero; - nopp_inverse: left_inverse ? nplus nzero nopp - }. - -definition abelian_group_of_nabelian_group: - ∀G:nabelian_group.(∀x,y:G.strong_decidable (x=y)) → abelian_group. - intros; - apply abelian_group_of_strong_decidable; - [2: apply (nplus G) - | skip - | apply (nzero G) - | apply (nopp G) - | assumption - | apply nplus_assoc; - | apply nplus_comm; - | apply nzero_neutral; - | apply nopp_inverse - ] -qed. - -definition Z_abelian_group: abelian_group. - apply abelian_group_of_nabelian_group; - [ constructor 1; - [ apply Z - | apply Zplus - | apply OZ - | apply Zopp - | whd; - intros; - symmetry; - apply associative_Zplus - | apply sym_Zplus - | intro; - reflexivity - | intro; - rewrite > sym_Zplus; - apply Zplus_Zopp; - ] - | simplify; - intros; - unfold; - generalize in match (eqZb_to_Prop x y); - elim (eqZb x y); - simplify in H; - [ left ; assumption - | right; assumption - ] - ] -qed. - -record nordered_set: Type ≝ - { nos_carr:> Type; - nos_le: nos_carr → nos_carr → Prop; - nos_reflexive: reflexive ? nos_le; - nos_transitive: transitive ? nos_le - }. - -definition excess_of_nordered_group: - ∀O:nordered_set.(∀x,y:O. strong_decidable (nos_le ? x y)) → excess. - intros; - constructor 1; - [ apply (nos_carr O) - | apply (λx,y.¬(nos_le ? x y)) - | apply reflexive_to_coreflexive; - apply nos_reflexive - | apply strong_decidable_to_transitive_to_cotransitive; - [ assumption - | apply nos_transitive - ] - ] -qed. - -lemma non_deve_stare_qui: reflexive ? Zle. - intro; - elim x; - [ exact I - |2,3: simplify; - apply le_n; - ] -qed. - -axiom non_deve_stare_qui3: ∀x,y:Z. x < y → x ≤ y. - -axiom non_deve_stare_qui4: ∀x,y:Z. x < y → y ≰ x. - -definition Z_excess: excess. - apply excess_of_nordered_group; - [ constructor 1; - [ apply Z - | apply Zle - | apply non_deve_stare_qui - | apply transitive_Zle - ] - | simplify; - intros; - unfold; - generalize in match (Z_compare_to_Prop x y); - cases (Z_compare x y); simplify; intro; - [ left; - apply non_deve_stare_qui3; - assumption - | left; - rewrite > H; - apply non_deve_stare_qui - | right; - apply non_deve_stare_qui4; - assumption - ] - ] -qed. \ No newline at end of file diff --git a/helm/software/matita/contribs/dama/dama/TODO b/helm/software/matita/contribs/dama/dama/TODO deleted file mode 100644 index 353329bea..000000000 --- a/helm/software/matita/contribs/dama/dama/TODO +++ /dev/null @@ -1,4 +0,0 @@ -changing file resets the display-notation ref, but not the GUI tick -mettere una maction in tutti i body (ma forse non basta) -la visualizzazione dellea notazione se viene disttivata e poi se ne definisce una... la rende causa -il fatto che disabilitarla significa rimuovere quelle definite fino ad ora, non disabilitarla in senso proprio. diff --git a/helm/software/matita/contribs/dama/dama/constructive_connectives.ma b/helm/software/matita/contribs/dama/dama/constructive_connectives.ma deleted file mode 100644 index 78e2ec571..000000000 --- a/helm/software/matita/contribs/dama/dama/constructive_connectives.ma +++ /dev/null @@ -1,53 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -include "logic/connectives.ma". - -inductive Or (A,B:Type) : Type ≝ - Left : A → Or A B - | Right : B → Or A B. - -interpretation "constructive or" 'or x y = - (cic:/matita/constructive_connectives/Or.ind#xpointer(1/1) x y). - -inductive And (A,B:Type) : Type ≝ - | Conj : A → B → And A B. - -interpretation "constructive and" 'and x y = - (cic:/matita/constructive_connectives/And.ind#xpointer(1/1) x y). - -inductive exT (A:Type) (P:A→Type) : Type ≝ - ex_introT: ∀w:A. P w → exT A P. - -inductive ex (A:Type) (P:A→Prop) : Type ≝ - ex_intro: ∀w:A. P w → ex A P. - -(* -notation < "hvbox(Σ ident i opt (: ty) break . p)" - right associative with precedence 20 -for @{ 'sigma ${default - @{\lambda ${ident i} : $ty. $p)} - @{\lambda ${ident i} . $p}}}. -*) - -interpretation "constructive exists" 'exists \eta.x = - (cic:/matita/constructive_connectives/ex.ind#xpointer(1/1) _ x). -interpretation "constructive exists (Type)" 'exists \eta.x = - (cic:/matita/constructive_connectives/exT.ind#xpointer(1/1) _ x). - -alias id "False" = "cic:/matita/logic/connectives/False.ind#xpointer(1/1)". -definition Not ≝ λx:Type.x → False. - -interpretation "constructive not" 'not x = - (cic:/matita/constructive_connectives/Not.con x). diff --git a/helm/software/matita/contribs/dama/dama/constructive_higher_order_relations.ma b/helm/software/matita/contribs/dama/dama/constructive_higher_order_relations.ma deleted file mode 100644 index 8d195396c..000000000 --- a/helm/software/matita/contribs/dama/dama/constructive_higher_order_relations.ma +++ /dev/null @@ -1,51 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - - - -include "constructive_connectives.ma". -include "higher_order_defs/relations.ma". - -definition cotransitive ≝ - λC:Type.λlt:C→C→Type.∀x,y,z:C. lt x y → lt x z ∨ lt z y. - -definition coreflexive ≝ λC:Type.λlt:C→C→Type. ∀x:C. ¬ (lt x x). - -definition antisymmetric ≝ - λC:Type.λle:C→C→Type.λeq:C→C→Type.∀x,y:C.le x y → le y x → eq x y. - -definition symmetric ≝ - λC:Type.λle:C→C→Type.∀x,y:C.le x y → le y x. - -definition transitive ≝ - λC:Type.λle:C→C→Type.∀x,y,z:C.le x y → le y z → le x z. - -definition associative ≝ - λC:Type.λop:C→C→C.λeq:C→C→Type.∀x,y,z. eq (op x (op y z)) (op (op x y) z). - -definition commutative ≝ - λC:Type.λop:C→C→C.λeq:C→C→Type.∀x,y. eq (op x y) (op y x). - -alias id "antisymmetric" = "cic:/matita/higher_order_defs/relations/antisymmetric.con". -theorem antisimmetric_to_cotransitive_to_transitive: - ∀C:Type.∀le:C→C→Prop. antisymmetric ? le → cotransitive ? le → transitive ? le. -intros (T f Af cT); unfold transitive; intros (x y z fxy fyz); -lapply (cT ??z fxy) as H; cases H; [assumption] cases (Af ? ? fyz H1); -qed. - -lemma Or_symmetric: symmetric ? Or. -unfold; intros (x y H); cases H; [right|left] assumption; -qed. - - diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends index dcbfcc6f0..e69de29bb 100644 --- a/helm/software/matita/contribs/dama/dama/depends +++ b/helm/software/matita/contribs/dama/dama/depends @@ -1,38 +0,0 @@ -metric_lattice.ma excess.ma lattice.ma metric_space.ma -metric_space.ma ordered_divisible_group.ma -sandwich.ma metric_lattice.ma nat/orders.ma nat/plus.ma tend.ma -premetric_lattice.ma lattice.ma metric_space.ma -ordered_group.ma group.ma -divisible_group.ma group.ma nat/orders.ma -ordered_divisible_group.ma divisible_group.ma nat/orders.ma nat/times.ma ordered_group.ma -sequence.ma excess.ma -constructive_connectives.ma logic/connectives.ma -group.ma excess.ma -prevalued_lattice.ma ordered_group.ma -excess.ma constructive_connectives.ma constructive_higher_order_relations.ma higher_order_defs/relations.ma nat/plus.ma -sandwich_corollary.ma sandwich.ma -Q_is_orded_divisble_group.ma Q/q.ma ordered_divisible_group.ma -limit.ma excess.ma infsup.ma metric_lattice.ma tend.ma -lattice.ma excess.ma -tend.ma metric_space.ma nat/orders.ma sequence.ma -constructive_higher_order_relations.ma constructive_connectives.ma higher_order_defs/relations.ma -infsup.ma excess.ma sequence.ma -constructive_pointfree/lebesgue.ma constructive_connectives.ma metric_lattice.ma sequence.ma -classical_pointwise/topology.ma classical_pointwise/sets.ma -classical_pointwise/sigma_algebra.ma classical_pointwise/topology.ma -classical_pointwise/sets.ma logic/connectives.ma nat/nat.ma -classical_pointfree/ordered_sets.ma excess.ma -classical_pointfree/ordered_sets2.ma classical_pointfree/ordered_sets.ma -attic/fields.ma attic/rings.ma -attic/reals.ma attic/ordered_fields_ch0.ma -attic/integration_algebras.ma attic/vector_spaces.ma lattice.ma -attic/vector_spaces.ma attic/reals.ma -attic/rings.ma group.ma -attic/ordered_fields_ch0.ma group.ma attic/fields.ma ordered_group.ma -Q/q.ma -higher_order_defs/relations.ma -logic/connectives.ma -nat/nat.ma -nat/orders.ma -nat/plus.ma -nat/times.ma diff --git a/helm/software/matita/contribs/dama/dama/divisible_group.ma b/helm/software/matita/contribs/dama/dama/divisible_group.ma deleted file mode 100644 index 3a79b11bb..000000000 --- a/helm/software/matita/contribs/dama/dama/divisible_group.ma +++ /dev/null @@ -1,99 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - - - -include "nat/orders.ma". -include "group.ma". - -let rec gpow (G : abelian_group) (x : G) (n : nat) on n : G ≝ - match n with [ O ⇒ 0 | S m ⇒ x + gpow ? x m]. - -interpretation "additive abelian group pow" 'times n x = - (cic:/matita/divisible_group/gpow.con _ x n). - -record dgroup : Type ≝ { - dg_carr:> abelian_group; - dg_prop: ∀x:dg_carr.∀n:nat.∃y.S n * y ≈ x -}. - -lemma divide: ∀G:dgroup.G → nat → G. -intros (G x n); cases (dg_prop G x n); apply w; -qed. - -interpretation "divisible group divide" 'divide x n = - (cic:/matita/divisible_group/divide.con _ x n). - -lemma divide_divides: - ∀G:dgroup.∀x:G.∀n. S n * (x / n) ≈ x. -intro G; cases G; unfold divide; intros (x n); simplify; -cases (f x n); simplify; exact H; -qed. - -lemma feq_mul: ∀G:dgroup.∀x,y:G.∀n.x≈y → n * x ≈ n * y. -intros (G x y n H); elim n; [apply eq_reflexive] -simplify; apply (Eq≈ (x + (n1 * y)) H1); -apply (Eq≈ (y+n1*y) H (eq_reflexive ??)); -qed. - -lemma div1: ∀G:dgroup.∀x:G.x/O ≈ x. -intro G; cases G; unfold divide; intros; simplify; -cases (f x O); simplify; simplify in H; intro; apply H; -apply (Ap≪ ? (plus_comm ???)); -apply (Ap≪ w (zero_neutral ??)); assumption; -qed. - -lemma apmul_ap: ∀G:dgroup.∀x,y:G.∀n.S n * x # S n * y → x # y. -intros 4 (G x y n); elim n; [2: - simplify in a; - cases (applus ????? a); [assumption] - apply f; assumption;] -apply (plus_cancr_ap ??? 0); assumption; -qed. - -lemma plusmul: ∀G:dgroup.∀x,y:G.∀n.n * (x+y) ≈ n * x + n * y. -intros (G x y n); elim n; [ - simplify; apply (Eq≈ 0 ? (zero_neutral ? 0)); apply eq_reflexive] -simplify; apply eq_sym; apply (Eq≈ (x+y+(n1*x+n1*y))); [ - apply (Eq≈ (x+(n1*x+(y+(n1*y))))); [ - apply eq_sym; apply plus_assoc;] - apply (Eq≈ (x+((n1*x+y+(n1*y))))); [ - apply feq_plusl; apply plus_assoc;] - apply (Eq≈ (x+(y+n1*x+n1*y))); [ - apply feq_plusl; apply feq_plusr; apply plus_comm;] - apply (Eq≈ (x+(y+(n1*x+n1*y)))); [ - apply feq_plusl; apply eq_sym; apply plus_assoc;] - apply plus_assoc;] -apply feq_plusl; apply eq_sym; assumption; -qed. - -lemma mulzero: ∀G:dgroup.∀n.n*0 ≈ 0. [2: apply dg_carr; apply G] -intros; elim n; [simplify; apply eq_reflexive] -simplify; apply (Eq≈ ? (zero_neutral ??)); assumption; -qed. - -let rec gpowS (G : abelian_group) (x : G) (n : nat) on n : G ≝ - match n with [ O ⇒ x | S m ⇒ gpowS ? x m + x]. - -lemma gpowS_gpow: ∀G:dgroup.∀e:G.∀n. S n * e ≈ gpowS ? e n. -intros (G e n); elim n; simplify; [ - apply (Eq≈ ? (plus_comm ???));apply zero_neutral] -apply (Eq≈ ?? (plus_comm ???)); -apply (Eq≈ (e+S n1*e) ? H); clear H; simplify; apply eq_reflexive; -qed. - -lemma divpow: ∀G:dgroup.∀e:G.∀n. e ≈ gpowS ? (e/n) n. -intros (G e n); apply (Eq≈ ?? (gpowS_gpow ?(e/n) n)); -apply eq_sym; apply divide_divides; -qed. diff --git a/helm/software/matita/contribs/dama/dama/doc/apal.pdf b/helm/software/matita/contribs/dama/dama/doc/apal.pdf new file mode 100644 index 000000000..393e71e9d Binary files /dev/null and b/helm/software/matita/contribs/dama/dama/doc/apal.pdf differ diff --git a/helm/software/matita/contribs/dama/dama/excess.ma b/helm/software/matita/contribs/dama/dama/excess.ma deleted file mode 100644 index 9068d297b..000000000 --- a/helm/software/matita/contribs/dama/dama/excess.ma +++ /dev/null @@ -1,279 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - - - -include "higher_order_defs/relations.ma". -include "nat/plus.ma". -include "constructive_higher_order_relations.ma". -include "constructive_connectives.ma". - -record excess_base : Type ≝ { - exc_carr:> Type; - exc_excess: exc_carr → exc_carr → Type; - exc_coreflexive: coreflexive ? exc_excess; - exc_cotransitive: cotransitive ? exc_excess -}. - -interpretation "Excess base excess" 'nleq a b = (cic:/matita/excess/exc_excess.con _ a b). - -(* E(#,≰) → E(#,sym(≰)) *) -lemma make_dual_exc: excess_base → excess_base. -intro E; -apply (mk_excess_base (exc_carr E)); - [ apply (λx,y:E.y≰x);|apply exc_coreflexive; - | unfold cotransitive; simplify; intros (x y z H); - cases (exc_cotransitive E ??z H);[right|left]assumption] -qed. - -record excess_dual : Type ≝ { - exc_dual_base:> excess_base; - exc_dual_dual_ : excess_base; - exc_with: exc_dual_dual_ = make_dual_exc exc_dual_base -}. - -lemma mk_excess_dual_smart: excess_base → excess_dual. -intro; apply mk_excess_dual; [apply e| apply (make_dual_exc e)|reflexivity] -qed. - -definition exc_dual_dual: excess_dual → excess_base. -intro E; apply (make_dual_exc E); -qed. - -coercion cic:/matita/excess/exc_dual_dual.con. - -record apartness : Type ≝ { - ap_carr:> Type; - ap_apart: ap_carr → ap_carr → Type; - ap_coreflexive: coreflexive ? ap_apart; - ap_symmetric: symmetric ? ap_apart; - ap_cotransitive: cotransitive ? ap_apart -}. - -notation "hvbox(a break # b)" non associative with precedence 50 for @{ 'apart $a $b}. -interpretation "apartness" 'apart x y = (cic:/matita/excess/ap_apart.con _ x y). - -definition apartness_of_excess_base: excess_base → apartness. -intros (E); apply (mk_apartness E (λa,b:E. a ≰ b ∨ b ≰ a)); -[1: unfold; cases E; simplify; clear E; intros (x); unfold; - intros (H1); apply (H x); cases H1; assumption; -|2: unfold; intros(x y H); cases H; clear H; [right|left] assumption; -|3: intros (E); unfold; cases E (T f _ cTf); simplify; intros (x y z Axy); - cases Axy (H H); lapply (cTf ? ? z H) as H1; cases H1; clear Axy H1; - [left; left|right; left|right; right|left; right] assumption] -qed. - -record excess_ : Type ≝ { - exc_exc:> excess_dual; - exc_ap_: apartness; - exc_with1: ap_carr exc_ap_ = exc_carr exc_exc -}. - -definition exc_ap: excess_ → apartness. -intro E; apply (mk_apartness E); unfold Type_OF_excess_; -cases (exc_with1 E); simplify; -[apply (ap_apart (exc_ap_ E)); -|apply ap_coreflexive;|apply ap_symmetric;|apply ap_cotransitive] -qed. - -coercion cic:/matita/excess/exc_ap.con. - -interpretation "Excess excess_" 'nleq a b = - (cic:/matita/excess/exc_excess.con (cic:/matita/excess/excess_base_OF_excess_1.con _) a b). - -record excess : Type ≝ { - excess_carr:> excess_; - ap2exc: ∀y,x:excess_carr. y # x → y ≰ x ∨ x ≰ y; - exc2ap: ∀y,x:excess_carr.y ≰ x ∨ x ≰ y → y # x -}. - -interpretation "Excess excess" 'nleq a b = - (cic:/matita/excess/exc_excess.con (cic:/matita/excess/excess_base_OF_excess1.con _) a b). - -interpretation "Excess (dual) excess" 'ngeq a b = - (cic:/matita/excess/exc_excess.con (cic:/matita/excess/excess_base_OF_excess.con _) a b). - -definition strong_ext ≝ λA:apartness.λop:A→A.∀x,y. op x # op y → x # y. - -definition le ≝ λE:excess_base.λa,b:E. ¬ (a ≰ b). - -interpretation "Excess less or equal than" 'leq a b = - (cic:/matita/excess/le.con (cic:/matita/excess/excess_base_OF_excess1.con _) a b). - -interpretation "Excess less or equal than" 'geq a b = - (cic:/matita/excess/le.con (cic:/matita/excess/excess_base_OF_excess.con _) a b). - -lemma le_reflexive: ∀E.reflexive ? (le E). -unfold reflexive; intros 3 (E x H); apply (exc_coreflexive ?? H); -qed. - -lemma le_transitive: ∀E.transitive ? (le E). -unfold transitive; intros 7 (E x y z H1 H2 H3); cases (exc_cotransitive ??? y H3) (H4 H4); -[cases (H1 H4)|cases (H2 H4)] -qed. - -definition eq ≝ λA:apartness.λa,b:A. ¬ (a # b). - -notation "hvbox(a break ≈ b)" non associative with precedence 50 for @{ 'napart $a $b}. -interpretation "Apartness alikeness" 'napart a b = (cic:/matita/excess/eq.con _ a b). -interpretation "Excess alikeness" 'napart a b = (cic:/matita/excess/eq.con (cic:/matita/excess/excess_base_OF_excess1.con _) a b). -interpretation "Excess (dual) alikeness" 'napart a b = (cic:/matita/excess/eq.con (cic:/matita/excess/excess_base_OF_excess.con _) a b). - -lemma eq_reflexive:∀E:apartness. reflexive ? (eq E). -intros (E); unfold; intros (x); apply ap_coreflexive; -qed. - -lemma eq_sym_:∀E:apartness.symmetric ? (eq E). -unfold symmetric; intros 5 (E x y H H1); cases (H (ap_symmetric ??? H1)); -qed. - -lemma eq_sym:∀E:apartness.∀x,y:E.x ≈ y → y ≈ x ≝ eq_sym_. - -(* SETOID REWRITE *) -coercion cic:/matita/excess/eq_sym.con. - -lemma eq_trans_: ∀E:apartness.transitive ? (eq E). -(* bug. intros k deve fare whd quanto basta *) -intros 6 (E x y z Exy Eyz); intro Axy; cases (ap_cotransitive ???y Axy); -[apply Exy|apply Eyz] assumption. -qed. - -lemma eq_trans:∀E:apartness.∀x,z,y:E.x ≈ y → y ≈ z → x ≈ z ≝ - λE,x,y,z.eq_trans_ E x z y. - -notation > "'Eq'≈" non associative with precedence 50 for @{'eqrewrite}. -interpretation "eq_rew" 'eqrewrite = (cic:/matita/excess/eq_trans.con _ _ _). - -alias id "antisymmetric" = "cic:/matita/constructive_higher_order_relations/antisymmetric.con". -lemma le_antisymmetric: - ∀E:excess.antisymmetric ? (le (excess_base_OF_excess1 E)) (eq E). -intros 5 (E x y Lxy Lyx); intro H; -cases (ap2exc ??? H); [apply Lxy;|apply Lyx] assumption; -qed. - -definition lt ≝ λE:excess.λa,b:E. a ≤ b ∧ a # b. - -interpretation "ordered sets less than" 'lt a b = (cic:/matita/excess/lt.con _ a b). - -lemma lt_coreflexive: ∀E.coreflexive ? (lt E). -intros 2 (E x); intro H; cases H (_ ABS); -apply (ap_coreflexive ? x ABS); -qed. - -lemma lt_transitive: ∀E.transitive ? (lt E). -intros (E); unfold; intros (x y z H1 H2); cases H1 (Lxy Axy); cases H2 (Lyz Ayz); -split; [apply (le_transitive ???? Lxy Lyz)] clear H1 H2; -elim (ap2exc ??? Axy) (H1 H1); elim (ap2exc ??? Ayz) (H2 H2); [1:cases (Lxy H1)|3:cases (Lyz H2)] -clear Axy Ayz;lapply (exc_cotransitive (exc_dual_base E)) as c; unfold cotransitive in c; -lapply (exc_coreflexive (exc_dual_base E)) as r; unfold coreflexive in r; -[1: lapply (c ?? y H1) as H3; elim H3 (H4 H4); [cases (Lxy H4)|cases (r ? H4)] -|2: lapply (c ?? x H2) as H3; elim H3 (H4 H4); [apply exc2ap; right; assumption|cases (Lxy H4)]] -qed. - -theorem lt_to_excess: ∀E:excess.∀a,b:E. (a < b) → (b ≰ a). -intros (E a b Lab); elim Lab (LEab Aab); -elim (ap2exc ??? Aab) (H H); [cases (LEab H)] fold normalize (b ≰ a); assumption; (* BUG *) -qed. - -lemma le_rewl: ∀E:excess.∀z,y,x:E. x ≈ y → x ≤ z → y ≤ z. -intros (E z y x Exy Lxz); apply (le_transitive ???? ? Lxz); -intro Xyz; apply Exy; apply exc2ap; right; assumption; -qed. - -lemma le_rewr: ∀E:excess.∀z,y,x:E. x ≈ y → z ≤ x → z ≤ y. -intros (E z y x Exy Lxz); apply (le_transitive ???? Lxz); -intro Xyz; apply Exy; apply exc2ap; left; assumption; -qed. - -notation > "'Le'≪" non associative with precedence 50 for @{'lerewritel}. -interpretation "le_rewl" 'lerewritel = (cic:/matita/excess/le_rewl.con _ _ _). -notation > "'Le'≫" non associative with precedence 50 for @{'lerewriter}. -interpretation "le_rewr" 'lerewriter = (cic:/matita/excess/le_rewr.con _ _ _). - -lemma ap_rewl: ∀A:apartness.∀x,z,y:A. x ≈ y → y # z → x # z. -intros (A x z y Exy Ayz); cases (ap_cotransitive ???x Ayz); [2:assumption] -cases (Exy (ap_symmetric ??? a)); -qed. - -lemma ap_rewr: ∀A:apartness.∀x,z,y:A. x ≈ y → z # y → z # x. -intros (A x z y Exy Azy); apply ap_symmetric; apply (ap_rewl ???? Exy); -apply ap_symmetric; assumption; -qed. - -notation > "'Ap'≪" non associative with precedence 50 for @{'aprewritel}. -interpretation "ap_rewl" 'aprewritel = (cic:/matita/excess/ap_rewl.con _ _ _). -notation > "'Ap'≫" non associative with precedence 50 for @{'aprewriter}. -interpretation "ap_rewr" 'aprewriter = (cic:/matita/excess/ap_rewr.con _ _ _). - -alias symbol "napart" = "Apartness alikeness". -lemma exc_rewl: ∀A:excess.∀x,z,y:A. x ≈ y → y ≰ z → x ≰ z. -intros (A x z y Exy Ayz); elim (exc_cotransitive ???x Ayz); [2:assumption] -cases Exy; apply exc2ap; right; assumption; -qed. - -lemma exc_rewr: ∀A:excess.∀x,z,y:A. x ≈ y → z ≰ y → z ≰ x. -intros (A x z y Exy Azy); elim (exc_cotransitive ???x Azy); [assumption] -elim (Exy); apply exc2ap; left; assumption; -qed. - -notation > "'Ex'≪" non associative with precedence 50 for @{'excessrewritel}. -interpretation "exc_rewl" 'excessrewritel = (cic:/matita/excess/exc_rewl.con _ _ _). -notation > "'Ex'≫" non associative with precedence 50 for @{'excessrewriter}. -interpretation "exc_rewr" 'excessrewriter = (cic:/matita/excess/exc_rewr.con _ _ _). - -lemma lt_rewr: ∀A:excess.∀x,z,y:A. x ≈ y → z < y → z < x. -intros (A x y z E H); split; elim H; -[apply (Le≫ ? (eq_sym ??? E));|apply (Ap≫ ? E)] assumption; -qed. - -lemma lt_rewl: ∀A:excess.∀x,z,y:A. x ≈ y → y < z → x < z. -intros (A x y z E H); split; elim H; -[apply (Le≪ ? (eq_sym ??? E));| apply (Ap≪ ? E);] assumption; -qed. - -notation > "'Lt'≪" non associative with precedence 50 for @{'ltrewritel}. -interpretation "lt_rewl" 'ltrewritel = (cic:/matita/excess/lt_rewl.con _ _ _). -notation > "'Lt'≫" non associative with precedence 50 for @{'ltrewriter}. -interpretation "lt_rewr" 'ltrewriter = (cic:/matita/excess/lt_rewr.con _ _ _). - -lemma lt_le_transitive: ∀A:excess.∀x,y,z:A.x < y → y ≤ z → x < z. -intros (A x y z LT LE); cases LT (LEx APx); split; [apply (le_transitive ???? LEx LE)] -apply exc2ap; cases (ap2exc ??? APx) (EXx EXx); [cases (LEx EXx)] -cases (exc_cotransitive ??? z EXx) (EXz EXz); [cases (LE EXz)] -right; assumption; -qed. - -lemma le_lt_transitive: ∀A:excess.∀x,y,z:A.x ≤ y → y < z → x < z. -intros (A x y z LE LT); cases LT (LEx APx); split; [apply (le_transitive ???? LE LEx)] -elim (ap2exc ??? APx) (EXx EXx); [cases (LEx EXx)] -elim (exc_cotransitive ??? x EXx) (EXz EXz); [apply exc2ap; right; assumption] -cases LE; assumption; -qed. - -lemma le_le_eq: ∀E:excess.∀a,b:E. a ≤ b → b ≤ a → a ≈ b. -intros (E x y L1 L2); intro H; cases (ap2exc ??? H); [apply L1|apply L2] assumption; -qed. - -lemma eq_le_le: ∀E:excess.∀a,b:E. a ≈ b → a ≤ b ∧ b ≤ a. -intros (E x y H); whd in H; -split; intro; apply H; apply exc2ap; [left|right] assumption. -qed. - -lemma ap_le_to_lt: ∀E:excess.∀a,c:E.c # a → c ≤ a → c < a. -intros; split; assumption; -qed. - -definition total_order_property : ∀E:excess. Type ≝ - λE:excess. ∀a,b:E. a ≰ b → b < a. - diff --git a/helm/software/matita/contribs/dama/dama/group.ma b/helm/software/matita/contribs/dama/dama/group.ma deleted file mode 100644 index 104dcf274..000000000 --- a/helm/software/matita/contribs/dama/dama/group.ma +++ /dev/null @@ -1,220 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - - - -include "excess.ma". - -definition left_neutral ≝ λC:apartness.λop.λe:C. ∀x:C. op e x ≈ x. -definition right_neutral ≝ λC:apartness.λop. λe:C. ∀x:C. op x e ≈ x. -definition left_inverse ≝ λC:apartness.λop.λe:C.λinv:C→C. ∀x:C. op (inv x) x ≈ e. -definition right_inverse ≝ λC:apartness.λop.λe:C.λ inv: C→ C. ∀x:C. op x (inv x) ≈ e. -(* ALLOW DEFINITION WITH SOME METAS *) - -definition distributive_left ≝ - λA:apartness.λf:A→A→A.λg:A→A→A. - ∀x,y,z. f x (g y z) ≈ g (f x y) (f x z). - -definition distributive_right ≝ - λA:apartness.λf:A→A→A.λg:A→A→A. - ∀x,y,z. f (g x y) z ≈ g (f x z) (f y z). - -record abelian_group : Type ≝ - { carr:> apartness; - plus: carr → carr → carr; - zero: carr; - opp: carr → carr; - plus_assoc_: associative ? plus (eq carr); - plus_comm_: commutative ? plus (eq carr); - zero_neutral_: left_neutral ? plus zero; - opp_inverse_: left_inverse ? plus zero opp; - plus_strong_ext: ∀z.strong_ext ? (plus z) -}. - -notation "0" with precedence 89 for @{ 'zero }. - -interpretation "Abelian group zero" 'zero = - (cic:/matita/group/zero.con _). - -interpretation "Abelian group plus" 'plus a b = - (cic:/matita/group/plus.con _ a b). - -interpretation "Abelian group opp" 'uminus a = - (cic:/matita/group/opp.con _ a). - -definition minus ≝ - λG:abelian_group.λa,b:G. a + -b. - -interpretation "Abelian group minus" 'minus a b = - (cic:/matita/group/minus.con _ a b). - -lemma plus_assoc: ∀G:abelian_group.∀x,y,z:G.x+(y+z)≈x+y+z ≝ plus_assoc_. -lemma plus_comm: ∀G:abelian_group.∀x,y:G.x+y≈y+x ≝ plus_comm_. -lemma zero_neutral: ∀G:abelian_group.∀x:G.0+x≈x ≝ zero_neutral_. -lemma opp_inverse: ∀G:abelian_group.∀x:G.-x+x≈0 ≝ opp_inverse_. - -definition ext ≝ λA:apartness.λop:A→A. ∀x,y. x ≈ y → op x ≈ op y. - -lemma strong_ext_to_ext: ∀A:apartness.∀op:A→A. strong_ext ? op → ext ? op. -intros 6 (A op SEop x y Exy); intro Axy; apply Exy; apply SEop; assumption; -qed. - -lemma feq_plusl: ∀G:abelian_group.∀x,y,z:G. y ≈ z → x+y ≈ x+z. -intros (G x y z Eyz); apply (strong_ext_to_ext ?? (plus_strong_ext ? x)); -assumption; -qed. - -coercion cic:/matita/group/feq_plusl.con nocomposites. - -lemma plus_strong_extr: ∀G:abelian_group.∀z:G.strong_ext ? (λx.x + z). -intros 5 (G z x y A); simplify in A; -lapply (plus_comm ? z x) as E1; lapply (plus_comm ? z y) as E2; -lapply (Ap≪ ? E1 A) as A1; lapply (Ap≫ ? E2 A1) as A2; -apply (plus_strong_ext ???? A2); -qed. - -lemma plus_cancl_ap: ∀G:abelian_group.∀x,y,z:G.z+x # z + y → x # y. -intros; apply plus_strong_ext; assumption; -qed. - -lemma plus_cancr_ap: ∀G:abelian_group.∀x,y,z:G.x+z # y+z → x # y. -intros; apply plus_strong_extr; assumption; -qed. - -lemma feq_plusr: ∀G:abelian_group.∀x,y,z:G. y ≈ z → y+x ≈ z+x. -intros (G x y z Eyz); apply (strong_ext_to_ext ?? (plus_strong_extr ? x)); -assumption; -qed. - -coercion cic:/matita/group/feq_plusr.con nocomposites. - -(* generation of coercions to make *_rew[lr] easier *) -lemma feq_plusr_sym_: ∀G:abelian_group.∀x,y,z:G.z ≈ y → y+x ≈ z+x. -compose feq_plusr with eq_sym (H); apply H; assumption; -qed. -coercion cic:/matita/group/feq_plusr_sym_.con nocomposites. -lemma feq_plusl_sym_: ∀G:abelian_group.∀x,y,z:G.z ≈ y → x+y ≈ x+z. -compose feq_plusl with eq_sym (H); apply H; assumption; -qed. -coercion cic:/matita/group/feq_plusl_sym_.con nocomposites. - -lemma fap_plusl: ∀G:abelian_group.∀x,y,z:G. y # z → x+y # x+z. -intros (G x y z Ayz); apply (plus_strong_ext ? (-x)); -apply (Ap≪ ((-x + x) + y)); -[1: apply plus_assoc; -|2: apply (Ap≫ ((-x +x) +z)); - [1: apply plus_assoc; - |2: apply (Ap≪ (0 + y)); - [1: apply (feq_plusr ???? (opp_inverse ??)); - |2: apply (Ap≪ ? (zero_neutral ? y)); - apply (Ap≫ (0 + z) (opp_inverse ??)); - apply (Ap≫ ? (zero_neutral ??)); assumption;]]] -qed. - -lemma fap_plusr: ∀G:abelian_group.∀x,y,z:G. y # z → y+x # z+x. -intros (G x y z Ayz); apply (plus_strong_extr ? (-x)); -apply (Ap≪ (y + (x + -x))); -[1: apply (eq_sym ??? (plus_assoc ????)); -|2: apply (Ap≫ (z + (x + -x))); - [1: apply (eq_sym ??? (plus_assoc ????)); - |2: apply (Ap≪ (y + (-x+x)) (plus_comm ? x (-x))); - apply (Ap≪ (y + 0) (opp_inverse ??)); - apply (Ap≪ (0 + y) (plus_comm ???)); - apply (Ap≪ y (zero_neutral ??)); - apply (Ap≫ (z + (-x+x)) (plus_comm ? x (-x))); - apply (Ap≫ (z + 0) (opp_inverse ??)); - apply (Ap≫ (0 + z) (plus_comm ???)); - apply (Ap≫ z (zero_neutral ??)); - assumption]] -qed. - -lemma applus: ∀E:abelian_group.∀x,a,y,b:E.x + a # y + b → x # y ∨ a # b. -intros; cases (ap_cotransitive ??? (y+a) a1); [left|right] -[apply (plus_cancr_ap ??? a)|apply (plus_cancl_ap ??? y)] -assumption; -qed. - -lemma plus_cancl: ∀G:abelian_group.∀y,z,x:G. x+y ≈ x+z → y ≈ z. -intros 6 (G y z x E Ayz); apply E; apply fap_plusl; assumption; -qed. - -lemma plus_cancr: ∀G:abelian_group.∀y,z,x:G. y+x ≈ z+x → y ≈ z. -intros 6 (G y z x E Ayz); apply E; apply fap_plusr; assumption; -qed. - -theorem eq_opp_plus_plus_opp_opp: - ∀G:abelian_group.∀x,y:G. -(x+y) ≈ -x + -y. -intros (G x y); apply (plus_cancr ??? (x+y)); -apply (Eq≈ 0 (opp_inverse ??)); -apply (Eq≈ (-x + -y + x + y)); [2: apply (eq_sym ??? (plus_assoc ????))] -apply (Eq≈ (-y + -x + x + y)); [2: repeat apply feq_plusr; apply plus_comm] -apply (Eq≈ (-y + (-x + x) + y)); [2: apply feq_plusr; apply plus_assoc;] -apply (Eq≈ (-y + 0 + y)); - [2: apply feq_plusr; apply feq_plusl; apply eq_sym; apply opp_inverse] -apply (Eq≈ (-y + y)); - [2: apply feq_plusr; apply eq_sym; - apply (Eq≈ (0+-y)); [apply plus_comm|apply zero_neutral]] -apply eq_sym; apply opp_inverse. -qed. - -theorem eq_opp_opp_x_x: ∀G:abelian_group.∀x:G.--x ≈ x. -intros (G x); apply (plus_cancl ??? (-x)); -apply (Eq≈ (--x + -x) (plus_comm ???)); -apply (Eq≈ 0 (opp_inverse ??)); -apply eq_sym; apply opp_inverse; -qed. - -theorem eq_zero_opp_zero: ∀G:abelian_group.0 ≈ -0. [assumption] -intro G; apply (plus_cancr ??? 0); -apply (Eq≈ 0); [apply zero_neutral;] -apply eq_sym; apply opp_inverse; -qed. - -lemma feq_oppr: ∀G:abelian_group.∀x,y,z:G. y ≈ z → x ≈ -y → x ≈ -z. -intros (G x y z H1 H2); apply (plus_cancr ??? z); -apply (Eq≈ 0 ? (opp_inverse ??)); -apply (Eq≈ (-y + z) H2); -apply (Eq≈ (-y + y) H1); -apply (Eq≈ 0 (opp_inverse ??)); -apply eq_reflexive; -qed. - -lemma feq_oppl: ∀G:abelian_group.∀x,y,z:G. y ≈ z → -y ≈ x → -z ≈ x. -intros (G x y z H1 H2); apply eq_sym; apply (feq_oppr ??y); -[2:apply eq_sym] assumption; -qed. - -lemma feq_opp: ∀G:abelian_group.∀x,y:G. x ≈ y → -x ≈ -y. -intros (G x y H); apply (feq_oppl ??y ? H); apply eq_reflexive; -qed. - -coercion cic:/matita/group/feq_opp.con nocomposites. - -lemma eq_opp_sym: ∀G:abelian_group.∀x,y:G. y ≈ x → -x ≈ -y. -compose feq_opp with eq_sym (H); apply H; assumption; -qed. - -coercion cic:/matita/group/eq_opp_sym.con nocomposites. - -lemma eq_opp_plusr: ∀G:abelian_group.∀x,y,z:G. x ≈ y → -(x + z) ≈ -(y + z). -compose feq_plusr with feq_opp(H); apply H; assumption; -qed. - -coercion cic:/matita/group/eq_opp_plusr.con nocomposites. - -lemma eq_opp_plusl: ∀G:abelian_group.∀x,y,z:G. x ≈ y → -(z + x) ≈ -(z + y). -compose feq_plusl with feq_opp(H); apply H; assumption; -qed. - -coercion cic:/matita/group/eq_opp_plusl.con nocomposites. diff --git a/helm/software/matita/contribs/dama/dama/infsup.ma b/helm/software/matita/contribs/dama/dama/infsup.ma deleted file mode 100644 index cc3292fd0..000000000 --- a/helm/software/matita/contribs/dama/dama/infsup.ma +++ /dev/null @@ -1,53 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -include "sequence.ma". - -definition upper_bound ≝ λO:excess.λa:sequence O.λu:O.∀n:nat.a n ≤ u. - -definition weak_sup ≝ - λO:excess.λs:sequence O.λx. - upper_bound ? s x ∧ (∀y:O.upper_bound ? s y → x ≤ y). - -definition strong_sup ≝ - λO:excess.λs:sequence O.λx.upper_bound ? s x ∧ (∀y:O.x ≰ y → ∃n.s n ≰ y). - -definition increasing ≝ λO:excess.λa:sequence O.∀n:nat.a n ≤ a (S n). - -notation < "x \nbsp 'is_upper_bound' \nbsp s" non associative with precedence 50 for @{'upper_bound $_ $s $x}. -notation < "x \nbsp 'is_lower_bound' \nbsp s" non associative with precedence 50 for @{'lower_bound $_ $s $x}. -notation < "s \nbsp 'is_increasing'" non associative with precedence 50 for @{'increasing $_ $s}. -notation < "s \nbsp 'is_decreasing'" non associative with precedence 50 for @{'decreasing $_ $s}. -notation < "x \nbsp 'is_strong_sup' \nbsp s" non associative with precedence 50 for @{'strong_sup $_ $s $x}. -notation < "x \nbsp 'is_strong_inf' \nbsp s" non associative with precedence 50 for @{'strong_inf $_ $s $x}. - -notation > "x 'is_upper_bound' s 'in' e" non associative with precedence 50 for @{'upper_bound $e $s $x}. -notation > "x 'is_lower_bound' s 'in' e" non associative with precedence 50 for @{'lower_bound $e $s $x}. -notation > "s 'is_increasing' 'in' e" non associative with precedence 50 for @{'increasing $e $s}. -notation > "s 'is_decreasing' 'in' e" non associative with precedence 50 for @{'decreasing $e $s}. -notation > "x 'is_strong_sup' s 'in' e" non associative with precedence 50 for @{'strong_sup $e $s $x}. -notation > "x 'is_strong_inf' s 'in' e" non associative with precedence 50 for @{'strong_inf $e $s $x}. - -interpretation "Excess upper bound" 'upper_bound e s x = (cic:/matita/infsup/upper_bound.con e s x). -interpretation "Excess lower bound" 'lower_bound e s x = (cic:/matita/infsup/upper_bound.con (cic:/matita/excess/dual_exc.con e) s x). -interpretation "Excess increasing" 'increasing e s = (cic:/matita/infsup/increasing.con e s). -interpretation "Excess decreasing" 'decreasing e s = (cic:/matita/infsup/increasing.con (cic:/matita/excess/dual_exc.con e) s). -interpretation "Excess strong sup" 'strong_sup e s x = (cic:/matita/infsup/strong_sup.con e s x). -interpretation "Excess strong inf" 'strong_inf e s x = (cic:/matita/infsup/strong_sup.con (cic:/matita/excess/dual_exc.con e) s x). - -lemma strong_sup_is_weak: - ∀O:excess.∀s:sequence O.∀x:O.strong_sup ? s x → weak_sup ? s x. -intros (O s x Ssup); elim Ssup (Ubx M); clear Ssup; split; [assumption] -intros 3 (y Uby E); cases (M ? E) (n En); unfold in Uby; cases (Uby ? En); -qed. diff --git a/helm/software/matita/contribs/dama/dama/lattice.ma b/helm/software/matita/contribs/dama/dama/lattice.ma deleted file mode 100644 index adf751b83..000000000 --- a/helm/software/matita/contribs/dama/dama/lattice.ma +++ /dev/null @@ -1,484 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -include "excess.ma". - -record semi_lattice_base : Type ≝ { - sl_carr:> apartness; - sl_op: sl_carr → sl_carr → sl_carr; - sl_op_refl: ∀x.sl_op x x ≈ x; - sl_op_comm: ∀x,y:sl_carr. sl_op x y ≈ sl_op y x; - sl_op_assoc: ∀x,y,z:sl_carr. sl_op x (sl_op y z) ≈ sl_op (sl_op x y) z; - sl_strong_extop: ∀x.strong_ext ? (sl_op x) -}. - -notation "a \cross b" left associative with precedence 50 for @{ 'op $a $b }. -interpretation "semi lattice base operation" 'op a b = (cic:/matita/lattice/sl_op.con _ a b). - -lemma excess_of_semi_lattice_base: semi_lattice_base → excess. -intro l; -apply mk_excess; -[1: apply mk_excess_; - [1: apply mk_excess_dual_smart; - - apply (mk_excess_base (sl_carr l)); - [1: apply (λa,b:sl_carr l.a # (a ✗ b)); - |2: unfold; intros 2 (x H); simplify in H; - lapply (Ap≪ ? (sl_op_refl ??) H) as H1; clear H; - apply (ap_coreflexive ?? H1); - |3: unfold; simplify; intros (x y z H1); - cases (ap_cotransitive ??? ((x ✗ z) ✗ y) H1) (H2 H2);[2: - lapply (Ap≪ ? (sl_op_comm ???) H2) as H21; - lapply (Ap≫ ? (sl_op_comm ???) H21) as H22; clear H21 H2; - lapply (sl_strong_extop ???? H22); clear H22; - left; apply ap_symmetric; assumption;] - cases (ap_cotransitive ??? (x ✗ z) H2) (H3 H3);[left;assumption] - right; lapply (Ap≫ ? (sl_op_assoc ????) H3) as H31; - apply (sl_strong_extop ???? H31);] - - |2: - apply apartness_of_excess_base; - - apply (mk_excess_base (sl_carr l)); - [1: apply (λa,b:sl_carr l.a # (a ✗ b)); - |2: unfold; intros 2 (x H); simplify in H; - lapply (Ap≪ ? (sl_op_refl ??) H) as H1; clear H; - apply (ap_coreflexive ?? H1); - |3: unfold; simplify; intros (x y z H1); - cases (ap_cotransitive ??? ((x ✗ z) ✗ y) H1) (H2 H2);[2: - lapply (Ap≪ ? (sl_op_comm ???) H2) as H21; - lapply (Ap≫ ? (sl_op_comm ???) H21) as H22; clear H21 H2; - lapply (sl_strong_extop ???? H22); clear H22; - left; apply ap_symmetric; assumption;] - cases (ap_cotransitive ??? (x ✗ z) H2) (H3 H3);[left;assumption] - right; lapply (Ap≫ ? (sl_op_assoc ????) H3) as H31; - apply (sl_strong_extop ???? H31);] - - |3: apply refl_eq;] -|2,3: intros (x y H); assumption;] -qed. - -record semi_lattice : Type ≝ { - sl_exc:> excess; - sl_meet: sl_exc → sl_exc → sl_exc; - sl_meet_refl: ∀x.sl_meet x x ≈ x; - sl_meet_comm: ∀x,y. sl_meet x y ≈ sl_meet y x; - sl_meet_assoc: ∀x,y,z. sl_meet x (sl_meet y z) ≈ sl_meet (sl_meet x y) z; - sl_strong_extm: ∀x.strong_ext ? (sl_meet x); - sl_le_to_eqm: ∀x,y.x ≤ y → x ≈ sl_meet x y; - sl_lem: ∀x,y.(sl_meet x y) ≤ y -}. - -interpretation "semi lattice meet" 'and a b = (cic:/matita/lattice/sl_meet.con _ a b). - -lemma sl_feq_ml: ∀ml:semi_lattice.∀a,b,c:ml. a ≈ b → (c ∧ a) ≈ (c ∧ b). -intros (l a b c H); unfold eq in H ⊢ %; unfold Not in H ⊢ %; -intro H1; apply H; clear H; apply (sl_strong_extm ???? H1); -qed. - -lemma sl_feq_mr: ∀ml:semi_lattice.∀a,b,c:ml. a ≈ b → (a ∧ c) ≈ (b ∧ c). -intros (l a b c H); -apply (Eq≈ ? (sl_meet_comm ???)); apply (Eq≈ ?? (sl_meet_comm ???)); -apply sl_feq_ml; assumption; -qed. - - -(* -lemma semi_lattice_of_semi_lattice_base: semi_lattice_base → semi_lattice. -intro slb; apply (mk_semi_lattice (excess_of_semi_lattice_base slb)); -[1: apply (sl_op slb); -|2: intro x; apply (eq_trans (excess_of_semi_lattice_base slb)); [2: - apply (sl_op_refl slb);|1:skip] (sl_op slb x x)); ? (sl_op_refl slb x)); - - unfold excess_of_semi_lattice_base; simplify; - intro H; elim H; - [ - - - lapply (ap_rewl (excess_of_semi_lattice_base slb) x ? (sl_op slb x x) - (eq_sym (excess_of_semi_lattice_base slb) ?? (sl_op_refl slb x)) t); - change in x with (sl_carr slb); - apply (Ap≪ (x ✗ x)); (sl_op_refl slb x)); - -whd in H; elim H; clear H; - [ apply (ap_coreflexive (excess_of_semi_lattice_base slb) (x ✗ x) t); - -prelattice (excess_of_directed l_)); [apply (sl_op l_);] -unfold excess_of_directed; try unfold apart_of_excess; simplify; -unfold excl; simplify; -[intro x; intro H; elim H; clear H; - [apply (sl_op_refl l_ x); - lapply (Ap≫ ? (sl_op_comm ???) t) as H; clear t; - lapply (sl_strong_extop l_ ??? H); apply ap_symmetric; assumption - | lapply (Ap≪ ? (sl_op_refl ?x) t) as H; clear t; - lapply (sl_strong_extop l_ ??? H); apply (sl_op_refl l_ x); - apply ap_symmetric; assumption] -|intros 3 (x y H); cases H (H1 H2); clear H; - [lapply (Ap≪ ? (sl_op_refl ? (sl_op l_ x y)) H1) as H; clear H1; - lapply (sl_strong_extop l_ ??? H) as H1; clear H; - lapply (Ap≪ ? (sl_op_comm ???) H1); apply (ap_coreflexive ?? Hletin); - |lapply (Ap≪ ? (sl_op_refl ? (sl_op l_ y x)) H2) as H; clear H2; - lapply (sl_strong_extop l_ ??? H) as H1; clear H; - lapply (Ap≪ ? (sl_op_comm ???) H1);apply (ap_coreflexive ?? Hletin);] -|intros 4 (x y z H); cases H (H1 H2); clear H; - [lapply (Ap≪ ? (sl_op_refl ? (sl_op l_ x (sl_op l_ y z))) H1) as H; clear H1; - lapply (sl_strong_extop l_ ??? H) as H1; clear H; - lapply (Ap≪ ? (eq_sym ??? (sl_op_assoc ?x y z)) H1) as H; clear H1; - apply (ap_coreflexive ?? H); - |lapply (Ap≪ ? (sl_op_refl ? (sl_op l_ (sl_op l_ x y) z)) H2) as H; clear H2; - lapply (sl_strong_extop l_ ??? H) as H1; clear H; - lapply (Ap≪ ? (sl_op_assoc ?x y z) H1) as H; clear H1; - apply (ap_coreflexive ?? H);] -|intros (x y z H); elim H (H1 H1); clear H; - lapply (Ap≪ ? (sl_op_refl ??) H1) as H; clear H1; - lapply (sl_strong_extop l_ ??? H) as H1; clear H; - lapply (sl_strong_extop l_ ??? H1) as H; clear H1; - cases (ap_cotransitive ??? (sl_op l_ y z) H);[left|right|right|left] try assumption; - [apply ap_symmetric;apply (Ap≪ ? (sl_op_comm ???)); - |apply (Ap≫ ? (sl_op_comm ???)); - |apply ap_symmetric;] assumption; -|intros 4 (x y H H1); apply H; clear H; elim H1 (H H); - lapply (Ap≪ ? (sl_op_refl ??) H) as H1; clear H; - lapply (sl_strong_extop l_ ??? H1) as H; clear H1;[2: apply ap_symmetric] - assumption -|intros 3 (x y H); - cut (sl_op l_ x y ≈ sl_op l_ x (sl_op l_ y y)) as H1;[2: - intro; lapply (sl_strong_extop ???? a); apply (sl_op_refl l_ y); - apply ap_symmetric; assumption;] - lapply (Ap≪ ? (eq_sym ??? H1) H); apply (sl_op_assoc l_ x y y); - assumption; ] -qed. -*) - -(* ED(≰,≱) → EB(≰') → ED(≰',≱') *) -lemma subst_excess_base: excess_dual → excess_base → excess_dual. -intros; apply (mk_excess_dual_smart e1); -qed. - -(* E_(ED(≰,≱),AP(#),c ED = c AP) → ED' → c DE' = c E_ → E_(ED',#,p) *) -lemma subst_dual_excess: ∀e:excess_.∀e1:excess_dual.exc_carr e = exc_carr e1 → excess_. -intros (e e1 p); apply (mk_excess_ e1 e); cases p; reflexivity; -qed. - -(* E(E_,H1,H2) → E_' → H1' → H2' → E(E_',H1',H2') *) -alias symbol "nleq" = "Excess excess_". -lemma subst_excess_: ∀e:excess. ∀e1:excess_. - (∀y,x:e1. y # x → y ≰ x ∨ x ≰ y) → - (∀y,x:e1.y ≰ x ∨ x ≰ y → y # x) → - excess. -intros (e e1 H1 H2); apply (mk_excess e1 H1 H2); -qed. - -definition hole ≝ λT:Type.λx:T.x. - -notation < "\ldots" non associative with precedence 50 for @{'hole}. -interpretation "hole" 'hole = (cic:/matita/lattice/hole.con _ _). - -(* SL(E,M,H2-5(#),H67(≰)) → E' → c E = c E' → H67'(≰') → SL(E,M,p2-5,H67') *) -lemma subst_excess: - ∀l:semi_lattice. - ∀e:excess. - ∀p:exc_ap l = exc_ap e. - (∀x,y:e.(le (exc_dual_base e)) x y → x ≈ (?(sl_meet l)) x y) → - (∀x,y:e.(le (exc_dual_base e)) ((?(sl_meet l)) x y) y) → - semi_lattice. -[1,2:intro M; - change with ((λx.ap_carr x) e -> (λx.ap_carr x) e -> (λx.ap_carr x) e); - cases p; apply M; -|intros (l e p H1 H2); - apply (mk_semi_lattice e); - [ change with ((λx.ap_carr x) e -> (λx.ap_carr x) e -> (λx.ap_carr x) e); - cases p; simplify; apply (sl_meet l); - |2: change in ⊢ (% → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_meet_refl; - |3: change in ⊢ (% → % → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_meet_comm; - |4: change in ⊢ (% → % → % → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_meet_assoc; - |5: change in ⊢ (% → ?) with ((λx.ap_carr x) e); cases p; simplify; apply sl_strong_extm; - |6: clear H2; apply hole; apply H1; - |7: clear H1; apply hole; apply H2;]] -qed. - -lemma excess_of_excess_base: excess_base → excess. -intro eb; -apply mk_excess; - [apply (mk_excess_ (mk_excess_dual_smart eb)); - [apply (apartness_of_excess_base eb); - |reflexivity] - |2,3: intros; assumption] -qed. - -lemma subst_excess_preserves_aprtness: - ∀l:semi_lattice. - ∀e:excess. - ∀p,H1,H2. - exc_ap l = exc_ap (subst_excess l e p H1 H2). -intros; -unfold subst_excess; -simplify; assumption; -qed. - - -lemma subst_excess__preserves_aprtness: - ∀l:excess. - ∀e:excess_base. - ∀p,H1,H2. - exc_ap l = apartness_OF_excess (subst_excess_ l (subst_dual_excess l (subst_excess_base l e) p) H1 H2). -intros 3; (unfold subst_excess_; unfold subst_dual_excess; unfold subst_excess_base; unfold exc_ap; unfold mk_excess_dual_smart; simplify); -(unfold subst_excess_base in p; unfold mk_excess_dual_smart in p; simplify in p); -intros; cases p; -reflexivity; -qed. - -lemma subst_excess_base_in_excess_: - ∀d:excess_. - ∀eb:excess_base. - ∀p:exc_carr d = exc_carr eb. - excess_. -intros (e_ eb); -apply (subst_dual_excess e_); - [apply (subst_excess_base e_ eb); - |assumption] -qed. - -lemma subst_excess_base_in_excess: - ∀d:excess. - ∀eb:excess_base. - ∀p:exc_carr d = exc_carr eb. - (∀y1,x1:eb. (?(ap_apart d)) y1 x1 → y1 ≰ x1 ∨ x1 ≰ y1) → - (∀y2,x2:eb.y2 ≰ x2 ∨ x2 ≰ y2 → (?(ap_apart d)) y2 x2) → - excess. -[1,3,4:apply Type|2,5:intro f; cases p; apply f] -intros (d eb p H1 H2); -apply (subst_excess_ d); - [apply (subst_excess_base_in_excess_ d eb p); - |apply hole; clear H2; - change in ⊢ (%→%→?) with (exc_carr eb); - change in ⊢ (?→?→?→? (? % ? ?) (? % ? ?)) with eb; intros (y x H3); - apply H1; generalize in match H3; - unfold ap_apart; unfold subst_excess_base_in_excess_; - unfold subst_dual_excess; simplify; - generalize in match x; - generalize in match y; - cases p; simplify; intros; assumption; - |apply hole; clear H1; - change in ⊢ (%→%→?) with (exc_carr eb); - change in ⊢ (?→?→? (? % ? ?) (? % ? ?)→?) with eb; intros (y x H3); - unfold ap_apart; unfold subst_excess_base_in_excess_; - unfold subst_dual_excess; simplify; generalize in match (H2 ?? H3); - generalize in match x; generalize in match y; cases p; - intros; assumption;] -qed. - -lemma tech1: ∀e:excess. - ∀eb:excess_base. - ∀p,H1,H2. - exc_ap e = exc_ap_ (subst_excess_base_in_excess e eb p H1 H2). -intros (e eb p H1 H2); -unfold subst_excess_base_in_excess; -unfold subst_excess_; simplify; -unfold subst_excess_base_in_excess_; -unfold subst_dual_excess; simplify; reflexivity; -qed. - -lemma tech2: - ∀e:excess_.∀eb.∀p. - exc_ap e = exc_ap (mk_excess_ (subst_excess_base e eb) (exc_ap e) p). -intros (e eb p);unfold exc_ap; simplify; cases p; simplify; reflexivity; -qed. - -(* -lemma eq_fap: - ∀a1,b1,a2,b2,a3,b3,a4,b4,a5,b5. - a1=b1 → a2=b2 → a3=b3 → a4=b4 → a5=b5 → mk_apartness a1 a2 a3 a4 a5 = mk_apartness b1 b2 b3 b4 b5. -intros; cases H; cases H1; cases H2; cases H3; cases H4; reflexivity; -qed. -*) - -lemma subst_excess_base_in_excess_preserves_apartness: - ∀e:excess. - ∀eb:excess_base. - ∀H,H1,H2. - apartness_OF_excess e = - apartness_OF_excess (subst_excess_base_in_excess e eb H H1 H2). -intros (e eb p H1 H2); -unfold subst_excess_base_in_excess; -unfold subst_excess_; unfold subst_excess_base_in_excess_; -unfold subst_dual_excess; unfold apartness_OF_excess; -simplify in ⊢ (? ? ? (? %)); -rewrite < (tech2 e eb ); -reflexivity; -qed. - - - -alias symbol "nleq" = "Excess base excess". -lemma subst_excess_base_in_semi_lattice: - ∀sl:semi_lattice. - ∀eb:excess_base. - ∀p:exc_carr sl = exc_carr eb. - (∀y1,x1:eb. (?(ap_apart sl)) y1 x1 → y1 ≰ x1 ∨ x1 ≰ y1) → - (∀y2,x2:eb.y2 ≰ x2 ∨ x2 ≰ y2 → (?(ap_apart sl)) y2 x2) → - (∀x3,y3:eb.(le eb) x3 y3 → (?(eq sl)) x3 ((?(sl_meet sl)) x3 y3)) → - (∀x4,y4:eb.(le eb) ((?(sl_meet sl)) x4 y4) y4) → - semi_lattice. -[2:apply Prop|3,7,9,10:apply Type|4:apply (exc_carr eb)|1,5,6,8,11:intro f; cases p; apply f;] -intros (sl eb H H1 H2 H3 H4); -apply (subst_excess sl); - [apply (subst_excess_base_in_excess sl eb H H1 H2); - |apply subst_excess_base_in_excess_preserves_apartness; - |change in ⊢ (%→%→?) with ((λx.ap_carr x) (subst_excess_base_in_excess (sl_exc sl) eb H H1 H2)); simplify; - intros 3 (x y LE); clear H3 LE; - generalize in match x as x; generalize in match y as y; - generalize in match H1 as H1;generalize in match H2 as H2; - clear x y H1 H2 H4; STOP - - apply (match H return λr:Type.λm:Type_OF_semi_lattice sl=r. - ∀H2:(Πy2:exc_carr eb - .Πx2:exc_carr eb - .Or (exc_excess eb y2 x2) (exc_excess eb x2 y2) - →match H -  in eq -  return  - λright_1:Type - .(λmatched:eq Type (Type_OF_semi_lattice sl) right_1 - .right_1→right_1→Type) -  with  - [refl_eq⇒ap_apart (apartness_OF_semi_lattice sl)] y2 x2) -.∀H1:Πy1:exc_carr eb - .Πx1:exc_carr eb - .match H -  in eq -  return  - λright_1:Type - .(λmatched:eq Type (Type_OF_semi_lattice sl) right_1 - .right_1→right_1→Type) -  with  - [refl_eq⇒ap_apart (apartness_OF_semi_lattice sl)] y1 x1 - →Or (exc_excess eb y1 x1) (exc_excess eb x1 y1) - .∀y:ap_carr - (apartness_OF_excess (subst_excess_base_in_excess (sl_exc sl) eb H H1 H2)) - .∀x:ap_carr - (apartness_OF_excess - (subst_excess_base_in_excess (sl_exc sl) eb H H1 H2)) - .eq - (apartness_OF_excess (subst_excess_base_in_excess (sl_exc sl) eb H H1 H2)) x - (match  - subst_excess_base_in_excess_preserves_apartness (sl_exc sl) eb H H1 H2 -  in eq -  return  - λright_1:apartness - .(λmatched:eq apartness (apartness_OF_semi_lattice sl) right_1 - .ap_carr right_1→ap_carr right_1→ap_carr right_1) -  with  - [refl_eq⇒sl_meet sl] x y) - - with [ refl_eq ⇒ ?]); - - - cases (subst_excess_base_in_excess_preserves_apartness sl eb H H1 H2); - cases H; - cases (subst_excess_base_in_excess_preserves_apartness (sl_exc sl) eb H H1 H2); simplify; - change in x:(%) with (exc_carr eb); - change in y:(%) with (exc_carr eb); - generalize in match OK; generalize in match x as x; generalize in match y as y; - cases H; simplify; (* funge, ma devo fare 2 rewrite in un colpo solo *) - *) - |cases FALSE; - ] -qed. - -record lattice_ : Type ≝ { - latt_mcarr:> semi_lattice; - latt_jcarr_: semi_lattice; - W1:?; W2:?; W3:?; W4:?; W5:?; - latt_with1: latt_jcarr_ = subst_excess_base_in_semi_lattice latt_jcarr_ - (excess_base_OF_semi_lattice latt_mcarr) W1 W2 W3 W4 W5 -}. - -lemma latt_jcarr : lattice_ → semi_lattice. -intro l; apply (subst_excess_base_in_semi_lattice (latt_jcarr_ l) (excess_base_OF_semi_lattice (latt_mcarr l)) (W1 l) (W2 l) (W3 l) (W4 l) (W5 l)); -qed. - -coercion cic:/matita/lattice/latt_jcarr.con. - -interpretation "Lattice meet" 'and a b = - (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_mcarr.con _) a b). - -interpretation "Lattice join" 'or a b = - (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_jcarr.con _) a b). - -record lattice : Type ≝ { - latt_carr:> lattice_; - absorbjm: ∀f,g:latt_carr. (f ∨ (f ∧ g)) ≈ f; - absorbmj: ∀f,g:latt_carr. (f ∧ (f ∨ g)) ≈ f -}. - -notation "'meet'" non associative with precedence 50 for @{'meet}. -notation "'meet_refl'" non associative with precedence 50 for @{'meet_refl}. -notation "'meet_comm'" non associative with precedence 50 for @{'meet_comm}. -notation "'meet_assoc'" non associative with precedence 50 for @{'meet_assoc}. -notation "'strong_extm'" non associative with precedence 50 for @{'strong_extm}. -notation "'le_to_eqm'" non associative with precedence 50 for @{'le_to_eqm}. -notation "'lem'" non associative with precedence 50 for @{'lem}. -notation "'join'" non associative with precedence 50 for @{'join}. -notation "'join_refl'" non associative with precedence 50 for @{'join_refl}. -notation "'join_comm'" non associative with precedence 50 for @{'join_comm}. -notation "'join_assoc'" non associative with precedence 50 for @{'join_assoc}. -notation "'strong_extj'" non associative with precedence 50 for @{'strong_extj}. -notation "'le_to_eqj'" non associative with precedence 50 for @{'le_to_eqj}. -notation "'lej'" non associative with precedence 50 for @{'lej}. - -interpretation "Lattice meet" 'meet = (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_mcarr.con _)). -interpretation "Lattice meet_refl" 'meet_refl = (cic:/matita/lattice/sl_meet_refl.con (cic:/matita/lattice/latt_mcarr.con _)). -interpretation "Lattice meet_comm" 'meet_comm = (cic:/matita/lattice/sl_meet_comm.con (cic:/matita/lattice/latt_mcarr.con _)). -interpretation "Lattice meet_assoc" 'meet_assoc = (cic:/matita/lattice/sl_meet_assoc.con (cic:/matita/lattice/latt_mcarr.con _)). -interpretation "Lattice strong_extm" 'strong_extm = (cic:/matita/lattice/sl_strong_extm.con (cic:/matita/lattice/latt_mcarr.con _)). -interpretation "Lattice le_to_eqm" 'le_to_eqm = (cic:/matita/lattice/sl_le_to_eqm.con (cic:/matita/lattice/latt_mcarr.con _)). -interpretation "Lattice lem" 'lem = (cic:/matita/lattice/sl_lem.con (cic:/matita/lattice/latt_mcarr.con _)). -interpretation "Lattice join" 'join = (cic:/matita/lattice/sl_meet.con (cic:/matita/lattice/latt_jcarr.con _)). -interpretation "Lattice join_refl" 'join_refl = (cic:/matita/lattice/sl_meet_refl.con (cic:/matita/lattice/latt_jcarr.con _)). -interpretation "Lattice join_comm" 'join_comm = (cic:/matita/lattice/sl_meet_comm.con (cic:/matita/lattice/latt_jcarr.con _)). -interpretation "Lattice join_assoc" 'join_assoc = (cic:/matita/lattice/sl_meet_assoc.con (cic:/matita/lattice/latt_jcarr.con _)). -interpretation "Lattice strong_extm" 'strong_extj = (cic:/matita/lattice/sl_strong_extm.con (cic:/matita/lattice/latt_jcarr.con _)). -interpretation "Lattice le_to_eqj" 'le_to_eqj = (cic:/matita/lattice/sl_le_to_eqm.con (cic:/matita/lattice/latt_jcarr.con _)). -interpretation "Lattice lej" 'lej = (cic:/matita/lattice/sl_lem.con (cic:/matita/lattice/latt_jcarr.con _)). - -notation "'feq_jl'" non associative with precedence 50 for @{'feq_jl}. -notation "'feq_jr'" non associative with precedence 50 for @{'feq_jr}. -notation "'feq_ml'" non associative with precedence 50 for @{'feq_ml}. -notation "'feq_mr'" non associative with precedence 50 for @{'feq_mr}. -interpretation "Lattice feq_jl" 'feq_jl = (cic:/matita/lattice/sl_feq_ml.con (cic:/matita/lattice/latt_jcarr.con _)). -interpretation "Lattice feq_jr" 'feq_jr = (cic:/matita/lattice/sl_feq_mr.con (cic:/matita/lattice/latt_jcarr.con _)). -interpretation "Lattice feq_ml" 'feq_ml = (cic:/matita/lattice/sl_feq_ml.con (cic:/matita/lattice/latt_mcarr.con _)). -interpretation "Lattice feq_mr" 'feq_mr = (cic:/matita/lattice/sl_feq_mr.con (cic:/matita/lattice/latt_mcarr.con _)). - - -interpretation "Lattive meet le" 'leq a b = - (cic:/matita/excess/le.con (cic:/matita/lattice/excess_OF_lattice1.con _) a b). - -interpretation "Lattive join le (aka ge)" 'geq a b = - (cic:/matita/excess/le.con (cic:/matita/lattice/excess_OF_lattice.con _) a b). - -(* these coercions help unification, handmaking a bit of conversion - over an open term -*) -lemma le_to_ge: ∀l:lattice.∀a,b:l.a ≤ b → b ≥ a. -intros(l a b H); apply H; -qed. - -lemma ge_to_le: ∀l:lattice.∀a,b:l.b ≥ a → a ≤ b. -intros(l a b H); apply H; -qed. - -coercion cic:/matita/lattice/le_to_ge.con nocomposites. -coercion cic:/matita/lattice/ge_to_le.con nocomposites. \ No newline at end of file diff --git a/helm/software/matita/contribs/dama/dama/limit.ma b/helm/software/matita/contribs/dama/dama/limit.ma deleted file mode 100644 index 1250511e8..000000000 --- a/helm/software/matita/contribs/dama/dama/limit.ma +++ /dev/null @@ -1,67 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -include "infsup.ma". - -definition shift ≝ λT:Type.λs:sequence T.λk:nat.λn.s (n+k). - -(* 3.28 *) -definition limsup ≝ - λE:excess.λxn:sequence E.λx:E.∃alpha:sequence E. - (∀k.(alpha k) is_strong_sup (shift ? xn k) in E) ∧ - x is_strong_inf alpha in E. - -notation < "x \nbsp 'is_limsup' \nbsp s" non associative with precedence 50 for @{'limsup $_ $s $x}. -notation < "x \nbsp 'is_liminf' \nbsp s" non associative with precedence 50 for @{'liminf $_ $s $x}. -notation > "x 'is_limsup' s 'in' e" non associative with precedence 50 for @{'limsup $e $s $x}. -notation > "x 'is_liminf' s 'in' e" non associative with precedence 50 for @{'liminf $e $s $x}. - -interpretation "Excess limsup" 'limsup e s x = (cic:/matita/limit/limsup.con e s x). -interpretation "Excess liminf" 'liminf e s x = (cic:/matita/limit/limsup.con (cic:/matita/excess/dual_exc.con e) s x). - -(* 3.29 *) -definition lim ≝ - λE:excess.λxn:sequence E.λx:E. x is_limsup xn in E ∧ x is_liminf xn in E. - -notation < "x \nbsp 'is_lim' \nbsp s" non associative with precedence 50 for @{'lim $_ $s $x}. -notation > "x 'is_lim' s 'in' e" non associative with precedence 50 for @{'lim $e $s $x}. -interpretation "Excess lim" 'lim e s x = (cic:/matita/limit/lim.con e s x). - -lemma sup_decreasing: - ∀E:excess.∀xn:sequence E. - ∀alpha:sequence E. (∀k.(alpha k) is_strong_sup xn in E) → - alpha is_decreasing in E. -intros (E xn alpha H); unfold strong_sup in H; unfold upper_bound in H; unfold; -intro r; -elim (H r) (H1r H2r); -elim (H (S r)) (H1sr H2sr); clear H H2r H1sr; -intro e; cases (H2sr (alpha r) e) (w Hw); clear e H2sr; -cases (H1r w Hw); -qed. - -include "tend.ma". -include "metric_lattice.ma". - -(* 3.30 *) -lemma lim_tends: - ∀R.∀ml:mlattice R.∀xn:sequence ml.∀x:ml. - x is_lim xn in ml → xn ⇝ x. -intros (R ml xn x Hl); unfold lim in Hl; unfold limsup in Hl; -cases Hl (e1 e2); cases e1 (an Han); cases e2 (bn Hbn); clear Hl e1 e2; -cases Han (SSan SIxan); cases Hbn (SSbn SIxbn); clear Han Hbn; -cases SIxan (LBxan Hxg); cases SIxbn (UPxbn Hxl); clear SIxbn SIxan; -change in UPxbn:(%) with (x is_lower_bound bn in ml); -unfold upper_bound in UPxbn LBxan; change -intros (e He); -(* 2.6 OC *) diff --git a/helm/software/matita/contribs/dama/dama/metric_lattice.ma b/helm/software/matita/contribs/dama/dama/metric_lattice.ma deleted file mode 100644 index 010360757..000000000 --- a/helm/software/matita/contribs/dama/dama/metric_lattice.ma +++ /dev/null @@ -1,117 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -include "metric_space.ma". -include "lattice.ma". - -record mlattice_ (R : todgroup) : Type ≝ { - ml_mspace_: metric_space R; - ml_lattice:> lattice; - ml_with: ms_carr ? ml_mspace_ = Type_OF_lattice ml_lattice -}. - -lemma ml_mspace: ∀R.mlattice_ R → metric_space R. -intros (R ml); apply (mk_metric_space R (Type_OF_mlattice_ ? ml)); -unfold Type_OF_mlattice_; cases (ml_with ? ml); simplify; -[apply (metric ? (ml_mspace_ ? ml));|apply (mpositive ? (ml_mspace_ ? ml)); -|apply (mreflexive ? (ml_mspace_ ? ml));|apply (msymmetric ? (ml_mspace_ ? ml)); -|apply (mtineq ? (ml_mspace_ ? ml))] -qed. - -coercion cic:/matita/metric_lattice/ml_mspace.con. - -alias symbol "plus" = "Abelian group plus". -alias symbol "leq" = "Excess less or equal than". -record mlattice (R : todgroup) : Type ≝ { - ml_carr :> mlattice_ R; - ml_prop1: ∀a,b:ml_carr. 0 < δ a b → a # b; - ml_prop2: ∀a,b,c:ml_carr. δ (a∨b) (a∨c) + δ (a∧b) (a∧c) ≤ (δ b c) -}. - -interpretation "Metric lattice leq" 'leq a b = - (cic:/matita/excess/le.con (cic:/matita/metric_lattice/excess_OF_mlattice1.con _ _) a b). -interpretation "Metric lattice geq" 'geq a b = - (cic:/matita/excess/le.con (cic:/matita/metric_lattice/excess_OF_mlattice.con _ _) a b). - -lemma eq_to_ndlt0: ∀R.∀ml:mlattice R.∀a,b:ml. a ≈ b → ¬ 0 < δ a b. -intros (R ml a b E); intro H; apply E; apply ml_prop1; -assumption; -qed. - -lemma eq_to_dzero: ∀R.∀ml:mlattice R.∀x,y:ml.x ≈ y → δ x y ≈ 0. -intros (R ml x y H); intro H1; apply H; clear H; -apply ml_prop1; split [apply mpositive] apply ap_symmetric; -assumption; -qed. - -lemma meq_l: ∀R.∀ml:mlattice R.∀x,y,z:ml. x≈z → δx y ≈ δz y. -intros (R ml x y z); apply le_le_eq; -[ apply (le_transitive ???? (mtineq ???y z)); - apply (le_rewl ??? (0+δz y) (eq_to_dzero ???? H)); - apply (le_rewl ??? (δz y) (zero_neutral ??)); apply le_reflexive; -| apply (le_transitive ???? (mtineq ???y x)); - apply (le_rewl ??? (0+δx y) (eq_to_dzero ??z x H)); - apply (le_rewl ??? (δx y) (zero_neutral ??)); apply le_reflexive;] -qed. - -(* 3.3 *) -lemma meq_r: ∀R.∀ml:mlattice R.∀x,y,z:ml. x≈z → δy x ≈ δy z. -intros; apply (eq_trans ???? (msymmetric ??y x)); -apply (eq_trans ????? (msymmetric ??z y)); apply meq_l; assumption; -qed. - -lemma dap_to_lt: ∀R.∀ml:mlattice R.∀x,y:ml. δ x y # 0 → 0 < δ x y. -intros; split [apply mpositive] apply ap_symmetric; assumption; -qed. - -lemma dap_to_ap: ∀R.∀ml:mlattice R.∀x,y:ml. δ x y # 0 → x # y. -intros (R ml x y H); apply ml_prop1; split; [apply mpositive;] -apply ap_symmetric; assumption; -qed. - -(* 3.11 *) -lemma le_mtri: - ∀R.∀ml:mlattice R.∀x,y,z:ml. x ≤ y → y ≤ z → δ x z ≈ δ x y + δ y z. -intros (R ml x y z Lxy Lyz); apply le_le_eq; [apply mtineq] -apply (le_transitive ????? (ml_prop2 ?? (y) ??)); -cut ( δx y+ δy z ≈ δ(y∨x) (y∨z)+ δ(y∧x) (y∧z)); [ - apply (le_rewr ??? (δx y+ δy z)); [assumption] apply le_reflexive] -lapply (le_to_eqm y x Lxy) as Dxm; lapply (le_to_eqm z y Lyz) as Dym; -lapply (le_to_eqj x y Lxy) as Dxj; lapply (le_to_eqj y z Lyz) as Dyj; clear Lxy Lyz; - STOP -apply (Eq≈ (δ(x∧y) y + δy z) (meq_l ????? Dxm)); -apply (Eq≈ (δ(x∧y) (y∧z) + δy z) (meq_r ????? Dym)); -apply (Eq≈ (δ(x∧y) (y∧z) + δ(y∨x) z));[ - apply feq_plusl; apply meq_l; clear Dyj Dxm Dym; assumption] -apply (Eq≈ (δ(x∧y) (y∧z) + δ(y∨x) (z∨y))); [ - apply (feq_plusl ? (δ(x∧y) (y∧z)) ?? (meq_r ??? (y∨x) ? Dyj));] -apply (Eq≈ ? (plus_comm ???)); -apply (Eq≈ (δ(y∨x) (y∨z)+ δ(x∧y) (y∧z)));[ - apply feq_plusr; apply meq_r; apply (join_comm ??);] -apply feq_plusl; -apply (Eq≈ (δ(y∧x) (y∧z)) (meq_l ????? (meet_comm ??))); -apply eq_reflexive; -qed. - - -(* 3.17 conclusione: δ x y ≈ 0 *) -(* 3.20 conclusione: δ x y ≈ 0 *) -(* 3.21 sup forte - strong_sup x ≝ ∀n. s n ≤ x ∧ ∀y x ≰ y → ∃n. s n ≰ y - strong_sup_zoli x ≝ ∀n. s n ≤ x ∧ ∄y. y#x ∧ y ≤ x -*) -(* 3.22 sup debole (più piccolo dei maggioranti) *) -(* 3.23 conclusion: δ x sup(...) ≈ 0 *) -(* 3.25 vero nel reticolo e basta (niente δ) *) -(* 3.36 conclusion: δ x y ≈ 0 *) diff --git a/helm/software/matita/contribs/dama/dama/metric_space.ma b/helm/software/matita/contribs/dama/dama/metric_space.ma deleted file mode 100644 index 2266fe9e9..000000000 --- a/helm/software/matita/contribs/dama/dama/metric_space.ma +++ /dev/null @@ -1,46 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -include "ordered_divisible_group.ma". - -record metric_space (R: todgroup) : Type ≝ { - ms_carr :> Type; - metric: ms_carr → ms_carr → R; - mpositive: ∀a,b:ms_carr. 0 ≤ metric a b; - mreflexive: ∀a. metric a a ≈ 0; - msymmetric: ∀a,b. metric a b ≈ metric b a; - mtineq: ∀a,b,c:ms_carr. metric a b ≤ metric a c + metric c b -}. - -notation < "\nbsp \delta a \nbsp b" non associative with precedence 80 for @{ 'delta2 $a $b}. -interpretation "metric" 'delta2 a b = (cic:/matita/metric_space/metric.con _ _ a b). -notation "\delta" non associative with precedence 80 for @{ 'delta }. -interpretation "metric" 'delta = (cic:/matita/metric_space/metric.con _ _). - -lemma apart_of_metric_space: ∀R.metric_space R → apartness. -intros (R ms); apply (mk_apartness ? (λa,b:ms.0 < δ a b)); unfold; -[1: intros 2 (x H); cases H (H1 H2); clear H; - lapply (Ap≫ ? (eq_sym ??? (mreflexive ??x)) H2); - apply (ap_coreflexive R 0); assumption; -|2: intros (x y H); cases H; split; - [1: apply (Le≫ ? (msymmetric ????)); assumption - |2: apply (Ap≫ ? (msymmetric ????)); assumption] -|3: simplify; intros (x y z H); elim H (LExy Axy); - lapply (mtineq ?? x y z) as H1; elim (ap2exc ??? Axy) (H2 H2); [cases (LExy H2)] - clear LExy; lapply (lt_le_transitive ???? H H1) as LT0; - apply (lt0plus_orlt ????? LT0); apply mpositive;] -qed. - -lemma ap2delta: ∀R.∀m:metric_space R.∀x,y:m.ap_apart (apart_of_metric_space ? m) x y → 0 < δ x y. -intros 2 (R m); cases m 0; simplify; intros; assumption; qed. diff --git a/helm/software/matita/contribs/dama/dama/ordered_divisible_group.ma b/helm/software/matita/contribs/dama/dama/ordered_divisible_group.ma deleted file mode 100644 index a9dfc4a58..000000000 --- a/helm/software/matita/contribs/dama/dama/ordered_divisible_group.ma +++ /dev/null @@ -1,75 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - - - -include "nat/orders.ma". -include "nat/times.ma". -include "ordered_group.ma". -include "divisible_group.ma". - -record todgroup : Type ≝ { - todg_order:> togroup; - todg_division_: dgroup; - todg_with_: dg_carr todg_division_ = og_abelian_group todg_order -}. - -lemma todg_division: todgroup → dgroup. -intro G; apply (mk_dgroup G); unfold abelian_group_OF_todgroup; -cases (todg_with_ G); exact (dg_prop (todg_division_ G)); -qed. - -coercion cic:/matita/ordered_divisible_group/todg_division.con. - -lemma mul_ge: ∀G:todgroup.∀x:G.∀n.0 ≤ x → 0 ≤ n * x. -intros (G x n); elim n; simplify; [apply le_reflexive] -apply (le_transitive ???? H1); -apply (Le≪ (0+(n1*x)) (zero_neutral ??)); -apply fle_plusr; assumption; -qed. - -lemma lt_ltmul: ∀G:todgroup.∀x,y:G.∀n. x < y → S n * x < S n * y. -intros; elim n; [simplify; apply flt_plusr; assumption] -simplify; apply (ltplus); [assumption] assumption; -qed. - -lemma ltmul_lt: ∀G:todgroup.∀x,y:G.∀n. S n * x < S n * y → x < y. -intros 4; elim n; [apply (plus_cancr_lt ??? 0); assumption] -simplify in l; cases (ltplus_orlt ????? l); [assumption] -apply f; assumption; -qed. - -lemma divide_preserves_lt: ∀G:todgroup.∀e:G.∀n.0 sym_plus; simplify; apply (Lt≪ (0+(y+n*y))); [ - apply eq_sym; apply zero_neutral] - apply flt_plusr; assumption;] -apply (lt_transitive ???? l); rewrite > sym_plus; simplify; -rewrite > (sym_plus n); simplify; repeat apply flt_plusl; -apply (Lt≪ (0+(n1+n)*y)); [apply eq_sym; apply zero_neutral] -apply flt_plusr; assumption; -qed. - diff --git a/helm/software/matita/contribs/dama/dama/ordered_group.ma b/helm/software/matita/contribs/dama/dama/ordered_group.ma deleted file mode 100644 index 7d25273aa..000000000 --- a/helm/software/matita/contribs/dama/dama/ordered_group.ma +++ /dev/null @@ -1,328 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - - - -include "group.ma". - -record pogroup_ : Type ≝ { - og_abelian_group_: abelian_group; - og_excess:> excess; - og_with: carr og_abelian_group_ = exc_ap og_excess -}. - -lemma og_abelian_group: pogroup_ → abelian_group. -intro G; apply (mk_abelian_group G); unfold apartness_OF_pogroup_; -cases (og_with G); simplify; -[apply (plus (og_abelian_group_ G));|apply zero;|apply opp -|apply plus_assoc|apply plus_comm|apply zero_neutral|apply opp_inverse|apply plus_strong_ext] -qed. - -coercion cic:/matita/ordered_group/og_abelian_group.con. - -record pogroup : Type ≝ { - og_carr:> pogroup_; - plus_cancr_exc: ∀f,g,h:og_carr. f+h ≰ g+h → f ≰ g -}. - -lemma fexc_plusr: - ∀G:pogroup.∀x,y,z:G. x ≰ y → x+z ≰ y + z. -intros 5 (G x y z L); apply (plus_cancr_exc ??? (-z)); -apply (Ex≪ (x + (z + -z)) (plus_assoc ????)); -apply (Ex≪ (x + (-z + z)) (plus_comm ??z)); -apply (Ex≪ (x+0) (opp_inverse ??)); -apply (Ex≪ (0+x) (plus_comm ???)); -apply (Ex≪ x (zero_neutral ??)); -apply (Ex≫ (y + (z + -z)) (plus_assoc ????)); -apply (Ex≫ (y + (-z + z)) (plus_comm ??z)); -apply (Ex≫ (y+0) (opp_inverse ??)); -apply (Ex≫ (0+y) (plus_comm ???)); -apply (Ex≫ y (zero_neutral ??) L); -qed. - -coercion cic:/matita/ordered_group/fexc_plusr.con nocomposites. - -lemma plus_cancl_exc: ∀G:pogroup.∀f,g,h:G. h+f ≰ h+g → f ≰ g. -intros 5 (G x y z L); apply (plus_cancr_exc ??? z); -apply (Ex≪ (z+x) (plus_comm ???)); -apply (Ex≫ (z+y) (plus_comm ???) L); -qed. - -lemma fexc_plusl: - ∀G:pogroup.∀x,y,z:G. x ≰ y → z+x ≰ z+y. -intros 5 (G x y z L); apply (plus_cancl_exc ??? (-z)); -apply (Ex≪? (plus_assoc ??z x)); -apply (Ex≫? (plus_assoc ??z y)); -apply (Ex≪ (0+x) (opp_inverse ??)); -apply (Ex≫ (0+y) (opp_inverse ??)); -apply (Ex≪? (zero_neutral ??)); -apply (Ex≫? (zero_neutral ??) L); -qed. - -coercion cic:/matita/ordered_group/fexc_plusl.con nocomposites. - -lemma plus_cancr_le: - ∀G:pogroup.∀x,y,z:G.x+z ≤ y + z → x ≤ y. -intros 5 (G x y z L); -apply (Le≪ (0+x) (zero_neutral ??)); -apply (Le≪ (x+0) (plus_comm ???)); -apply (Le≪ (x+(-z+z)) (opp_inverse ??)); -apply (Le≪ (x+(z+ -z)) (plus_comm ??z)); -apply (Le≪ (x+z+ -z) (plus_assoc ????)); -apply (Le≫ (0+y) (zero_neutral ??)); -apply (Le≫ (y+0) (plus_comm ???)); -apply (Le≫ (y+(-z+z)) (opp_inverse ??)); -apply (Le≫ (y+(z+ -z)) (plus_comm ??z)); -apply (Le≫ (y+z+ -z) (plus_assoc ????)); -intro H; apply L; clear L; apply (plus_cancr_exc ??? (-z) H); -qed. - -lemma fle_plusl: ∀G:pogroup. ∀f,g,h:G. f≤g → h+f≤h+g. -intros (G f g h); -apply (plus_cancr_le ??? (-h)); -apply (Le≪ (f+h+ -h) (plus_comm ? f h)); -apply (Le≪ (f+(h+ -h)) (plus_assoc ????)); -apply (Le≪ (f+(-h+h)) (plus_comm ? h (-h))); -apply (Le≪ (f+0) (opp_inverse ??)); -apply (Le≪ (0+f) (plus_comm ???)); -apply (Le≪ (f) (zero_neutral ??)); -apply (Le≫ (g+h+ -h) (plus_comm ? h ?)); -apply (Le≫ (g+(h+ -h)) (plus_assoc ????)); -apply (Le≫ (g+(-h+h)) (plus_comm ??h)); -apply (Le≫ (g+0) (opp_inverse ??)); -apply (Le≫ (0+g) (plus_comm ???)); -apply (Le≫ (g) (zero_neutral ??) H); -qed. - -lemma fle_plusr: ∀G:pogroup. ∀f,g,h:G. f≤g → f+h≤g+h. -intros (G f g h H); apply (Le≪? (plus_comm ???)); -apply (Le≫? (plus_comm ???)); apply fle_plusl; assumption; -qed. - -lemma plus_cancl_le: - ∀G:pogroup.∀x,y,z:G.z+x ≤ z+y → x ≤ y. -intros 5 (G x y z L); -apply (Le≪ (0+x) (zero_neutral ??)); -apply (Le≪ ((-z+z)+x) (opp_inverse ??)); -apply (Le≪ (-z+(z+x)) (plus_assoc ????)); -apply (Le≫ (0+y) (zero_neutral ??)); -apply (Le≫ ((-z+z)+y) (opp_inverse ??)); -apply (Le≫ (-z+(z+y)) (plus_assoc ????)); -apply (fle_plusl ??? (-z) L); -qed. - -lemma plus_cancl_lt: - ∀G:pogroup.∀x,y,z:G.z+x < z+y → x < y. -intros 5 (G x y z L); elim L (A LE); split; [apply plus_cancl_le; assumption] -apply (plus_cancl_ap ???? LE); -qed. - -lemma plus_cancr_lt: - ∀G:pogroup.∀x,y,z:G.x+z < y+z → x < y. -intros 5 (G x y z L); elim L (A LE); split; [apply plus_cancr_le; assumption] -apply (plus_cancr_ap ???? LE); -qed. - - -lemma exc_opp_x_zero_to_exc_zero_x: - ∀G:pogroup.∀x:G.-x ≰ 0 → 0 ≰ x. -intros (G x H); apply (plus_cancr_exc ??? (-x)); -apply (Ex≫? (plus_comm ???)); -apply (Ex≫? (opp_inverse ??)); -apply (Ex≪? (zero_neutral ??) H); -qed. - -lemma le_zero_x_to_le_opp_x_zero: - ∀G:pogroup.∀x:G.0 ≤ x → -x ≤ 0. -intros (G x Px); apply (plus_cancr_le ??? x); -apply (Le≪ 0 (opp_inverse ??)); -apply (Le≫ x (zero_neutral ??) Px); -qed. - -lemma lt_zero_x_to_lt_opp_x_zero: - ∀G:pogroup.∀x:G.0 < x → -x < 0. -intros (G x Px); apply (plus_cancr_lt ??? x); -apply (Lt≪ 0 (opp_inverse ??)); -apply (Lt≫ x (zero_neutral ??) Px); -qed. - -lemma exc_zero_opp_x_to_exc_x_zero: - ∀G:pogroup.∀x:G. 0 ≰ -x → x ≰ 0. -intros (G x H); apply (plus_cancl_exc ??? (-x)); -apply (Ex≫? (plus_comm ???)); -apply (Ex≪? (opp_inverse ??)); -apply (Ex≫? (zero_neutral ??) H); -qed. - -lemma le_x_zero_to_le_zero_opp_x: - ∀G:pogroup.∀x:G. x ≤ 0 → 0 ≤ -x. -intros (G x Lx0); apply (plus_cancr_le ??? x); -apply (Le≫ 0 (opp_inverse ??)); -apply (Le≪ x (zero_neutral ??)); -assumption; -qed. - -lemma lt_x_zero_to_lt_zero_opp_x: - ∀G:pogroup.∀x:G. x < 0 → 0 < -x. -intros (G x Lx0); apply (plus_cancr_lt ??? x); -apply (Lt≫ 0 (opp_inverse ??)); -apply (Lt≪ x (zero_neutral ??)); -assumption; -qed. - -lemma lt_opp_x_zero_to_lt_zero_x: - ∀G:pogroup.∀x:G. -x < 0 → 0 < x. -intros (G x Lx0); apply (plus_cancr_lt ??? (-x)); -apply (Lt≪ (-x) (zero_neutral ??)); -apply (Lt≫ (-x+x) (plus_comm ???)); -apply (Lt≫ 0 (opp_inverse ??)); -assumption; -qed. - -lemma lt0plus_orlt: - ∀G:pogroup. ∀x,y:G. 0 ≤ x → 0 ≤ y → 0 < x + y → 0 < x ∨ 0 < y. -intros (G x y LEx LEy LT); cases LT (H1 H2); cases (ap_cotransitive ??? y H2); -[right; split; assumption|left;split;[assumption]] -apply (plus_cancr_ap ??? y); apply (Ap≪? (zero_neutral ??)); -assumption; -qed. - -lemma le0plus_le: - ∀G:pogroup.∀a,b,c:G. 0 ≤ b → a + b ≤ c → a ≤ c. -intros (G a b c L H); apply (le_transitive ????? H); -apply (plus_cancl_le ??? (-a)); -apply (Le≪ 0 (opp_inverse ??)); -apply (Le≫ (-a + a + b) (plus_assoc ????)); -apply (Le≫ (0 + b) (opp_inverse ??)); -apply (Le≫ b (zero_neutral ??)); -assumption; -qed. - -lemma le_le0plus: - ∀G:pogroup.∀a,b:G. 0 ≤ a → 0 ≤ b → 0 ≤ a + b. -intros (G a b L1 L2); apply (le_transitive ???? L1); -apply (plus_cancl_le ??? (-a)); -apply (Le≪ 0 (opp_inverse ??)); -apply (Le≫ (-a + a + b) (plus_assoc ????)); -apply (Le≫ (0 + b) (opp_inverse ??)); -apply (Le≫ b (zero_neutral ??)); -assumption; -qed. - -lemma flt_plusl: - ∀G:pogroup.∀x,y,z:G.x < y → z + x < z + y. -intros (G x y z H); cases H; split; [apply fle_plusl; assumption] -apply fap_plusl; assumption; -qed. - -lemma flt_plusr: - ∀G:pogroup.∀x,y,z:G.x < y → x + z < y + z. -intros (G x y z H); cases H; split; [apply fle_plusr; assumption] -apply fap_plusr; assumption; -qed. - - -lemma ltxy_ltyyxx: ∀G:pogroup.∀x,y:G. y < x → y+y < x+x. -intros; apply (lt_transitive ?? (y+x));[2: - apply (Lt≪? (plus_comm ???)); - apply (Lt≫? (plus_comm ???));] -apply flt_plusl;assumption; -qed. - -lemma lew_opp : ∀O:pogroup.∀a,b,c:O.0 ≤ b → a ≤ c → a + -b ≤ c. -intros (O a b c L0 L); -apply (le_transitive ????? L); -apply (plus_cancl_le ??? (-a)); -apply (Le≫ 0 (opp_inverse ??)); -apply (Le≪ (-a+a+-b) (plus_assoc ????)); -apply (Le≪ (0+-b) (opp_inverse ??)); -apply (Le≪ (-b) (zero_neutral ?(-b))); -apply le_zero_x_to_le_opp_x_zero; -assumption; -qed. - -lemma ltw_opp : ∀O:pogroup.∀a,b,c:O.0 < b → a < c → a + -b < c. -intros (O a b c P L); -apply (lt_transitive ????? L); -apply (plus_cancl_lt ??? (-a)); -apply (Lt≫ 0 (opp_inverse ??)); -apply (Lt≪ (-a+a+-b) (plus_assoc ????)); -apply (Lt≪ (0+-b) (opp_inverse ??)); -apply (Lt≪ ? (zero_neutral ??)); -apply lt_zero_x_to_lt_opp_x_zero; -assumption; -qed. - -record togroup : Type ≝ { - tog_carr:> pogroup; - tog_total: ∀x,y:tog_carr.x≰y → y < x -}. - -lemma lexxyy_lexy: ∀G:togroup. ∀x,y:G. x+x ≤ y+y → x ≤ y. -intros (G x y H); intro H1; lapply (tog_total ??? H1) as H2; -lapply (ltxy_ltyyxx ??? H2) as H3; lapply (lt_to_excess ??? H3) as H4; -cases (H H4); -qed. - -lemma eqxxyy_eqxy: ∀G:togroup.∀x,y:G. x + x ≈ y + y → x ≈ y. -intros (G x y H); cases (eq_le_le ??? H); apply le_le_eq; -apply lexxyy_lexy; assumption; -qed. - -lemma applus_orap: ∀G:abelian_group. ∀x,y:G. 0 # x + y → 0 #x ∨ 0#y. -intros; cases (ap_cotransitive ??? y a); [right; assumption] -left; apply (plus_cancr_ap ??? y); apply (Ap≪y (zero_neutral ??)); -assumption; -qed. - -lemma ltplus: ∀G:pogroup.∀a,b,c,d:G. a < b → c < d → a+c < b + d. -intros (G a b c d H1 H2); -lapply (flt_plusr ??? c H1) as H3; -apply (lt_transitive ???? H3); -apply flt_plusl; assumption; -qed. - -lemma excplus_orexc: ∀G:pogroup.∀a,b,c,d:G. a+c ≰ b + d → a ≰ b ∨ c ≰ d. -intros (G a b c d H1 H2); -cases (exc_cotransitive ??? (a + d) H1); [ - right; apply (plus_cancl_exc ??? a); assumption] -left; apply (plus_cancr_exc ??? d); assumption; -qed. - -lemma leplus: ∀G:pogroup.∀a,b,c,d:G. a ≤ b → c ≤ d → a+c ≤ b + d. -intros (G a b c d H1 H2); intro H3; cases (excplus_orexc ????? H3); -[apply H1|apply H2] assumption; -qed. - -lemma leplus_lt_le: ∀G:togroup.∀x,y:G. 0 ≤ x + y → x < 0 → 0 ≤ y. -intros; intro; apply H; lapply (lt_to_excess ??? l); -lapply (tog_total ??? e); -lapply (tog_total ??? Hletin); -lapply (ltplus ????? Hletin2 Hletin1); -apply (Ex≪ (0+0)); [apply eq_sym; apply zero_neutral] -apply lt_to_excess; assumption; -qed. - -lemma ltplus_orlt: ∀G:togroup.∀a,b,c,d:G. a+c < b + d → a < b ∨ c < d. -intros (G a b c d H1 H2); lapply (lt_to_excess ??? H1); -cases (excplus_orexc ????? Hletin); [left|right] apply tog_total; assumption; -qed. - -lemma excplus: ∀G:togroup.∀a,b,c,d:G.a ≰ b → c ≰ d → a + c ≰ b + d. -intros (G a b c d L1 L2); -lapply (fexc_plusr ??? (c) L1) as L3; -elim (exc_cotransitive ??? (b+d) L3); [assumption] -lapply (plus_cancl_exc ???? b1); lapply (tog_total ??? Hletin); -cases Hletin1; cases (H L2); -qed. diff --git a/helm/software/matita/contribs/dama/dama/premetric_lattice.ma b/helm/software/matita/contribs/dama/dama/premetric_lattice.ma deleted file mode 100644 index 6c904055c..000000000 --- a/helm/software/matita/contribs/dama/dama/premetric_lattice.ma +++ /dev/null @@ -1,70 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - - - -include "metric_space.ma". - -record premetric_lattice_ (R : todgroup) : Type ≝ { - pml_carr:> metric_space R; - meet: pml_carr → pml_carr → pml_carr; - join: pml_carr → pml_carr → pml_carr -}. - -interpretation "valued lattice meet" 'and a b = - (cic:/matita/premetric_lattice/meet.con _ _ a b). - -interpretation "valued lattice join" 'or a b = - (cic:/matita/premetric_lattice/join.con _ _ a b). - -record premetric_lattice_props (R : todgroup) (ml : premetric_lattice_ R) : Prop ≝ { - prop1a: ∀a : ml.δ (a ∧ a) a ≈ 0; - prop1b: ∀a : ml.δ (a ∨ a) a ≈ 0; - prop2a: ∀a,b: ml. δ (a ∨ b) (b ∨ a) ≈ 0; - prop2b: ∀a,b: ml. δ (a ∧ b) (b ∧ a) ≈ 0; - prop3a: ∀a,b,c: ml. δ (a ∨ (b ∨ c)) ((a ∨ b) ∨ c) ≈ 0; - prop3b: ∀a,b,c: ml. δ (a ∧ (b ∧ c)) ((a ∧ b) ∧ c) ≈ 0; - prop4a: ∀a,b: ml. δ (a ∨ (a ∧ b)) a ≈ 0; - prop4b: ∀a,b: ml. δ (a ∧ (a ∨ b)) a ≈ 0; - prop5: ∀a,b,c: ml. δ (a ∨ b) (a ∨ c) + δ (a ∧ b) (a ∧ c) ≤ δ b c -}. - -record pmlattice (R : todgroup) : Type ≝ { - carr :> premetric_lattice_ R; - ispremetriclattice:> premetric_lattice_props R carr -}. - -include "lattice.ma". - -lemma lattice_of_pmlattice: ∀R: todgroup. pmlattice R → lattice. -intros (R pml); not ported to duality -apply (mk_lattice (apart_of_metric_space ? pml)); -[apply (join ? pml)|apply (meet ? pml) -|3,4,5,6,7,8,9,10: intros (x y z); whd; intro H; whd in H; cases H (LE AP);] -[apply (prop1b ? pml pml x); |apply (prop1a ? pml pml x); -|apply (prop2a ? pml pml x y); |apply (prop2b ? pml pml x y); -|apply (prop3a ? pml pml x y z);|apply (prop3b ? pml pml x y z); -|apply (prop4a ? pml pml x y); |apply (prop4b ? pml pml x y);] -try (apply ap_symmetric; assumption); intros 4 (x y z H); change with (0 < (δ y z)); -[ change in H with (0 < δ (x ∨ y) (x ∨ z)); - apply (lt_le_transitive ???? H); - apply (le0plus_le ???? (mpositive ? pml ??) (prop5 ? pml pml x y z)); -| change in H with (0 < δ (x ∧ y) (x ∧ z)); - apply (lt_le_transitive ???? H); - apply (le0plus_le ???? (mpositive ? pml (x∨y) (x∨z))); - apply (le_rewl ??? ? (plus_comm ???)); - apply (prop5 ? pml pml);] -qed. - -coercion cic:/matita/premetric_lattice/lattice_of_pmlattice.con. \ No newline at end of file diff --git a/helm/software/matita/contribs/dama/dama/prevalued_lattice.ma b/helm/software/matita/contribs/dama/dama/prevalued_lattice.ma deleted file mode 100644 index 53b2b0a1b..000000000 --- a/helm/software/matita/contribs/dama/dama/prevalued_lattice.ma +++ /dev/null @@ -1,243 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - - - -include "ordered_group.ma". - -record vlattice (R : togroup) : Type ≝ { - wl_carr:> Type; - value: wl_carr → R; - join: wl_carr → wl_carr → wl_carr; - meet: wl_carr → wl_carr → wl_carr; - meet_refl: ∀x. value (meet x x) ≈ value x; - join_refl: ∀x. value (join x x) ≈ value x; - meet_comm: ∀x,y. value (meet x y) ≈ value (meet y x); - join_comm: ∀x,y. value (join x y) ≈ value (join y x); - join_assoc: ∀x,y,z. value (join x (join y z)) ≈ value (join (join x y) z); - meet_assoc: ∀x,y,z. value (meet x (meet y z)) ≈ value (meet (meet x y) z); - meet_wins1: ∀x,y. value (join x (meet x y)) ≈ value x; - meet_wins2: ∀x,y. value (meet x (join x y)) ≈ value x; - modular_mjp: ∀x,y. value (join x y) + value (meet x y) ≈ value x + value y; - join_meet_le: ∀x,y,z. value (join x (meet y z)) ≤ value (join x y); - meet_join_le: ∀x,y,z. value (meet x y) ≤ value (meet x (join y z)) -}. - -interpretation "valued lattice meet" 'and a b = - (cic:/matita/prevalued_lattice/meet.con _ _ a b). - -interpretation "valued lattice join" 'or a b = - (cic:/matita/prevalued_lattice/join.con _ _ a b). - -notation < "\nbsp \mu a" non associative with precedence 80 for @{ 'value2 $a}. -interpretation "lattice value" 'value2 a = (cic:/matita/prevalued_lattice/value.con _ _ a). - -notation "\mu" non associative with precedence 80 for @{ 'value }. -interpretation "lattice value" 'value = (cic:/matita/prevalued_lattice/value.con _ _). - -lemma feq_joinr: ∀R.∀L:vlattice R.∀x,y,z:L. - μ x ≈ μ y → μ (z ∧ x) ≈ μ (z ∧ y) → μ (z ∨ x) ≈ μ (z ∨ y). -intros (R L x y z H H1); -apply (plus_cancr ??? (μ(z∧x))); -apply (Eq≈ (μz + μx) (modular_mjp ????)); -apply (Eq≈ (μz + μy) H); clear H; -apply (Eq≈ (μ(z∨y) + μ(z∧y)) (modular_mjp ??z y)); -apply (plus_cancl ??? (- μ (z ∨ y))); -apply (Eq≈ ? (plus_assoc ????)); -apply (Eq≈ (0+ μ(z∧y)) (opp_inverse ??)); -apply (Eq≈ ? (zero_neutral ??)); -apply (Eq≈ (- μ(z∨y)+ μ(z∨y)+ μ(z∧x)) ? (plus_assoc ????)); -apply (Eq≈ (0+ μ(z∧x)) ? (opp_inverse ??)); -apply (Eq≈ (μ (z ∧ x)) H1 (zero_neutral ??)); -qed. - -lemma modularj: ∀R.∀L:vlattice R.∀y,z:L. μ(y∨z) ≈ μy + μz + -μ (y ∧ z). -intros (R L y z); -lapply (modular_mjp ?? y z) as H1; -apply (plus_cancr ??? (μ(y ∧ z))); -apply (Eq≈ ? H1); clear H1; -apply (Eq≈ ?? (plus_assoc ????)); -apply (Eq≈ (μy+ μz + 0) ? (opp_inverse ??)); -apply (Eq≈ ?? (plus_comm ???)); -apply (Eq≈ (μy + μz) ? (eq_sym ??? (zero_neutral ??))); -apply eq_reflexive. -qed. - -lemma modularm: ∀R.∀L:vlattice R.∀y,z:L. μ(y∧z) ≈ μy + μz + -μ (y ∨ z). -(* CSC: questa è la causa per cui la hint per cercare i duplicati ci sta 1 mese *) -(* exact modularj; *) -intros (R L y z); -lapply (modular_mjp ?? y z) as H1; -apply (plus_cancl ??? (μ(y ∨ z))); -apply (Eq≈ ? H1); clear H1; -apply (Eq≈ ?? (plus_comm ???)); -apply (Eq≈ ?? (plus_assoc ????)); -apply (Eq≈ (μy+ μz + 0) ? (opp_inverse ??)); -apply (Eq≈ ?? (plus_comm ???)); -apply (Eq≈ (μy + μz) ? (eq_sym ??? (zero_neutral ??))); -apply eq_reflexive. -qed. - -lemma modularmj: ∀R.∀L:vlattice R.∀x,y,z:L.μ(x∧(y∨z))≈(μx + μ(y ∨ z) + - μ(x∨(y∨z))). -intros (R L x y z); -lapply (modular_mjp ?? x (y ∨ z)) as H1; -apply (Eq≈ (μ(x∨(y∨z))+ μ(x∧(y∨z)) +-μ(x∨(y∨z))) ? (feq_plusr ???? H1)); clear H1; -apply (Eq≈ ? ? (plus_comm ???)); -apply (Eq≈ (- μ(x∨(y∨z))+ μ(x∨(y∨z))+ μ(x∧(y∨z))) ? (plus_assoc ????)); -apply (Eq≈ (0+μ(x∧(y∨z))) ? (opp_inverse ??)); -apply (Eq≈ (μ(x∧(y∨z))) ? (zero_neutral ??)); -apply eq_reflexive. -qed. - -lemma modularjm: ∀R.∀L:vlattice R.∀x,y,z:L.μ(x∨(y∧z))≈(μx + μ(y ∧ z) + - μ(x∧(y∧z))). -intros (R L x y z); -lapply (modular_mjp ?? x (y ∧ z)) as H1; -apply (Eq≈ (μ(x∧(y∧z))+ μ(x∨(y∧z)) +-μ(x∧(y∧z)))); [2: apply feq_plusr; apply (eq_trans ???? (plus_comm ???)); apply H1] clear H1; -apply (Eq≈ ? ? (plus_comm ???)); -apply (Eq≈ (- μ(x∧(y∧z))+ μ(x∧(y∧z))+ μ(x∨y∧z)) ? (plus_assoc ????)); -apply (Eq≈ (0+ μ(x∨y∧z)) ? (opp_inverse ??)); -apply eq_sym; apply zero_neutral; -qed. - -lemma step1_3_57': ∀R.∀L:vlattice R.∀x,y,z:L. - μ(x ∨ (y ∧ z)) ≈ (μ x) + (μ y) + μ z + -μ (y ∨ z) + -μ (z ∧ (x ∧ y)). -intros (R L x y z); -apply (Eq≈ ? (modularjm ?? x y z)); -apply (Eq≈ ( μx+ (μy+ μz+- μ(y∨z)) +- μ(x∧(y∧z)))); [ - apply feq_plusr; apply feq_plusl; apply (modularm ?? y z);] -apply (Eq≈ (μx+ μy+ μz+- μ(y∨z)+- μ(x∧(y∧z)))); [2: - apply feq_plusl; apply feq_opp; - apply (Eq≈ ? (meet_assoc ?????)); - apply (Eq≈ ? (meet_comm ????)); - apply eq_reflexive;] -apply feq_plusr; apply (Eq≈ ? (plus_assoc ????)); -apply feq_plusr; apply plus_assoc; -qed. - -lemma step1_3_57: ∀R.∀L:vlattice R.∀x,y,z:L. - μ(x ∧ (y ∨ z)) ≈ (μ x) + (μ y) + μ z + -μ (y ∧ z) + -μ (z ∨ (x ∨ y)). -intros (R L x y z); -apply (Eq≈ ? (modularmj ?? x y z)); -apply (Eq≈ ( μx+ (μy+ μz+- μ(y∧z)) +- μ(x∨(y∨z)))); [ - apply feq_plusr; apply feq_plusl; apply (modularj ?? y z);] -apply (Eq≈ (μx+ μy+ μz+- μ(y∧z)+- μ(x∨(y∨z)))); [2: - apply feq_plusl; apply feq_opp; - apply (Eq≈ ? (join_assoc ?????)); - apply (Eq≈ ? (join_comm ????)); - apply eq_reflexive;] -apply feq_plusr; apply (Eq≈ ? (plus_assoc ????)); -apply feq_plusr; apply plus_assoc; -qed. - -(* LEMMA 3.57 *) - -lemma join_meet_le_join: ∀R.∀L:vlattice R.∀x,y,z:L.μ (x ∨ (y ∧ z)) ≤ μ (x ∨ z). -intros (R L x y z); -apply (le_rewl ??? ? (eq_sym ??? (step1_3_57' ?????))); -apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+ -μ(z∧x∧y))); [ - apply feq_plusl; apply feq_opp; apply (eq_trans ?? ? ?? (eq_sym ??? (meet_assoc ?????))); apply eq_reflexive;] -apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+ (- ( μ(z∧x)+ μy+- μ((z∧x)∨y))))); [ - apply feq_plusl; apply feq_opp; apply eq_sym; apply modularm] -apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+ (- μ(z∧x)+ -μy+-- μ((z∧x)∨y)))); [ - apply feq_plusl; apply (Eq≈ (- (μ(z∧x)+ μy) + -- μ((z∧x)∨y))); [ - apply feq_plusr; apply eq_sym; apply eq_opp_plus_plus_opp_opp;] - apply eq_sym; apply eq_opp_plus_plus_opp_opp;] -apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+(- μ(z∧x)+- μy+ μ(y∨(z∧x))))); [ - repeat apply feq_plusl; apply eq_sym; apply (Eq≈ (μ((z∧x)∨y)) (eq_opp_opp_x_x ??)); - apply join_comm;] -apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+(- μ(z∧x)+- μy)+ μ(y∨(z∧x)))); [ - apply eq_sym; apply plus_assoc;] -apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+(- μy + - μ(z∧x))+ μ(y∨(z∧x)))); [ - repeat apply feq_plusr; repeat apply feq_plusl; apply plus_comm;] -apply (le_rewl ??? (μx+ μy+ μz+- μ(y∨z)+- μy + - μ(z∧x)+ μ(y∨(z∧x)))); [ - repeat apply feq_plusr; apply eq_sym; apply plus_assoc;] -apply (le_rewl ??? (μx+ μy+ μz+- μy + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [ - repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????)); - apply (Eq≈ ( μx+ μy+ μz+(- μy+- μ(y∨z))) (eq_sym ??? (plus_assoc ????))); - apply feq_plusl; apply plus_comm;] -apply (le_rewl ??? (μx+ μy+ -μy+ μz + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [ - repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????)); - apply (Eq≈ (μx+ μy+( -μy+ μz)) (eq_sym ??? (plus_assoc ????))); - apply feq_plusl; apply plus_comm;] -apply (le_rewl ??? (μx+ 0 + μz + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [ - repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????)); - apply feq_plusl; apply eq_sym; apply (eq_trans ?? ? ? (plus_comm ???)); - apply opp_inverse; apply eq_reflexive;] -apply (le_rewl ??? (μx+ μz + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [ - repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_comm ???)); - apply eq_sym; apply zero_neutral;] -apply (le_rewl ??? (μz+ μx + - μ(y∨z)+- μ(z∧x)+ μ(y∨(z∧x)))); [ - repeat apply feq_plusr; apply plus_comm;] -apply (le_rewl ??? (μz+ μx +- μ(z∧x)+ - μ(y∨z)+ μ(y∨(z∧x)))); [ - repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????)); - apply (eq_trans ?? ? ? (eq_sym ??? (plus_assoc ????))); apply feq_plusl; - apply plus_comm;] -apply (le_rewl ??? (μ(z∨x)+ - μ(y∨z)+ μ(y∨(z∧x)))); [ - repeat apply feq_plusr; apply modularj;] -apply (le_rewl ??? (μ(z∨x)+ (- μ(y∨z)+ μ(y∨(z∧x)))) (plus_assoc ????)); -apply (le_rewr ??? (μ(x∨z) + 0)); [apply (eq_trans ?? ? ? (plus_comm ???)); apply zero_neutral] -apply (le_rewr ??? (μ(x∨z) + (-μ(y∨z) + μ(y∨z)))); [ apply feq_plusl; apply opp_inverse] -apply (le_rewr ??? (μ(z∨x) + (-μ(y∨z) + μ(y∨z)))); [ apply feq_plusr; apply join_comm;] -repeat apply fle_plusl; apply join_meet_le; -qed. - -lemma meet_le_meet_join: ∀R.∀L:vlattice R.∀x,y,z:L.μ (x ∧ z) ≤ μ (x ∧ (y ∨ z)). -intros (R L x y z); -apply (le_rewr ??? ? (eq_sym ??? (step1_3_57 ?????))); -apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+ -μ(z∨x∨y))); [ - apply feq_plusl; apply feq_opp; apply (eq_trans ?? ? ?? (eq_sym ??? (join_assoc ?????))); apply eq_reflexive;] -apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+ (- ( μ(z∨x)+ μy+- μ((z∨x)∧y))))); [ - apply feq_plusl; apply feq_opp; apply eq_sym; apply modularj] -apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+ (- μ(z∨x)+ -μy+-- μ((z∨x)∧y)))); [ - apply feq_plusl; apply (Eq≈ (- (μ(z∨x)+ μy) + -- μ((z∨x)∧y))); [ - apply feq_plusr; apply eq_sym; apply eq_opp_plus_plus_opp_opp;] - apply eq_sym; apply eq_opp_plus_plus_opp_opp;] -apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+(- μ(z∨x)+- μy+ μ(y∧(z∨x))))); [ - repeat apply feq_plusl; apply eq_sym; apply (Eq≈ (μ((z∨x)∧y)) (eq_opp_opp_x_x ??)); - apply meet_comm;] -apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+(- μ(z∨x)+- μy)+ μ(y∧(z∨x)))); [ - apply eq_sym; apply plus_assoc;] -apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+(- μy + - μ(z∨x))+ μ(y∧(z∨x)))); [ - repeat apply feq_plusr; repeat apply feq_plusl; apply plus_comm;] -apply (le_rewr ??? (μx+ μy+ μz+- μ(y∧z)+- μy + - μ(z∨x)+ μ(y∧(z∨x)))); [ - repeat apply feq_plusr; apply eq_sym; apply plus_assoc;] -apply (le_rewr ??? (μx+ μy+ μz+- μy + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [ - repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????)); - apply (Eq≈ ( μx+ μy+ μz+(- μy+- μ(y∧z))) (eq_sym ??? (plus_assoc ????))); - apply feq_plusl; apply plus_comm;] -apply (le_rewr ??? (μx+ μy+ -μy+ μz + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [ - repeat apply feq_plusr; apply (Eq≈ ?? (plus_assoc ????)); - apply (Eq≈ (μx+ μy+( -μy+ μz)) (eq_sym ??? (plus_assoc ????))); - apply feq_plusl; apply plus_comm;] -apply (le_rewr ??? (μx+ 0 + μz + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [ - repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????)); - apply feq_plusl; apply eq_sym; apply (eq_trans ?? ? ? (plus_comm ???)); - apply opp_inverse; apply eq_reflexive;] -apply (le_rewr ??? (μx+ μz + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [ - repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_comm ???)); - apply eq_sym; apply zero_neutral;] -apply (le_rewr ??? (μz+ μx + - μ(y∧z)+- μ(z∨x)+ μ(y∧(z∨x)))); [ - repeat apply feq_plusr; apply plus_comm;] -apply (le_rewr ??? (μz+ μx +- μ(z∨x)+ - μ(y∧z)+ μ(y∧(z∨x)))); [ - repeat apply feq_plusr; apply (eq_trans ?? ? ?? (plus_assoc ????)); - apply (eq_trans ?? ? ? (eq_sym ??? (plus_assoc ????))); apply feq_plusl; - apply plus_comm;] -apply (le_rewr ??? (μ(z∧x)+ - μ(y∧z)+ μ(y∧(z∨x)))); [ - repeat apply feq_plusr; apply modularm;] -apply (le_rewr ??? (μ(z∧x)+ (- μ(y∧z)+ μ(y∧(z∨x)))) (plus_assoc ????)); -apply (le_rewl ??? (μ(x∧z) + 0)); [apply (eq_trans ?? ? ? (plus_comm ???)); apply zero_neutral] -apply (le_rewl ??? (μ(x∧z) + (-μ(y∧z) + μ(y∧z)))); [ apply feq_plusl; apply opp_inverse] -apply (le_rewl ??? (μ(z∧x) + (-μ(y∧z) + μ(y∧z)))); [ apply feq_plusr; apply meet_comm;] -repeat apply fle_plusl; apply meet_join_le; -qed. diff --git a/helm/software/matita/contribs/dama/dama/sandwich.ma b/helm/software/matita/contribs/dama/dama/sandwich.ma deleted file mode 100644 index aaea369f5..000000000 --- a/helm/software/matita/contribs/dama/dama/sandwich.ma +++ /dev/null @@ -1,81 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - - - -include "nat/plus.ma". -include "nat/orders.ma". - -lemma ltwl: ∀a,b,c:nat. b + a < c → a < c. -intros 3 (x y z); elim y (H z IH H); [apply H] -apply IH; apply lt_S_to_lt; apply H; -qed. - -lemma ltwr: ∀a,b,c:nat. a + b < c → a < c. -intros 3 (x y z); rewrite > sym_plus; apply ltwl; -qed. - -include "tend.ma". -include "metric_lattice.ma". - -alias symbol "leq" = "ordered sets less or equal than". -alias symbol "and" = "constructive and". -theorem sandwich: -let ugo ≝ excess_OF_lattice1 in - ∀R.∀ml:mlattice R.∀an,bn,xn:sequence ml.∀x:ml. - (∀n. (xn n ≤ an n) ∧ (bn n ≤ xn n)) → - an ⇝ x → bn ⇝ x → xn ⇝ x. -intros (R ml an bn xn x H Ha Hb); -unfold tends0 in Ha Hb ⊢ %; unfold d2s in Ha Hb ⊢ %; intros (e He); -alias num (instance 0) = "natural number". -cases (Ha (e/2) (divide_preserves_lt ??? He)) (n1 H1); clear Ha; -cases (Hb (e/2) (divide_preserves_lt ??? He)) (n2 H2); clear Hb; -apply (ex_introT ?? (n1+n2)); intros (n3 Lt_n1n2_n3); -lapply (ltwr ??? Lt_n1n2_n3) as Lt_n1n3; lapply (ltwl ??? Lt_n1n2_n3) as Lt_n2n3; -cases (H1 ? Lt_n1n3) (c daxe); cases (H2 ? Lt_n2n3) (c dbxe); -cases (H n3) (H7 H8); clear Lt_n1n3 Lt_n2n3 Lt_n1n2_n3 c H1 H2 H n1 n2; -(* the main inequality *) -cut (δ (xn n3) x ≤ δ (bn n3) x + δ (an n3) x + δ (an n3) x) as main_ineq; [2: - apply (le_transitive ???? (mtineq ???? (an n3))); - cut ( δ(an n3) (bn n3)+- δ(xn n3) (bn n3)≈( δ(an n3) (xn n3))) as H11; [2: - lapply (le_mtri ?? ??? H8 H7) as H9; clear H7 H8; - lapply (Eq≈ ? (msymmetric ????) H9) as H10; clear H9; - lapply (feq_plusr ? (- δ(xn n3) (bn n3)) ?? H10) as H9; clear H10; - apply (Eq≈ ? H9); clear H9; - apply (Eq≈ (δ(xn n3) (an n3)+ δ(bn n3) (xn n3)+- δ(xn n3) (bn n3)) (plus_comm ??( δ(xn n3) (an n3)))); - apply (Eq≈ (δ(xn n3) (an n3)+ δ(bn n3) (xn n3)+- δ(bn n3) (xn n3)) (feq_opp ??? (msymmetric ????))); - apply (Eq≈ ( δ(xn n3) (an n3)+ (δ(bn n3) (xn n3)+- δ(bn n3) (xn n3))) (plus_assoc ????)); - apply (Eq≈ (δ(xn n3) (an n3) + (- δ(bn n3) (xn n3) + δ(bn n3) (xn n3))) (plus_comm ??(δ(bn n3) (xn n3)))); - apply (Eq≈ (δ(xn n3) (an n3) + 0) (opp_inverse ??)); - apply (Eq≈ ? (plus_comm ???)); - apply (Eq≈ ? (zero_neutral ??)); - apply (Eq≈ ? (msymmetric ????)); - apply eq_reflexive;] - apply (Le≪ (δ(an n3) (xn n3)+ δ(an n3) x) (msymmetric ??(an n3)(xn n3))); - apply (Le≪ (δ(an n3) (bn n3)+- δ(xn n3) (bn n3)+ δ(an n3) x) H11); - apply (Le≪ (- δ(xn n3) (bn n3)+ δ(an n3) (bn n3)+δ(an n3) x) (plus_comm ??(δ(an n3) (bn n3)))); - apply (Le≪ (- δ(xn n3) (bn n3)+ (δ(an n3) (bn n3)+δ(an n3) x)) (plus_assoc ????)); - apply (Le≪ ((δ(an n3) (bn n3)+δ(an n3) x)+- δ(xn n3) (bn n3)) (plus_comm ???)); - apply lew_opp; [apply mpositive] apply fle_plusr; - apply (Le≫ ? (plus_comm ???)); - apply (Le≫ ( δ(an n3) x+ δx (bn n3)) (msymmetric ????)); - apply mtineq;] -split; [ (* first the trivial case: -e< δ(xn n3) x *) - apply (lt_le_transitive ????? (mpositive ????)); - apply lt_zero_x_to_lt_opp_x_zero; assumption;] -(* the main goal: δ(xn n3) x