--- /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_set.ma".
+
+include "nat/compare.ma".
+include "cprop_connectives.ma".
+
+definition nat_excess : nat → nat → CProp ≝ λn,m. m<n.
+
+lemma nat_elim2:
+ ∀R:nat → nat → CProp.
+ (∀ n:nat. R O n) → (∀n:nat. R (S n) O) → (∀n,m:nat. R n m → R (S n) (S m)) →
+ ∀n,m:nat. R n m.
+intros 5;elim n; [apply H]
+cases m;[ apply H1| apply H2; apply H3 ]
+qed.
+
+lemma nat_discriminable: ∀x,y:nat.x < y ∨ x = y ∨ y < x.
+intros (x y); apply (nat_elim2 ???? x y);
+[1: intro;left;cases n; [right;reflexivity] left; apply lt_O_S;
+|2: intro;right;apply lt_O_S;
+|3: intros; cases H;
+ [1: cases H1; [left; left; apply le_S_S; assumption]
+ left;right;rewrite > 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.
(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:
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
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<n1); (* is sort elimination not allowed preserved by delta? *)
+ cases (le_to_or_lt_eq ?? H1); [apply le_S_S_to_le;assumption]
+ cases (Hs n); rewrite < H3 in H2; assumption (* ogni goal di tipo Prop non è anche di tipo CProp *)
+|2: cases (os_cotransitive ??? (a n1) H2); [assumption]
+ cases (Hs n1); assumption;]
qed.
-
+
+lemma strictly_increasing_reaches:
+ ∀C:ordered_set.∀m:sequence nat_ordered_set.
+ m is_strictly_increasing → ∀w.∃t.m t ≰ w.
+intros; elim w;
+[1: cases (nat_discriminable O (m O)); [2: cases (not_le_Sn_n O (ltn_to_ltO ?? H1))]
+ cases H1; [exists [apply O] apply H2;]
+ exists [apply (S O)] lapply (H O) as H3; rewrite < H2 in H3; assumption
+|2: cases H1 (p Hp); cases (nat_discriminable (S n) (m p));
+ [ cases H2; clear H2;
+ [ exists [apply p]; assumption;
+ | exists [apply (S p)]; rewrite > H3; apply H;]
+ | cases (?:False); change in Hp with (n<m p);
+apply (not_le_Sn_n (m p) ?).
+ apply (transitive_le (S (m p)) (S n) (m p) ? ?);
+ [apply (H2).
+ |apply (Hp).
+ ]]]
+qed.
+
lemma selection:
∀C:ordered_set.∀m:sequence nat_ordered_set.m is_strictly_increasing →
∀a:sequence C.∀u.a ↑ u → (λx.a (m x)) ↑ u.
intros (C m Hm a u Ha); cases Ha (Ia Su); cases Su (Uu Hu); repeat split;
-[1: intro n; simplify; apply trans_increasing; [assumption]
- lapply (Hm n) as W; unfold nat_ordered_set in W; simplify in W;
- cases W;
-|2: intro n;
-|3:
-
\ No newline at end of file
+[1: intro n; simplify; apply trans_increasing; [assumption] apply (Hm n);
+|2: intro n; simplify; apply Uu;
+|3: intros (y Hy); simplify; cases (Hu ? Hy);
+ cases (strictly_increasing_reaches C ? Hm w);
+ exists [apply w1]; cases (os_cotransitive ??? (a (m w1)) H); [2:assumption]
+ cases (trans_increasing C ? Ia ?? H1); assumption;]
+qed. (* dovevo usare il lemma 2.3! *)
+
projects / helm.git / commitdiff