...

[helm.git] / helm / software / matita / library / nat / generic_iter_p.ma

diff --git a/helm/software/matita/library/nat/generic_iter_p.ma b/helm/software/matita/library/nat/generic_iter_p.ma
index 249957f1b3bc44453e46caf4099361818b4cbbff..28ef391eb4e6790124601cba297cf7a7ea16c467 100644 (file)
--- a/helm/software/matita/library/nat/generic_iter_p.ma
+++ b/helm/software/matita/library/nat/generic_iter_p.ma
@@ -12,8 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/generic_iter_p".
-
+include "nat/div_and_mod_diseq.ma".
 include "nat/primes.ma".
 include "nat/ord.ma".
 
@@ -47,8 +46,6 @@ rewrite > H.
 reflexivity.
 qed.
 
-
-
 theorem false_to_iter_p_gen_Sn: 
 \forall n:nat. \forall p:nat \to bool. \forall A:Type. \forall g:nat \to A.
 \forall baseA:A. \forall plusA: A \to A \to A.
@@ -59,7 +56,6 @@ rewrite > H.
 reflexivity.
 qed.
 
-
 theorem eq_iter_p_gen: \forall p1,p2:nat \to bool. \forall A:Type.
 \forall g1,g2: nat \to A. \forall baseA: A. 
 \forall plusA: A \to A \to A. \forall n:nat.
@@ -162,8 +158,7 @@ iter_p_gen (k + n) p A g baseA plusA
 intros.
 
 elim k
-[ rewrite < (plus_n_O n).
-  simplify.
+[ simplify.
   rewrite > H in \vdash (? ? ? %).
   rewrite > (H1 ?).
   reflexivity
@@ -287,8 +282,7 @@ elim n
           rewrite > sym_plus.
           rewrite > (div_plus_times ? ? ? H5).
           rewrite > (mod_plus_times ? ? ? H5).
-          rewrite > H4.
-          simplify.reflexivity.   
+          reflexivity.   
         ]
       | reflexivity
       ]
@@ -370,8 +364,7 @@ elim n
           rewrite > sym_plus.
           rewrite > (div_plus_times ? ? ? H5).
           rewrite > (mod_plus_times ? ? ? H5).
-          rewrite > H4.
-          simplify.reflexivity.   
+          reflexivity.   
         ]
       | reflexivity
       ]
@@ -708,9 +701,38 @@ elim n
 ]
 qed.
 
-
-(* da spostare *)
-
+theorem eq_iter_p_gen_pred: 
+\forall A:Type.
+\forall baseA: A.
+\forall plusA: A \to A \to A.
+\forall n,p,g.
+p O = true \to
+(symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a  baseA) = a) \to
+iter_p_gen (S n) (\lambda i.p (pred i)) A (\lambda i.g(pred i)) baseA plusA = 
+plusA (iter_p_gen n p A g baseA plusA) (g O).
+intros.
+elim n
+  [rewrite > true_to_iter_p_gen_Sn
+    [simplify.apply H1
+    |assumption
+    ]
+  |apply (bool_elim ? (p n1));intro
+    [rewrite > true_to_iter_p_gen_Sn
+      [rewrite > true_to_iter_p_gen_Sn in ⊢ (? ? ? %)
+        [rewrite > H2 in ⊢ (? ? ? %).
+         apply eq_f.assumption
+        |assumption
+        ]
+      |assumption
+      ]
+    |rewrite > false_to_iter_p_gen_Sn
+      [rewrite > false_to_iter_p_gen_Sn in ⊢ (? ? ? %);assumption
+      |assumption
+      ]
+    ]
+  ]
+qed.
+    
 definition p_ord_times \def
 \lambda p,m,x.
   match p_ord x p with
@@ -749,23 +771,6 @@ elim (le_to_or_lt_eq O ? (le_O_n m))
   ]
 qed.
 
-(* lemmino da postare *)
-theorem lt_times_to_lt_div: \forall i,n,m. i < n*m \to i/m < n.
-intros.
-cut (O < m)
-  [apply (lt_times_n_to_lt m)
-    [assumption
-    |apply (le_to_lt_to_lt ? i)
-      [rewrite > (div_mod i m) in \vdash (? ? %).
-       apply le_plus_n_r.
-       assumption
-      |assumption
-      ]
-    ]
-  |apply (lt_times_to_lt_O ? ? ? H)
-  ]
-qed.
-
 theorem iter_p_gen_knm:
 \forall A:Type.
 \forall baseA: A.
@@ -1563,7 +1568,10 @@ apply (trans_eq ? ?
                 [ assumption
                 | assumption
                 ]
-              | rewrite > H14.
+              | unfold ha.
+                unfold ha12.
+                unfold ha22.
+                rewrite > H14.
                 rewrite > H13.
                 apply sym_eq.
                 apply div_mod.
@@ -1610,18 +1618,23 @@ apply (trans_eq ? ?
                 rewrite > Hcut.
                 assumption
               ] 
-            | rewrite > Hcut1.
+            | unfold ha.
+              unfold ha12.
+              rewrite > Hcut1.
               rewrite > Hcut.
               assumption
             ]
-          | rewrite > Hcut1.
+          | unfold ha.
+            unfold ha22.
+            rewrite > Hcut1.
             rewrite > Hcut.
             assumption            
           ]
         | cut(O \lt m1)
           [ cut(O \lt n1)      
             [ apply (lt_to_le_to_lt ? ((h11 i j)*m1 + m1) )
-              [ apply (lt_plus_r).
+              [ unfold ha.
+                apply (lt_plus_r).
                 assumption
               | rewrite > sym_plus.
                 rewrite > (sym_times (h11 i j) m1).
@@ -1747,7 +1760,4 @@ apply (iter_p_gen_2_eq A baseA plusA H H1 H2 (\lambda x,y. g x y) (\lambda x,y.y
     |assumption
     ]
   ]
-qed.
-
-
-
+qed.
\ No newline at end of file