From: Enrico Tassi Date: Sun, 1 Jun 2008 15:38:46 +0000 (+0000) Subject: more work on supremum X-Git-Tag: make_still_working~5093 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2cb6a7c755375fa6b64a3590ebc98957829afdca;p=helm.git more work on supremum --- diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends index 77abdf673..5a19b2a54 100644 --- a/helm/software/matita/contribs/dama/dama/depends +++ b/helm/software/matita/contribs/dama/dama/depends @@ -1,9 +1,12 @@ +.unnamed.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 sequence.ma nat/nat.ma -supremum.ma bishop_set.ma ordered_set.ma sequence.ma +supremum.ma bishop_set.ma cprop_connectives.ma nat_ordered_set.ma ordered_set.ma sequence.ma +bishop_set_rewrite.ma bishop_set.ma +cprop_connectives.ma logic/equality.ma +nat_ordered_set.ma cprop_connectives.ma nat/compare.ma ordered_set.ma +ordered_set.ma cprop_connectives.ma +extra.ma bishop_set_rewrite.ma logic/equality.ma +nat/compare.ma nat/nat.ma diff --git a/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma b/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma new file mode 100644 index 000000000..e7dfec461 --- /dev/null +++ b/helm/software/matita/contribs/dama/dama/nat_ordered_set.ma @@ -0,0 +1,51 @@ +(**************************************************************************) +(* ___ *) +(* ||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". + +include "nat/compare.ma". +include "cprop_connectives.ma". + +definition nat_excess : nat → nat → CProp ≝ λn,m. m H2; reflexivity; + |2: right;apply le_S_S; assumption]] +qed. + +lemma nat_excess_cotransitive: cotransitive ? nat_excess. +intros 3 (x y z); unfold nat_excess; simplify; intros; +cases (nat_discriminable x z); [2: left; assumption] cases H1; clear H1; +[1: right; apply (trans_lt ??? H H2); +|2: right; rewrite < H2; assumption;] +qed. + +lemma nat_ordered_set : ordered_set. +apply (mk_ordered_set ? nat_excess); +[1: intro x; intro; apply (not_le_Sn_n ? H); +|2: apply nat_excess_cotransitive] +qed. diff --git a/helm/software/matita/contribs/dama/dama/supremum.ma b/helm/software/matita/contribs/dama/dama/supremum.ma index 7fb1da4ba..40026abc2 100644 --- a/helm/software/matita/contribs/dama/dama/supremum.ma +++ b/helm/software/matita/contribs/dama/dama/supremum.ma @@ -43,9 +43,7 @@ interpretation "Ordered set increasing" 'increasing s = (cic:/matita/dama/supremum/increasing.con _ s). interpretation "Ordered set strong sup" 'supremum s x = (cic:/matita/dama/supremum/supremum.con _ s x). - -include "nat/compare.ma". -include "nat/plus.ma". + include "bishop_set.ma". lemma uniq_supremum: @@ -66,25 +64,9 @@ cases (H1 ? H) (w Hw); apply Hv; assumption; qed. (* Lemma 2.6 *) -definition strictly_increasing ≝ λC:ordered_set.λa:sequence C.∀n:nat.a (S n) ≰ a n. +definition strictly_increasing ≝ + λC:ordered_set.λa:sequence C.∀n:nat.a (S n) ≰ a n. -definition nat_excess : nat → nat → CProp ≝ λn,m. leb (m+S O) n = true. - -axiom nat_excess_cotransitive: cotransitive ? nat_excess. -(*intros 3 (x y z); elim x 0; elim y 0; elim z 0; - [1: intros; left; assumption - |2,5,6,7: intros; first [right; constructor 1|left; constructor 1] - |3: intros (n H abs); simplify in abs; destruct abs; - |4: intros (n H m W abs); simplify in abs; destruct abs; - |8: clear x y z; intros (x H1 y H2 z H3 H4); -*) - -lemma nat_ordered_set : ordered_set. -apply (mk_ordered_set ? nat_excess); -[1: intro x; elim x (w H); simplify; intro X; [destruct X] apply H; assumption; -|2: apply nat_excess_cotransitive] -qed. - notation < "s \nbsp 'is_strictly_increasing'" non associative with precedence 50 for @{'strictly_increasing $s}. notation > "s 'is_strictly_increasing'" non associative with precedence 50 @@ -92,27 +74,56 @@ notation > "s 'is_strictly_increasing'" non associative with precedence 50 interpretation "Ordered set increasing" 'strictly_increasing s = (cic:/matita/dama/supremum/strictly_increasing.con _ s). -notation "a \uparrow u" non associative with precedence 50 for @{'sup_inc $a $u}. +notation "a \uparrow u" non associative with precedence 50 for @{'sup_inc $a $u}. interpretation "Ordered set supremum of increasing" 'sup_inc s u = (cic:/matita/dama/cprop_connectives/And.ind#xpointer(1/1) (cic:/matita/dama/supremum/increasing.con _ s) (cic:/matita/dama/supremum/supremum.con _ s u)). + +include "nat_ordered_set.ma". +alias symbol "nleq" = "Ordered set excess". +alias symbol "leq" = "Ordered set less or equal than". lemma trans_increasing: - ∀C:ordered_set.∀s:sequence C.s is_increasing → ∀n,m. m ≰ n → s n ≤ s m. -intros 5 (C s Hs n m); elim m; [1: cases (?:False); autobatch] -cases (le_to_or_lt_eq ?? H1); - [2: destruct H2; apply Hs; - |1: apply (le_transitive ???? (H (lt_S_S_to_lt ?? H2))); apply Hs;] + ∀C:ordered_set.∀a:sequence C.a is_increasing → ∀n,m:nat_ordered_set. m ≰ n → a n ≤ a m. +intros 5 (C a Hs n m); elim m; [cases (not_le_Sn_O n H);] +intro; apply H; +[1: change in n1 with (os_carr nat_ordered_set); (* canonical structures *) + change with (n H3; apply H;] + | cases (?:False); change in Hp with (n