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.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "arithmetics/nat.ma".
14 definition injn: (nat → nat) → nat → Prop ≝ λf,n.∀i,j:nat.
15 i ≤ n → j ≤ n → f i = f j → i = j.
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 //|//]
21 theorem injective_to_injn: ∀f,n. injective nat nat f → injn f n.
22 #f #n #Hinj #i #j #_ #_ #eqf @Hinj //
25 definition permut : (nat → nat) → nat → Prop
26 ≝ λf,m.(∀i.i ≤ m → f i ≤ m )∧ injn f m.
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 //
32 theorem permut_S_to_permut: ∀f,m.
33 permut f (S m) → f (S m) = (S m) → permut f m.
35 [#i #leim cases(le_to_or_lt_eq … (H1 … (le_S … leim)))
37 |#H @False_ind @(absurd ? leim) @lt_to_not_le
38 lapply Hf <H in ⊢ (???%→?); -H #H <(H2 … H) // @le_S //
40 |#i #j #lei #lej #eqf @H2 [@le_S //|@le_S // |//]
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.
50 notation < "(❲i↹j❳) term 72 n" with precedence 71
51 for @{ 'transposition $i $j $n}.
53 notation "(❲i \atop j❳) term 72 n" with precedence 71
54 for @{ 'transposition $i $j $n}.
56 notation > "(❲\frac term 90 i term 90 j❳)n" with precedence 71
57 for @{ 'transposition $i $j $n}.
60 interpretation "natural transposition" 'transposition i j n = (transpose i j n).
62 lemma transpose_i_j_i: ∀i,j. transpose i j i = j.
63 #i #j normalize >(eqb_n_n i) //
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) //
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) // |// ]
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) //
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)
92 |cases (true_or_false (eqb n j)) #Hnj >Hnj normalize
93 [>(eqb_n_n i) normalize @sym_eq @(eqb_true_to_eq … Hnj)
99 theorem injective_transpose : ∀i,j:nat.
100 injective nat nat (transpose i j).
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) //
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 | //]
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 //
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 //
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)
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) %
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 //]
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
164 |@False_ind @(absurd (i= S m))
165 [@permf2 [@le_S // | //| //]
166 |@(not_to_not ? (S m ≤ m)) [// |@lt_to_not_le //]
170 |#a #b #leam #lebm #H @permf2
171 [@le_S //|@le_S //| @(injective_transpose … H)]
175 (* bounded bijectivity *)
177 definition bijn : (nat → nat) → nat → Prop ≝
178 λf,n.∀m:nat. m ≤ n → ex nat (λp. p ≤ n ∧ f p = m).
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 //
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 //
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
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} % //
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} % //
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 %
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/
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/
242 theorem permut_to_bijn: ∀n,f. permut f n → bijn f n.
244 [#f normalize * #H #H1 #m #lem0 %{0} % //
245 @(le_n_O_elim … lem0) @sym_eq @le_n_O_to_eq @H //
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 // |//]
253 [@Hind @permut_S_to_permut_transpose //
254 |normalize >(eqb_n_n (f (S m))) %
261 let rec invert_permut n f m ≝
262 match eqb m (f n) with
267 |(S p) ⇒ invert_permut p f m]].
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)))
276 |% #eqf @(absurd (m = S m0))
277 [@H1 [@le_S // |//|//] |@lt_to_not_eq @le_S_S //]
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
288 <fa <fb >(invert_permut_f … lean injf) >(invert_permut_f … lebn injf) //
291 theorem permut_invert_permut: ∀f,n.
292 permut f n → permut (invert_permut n f) n.
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 //]
298 |@injective_invert_permut //
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)
307 |@invert_permut_f [@Hle //| //]
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) //
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
329 [@injh [@(transitive_le … lekn) @lt_to_le // |@lejn|@H //]] #Hj