Complete proof of Bertrand for n >= 256.

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

diff --git a/helm/software/matita/library/nat/permutation.ma b/helm/software/matita/library/nat/permutation.ma
index 9ab0358c580b231e7d30b0dc41eaeaa9cd87d7b2..884c18ddc17c0f2a3dafe344c38dabb24160ec38 100644 (file)
--- a/helm/software/matita/library/nat/permutation.ma
+++ b/helm/software/matita/library/nat/permutation.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/permutation".
-
 include "nat/compare.ma".
 include "nat/sigma_and_pi.ma".
 
@@ -73,7 +71,18 @@ match eqb n i with
       match eqb n j with
       [ true \Rightarrow i
       | false \Rightarrow n]].
-      
+
+notation < "(❲i↹j❳)n"
+  right associative with precedence 71 
+for @{ 'transposition $i $j $n}.
+
+notation < "(❲i \atop j❳)n"
+  right associative with precedence 71 
+for @{ 'transposition $i $j $n}.
+
+interpretation "natural transposition" 'transposition i j n =
+  (cic:/matita/nat/permutation/transpose.con i j n).
+
 lemma transpose_i_j_i: \forall i,j:nat. transpose i j i = j.
 intros.unfold transpose.
 rewrite > (eqb_n_n i).simplify. reflexivity.
@@ -609,7 +618,7 @@ apply le_S.apply le_n.assumption.
 apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g 
 (transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) m))) f n)).
 apply (H2 O ? ? (S(m1+i))).
-unfold lt.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.id.
 apply (trans_le ? i).assumption.
 change with (i \le (S m1)+i).apply le_plus_n.
 exact H4.
@@ -683,42 +692,62 @@ theorem permut_to_eq_map_iter_i:\forall f:nat\to nat \to nat.associative nat f \
 symmetric2 nat nat f \to \forall k,n:nat.\forall g,h:nat \to nat.
 permut h (k+n) \to (\forall m:nat. m \lt n \to h m = m) \to
 map_iter_i k g f n = map_iter_i k (\lambda m.g(h m)) f n.
-intros 4.elim k.
-simplify.rewrite > (permut_n_to_eq_n h).reflexivity.assumption.assumption.
-apply (trans_eq ? ? (map_iter_i (S n) (\lambda m.g ((transpose (h (S n+n1)) (S n+n1)) m)) f n1)).
-unfold permut in H3.
-elim H3.
-apply (eq_map_iter_i_transpose2 f H H1 n1 n ? ? g).
-apply (permut_n_to_le h n1 (S n+n1)).
-apply le_plus_n.assumption.assumption.apply le_plus_n.apply le_n.
-apply H5.apply le_n.apply le_plus_n.apply le_n.
-apply (trans_eq ? ? (map_iter_i (S n) (\lambda m.
-(g(transpose (h (S n+n1)) (S n+n1) 
-(transpose (h (S n+n1)) (S n+n1) (h m)))) )f n1)).
-simplify.fold simplify (transpose (h (S n+n1)) (S n+n1) (S n+n1)).
-apply eq_f2.apply eq_f.
-rewrite > transpose_i_j_j.
-rewrite > transpose_i_j_i.
-rewrite > transpose_i_j_j.reflexivity.
-apply (H2 n1 (\lambda m.(g(transpose (h (S n+n1)) (S n+n1) m)))).
-apply permut_S_to_permut_transpose.
-assumption.
-intros.
-unfold transpose.
-rewrite > (not_eq_to_eqb_false (h m) (h (S n+n1))).
-rewrite > (not_eq_to_eqb_false (h m) (S n+n1)).
-simplify.apply H4.assumption.
-rewrite > H4.
-apply lt_to_not_eq.apply (trans_lt ? n1).assumption.
-simplify.unfold lt.apply le_S_S.apply le_plus_n.assumption.
-unfold permut in H3.elim H3.
-simplify.unfold Not.intro.
-apply (lt_to_not_eq m (S n+n1)).apply (trans_lt ? n1).assumption.
-simplify.unfold lt.apply le_S_S.apply le_plus_n.
-unfold injn in H7.
-apply (H7 m (S n+n1)).apply (trans_le ? n1).
-apply lt_to_le.assumption.apply le_plus_n.apply le_n.
-assumption.
-apply eq_map_iter_i.intros.
-rewrite > transpose_transpose.reflexivity.
+intros 4.elim k
+  [simplify.rewrite > (permut_n_to_eq_n h)
+    [reflexivity|assumption|assumption]
+  |apply (trans_eq ? ? (map_iter_i (S n) (\lambda m.g ((transpose (h (S n+n1)) (S n+n1)) m)) f n1))
+    [unfold permut in H3.
+     elim H3.
+     apply (eq_map_iter_i_transpose2 f H H1 n1 n ? ? g)
+      [apply (permut_n_to_le h n1 (S n+n1))
+        [apply le_plus_n|assumption|assumption|apply le_plus_n|apply le_n]
+      |apply H5.apply le_n
+      |apply le_plus_n
+      |apply le_n
+      ]
+    |apply (trans_eq ? ? (map_iter_i (S n) (\lambda m.
+      (g(transpose (h (S n+n1)) (S n+n1) 
+      (transpose (h (S n+n1)) (S n+n1) (h m)))) )f n1))
+      [simplify.fold simplify (transpose (h (S n+n1)) (S n+n1) (S n+n1)).
+       apply eq_f2
+        [apply eq_f.
+         rewrite > transpose_i_j_j.
+         rewrite > transpose_i_j_i.
+         rewrite > transpose_i_j_j.
+         reflexivity.
+        |apply (H2 n1 (\lambda m.(g(transpose (h (S n+n1)) (S n+n1) m))))
+          [apply permut_S_to_permut_transpose.assumption
+          |intros.
+           unfold transpose.
+           rewrite > (not_eq_to_eqb_false (h m) (h (S n+n1)))
+            [rewrite > (not_eq_to_eqb_false (h m) (S n+n1))
+              [simplify.apply H4.assumption
+              |rewrite > H4
+                [apply lt_to_not_eq.
+                 apply (trans_lt ? n1)
+                  [assumption|simplify.unfold lt.apply le_S_S.apply le_plus_n]
+                |assumption
+                ]
+              ]
+            |unfold permut in H3.elim H3.
+             simplify.unfold Not.intro.
+             apply (lt_to_not_eq m (S n+n1))
+              [apply (trans_lt ? n1)
+                [assumption|simplify.unfold lt.apply le_S_S.apply le_plus_n]
+              |unfold injn in H7.
+               apply (H7 m (S n+n1))
+                [apply (trans_le ? n1)
+                  [apply lt_to_le.assumption|apply le_plus_n]
+                |apply le_n
+                |assumption
+                ]
+              ]
+            ]
+          ]
+        ]
+      |apply eq_map_iter_i.intros.
+       rewrite > transpose_transpose.reflexivity
+      ]
+    ]
+  ]
 qed.
\ No newline at end of file