From 0538bf9e109bbd963816e20254213a5df114ce84 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 16 Jun 2008 15:24:57 +0000 Subject: [PATCH] Dedekind sigma completeness for the natural numbers. --- .../matita/contribs/dama/dama/depends | 17 +- .../contribs/dama/dama/models/uniformnat.ma | 238 +++++++----------- 2 files changed, 93 insertions(+), 162 deletions(-) diff --git a/helm/software/matita/contribs/dama/dama/depends b/helm/software/matita/contribs/dama/dama/depends index 99165ee70..f2a739aa7 100644 --- a/helm/software/matita/contribs/dama/dama/depends +++ b/helm/software/matita/contribs/dama/dama/depends @@ -1,20 +1,21 @@ -property_sigma.ma ordered_uniform.ma russell_support.ma bishop_set.ma ordered_set.ma -ordered_uniform.ma uniform.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 +uniform.ma supremum.ma +supremum.ma datatypes/constructors.ma nat/plus.ma nat_ordered_set.ma sequence.ma nat_ordered_set.ma bishop_set.ma nat/compare.ma -lebesgue.ma property_exhaustivity.ma sandwich.ma +property_sigma.ma ordered_uniform.ma russell_support.ma +ordered_uniform.ma uniform.ma property_exhaustivity.ma ordered_uniform.ma property_sigma.ma -cprop_connectives.ma logic/equality.ma -ordered_set.ma cprop_connectives.ma +lebesgue.ma property_exhaustivity.ma sandwich.ma sandwich.ma ordered_uniform.ma russell_support.ma cprop_connectives.ma nat/nat.ma -uniform.ma supremum.ma -supremum.ma datatypes/constructors.ma nat/plus.ma nat_ordered_set.ma sequence.ma -models/uniformnat.ma bishop_set_rewrite.ma nat_ordered_set.ma ordered_uniform.ma russell_support.ma uniform.ma +models/uniformnat.ma bishop_set_rewrite.ma nat/le_arith.ma nat_ordered_set.ma ordered_uniform.ma russell_support.ma uniform.ma datatypes/constructors.ma logic/equality.ma nat/compare.ma +nat/le_arith.ma nat/nat.ma nat/plus.ma diff --git a/helm/software/matita/contribs/dama/dama/models/uniformnat.ma b/helm/software/matita/contribs/dama/dama/models/uniformnat.ma index 824d6c293..d1c90dcd6 100644 --- a/helm/software/matita/contribs/dama/dama/models/uniformnat.ma +++ b/helm/software/matita/contribs/dama/dama/models/uniformnat.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "nat/le_arith.ma". include "nat_ordered_set.ma". include "bishop_set_rewrite.ma". include "uniform.ma". @@ -50,8 +51,6 @@ notation "\naturals" non associative with precedence 99 for @{'nat}. interpretation "naturals" 'nat = nat. interpretation "Ordered set N" 'nat = nat_ordered_set. -include "russell_support.ma". - inductive cmp_cases (n,m:nat) : CProp ≝ | cmp_lt : n < m → cmp_cases n m | cmp_eq : n = m → cmp_cases n m @@ -76,8 +75,8 @@ lemma key: intros; cases (cmp_nat n m); [assumption |generalize in match H1; rewrite < H2; intros; - cases (not_lt_n_n (fst (a n))); apply os_lt_to_nat_lt; apply H3; -|cases (not_lt_n_n (fst (a m))); + cases (Not_lt_n_n (fst (a n))); apply os_lt_to_nat_lt; apply H3; +|cases (Not_lt_n_n (fst (a m))); apply (trans_le_lt_lt ? (fst (a n))); [2: apply os_lt_to_nat_lt; apply H1; |1: apply os_le_to_nat_le; apply (trans_increasing ?? H m n); @@ -95,14 +94,16 @@ split; cases Hcut1; assumption] qed. +include "russell_support.ma". + alias symbol "pi1" = "exT fst". lemma nat_dedekind_sigma_complete: ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing → ∀x.x is_supremum a → ∃i.∀j.i ≤ j → fst x = fst (a j). intros 5; cases x (s Hs); clear x; letin X ≝ (〈s,Hs〉); fold normalize X; intros; cases H1; -letin spec ≝ (λi,j.fst (a j) = s ∨ (i ≤ j ∧ match i with [ O ⇒ fst (a j) = fst (a O) | S m ⇒ fst(a m) < fst (a j)])); -letin m ≝ ( +letin spec ≝ (λi,j.(u≤i ∧ s = fst (a j)) ∨ (i < u ∧ s+i ≤ u + fst (a j))); (* s - aj <= max 0 (u - i) *) +letin m ≝ (hide ? ( let rec aux i ≝ match i with [ O ⇒ O @@ -115,35 +116,72 @@ letin m ≝ ( | cmp_lt nP ⇒ fst (H3 apred nP)]] in aux : - ∀i:nat.∃j:nat.spec i j);unfold spec in aux ⊢ %; + ∀i:nat.∃j:nat.spec i j));unfold spec in aux ⊢ %; [1: apply (H2 pred nP); -|4: right; split; whd; constructor 1; -|2,3: whd in ⊢ (? ? %); - [1: left; assumption - |2: elim (H3 (a (aux n1)) H5) (res_n); - change with (fst (a res_n) = s ∨ (n1 < res_n ∧ fst (a n1) < fst (a res_n))); - change in H7 with (fst (a (aux n1)) < fst (a res_n)); - elim (aux n1) in H7 ⊢ % (pred); - change in H8 with (fst (a pred) < fst (a res_n)); - cases H7; clear H7; - [ left; apply le_to_le_to_eq; - [ apply os_le_to_nat_le; apply (H2 res_n); - | rewrite < H9; apply le_S_S_to_le; apply le_S; apply H8;] - | cases H9; clear H9; right; split; - [ lapply (trans_increasing ?? H n1 pred (nat_le_to_os_le ?? H7)) as H11; - clear H6; apply (key ??? H); - apply (le_lt_transitive ?? (a pred)); [assumption] - generalize in match H8; cases (a pred); cases (a res_n); - simplify; intro D; lapply (nat_lt_to_os_lt ?? D) as Q; - cases Q; clear D Q; split; assumption; - | generalize in match H10; generalize in match H7; clear H7 H10; - cases n1; intros; - [ rewrite < H9; assumption - | clear H9; apply (trans_le_lt_lt ??? ? H8); - apply os_le_to_nat_le; lapply (nat_le_to_os_le ?? H7) as H77; - apply(trans_increasing ?? H (S n2) (pred) H77);]]]]] +|4: unfold X in H2; clear H4 n aux spec H3 H1 H X; + generalize in match H2; + generalize in match Hs; + generalize in match a; + clear H2 Hs a; cases u; intros (a Hs H); + [1: left; split; [apply le_n] + generalize in match H; + generalize in match Hs; + rewrite > (?:s = O); + [2: cases Hs; lapply (os_le_to_nat_le ?? H1); + apply (symmetric_eq nat O s ?).apply (le_n_O_to_eq s ?).apply (Hletin). + |1: intros; lapply (os_le_to_nat_le (fst (a O)) O (H2 O)); + lapply (le_n_O_to_eq ? Hletin); assumption;] + |2: right; cases Hs; rewrite > (sym_plus s O); split; [apply le_S_S; apply le_O_n]; + apply (trans_le ??? (os_le_to_nat_le ?? H1)); + apply le_plus_n_r;] +|2,3: clear H6; + generalize in match H5; clear H5; cases (aux n1); intros; + change in match (a 〈w,H5〉) in H6 ⊢ % with (a w); + cases H5; clear H5; cases H7; clear H7; + [1: left; + split; + [ apply (le_S ?? H5) + | assumption] + |3: elimType False; + rewrite < H8 in H6; + apply (not_le_Sn_n ? H6) + |*: cut (u ≤ S n1 ∨ S n1 < u); + [2,4: cases (cmp_nat u (S n1)); + [1,4: left; apply lt_to_le; assumption + |2,5: rewrite > H7; left; apply le_n + |3,6: right; assumption ] + |*: cases Hcut; clear Hcut + [1,3: left; split; [1,3: assumption |2: symmetry; assumption] + cut (u = S n1); [2: apply le_to_le_to_eq; assumption ] + clear H7 H5 H4;rewrite > Hcut in H8:(? ? (? % ?)); clear Hcut; + cut (s = S (fst (a w))) + [2: apply le_to_le_to_eq; + [2:assumption + | change in H8 with (s + n1 ≤ S (n1 + fst (a w))); + rewrite > plus_n_Sm in H8; + rewrite > sym_plus in H8; + apply le_plus_to_le [2: apply H8]] + | cases (H3 (a w) H6); + change with (s = fst (a w1)); + change in H4 with (fst (a w) < fst (a w1)); + apply le_to_le_to_eq; + [ rewrite > Hcut; + assumption + | apply (os_le_to_nat_le (fst (a w1)) s (H2 w1));]] + |*: right; split; + [1,3: assumption + |2: rewrite > sym_plus in ⊢ (? ? %); + rewrite < H6; + apply le_plus_r; + assumption + | cases (H3 (a w) H6); + change with (s + S n1 ≤ u + fst (a w1)); + rewrite < plus_n_Sm; + apply (trans_le ? (S (u + fst (a w)))); [ apply le_S_S; assumption] + rewrite > plus_n_Sm; + apply le_plus; [ apply le_n ] + apply H9]]]]] clearbody m; unfold spec in m; clear spec; -cut (∀i.fst (a (m i)) = s ∨ i ≤ fst (a (m i))) as key2;[ letin find ≝ ( let rec find i u on u : nat ≝ match u with @@ -158,127 +196,18 @@ letin find ≝ ( apply H6; rewrite < H7; simplify; apply plus_n_Sm; |2: intros; rewrite > (eqb_true_to_eq ?? H5); reflexivity |3: intros; rewrite > sym_plus in H5; rewrite > H5; clear H5 H4 n n1; - cases (key2 u); [symmetry;assumption] - cases Hs; apply le_to_le_to_eq;[2:change with (fst (a (m u)) ≤ fst X); apply os_le_to_nat_le; apply (H2 (m u));] - apply (trans_le ??? (os_le_to_nat_le ?? H5) H4); -|4: clearbody find; cases (find O u); - exists [apply w]; intros; change with (s = fst (a j)); - rewrite > (H4 ?); [2: reflexivity] - apply le_to_le_to_eq; [apply os_le_to_nat_le; - apply (trans_increasing ?? H ? ? (nat_le_to_os_le ?? H5));] - apply (trans_le ? s ?);[apply os_le_to_nat_le; apply (H2 j);] - rewrite < (H4 ?); [2: reflexivity] apply le_n;]] -alias symbol "pi1" (instance 15) = "exT fst". -alias symbol "pi1" (instance 10) = "exT fst". -alias symbol "pi1" (instance 7) = "exT fst". -alias symbol "pi1" (instance 4) = "exT fst". -alias symbol "nat" = "naturals". -cut (∀i.fst (a (fst (m i))) = s - ∨ - i ≤ fst (m i) - ∧ - match i in nat return λn:ℕ.Prop with  - [O⇒ fst (a (fst(m i))) = fst (a O) - |S (w:ℕ)⇒fst (a w) < fst (a (fst(m i)))]) as mitico;[2: - intro; cases (m i); apply H4;] -cut (∀i.fst (a (m i)) = s ∨ fst (a (m i)) < fst (a (m (S i))));[2: - intro; - cases (mitico (S i)); - [2: cases (mitico i); - [2: cases H5 (H6 _); cases H4 (_ H7); clear H4 H5; - change in H7 with (fst (a i) < fst (a (fst (m (S i))))); - right; - - - generalize in match (mitico i); clear mitico; - - - cases (m i); intros; cases H5; clear H5; - [left; assumption] - cases H6; clear H6; simplify in H7; - - change with (fst (a w)=s ∨ a w H5; apply (H2 (m O)); - | - |2: cases H5; clear H5; change in H6 with (fst (a O) < fst (a w)); - right; split; [change with (le nat_ordered_set (fst (a (m O))) (fst (a w))); - apply nat_le_to_os_le; apply le_S_S_to_le; apply le_S; - (* apply H6; *) - |]] - - - - cases (m O); change with (fst (a w) = s ∨ a w < a (m (S O))); - cases H4[left; assumption] cases H5; clear H4 H5; - change in H7 with (fst (a w) = fst (a O)); - - -intro; elim i; [1: right; apply le_O_n;] -generalize in match (refl_eq ? (S n):S n = S n); -generalize in match (S n) in ⊢ (? ? ? % → %); intro R; -cases (m R); intros; change with (fst (a w) = s ∨ R ≤ fst (a w)); -rewrite < H6 in H5 ⊢ %; clear H6 R; cases H5; [left; assumption] -cases H6; clear H6 H5; change in H8 with (fst (a n) < fst (a w)); -lapply (key l u a H n w); - -w = m (S n) - - - -STOP - - -letin m ≝ ( - let rec aux i ≝ - match i with - [ O ⇒ - let a0 ≝ a O in - match cmp_nat (fst a0) s with - [ cmp_eq _ ⇒ O - | cmp_gt nP ⇒ match ? in False return λ_.nat with [] - | cmp_lt nP ⇒ fst (H3 a0 nP)] - | S m ⇒ - let pred ≝ aux m in - let apred ≝ a pred in - match cmp_nat (fst apred) s with - [ cmp_eq _ ⇒ pred - | cmp_gt nP ⇒ match ? in False return λ_.nat with [] - | cmp_lt nP ⇒ - - fst (H3 apred nP)]] - in aux - : - ∀i:nat.∃j:nat.spec i j);unfold spec in aux ⊢ %; -[1: apply (H2 O nP); -|2: apply (H2 pred nP); -|5: left; assumption; -|6: right; cases (H3 (a O) H5); change with (fst (a O) < fst (a w)); - apply H7; -|4: right; elim (H3 (a (aux n1)) H5); change with (fst (a (S n1)) < fst (a a1)); - rewrite < H4; elim (aux n1) in H7 ⊢ %; elim H7 in H8; clear H7; - simplify in H9; - -|3: clear H6; generalize in match H5; cases (aux n1); intros; clear H5; - simplify - - -STOP - + cases (m u); cases H4; clear H4; cases H5; clear H5; [assumption] + cases (not_le_Sn_n ? H4) +] +clearbody find; cases (find O u); +exists [apply w]; intros; change with (s = fst (a j)); +rewrite > (H4 ?); [2: reflexivity] +apply le_to_le_to_eq; + [ apply os_le_to_nat_le; + apply (trans_increasing ?? H ? ? (nat_le_to_os_le ?? H5)); + | apply (trans_le ? s ?);[apply os_le_to_nat_le; apply (H2 j);] + rewrite < (H4 ?); [2: reflexivity] apply le_n;] +qed. definition nat_uniform_space: uniform_space. apply (discrete_uniform_space_of_bishop_set ℕ); @@ -306,3 +235,4 @@ cases (H10 (sig_in ?? x1 H2)); exists [1,3:apply x1] intros; apply H6; + -- 2.39.2