From 0e8bc7cfc6dc7f3bcd1249d4cd35d17366cc42d7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 12 Nov 2007 16:38:46 +0000 Subject: [PATCH] removed dust --- helm/software/matita/dama/ordered_sets.ma | 281 +--------------------- 1 file changed, 1 insertion(+), 280 deletions(-) diff --git a/helm/software/matita/dama/ordered_sets.ma b/helm/software/matita/dama/ordered_sets.ma index b8c6952c7..fe16db53f 100644 --- a/helm/software/matita/dama/ordered_sets.ma +++ b/helm/software/matita/dama/ordered_sets.ma @@ -111,286 +111,7 @@ lapply (exc_coreflexive E) as r; unfold coreflexive in r; |2: lapply (c ?? x H2) as H3; cases H3 (H4 H4); [right; assumption|cases (Lxy H4)]] qed. -theorem mah: ∀E:excedence.∀a,b:E. (a < b) → (b ≰ a). +theorem lt_to_excede: ∀E:excedence.∀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. - --- altro file -opposto TH è assioma per ordine totale. - --- - - - - - - - -record is_order_relation (C:Type) (le:C→C→Prop) (eq:C→C→Prop) : Type ≝ { - or_reflexive: reflexive ? le; - or_transitive: transitive ? le; - or_antisimmetric: antisymmetric ? le eq -}. - -record ordered_set: Type ≝ { - os_carr:> excedence; - os_order_relation_properties:> is_order_relation ? (le os_carr) (apart os_carr) -}. - -ordered_set. - -E - -E - -theorem antisimmetric_to_cotransitive_to_transitive: - ∀C.∀le:relation C. antisimmetric ? le → cotransitive ? le → - transitive ? le. - intros; - unfold transitive; - intros; - elim (c ? ? z H1); - [ assumption - | rewrite < (H ? ? H2 t); - assumption - ]. -qed. - -definition is_increasing ≝ λO:ordered_set.λa:nat→O.∀n:nat.a n ≤ a (S n). -definition is_decreasing ≝ λO:ordered_set.λa:nat→O.∀n:nat.a (S n) ≤ a n. - -definition is_upper_bound ≝ λO:ordered_set.λa:nat→O.λu:O.∀n:nat.a n ≤ u. -definition is_lower_bound ≝ λO:ordered_set.λa:nat→O.λu:O.∀n:nat.u ≤ a n. - -record is_sup (O:ordered_set) (a:nat→O) (u:O) : Prop ≝ - { sup_upper_bound: is_upper_bound O a u; - sup_least_upper_bound: ∀v:O. is_upper_bound O a v → u≤v - }. - -record is_inf (O:ordered_set) (a:nat→O) (u:O) : Prop ≝ - { inf_lower_bound: is_lower_bound O a u; - inf_greatest_lower_bound: ∀v:O. is_lower_bound O a v → v≤u - }. - -record is_bounded_below (O:ordered_set) (a:nat→O) : Type ≝ - { ib_lower_bound: O; - ib_lower_bound_is_lower_bound: is_lower_bound ? a ib_lower_bound - }. - -record is_bounded_above (O:ordered_set) (a:nat→O) : Type ≝ - { ib_upper_bound: O; - ib_upper_bound_is_upper_bound: is_upper_bound ? a ib_upper_bound - }. - -record is_bounded (O:ordered_set) (a:nat→O) : Type ≝ - { ib_bounded_below:> is_bounded_below ? a; - ib_bounded_above:> is_bounded_above ? a - }. - -record bounded_below_sequence (O:ordered_set) : Type ≝ - { bbs_seq:1> nat→O; - bbs_is_bounded_below:> is_bounded_below ? bbs_seq - }. - -record bounded_above_sequence (O:ordered_set) : Type ≝ - { bas_seq:1> nat→O; - bas_is_bounded_above:> is_bounded_above ? bas_seq - }. - -record bounded_sequence (O:ordered_set) : Type ≝ - { bs_seq:1> nat → O; - bs_is_bounded_below: is_bounded_below ? bs_seq; - bs_is_bounded_above: is_bounded_above ? bs_seq - }. - -definition bounded_below_sequence_of_bounded_sequence ≝ - λO:ordered_set.λb:bounded_sequence O. - mk_bounded_below_sequence ? b (bs_is_bounded_below ? b). - -coercion cic:/matita/ordered_sets/bounded_below_sequence_of_bounded_sequence.con. - -definition bounded_above_sequence_of_bounded_sequence ≝ - λO:ordered_set.λb:bounded_sequence O. - mk_bounded_above_sequence ? b (bs_is_bounded_above ? b). - -coercion cic:/matita/ordered_sets/bounded_above_sequence_of_bounded_sequence.con. - -definition lower_bound ≝ - λO:ordered_set.λb:bounded_below_sequence O. - ib_lower_bound ? b (bbs_is_bounded_below ? b). - -lemma lower_bound_is_lower_bound: - ∀O:ordered_set.∀b:bounded_below_sequence O. - is_lower_bound ? b (lower_bound ? b). - intros; - unfold lower_bound; - apply ib_lower_bound_is_lower_bound. -qed. - -definition upper_bound ≝ - λO:ordered_set.λb:bounded_above_sequence O. - ib_upper_bound ? b (bas_is_bounded_above ? b). - -lemma upper_bound_is_upper_bound: - ∀O:ordered_set.∀b:bounded_above_sequence O. - is_upper_bound ? b (upper_bound ? b). - intros; - unfold upper_bound; - apply ib_upper_bound_is_upper_bound. -qed. - -definition lt ≝ λO:ordered_set.λa,b:O.a ≤ b ∧ a ≠ b. - -interpretation "Ordered set lt" 'lt a b = - (cic:/matita/ordered_sets/lt.con _ a b). - -definition reverse_ordered_set: ordered_set → ordered_set. - intros; - apply mk_ordered_set; - [2:apply (λx,y:o.y ≤ x) - | skip - | apply mk_is_order_relation; - [ simplify; - intros; - apply (or_reflexive ? ? o) - | simplify; - intros; - apply (or_transitive ? ? o); - [2: apply H1 - | skip - | assumption - ] - | simplify; - intros; - apply (or_antisimmetric ? ? o); - assumption - ] - ]. -qed. - -interpretation "Ordered set ge" 'geq a b = - (cic:/matita/ordered_sets/os_le.con _ - (cic:/matita/ordered_sets/os_pre_ordered_set.con _ - (cic:/matita/ordered_sets/reverse_ordered_set.con _ _)) a b). - -lemma is_lower_bound_reverse_is_upper_bound: - ∀O:ordered_set.∀a:nat→O.∀l:O. - is_lower_bound O a l → is_upper_bound (reverse_ordered_set O) a l. - intros; - unfold; - intro; - unfold; - unfold reverse_ordered_set; - simplify; - apply H. -qed. - -lemma is_upper_bound_reverse_is_lower_bound: - ∀O:ordered_set.∀a:nat→O.∀l:O. - is_upper_bound O a l → is_lower_bound (reverse_ordered_set O) a l. - intros; - unfold; - intro; - unfold; - unfold reverse_ordered_set; - simplify; - apply H. -qed. - -lemma reverse_is_lower_bound_is_upper_bound: - ∀O:ordered_set.∀a:nat→O.∀l:O. - is_lower_bound (reverse_ordered_set O) a l → is_upper_bound O a l. - intros; - unfold in H; - unfold reverse_ordered_set in H; - apply H. -qed. - -lemma reverse_is_upper_bound_is_lower_bound: - ∀O:ordered_set.∀a:nat→O.∀l:O. - is_upper_bound (reverse_ordered_set O) a l → is_lower_bound O a l. - intros; - unfold in H; - unfold reverse_ordered_set in H; - apply H. -qed. - - -lemma is_inf_to_reverse_is_sup: - ∀O:ordered_set.∀a:bounded_below_sequence O.∀l:O. - is_inf O a l → is_sup (reverse_ordered_set O) a l. - intros; - apply (mk_is_sup (reverse_ordered_set O)); - [ apply is_lower_bound_reverse_is_upper_bound; - apply inf_lower_bound; - assumption - | intros; - change in v with (os_carrier O); - change with (v ≤ l); - apply (inf_greatest_lower_bound ? ? ? H); - apply reverse_is_upper_bound_is_lower_bound; - assumption - ]. -qed. - -lemma is_sup_to_reverse_is_inf: - ∀O:ordered_set.∀a:bounded_above_sequence O.∀l:O. - is_sup O a l → is_inf (reverse_ordered_set O) a l. - intros; - apply (mk_is_inf (reverse_ordered_set O)); - [ apply is_upper_bound_reverse_is_lower_bound; - apply sup_upper_bound; - assumption - | intros; - change in v with (os_carrier O); - change with (l ≤ v); - apply (sup_least_upper_bound ? ? ? H); - apply reverse_is_lower_bound_is_upper_bound; - assumption - ]. -qed. - -lemma reverse_is_sup_to_is_inf: - ∀O:ordered_set.∀a:bounded_above_sequence O.∀l:O. - is_sup (reverse_ordered_set O) a l → is_inf O a l. - intros; - apply mk_is_inf; - [ apply reverse_is_upper_bound_is_lower_bound; - change in l with (os_carrier (reverse_ordered_set O)); - apply sup_upper_bound; - assumption - | intros; - change in l with (os_carrier (reverse_ordered_set O)); - change in v with (os_carrier (reverse_ordered_set O)); - change with (os_le (reverse_ordered_set O) l v); - apply (sup_least_upper_bound ? ? ? H); - change in v with (os_carrier O); - apply is_lower_bound_reverse_is_upper_bound; - assumption - ]. -qed. - -lemma reverse_is_inf_to_is_sup: - ∀O:ordered_set.∀a:bounded_above_sequence O.∀l:O. - is_inf (reverse_ordered_set O) a l → is_sup O a l. - intros; - apply mk_is_sup; - [ apply reverse_is_lower_bound_is_upper_bound; - change in l with (os_carrier (reverse_ordered_set O)); - apply (inf_lower_bound ? ? ? H) - | intros; - change in l with (os_carrier (reverse_ordered_set O)); - change in v with (os_carrier (reverse_ordered_set O)); - change with (os_le (reverse_ordered_set O) v l); - apply (inf_greatest_lower_bound ? ? ? H); - change in v with (os_carrier O); - apply is_upper_bound_reverse_is_lower_bound; - assumption - ]. -qed. - -record cotransitively_ordered_set: Type := - { cos_ordered_set :> ordered_set; - cos_cotransitive: cotransitive ? (os_le cos_ordered_set) - }. -- 2.39.2