X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcontribs%2Fdama%2Fdama%2Fclassical_pointfree%2Fordered_sets.ma;fp=matita%2Fcontribs%2Fdama%2Fdama%2Fclassical_pointfree%2Fordered_sets.ma;h=2630da77c6474b93a99281982f1edc229ff27ae8;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/matita/contribs/dama/dama/classical_pointfree/ordered_sets.ma b/matita/contribs/dama/dama/classical_pointfree/ordered_sets.ma
new file mode 100644
index 000000000..2630da77c
--- /dev/null
+++ b/matita/contribs/dama/dama/classical_pointfree/ordered_sets.ma
@@ -0,0 +1,424 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 is_dedekind_sigma_complete (O:excess) : Type ≝
+ { dsc_inf: ∀a:nat→O.∀m:O. is_lower_bound ? a m → ex ? (λs:O.is_inf O a s);
+   dsc_inf_proof_irrelevant:
+    ∀a:nat→O.∀m,m':O.∀p:is_lower_bound ? a m.∀p':is_lower_bound ? a m'.
+     (match dsc_inf a m p with [ ex_intro s _ ⇒ s ]) =
+     (match dsc_inf a m' p' with [ ex_intro s' _ ⇒ s' ]); 
+   dsc_sup: ∀a:nat→O.∀m:O. is_upper_bound ? a m → ex ? (λs:O.is_sup O a s);
+   dsc_sup_proof_irrelevant:
+    ∀a:nat→O.∀m,m':O.∀p:is_upper_bound ? a m.∀p':is_upper_bound ? a m'.
+     (match dsc_sup a m p with [ ex_intro s _ ⇒ s ]) =
+     (match dsc_sup a m' p' with [ ex_intro s' _ ⇒ s' ])    
+ }.
+
+record dedekind_sigma_complete_ordered_set : Type ≝
+ { dscos_ordered_set:> excess;
+   dscos_dedekind_sigma_complete_properties:>
+    is_dedekind_sigma_complete dscos_ordered_set
+ }.
+
+definition inf:
+ ∀O:dedekind_sigma_complete_ordered_set.
+  bounded_below_sequence O → O.
+ intros;
+ elim
+  (dsc_inf O (dscos_dedekind_sigma_complete_properties O) b);
+  [ apply a
+  | apply (lower_bound ? b)
+  | apply lower_bound_is_lower_bound
+  ]
+qed.
+
+lemma inf_is_inf:
+ ∀O:dedekind_sigma_complete_ordered_set.
+  ∀a:bounded_below_sequence O.
+   is_inf ? a (inf ? a).
+ intros;
+ unfold inf;
+ simplify;
+ elim (dsc_inf O (dscos_dedekind_sigma_complete_properties O) a
+(lower_bound O a) (lower_bound_is_lower_bound O a));
+ simplify;
+ assumption.
+qed.
+
+lemma inf_proof_irrelevant:
+ ∀O:dedekind_sigma_complete_ordered_set.
+  ∀a,a':bounded_below_sequence O.
+   bbs_seq ? a = bbs_seq ? a' →
+    inf ? a = inf ? a'.
+ intros 3;
+ elim a 0;
+ elim a';
+ simplify in H;
+ generalize in match i1;
+ clear i1;
+ rewrite > H;
+ intro;
+ simplify;
+ rewrite < (dsc_inf_proof_irrelevant O O f (ib_lower_bound ? f i)
+  (ib_lower_bound ? f i2) (ib_lower_bound_is_lower_bound ? f i)
+  (ib_lower_bound_is_lower_bound ? f i2));
+ reflexivity.
+qed.
+
+definition sup:
+ ∀O:dedekind_sigma_complete_ordered_set.
+  bounded_above_sequence O → O.
+ intros;
+ elim
+  (dsc_sup O (dscos_dedekind_sigma_complete_properties O) b);
+  [ apply a
+  | apply (upper_bound ? b)
+  | apply upper_bound_is_upper_bound
+  ].
+qed.
+
+lemma sup_is_sup:
+ ∀O:dedekind_sigma_complete_ordered_set.
+  ∀a:bounded_above_sequence O.
+   is_sup ? a (sup ? a).
+ intros;
+ unfold sup;
+ simplify;
+ elim (dsc_sup O (dscos_dedekind_sigma_complete_properties O) a
+(upper_bound O a) (upper_bound_is_upper_bound O a));
+ simplify;
+ assumption.
+qed.
+
+lemma sup_proof_irrelevant:
+ ∀O:dedekind_sigma_complete_ordered_set.
+  ∀a,a':bounded_above_sequence O.
+   bas_seq ? a = bas_seq ? a' →
+    sup ? a = sup ? a'.
+ intros 3;
+ elim a 0;
+ elim a';
+ simplify in H;
+ generalize in match i1;
+ clear i1;
+ rewrite > H;
+ intro;
+ simplify;
+ rewrite < (dsc_sup_proof_irrelevant O O f (ib_upper_bound ? f i2)
+  (ib_upper_bound ? f i) (ib_upper_bound_is_upper_bound ? f i2)
+  (ib_upper_bound_is_upper_bound ? f i));
+ reflexivity.
+qed.
+
+axiom daemon: False.
+
+theorem inf_le_sup:
+ ∀O:dedekind_sigma_complete_ordered_set.
+  ∀a:bounded_sequence O. inf ? a ≤ sup ? a.
+ intros (O');
+ apply (or_transitive ? ? O' ? (a O));
+  [ elim daemon (*apply (inf_lower_bound ? ? ? ? (inf_is_inf ? ? a))*)
+  | elim daemon (*apply (sup_upper_bound ? ? ? ? (sup_is_sup ? ? a))*)
+  ].
+qed.
+
+lemma inf_respects_le:
+ ∀O:dedekind_sigma_complete_ordered_set.
+  ∀a:bounded_below_sequence O.∀m:O.
+   is_upper_bound ? a m → inf ? a ≤ m.
+ intros (O');
+ apply (or_transitive ? ? O' ? (sup ? (mk_bounded_sequence ? a ? ?)));
+  [ apply (bbs_is_bounded_below ? a)
+  | apply (mk_is_bounded_above ? ? m H)
+  | apply inf_le_sup 
+  | apply
+     (sup_least_upper_bound ? ? ?
+      (sup_is_sup ? (mk_bounded_sequence O' a a
+        (mk_is_bounded_above O' a m H))));
+    assumption
+  ].
+qed. 
+
+definition is_sequentially_monotone ≝
+ λO:excess.λf:O→O.
+  ∀a:nat→O.∀p:is_increasing ? a.
+   is_increasing ? (λi.f (a i)).
+
+record is_order_continuous
+ (O:dedekind_sigma_complete_ordered_set) (f:O→O) : Prop
+≝
+ { ioc_is_sequentially_monotone: is_sequentially_monotone ? f;
+   ioc_is_upper_bound_f_sup:
+    ∀a:bounded_above_sequence O.
+     is_upper_bound ? (λi.f (a i)) (f (sup ? a));
+   ioc_respects_sup:
+    ∀a:bounded_above_sequence O.
+     is_increasing ? a →
+      f (sup ? a) =
+       sup ? (mk_bounded_above_sequence ? (λi.f (a i))
+        (mk_is_bounded_above ? ? (f (sup ? a))
+         (ioc_is_upper_bound_f_sup a)));
+   ioc_is_lower_bound_f_inf:
+    ∀a:bounded_below_sequence O.
+     is_lower_bound ? (λi.f (a i)) (f (inf ? a));
+   ioc_respects_inf:
+    ∀a:bounded_below_sequence O.
+     is_decreasing ? a →
+      f (inf ? a) =
+       inf ? (mk_bounded_below_sequence ? (λi.f (a i))
+        (mk_is_bounded_below ? ? (f (inf ? a))
+         (ioc_is_lower_bound_f_inf a)))   
+ }.
+
+theorem tail_inf_increasing:
+ ∀O:dedekind_sigma_complete_ordered_set.
+  ∀a:bounded_below_sequence O.
+   let y ≝ λi.mk_bounded_below_sequence ? (λj.a (i+j)) ? in
+   let x ≝ λi.inf ? (y i) in
+    is_increasing ? x.
+ [ apply (mk_is_bounded_below ? ? (ib_lower_bound ? a a));
+   simplify;
+   intro;
+   apply (ib_lower_bound_is_lower_bound ? a a)
+ | intros;
+   unfold is_increasing;
+   intro;
+   unfold x in ⊢ (? ? ? %);
+   apply (inf_greatest_lower_bound ? ? ? (inf_is_inf ? (y (S n))));
+   change with (is_lower_bound ? (y (S n)) (inf ? (y n)));
+   unfold is_lower_bound;
+   intro;
+   generalize in match (inf_lower_bound ? ? ? (inf_is_inf ? (y n)) (S n1));
+   (*CSC: coercion per FunClass inserita a mano*)
+   suppose (inf ? (y n) ≤ bbs_seq ? (y n) (S n1)) (H);
+   cut (bbs_seq ? (y n) (S n1) = bbs_seq ? (y (S n)) n1);
+    [ rewrite < Hcut;
+      assumption
+    | unfold y;
+      simplify;
+      autobatch paramodulation library
+    ]
+ ].
+qed.
+
+definition is_liminf:
+ ∀O:dedekind_sigma_complete_ordered_set.
+  bounded_below_sequence O → O → Prop.
+ intros;
+ apply
+  (is_sup ? (λi.inf ? (mk_bounded_below_sequence ? (λj.b (i+j)) ?)) t);
+ apply (mk_is_bounded_below ? ? (ib_lower_bound ? b b));
+ simplify;
+ intros;
+ apply (ib_lower_bound_is_lower_bound ? b b).
+qed.  
+
+definition liminf:
+ ∀O:dedekind_sigma_complete_ordered_set.
+  bounded_sequence O → O.
+ intros;
+ apply
+  (sup ?
+   (mk_bounded_above_sequence ?
+     (λi.inf ?
+       (mk_bounded_below_sequence ?
+         (λj.b (i+j)) ?)) ?));
+  [ apply (mk_is_bounded_below ? ? (ib_lower_bound ? b b));
+    simplify;
+    intros;
+    apply (ib_lower_bound_is_lower_bound ? b b)
+  | apply (mk_is_bounded_above ? ? (ib_upper_bound ? b b));
+    unfold is_upper_bound;
+    intro;
+    change with
+     (inf O
+  (mk_bounded_below_sequence O (\lambda j:nat.b (n+j))
+   (mk_is_bounded_below O (\lambda j:nat.b (n+j)) (ib_lower_bound O b b)
+    (\lambda j:nat.ib_lower_bound_is_lower_bound O b b (n+j))))
+\leq ib_upper_bound O b b);
+    apply (inf_respects_le O);
+    simplify;
+    intro;
+    apply (ib_upper_bound_is_upper_bound ? b b)
+  ].
+qed.
+
+
+definition reverse_dedekind_sigma_complete_ordered_set:
+ dedekind_sigma_complete_ordered_set → dedekind_sigma_complete_ordered_set.
+ intros;
+ apply mk_dedekind_sigma_complete_ordered_set;
+  [ apply (reverse_ordered_set d)
+  | elim daemon
+    (*apply mk_is_dedekind_sigma_complete;
+     [ intros;
+       elim (dsc_sup ? ? d a m) 0;
+        [ generalize in match H; clear H;
+          generalize in match m; clear m;
+          elim d;
+          simplify in a1;
+          simplify;
+          change in a1 with (Type_OF_ordered_set ? (reverse_ordered_set ? o)); 
+          apply (ex_intro ? ? a1);
+          simplify in H1;
+          change in m with (Type_OF_ordered_set ? o);
+          apply (is_sup_to_reverse_is_inf ? ? ? ? H1)
+        | generalize in match H; clear H;
+          generalize in match m; clear m;
+          elim d;
+          simplify;
+          change in t with (Type_OF_ordered_set ? o);
+          simplify in t;
+          apply reverse_is_lower_bound_is_upper_bound;
+          assumption
+        ]
+     | apply is_sup_reverse_is_inf;
+     | apply m
+     | 
+     ]*)
+  ].
+qed.
+
+definition reverse_bounded_sequence:
+ ∀O:dedekind_sigma_complete_ordered_set.
+  bounded_sequence O →
+   bounded_sequence (reverse_dedekind_sigma_complete_ordered_set O).
+ intros;
+ apply mk_bounded_sequence;
+  [ apply bs_seq;
+    unfold reverse_dedekind_sigma_complete_ordered_set;
+    simplify;
+    elim daemon
+  | elim daemon
+  | elim daemon
+  ].
+qed.
+
+definition limsup ≝
+ λO:dedekind_sigma_complete_ordered_set.
+  λa:bounded_sequence O.
+   liminf (reverse_dedekind_sigma_complete_ordered_set O)
+    (reverse_bounded_sequence O a).
+
+notation "hvbox(〈a〉)"
+ non associative with precedence 45
+for @{ 'hide_everything_but $a }.
+
+interpretation "mk_bounded_above_sequence" 'hide_everything_but a
+= (cic:/matita/classical_pointfree/ordered_sets/bounded_above_sequence.ind#xpointer(1/1/1) _ _ a _).
+
+interpretation "mk_bounded_below_sequence" 'hide_everything_but a
+= (cic:/matita/classical_pointfree/ordered_sets/bounded_below_sequence.ind#xpointer(1/1/1) _ _ a _).
+
+theorem eq_f_sup_sup_f:
+ ∀O':dedekind_sigma_complete_ordered_set.
+  ∀f:O'→O'. ∀H:is_order_continuous ? f.
+   ∀a:bounded_above_sequence O'.
+    ∀p:is_increasing ? a.
+     f (sup ? a) = sup ? (mk_bounded_above_sequence ? (λi.f (a i)) ?).
+ [ apply (mk_is_bounded_above ? ? (f (sup ? a))); 
+   apply ioc_is_upper_bound_f_sup;
+   assumption
+ | intros;
+   apply ioc_respects_sup;
+   assumption
+ ].
+qed.
+
+theorem eq_f_sup_sup_f':
+ ∀O':dedekind_sigma_complete_ordered_set.
+  ∀f:O'→O'. ∀H:is_order_continuous ? f.
+   ∀a:bounded_above_sequence O'.
+    ∀p:is_increasing ? a.
+     ∀p':is_bounded_above ? (λi.f (a i)).
+      f (sup ? a) = sup ? (mk_bounded_above_sequence ? (λi.f (a i)) p').
+ intros;
+ rewrite > (eq_f_sup_sup_f ? f H a H1);
+ apply sup_proof_irrelevant;
+ reflexivity.
+qed.
+
+theorem eq_f_liminf_sup_f_inf:
+ ∀O':dedekind_sigma_complete_ordered_set.
+  ∀f:O'→O'. ∀H:is_order_continuous ? f.
+   ∀a:bounded_sequence O'.
+   let p1 := ? in
+    f (liminf ? a) =
+     sup ?
+      (mk_bounded_above_sequence ?
+        (λi.f (inf ?
+          (mk_bounded_below_sequence ?
+            (λj.a (i+j))
+            ?)))
+        p1).
+ [ apply (mk_is_bounded_below ? ? (ib_lower_bound ? a a));
+   simplify;
+   intro;
+   apply (ib_lower_bound_is_lower_bound ? a a)
+ | apply (mk_is_bounded_above ? ? (f (sup ? a)));
+   unfold is_upper_bound;
+   intro;
+   apply (or_transitive ? ? O' ? (f (a n)));
+    [ generalize in match (ioc_is_lower_bound_f_inf ? ? H);
+      intro H1;
+      simplify in H1;
+      rewrite > (plus_n_O n) in ⊢ (? ? ? (? (? ? ? %)));
+      apply (H1 (mk_bounded_below_sequence O' (\lambda j:nat.a (n+j))
+(mk_is_bounded_below O' (\lambda j:nat.a (n+j)) (ib_lower_bound O' a a)
+ (\lambda j:nat.ib_lower_bound_is_lower_bound O' a a (n+j)))) O);
+    | elim daemon (*apply (ioc_is_upper_bound_f_sup ? ? ? H)*)
+    ]
+ | intros;
+   unfold liminf;
+   clearbody p1;
+   generalize in match (\lambda n:nat
+.inf_respects_le O'
+ (mk_bounded_below_sequence O' (\lambda j:nat.a (plus n j))
+  (mk_is_bounded_below O' (\lambda j:nat.a (plus n j))
+   (ib_lower_bound O' a a)
+   (\lambda j:nat.ib_lower_bound_is_lower_bound O' a a (plus n j))))
+ (ib_upper_bound O' a a)
+ (\lambda n1:nat.ib_upper_bound_is_upper_bound O' a a (plus n n1)));
+   intro p2;
+   apply (eq_f_sup_sup_f' ? f H (mk_bounded_above_sequence O'
+(\lambda i:nat
+ .inf O'
+  (mk_bounded_below_sequence O' (\lambda j:nat.a (plus i j))
+   (mk_is_bounded_below O' (\lambda j:nat.a (plus i j))
+    (ib_lower_bound O' a a)
+    (\lambda n:nat.ib_lower_bound_is_lower_bound O' a a (plus i n)))))
+(mk_is_bounded_above O'
+ (\lambda i:nat
+  .inf O'
+   (mk_bounded_below_sequence O' (\lambda j:nat.a (plus i j))
+    (mk_is_bounded_below O' (\lambda j:nat.a (plus i j))
+     (ib_lower_bound O' a a)
+     (\lambda n:nat.ib_lower_bound_is_lower_bound O' a a (plus i n)))))
+ (ib_upper_bound O' a a) p2)));
+   unfold bas_seq;
+   change with
+    (is_increasing ? (\lambda i:nat
+.inf O'
+ (mk_bounded_below_sequence O' (\lambda j:nat.a (plus i j))
+  (mk_is_bounded_below O' (\lambda j:nat.a (plus i j))
+   (ib_lower_bound O' a a)
+   (\lambda n:nat.ib_lower_bound_is_lower_bound O' a a (plus i n))))));
+   apply tail_inf_increasing
+ ].
+qed.
+