matita/matita/lib/arithmetics/permutation.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "arithmetics/nat.ma".
  13
  14 definition injn: (nat → nat) → nat → Prop ≝ λf,n.∀i,j:nat.
  15   i ≤ n → j ≤ n → f i = f j → i = j.
  16
  17 theorem injn_Sn_n: ∀f,n. injn f (S n) → injn f n.
  18 #f #n #H #i #j #lei #lej #eqf @H [@le_S // |@le_S //|//]
  19 qed.
  20
  21 theorem injective_to_injn: ∀f,n. injective nat nat f → injn f n.
  22 #f #n #Hinj #i #j #_ #_ #eqf @Hinj //
  23 qed.
  24
  25 definition permut : (nat → nat) → nat → Prop
  26 ≝ λf,m.(∀i.i ≤ m → f i ≤ m )∧ injn f m.
  27
  28 theorem permut_O_to_eq_O: ∀h.permut h O → h O = O.
  29 #h * #H1 #_ @sym_eq @le_n_O_to_eq @H1 //
  30 qed.
  31
  32 theorem permut_S_to_permut: ∀f,m.
  33   permut f (S m) → f (S m) = (S m) → permut f m.
  34 #f #m * #H1 #H2 #Hf %
  35   [#i #leim cases(le_to_or_lt_eq … (H1 … (le_S … leim)))
  36     [#H @le_S_S_to_le @H
  37     |#H @False_ind @(absurd ? leim) @lt_to_not_le
  38      lapply Hf <H in ⊢ (???%→?); -H #H <(H2 … H) // @le_S //
  39     ]
  40   |#i #j #lei #lej #eqf @H2 [@le_S //|@le_S // |//]
  41   ]
  42 qed.
  43
  44 (* transpositions *)
  45
  46 definition transpose : nat → nat → nat → nat ≝ λi,j,n:nat.
  47   if eqb n i then j else if eqb n j then i else n.
  48
  49 (*
  50 notation < "(❲i↹j❳) term 72 n" with precedence 71
  51 for @{ 'transposition $i $j $n}.
  52
  53 notation "(❲i \atop j❳) term 72 n" with precedence 71
  54 for @{ 'transposition $i $j $n}.
  55
  56 notation > "(❲\frac term 90 i term 90 j❳)n" with precedence 71
  57 for @{ 'transposition $i $j $n}.
  58 *)
  59
  60 interpretation "natural transposition" 'transposition i j n = (transpose i j n).
  61
  62 lemma transpose_i_j_i: ∀i,j. transpose i j i = j.
  63 #i #j normalize >(eqb_n_n i) //
  64 qed.
  65
  66 lemma transpose_i_j_j: ∀i,j. transpose i j j = i.
  67 #i #j normalize cases(true_or_false (eqb j i)) #Hc
  68   [>Hc normalize >(eqb_true_to_eq … Hc) //
  69   |>Hc >(eqb_n_n j) //
  70   ]
  71 qed.
  72
  73 theorem transpose_i_i:  ∀i,n:nat. (transpose  i i n) = n.
  74 #i #n normalize cases (true_or_false (eqb n i)) #Hc >Hc
  75   [normalize >(eqb_true_to_eq … Hc) // |// ]
  76 qed.
  77
  78 theorem transpose_i_j_j_i: ∀i,j,n:nat.
  79 transpose i j n = transpose j i n.
  80 #i #j #n normalize cases (true_or_false (eqb n i)) #Hni >Hni
  81 cases (true_or_false (eqb n j)) #Hnj >Hnj normalize //
  82 <(eqb_true_to_eq … Hni) <(eqb_true_to_eq … Hnj) //
  83 qed.
  84
  85 theorem transpose_transpose: ∀i,j,n:nat.
  86   (transpose i j (transpose i j n)) = n.
  87 #i #j #n normalize cases (true_or_false (eqb n i)) #Hni >Hni normalize
  88   [cases (true_or_false (eqb j i)) #Hji >Hji normalize
  89     [>(eqb_true_to_eq … Hni) @(eqb_true_to_eq … Hji)
  90     |>(eqb_n_n j) normalize @sym_eq @(eqb_true_to_eq … Hni)
  91     ]
  92   |cases (true_or_false (eqb n j)) #Hnj >Hnj normalize
  93     [>(eqb_n_n i) normalize @sym_eq @(eqb_true_to_eq … Hnj)
  94     |>Hni >Hnj //
  95     ]
  96   ]
  97 qed.
  98
  99 theorem injective_transpose : ∀i,j:nat.
 100   injective nat nat (transpose i j).
 101 // qed.
 102
 103 theorem permut_transpose: ∀i,j,n. i ≤ n → j ≤ n → permut (transpose i j) n.
 104 #i #j #n #lein #lejn %
 105   [#a #lean normalize cases (eqb a i) cases (eqb a j) normalize //
 106   |#a #b #lean #lebn @(injective_to_injn (transpose i j) n) //
 107   ]
 108 qed.
 109
 110 theorem permut_fg: ∀f,g,n.
 111   permut f n → permut g n → permut (λm.(f(g m))) n.
 112 #f #g #n * #permf1 #permf2 * #permg1 #permg2 %
 113   [#i #lein @permf1 @permg1 @lein
 114   |#a #b #lean #lebn #Heq @permg2 // @permf2
 115     [@permg1 @lean |@permg1 @lebn | //]
 116   ]
 117 qed.
 118
 119 theorem permut_transpose_l: ∀f,m,i,j.i ≤ m → j ≤ m →
 120   permut f m → permut (λn.transpose i j (f n)) m.
 121 #f #m #i #j #leim #lejm #permf @(permut_fg … permf) @permut_transpose //
 122 qed.
 123
 124 theorem permut_transpose_r: ∀f,m,i,j. i ≤ m → j ≤ m →
 125   permut f m → permut (λn.f (transpose i j n)) m.
 126 #f #m #i #j #leim #lejm #permf @(permut_fg … permf) @permut_transpose //
 127 qed.
 128
 129 theorem eq_transpose : ∀i,j,k,n:nat. j≠i → i≠k → j≠k →
 130   transpose i j n = transpose i k (transpose k j (transpose i k n)).
 131 #i #j #k #n #Hji #Hik #Hjk normalize
 132 cases (true_or_false (eqb n i)) #Hni >Hni normalize
 133   [>(eqb_n_n k) normalize >(not_eq_to_eqb_false … Hji)
 134    >(not_eq_to_eqb_false … Hjk) %
 135   |cases (true_or_false (eqb n k)) #Hnk >Hnk normalize
 136     [>(not_eq_to_eqb_false n j)
 137       [2: @(not_to_not …Hjk) <(eqb_true_to_eq … Hnk) //]
 138      >(not_eq_to_eqb_false … Hik) >(not_eq_to_eqb_false … i j)
 139       [2: @(not_to_not … Hji) //]
 140      normalize >(eqb_n_n i) @(eqb_true_to_eq … Hnk)
 141     |>Hnk normalize
 142      cases (true_or_false (eqb n j)) #Hnj >Hnj normalize
 143       [>(not_eq_to_eqb_false k i)[2: @(not_to_not … Hik) //]
 144        normalize >(eqb_n_n k) %
 145       |>Hni >Hnk %
 146       ]
 147     ]
 148   ]
 149 qed.
 150
 151 theorem permut_S_to_permut_transpose: ∀f,m.
 152   permut f (S m) → permut (λn.transpose (f (S m)) (S m) (f n)) m.
 153 #f #m * #permf1 #permf2 %
 154   [#i #leim normalize >(not_eq_to_eqb_false (f i) (f (S m))) normalize
 155     [2: % #H @(absurd … (i= S m))
 156       [@(permf2 … H) [@le_S //|//]  |@lt_to_not_eq @le_S_S //]
 157     ]
 158    cases(le_to_or_lt_eq … (permf1 … (le_S … leim))) #Hfi
 159     [>(not_eq_to_eqb_false (f i) (S m)) [2:@lt_to_not_eq //]
 160      normalize @le_S_S_to_le @Hfi
 161     |>(eq_to_eqb_true …Hfi) normalize
 162      cases(le_to_or_lt_eq … (permf1 … (le_n (S m)))) #H
 163       [@le_S_S_to_le @H
 164       |@False_ind @(absurd (i= S m))
 165         [@permf2 [@le_S // | //| //]
 166         |@(not_to_not ? (S m ≤ m)) [// |@lt_to_not_le //]
 167         ]
 168       ]
 169     ]
 170   |#a #b #leam #lebm #H @permf2
 171     [@le_S //|@le_S //| @(injective_transpose … H)]
 172   ]
 173 qed.
 174
 175 (* bounded bijectivity *)
 176
 177 definition bijn : (nat → nat) → nat → Prop ≝
 178 λf,n.∀m:nat. m ≤ n → ex nat (λp. p ≤ n ∧ f p = m).
 179
 180 theorem eq_to_bijn:  ∀f,g,n.
 181   (∀i.i ≤ n → f i = g i) →  bijn f n → bijn g n.
 182 #f #g #n #H #bijf #i #lein cases (bijf … lein) #a * #lean #fa
 183 %{a} % // <fa @sym_eq @H //
 184 qed.
 185
 186 theorem bijn_Sn_n: ∀f,n.
 187   bijn f (S n) → f (S n) = S n → bijn f n.
 188 #f #n #bijf #fS #i #lein cases (bijf … (le_S … lein)) #a * #lean #fa
 189 cases (le_to_or_lt_eq … lean) #Hc
 190   [%{a} % [@le_S_S_to_le @Hc |@fa]
 191   |@False_ind @(absurd ?? (not_le_Sn_n n)) <fS //
 192   ]
 193 qed.
 194
 195 theorem bijn_n_Sn: ∀f,n.
 196   bijn f n → f (S n) = S n → bijn f (S n).
 197 #f #n #bijf #fS #i #lein
 198 cases (le_to_or_lt_eq … lein) #Hi
 199   [cases (bijf … (le_S_S_to_le … Hi)) #a * #lean #fa
 200    %{a} % [@le_S //|//]
 201   |%{i} % //
 202   ]
 203 qed.
 204
 205 theorem bijn_fg: ∀f,g:nat→ nat.∀n:nat.
 206   bijn f n → bijn g n → bijn (λp.f(g p)) n.
 207 #f #g #n #bijf #bijg #i #lein cases (bijf … lein) #a * #lean #ga
 208 cases (bijg … lean) #b * #lebn #gb %{b} % //
 209 qed.
 210
 211 (*
 212 theorem bijn_to_injn: ∀f,n. bijn f n → injn f n.
 213 #f #n normalize #H #i #j #lein #lejn #eqf
 214 cases (H … lein) #a * #lean #fa
 215 cases (H … lejn) #b * #lebn #fb
 216 cases (bijg … lean) #b * #lebn #gb %{b} % //
 217 qed.
 218 *)
 219
 220 theorem bijn_transpose : ∀n,i,j. i ≤ n → j ≤ n →
 221   bijn (transpose i j) n.
 222 #n #i #j #lein #lejn #a #lean
 223 cases (true_or_false (eqb a i)) #Hi
 224   [%{j} % // >transpose_i_j_j @sym_eq @(eqb_true_to_eq … Hi)
 225   |cases (true_or_false (eqb a j)) #Hj
 226     [%{i} % // >transpose_i_j_i @sym_eq @(eqb_true_to_eq … Hj)
 227     |%{a} % // normalize >Hi >Hj %
 228     ]
 229   ]
 230 qed.
 231
 232 theorem bijn_transpose_r: ∀f,n,i,j. i ≤ n → j ≤ n →
 233   bijn f n → bijn (λp.f (transpose i j p)) n.
 234 #f #n #i #j #lein #lejn #bijf @(bijn_fg f ?) /2/
 235 qed.
 236
 237 theorem bijn_transpose_l: ∀f,n,i,j. i ≤ n → j ≤ n →
 238   bijn f n → bijn (λp.transpose i j (f p)) n.
 239 #f #n #i #j #lein #lejn #bijf @(bijn_fg ? f) /2/
 240 qed.
 241
 242 theorem permut_to_bijn: ∀n,f. permut f n → bijn f n.
 243 #n elim n
 244   [#f normalize * #H #H1 #m #lem0 %{0} % //
 245    @(le_n_O_elim … lem0) @sym_eq @le_n_O_to_eq @H //
 246   |#m #Hind #f #permf
 247    @(eq_to_bijn (λp.
 248       (transpose (f (S m)) (S m)) (transpose (f (S m)) (S m) (f p))) f)
 249     [#i #lei @transpose_transpose
 250     |@(bijn_fg (transpose (f (S m)) (S m)))
 251       [cases permf #lef #_ @bijn_transpose [@lef // |//]
 252       |@bijn_n_Sn
 253         [@Hind @permut_S_to_permut_transpose //
 254         |normalize >(eqb_n_n (f (S m))) %
 255         ]
 256       ]
 257     ]
 258   ]
 259 qed.
 260
 261 let rec invert_permut n f m ≝
 262   match eqb m (f n) with
 263   [true ⇒ n
 264   |false ⇒
 265      match n with
 266      [O ⇒ O
 267      |(S p) ⇒ invert_permut p f m]].
 268
 269 theorem invert_permut_f: ∀f:nat → nat. ∀n,m:nat.
 270   m ≤ n → injn f n → invert_permut n f (f m) = m.
 271 #f #n #m #lenm elim lenm
 272   [cases m normalize [>(eqb_n_n (f O)) //| #a >(eqb_n_n (f (S a))) //]
 273   |#m0 #lem #H #H1 normalize
 274    >(not_eq_to_eqb_false (f m) (f (S m0)))
 275     [@H @injn_Sn_n //
 276     |% #eqf @(absurd (m = S m0))
 277       [@H1 [@le_S // |//|//] |@lt_to_not_eq @le_S_S //]
 278     ]
 279   ]
 280 qed.
 281
 282 theorem injective_invert_permut: ∀f,n.
 283   permut f n → injn (invert_permut n f) n.
 284 #f #n #permf #i #j #lein #lejn lapply (permut_to_bijn … permf) #bijf
 285 cases (bijf i lein) #a * #lean #fa
 286 cases (bijf j lejn) #b * #lebn #fb
 287 cases permf #_ #injf
 288 <fa <fb >(invert_permut_f … lean injf) >(invert_permut_f … lebn injf) //
 289 qed.
 290
 291 theorem permut_invert_permut: ∀f,n.
 292   permut f n → permut (invert_permut n f) n.
 293 #f #n #permf %
 294   [#i #lein elim n normalize
 295     [cases (eqb i (f O)) %
 296     |#n1 #Hind cases (eqb i (f (S n1))) [@le_n | normalize @le_S //]
 297     ]
 298   |@injective_invert_permut //
 299   ]
 300 qed.
 301
 302 theorem f_invert_permut: ∀f,n,m.
 303   m ≤ n → permut f n → f (invert_permut n f m) = m.
 304 #f #n #m #lemn #permf lapply (permut_invert_permut … permf)
 305 * #Hle #Hinj cases permf #lef #injf @(injective_invert_permut … permf … lemn)
 306   [@lef @Hle //
 307   |@invert_permut_f [@Hle //| //]
 308   ]
 309 qed.
 310
 311 theorem permut_n_to_eq_n: ∀h,n.
 312   permut h n → (∀m:nat. m < n → h m = m) → h n = n.
 313 #h #n #permh cases permh #leh #injh #eqh
 314 lapply (permut_invert_permut … permh) * #Hle #Hinj
 315 cases (le_to_or_lt_eq … (Hle … (le_n n))) #Hc
 316   [<(f_invert_permut … (le_n n) permh) in ⊢ (???%); @eq_f
 317    <(f_invert_permut … (le_n n) permh) in ⊢ (??%?); @eqh @Hc
 318   |<Hc in ⊢ (??%?); @(f_invert_permut h) //
 319   ]
 320 qed.
 321
 322 theorem permut_n_to_le: ∀h,k,n.
 323 k ≤ n → permut h n → (∀m.m < k → h m = m) →
 324   ∀j. k ≤ j → j ≤ n → k ≤ h j.
 325 #h #k #n #lekn * #leh #injh #H #j #lekj #lejn
 326 cases (decidable_lt (h j) k) #Hh
 327   [@False_ind @(absurd … lekj) @lt_to_not_le
 328    cut (h j = j)
 329     [@injh [@(transitive_le … lekn) @lt_to_le // |@lejn|@H //]] #Hj
 330    <Hj //
 331   |@not_lt_to_le //
 332   ]
 333 qed.