include "arithmetics/primes.ma".
-(* successor mod n *)
-definition S_mod: nat → nat → nat ≝
-λn,m:nat. (S m) \mod n.
+definition S_mod ≝ λn,m:nat. S m \mod n.
-definition congruent: nat → nat → nat → Prop ≝
-λn,m,p:nat. mod n p = mod m p.
+definition congruent ≝ λn,m,p:nat. mod n p = mod m p.
interpretation "congruent" 'congruent n m p = (congruent n m p).
-notation "hvbox(n break ≅_{p} m)"
- non associative with precedence 45
- for @{ 'congruent $n $m $p }.
-
-theorem congruent_n_n: ∀n,p:nat.n ≅_{p} n .
+theorem congruent_n_n: ∀n,p:nat.congruent n n p.
// qed.
-theorem transitive_congruent:
- ∀p.transitive nat (λn,m.congruent n m p).
-/2/ qed.
+theorem transitive_congruent: ∀p. transitive ? (λn,m. congruent n m p).
+// qed.
theorem le_to_mod: ∀n,m:nat. n < m → n = n \mod m.
#n #m #ltnm @(div_mod_spec_to_eq2 n m O n (n/m) (n \mod m))
qed.
theorem mod_mod : ∀n,p:nat. O<p → n \mod p = (n \mod p) \mod p.
-#n #p #posp >(div_mod (n \mod p) p) in ⊢ (? ? % ?);
+#n #p #posp >(div_mod (n \mod p) p) in ⊢ (??%?);
>(eq_div_O ? p) // @lt_mod_m_m //
qed.
theorem mod_times_mod : ∀n,m,p:nat. O<p → O<m →
n \mod p = (n \mod (m*p)) \mod p.
-#n #m #p #posp #posm
-@(div_mod_spec_to_eq2 n p (n/p) (n \mod p)
-(n/(m*p)*m + (n \mod (m*p)/p)))
+#n #m #p #posp #posm
+@(div_mod_spec_to_eq2 n p (n/p) (n \mod p) (n/(m*p)*m + (n \mod (m*p)/p)))
[@div_mod_spec_div_mod //
- |% [@lt_mod_m_m //] >distributive_times_plus_r
- >
associative_plus <div_mod >associative_times <div_mod //
+ |% [@lt_mod_m_m //]
+ >
distributive_times_plus_r >associative_plus <div_mod //
]
qed.
-theorem congruent_n_mod_n : ∀n,p:nat. O < p →
- n ≅_{p} (n \mod p).
-/2/ qed.
+theorem congruent_n_mod_n: ∀n,p. 0 < p →
+ congruent n (n \mod p) p.
+#n #p #posp @mod_mod //
+qed.
-theorem congruent_n_mod_times : ∀n,m,p:nat. O < p → O < m →
- n ≅_{p} (n \mod (m*p)).
-/2/ qed.
+theorem congruent_n_mod_times: ∀n,m,p. 0 < p → 0 < m →
+ congruent n (n \mod (m*p)) p.
+#n #p #posp @mod_times_mod
+qed.
-theorem eq_times_plus_to_congruent: ∀n,m,p,r:nat. O< p →
- n = r*p+m → n ≅_{p} m .
-#n #m #p #r #posp #eqn
+theorem eq_times_plus_to_congruent: ∀n,m,p,r:nat. 0 < p →
+ n = r*p+m → congruent n m p.
+#n #m #p #r #posp #Hn
@(div_mod_spec_to_eq2 n p (div n p) (mod n p) (r +(div m p)) (mod m p))
[@div_mod_spec_div_mod //
- |% [@lt_mod_m_m //] >distributive_times_plus_r
- >associative_plus <div_mod //
+ |% [@lt_mod_m_m //]
+ >commutative_times >distributive_times_plus >commutative_times
+ >(commutative_times p) >associative_plus //
]
qed.
-theorem divides_to_congruent: ∀n,m,p:nat. O < p → m ≤ n →
- p ∣(n - m) → n ≅_{p} m .
-#n #m #p #posp #lemn * #l #eqpl
-@(eq_times_plus_to_congruent … l posp) /2/
+theorem divides_to_congruent: ∀n,m,p:nat. 0 < p → m ≤ n →
+ divides p (n - m) → congruent n m p.
+#n #m #p #posp #lemn * #q #Hdiv @(eq_times_plus_to_congruent n m p q) //
+>commutative_plus @minus_to_plus //
qed.
-theorem congruent_to_divides: ∀n,m,p:nat.O < p →
- n ≅_{p} m → p ∣ (n - m).
-#n #m #p #posp #congnm @(quotient ? ? ((n / p)-(m / p)))
+theorem congruent_to_divides: ∀n,m,p:nat.
+ 0 < p → congruent n m p → divides p (n - m).
+#n #m #p #posp #Hcong %{((n / p)-(m / p))}
>commutative_times >(div_mod n p) in ⊢ (??%?);
->(div_mod m p) in ⊢ (??%?); <(commutative_plus (m \mod p))
-<congnm <(minus_plus ? (n \mod p)) <minus_plus_m_m //
+>(div_mod m p) in ⊢ (??%?); //
qed.
-theorem mod_times: ∀n,m,p:nat. O < p →
- n*m ≅_{p} (n \mod p)*(m \mod p).
-#n #m #p #posp @(eq_times_plus_to_congruent ?? p
+theorem mod_times: ∀n,m,p. 0 < p →
+ mod (n*m) p = mod ((mod n p)*(mod m p)) p.
+#n #m #p #posp
+@(eq_times_plus_to_congruent ? ? p
((n / p)*p*(m / p) + (n / p)*(m \mod p) + (n \mod p)*(m / p))) //
-@(trans_eq ?? (((n/p)*p+(n \mod p))*((m/p)*p+(m \mod p))))
- [@eq_f2 //
- |@(trans_eq ? ? (((n/p)*p)*((m/p)*p) + (n/p)*p*(m \mod p) +
- (n \mod p)*((m / p)*p) + (n \mod p)*(m \mod p))) //
- >distributive_times_plus >distributive_times_plus_r
- >distributive_times_plus_r <associative_plus @eq_f2 //
+@(trans_eq ? ? (((n/p)*p+(n \mod p))*((m/p)*p+(m \mod p)))) //
+@(trans_eq ? ? (((n/p)*p)*((m/p)*p) + (n/p)*p*(m \mod p) +
+ (n \mod p)*((m / p)*p) + (n \mod p)*(m \mod p)))
+ [cut (∀a,b,c,d.(a+b)*(c+d) = a*c +a*d + b*c + b*d)
+ [#a #b #c #d >(distributive_times_plus_r (c+d) a b)
+ >(distributive_times_plus a c d)
+ >(distributive_times_plus b c d) //] #Hcut
+ @Hcut
+ |@eq_f2
+ [<associative_times >(associative_times (n/p) p (m \mod p))
+ >(commutative_times p (m \mod p)) <(associative_times (n/p) (m \mod p) p)
+ >distributive_times_plus_r //
+ |%
+ ]
]
qed.
-theorem congruent_times: ∀n,m,n1,m1,p. O < p →
- n ≅_{p} n1 → m ≅_{p} m1 → n*m ≅_{p} n1*m1 .
-#n #m #n1 #m1 #p #posp #congn #congm
-@(transitive_congruent … (mod_times n m p posp))
->congn >congm @sym_eq @mod_times //
+theorem congruent_times: ∀n,m,n1,m1,p. O < p → congruent n n1 p →
+ congruent m m1 p → congruent (n*m) (n1*m1) p.
+#n #m #n1 #m1 #p #posp #Hcongn #Hcongm whd
+>(mod_times n m p posp) >Hcongn >Hcongm @sym_eq @mod_times //
qed.
-(*
-theorem congruent_pi: \forall f:nat \to nat. \forall n,m,p:nat.O < p \to
-congruent (pi n f m) (pi n (\lambda m. mod (f m) p) m) p.
-intros.
-elim n. simplify.
-apply congruent_n_mod_n.assumption.
-simplify.
-apply congruent_times.
-assumption.
-apply congruent_n_mod_n.assumption.
-assumption.
-qed. *)
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department of the University of Bologna, Italy.
+ ||I||
+ ||T||
+ ||A|| This file is distributed under the terms of the
+ \ / GNU General Public License Version 2
+ \ /
+ V_______________________________________________________________ *)
+
+include "arithmetics/exp.ma".
+include "arithmetics/gcd.ma".
+include "arithmetics/permutation.ma".
+include "arithmetics/congruence.ma".
+include "arithmetics/sigma_pi.ma".
+
+theorem permut_S_mod: ∀n:nat. permut (S_mod (S n)) n.
+#n %
+ [#i #lein @le_S_S_to_le @lt_mod_m_m //
+ |#i #j #lein #lejn #Heq @injective_S
+ <(lt_to_eq_mod i (S n)) [2: @le_S_S @lein]
+ <(lt_to_eq_mod j (S n)) [2: @le_S_S @lejn]
+ cases (le_to_or_lt_eq … lein) #Hi
+ cases (le_to_or_lt_eq … lejn) #Hj
+ [(* i < n, j< n *)
+ <mod_S
+ [<mod_S
+ [@Heq |@le_S_S >lt_to_eq_mod // @le_S // |//]
+ |@le_S_S >lt_to_eq_mod // @le_S //
+ |//
+ ]
+ |(* i < n, j=n *)
+ @False_ind @(absurd ?? (not_eq_O_S (i \mod (S n))))
+ @sym_eq <(mod_n_n (S n)) [2://]
+ <Hj in ⊢ (???(?%?)); <mod_S
+ [@Heq |>lt_to_eq_mod [@le_S_S @Hi |@le_S_S @lt_to_le @Hi]|//]
+ |(* i = n, j < n *)
+ @False_ind @(absurd ?? (not_eq_O_S (j \mod (S n))))
+ <(mod_n_n (S n)) [2://]
+ <Hi in ⊢ (??(?%?)?); <mod_S
+ [@Heq |>lt_to_eq_mod [@le_S_S @Hj |@le_S_S @lt_to_le @Hj]|//]
+ |(* i = n, j= n*)
+ >Hi >Hj %
+ ]
+ ]
+qed.
+
+theorem prime_to_not_divides_fact: ∀p.prime p → ∀n.n < p → p ∤ n!.
+#p #primep #n elim n
+ [normalize #_ % #divp @(absurd (p ≤1))
+ [@divides_to_le // |@lt_to_not_le @prime_to_lt_SO //]
+ |#n1 #Hind #ltn1 whd in match (fact ?); % #Hdiv
+ cases (divides_times_to_divides … Hdiv)
+ [-Hdiv #Hdiv @(absurd … Hdiv) @Hind @lt_to_le //
+ |-Hdiv #Hdiv @(absurd … (p ≤ S n1))
+ [@divides_to_le // |@lt_to_not_le //]
+ |@primep
+ ]
+ ]
+qed.
+
+theorem permut_mod: ∀p,a:nat. prime p →
+ p ∤ a → permut (λn.(mod (a*n) p)) (pred p).
+#p #a #primep #ndiv %
+ [#i #lei @le_S_S_to_le @(transitive_le ? p)
+ [@lt_mod_m_m @prime_to_lt_O //
+ |>S_pred [//| @prime_to_lt_O //]
+ ]
+ |#i #j #lei #lej #H cases (decidable_lt i j)
+ [(* i < j *) #ltij
+ @False_ind @(absurd (j-i < p))
+ [<(S_pred p) [2:@prime_to_lt_O //]
+ @le_S_S @le_plus_to_minus @(transitive_le … lej) //
+ |@le_to_not_lt @divides_to_le [@lt_plus_to_minus_r //]
+ cut (p ∣ a ∨ p ∣ (j-i))
+ [2:* [#Hdiv @False_ind /2/ | //]]
+ @divides_times_to_divides // >distributive_times_minus
+ @eq_mod_to_divides // @prime_to_lt_O //
+ ]
+ |#Hij cases (le_to_or_lt_eq … (not_lt_to_le … Hij)) -Hij #Hij
+ [(* j < i *)
+ @False_ind @(absurd (i-j < p))
+ [<(S_pred p) [2:@prime_to_lt_O //]
+ @le_S_S @le_plus_to_minus @(transitive_le … lei) //
+ |@le_to_not_lt @divides_to_le [@lt_plus_to_minus_r //]
+ cut (p ∣ a ∨ p ∣ (i-j))
+ [2:* [#Hdiv @False_ind /2/ | //]]
+ @divides_times_to_divides // >distributive_times_minus
+ @eq_mod_to_divides // @prime_to_lt_O //
+ ]
+ |(* i = j *) //
+ ]
+ ]
+ ]
+qed.
+
+theorem eq_fact_pi_p:∀n.
+ fact n = ∏_{i ∈ [1,S n[ } i.
+#n elim n // #n1 #Hind whd in ⊢ (??%?); >commutative_times >bigop_Strue
+ [cut (S n1 -1 = n1) [normalize //] #Hcut
+ <plus_n_Sm <plus_n_O @eq_f <Hcut in ⊢ (???%); // | % ]
+qed.
+
+theorem congruent_pi: ∀f,n,p.O < p →
+ congruent (∏_{i < n}(f i)) (∏_{i < n} (mod (f i) p)) p.
+#f #n elim n // #n1 #Hind #p #posp >bigop_Strue //
+@congruent_times // [@congruent_n_mod_n // |@Hind //]
+qed.
+
+theorem congruent_exp_pred_SO: ∀p,a:nat. prime p → ¬ divides p a →
+congruent (exp a (pred p)) (S O) p.
+#p #a #primep #ndiv
+cut (0 < a)
+ [lapply ndiv cases a // * #div0 @False_ind @div0 @(quotient ? 0 0) //] #posa
+cut (O < p) [@prime_to_lt_O //] #posp
+cut (O < pred p) [@le_S_S_to_le >S_pred [@prime_to_lt_SO //| @posp] ] #pospred
+@(divides_to_congruent … posp)
+ [@lt_O_exp //
+ |cut (divides p (exp a (pred p)-1) ∨ divides p (pred p)!)
+ [@divides_times_to_divides // >commutative_times
+ >distributive_times_minus <times_n_1
+ >eq_fact_pi_p >commutative_times
+ cut (pred p = S (pred p) -1) [//] #Hpred >Hpred in match (exp a ?);
+ >exp_pi_bc @congruent_to_divides //
+ @(transitive_congruent p ? (∏_{i ∈ [1,S(pred p)[ }(a*i \mod p)))
+ [@(congruent_pi (λm.a*(m +1))) //
+ |cut (∏_{i ∈ [1,S(pred p)[ } i = ∏_{i ∈ [1,S(pred p)[ } (a*i\mod p))
+ [2: #Heq <Heq @congruent_n_n]
+ >(bigop_I_gen 1 (S (pred p)) … 1 timesA) //
+ >(bigop_I_gen 1 (S (pred p)) … 1 timesA) //
+ @sym_eq @(bigop_iso … timesAC)
+ lapply (permut_mod … primep ndiv) #Hpermut
+ %{(λi.a*i \mod p)} %{(invert_permut (pred p) (λi.a*i \mod p))} %
+ [%
+ [#i #lti #_ %
+ |#i #lti #posi %
+ [%
+ [>(S_pred … posp) @lt_mod_m_m //
+ |>le_to_leb_true //
+ cases (le_to_or_lt_eq … (le_O_n (a*i \mod p))) [//]
+ #H @False_ind @(absurd ? (mod_O_to_divides …(sym_eq … H))) //
+ @(not_to_not … ndiv) #Hdiv cases(divides_times_to_divides … Hdiv)
+ // #divpi @False_ind @(absurd ? lti) @le_to_not_lt
+ >(S_pred … posp) @divides_to_le // @leb_true_to_le
+ @(andb_true_l … posi)
+ ]
+ |@invert_permut_f [@le_S_S_to_le //|cases Hpermut // ]
+ ]
+ ]
+ |lapply (permut_invert_permut … Hpermut) *
+ #le_invert_permut #inj_inv_permut
+ #i #lti #posi %
+ [%
+ [@le_S_S @le_invert_permut @le_S_S_to_le //
+ |>le_to_leb_true //
+ cases (le_to_or_lt_eq …
+ (le_O_n (invert_permut (pred p) (λi.a*i \mod p) i))) [//]
+ #H @False_ind
+ cut (a*0 \mod p = 0) [<times_n_O //] #H0
+ cut (a*0 \mod p = a*(invert_permut (pred p) (λi.a*i \mod p) i) \mod p)
+ [@(eq_f ?? (λi.a*i \mod p)) //]
+ >H0 >(f_invert_permut (λi.a*i \mod p) … Hpermut) [2:@le_S_S_to_le //]
+ #eq0i <eq0i in posi; normalize #H destruct (H)
+ ]
+ |@f_invert_permut [@le_S_S_to_le //| @Hpermut ]
+ ]
+ ]
+ ]
+ |* // #Hdiv @False_ind
+ @(absurd ? Hdiv (prime_to_not_divides_fact p primep (pred p) ?))
+ @le_S_S_to_le >S_pred //
+ ]
+ ]
+qed.
+
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department of the University of Bologna, Italy.
+ ||I||
+ ||T||
+ ||A|| This file is distributed under the terms of the
+ \ / GNU General Public License Version 2
+ \ /
+ V_______________________________________________________________ *)
+
+include "arithmetics/nat.ma".
+
+definition injn: (nat → nat) → nat → Prop ≝ λf,n.∀i,j:nat.
+ i ≤ n → j ≤ n → f i = f j → i = j.
+
+theorem injn_Sn_n: ∀f,n. injn f (S n) → injn f n.
+#f #n #H #i #j #lei #lej #eqf @H [@le_S // |@le_S //|//]
+qed.
+
+theorem injective_to_injn: ∀f,n. injective nat nat f → injn f n.
+#f #n #Hinj #i #j #_ #_ #eqf @Hinj //
+qed.
+
+definition permut : (nat → nat) → nat → Prop
+≝ λf,m.(∀i.i ≤ m → f i ≤ m )∧ injn f m.
+
+theorem permut_O_to_eq_O: ∀h.permut h O → h O = O.
+#h * #H1 #_ @sym_eq @le_n_O_to_eq @H1 //
+qed.
+
+theorem permut_S_to_permut: ∀f,m.
+ permut f (S m) → f (S m) = (S m) → permut f m.
+#f #m * #H1 #H2 #Hf %
+ [#i #leim cases(le_to_or_lt_eq … (H1 … (le_S … leim)))
+ [#H @le_S_S_to_le @H
+ |#H @False_ind @(absurd ? leim) @lt_to_not_le
+ lapply Hf <H in ⊢ (???%→?); -H #H <(H2 … H) // @le_S //
+ ]
+ |#i #j #lei #lej #eqf @H2 [@le_S //|@le_S // |//]
+ ]
+qed.
+
+(* transpositions *)
+
+definition transpose : nat → nat → nat → nat ≝ λi,j,n:nat.
+ if eqb n i then j else if eqb n j then i else n.
+
+(*
+notation < "(❲i↹j❳) term 72 n" with precedence 71
+for @{ 'transposition $i $j $n}.
+
+notation "(❲i \atop j❳) term 72 n" with precedence 71
+for @{ 'transposition $i $j $n}.
+
+notation > "(❲\frac term 90 i term 90 j❳)n" with precedence 71
+for @{ 'transposition $i $j $n}.
+*)
+
+interpretation "natural transposition" 'transposition i j n = (transpose i j n).
+
+lemma transpose_i_j_i: ∀i,j. transpose i j i = j.
+#i #j normalize >(eqb_n_n i) //
+qed.
+
+lemma transpose_i_j_j: ∀i,j. transpose i j j = i.
+#i #j normalize cases(true_or_false (eqb j i)) #Hc
+ [>Hc normalize >(eqb_true_to_eq … Hc) //
+ |>Hc >(eqb_n_n j) //
+ ]
+qed.
+
+theorem transpose_i_i: ∀i,n:nat. (transpose i i n) = n.
+#i #n normalize cases (true_or_false (eqb n i)) #Hc >Hc
+ [normalize >(eqb_true_to_eq … Hc) // |// ]
+qed.
+
+theorem transpose_i_j_j_i: ∀i,j,n:nat.
+transpose i j n = transpose j i n.
+#i #j #n normalize cases (true_or_false (eqb n i)) #Hni >Hni
+cases (true_or_false (eqb n j)) #Hnj >Hnj normalize //
+<(eqb_true_to_eq … Hni) <(eqb_true_to_eq … Hnj) //
+qed.
+
+theorem transpose_transpose: ∀i,j,n:nat.
+ (transpose i j (transpose i j n)) = n.
+#i #j #n normalize cases (true_or_false (eqb n i)) #Hni >Hni normalize
+ [cases (true_or_false (eqb j i)) #Hji >Hji normalize
+ [>(eqb_true_to_eq … Hni) @(eqb_true_to_eq … Hji)
+ |>(eqb_n_n j) normalize @sym_eq @(eqb_true_to_eq … Hni)
+ ]
+ |cases (true_or_false (eqb n j)) #Hnj >Hnj normalize
+ [>(eqb_n_n i) normalize @sym_eq @(eqb_true_to_eq … Hnj)
+ |>Hni >Hnj //
+ ]
+ ]
+qed.
+
+theorem injective_transpose : ∀i,j:nat.
+ injective nat nat (transpose i j).
+// qed.
+
+theorem permut_transpose: ∀i,j,n. i ≤ n → j ≤ n → permut (transpose i j) n.
+#i #j #n #lein #lejn %
+ [#a #lean normalize cases (eqb a i) cases (eqb a j) normalize //
+ |#a #b #lean #lebn @(injective_to_injn (transpose i j) n) //
+ ]
+qed.
+
+theorem permut_fg: ∀f,g,n.
+ permut f n → permut g n → permut (λm.(f(g m))) n.
+#f #g #n * #permf1 #permf2 * #permg1 #permg2 %
+ [#i #lein @permf1 @permg1 @lein
+ |#a #b #lean #lebn #Heq @permg2 // @permf2
+ [@permg1 @lean |@permg1 @lebn | //]
+ ]
+qed.
+
+theorem permut_transpose_l: ∀f,m,i,j.i ≤ m → j ≤ m →
+ permut f m → permut (λn.transpose i j (f n)) m.
+#f #m #i #j #leim #lejm #permf @(permut_fg … permf) @permut_transpose //
+qed.
+
+theorem permut_transpose_r: ∀f,m,i,j. i ≤ m → j ≤ m →
+ permut f m → permut (λn.f (transpose i j n)) m.
+#f #m #i #j #leim #lejm #permf @(permut_fg … permf) @permut_transpose //
+qed.
+
+theorem eq_transpose : ∀i,j,k,n:nat. j≠i → i≠k → j≠k →
+ transpose i j n = transpose i k (transpose k j (transpose i k n)).
+#i #j #k #n #Hji #Hik #Hjk normalize
+cases (true_or_false (eqb n i)) #Hni >Hni normalize
+ [>(eqb_n_n k) normalize >(not_eq_to_eqb_false … Hji)
+ >(not_eq_to_eqb_false … Hjk) %
+ |cases (true_or_false (eqb n k)) #Hnk >Hnk normalize
+ [>(not_eq_to_eqb_false n j)
+ [2: @(not_to_not …Hjk) <(eqb_true_to_eq … Hnk) //]
+ >(not_eq_to_eqb_false … Hik) >(not_eq_to_eqb_false … i j)
+ [2: @(not_to_not … Hji) //]
+ normalize >(eqb_n_n i) @(eqb_true_to_eq … Hnk)
+ |>Hnk normalize
+ cases (true_or_false (eqb n j)) #Hnj >Hnj normalize
+ [>(not_eq_to_eqb_false k i)[2: @(not_to_not … Hik) //]
+ normalize >(eqb_n_n k) %
+ |>Hni >Hnk %
+ ]
+ ]
+ ]
+qed.
+
+theorem permut_S_to_permut_transpose: ∀f,m.
+ permut f (S m) → permut (λn.transpose (f (S m)) (S m) (f n)) m.
+#f #m * #permf1 #permf2 %
+ [#i #leim normalize >(not_eq_to_eqb_false (f i) (f (S m))) normalize
+ [2: % #H @(absurd … (i= S m))
+ [@(permf2 … H) [@le_S //|//] |@lt_to_not_eq @le_S_S //]
+ ]
+ cases(le_to_or_lt_eq … (permf1 … (le_S … leim))) #Hfi
+ [>(not_eq_to_eqb_false (f i) (S m)) [2:@lt_to_not_eq //]
+ normalize @le_S_S_to_le @Hfi
+ |>(eq_to_eqb_true …Hfi) normalize
+ cases(le_to_or_lt_eq … (permf1 … (le_n (S m)))) #H
+ [@le_S_S_to_le @H
+ |@False_ind @(absurd (i= S m))
+ [@permf2 [@le_S // | //| //]
+ |@(not_to_not ? (S m ≤ m)) [// |@lt_to_not_le //]
+ ]
+ ]
+ ]
+ |#a #b #leam #lebm #H @permf2
+ [@le_S //|@le_S //| @(injective_transpose … H)]
+ ]
+qed.
+
+(* bounded bijectivity *)
+
+definition bijn : (nat → nat) → nat → Prop ≝
+λf,n.∀m:nat. m ≤ n → ex nat (λp. p ≤ n ∧ f p = m).
+
+theorem eq_to_bijn: ∀f,g,n.
+ (∀i.i ≤ n → f i = g i) → bijn f n → bijn g n.
+#f #g #n #H #bijf #i #lein cases (bijf … lein) #a * #lean #fa
+%{a} % // <fa @sym_eq @H //
+qed.
+
+theorem bijn_Sn_n: ∀f,n.
+ bijn f (S n) → f (S n) = S n → bijn f n.
+#f #n #bijf #fS #i #lein cases (bijf … (le_S … lein)) #a * #lean #fa
+cases (le_to_or_lt_eq … lean) #Hc
+ [%{a} % [@le_S_S_to_le @Hc |@fa]
+ |@False_ind @(absurd ?? (not_le_Sn_n n)) <fS //
+ ]
+qed.
+
+theorem bijn_n_Sn: ∀f,n.
+ bijn f n → f (S n) = S n → bijn f (S n).
+#f #n #bijf #fS #i #lein
+cases (le_to_or_lt_eq … lein) #Hi
+ [cases (bijf … (le_S_S_to_le … Hi)) #a * #lean #fa
+ %{a} % [@le_S //|//]
+ |%{i} % //
+ ]
+qed.
+
+theorem bijn_fg: ∀f,g:nat→ nat.∀n:nat.
+ bijn f n → bijn g n → bijn (λp.f(g p)) n.
+#f #g #n #bijf #bijg #i #lein cases (bijf … lein) #a * #lean #ga
+cases (bijg … lean) #b * #lebn #gb %{b} % //
+qed.
+
+(*
+theorem bijn_to_injn: ∀f,n. bijn f n → injn f n.
+#f #n normalize #H #i #j #lein #lejn #eqf
+cases (H … lein) #a * #lean #fa
+cases (H … lejn) #b * #lebn #fb
+cases (bijg … lean) #b * #lebn #gb %{b} % //
+qed.
+*)
+
+theorem bijn_transpose : ∀n,i,j. i ≤ n → j ≤ n →
+ bijn (transpose i j) n.
+#n #i #j #lein #lejn #a #lean
+cases (true_or_false (eqb a i)) #Hi
+ [%{j} % // >transpose_i_j_j @sym_eq @(eqb_true_to_eq … Hi)
+ |cases (true_or_false (eqb a j)) #Hj
+ [%{i} % // >transpose_i_j_i @sym_eq @(eqb_true_to_eq … Hj)
+ |%{a} % // normalize >Hi >Hj %
+ ]
+ ]
+qed.
+
+theorem bijn_transpose_r: ∀f,n,i,j. i ≤ n → j ≤ n →
+ bijn f n → bijn (λp.f (transpose i j p)) n.
+#f #n #i #j #lein #lejn #bijf @(bijn_fg f ?) /2/
+qed.
+
+theorem bijn_transpose_l: ∀f,n,i,j. i ≤ n → j ≤ n →
+ bijn f n → bijn (λp.transpose i j (f p)) n.
+#f #n #i #j #lein #lejn #bijf @(bijn_fg ? f) /2/
+qed.
+
+theorem permut_to_bijn: ∀n,f. permut f n → bijn f n.
+#n elim n
+ [#f normalize * #H #H1 #m #lem0 %{0} % //
+ @(le_n_O_elim … lem0) @sym_eq @le_n_O_to_eq @H //
+ |#m #Hind #f #permf
+ @(eq_to_bijn (λp.
+ (transpose (f (S m)) (S m)) (transpose (f (S m)) (S m) (f p))) f)
+ [#i #lei @transpose_transpose
+ |@(bijn_fg (transpose (f (S m)) (S m)))
+ [cases permf #lef #_ @bijn_transpose [@lef // |//]
+ |@bijn_n_Sn
+ [@Hind @permut_S_to_permut_transpose //
+ |normalize >(eqb_n_n (f (S m))) %
+ ]
+ ]
+ ]
+ ]
+qed.
+
+let rec invert_permut n f m ≝
+ match eqb m (f n) with
+ [true ⇒ n
+ |false ⇒
+ match n with
+ [O ⇒ O
+ |(S p) ⇒ invert_permut p f m]].
+
+theorem invert_permut_f: ∀f:nat → nat. ∀n,m:nat.
+ m ≤ n → injn f n → invert_permut n f (f m) = m.
+#f #n #m #lenm elim lenm
+ [cases m normalize [>(eqb_n_n (f O)) //| #a >(eqb_n_n (f (S a))) //]
+ |#m0 #lem #H #H1 normalize
+ >(not_eq_to_eqb_false (f m) (f (S m0)))
+ [@H @injn_Sn_n //
+ |% #eqf @(absurd (m = S m0))
+ [@H1 [@le_S // |//|//] |@lt_to_not_eq @le_S_S //]
+ ]
+ ]
+qed.
+
+theorem injective_invert_permut: ∀f,n.
+ permut f n → injn (invert_permut n f) n.
+#f #n #permf #i #j #lein #lejn lapply (permut_to_bijn … permf) #bijf
+cases (bijf i lein) #a * #lean #fa
+cases (bijf j lejn) #b * #lebn #fb
+cases permf #_ #injf
+<fa <fb >(invert_permut_f … lean injf) >(invert_permut_f … lebn injf) //
+qed.
+
+theorem permut_invert_permut: ∀f,n.
+ permut f n → permut (invert_permut n f) n.
+#f #n #permf %
+ [#i #lein elim n normalize
+ [cases (eqb i (f O)) %
+ |#n1 #Hind cases (eqb i (f (S n1))) [@le_n | normalize @le_S //]
+ ]
+ |@injective_invert_permut //
+ ]
+qed.
+
+theorem f_invert_permut: ∀f,n,m.
+ m ≤ n → permut f n → f (invert_permut n f m) = m.
+#f #n #m #lemn #permf lapply (permut_invert_permut … permf)
+* #Hle #Hinj cases permf #lef #injf @(injective_invert_permut … permf … lemn)
+ [@lef @Hle //
+ |@invert_permut_f [@Hle //| //]
+ ]
+qed.
+
+theorem permut_n_to_eq_n: ∀h,n.
+ permut h n → (∀m:nat. m < n → h m = m) → h n = n.
+#h #n #permh cases permh #leh #injh #eqh
+lapply (permut_invert_permut … permh) * #Hle #Hinj
+cases (le_to_or_lt_eq … (Hle … (le_n n))) #Hc
+ [<(f_invert_permut … (le_n n) permh) in ⊢ (???%); @eq_f
+ <(f_invert_permut … (le_n n) permh) in ⊢ (??%?); @eqh @Hc
+ |<Hc in ⊢ (??%?); @(f_invert_permut h) //
+ ]
+qed.
+
+theorem permut_n_to_le: ∀h,k,n.
+k ≤ n → permut h n → (∀m.m < k → h m = m) →
+ ∀j. k ≤ j → j ≤ n → k ≤ h j.
+#h #k #n #lekn * #leh #injh #H #j #lekj #lejn
+cases (decidable_lt (h j) k) #Hh
+ [@False_ind @(absurd … lekj) @lt_to_not_le
+ cut (h j = j)
+ [@injh [@(transitive_le … lekn) @lt_to_le // |@lejn|@H //]] #Hj
+ <Hj //
+ |@not_lt_to_le //
+ ]
+qed.
|>bigop_Sfalse [>bigop_Sfalse [@Hind|//] | //]
]
qed.
+
+theorem exp_pi_l: ∀n,a,f.
+ exp a n*(∏_{i < n}(f i)) = ∏_{i < n} (a*(f i)).
+#n #a #f elim n // #i #Hind >bigop_Strue // >bigop_Strue //
+<Hind <associative_times <associative_times @eq_f2 // normalize //
+qed.
+
+theorem exp_pi_bc: ∀a,b,c,f.
+ exp a (c-b)*(∏_{i ∈ [b,c[ }(f i)) = ∏_{i ∈ [b,c[ } (a*(f i)).
+#a #b #c #f @exp_pi_l
+qed.
\ No newline at end of file
projects / helm.git / commitdiff