]> matita.cs.unibo.it Git - helm.git/commitdiff
Renamed iterative into map_iter_p and moved around a few theorems.
authorAndrea Asperti <andrea.asperti@unibo.it>
Mon, 18 Dec 2006 11:52:57 +0000 (11:52 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Mon, 18 Dec 2006 11:52:57 +0000 (11:52 +0000)
matita/library/nat/euler_theorem.ma
matita/library/nat/gcd.ma
matita/library/nat/iteration.ma [deleted file]
matita/library/nat/map_iter_p.ma [new file with mode: 0644]
matita/library/nat/orders.ma

index 0655fb968e0c33fefdf9bec7947f780c4a2fec9b..d58f7c2b06668c70c87fe20d67a4244b1f1738cd 100644 (file)
 
 set "baseuri" "cic:/matita/nat/euler_theorem".
 
-include "nat/iteration.ma".
+include "nat/map_iter_p.ma".
 include "nat/totient.ma".
 
-(* da spostare *)
-lemma le_to_le_to_eq: \forall n,m. n \le m \to m \le n \to n = m.
-apply nat_elim2
-  [intros.apply le_n_O_to_eq.assumption
-  |intros.apply sym_eq.apply le_n_O_to_eq.assumption
-  |intros.apply eq_f.apply H
-    [apply le_S_S_to_le.assumption
-    |apply le_S_S_to_le.assumption
-    ]
-  ]
-qed.
-
-lemma gcd_n_n: \forall n.gcd n n = n.
-intro.elim n
-  [reflexivity
-  |apply le_to_le_to_eq
-    [apply divides_to_le
-      [apply lt_O_S
-      |apply divides_gcd_n
-      ]
-    |apply divides_to_le
-      [apply lt_O_gcd.apply lt_O_S
-      |apply divides_d_gcd
-        [apply divides_n_n|apply divides_n_n]
-      ]
-    ]
-  ]
-qed.
-
-
-lemma count_card: \forall p.\forall n.
-p O = false \to count (S n) p = card n p.
-intros.elim n
-  [simplify.rewrite > H. reflexivity
-  |simplify.
-   rewrite < plus_n_O.
-   apply eq_f.assumption
-  ]
-qed.
-
-lemma count_card1: \forall p.\forall n.
-p O = false \to p n = false \to count n p = card n p.
-intros 3.apply (nat_case n)
-  [intro.simplify.rewrite > H. reflexivity
-  |intros.rewrite > (count_card ? ? H).
-   simplify.rewrite > H1.reflexivity
-  ]
-qed.
+(* a reformulation of totient using card insted of count *)
 lemma totient_card: \forall n. 
 totient n = card n (\lambda i.eqb (gcd i n) (S O)).
 intro.apply (nat_case n)
@@ -80,106 +32,50 @@ intro.apply (nat_case n)
   ]
 qed.
 
-(* da spostare *)
-lemma gcd_n_times_nm: \forall n,m. O < m \to gcd n (n*m) = n.
-intro.apply (nat_case n)
-  [intros.reflexivity
-  |intros.
-   apply le_to_le_to_eq
-    [apply divides_to_le
-      [apply lt_O_S|apply divides_gcd_n]
-    |apply divides_to_le
-      [apply lt_O_gcd.rewrite > (times_n_O O).
-       apply lt_times[apply lt_O_S|assumption]
-      |apply divides_d_gcd
-        [apply (witness ? ? m1).reflexivity
-        |apply divides_n_n
-        ]
-      ]
-    ]
-  ]
-qed.
-
-(* da spostare *)
-lemma eq_gcd_SO_to_not_divides: \forall n,m. (S O) < n \to 
-(gcd n m) = (S O) \to \lnot (divides n m).
-intros.unfold.intro.
-elim H2.
-generalize in match H1.
-rewrite > H3.
-intro.
-cut (O < n2)
-  [elim (gcd_times_SO_to_gcd_SO n n n2 ? ? H4)
-    [cut (gcd n (n*n2) = n)
-      [apply (lt_to_not_eq (S O) n)
-        [assumption|rewrite < H4.assumption]
-      |apply gcd_n_times_nm.assumption
-      ]
-    |apply (trans_lt ? (S O))[apply le_n|assumption]
-    |assumption
-    ]
-  |elim (le_to_or_lt_eq O n2 (le_O_n n2))
-    [assumption
-    |apply False_ind.
-     apply (le_to_not_lt n (S O))
-      [rewrite < H4.
-       apply divides_to_le
-        [rewrite > H4.apply lt_O_S
-        |apply divides_d_gcd
-          [apply (witness ? ? n2).reflexivity
-          |apply divides_n_n
-          ]
-        ]
-      |assumption
-      ]
-    ]
-  ]
-qed.
-
-theorem gcd_Pi_P: \forall n,k. O < k \to k \le n \to
-gcd n (Pi_P (\lambda i.eqb (gcd i n) (S O)) k) = (S O).
+theorem gcd_pi_p: \forall n,k. O < k \to k \le n \to
+gcd n (pi_p (\lambda i.eqb (gcd i n) (S O)) k) = (S O).
 intros 3.elim H
