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 f9de36d1fa4a33fef91473d4f11d43bc86c0c7fd..bd528521dba3e8ea456a501256f8f5f93ef91800 100644 (file)
--- 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 2206017452995e0bc2d815dd0244da9838a1ddae..7bb312aff0284a0a6bef069af9d5fe19e4115a18 100644 (file)
--- 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: