From: Enrico Tassi Date: Thu, 29 May 2008 09:51:22 +0000 (+0000) Subject: first page of the new dama proof X-Git-Tag: make_still_working~5110 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=648db01678fac09ddfb3cce900bc72e8a1c420da;p=helm.git first page of the new dama proof --- diff --git a/helm/software/matita/contribs/dama/dama/bishop_set.ma b/helm/software/matita/contribs/dama/dama/bishop_set.ma new file mode 100644 index 000000000..b877e094c --- /dev/null +++ b/helm/software/matita/contribs/dama/dama/bishop_set.ma @@ -0,0 +1,74 @@ +(**************************************************************************) +(* ___ *) +(* ||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_set.ma". + +(* Definition 2.2, setoid *) +record bishop_set: Type ≝ { + bs_carr:> Type; + bs_apart: bs_carr → bs_carr → CProp; + bs_coreflexive: coreflexive ? bs_apart; + bs_symmetric: symmetric ? bs_apart; + bs_cotransitive: cotransitive ? bs_apart +}. + +notation "hvbox(a break # b)" non associative with precedence 50 + for @{ 'apart $a $b}. + +interpretation "bishop_setapartness" 'apart x y = + (cic:/matita/dama/bishop_set/bs_apart.con _ x y). + +definition bishop_set_of_ordered_set: ordered_set → bishop_set. +intros (E); apply (mk_bishop_set 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. + +(* Definition 2.2 (2) *) +definition eq ≝ λA:bishop_set.λa,b:A. ¬ (a # b). + +notation "hvbox(a break ≈ b)" non associative with precedence 50 + for @{ 'napart $a $b}. + +interpretation "Bishop set alikeness" 'napart a b = + (cic:/matita/dama/bishop_set/eq.con _ a b). + +lemma eq_reflexive:∀E:bishop_set. reflexive ? (eq E). +intros (E); unfold; intros (x); apply bs_coreflexive; +qed. + +lemma eq_sym_:∀E:bishop_set.symmetric ? (eq E). +intros 4 (E x y H); intro T; cases (H (bs_symmetric ??? T)); +qed. + +lemma eq_sym:∀E:bishop_set.∀x,y:E.x ≈ y → y ≈ x ≝ eq_sym_. + +lemma eq_trans_: ∀E:bishop_set.transitive ? (eq E). +(* bug. intros k deve fare whd quanto basta *) +intros 6 (E x y z Exy Eyz); intro Axy; cases (bs_cotransitive ???y Axy); +[apply Exy|apply Eyz] assumption. +qed. + +coercion cic:/matita/dama/bishop_set/bishop_set_of_ordered_set.con. + +lemma le_antisymmetric: + ∀E:ordered_set.antisymmetric E (le E) (eq E). +intros 5 (E x y Lxy Lyx); intro H; +cases H; [apply Lxy;|apply Lyx] assumption; +qed. + diff --git a/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma b/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma new file mode 100644 index 000000000..bd5a83a88 --- /dev/null +++ b/helm/software/matita/contribs/dama/dama/bishop_set_rewrite.ma @@ -0,0 +1,72 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "bishop_set.ma". + +coercion cic:/matita/dama/bishop_set/eq_sym.con. + +lemma eq_trans:∀E:bishop_set.∀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/dama/bishop_set/eq_trans.con _ _ _). + +lemma le_rewl: ∀E:ordered_set.∀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; right; assumption; +qed. + +lemma le_rewr: ∀E:ordered_set.∀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; left; assumption; +qed. + +notation > "'Le'≪" non associative with precedence 50 for @{'lerewritel}. +interpretation "le_rewl" 'lerewritel = (cic:/matita/dama/bishop_set_rewrite/le_rewl.con _ _ _). +notation > "'Le'≫" non associative with precedence 50 for @{'lerewriter}. +interpretation "le_rewr" 'lerewriter = (cic:/matita/dama/bishop_set_rewrite/le_rewr.con _ _ _). + +lemma ap_rewl: ∀A:bishop_set.∀x,z,y:A. x ≈ y → y # z → x # z. +intros (A x z y Exy Ayz); cases (bs_cotransitive ???x Ayz); [2:assumption] +cases (eq_sym ??? Exy H); +qed. + +lemma ap_rewr: ∀A:bishop_set.∀x,z,y:A. x ≈ y → z # y → z # x. +intros (A x z y Exy Azy); apply bs_symmetric; apply (ap_rewl ???? Exy); +apply bs_symmetric; assumption; +qed. + +notation > "'Ap'≪" non associative with precedence 50 for @{'aprewritel}. +interpretation "ap_rewl" 'aprewritel = (cic:/matita/dama/bishop_set_rewrite/ap_rewl.con _ _ _). +notation > "'Ap'≫" non associative with precedence 50 for @{'aprewriter}. +interpretation "ap_rewr" 'aprewriter = (cic:/matita/dama/bishop_set_rewrite/ap_rewr.con _ _ _). + +lemma exc_rewl: ∀A:ordered_set.∀x,z,y:A. x ≈ y → y ≰ z → x ≰ z. +intros (A x z y Exy Ayz); cases (os_cotransitive ??? x Ayz); [2:assumption] +cases Exy; right; assumption; +qed. + +lemma exc_rewr: ∀A:ordered_set.∀x,z,y:A. x ≈ y → z ≰ y → z ≰ x. +intros (A x z y Exy Azy); cases (os_cotransitive ???x Azy); [assumption] +cases (Exy); left; assumption; +qed. + +notation > "'Ex'≪" non associative with precedence 50 for @{'ordered_setrewritel}. +interpretation "exc_rewl" 'ordered_setrewritel = (cic:/matita/dama/bishop_set_rewrite/exc_rewl.con _ _ _). +notation > "'Ex'≫" non associative with precedence 50 for @{'ordered_setrewriter}. +interpretation "exc_rewr" 'ordered_setrewriter = (cic:/matita/dama/bishop_set_rewrite/exc_rewr.con _ _ _). + diff --git a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma new file mode 100644 index 000000000..c84382e85 --- /dev/null +++ b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma @@ -0,0 +1,61 @@ +(**************************************************************************) +(* ___ *) +(* ||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/equality.ma". + +inductive Or (A,B:CProp) : CProp ≝ + Left : A → Or A B + | Right : B → Or A B. + +interpretation "constructive or" 'or x y = + (cic:/matita/dama/cprop_connectives/Or.ind#xpointer(1/1) x y). + +inductive And (A,B:CProp) : CProp ≝ + | Conj : A → B → And A B. + +interpretation "constructive and" 'and x y = + (cic:/matita/dama/cprop_connectives/And.ind#xpointer(1/1) x y). + +inductive exT (A:Type) (P:A→CProp) : CProp ≝ + 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. + +interpretation "constructive exists" 'exists \eta.x = + (cic:/matita/dama/cprop_connectives/ex.ind#xpointer(1/1) _ x). + +interpretation "constructive exists (Type)" 'exists \eta.x = + (cic:/matita/dama/cprop_connectives/exT.ind#xpointer(1/1) _ x). + +inductive False : CProp ≝ . + +definition Not ≝ λx:CProp.x → False. + +interpretation "constructive not" 'not x = + (cic:/matita/dama/cprop_connectives/Not.con x). + +definition cotransitive ≝ + λC:Type.λlt:C→C→CProp.∀x,y,z:C. lt x y → lt x z ∨ lt z y. + +definition coreflexive ≝ λC:Type.λlt:C→C→CProp. ∀x:C. ¬ (lt x x). + +definition symmetric ≝ λC:Type.λlt:C→C→CProp. ∀x,y:C.lt x y → lt y x. + +definition antisymmetric ≝ λA:Type.λR:A→A→CProp.λeq:A→A→CProp.∀x:A.∀y:A.R x y→R y x→eq x y. + +definition reflexive ≝ λA:Type.λR:A→A→CProp.∀x:A.R x x. + +definition transitive ≝ λA:Type.λR:A→A→CProp.∀x,y,z:A.R x y → R y z → R x z. + diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends index 26836c7fd..dd9a395d6 100644 --- a/helm/software/matita/contribs/dama/dama/depends +++ b/helm/software/matita/contribs/dama/dama/depends @@ -1,2 +1,6 @@ -excedence.ma logic/equality.ma +bishop_set.ma ordered_set.ma +extra.ma bishop_set_rewrite.ma +ordered_set.ma cprop_connectives.ma +cprop_connectives.ma logic/equality.ma +bishop_set_rewrite.ma bishop_set.ma logic/equality.ma diff --git a/helm/software/matita/contribs/dama/dama/excedence.ma b/helm/software/matita/contribs/dama/dama/excedence.ma deleted file mode 100644 index ad0f45491..000000000 --- a/helm/software/matita/contribs/dama/dama/excedence.ma +++ /dev/null @@ -1,260 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "logic/equality.ma". - -inductive Or (A,B:CProp) : CProp ≝ - Left : A → Or A B - | Right : B → Or A B. - -interpretation "constructive or" 'or x y = - (cic:/matita/dama/excess/Or.ind#xpointer(1/1) x y). - -inductive And (A,B:CProp) : CProp ≝ - | Conj : A → B → And A B. - -interpretation "constructive and" 'and x y = - (cic:/matita/dama/excess/And.ind#xpointer(1/1) x y). - -inductive exT (A:Type) (P:A→CProp) : CProp ≝ - 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. - -interpretation "constructive exists" 'exists \eta.x = - (cic:/matita/dama/excess/ex.ind#xpointer(1/1) _ x). -interpretation "constructive exists (Type)" 'exists \eta.x = - (cic:/matita/dama/excess/exT.ind#xpointer(1/1) _ x). - -inductive False : CProp ≝ . - -definition Not ≝ λx:CProp.x → False. - -interpretation "constructive not" 'not x = - (cic:/matita/dama/excess/Not.con x). - -definition cotransitive ≝ - λC:Type.λlt:C→C→CProp.∀x,y,z:C. lt x y → lt x z ∨ lt z y. - -definition coreflexive ≝ λC:Type.λlt:C→C→CProp. ∀x:C. ¬ (lt x x). - -definition symmetric ≝ λC:Type.λlt:C→C→CProp. ∀x,y:C.lt x y → lt y x. - -definition antisymmetric ≝ λA:Type.λR:A→A→CProp.λeq:A→A→CProp.∀x:A.∀y:A.R x y→R y x→eq x y. - -definition reflexive ≝ λA:Type.λR:A→A→CProp.∀x:A.R x x. - -definition transitive ≝ λA:Type.λR:A→A→CProp.∀x,y,z:A.R x y → R y z → R x z. - -record excess : Type ≝ { - exc_carr:> Type; - exc_excess: exc_carr → exc_carr → CProp; - exc_coreflexive: coreflexive ? exc_excess; - exc_cotransitive: cotransitive ? exc_excess -}. - -interpretation "Excess" 'nleq a b = (cic:/matita/dama/excess/exc_excess.con _ a b). - -record apartness : Type ≝ { - ap_carr:> Type; - ap_apart: ap_carr → ap_carr → CProp; - 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/dama/excess/ap_apart.con _ x y). - -definition apartness_of_excess: excess → 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. - -definition strong_ext ≝ λA:apartness.λop:A→A.∀x,y. op x # op y → x # y. - -definition le ≝ λE:excess.λa,b:E. ¬ (a ≰ b). - -interpretation "Excess less or equal than" 'leq a b = - (cic:/matita/dama/excess/le.con _ a b). - -interpretation "Excess less or equal than" 'geq a b = - (cic:/matita/excess/le.con _ b a). - -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/dama/excess/eq.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). -intros 4 (E x y H); intro T; cases (H (ap_symmetric ??? T)); -qed. - -lemma eq_sym:∀E:apartness.∀x,y:E.x ≈ y → y ≈ x ≝ eq_sym_. - -(* SETOID REWRITE *) -coercion cic:/matita/dama/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/dama/excess/eq_trans.con _ _ _). - -coercion cic:/matita/dama/excess/apartness_of_excess.con. - -lemma le_antisymmetric: - ∀E:excess.antisymmetric E (le E) (eq E). -intros 5 (E x y Lxy Lyx); intro H; -cases 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/dama/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; -cases Axy (H1 H1); cases Ayz (H2 H2); [1:cases (Lxy H1)|3:cases (Lyz H2)]clear Axy Ayz; -[1: cases (exc_cotransitive ??? y H1) (X X); [cases (Lxy X)|cases (exc_coreflexive ?? X)] -|2: cases (exc_cotransitive ??? x H2) (X X); [right;assumption|cases (Lxy X)]] -qed. - -theorem lt_to_excess: ∀E:excess.∀a,b:E. (a < b) → (b ≰ a). -intros (E a b Lab); cases Lab (LEab Aab); cases 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; 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; left; assumption; -qed. - -notation > "'Le'≪" non associative with precedence 50 for @{'lerewritel}. -interpretation "le_rewl" 'lerewritel = (cic:/matita/dama/excess/le_rewl.con _ _ _). -notation > "'Le'≫" non associative with precedence 50 for @{'lerewriter}. -interpretation "le_rewr" 'lerewriter = (cic:/matita/dama/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 (eq_sym ??? Exy H); -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/dama/excess/ap_rewl.con _ _ _). -notation > "'Ap'≫" non associative with precedence 50 for @{'aprewriter}. -interpretation "ap_rewr" 'aprewriter = (cic:/matita/dama/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); cases (exc_cotransitive ??? x Ayz); [2:assumption] -cases Exy; 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); cases (exc_cotransitive ???x Azy); [assumption] -cases (Exy); left; assumption; -qed. - -notation > "'Ex'≪" non associative with precedence 50 for @{'excessrewritel}. -interpretation "exc_rewl" 'excessrewritel = (cic:/matita/dama/excess/exc_rewl.con _ _ _). -notation > "'Ex'≫" non associative with precedence 50 for @{'excessrewriter}. -interpretation "exc_rewr" 'excessrewriter = (cic:/matita/dama/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; cases 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; cases 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/dama/excess/lt_rewl.con _ _ _). -notation > "'Lt'≫" non associative with precedence 50 for @{'ltrewriter}. -interpretation "lt_rewr" 'ltrewriter = (cic:/matita/dama/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)] -cases 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)] -cases APx (EXx EXx); [cases (LEx EXx)] -cases (exc_cotransitive ??? x EXx) (EXz EXz); [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 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; [left|right] assumption. -qed. - -lemma ap_le_to_lt: ∀E:excess.∀a,c:E.c # a → c ≤ a → c < a. -intros; split; assumption; -qed. - -definition total_order_property : ∀E:excess. Type ≝ - λE:excess. ∀a,b:E. a ≰ b → b < a. - diff --git a/helm/software/matita/contribs/dama/dama/extra.ma b/helm/software/matita/contribs/dama/dama/extra.ma new file mode 100644 index 000000000..d36e0db7e --- /dev/null +++ b/helm/software/matita/contribs/dama/dama/extra.ma @@ -0,0 +1,87 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "bishop_set_rewrite.ma". + +definition strong_ext ≝ λA:bishop_set.λop:A→A.∀x,y. op x # op y → x # y. + + + +definition lt ≝ λE:excess.λa,b:E. a ≤ b ∧ a # b. + +interpretation "ordered sets less than" 'lt a b = (cic:/matita/dama/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; +cases Axy (H1 H1); cases Ayz (H2 H2); [1:cases (Lxy H1)|3:cases (Lyz H2)]clear Axy Ayz; +[1: cases (exc_cotransitive ??? y H1) (X X); [cases (Lxy X)|cases (exc_coreflexive ?? X)] +|2: cases (exc_cotransitive ??? x H2) (X X); [right;assumption|cases (Lxy X)]] +qed. + +theorem lt_to_excess: ∀E:excess.∀a,b:E. (a < b) → (b ≰ a). +intros (E a b Lab); cases Lab (LEab Aab); cases Aab (H H);[cases (LEab H)] +fold normalize (b ≰ a); assumption; (* BUG *) +qed. + +lemma lt_rewr: ∀A:excess.∀x,z,y:A. x ≈ y → z < y → z < x. +intros (A x y z E H); split; cases 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; cases 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/dama/excess/lt_rewl.con _ _ _). +notation > "'Lt'≫" non associative with precedence 50 for @{'ltrewriter}. +interpretation "lt_rewr" 'ltrewriter = (cic:/matita/dama/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)] +cases 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)] +cases APx (EXx EXx); [cases (LEx EXx)] +cases (exc_cotransitive ??? x EXx) (EXz EXz); [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 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; [left|right] assumption. +qed. + +lemma ap_le_to_lt: ∀E:excess.∀a,c:E.c # a → c ≤ a → c < a. +intros; split; assumption; +qed. + +definition total_order_property : ∀E:excess. Type ≝ + λE:excess. ∀a,b:E. a ≰ b → b < a. + diff --git a/helm/software/matita/contribs/dama/dama/ordered_set.ma b/helm/software/matita/contribs/dama/dama/ordered_set.ma new file mode 100644 index 000000000..b5b4d8e78 --- /dev/null +++ b/helm/software/matita/contribs/dama/dama/ordered_set.ma @@ -0,0 +1,55 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "cprop_connectives.ma". + +(* Definition 2.1 *) +record ordered_set: Type ≝ { + os_carr:> Type; + os_excess: os_carr → os_carr → CProp; + os_coreflexive: coreflexive ? os_excess; + os_cotransitive: cotransitive ? os_excess +}. + +interpretation "Ordered set excess" 'nleq a b = + (cic:/matita/dama/ordered_set/os_excess.con _ a b). + +(* Definition 2.2 (3) *) +definition le ≝ λE:ordered_set.λa,b:E. ¬ (a ≰ b). + +interpretation "Ordered set greater or equal than" 'geq a b = + (cic:/matita/dama/ordered_set/le.con _ b a). + +interpretation "Ordered set less or equal than" 'leq a b = + (cic:/matita/dama/ordered_set/le.con _ a b). + +lemma le_reflexive: ∀E.reflexive ? (le E). +unfold reflexive; intros 3 (E x H); apply (os_coreflexive ?? H); +qed. + +lemma le_transitive: ∀E.transitive ? (le E). +unfold transitive; intros 7 (E x y z H1 H2 H3); cases (os_cotransitive ??? y H3) (H4 H4); +[cases (H1 H4)|cases (H2 H4)] +qed. + +(* Lemma 2.3 *) +lemma exc_le_variance: + ∀O:ordered_set.∀a,b,a',b':O.a ≰ b → a ≤ a' → b' ≤ b → a' ≰ b'. +intros (O a b a1 b1 Eab Laa1 Lb1b); +cases (os_cotransitive ??? a1 Eab) (H H); [cases (Laa1 H)] +cases (os_cotransitive ??? b1 H) (H1 H1); [assumption] +cases (Lb1b H1); +qed. + + \ No newline at end of file