-  [rewrite > Pi_P_S.
+  [rewrite > pi_p_S.
    cut (eqb (gcd (S O) n) (S O) = true)
     [rewrite > Hcut.
      change with ((gcd n (S O)) = (S O)).auto
     |apply eq_to_eqb_true.auto
     ]
-  |rewrite > Pi_P_S.
+  |rewrite > pi_p_S.
    apply eqb_elim
     [intro.
      change with 
-       ((gcd n ((S n1)*(Pi_P (\lambda i.eqb (gcd i n) (S O)) n1))) = (S O)).
+       ((gcd n ((S n1)*(pi_p (\lambda i.eqb (gcd i n) (S O)) n1))) = (S O)).
      apply eq_gcd_times_SO
       [unfold.apply le_S.assumption
-      |apply lt_O_Pi_P.
+      |apply lt_O_pi_p.
       |rewrite > sym_gcd. assumption.
       |apply H2.
        apply (trans_le ? (S n1))[apply le_n_Sn|assumption]
       ]
     |intro.
      change with 
-       (gcd n (Pi_P (\lambda i.eqb (gcd i n) (S O)) n1) = (S O)).
+       (gcd n (pi_p (\lambda i.eqb (gcd i n) (S O)) n1) = (S O)).
      apply H2.
      apply (trans_le ? (S n1))[apply le_n_Sn|assumption]
     ]
   ]
 qed.
 
-theorem congruent_map_iter_P_times:\forall f:nat \to nat. \forall a,n:nat.
+theorem congruent_map_iter_p_times:\forall f:nat \to nat. \forall a,n:nat.
 O < a \to
 congruent
-(map_iter_P n (\lambda i.eqb (gcd i a) (S O)) (\lambda x.f x) (S O) times)
-(map_iter_P n (\lambda i.eqb (gcd i a) (S O)) 
+(map_iter_p n (\lambda i.eqb (gcd i a) (S O)) (\lambda x.f x) (S O) times)
+(map_iter_p n (\lambda i.eqb (gcd i a) (S O)) 
  (\lambda x.f x \mod a) (S O) times) a.     
 intros.
 elim n
-  [rewrite > map_iter_P_O.
+  [rewrite > map_iter_p_O.
    apply (congruent_n_n ? a)
   |apply (eqb_elim (gcd (S n1) a) (S O))
     [intro.
-     rewrite > map_iter_P_S_true
-      [rewrite > map_iter_P_S_true
+     rewrite > map_iter_p_S_true
+      [rewrite > map_iter_p_S_true
         [apply congruent_times
           [assumption
           |apply congruent_n_mod_n.assumption
@@ -190,8 +86,8 @@ elim n
       |apply eq_to_eqb_true.assumption
       ]
     |intro. 
-     rewrite > map_iter_P_S_false
-      [rewrite > map_iter_P_S_false
+     rewrite > map_iter_p_S_false
+      [rewrite > map_iter_p_S_false
         [assumption
         |apply not_eq_to_eqb_false.assumption
         ]
@@ -201,44 +97,6 @@ elim n
   ]
 qed.
 
-theorem lt_S_to_lt: \forall n,m. S n < m \to n < m.
-intros.
-apply (trans_lt ? (S n))
-  [apply le_n|assumption]
-qed.
-
-theorem gcd_SO_to_lt_O: \forall i,n. (S O) < n \to gcd i n = (S O) \to
-O < i.
-intros.
-elim (le_to_or_lt_eq ? ? (le_O_n i))
-  [assumption
-  |absurd ((gcd i n) = (S O))
-    [assumption
-    |rewrite < H2.
-     simplify.
-     unfold.intro.
-     apply (lt_to_not_eq (S O) n H).
-     apply sym_eq.assumption
-    ]
-  ]
-qed.
-
-theorem gcd_SO_to_lt_n: \forall i,n. (S O) < n \to i \le n \to gcd i n = (S O) \to
-i < n.
-intros.
-elim (le_to_or_lt_eq ? ? H1)
-  [assumption
-  |absurd ((gcd i n) = (S O))
-    [assumption
-    |rewrite > H3.
-     rewrite > gcd_n_n.
-     unfold.intro.
-     apply (lt_to_not_eq (S O) n H).
-     apply sym_eq.assumption
-    ]
-  ]
-qed.
-
 theorem permut_p_mod: \forall a,n. S O < n \to O < a \to gcd a n = (S O) \to
 permut_p (\lambda x:nat.a*x \mod n) (\lambda i:nat.eqb (gcd i n) (S O)) n.
 intros.
@@ -335,9 +193,9 @@ cut (O < a)
   [apply divides_to_congruent
     [apply (trans_lt ? (S O)).apply lt_O_S. assumption
     |change with (O < exp a (totient n)).apply lt_O_exp.assumption
-    |apply (gcd_SO_to_divides_times_to_divides (Pi_P (\lambda i.eqb (gcd i n) (S O)) n))
+    |apply (gcd_SO_to_divides_times_to_divides (pi_p (\lambda i.eqb (gcd i n) (S O)) n))
       [apply (trans_lt ? (S O)).apply lt_O_S. assumption
-      |apply gcd_Pi_P
+      |apply gcd_pi_p
         [apply (trans_lt ? (S O)).apply lt_O_S. assumption
         |apply le_n
         ]
@@ -346,17 +204,17 @@ cut (O < a)
        rewrite > (sym_times (S O)).
        rewrite < times_n_SO.
        rewrite > totient_card.
-       rewrite > a_times_Pi_P.
+       rewrite > a_times_pi_p.
        apply congruent_to_divides
         [apply (trans_lt ? (S O)).apply lt_O_S. assumption
         | apply (transitive_congruent n ? 
-                 (map_iter_P n (\lambda i.eqb (gcd i n) (S O)) (\lambda x.a*x \mod n) (S O) times))
-          [apply (congruent_map_iter_P_times ? n n).
+                 (map_iter_p n (\lambda i.eqb (gcd i n) (S O)) (\lambda x.a*x \mod n) (S O) times))
+          [apply (congruent_map_iter_p_times ? n n).
            apply (trans_lt ? (S O))
             [apply lt_O_S|assumption]
-            |unfold Pi_P.
-             cut ( (map_iter_P n (\lambda i:nat.eqb (gcd i n) (S O)) (\lambda n:nat.n) (S O) times)
-                 = (map_iter_P n (\lambda i:nat.eqb (gcd i n) (S O)) (\lambda x:nat.a*x\mod n) (S O) times))
+            |unfold pi_p.
+             cut ( (map_iter_p n (\lambda i:nat.eqb (gcd i n) (S O)) (\lambda n:nat.n) (S O) times)
+                 = (map_iter_p n (\lambda i:nat.eqb (gcd i n) (S O)) (\lambda x:nat.a*x\mod n) (S O) times))
               [rewrite < Hcut1.apply congruent_n_n
               |apply (eq_map_iter_p_permut ? ? ? ? ? (λm.m))
                 [apply assoc_times
index cb29da2f87aa67edaf100a3b2533db05e82e1dde..6da8e13d02780dd627233655593f7dcedf311e2c 100644 (file)
@@ -384,6 +384,74 @@ rewrite < H4 in \vdash (? ? %).assumption.
 intros.unfold lt.apply le_S_S.apply le_O_n.
 qed.
 
+theorem gcd_n_n: \forall n.gcd n n = n.
+intro.elim n
+  [reflexivity
+  |apply le_to_le_to_eq
+    [apply divides_to_le
+      [apply lt_O_S
+      |apply divides_gcd_n
+      ]
+    |apply divides_to_le
+      [apply lt_O_gcd.apply lt_O_S
+      |apply divides_d_gcd
+        [apply divides_n_n|apply divides_n_n]
+      ]
+    ]
+  ]
+qed.
+
+theorem gcd_SO_to_lt_O: \forall i,n. (S O) < n \to gcd i n = (S O) \to
+O < i.
+intros.
+elim (le_to_or_lt_eq ? ? (le_O_n i))
+  [assumption
+  |absurd ((gcd i n) = (S O))
+    [assumption
+    |rewrite < H2.
+     simplify.
+     unfold.intro.
+     apply (lt_to_not_eq (S O) n H).
+     apply sym_eq.assumption
+    ]
+  ]
+qed.
+
+theorem gcd_SO_to_lt_n: \forall i,n. (S O) < n \to i \le n \to gcd i n = (S O) \to
+i < n.
+intros.
+elim (le_to_or_lt_eq ? ? H1)
+  [assumption
+  |absurd ((gcd i n) = (S O))
+    [assumption
+    |rewrite > H3.
+     rewrite > gcd_n_n.
+     unfold.intro.
+     apply (lt_to_not_eq (S O) n H).
+     apply sym_eq.assumption
+    ]
+  ]
+qed.
+
+theorem  gcd_n_times_nm: \forall n,m. O < m \to gcd n (n*m) = n.
+intro.apply (nat_case n)
+  [intros.reflexivity
+  |intros.
+   apply le_to_le_to_eq
+    [apply divides_to_le
+      [apply lt_O_S|apply divides_gcd_n]
+    |apply divides_to_le
+      [apply lt_O_gcd.rewrite > (times_n_O O).
+       apply lt_times[apply lt_O_S|assumption]
+      |apply divides_d_gcd
+        [apply (witness ? ? m1).reflexivity
+        |apply divides_n_n
+        ]
+      ]
+    ]
+  ]
+qed.
+
 theorem symmetric_gcd: symmetric nat gcd.
 (*CSC: bug here: unfold symmetric does not work *)
 change with 
@@ -440,6 +508,41 @@ qed.
 
 (* for the "converse" of the previous result see the end  of this development *)
 
+theorem eq_gcd_SO_to_not_divides: \forall n,m. (S O) < n \to 
+(gcd n m) = (S O) \to \lnot (divides n m).
+intros.unfold.intro.
+elim H2.
+generalize in match H1.
+rewrite > H3.
+intro.
+cut (O < n2)
+  [elim (gcd_times_SO_to_gcd_SO n n n2 ? ? H4)
+    [cut (gcd n (n*n2) = n)
+      [apply (lt_to_not_eq (S O) n)
+        [assumption|rewrite < H4.assumption]
+      |apply gcd_n_times_nm.assumption
+      ]
+    |apply (trans_lt ? (S O))[apply le_n|assumption]
+    |assumption
+    ]
+  |elim (le_to_or_lt_eq O n2 (le_O_n n2))
+    [assumption
+    |apply False_ind.
+     apply (le_to_not_lt n (S O))
+      [rewrite < H4.
+       apply divides_to_le
+        [rewrite > H4.apply lt_O_S
+        |apply divides_d_gcd
+          [apply (witness ? ? n2).reflexivity
+          |apply divides_n_n
+          ]
+        ]
+      |assumption
+      ]
+    ]
+  ]
+qed.
+
 theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O).
 intro.
 apply antisym_le.apply divides_to_le.unfold lt.apply le_n.
diff --git a/matita/library/nat/iteration.ma b/matita/library/nat/iteration.ma
deleted file mode 100644 (file)
index 404cbbd..0000000
+++ /dev/null
@@ -1,904 +0,0 @@
-(**************************************************************************)
-(*       ___                                                             *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
-(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU Lesser General Public License Version 2.1         *)
-(*                                                                        *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/nat/iteration.ma".
-
-include "nat/permutation.ma".
-include "nat/count.ma".
-
-lemma le_to_le_to_eq: \forall n,m. n \le m \to m \le n \to n = m.
-apply nat_elim2
-  [intros.apply le_n_O_to_eq.assumption
-  |intros.apply sym_eq.apply le_n_O_to_eq.assumption
-  |intros.apply eq_f.apply H
-    [apply le_S_S_to_le.assumption
-    |apply le_S_S_to_le.assumption
-    ]
-  ]
-qed.
-
-let rec map_iter_P n p (g:nat \to nat) (a:nat) f \def
-  match n with
-   [ O \Rightarrow a
-   | (S k) \Rightarrow 
-      match p (S k) with
-      [true \Rightarrow f (g (S k)) (map_iter_P k p g a f)
-      |false \Rightarrow map_iter_P k p g a f]
-   ].
-
-theorem eq_map_iter_P: \forall g1,g2:nat \to nat.
-\forall p:nat \to bool.
-\forall f:nat \to nat \to nat. \forall a,n:nat.
-(\forall m:nat. m \le n \to g1 m = g2 m) \to 
-map_iter_P n p g1 a f = map_iter_P n p g2 a f.
-intros 6.elim n
-  [simplify.reflexivity.
-  |simplify.elim (p (S n1))
-    [simplify.apply eq_f2
-      [apply H1.apply le_n
-      |simplify.apply H.intros.apply H1.
-       apply le_S.assumption
-      ]
-    |simplify.apply H.intros.apply H1.
-     apply le_S.assumption
-    ]
- ]
-qed.
-
-(* useful since simply simpifies too much *)
-
-theorem map_iter_P_O: \forall p.\forall g.\forall f. \forall a:nat.
-map_iter_P O p g a f = a.
-intros.simplify.reflexivity.
-qed.
-
-theorem map_iter_P_S_true: \forall p.\forall g.\forall f. \forall a,n:nat.
-p (S n) = true \to 
-map_iter_P (S n) p g a f = f (g (S n)) (map_iter_P n p g a f).
-intros.simplify.rewrite > H.reflexivity.
-qed.
-
-theorem map_iter_P_S_false: \forall p.\forall g.\forall f. \forall a,n:nat.
-p (S n) = false \to 
-map_iter_P (S n) p g a f = map_iter_P n p g a f.
-intros.simplify.rewrite > H.reflexivity.
-qed.
-
-(* map_iter examples *)
-definition Pi_P \def \lambda p. \lambda n.
-map_iter_P n p (\lambda n.n) (S O) times.
-
-lemma Pi_P_S: \forall n.\forall p.
-Pi_P p (S n) = 
-  match p (S n) with
-    [true \Rightarrow (S n)*(Pi_P p n)
-    |false \Rightarrow (Pi_P p n)
-    ].
-intros.reflexivity.
-qed.
-
-lemma lt_O_Pi_P: \forall n.\forall p.
-O < Pi_P p n.
-intros.elim n
-  [simplify.apply le_n
-  |rewrite > Pi_P_S.
-   elim p (S n1)
-    [change with (O < (S n1)*(Pi_P p n1)).
-     rewrite >(times_n_O n1).
-     apply lt_times[apply le_n|assumption]
-    | assumption
-    ]
-  ]
-qed.
-
-let rec card n p \def 
-  match n with
-  [O \Rightarrow O
-  |(S m) \Rightarrow 
-      (bool_to_nat (p (S m))) + (card m p)].
-lemma a_times_Pi_P: \forall p. \forall a,n.
-exp a (card n p) * Pi_P p n = map_iter_P n p (\lambda n.a*n) (S O) times.
-intros.elim n
-  [simplify.reflexivity
-  |simplify.apply (bool_elim ? (p (S n1)))
-    [intro.
-     change with 
-      (a*exp a (card n1 p) * ((S n1) * (Pi_P p n1)) = 
-       a*(S n1)*map_iter_P n1 p (\lambda n.a*n) (S O) times).
-       rewrite < H.
-       auto
-    |intro.assumption
-    ]
-  ]
-qed.
-
-definition permut_p \def \lambda f. \lambda p:nat\to bool. \lambda n.
-\forall i. i \le n \to p i = true \to ((f i \le n \land p (f i) = true)
-\land (\forall j. p j = true \to j \le n \to i \neq j \to (f i \neq f j))).
-
-definition extentional_eq_n \def \lambda f,g:nat \to nat.\lambda n.
-\forall x. x \le n \to f x = g x.
-
-lemma extentional_eq_n_to_permut_p: \forall f,g. \forall p. \forall n. 
-extentional_eq_n f g n\to permut_p f p n \to permut_p g p n.
-intros.unfold permut_p.
-intros.
-elim (H1 i H2 H3).
-split
-  [elim H4.split
-    [rewrite < (H  i H2).assumption
-    |rewrite < (H  i H2).assumption
-    ]
-  |intros.
-   unfold.intro.apply (H5 j H6 H7 H8).
-     rewrite > (H  i H2).
-     rewrite > (H  j H7).assumption
-  ]
-qed.
-
-theorem permut_p_compose: \forall f,g.\forall p.\forall n.
-permut_p f p n \to permut_p g p n \to permut_p (compose  ? ? ? g f) p n.
-intros.unfold permut_p.intros.
-elim (H i H2 H3).
-elim H4.
-elim (H1 (f i) H6 H7).
-elim H8.
-split
-  [split
-    [unfold compose.assumption
-    |unfold compose.rewrite < H11.reflexivity
-    ]
-  |intros.
-   unfold compose.
-   apply (H9 (f j))
-    [elim (H j H13 H12).elim H15.rewrite < H18.reflexivity
-    |elim (H j H13 H12).elim H15.assumption.
-    |apply (H5 j H12 H13 H14)
-    ]
-  ]
-qed.
-
-theorem permut_p_S_to_permut_p: \forall f.\forall p.\forall n.
-permut_p f p (S n) \to (f (S n)) = (S n) \to permut_p f p n.
-intros.
-unfold permut_p.
-intros.
-split
-  [elim (H i (le_S i n H2) H3).split
-    [elim H4.
-     elim (le_to_or_lt_eq (f i) (S n))
-      [apply le_S_S_to_le.assumption
-      |absurd (f i = (S n))
-        [assumption
-        |rewrite < H1.
-         apply H5
-          [rewrite < H8.assumption
-          |apply le_n
-          |unfold.intro.rewrite > H8 in H2.
-           apply (not_le_Sn_n n).rewrite < H9.assumption
-          ]   
-        ]
-      |assumption
-      ]
-    |elim H4.assumption
-    ]
-  |intros.
-   elim (H i (le_S i n H2) H3).
-   apply H8
-    [assumption|apply le_S.assumption|assumption]
-  ]
-qed.
-
-lemma permut_p_transpose: \forall p.\forall i,j,n.
-i \le n \to j \le n \to p i = p j \to
-permut_p (transpose i j) p n.
-unfold permut_p.intros.
-split
-  [split
-    [unfold transpose.
-     apply (eqb_elim i1 i)
-      [intro.
-       apply (eqb_elim i1 j)
-        [simplify.intro.assumption
-        |simplify.intro.assumption
-        ]
-      |intro.
-       apply (eqb_elim i1 j)
-        [simplify.intro.assumption
-        |simplify.intro.assumption
-        ]
-      ]
-    |unfold transpose.
-     apply (eqb_elim i1 i)
-      [intro.
-       apply (eqb_elim i1 j)
-        [simplify.intro.rewrite < H6.assumption
-        |simplify.intro.rewrite < H2.rewrite < H5.assumption
-        ]
-      |intro.
-       apply (eqb_elim i1 j)
-        [simplify.intro.rewrite > H2.rewrite < H6.assumption
-        |simplify.intro.assumption
-        ]
-      ]
-    ]
-  |intros.unfold Not.
-   intro.apply H7.
-   apply (injective_transpose ? ? ? ? H8).
-  ]
-qed.
-
-theorem eq_map_iter_P_k: \forall f,g.\forall p.\forall a,k,n:nat.
-p (S n-k) = true \to (\forall i. (S n)-k < i \to i \le (S n) \to (p i) = false) \to
-map_iter_P (S n) p g a f = map_iter_P (S n-k) p g a f.
-intros 5.
-elim k 3
-  [rewrite < minus_n_O.reflexivity
-  |apply (nat_case n1)
-    [intros.
-     rewrite > map_iter_P_S_false
-      [reflexivity
-      |apply H2[simplify.apply lt_O_S.|apply le_n]
-      ]
-    |intros.
-     rewrite > map_iter_P_S_false
-      [rewrite > (H m H1)
-        [reflexivity
-        |intros.
-         apply (H2 i H3).
-         apply le_S.
-         assumption
-        ]
-      |apply H2[auto|apply le_n]
-      ]
-    ]
-  ]
-qed.
-
-theorem eq_map_iter_p_a: \forall p.\forall f.\forall g. \forall a,n:nat. 
-(\forall i.i \le n \to p i = false) \to map_iter_P n p g a f = a.
-intros 5.
-elim n
-  [simplify.reflexivity
-  |rewrite > map_iter_P_S_false
-    [apply H.
-     intros.
-     apply H1.apply le_S.assumption
-    |apply H1.apply le_n
-    ]
-  ]
-qed.
-theorem eq_map_iter_p_transpose: \forall p.\forall f.associative nat f \to
-symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. k < n \to
-(p (S n) = true) \to (p (n-k)) = true \to (\forall i. n-k < i \to i \le n \to (p i) = false)
-\to map_iter_P (S n) p g a f = map_iter_P (S n) p (\lambda m. g (transpose (n-k) (S n) m)) a f.
-intros 8.
-apply (nat_case n)
-  [intro.absurd (k < O)
-    [assumption|apply le_to_not_lt.apply le_O_n]
-  |intros.
-   rewrite > (map_iter_P_S_true ? ? ? ? ? H3).
-   rewrite > (map_iter_P_S_true ? ? ? ? ? H3).
-   rewrite > (eq_map_iter_P_k ? ? ? ? ? ? H4 H5).
-   rewrite > (eq_map_iter_P_k ? ? ? ? ? ? H4 H5).
-   generalize in match H4.
-   rewrite > minus_Sn_m
-    [intro.
-     rewrite > (map_iter_P_S_true ? ? ? ? ? H6).
-     rewrite > (map_iter_P_S_true ? ? ? ? ? H6).
-     rewrite > transpose_i_j_j.
-     rewrite > transpose_i_j_i.
-     cut (map_iter_P (m-k) p g a f =
-      map_iter_P (m-k) p (\lambda x.g (transpose (S(m-k)) (S(S m)) x)) a f)
-      [rewrite < Hcut.
-       rewrite < H.
-       rewrite < H1 in \vdash (? ? (? % ?) ?).
-       rewrite > H.
-       reflexivity
-      |apply eq_map_iter_P.
-       intros.unfold transpose.
-       cut (eqb m1 (S (m-k)) =false)
-        [cut (eqb m1 (S (S m)) =false)
-          [rewrite > Hcut.
-           rewrite > Hcut1.
-           reflexivity
-          |apply not_eq_to_eqb_false.
-           apply lt_to_not_eq.
-           apply (le_to_lt_to_lt ? m)
-            [apply (trans_le ? (m-k))
-              [assumption|auto]
-            |apply le_S.apply le_n
-            ]
-          ]
-        |apply not_eq_to_eqb_false.
-         apply lt_to_not_eq.
-         unfold.auto
-        ]
-      ]
-    |apply le_S_S_to_le.assumption
-    ]
-  ]
-qed.
-
-theorem eq_map_iter_p_transpose1: \forall p.\forall f.associative nat f \to
-symmetric2 nat nat f \to \forall g. \forall a,k1,k2,n:nat. O < k1 \to k1 < k2 \to k2 \le n \to
-(p k1) = true \to (p k2) = true \to (\forall i. k1 < i \to i < k2 \to (p i) = false)
-\to map_iter_P n p g a f = map_iter_P n p (\lambda m. g (transpose k1 k2 m)) a f.
-intros 10.
-elim n 2
-  [absurd (k2 \le O)
-    [assumption|apply lt_to_not_le.apply (trans_lt ? k1 ? H2 H3)]
-  |apply (eqb_elim (S n1) k2)
-   [intro.
-    rewrite < H4.
-    intros.
-    cut (k1 = n1 - (n1 -k1))
-     [rewrite > Hcut.
-      apply (eq_map_iter_p_transpose p f H H1 g a (n1-k1))
-        [cut (k1 \le n1)[auto|auto]
-        |assumption
-        |rewrite < Hcut.assumption
-        |rewrite < Hcut.intros.
-         apply (H9 i H10).unfold.auto   
-       ]
-     |apply sym_eq.
-       apply plus_to_minus.
-       auto.
-     ]
-   |intros.
-     cut ((S n1) \neq k1)
-      [apply (bool_elim ? (p (S n1)))
-       [intro. 
-        rewrite > map_iter_P_S_true
-          [rewrite > map_iter_P_S_true
-            [cut ((transpose k1 k2 (S n1)) = (S n1))
-              [rewrite > Hcut1.
-               apply eq_f.
-               apply (H3 H5)
-                [elim (le_to_or_lt_eq ? ? H6)
-                  [auto
-                  |absurd (S n1=k2)[apply sym_eq.assumption|assumption]
-                  ]
-                |assumption
-                |assumption
-                |assumption
-                ]
-              |unfold transpose.
-               rewrite > (not_eq_to_eqb_false ? ? Hcut).
-               rewrite > (not_eq_to_eqb_false ? ? H4).
-               reflexivity
-              ]
-            |assumption
-            ]
-          |assumption
-          ]
-        |intro.
-          rewrite > map_iter_P_S_false
-          [rewrite > map_iter_P_S_false
-            [apply (H3 H5)
-              [elim (le_to_or_lt_eq ? ? H6)
-                [auto
-                |absurd (S n1=k2)[apply sym_eq.assumption|assumption]
-                ]
-              |assumption
-              |assumption
-              |assumption
-              ]
-            |assumption
-            ]
-          |assumption
-          ]
-        ]
-      |unfold.intro.
-       absurd (k1 < k2)
-        [assumption
-        |apply le_to_not_lt.
-         rewrite < H10.
-         assumption
-        ]
-      ]
-    ]
-  ]
-qed.
-
-lemma decidable_n:\forall p.\forall n.
-(\forall m. m \le n \to (p m) = false) \lor 
-(\exists m. m \le n \land (p m) = true \land 
-\forall i. m < i \to i \le n \to (p i) = false).
-intros.
-elim n
-  [apply (bool_elim ? (p O))
-    [intro.right.
-     apply (ex_intro ? ? O).
-     split
-      [split[apply le_n|assumption]
-      |intros.absurd (O<i)[assumption|apply le_to_not_lt.assumption]
-      ]
-    |intro.left.
-     intros.apply (le_n_O_elim m H1).assumption
-    ]
-  |apply (bool_elim ? (p (S n1)))
-    [intro.right.
-     apply (ex_intro ? ? (S n1)).
-     split
-      [split[apply le_n|assumption]
-      |intros.absurd (S n1<i)[assumption|apply le_to_not_lt.assumption]
-      ]
-    |elim H
-      [left.
-       intros.
-       elim (le_to_or_lt_eq m (S n1) H3)
-        [apply H1.apply le_S_S_to_le.assumption
-        |rewrite > H4.assumption
-        ]
-      |right.
-       elim H1.elim H3.elim H4.
-       apply (ex_intro ? ? a).
-       split
-        [split[apply le_S.assumption|assumption]
-        |intros.elim (le_to_or_lt_eq i (S n1) H9)
-          [apply H5[assumption|apply le_S_S_to_le.assumption]
-          |rewrite > H10.assumption
-          ]
-        ]
-      ]
-    ]
-  ]
-qed.
-
-lemma decidable_n1:\forall p.\forall n,j. j \le n \to (p j)=true \to
-(\forall m. j < m \to m \le n \to (p m) = false) \lor 
-(\exists m. j < m \land m \le n \land (p m) = true \land 
-\forall i. m < i \to i \le n \to (p i) = false).
-intros.
-elim (decidable_n p n)
-  [absurd ((p j)=true)
-    [assumption
-    |unfold.intro.
-     apply not_eq_true_false.
-     rewrite < H3.
-     apply H2.assumption
-    ]
-  |elim H2.clear H2.
-   apply (nat_compare_elim j a)
-    [intro.
-     right.
-     apply (ex_intro ? ? a).
-     elim H3.clear H3.
-     elim H4.clear H4.
-     split
-      [split
-        [split
-          [assumption|assumption]
-        |assumption
-        ]
-      |assumption
-      ]
-    |intro.
-     rewrite > H2.
-     left.
-     elim H3 2.assumption
-    |intro.
-     absurd (p j = true)
-      [assumption
-      |unfold.intro.
-       apply not_eq_true_false.
-       rewrite < H4.
-       elim H3.clear H3.
-       apply (H6 j H2).assumption
-      ]
-    ]
-  ]
-qed.    
-
-lemma decidable_n2:\forall p.\forall n,j. j \le n \to (p j)=true \to
-(\forall m. j < m \to m \le n \to (p m) = false) \lor 
-(\exists m. j < m \land m \le n \land (p m) = true \land 
-\forall i. j < i \to i < m \to (p i) = false).
-intros 3.
-elim n
-  [left.
-   apply (le_n_O_elim j H).intros.
-   absurd (m \le O)
-    [assumption|apply lt_to_not_le.assumption]
-  |elim (le_to_or_lt_eq ? ? H1)
-    [cut (j \le n1)
-      [elim (H Hcut H2)
-        [apply (bool_elim ? (p (S n1)))
-          [intro.
-           right.
-           apply (ex_intro ? ? (S n1)).
-           split
-            [split
-              [split
-                [assumption|apply le_n]
-              |assumption
-              ]
-            |intros.
-             apply (H4 i H6).
-             apply le_S_S_to_le.
-             assumption
-            ]
-          |intro.
-           left.
-           intros.
-           elim (le_to_or_lt_eq ? ? H7)
-            [apply H4
-              [assumption|apply le_S_S_to_le.assumption]
-            |rewrite > H8.assumption
-            ]
-          ]
-        |right.
-         elim H4.clear H4.
-         elim H5.clear H5.
-         elim H4.clear H4.
-         elim H5.clear H5.
-         apply (ex_intro ? ? a).
-         split
-          [split
-            [split[assumption|apply le_S.assumption]
-            |assumption
-            ]
-          |assumption
-          ]
-        ]
-      |apply le_S_S_to_le.
-       assumption
-      ]
-    |left.
-     intros.
-     absurd (j < m)
-      [assumption
-      |apply le_to_not_lt.
-       rewrite > H3.
-       assumption
-      ]
-    ]
-  ]
-qed.
-
-(* tutti d spostare *)
-theorem lt_minus_to_lt_plus:
-\forall n,m,p. n - m < p \to n < m + p.
-intros 2.
-apply (nat_elim2 ? ? ? ? n m)
-  [simplify.intros.auto.
-  |intros 2.rewrite < minus_n_O.
-   intro.assumption
-  |intros.
-   simplify.
-   cut (n1 < m1+p)
-    [auto
-    |apply H.
-     apply H1
-    ]
-  ]
-qed.
-
-theorem lt_plus_to_lt_minus:
-\forall n,m,p. m \le n \to n < m + p \to n - m < p.
-intros 2.
-apply (nat_elim2 ? ? ? ? n m)
-  [simplify.intros 3.
-   apply (le_n_O_elim ? H).
-   simplify.intros.assumption
-  |simplify.intros.assumption.
-  |intros.
-   simplify.
-   apply H
-    [apply le_S_S_to_le.assumption
-    |apply le_S_S_to_le.apply H2
-    ]
-  ]
-qed. 
-
-theorem minus_m_minus_mn: \forall n,m. n\le m \to n=m-(m-n).
-intros.
-apply sym_eq.
-apply plus_to_minus.
-auto.
-qed.
-
-theorem eq_map_iter_p_transpose2: \forall p.\forall f.associative nat f \to
-symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. O < k \to k \le n \to
-(p (S n) = true) \to (p k) = true 
-\to map_iter_P (S n) p g a f = map_iter_P (S n) p (\lambda m. g (transpose k (S n) m)) a f.
-intros 10.
-cut (k = (S n)-(S n -k))
-  [generalize in match H3.clear H3.
-   generalize in match g.
-   generalize in match H2.clear H2.
-   rewrite > Hcut.
-   (*generalize in match Hcut.clear Hcut.*)
-   (* generalize in match H3.clear H3.*)
-   (* something wrong here 
-     rewrite > Hcut in \vdash (?\rarr ?\rarr %). *)
-   apply (nat_elim1 (S n - k)).
-     intros.
-     elim (decidable_n2 p n (S n -m) H4 H6)
-      [apply (eq_map_iter_p_transpose1 p f H H1 f1 a)
-        [assumption.
-        |unfold.auto.
-        |apply le_n
-        |assumption
-        |assumption
-        |intros.apply H7
-          [assumption|apply le_S_S_to_le.assumption]
-        ]
-      |elim H7.clear H7.
-       elim H8.clear H8.
-       elim H7.clear H7.
-       elim H8.clear H8.
-       apply (trans_eq  ? ? 
-        (map_iter_P (S n) p (\lambda i.f1 (transpose a1 (S n) (transpose (S n -m) a1 i))) a f))
-        [apply (trans_eq  ? ? 
-         (map_iter_P (S n) p (\lambda i.f1 (transpose a1 (S n) i)) a f))
-          [cut (a1 = (S n -(S n -a1)))
-            [rewrite > Hcut1.
-             apply H2
-              [apply lt_plus_to_lt_minus
-                [apply le_S.assumption
-                |rewrite < sym_plus.
-                 apply lt_minus_to_lt_plus.
-                 assumption
-                ]
-              |rewrite < Hcut1.
-               apply (trans_lt ? (S n -m))[assumption|assumption]
-              |rewrite < Hcut1.assumption
-              |assumption
-              |rewrite < Hcut1.assumption
-              ]
-           |apply minus_m_minus_mn.
-            apply le_S.assumption
-           ]
-         |apply (eq_map_iter_p_transpose1 p f H H1)
-          [assumption
-          |assumption
-          |apply le_S.assumption
-          |assumption
-          |assumption
-          |assumption
-          ]
-        ]
-      |apply (trans_eq  ? ? 
-        (map_iter_P (S n) p (\lambda i.f1 (transpose a1 (S n) (transpose (S n -m) a1 (transpose (S n -(S n -a1)) (S n) i)))) a f)) 
-        [cut (a1 = (S n) -(S n -a1))
-          [apply H2 
-            [apply lt_plus_to_lt_minus
-              [apply le_S.assumption
-              |rewrite < sym_plus.
-               apply lt_minus_to_lt_plus.
-               assumption
-              ]
-            |rewrite < Hcut1.
-             apply (trans_lt ? (S n -m))[assumption|assumption]
-            |rewrite < Hcut1.assumption
-            |assumption
-            |rewrite < Hcut1.assumption
-            ]
-          |apply minus_m_minus_mn.
-           apply le_S.assumption
-          ]
-        |apply eq_map_iter_P.
-         cut (a1 = (S n) -(S n -a1))
-          [intros.
-           apply eq_f.
-           rewrite < Hcut1.
-           rewrite < transpose_i_j_j_i.
-           rewrite > (transpose_i_j_j_i (S n -m)).
-           rewrite > (transpose_i_j_j_i a1 (S n)).
-           rewrite > (transpose_i_j_j_i (S n -m)).
-           apply sym_eq.
-           apply eq_transpose
-            [unfold.intro.
-             apply (not_le_Sn_n n).
-             rewrite < H12.assumption
-            |unfold.intro.
-             apply (not_le_Sn_n n).
-             rewrite > H12.assumption
-            |unfold.intro.
-             apply (not_le_Sn_n a1).
-             rewrite < H12 in \vdash (? (? %) ?).assumption
-            ]
-          |apply minus_m_minus_mn.
-           apply le_S.assumption
-          ]
-        ]
-      ]
-    ]
-  |apply minus_m_minus_mn.
-   apply le_S.assumption
-  ]
-qed.
-
-theorem eq_map_iter_p_transpose3: \forall p.\forall f.associative nat f \to
-symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. O < k \to k \le (S n) \to
-(p (S n) = true) \to (p k) = true 
-\to map_iter_P (S n) p g a f = map_iter_P (S n) p (\lambda m. g (transpose k (S n) m)) a f.
-intros.
-elim (le_to_or_lt_eq ? ? H3)
-  [apply (eq_map_iter_p_transpose2 p f H H1 g a k n H2)
-    [apply le_S_S_to_le.assumption|assumption|assumption]
-  |rewrite > H6.
-   apply eq_map_iter_P.
-   intros.
-   apply eq_f.apply sym_eq. apply transpose_i_i. 
-  ]
-qed.
-
-lemma permut_p_O: \forall p.\forall h.\forall n.
-permut_p h p n \to p O = false \to \forall m. (S m) \le n \to p (S m) = true \to O < h(S m).
-intros.unfold permut_p in H.
-apply not_le_to_lt.unfold.intro.
-elim (H (S m) H2 H3).
-elim H5.
-absurd (p (h (S m)) = true)
-  [assumption
-  |apply (le_n_O_elim ? H4).
-   unfold.intro.
-   apply not_eq_true_false.
-   rewrite < H9.rewrite < H1.reflexivity
-  ]
-qed.
-
-theorem eq_map_iter_p_permut: \forall p.\forall f.associative nat f \to
-symmetric2 nat nat f \to \forall n.\forall g. \forall h.\forall a:nat.
-permut_p h p n \to p O = false \to
-map_iter_P n p g a f = map_iter_P n p (compose ? ? ? g h) a f .
-intros 5.
-elim n
-  [simplify.reflexivity 
-  |apply (bool_elim ? (p (S n1)))
-    [intro.
-     apply (trans_eq ? ? (map_iter_P (S n1) p (\lambda m.g ((transpose (h (S n1)) (S n1)) m)) a f))
-      [unfold permut_p in H3.
-       elim (H3 (S n1) (le_n ?) H5).
-       elim H6. clear H6.
-       apply (eq_map_iter_p_transpose3 p f H H1 g a (h(S n1)) n1)
-        [apply (permut_p_O ? ? ? H3 H4)
-          [apply le_n|assumption]
-        |assumption
-        |assumption
-        |assumption
-        ]
-      |apply (trans_eq ? ? (map_iter_P (S n1) p (\lambda m.
-        (g(transpose (h (S n1)) (S n1) 
-         (transpose (h (S n1)) (S n1) (h m)))) ) a f))
-        [rewrite > (map_iter_P_S_true ? ? ? ? ? H5).
-         rewrite > (map_iter_P_S_true ? ? ? ? ? H5).
-         apply eq_f2
-          [rewrite > transpose_i_j_j.
-           rewrite > transpose_i_j_i.
-           rewrite > transpose_i_j_j.
-           reflexivity
-          |apply (H2 (\lambda m.(g(transpose (h (S n1)) (S n1) m))) ?)
-            [unfold.intros.
-             split
-              [split
-                [simplify.
-                 unfold permut_p in H3.
-                 elim (H3 i (le_S ? ? H6) H7).
-                 elim H8. clear H8.
-                 elim (le_to_or_lt_eq ? ? H10)
-                  [unfold transpose.
-                   rewrite > (not_eq_to_eqb_false ? ? (lt_to_not_eq ? ? H8)). 
-                   cut (h i \neq h (S n1))
-                    [rewrite > (not_eq_to_eqb_false ? ? Hcut). 
-                     simplify.
-                     apply le_S_S_to_le.
-                     assumption
-                    |apply H9
-                      [apply H5
-                      |apply le_n
-                      |apply lt_to_not_eq.
-                       unfold.apply le_S_S.assumption
-                      ]
-                    ]
-                  |rewrite > H8.
-                   apply (eqb_elim (S n1) (h (S n1)))
-                    [intro.
-                     absurd (h i = h (S n1))
-                      [rewrite > H8.
-                       assumption
-                      |apply H9
-                        [assumption
-                        |apply le_n
-                        |apply lt_to_not_eq.
-                         unfold.apply le_S_S.assumption
-                        ]
-                      ]
-                    |intro.
-                     unfold transpose.
-                     rewrite > (not_eq_to_eqb_false ? ? H12).
-                     rewrite > (eq_to_eqb_true ? ? (refl_eq ? (S n1))).
-                     simplify.
-                     elim (H3 (S n1) (le_n ? ) H5).
-                     elim H13.clear H13.
-                     elim (le_to_or_lt_eq ? ? H15)
-                      [apply le_S_S_to_le.assumption
-                      |apply False_ind.
-                       apply H12.
-                       apply sym_eq.assumption
-                      ]
-                    ]
-                  ]
-                |simplify.
-                 unfold permut_p in H3.
-                 unfold transpose.
-                 apply (eqb_elim (h i) (S n1))
-                  [intro.
-                   apply (eqb_elim (h i) (h (S n1)))
-                    [intro.simplify.assumption
-                    |intro.simplify.
-                     elim (H3 (S n1) (le_n ? ) H5).
-                     elim H10. assumption
-                    ]
-                  |intro.
-                   apply (eqb_elim (h i) (h (S n1)))
-                    [intro.simplify.assumption
-                    |intro.simplify.
-                     elim (H3 i (le_S ? ? H6) H7).
-                     elim H10. assumption
-                    ]
-                  ]
-                ]
-              |simplify.intros.unfold Not.intro.
-               unfold permut_p in H3.
-               elim (H3 i (le_S i ? H6) H7).
-               apply (H13 j H8 (le_S j ? H9) H10).
-               apply (injective_transpose ? ? ? ? H11)
-              ]
-            |assumption
-            ]
-          ]
-        |apply eq_map_iter_P.
-         intros.
-         rewrite > transpose_transpose.reflexivity
-        ]
-      ]
-  |intro.
-   rewrite > (map_iter_P_S_false ? ? ? ? ? H5).
-   rewrite > (map_iter_P_S_false ? ? ? ? ? H5).
-   apply H2
-    [unfold permut_p.
-     unfold permut_p in H3.
-     intros.
-     elim (H3 i (le_S i ? H6) H7).
-     elim H8.
-      split
-        [split
-          [elim (le_to_or_lt_eq ? ? H10)
-            [apply le_S_S_to_le.assumption
-            |absurd (p (h i) = true)
-              [assumption
-              |rewrite > H12.
-               rewrite > H5.
-               unfold.intro.apply not_eq_true_false.
-               apply sym_eq.assumption
-              ]
-            ]
-          |assumption
-          ]
-        |intros.
-         apply H9
-          [assumption|apply (le_S ? ? H13)|assumption]
-        ]
-      |assumption
-      ]
-    ]
-  ]           
-qed.
diff --git a/matita/library/nat/map_iter_p.ma b/matita/library/nat/map_iter_p.ma
new file mode 100644 (file)
index 0000000..c263076
--- /dev/null
@@ -0,0 +1,912 @@
+(**************************************************************************)
+(*       ___                                                             *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/nat/map_iter_p.ma".
+
+include "nat/permutation.ma".
+include "nat/count.ma".
+
+let rec map_iter_p n p (g:nat \to nat) (a:nat) f \def
+  match n with
+   [ O \Rightarrow a
+   | (S k) \Rightarrow 
+      match p (S k) with
+      [true \Rightarrow f (g (S k)) (map_iter_p k p g a f)
+      |false \Rightarrow map_iter_p k p g a f]
+   ].
+
+theorem eq_map_iter_p: \forall g1,g2:nat \to nat.
+\forall p:nat \to bool.
+\forall f:nat \to nat \to nat. \forall a,n:nat.
+(\forall m:nat. m \le n \to g1 m = g2 m) \to 
+map_iter_p n p g1 a f = map_iter_p n p g2 a f.
+intros 6.elim n
+  [simplify.reflexivity.
+  |simplify.elim (p (S n1))
+    [simplify.apply eq_f2
+      [apply H1.apply le_n
+      |simplify.apply H.intros.apply H1.
+       apply le_S.assumption
+      ]
+    |simplify.apply H.intros.apply H1.
+     apply le_S.assumption
+    ]
+ ]
+qed.
+
+(* useful since simplify simpifies too much *)
+
+theorem map_iter_p_O: \forall p.\forall g.\forall f. \forall a:nat.
+map_iter_p O p g a f = a.
+intros.simplify.reflexivity.
+qed.
+
+theorem map_iter_p_S_true: \forall p.\forall g.\forall f. \forall a,n:nat.
+p (S n) = true \to 
+map_iter_p (S n) p g a f = f (g (S n)) (map_iter_p n p g a f).
+intros.simplify.rewrite > H.reflexivity.
+qed.
+
+theorem map_iter_p_S_false: \forall p.\forall g.\forall f. \forall a,n:nat.
+p (S n) = false \to 
+map_iter_p (S n) p g a f = map_iter_p n p g a f.
+intros.simplify.rewrite > H.reflexivity.
+qed.
+
+(* map_iter examples *)
+definition pi_p \def \lambda p. \lambda n.
+map_iter_p n p (\lambda n.n) (S O) times.
+
+lemma pi_p_S: \forall n.\forall p.
+pi_p p (S n) = 
+  match p (S n) with
+    [true \Rightarrow (S n)*(pi_p p n)
+    |false \Rightarrow (pi_p p n)
+    ].
+intros.reflexivity.
+qed.
+
+lemma lt_O_pi_p: \forall n.\forall p.
+O < pi_p p n.
+intros.elim n
+  [simplify.apply le_n
+  |rewrite > pi_p_S.
+   elim p (S n1)
+    [change with (O < (S n1)*(pi_p p n1)).
+     rewrite >(times_n_O n1).
+     apply lt_times[apply le_n|assumption]
+    | assumption
+    ]
+  ]
+qed.
+
+let rec card n p \def 
+  match n with
+  [O \Rightarrow O
+  |(S m) \Rightarrow 
+      (bool_to_nat (p (S m))) + (card m p)].
+
+lemma count_card: \forall p.\forall n.
+p O = false \to count (S n) p = card n p.
+intros.elim n
+  [simplify.rewrite > H. reflexivity
+  |simplify.
+   rewrite < plus_n_O.
+   apply eq_f.assumption
+  ]
+qed.
+
+lemma count_card1: \forall p.\forall n.
+p O = false \to p n = false \to count n p = card n p.
+intros 3.apply (nat_case n)
+  [intro.simplify.rewrite > H. reflexivity
+  |intros.rewrite > (count_card ? ? H).
+   simplify.rewrite > H1.reflexivity
+  ]
+qed.
+lemma a_times_pi_p: \forall p. \forall a,n.
+exp a (card n p) * pi_p p n = map_iter_p n p (\lambda n.a*n) (S O) times.
+intros.elim n
+  [simplify.reflexivity
+  |simplify.apply (bool_elim ? (p (S n1)))
+    [intro.
+     change with 
+      (a*exp a (card n1 p) * ((S n1) * (pi_p p n1)) = 
+       a*(S n1)*map_iter_p n1 p (\lambda n.a*n) (S O) times).
+       rewrite < H.
+       auto
+    |intro.assumption
+    ]
+  ]
+qed.
+
+definition permut_p \def \lambda f. \lambda p:nat\to bool. \lambda n.
+\forall i. i \le n \to p i = true \to ((f i \le n \land p (f i) = true)
+\land (\forall j. p j = true \to j \le n \to i \neq j \to (f i \neq f j))).
+
+definition extentional_eq_n \def \lambda f,g:nat \to nat.\lambda n.
+\forall x. x \le n \to f x = g x.
+
+lemma extentional_eq_n_to_permut_p: \forall f,g. \forall p. \forall n. 
+extentional_eq_n f g n\to permut_p f p n \to permut_p g p n.
+intros.unfold permut_p.
+intros.
+elim (H1 i H2 H3).
+split
+  [elim H4.split
+    [rewrite < (H  i H2).assumption
+    |rewrite < (H  i H2).assumption
+    ]
+  |intros.
+   unfold.intro.apply (H5 j H6 H7 H8).
+     rewrite > (H  i H2).
+     rewrite > (H  j H7).assumption
+  ]
+qed.
+
+theorem permut_p_compose: \forall f,g.\forall p.\forall n.
+permut_p f p n \to permut_p g p n \to permut_p (compose  ? ? ? g f) p n.
+intros.unfold permut_p.intros.
+elim (H i H2 H3).
+elim H4.
+elim (H1 (f i) H6 H7).
+elim H8.
+split
+  [split
+    [unfold compose.assumption
+    |unfold compose.rewrite < H11.reflexivity
+    ]
+  |intros.
+   unfold compose.
+   apply (H9 (f j))
+    [elim (H j H13 H12).elim H15.rewrite < H18.reflexivity
+    |elim (H j H13 H12).elim H15.assumption.
+    |apply (H5 j H12 H13 H14)
+    ]
+  ]
+qed.
+
+theorem permut_p_S_to_permut_p: \forall f.\forall p.\forall n.
+permut_p f p (S n) \to (f (S n)) = (S n) \to permut_p f p n.
+intros.
+unfold permut_p.
+intros.
+split
+  [elim (H i (le_S i n H2) H3).split
+    [elim H4.
+     elim (le_to_or_lt_eq (f i) (S n))
+      [apply le_S_S_to_le.assumption
+      |absurd (f i = (S n))
+        [assumption
+        |rewrite < H1.
+         apply H5
+          [rewrite < H8.assumption
+          |apply le_n
+          |unfold.intro.rewrite > H8 in H2.
+           apply (not_le_Sn_n n).rewrite < H9.assumption
+          ]   
+        ]
+      |assumption
+      ]
+    |elim H4.assumption
+    ]
+  |intros.
+   elim (H i (le_S i n H2) H3).
+   apply H8
+    [assumption|apply le_S.assumption|assumption]
+  ]
+qed.
+
+lemma permut_p_transpose: \forall p.\forall i,j,n.
+i \le n \to j \le n \to p i = p j \to
+permut_p (transpose i j) p n.
+unfold permut_p.intros.
+split
+  [split
+    [unfold transpose.
+     apply (eqb_elim i1 i)
+      [intro.
+       apply (eqb_elim i1 j)
+        [simplify.intro.assumption
+        |simplify.intro.assumption
+        ]
+      |intro.
+       apply (eqb_elim i1 j)
+        [simplify.intro.assumption
+        |simplify.intro.assumption
+        ]
+      ]
+    |unfold transpose.
+     apply (eqb_elim i1 i)
+      [intro.
+       apply (eqb_elim i1 j)
+        [simplify.intro.rewrite < H6.assumption
+        |simplify.intro.rewrite < H2.rewrite < H5.assumption
+        ]
+      |intro.
+       apply (eqb_elim i1 j)
+        [simplify.intro.rewrite > H2.rewrite < H6.assumption
+        |simplify.intro.assumption
+        ]
+      ]
+    ]
+  |intros.unfold Not.
+   intro.apply H7.
+   apply (injective_transpose ? ? ? ? H8).
+  ]
+qed.
+
+theorem eq_map_iter_p_k: \forall f,g.\forall p.\forall a,k,n:nat.
+p (S n-k) = true \to (\forall i. (S n)-k < i \to i \le (S n) \to (p i) = false) \to
+map_iter_p (S n) p g a f = map_iter_p (S n-k) p g a f.
+intros 5.
+elim k 3
+  [rewrite < minus_n_O.reflexivity
+  |apply (nat_case n1)
+    [intros.
+     rewrite > map_iter_p_S_false
+      [reflexivity
+      |apply H2[simplify.apply lt_O_S.|apply le_n]
+      ]
+    |intros.
+     rewrite > map_iter_p_S_false
+      [rewrite > (H m H1)
+        [reflexivity
+        |intros.
+         apply (H2 i H3).
+         apply le_S.
+         assumption
+        ]
+      |apply H2[auto|apply le_n]
+      ]
+    ]
+  ]
+qed.
+
+theorem eq_map_iter_p_a: \forall p.\forall f.\forall g. \forall a,n:nat. 
+(\forall i.i \le n \to p i = false) \to map_iter_p n p g a f = a.
+intros 5.
+elim n
+  [simplify.reflexivity
+  |rewrite > map_iter_p_S_false
+    [apply H.
+     intros.
+     apply H1.apply le_S.assumption
+    |apply H1.apply le_n
+    ]
+  ]
+qed.
+theorem eq_map_iter_p_transpose: \forall p.\forall f.associative nat f \to
+symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. k < n \to
+(p (S n) = true) \to (p (n-k)) = true \to (\forall i. n-k < i \to i \le n \to (p i) = false)
+\to map_iter_p (S n) p g a f = map_iter_p (S n) p (\lambda m. g (transpose (n-k) (S n) m)) a f.
+intros 8.
+apply (nat_case n)
+  [intro.absurd (k < O)
+    [assumption|apply le_to_not_lt.apply le_O_n]
+  |intros.
+   rewrite > (map_iter_p_S_true ? ? ? ? ? H3).
+   rewrite > (map_iter_p_S_true ? ? ? ? ? H3).
+   rewrite > (eq_map_iter_p_k ? ? ? ? ? ? H4 H5).
+   rewrite > (eq_map_iter_p_k ? ? ? ? ? ? H4 H5).
+   generalize in match H4.
+   rewrite > minus_Sn_m
+    [intro.
+     rewrite > (map_iter_p_S_true ? ? ? ? ? H6).
+     rewrite > (map_iter_p_S_true ? ? ? ? ? H6).
+     rewrite > transpose_i_j_j.
+     rewrite > transpose_i_j_i.
+     cut (map_iter_p (m-k) p g a f =
+      map_iter_p (m-k) p (\lambda x.g (transpose (S(m-k)) (S(S m)) x)) a f)
+      [rewrite < Hcut.
+       rewrite < H.
+       rewrite < H1 in \vdash (? ? (? % ?) ?).
+       rewrite > H.
+       reflexivity
+      |apply eq_map_iter_p.
+       intros.unfold transpose.
+       cut (eqb m1 (S (m-k)) =false)
+        [cut (eqb m1 (S (S m)) =false)
+          [rewrite > Hcut.
+           rewrite > Hcut1.
+           reflexivity
+          |apply not_eq_to_eqb_false.
+           apply lt_to_not_eq.
+           apply (le_to_lt_to_lt ? m)
+            [apply (trans_le ? (m-k))
+              [assumption|auto]
+            |apply le_S.apply le_n
+            ]
+          ]
+        |apply not_eq_to_eqb_false.
+         apply lt_to_not_eq.
+         unfold.auto
+        ]
+      ]
+    |apply le_S_S_to_le.assumption
+    ]
+  ]
+qed.
+
+theorem eq_map_iter_p_transpose1: \forall p.\forall f.associative nat f \to
+symmetric2 nat nat f \to \forall g. \forall a,k1,k2,n:nat. O < k1 \to k1 < k2 \to k2 \le n \to
+(p k1) = true \to (p k2) = true \to (\forall i. k1 < i \to i < k2 \to (p i) = false)
+\to map_iter_p n p g a f = map_iter_p n p (\lambda m. g (transpose k1 k2 m)) a f.
+intros 10.
+elim n 2
+  [absurd (k2 \le O)
+    [assumption|apply lt_to_not_le.apply (trans_lt ? k1 ? H2 H3)]
+  |apply (eqb_elim (S n1) k2)
+   [intro.
+    rewrite < H4.
+    intros.
+    cut (k1 = n1 - (n1 -k1))
+     [rewrite > Hcut.
+      apply (eq_map_iter_p_transpose p f H H1 g a (n1-k1))
+        [cut (k1 \le n1)[auto|auto]
+        |assumption
+        |rewrite < Hcut.assumption
+        |rewrite < Hcut.intros.
+         apply (H9 i H10).unfold.auto   
+       ]
+     |apply sym_eq.
+       apply plus_to_minus.
+       auto.
+     ]
+   |intros.
+     cut ((S n1) \neq k1)
+      [apply (bool_elim ? (p (S n1)))
+       [intro. 
+        rewrite > map_iter_p_S_true
+          [rewrite > map_iter_p_S_true
+            [cut ((transpose k1 k2 (S n1)) = (S n1))
+              [rewrite > Hcut1.
+               apply eq_f.
+               apply (H3 H5)
+                [elim (le_to_or_lt_eq ? ? H6)
+                  [auto
+                  |absurd (S n1=k2)[apply sym_eq.assumption|assumption]
+                  ]
+                |assumption
+                |assumption
+                |assumption
+                ]
+              |unfold transpose.
+               rewrite > (not_eq_to_eqb_false ? ? Hcut).
+               rewrite > (not_eq_to_eqb_false ? ? H4).
+               reflexivity
+              ]
+            |assumption
+            ]
+          |assumption
+          ]
+        |intro.
+          rewrite > map_iter_p_S_false
+          [rewrite > map_iter_p_S_false
+            [apply (H3 H5)
+              [elim (le_to_or_lt_eq ? ? H6)
+                [auto
+                |absurd (S n1=k2)[apply sym_eq.assumption|assumption]
+                ]
+              |assumption
+              |assumption
+              |assumption
+              ]
+            |assumption
+            ]
+          |assumption
+          ]
+        ]
+      |unfold.intro.
+       absurd (k1 < k2)
+        [assumption
+        |apply le_to_not_lt.
+         rewrite < H10.
+         assumption
+        ]
+      ]
+    ]
+  ]
+qed.
+
+lemma decidable_n:\forall p.\forall n.
+(\forall m. m \le n \to (p m) = false) \lor 
+(\exists m. m \le n \land (p m) = true \land 
+\forall i. m < i \to i \le n \to (p i) = false).
+intros.
+elim n
+  [apply (bool_elim ? (p O))
+    [intro.right.
+     apply (ex_intro ? ? O).
+     split
+      [split[apply le_n|assumption]
+      |intros.absurd (O<i)[assumption|apply le_to_not_lt.assumption]
+      ]
+    |intro.left.
+     intros.apply (le_n_O_elim m H1).assumption
+    ]
+  |apply (bool_elim ? (p (S n1)))
+    [intro.right.
+     apply (ex_intro ? ? (S n1)).
+     split
+      [split[apply le_n|assumption]
+      |intros.absurd (S n1<i)[assumption|apply le_to_not_lt.assumption]
+      ]
+    |elim H
+      [left.
+       intros.
+       elim (le_to_or_lt_eq m (S n1) H3)
+        [apply H1.apply le_S_S_to_le.assumption
+        |rewrite > H4.assumption
+        ]
+      |right.
+       elim H1.elim H3.elim H4.
+       apply (ex_intro ? ? a).
+       split
+        [split[apply le_S.assumption|assumption]
+        |intros.elim (le_to_or_lt_eq i (S n1) H9)
+          [apply H5[assumption|apply le_S_S_to_le.assumption]
+          |rewrite > H10.assumption
+          ]
+        ]
+      ]
+    ]
+  ]
+qed.
+
+lemma decidable_n1:\forall p.\forall n,j. j \le n \to (p j)=true \to
+(\forall m. j < m \to m \le n \to (p m) = false) \lor 
+(\exists m. j < m \land m \le n \land (p m) = true \land 
+\forall i. m < i \to i \le n \to (p i) = false).
+intros.
+elim (decidable_n p n)
+  [absurd ((p j)=true)
+    [assumption
+    |unfold.intro.
+     apply not_eq_true_false.
+     rewrite < H3.
+     apply H2.assumption
+    ]
+  |elim H2.clear H2.
+   apply (nat_compare_elim j a)
+    [intro.
+     right.
+     apply (ex_intro ? ? a).
+     elim H3.clear H3.
+     elim H4.clear H4.
+     split
+      [split
+        [split
+          [assumption|assumption]
+        |assumption
+        ]
+      |assumption
+      ]
+    |intro.
+     rewrite > H2.
+     left.
+     elim H3 2.assumption
+    |intro.
+     absurd (p j = true)
+      [assumption
+      |unfold.intro.
+       apply not_eq_true_false.
+       rewrite < H4.
+       elim H3.clear H3.
+       apply (H6 j H2).assumption
+      ]
+    ]
+  ]
+qed.    
+
+lemma decidable_n2:\forall p.\forall n,j. j \le n \to (p j)=true \to
+(\forall m. j < m \to m \le n \to (p m) = false) \lor 
+(\exists m. j < m \land m \le n \land (p m) = true \land 
+\forall i. j < i \to i < m \to (p i) = false).
+intros 3.
+elim n
+  [left.
+   apply (le_n_O_elim j H).intros.
+   absurd (m \le O)
+    [assumption|apply lt_to_not_le.assumption]
+  |elim (le_to_or_lt_eq ? ? H1)
+    [cut (j \le n1)
+      [elim (H Hcut H2)
+        [apply (bool_elim ? (p (S n1)))
+          [intro.
+           right.
+           apply (ex_intro ? ? (S n1)).
+           split
+            [split
+              [split
+                [assumption|apply le_n]
+              |assumption
+              ]
+            |intros.
+             apply (H4 i H6).
+             apply le_S_S_to_le.
+             assumption
+            ]
+          |intro.
+           left.
+           intros.
+           elim (le_to_or_lt_eq ? ? H7)
+            [apply H4
+              [assumption|apply le_S_S_to_le.assumption]
+            |rewrite > H8.assumption
+            ]
+          ]
+        |right.
+         elim H4.clear H4.
+         elim H5.clear H5.
+         elim H4.clear H4.
+         elim H5.clear H5.
+         apply (ex_intro ? ? a).
+         split
+          [split
+            [split[assumption|apply le_S.assumption]
+            |assumption
+            ]
+          |assumption
+          ]
+        ]
+      |apply le_S_S_to_le.
+       assumption
+      ]
+    |left.
+     intros.
+     absurd (j < m)
+      [assumption
+      |apply le_to_not_lt.
+       rewrite > H3.
+       assumption
+      ]
+    ]
+  ]
+qed.
+
+(* tutti d spostare *)
+theorem lt_minus_to_lt_plus:
+\forall n,m,p. n - m < p \to n < m + p.
+intros 2.
+apply (nat_elim2 ? ? ? ? n m)
+  [simplify.intros.auto.
+  |intros 2.rewrite < minus_n_O.
+   intro.assumption
+  |intros.
+   simplify.
+   cut (n1 < m1+p)
+    [auto
+    |apply H.
+     apply H1
+    ]
+  ]
+qed.
+
+theorem lt_plus_to_lt_minus:
+\forall n,m,p. m \le n \to n < m + p \to n - m < p.
+intros 2.
+apply (nat_elim2 ? ? ? ? n m)
+  [simplify.intros 3.
+   apply (le_n_O_elim ? H).
+   simplify.intros.assumption
+  |simplify.intros.assumption.
+  |intros.
+   simplify.
+   apply H
+    [apply le_S_S_to_le.assumption
+    |apply le_S_S_to_le.apply H2
+    ]
+  ]
+qed. 
+
+theorem minus_m_minus_mn: \forall n,m. n\le m \to n=m-(m-n).
+intros.
+apply sym_eq.
+apply plus_to_minus.
+auto.
+qed.
+
+theorem eq_map_iter_p_transpose2: \forall p.\forall f.associative nat f \to
+symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. O < k \to k \le n \to
+(p (S n) = true) \to (p k) = true 
+\to map_iter_p (S n) p g a f = map_iter_p (S n) p (\lambda m. g (transpose k (S n) m)) a f.
+intros 10.
+cut (k = (S n)-(S n -k))
+  [generalize in match H3.clear H3.
+   generalize in match g.
+   generalize in match H2.clear H2.
+   rewrite > Hcut.
+   (*generalize in match Hcut.clear Hcut.*)
+   (* generalize in match H3.clear H3.*)
+   (* something wrong here 
+     rewrite > Hcut in \vdash (?\rarr ?\rarr %). *)
+   apply (nat_elim1 (S n - k)).
+     intros.
+     elim (decidable_n2 p n (S n -m) H4 H6)
+      [apply (eq_map_iter_p_transpose1 p f H H1 f1 a)
+        [assumption.
+        |unfold.auto.
+        |apply le_n
+        |assumption
+        |assumption
+        |intros.apply H7
+          [assumption|apply le_S_S_to_le.assumption]
+        ]
+      |elim H7.clear H7.
+       elim H8.clear H8.
+       elim H7.clear H7.
+       elim H8.clear H8.
+       apply (trans_eq  ? ? 
+        (map_iter_p (S n) p (\lambda i.f1 (transpose a1 (S n) (transpose (S n -m) a1 i))) a f))
+        [apply (trans_eq  ? ? 
+         (map_iter_p (S n) p (\lambda i.f1 (transpose a1 (S n) i)) a f))
+          [cut (a1 = (S n -(S n -a1)))
+            [rewrite > Hcut1.
+             apply H2
+              [apply lt_plus_to_lt_minus
+                [apply le_S.assumption
+                |rewrite < sym_plus.
+                 apply lt_minus_to_lt_plus.
+                 assumption
+                ]
+              |rewrite < Hcut1.
+               apply (trans_lt ? (S n -m))[assumption|assumption]
+              |rewrite < Hcut1.assumption
+              |assumption
+              |rewrite < Hcut1.assumption
+              ]
+           |apply minus_m_minus_mn.
+            apply le_S.assumption
+           ]
+         |apply (eq_map_iter_p_transpose1 p f H H1)
+          [assumption
+          |assumption
+          |apply le_S.assumption
+          |assumption
+          |assumption
+          |assumption
+          ]
+        ]
+      |apply (trans_eq  ? ? 
+        (map_iter_p (S n) p (\lambda i.f1 (transpose a1 (S n) (transpose (S n -m) a1 (transpose (S n -(S n -a1)) (S n) i)))) a f)) 
+        [cut (a1 = (S n) -(S n -a1))
+          [apply H2 
+            [apply lt_plus_to_lt_minus
+              [apply le_S.assumption
+              |rewrite < sym_plus.
+               apply lt_minus_to_lt_plus.
+               assumption
+              ]
+            |rewrite < Hcut1.
+             apply (trans_lt ? (S n -m))[assumption|assumption]
+            |rewrite < Hcut1.assumption
+            |assumption
+            |rewrite < Hcut1.assumption
+            ]
+          |apply minus_m_minus_mn.
+           apply le_S.assumption
+          ]
+        |apply eq_map_iter_p.
+         cut (a1 = (S n) -(S n -a1))
+          [intros.
+           apply eq_f.
+           rewrite < Hcut1.
+           rewrite < transpose_i_j_j_i.
+           rewrite > (transpose_i_j_j_i (S n -m)).
+           rewrite > (transpose_i_j_j_i a1 (S n)).
+           rewrite > (transpose_i_j_j_i (S n -m)).
+           apply sym_eq.
+           apply eq_transpose
+            [unfold.intro.
+             apply (not_le_Sn_n n).
+             rewrite < H12.assumption
+            |unfold.intro.
+             apply (not_le_Sn_n n).
+             rewrite > H12.assumption
+            |unfold.intro.
+             apply (not_le_Sn_n a1).
+             rewrite < H12 in \vdash (? (? %) ?).assumption
+            ]
+          |apply minus_m_minus_mn.
+           apply le_S.assumption
+          ]
+        ]
+      ]
+    ]
+  |apply minus_m_minus_mn.
+   apply le_S.assumption
+  ]
+qed.
+
+theorem eq_map_iter_p_transpose3: \forall p.\forall f.associative nat f \to
+symmetric2 nat nat f \to \forall g. \forall a,k,n:nat. O < k \to k \le (S n) \to
+(p (S n) = true) \to (p k) = true 
+\to map_iter_p (S n) p g a f = map_iter_p (S n) p (\lambda m. g (transpose k (S n) m)) a f.
+intros.
+elim (le_to_or_lt_eq ? ? H3)
+  [apply (eq_map_iter_p_transpose2 p f H H1 g a k n H2)
+    [apply le_S_S_to_le.assumption|assumption|assumption]
+  |rewrite > H6.
+   apply eq_map_iter_p.
+   intros.
+   apply eq_f.apply sym_eq. apply transpose_i_i. 
+  ]
+qed.
+
+lemma permut_p_O: \forall p.\forall h.\forall n.
+permut_p h p n \to p O = false \to \forall m. (S m) \le n \to p (S m) = true \to O < h(S m).
+intros.unfold permut_p in H.
+apply not_le_to_lt.unfold.intro.
+elim (H (S m) H2 H3).
+elim H5.
+absurd (p (h (S m)) = true)
+  [assumption
+  |apply (le_n_O_elim ? H4).
+   unfold.intro.
+   apply not_eq_true_false.
+   rewrite < H9.rewrite < H1.reflexivity
+  ]
+qed.
+
+theorem eq_map_iter_p_permut: \forall p.\forall f.associative nat f \to
+symmetric2 nat nat f \to \forall n.\forall g. \forall h.\forall a:nat.
+permut_p h p n \to p O = false \to
+map_iter_p n p g a f = map_iter_p n p (compose ? ? ? g h) a f .
+intros 5.
+elim n
+  [simplify.reflexivity 
+  |apply (bool_elim ? (p (S n1)))
+    [intro.
+     apply (trans_eq ? ? (map_iter_p (S n1) p (\lambda m.g ((transpose (h (S n1)) (S n1)) m)) a f))
+      [unfold permut_p in H3.
+       elim (H3 (S n1) (le_n ?) H5).
+       elim H6. clear H6.
+       apply (eq_map_iter_p_transpose3 p f H H1 g a (h(S n1)) n1)
+        [apply (permut_p_O ? ? ? H3 H4)
+          [apply le_n|assumption]
+        |assumption
+        |assumption
+        |assumption
+        ]
+      |apply (trans_eq ? ? (map_iter_p (S n1) p (\lambda m.
+        (g(transpose (h (S n1)) (S n1) 
+         (transpose (h (S n1)) (S n1) (h m)))) ) a f))
+        [rewrite > (map_iter_p_S_true ? ? ? ? ? H5).
+         rewrite > (map_iter_p_S_true ? ? ? ? ? H5).
+         apply eq_f2
+          [rewrite > transpose_i_j_j.
+           rewrite > transpose_i_j_i.
+           rewrite > transpose_i_j_j.
+           reflexivity
+          |apply (H2 (\lambda m.(g(transpose (h (S n1)) (S n1) m))) ?)
+            [unfold.intros.
+             split
+              [split
+                [simplify.
+                 unfold permut_p in H3.
+                 elim (H3 i (le_S ? ? H6) H7).
+                 elim H8. clear H8.
+                 elim (le_to_or_lt_eq ? ? H10)
+                  [unfold transpose.
+                   rewrite > (not_eq_to_eqb_false ? ? (lt_to_not_eq ? ? H8)). 
+                   cut (h i \neq h (S n1))
+                    [rewrite > (not_eq_to_eqb_false ? ? Hcut). 
+                     simplify.
+                     apply le_S_S_to_le.
+                     assumption
+                    |apply H9
+                      [apply H5
+                      |apply le_n
+                      |apply lt_to_not_eq.
+                       unfold.apply le_S_S.assumption
+                      ]
+                    ]
+                  |rewrite > H8.
+                   apply (eqb_elim (S n1) (h (S n1)))
+                    [intro.
+                     absurd (h i = h (S n1))
+                      [rewrite > H8.
+                       assumption
+                      |apply H9
+                        [assumption
+                        |apply le_n
+                        |apply lt_to_not_eq.
+                         unfold.apply le_S_S.assumption
+                        ]
+                      ]
+                    |intro.
+                     unfold transpose.
+                     rewrite > (not_eq_to_eqb_false ? ? H12).
+                     rewrite > (eq_to_eqb_true ? ? (refl_eq ? (S n1))).
+                     simplify.
+                     elim (H3 (S n1) (le_n ? ) H5).
+                     elim H13.clear H13.
+                     elim (le_to_or_lt_eq ? ? H15)
+                      [apply le_S_S_to_le.assumption
+                      |apply False_ind.
+                       apply H12.
+                       apply sym_eq.assumption
+                      ]
+                    ]
+                  ]
+                |simplify.
+                 unfold permut_p in H3.
+                 unfold transpose.
+                 apply (eqb_elim (h i) (S n1))
+                  [intro.
+                   apply (eqb_elim (h i) (h (S n1)))
+                    [intro.simplify.assumption
+                    |intro.simplify.
+                     elim (H3 (S n1) (le_n ? ) H5).
+                     elim H10. assumption
+                    ]
+                  |intro.
+                   apply (eqb_elim (h i) (h (S n1)))
+                    [intro.simplify.assumption
+                    |intro.simplify.
+                     elim (H3 i (le_S ? ? H6) H7).
+                     elim H10. assumption
+                    ]
+                  ]
+                ]
+              |simplify.intros.unfold Not.intro.
+               unfold permut_p in H3.
+               elim (H3 i (le_S i ? H6) H7).
+               apply (H13 j H8 (le_S j ? H9) H10).
+               apply (injective_transpose ? ? ? ? H11)
+              ]
+            |assumption
+            ]
+          ]
+        |apply eq_map_iter_p.
+         intros.
+         rewrite > transpose_transpose.reflexivity
+        ]
+      ]
+  |intro.
+   rewrite > (map_iter_p_S_false ? ? ? ? ? H5).
+   rewrite > (map_iter_p_S_false ? ? ? ? ? H5).
+   apply H2
+    [unfold permut_p.
+     unfold permut_p in H3.
+     intros.
+     elim (H3 i (le_S i ? H6) H7).
+     elim H8.
+      split
+        [split
+          [elim (le_to_or_lt_eq ? ? H10)
+            [apply le_S_S_to_le.assumption
+            |absurd (p (h i) = true)
+              [assumption
+              |rewrite > H12.
+               rewrite > H5.
+               unfold.intro.apply not_eq_true_false.
+               apply sym_eq.assumption
+              ]
+            ]
+          |assumption
+          ]
+        |intros.
+         apply H9
+          [assumption|apply (le_S ? ? H13)|assumption]
+        ]
+      |assumption
+      ]
+    ]
+  ]           
+qed.
index 587134afcc9c0873eea6fa14a61677e34fbb6e63..807906bd21abd4572f75e96fa9bd39977a2309e5 100644 (file)
@@ -191,6 +191,18 @@ apply H2.reflexivity.
 apply H3. apply le_S_S. assumption.
 qed.
 
+(* le to eq *)
+lemma le_to_le_to_eq: \forall n,m. n \le m \to m \le n \to n = m.
+apply nat_elim2
+  [intros.apply le_n_O_to_eq.assumption
+  |intros.apply sym_eq.apply le_n_O_to_eq.assumption
+  |intros.apply eq_f.apply H
+    [apply le_S_S_to_le.assumption
+    |apply le_S_S_to_le.assumption
+    ]
+  ]
+qed.
+
 (* lt and le trans *)
 theorem lt_O_S : \forall n:nat. O < S n.
 intro. unfold. apply le_S_S. apply le_O_n.
@@ -207,6 +219,12 @@ assumption.apply H2.unfold lt.
 apply lt_to_le.assumption.
 qed.
 
+theorem lt_S_to_lt: \forall n,m. S n < m \to n < m.
+intros.
+apply (trans_lt ? (S n))
+  [apply le_n|assumption]
+qed.
+
 theorem ltn_to_ltO: \forall n,m:nat. lt n m \to lt O m.
 intros.apply (le_to_lt_to_lt O n).
 apply le_O_n.assumption.