notation factored, coercion commant taking terms and not only URI

[helm.git] / helm / software / matita / contribs / dama / dama / models / nat_dedekind_sigma_complete.ma

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 0908b6f7079ae8f2acf97cfac5758717b3124054..bc009b5c6fc6bcdb67dee6c63d84ddd7e819eed4 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
@@ -28,14 +28,16 @@ cases (nat_compare n m); intros;
 [constructor 1|constructor 2|constructor 3] assumption;
 qed.
 
-alias symbol "pi1" = "exT fst".
+alias symbol "pi1" = "exT \fst".
 alias symbol "leq" = "natural 'less or equal to'".
 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).
+    ∀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:ℕ.(u≤i ∧ s = fst (a j)) ∨ (i < u ∧ s+i ≤ u + fst (a j))); (* s - aj <= max 0 (u - i) *)  
+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) *)  
 letin m ≝ (hide ? (
   let rec aux i ≝
     match i with
@@ -43,10 +45,10 @@ letin m ≝ (hide ? (
     | S m ⇒ 
         let pred ≝ aux m in
         let apred ≝ a pred in 
-        match cmp_nat (fst apred) s with
+        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)]]
+        | cmp_lt nP ⇒ \fst (H3 apred nP)]]
   in aux 
    :
    ∀i:nat.∃j:nat.spec i j));unfold spec in aux ⊢ %;
@@ -59,7 +61,7 @@ letin m ≝ (hide ? (
         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));
+        |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));
@@ -79,21 +81,21 @@ letin m ≝ (hide ? (
             [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)));
+                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)));
+                    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));
+                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));
+                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;
+                    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;
@@ -101,20 +103,20 @@ letin find ≝ (
  let rec find i u on u : nat ≝
   match u with
   [ O ⇒ (m i:nat)
-  | S w ⇒ match eqb (fst (a (m i))) s with
+  | S w ⇒ match eqb (\fst (a (m i))) s with
           [ true ⇒ (m i:nat)
           | false ⇒ find (S i) w]]
  in find
  :
-  ∀i,bound.∃j.i + bound = u → s = fst (a j));
-[1: cases (find (S n) n2); intro; change with (s = fst (a w));
+  ∀i,bound.∃j.i + bound = u → s = \fst (a j));
+[1: cases (find (S n) n2); intro; change with (s = \fst (a w));
     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 (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));
+exists [apply w]; intros; change with (s = \fst (a j));
 rewrite > (H4 ?); [2: reflexivity]
 apply le_to_le_to_eq;
 [1: apply os_le_to_nat_le;
@@ -123,8 +125,9 @@ apply le_to_le_to_eq;
     rewrite < (H4 ?); [2: reflexivity] apply le_n;]
 qed.
 
-alias symbol "pi1" = "exT fst".
+alias symbol "pi1" = "exT \fst".
 alias symbol "leq" = "natural 'less or equal to'".
+alias symbol "nat" = "ordered set N".
 axiom nat_dedekind_sigma_complete_r:
   ∀l,u:ℕ.∀a:sequence {[l,u]}.a is_decreasing → 
-    ∀x.x is_infimum a → ∃i.∀j.i ≤ j → fst x = fst (a j).
+    ∀x.x is_infimum a → ∃i.∀j.i ≤ j → \fst x = \fst (a j).