+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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
+++ /dev/null
-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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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).
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
-
-
-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
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
-
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 *)
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 *)
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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<e → 0 < e/n.
-intros; elim n; [apply (Lt≫ ? (div1 ??));assumption]
-unfold divide; elim (dg_prop G e (S n1)); simplify; simplify in f;
-apply (ltmul_lt ??? (S n1)); simplify; apply (Lt≫ ? p);
-apply (Lt≪ ? (zero_neutral ??)); (* bug se faccio repeat *)
-apply (Lt≪ ? (zero_neutral ??));
-apply (Lt≪ ? (mulzero ?n1));
-assumption;
-qed.
-
-lemma muleqplus_lt: ∀G:todgroup.∀x,y:G.∀n,m.
- 0<x → 0<y → S n * x ≈ S (n + S m) * y → y < x.
-intros (G x y n m H1 H2 H3); apply (ltmul_lt ??? n); apply (Lt≫ ? H3);
-clear H3; elim m; [
- rewrite > 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.
-
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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<e *)
-apply (le_lt_transitive ???? main_ineq);
-apply (Lt≫ (e/2+e/2+e/2)); [apply (divpow ?e 2)]
-repeat (apply ltplus; try assumption);
-qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 "sandwich.ma".
-
-(* 3.17 *)
-lemma tends_uniq:
- ∀R.∀ml:mlattice R.∀xn:sequence ml.∀x,y:ml.
- xn ⇝ x → xn ⇝ y → δ x y ≈ 0.
-intros (R ml xn x y H1 H2); unfold tends0 in H1 H2; unfold d2s in H1 H2;
-intro Axy; lapply (ap_le_to_lt ??? (ap_symmetric ??? Axy) (mpositive ? ml ??)) as ge0;
-cases (H1 (δ x y/1) (divide_preserves_lt ??? ge0)) (n1 Hn1); clear H1;
-cases (H2 (δ x y/1) (divide_preserves_lt ??? ge0)) (n2 Hn2); clear H2;
-letin N ≝ (S (n2 + n1));
-cases (Hn1 N ?) (H1 H2); [apply (ltwr ? n2); rewrite < sym_plus; apply le_n;]
-cases (Hn2 N ?) (H3 H4); [apply (ltwl ? n1); rewrite < sym_plus; apply le_n;]
-clear H1 H3 Hn2 Hn1 N ge0 Axy; lapply (mtineq ?? x y (xn (S (n2+n1)))) as H5;
-cut ( δx (xn (S (n2+n1)))+ δ(xn (S (n2+n1))) y < δx y/1 + δ(xn (S (n2+n1))) y) as H6;[2:
- apply flt_plusr; apply (Lt≪ ? (msymmetric ????)); assumption]
-lapply (le_lt_transitive ???? H5 H6) as H7; clear H6;
-cut (δx y/1+ δ(xn (S (n2+n1))) y < δx y/1+ δx y/1) as H6; [2:apply flt_plusl; assumption]
-lapply (lt_transitive ???? H7 H6) as ABS; clear H6 H7 H4 H5 H2 n1 n2 xn;
-lapply (divpow ? (δ x y) 1) as D; lapply (Lt≪ ? (eq_sym ??? D) ABS) as H;
-change in H with ( δx y/1+ δx y/1< δx y/1+ δx y/1);
-apply (lt_coreflexive ?? H);
-qed.
-
-(* 3.18 *)
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 sequence := λO:Type.nat → O.
-
-definition fun_of_sequence: ∀O:Type.sequence O → nat → O ≝ λO.λx:sequence O.x.
-
-coercion cic:/matita/sequence/fun_of_sequence.con 1.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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".
-include "metric_space.ma".
-include "nat/orders.ma".
-
-definition tends0 ≝
- λO:pogroup.λs:sequence O.∀e:O.0 < e → ∃N.∀n.N < n → -e < s n ∧ s n < e.
-
-definition d2s ≝
- λR.λms:metric_space R.λs:sequence ms.λk.λn. δ (s n) k.
-
-notation "s ⇝ x" non associative with precedence 50 for @{'tends $s $x}.
-interpretation "tends to" 'tends s x =
- (cic:/matita/tend/tends0.con _ (cic:/matita/tend/d2s.con _ _ s x)).
-
projects / helm.git / commitdiff