From: Enrico Tassi Date: Tue, 15 Jul 2008 10:16:06 +0000 (+0000) Subject: models over N fixed X-Git-Tag: make_still_working~4928 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=aba6841906f09875a5800f58b24862444a1f4baf;p=helm.git models over N fixed --- diff --git a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma index f9de36d1f..bd528521d 100644 --- a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma +++ b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma @@ -62,7 +62,7 @@ interpretation "constructive quaternary and" 'and4 x y z t = (And4 x y z t). inductive exT (A:Type) (P:A→CProp) : CProp ≝ ex_introT: ∀w:A. P w → exT A P. -record sigT (A:Type) (P:A→CProp) : Type ≝ { +record sigT (A:Type) (P:A→Prop) : Type ≝ { fstT:A; sndT:P fstT }. diff --git a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma index 220601745..7bb312aff 100644 --- a/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma +++ b/helm/software/matita/contribs/dama/dama/models/nat_dedekind_sigma_complete.ma @@ -17,7 +17,7 @@ include "supremum.ma". include "nat/le_arith.ma". include "russell_support.ma". -alias symbol "pi1" = "exT \fst". +alias symbol "pi1" = "sigT \fst". alias symbol "leq" = "natural 'less or equal to'". lemma nat_dedekind_sigma_complete: ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_increasing → @@ -26,7 +26,9 @@ intros 5; cases x (s Hs); clear x; letin X ≝ (〈s,Hs〉); fold normalize X; intros; cases H1; alias symbol "plus" = "natural plus". alias symbol "nat" = "Uniform space N". -letin spec ≝ (λi,j:ℕ.(u≤i ∧ s = \fst (a j)) ∨ (i < u ∧ s+i ≤ u + \fst (a j))); (* s - aj <= max 0 (u - i) *) +alias symbol "and" = "logical and". +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 @@ -34,15 +36,13 @@ letin m ≝ (hide ? ( | 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)]] + match cmp_nat s (\fst apred) with + [ cmp_le _ ⇒ pred + | cmp_gt nP ⇒ \fst (H3 apred ?)]] in aux : - ∀i:nat.∃j:nat.spec i j));unfold spec in aux ⊢ %; -[1: apply (H2 pred nP); -|4: unfold X in H2; clear H4 n aux spec H3 H1 H X; + ∀i:nat.∃j:nat.spec i j));[whd; apply nP;] unfold spec in aux ⊢ %; +[3: unfold X in H2; clear H4 n aux spec H3 H1 H X; cases u in H2 Hs a ⊢ %; intros (a Hs H); [1: left; split; [apply le_n] generalize in match H; @@ -55,38 +55,38 @@ letin m ≝ (hide ? ( |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; +|2: clear H6; cut (s = \fst (a (aux n1))); [2: + cases (le_to_or_lt_eq ?? H5); [2: assumption] + cases (?:False); apply (H2 (aux n1) H6);] clear H5; + generalize in match Hcut; clear Hcut; intro H5; +|1: clear H6] +[2,1: cases (aux n1) in H5 ⊢ %; 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: cases (?: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 ??? 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; try assumption; - [1: rewrite > sym_plus in ⊢ (? ? %); - rewrite < H6; apply le_plus_r; assumption; - |2: cases (H3 (a w) H6); - change with (s + S n1 ≤ u + \fst (a w1));rewrite < plus_n_Sm; - apply (trans_le ??? (le_S_S ?? H8)); rewrite > plus_n_Sm; - apply (le_plus ???? (le_n ?) H9);]]]]] + |*: cases (cmp_nat u (S n1)); + [1,3: left; split; [1,3: assumption |2: 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 ??? 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; try assumption; + [1: rewrite > sym_plus in ⊢ (? ? %); + rewrite < H6; apply le_plus_r; assumption; + |2: cases (H3 (a w) H6); + change with (s + S n1 ≤ u + \fst (a w1));rewrite < plus_n_Sm; + apply (trans_le ??? (le_S_S ?? H8)); rewrite > plus_n_Sm; + apply (le_plus ???? (le_n ?) H9);]]]] clearbody m; unfold spec in m; clear spec; letin find ≝ ( let rec find i u on u : nat ≝ @@ -114,7 +114,7 @@ apply le_to_le_to_eq; rewrite < (H4 ?); [2: reflexivity] apply le_n;] qed. -alias symbol "pi1" = "exT \fst". +alias symbol "pi1" = "sigT \fst". alias symbol "leq" = "natural 'less or equal to'". alias symbol "nat" = "ordered set N". axiom nat_dedekind_sigma_complete_r: