]
qed.
-(* Sigma e Pi - da generalizzare *)
+(* Sigma e Pi *)
notation "Σ_{ ident i < n | p } f"
with precedence 80
for @{'bigop $n plus 0 (λ${ident i}.p) (λ${ident i}. $f)}.
--- /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/bigops.ma".
+include "arithmetics/primes.ma".
+
+(* binomial coefficient *)
+definition bc ≝ λn,k. n!/(k!*(n-k)!).
+
+lemma bceq :∀n,k. bc n k = n!/(k!*(n-k)!).
+// qed.
+
+theorem bc_n_n: ∀n. bc n n = 1.
+#n >bceq <minus_n_n <times_n_1 @div_n_n //
+qed.
+
+theorem bc_n_O: ∀n. bc n O = 1.
+#n >bceq <minus_n_O /2/
+qed.
+
+theorem fact_minus: ∀n,k. k < n →
+ (n-k)*(n - S k)! = (n - k)!.
+#n #k (cases n)
+ [#ltO @False_ind /2/
+ |#l #ltl >minus_Sn_m [>commutative_times //|@le_S_S_to_le //]
+ ]
+qed.
+
+theorem bc2 : ∀n.
+∀k. k ≤n → k!*(n-k)! ∣ n!.
+#n (elim n)
+ [#k #lek0 <(le_n_O_to_eq ? lek0) //
+ |#m #Hind #k generalize in match H1;cases k
+ [intro;simplify in ⊢ (? (? ? (? %)) ?);simplify in ⊢ (? (? % ?) ?);
+ rewrite > sym_times;rewrite < times_n_SO;apply reflexive_divides
+ |intro;elim (decidable_eq_nat n2 n1)
+ [rewrite > H3;rewrite < minus_n_n;
+ rewrite > times_n_SO in ⊢ (? ? %);apply reflexive_divides
+ |lapply (H n2)
+ [lapply (H (n1 - (S n2)))
+ [change in ⊢ (? ? %) with ((S n1)*n1!);
+ rewrite > (plus_minus_m_m n1 n2) in ⊢ (? ? (? (? %) ?))
+ [rewrite > sym_plus;
+ change in ⊢ (? ? (? % ?)) with ((S n2) + (n1 - n2));
+ rewrite > sym_times in \vdash (? ? %);
+ rewrite > distr_times_plus in ⊢ (? ? %);
+ simplify in ⊢ (? (? ? (? %)) ?);
+ apply divides_plus
+ [rewrite > sym_times;
+ change in ⊢ (? (? ? %) ?) with ((S n2)*n2!);
+ rewrite > sym_times in ⊢ (? (? ? %) ?);
+ rewrite < assoc_times;
+ apply divides_times
+ [rewrite > sym_times;assumption
+ |apply reflexive_divides]
+ |rewrite < fact_minus in ⊢ (? (? ? %) ?)
+ [rewrite > sym_times in ⊢ (? (? ? %) ?);
+ rewrite < assoc_times;
+ apply divides_times
+ [rewrite < eq_plus_minus_minus_minus in Hletin1;
+ [rewrite > sym_times;rewrite < minus_n_n in Hletin1;
+ rewrite < plus_n_O in Hletin1;assumption
+ |lapply (le_S_S_to_le ? ? H2);
+ elim (le_to_or_lt_eq ? ? Hletin2);
+ [assumption
+ |elim (H3 H4)]
+ |constructor 1]
+ |apply reflexive_divides]
+ |lapply (le_S_S_to_le ? ? H2);
+ elim (le_to_or_lt_eq ? ? Hletin2);
+ [assumption
+ |elim (H3 H4)]]]
+ |apply le_S_S_to_le;assumption]
+ |apply le_minus_m;apply le_S_S_to_le;assumption]
+ |apply le_S_S_to_le;assumption]]]]
+qed.
+
+theorem bc1: \forall n.\forall k. k < n \to bc (S n) (S k) = (bc n k) + (bc n (S k)).
+intros.unfold bc.
+rewrite > (lt_to_lt_to_eq_div_div_times_times ? ? (S k)) in ⊢ (? ? ? (? % ?))
+ [rewrite > sym_times in ⊢ (? ? ? (? (? ? %) ?)).
+ rewrite < assoc_times in ⊢ (? ? ? (? (? ? %) ?)).
+ rewrite > (lt_to_lt_to_eq_div_div_times_times ? ? (n - k)) in ⊢ (? ? ? (? ? %))
+ [rewrite > assoc_times in ⊢ (? ? ? (? ? (? ? %))).
+ rewrite > sym_times in ⊢ (? ? ? (? ? (? ? (? ? %)))).
+ rewrite > fact_minus
+ [rewrite < eq_div_plus
+ [rewrite < distr_times_plus.
+ simplify in ⊢ (? ? ? (? (? ? %) ?)).
+ rewrite > sym_plus in ⊢ (? ? ? (? (? ? (? %)) ?)).
+ rewrite < plus_minus_m_m
+ [rewrite > sym_times in ⊢ (? ? ? (? % ?)).
+ reflexivity
+ |apply lt_to_le.
+ assumption
+ ]
+ |rewrite > (times_n_O O).
+ apply lt_times;apply lt_O_fact
+ |change in ⊢ (? (? % ?) ?) with ((S k)*k!);
+ rewrite < sym_times in ⊢ (? ? %);
+ rewrite > assoc_times;apply divides_times
+ [apply reflexive_divides
+ |apply bc2;apply le_S_S_to_le;constructor 2;assumption]
+ |rewrite < fact_minus
+ [rewrite > sym_times in ⊢ (? (? ? %) ?);rewrite < assoc_times;
+ apply divides_times
+ [apply bc2;assumption
+ |apply reflexive_divides]
+ |assumption]]
+ |assumption]
+ |apply lt_to_lt_O_minus;assumption
+ |rewrite > (times_n_O O).
+ apply lt_times;apply lt_O_fact]
+|apply lt_O_S
+|rewrite > (times_n_O O).
+ apply lt_times;apply lt_O_fact]
+qed.
+
+theorem lt_O_bc: \forall n,m. m \le n \to O < bc n m.
+intro.elim n
+ [apply (le_n_O_elim ? H).
+ simplify.apply le_n
+ |elim (le_to_or_lt_eq ? ? H1)
+ [generalize in match H2.cases m;intro
+ [rewrite > bc_n_O.apply le_n
+ |rewrite > bc1
+ [apply (trans_le ? (bc n1 n2))
+ [apply H.apply le_S_S_to_le.apply lt_to_le.assumption
+ |apply le_plus_n_r
+ ]
+ |apply le_S_S_to_le.assumption
+ ]
+ ]
+ |rewrite > H2.
+ rewrite > bc_n_n.
+ apply le_n
+ ]
+ ]
+qed.
+
+theorem exp_plus_sigma_p:\forall a,b,n.
+exp (a+b) n = sigma_p (S n) (\lambda k.true)
+ (\lambda k.(bc n k)*(exp a (n-k))*(exp b k)).
+intros.elim n
+ [simplify.reflexivity
+ |simplify in ⊢ (? ? % ?).
+ rewrite > true_to_sigma_p_Sn
+ [rewrite > H;rewrite > sym_times in ⊢ (? ? % ?);
+ rewrite > distr_times_plus in ⊢ (? ? % ?);
+ rewrite < minus_n_n in ⊢ (? ? ? (? (? (? ? (? ? %)) ?) ?));
+ rewrite > sym_times in ⊢ (? ? (? % ?) ?);
+ rewrite > sym_times in ⊢ (? ? (? ? %) ?);
+ rewrite > distributive_times_plus_sigma_p in ⊢ (? ? (? % ?) ?);
+ rewrite > distributive_times_plus_sigma_p in ⊢ (? ? (? ? %) ?);
+ rewrite > true_to_sigma_p_Sn in ⊢ (? ? (? ? %) ?)
+ [rewrite < assoc_plus;rewrite < sym_plus in ⊢ (? ? (? % ?) ?);
+ rewrite > assoc_plus;
+ apply eq_f2
+ [rewrite > sym_times;rewrite > assoc_times;autobatch paramodulation
+ |rewrite > (sigma_p_gi ? ? O);
+ [rewrite < (eq_sigma_p_gh ? S pred n1 (S n1) (λx:nat.true)) in ⊢ (? ? (? (? ? %) ?) ?)
+ [rewrite > (sigma_p_gi ? ? O) in ⊢ (? ? ? %);
+ [rewrite > assoc_plus;apply eq_f2
+ [autobatch paramodulation;
+ |rewrite < sigma_p_plus_1;
+ rewrite < (eq_sigma_p_gh ? S pred n1 (S n1) (λx:nat.true)) in \vdash (? ? ? %);
+ [apply eq_sigma_p
+ [intros;reflexivity
+ |intros;rewrite > sym_times;rewrite > assoc_times;
+ rewrite > sym_times in ⊢ (? ? (? (? ? %) ?) ?);
+ rewrite > assoc_times;rewrite < assoc_times in ⊢ (? ? (? (? ? %) ?) ?);
+ rewrite > sym_times in ⊢ (? ? (? (? ? (? % ?)) ?) ?);
+ change in ⊢ (? ? (? (? ? (? % ?)) ?) ?) with (exp a (S (n1 - S x)));
+ rewrite < (minus_Sn_m ? ? H1);rewrite > minus_S_S;
+ rewrite > sym_times in \vdash (? ? (? ? %) ?);
+ rewrite > assoc_times;
+ rewrite > sym_times in ⊢ (? ? (? ? (? ? %)) ?);
+ change in \vdash (? ? (? ? (? ? %)) ?) with (exp b (S x));
+ rewrite > assoc_times in \vdash (? ? (? ? %) ?);
+ rewrite > sym_times in \vdash (? ? (? % ?) ?);
+ rewrite > sym_times in \vdash (? ? (? ? %) ?);
+ rewrite > assoc_times in \vdash (? ? ? %);
+ rewrite > sym_times in \vdash (? ? ? %);
+ rewrite < distr_times_plus;
+ rewrite > sym_plus;rewrite < bc1;
+ [reflexivity|assumption]]
+ |intros;simplify;reflexivity
+ |intros;simplify;reflexivity
+ |intros;apply le_S_S;assumption
+ |intros;reflexivity
+ |intros 2;elim j
+ [simplify in H2;destruct H2
+ |simplify;reflexivity]
+ |intro;elim j
+ [simplify in H2;destruct H2
+ |simplify;apply le_S_S_to_le;assumption]]]
+ |apply le_S_S;apply le_O_n
+ |reflexivity]
+ |intros;simplify;reflexivity
+ |intros;simplify;reflexivity
+ |intros;apply le_S_S;assumption
+ |intros;reflexivity
+ |intros 2;elim j
+ [simplify in H2;destruct H2
+ |simplify;reflexivity]
+ |intro;elim j
+ [simplify in H2;destruct H2
+ |simplify;apply le_S_S_to_le;assumption]]
+ |apply le_S_S;apply le_O_n
+ |reflexivity]]
+ |reflexivity]
+ |reflexivity]]
+qed.
+
+theorem exp_S_sigma_p:\forall a,n.
+exp (S a) n = sigma_p (S n) (\lambda k.true) (\lambda k.(bc n k)*(exp a (n-k))).
+intros.
+rewrite > plus_n_SO.
+rewrite > exp_plus_sigma_p.
+apply eq_sigma_p;intros
+ [reflexivity
+ |rewrite < exp_SO_n.
+ rewrite < times_n_SO.
+ reflexivity
+ ]
+qed.
+
+theorem exp_Sn_SSO: \forall n. exp (S n) 2 = S((exp n 2) + 2*n).
+intros.simplify.
+rewrite < times_n_SO.
+rewrite < plus_n_O.
+rewrite < sym_times.simplify.
+rewrite < assoc_plus.
+rewrite < sym_plus.
+reflexivity.
+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/primes.ma".
+
+(* successor mod n *)
+definition S_mod: nat → nat → nat ≝
+λn,m:nat. (S m) \mod n.
+
+definition congruent: nat → nat → nat → Prop ≝
+λ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 .
+// qed.
+
+theorem transitive_congruent:
+ ∀p.transitive nat (λn,m.congruent n m p).
+/2/ 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))
+% // @lt_mod_m_m @(ltn_to_ltO … ltnm)
+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 ⊢ (? ? % ?)
+>(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)))
+ [@div_mod_spec_div_mod //
+ |% [@lt_mod_m_m //] >distributive_times_plus_r
+ >associative_plus <div_mod >associative_times <div_mod //
+ ]
+qed.
+
+theorem congruent_n_mod_n : ∀n,p:nat. O < p →
+ n ≅_{p} (n \mod p).
+/2/ qed.
+
+theorem congruent_n_mod_times : ∀n,m,p:nat. O < p → O < m →
+ n ≅_{p} (n \mod (m*p)).
+/2/ 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
+@(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 //
+ ]
+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/
+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)))
+>commutative_times >(div_mod n p) in ⊢ (??%?)
+>(div_mod m p) in ⊢ (??%?) <(commutative_plus (m \mod p))
+<congnm <(minus_minus ? (n \mod p)) <minus_plus_m_m //
+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
+ ((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 //
+ ]
+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 //
+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. *)
@(div_mod_spec_to_eq (a*b) b … O (div_mod_spec_div_mod …))
// @div_mod_spec_intro // qed.
-(*
theorem div_n_n: ∀n:nat. O < n → n / n = 1.
/2/ qed.
theorem mod_n_n: ∀n:nat. O < n → n \mod n = O.
#n #posn
@(div_mod_spec_to_eq2 n n … 1 0 (div_mod_spec_div_mod …))
-/2/ qed. *)
+/2/ qed.
theorem mod_S: ∀n,m:nat. O < m → S (n \mod m) < m →
((S n) \mod m) = S (n \mod m).
@(div_mod_spec_to_eq2 (a*c) (b*c) (a/b) ((a*c) \mod (b*c)) (a/b) (c*(a \mod b)))
[>(div_times_times … posc) // @div_mod_spec_div_mod /2/
|@div_mod_spec_intro
- [(applyS monotonic_lt_times_l) /2/
+ [applyS (monotonic_lt_times_r … c posc) /2/
|(applyS (eq_f …(λx.x*c))) //
]
]
theorem le_exp: ∀n,m,p:nat. O < p →
n ≤m → p^n ≤ p^m.
-@nat_elim2
- [#n #m #ltm #len @lt_O_exp //
- |#n #m #_ #len @False_ind /2/
- |#n #m #Hind #p #posp #lenm normalize @le_times //
- @Hind /2/
+@nat_elim2 #n #m
+ [#ltm #len @lt_O_exp //
+ |#_ #len @False_ind /2/
+ |#Hind #p #posp #lenm normalize @le_times // @Hind /2/
]
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/primes.ma".
+
+let rec gcd_aux p m n: nat ≝
+match p with
+ [O ⇒ m
+ |S q ⇒
+ match dividesb n m with
+ [ true ⇒ n
+ | false ⇒ gcd_aux q n (m \mod n)]].
+
+definition gcd : nat → nat → nat ≝ λn,m:nat.
+ match leb n m with
+ [ true ⇒ gcd_aux n m n
+ | false ⇒ gcd_aux m n m ].
+
+theorem commutative_gcd: ∀n,m. gcd n m = gcd m n.
+#n #m normalize @leb_elim
+ [#lenm cases(le_to_or_lt_eq … lenm)
+ [#ltnm >not_le_to_leb_false // @lt_to_not_le //
+ |#eqnm >eqnm (cases (leb m m)) //
+ ]
+ |#notlenm >le_to_leb_true // @(transitive_le ? (S m)) //
+ @not_le_to_lt //
+ ]
+qed.
+
+theorem gcd_O_l: ∀m. gcd O m = m.
+// qed.
+
+theorem divides_mod: ∀p,m,n:nat. O < n →
+ p ∣ m → p ∣ n → p ∣ (m \mod n).
+#p #m #n #posn * #qm #eqm * #qn #eqn
+@(quotient ?? (qm - qn*(m / n))) >distributive_times_minus
+<eqm <associative_times <eqn @sym_eq @plus_to_minus /2/
+qed.
+
+theorem divides_mod_to_divides: ∀p,m,n:nat. O < n →
+ p ∣ (m \mod n) → p ∣ n → p ∣ m.
+#p #m #n #posn * #q1 #eq1 * #q2 #eq2
+@(quotient p m ((q2*(m / n))+q1)) >distributive_times_plus
+<eq1 <associative_times <eq2 /2/
+qed.
+
+lemma divides_to_gcd_aux: ∀p,m,n. O < p → O < n →n ∣ m →
+ gcd_aux p m n = n.
+#p #m #n #posp @(lt_O_n_elim … posp) #l #posn #divnm normalize
+>divides_to_dividesb_true normalize //
+qed.
+
+theorem divides_to_gcd: ∀m,n. O < n → n ∣ m →
+ gcd n m = n.
+#m #n #posn (cases m)
+ [>commutative_gcd //
+ |#l #divn (cut (n ≤ (S l))) [@divides_to_le //] #len normalize
+ >le_to_leb_true // normalize @divides_to_gcd_aux //
+ ]
+qed.
+
+lemma not_divides_to_gcd_aux: ∀p,m,n. 0 < n → n ∤ m →
+ gcd_aux (S p) m n = gcd_aux p n (m \mod n).
+#p #m #n #lenm #divnm normalize >not_divides_to_dividesb_false
+normalize // qed.
+
+theorem divides_gcd_aux_mn: ∀p,m,n. O < n → n ≤ m → n ≤ p →
+ gcd_aux p m n ∣ m ∧ gcd_aux p m n ∣ n.
+#p (elim p)
+ [#m #n #posn #lenm #lenO @False_ind @(absurd … posn) /2/
+ |#q #Hind #m #n #posn #lenm #lenS cases(decidable_divides n m)
+ [#divnm >(divides_to_gcd_aux … posn divnm) // % //
+ |#ndivnm >(not_divides_to_gcd_aux … posn ndivnm)
+ cut (gcd_aux q n (m \mod n) ∣ n ∧
+ gcd_aux q n (m \mod n) ∣ mod m n)
+ [cut (m \mod n < n) [@lt_mod_m_m //] #ltmod
+ @Hind
+ [cases(le_to_or_lt_eq … (le_O_n (m \mod n))) // #modO
+ @False_ind @(absurd ?? ndivnm) @mod_O_to_divides //
+ |/2/
+ |@le_S_S_to_le @(transitive_le … ltmod lenS)
+ ]
+ |* #H #H1 % [@(divides_mod_to_divides … posn H1) // |//]
+ ]
+ ]
+ ]
+qed.
+
+theorem divides_gcd_nm: ∀n,m.
+ gcd n m ∣ m ∧ gcd n m ∣ n.
+#n #m cases(le_to_or_lt_eq …(le_O_n n)) [|#eqnO <eqnO /2/]
+#posn cases(le_to_or_lt_eq …(le_O_n m)) [|#eqmO <eqmO /2/]
+#posm normalize @leb_elim normalize
+ [#lenm @divides_gcd_aux_mn //
+ |#notlt normalize cut (∀A,B. A∧B → B∧A) [#A #B * /2/] #sym_and
+ @sym_and @divides_gcd_aux_mn // @(transitive_le ? (S m)) //
+ @not_le_to_lt //
+ ]
+qed.
+
+theorem divides_gcd_l: ∀n,m. gcd n m ∣ n.
+#n #m @(proj2 ? ? (divides_gcd_nm n m)).
+qed.
+
+theorem divides_gcd_r: \forall n,m. gcd n m ∣ m.
+#n #m @(proj1 ? ? (divides_gcd_nm n m)).
+qed.
+
+theorem divides_times_gcd_aux: ∀p,m,n,d,c.
+ O < c → O < n → n ≤ m → n ≤ p →
+ d ∣ (c*m) → d ∣ (c*n) → d ∣ c*gcd_aux p m n.
+#p (elim p)
+ [#m #n #d #c #_ #posn #_ #lenO @False_ind @(absurd … lenO) /2/
+ |#q #Hind #m #n #d #c #posc #posn #lenm #lenS #dcm #dcn
+ cases(decidable_divides n m)
+ [#divnm >(divides_to_gcd_aux … posn divnm) //
+ |#ndivnm >(not_divides_to_gcd_aux … posn ndivnm)
+ cut (m \mod n < n) [@lt_mod_m_m //] #ltmod
+ @Hind //
+ [cases(le_to_or_lt_eq … (le_O_n (m \mod n))) // #modO
+ @False_ind @(absurd ?? ndivnm) @mod_O_to_divides //
+ |/2/
+ |@le_S_S_to_le @(transitive_le … ltmod lenS)
+ |<times_mod // < (commutative_times c m)
+ <(commutative_times c n) @divides_mod //
+ >(times_n_O 0) @lt_times //
+ ]
+ ]
+ ]
+qed.
+
+(*a particular case of the previous theorem, with c=1 *)
+theorem divides_gcd_aux: ∀p,m,n,d. O < n → n ≤ m → n ≤ p →
+ d ∣ m \to d ∣ n \to d ∣ gcd_aux p m n.
+ (* bell'esempio di smart application *)
+/2/ qed.
+
+theorem divides_d_times_gcd: ∀m,n,d,c. O < c →
+ d ∣ (c*m) → d ∣ (c*n) → d ∣ c*gcd n m.
+#m #n #d #c #posc #dcm #dcn
+cases(le_to_or_lt_eq …(le_O_n n)) [|#eqnO <eqnO @dcm] #posn
+cases(le_to_or_lt_eq …(le_O_n m)) [|#eqmO <eqmO <commutative_gcd @dcn] #posm
+normalize @leb_elim normalize
+ [#lenm @divides_times_gcd_aux //
+ |#nlenm @divides_times_gcd_aux //
+ @(transitive_le ? (S m)) // @not_le_to_lt //
+ ]
+qed.
+
+(* a particular case of the previous theorem, with c=1 *)
+theorem divides_d_gcd: ∀m,n,d.
+ d ∣ m → d ∣ n → d ∣ gcd n m.
+/2/ (* bello *)
+qed.
+
+theorem eq_minus_gcd_aux: ∀p,m,n.O < n → n ≤ m → n ≤ p →
+ ∃a,b. a*n - b*m = gcd_aux p m n ∨ b*m - a*n = gcd_aux p m n.
+#p (elim p)
+ [#m #n #posn #lenm #lenO @False_ind @(absurd … posn) /2/
+ |#q #Hind #m #n #posn #lenm #lenS
+ cut (0 < m) [@lt_to_le_to_lt //] #posm
+ cases(decidable_divides n m)
+ [#divnm >(divides_to_gcd_aux … posn divnm) //
+ @(ex_intro ?? 1) @(ex_intro ?? 0) %1 //
+ |#ndivnm >(not_divides_to_gcd_aux … posn ndivnm)
+ cut (m \mod n < n) [@lt_mod_m_m //] #ltmod
+ lapply (Hind n (m \mod n) ???)
+ [@le_S_S_to_le @(transitive_le … ltmod lenS)
+ |/2/
+ |cases(le_to_or_lt_eq … (le_O_n (m \mod n))) // #modO
+ @False_ind @(absurd ?? ndivnm) @mod_O_to_divides //
+ ]
+ * #a * #b * #H
+ [(* first case *)
+ <H @(ex_intro ?? (b+a*(m / n))) @(ex_intro ?? a) %2
+ <commutative_plus >distributive_times_plus_r
+ >(div_mod m n) in ⊢(? ? (? % ?) ?)
+ >associative_times <commutative_plus >distributive_times_plus
+ <minus_minus <commutative_plus <plus_minus //
+ |(* second case *)
+ <H @(ex_intro ?? (b+a*(m / n))) @(ex_intro ?? a) %1
+ >distributive_times_plus_r
+ >(div_mod m n) in ⊢ (? ? (? ? %) ?)
+ >distributive_times_plus >associative_times
+ <minus_minus <commutative_plus <plus_minus //
+ ]
+ ]
+ ]
+qed.
+
+theorem eq_minus_gcd:
+ ∀m,n.∃ a,b.a*n - b*m = gcd n m ∨ b*m - a*n = gcd n m.
+ #m #n cases(le_to_or_lt_eq …(le_O_n n))
+ [|#eqn0 >eqn0 @(ex_intro ?? O) @(ex_intro ? ? 1) %2 applyS minus_n_O]
+#posn cases(le_to_or_lt_eq …(le_O_n m))
+ [|#eqm0 >eqm0 @(ex_intro ?? 1) @(ex_intro ? ? 0) %1 applyS minus_n_O]
+#posm normalize @leb_elim normalize
+ [#lenm @eq_minus_gcd_aux //
+ |#nlenm lapply(eq_minus_gcd_aux m n m posm ? (le_n m))
+ [@(transitive_le … (not_le_to_lt … nlenm)) //]
+ * #a * #b * #H @(ex_intro ?? b) @(ex_intro ?? a) [%2 // |%1 //]
+ ]
+qed.
+
+(* some properties of gcd *)
+
+theorem gcd_O_to_eq_O:∀m,n:nat.
+ gcd m n = O → m = O ∧ n = O.
+#m #n #H cut (O ∣ n ∧ O ∣ m)
+ [<H @divides_gcd_nm| * * #q1 #H1 * #q2 #H2 % // ]
+qed.
+
+theorem lt_O_gcd:∀m,n:nat. O < n → O < gcd m n.
+#m #n #posn @(nat_case (gcd m n)) //
+#H (cases (gcd_O_to_eq_O m n H)) //
+qed.
+
+theorem gcd_n_n: ∀n.gcd n n = n.
+#n (cases n) //
+#m @le_to_le_to_eq
+ [@divides_to_le //
+ |@divides_to_le (*/2/*) [@lt_O_gcd // |@divides_d_gcd // ]
+ ]
+qed.
+
+(* some properties or relative primes - i.e. gcd = 1 *)
+theorem gcd_1_to_lt_O: ∀i,n. 1 < n → gcd i n = 1 → O < i.
+#i #n #lt1n #gcd1 cases (le_to_or_lt_eq ?? (le_O_n i)) //
+#iO @False_ind @(absurd … gcd1) <iO normalize
+@sym_not_eq @lt_to_not_eq //
+qed.
+
+theorem gcd_1_to_lt_n: ∀i,n. 1 < n →
+ i ≤ n → gcd i n = 1 → i < n.
+#i #n #lt1n #lein #gcd1 cases (le_to_or_lt_eq ?? lein) //
+(* impressive *)
+qed.
+
+theorem gcd_n_times_nm: ∀n,m. O < m → gcd n (n*m) = n.
+#n #m #posm @(nat_case n) //
+#l #eqn @le_to_le_to_eq
+ [@divides_to_le //
+ |@divides_to_le
+ [@lt_O_gcd >(times_n_O O) @lt_times // |@divides_d_gcd /2/]
+ ]
+qed.
+
+theorem le_gcd_times: ∀m,n,p. O< p → gcd m n ≤ gcd m (n*p).
+#m #n #p #posp @(nat_case n) //
+#l #eqn @divides_to_le [@lt_O_gcd >(times_n_O O) @lt_times //]
+@divides_d_gcd [@(transitive_divides ? (S l)) /2/ |//]
+qed.
+
+theorem gcd_times_SO_to_gcd_SO: ∀m,n,p:nat. O < n → O < p →
+ gcd m (n*p) = 1 → gcd m n = 1.
+#m #n #p #posn #posp #gcd1 @le_to_le_to_eq
+ [<gcd1 @le_gcd_times // | @lt_O_gcd //]
+qed.
+
+(* for the "converse" of the previous result see the end of this development *)
+
+theorem eq_gcd_SO_to_not_divides: ∀n,m. 1 < n →
+ gcd n m = 1 → n ∤ m.
+#n #m #lt1n #gcd1 @(not_to_not … (gcd n m = n))
+ [#divnm @divides_to_gcd /2/ | /2/]
+qed.
+
+theorem gcd_SO_n: ∀n:nat. gcd 1 n = 1.
+#n @le_to_le_to_eq
+ [@divides_to_le // |>commutative_gcd @lt_O_gcd //]
+qed.
+
+theorem divides_gcd_mod: ∀m,n:nat. O < n →
+ gcd m n ∣ gcd n (m \mod n).
+#m #n #posn @divides_d_gcd [@divides_mod // | //]
+qed.
+
+theorem divides_mod_gcd: ∀m,n:nat. O < n →
+ gcd n (m \mod n) ∣ gcd m n.
+#m #n #posn @divides_d_gcd
+ [@divides_gcd_l |@(divides_mod_to_divides ?? n) //]
+qed.
+
+theorem gcd_mod: ∀m,n:nat. O < n →
+ gcd n (m \mod n) = gcd m n.
+#m #n #posn @antisymmetric_divides
+ [@divides_mod_gcd // | @divides_gcd_mod //]
+qed.
+
+(* gcd and primes *)
+
+theorem prime_to_gcd_1: ∀n,m:nat. prime n → n ∤ m →
+ gcd n m = 1.
+(* bella dimostrazione *)
+#n #m * #lt1n #primen #ndivnm @le_to_le_to_eq
+ [@not_lt_to_le @(not_to_not … (primen (gcd n m) (divides_gcd_l …)))
+ @(not_to_not ? (n ∣m)) //
+ |@lt_O_gcd @not_eq_to_le_to_lt // @(not_to_not ? (n ∣ m)) //
+ ]
+qed.
+
+(* primes and divides *)
+theorem divides_times_to_divides: ∀p,n,m:nat.prime p →
+ p ∣ n*m → p ∣ n ∨ p ∣ m.
+#p #n #m #primp * #c #nm
+cases (decidable_divides p n) /2/ #ndivpn %2
+cut (∃a,b. a*n - b*p = 1 ∨ b*p - a*n = 1)
+ [<(prime_to_gcd_1 … primp ndivpn) >commutative_gcd @eq_minus_gcd]
+* #a * #b * #H
+ [@(quotient ?? (a*c-b*m)) >distributive_times_minus <associative_times
+ >(commutative_times p) >associative_times <nm <associative_times
+ <associative_times <commutative_times >(commutative_times (p*b))
+ <distributive_times_minus //
+ |@(quotient ?? (b*m -a*c)) >distributive_times_minus <(associative_times p)
+ <(associative_times p) <(commutative_times a) >(associative_times a)
+ <nm <(associative_times a) <commutative_times >(commutative_times (a*n))
+ <distributive_times_minus //
+ ]
+qed.
+
+theorem divides_exp_to_divides:
+∀p,n,m:nat. prime p → p ∣n^m → p ∣ n.
+#p #n #m #primep (elim m) normalize /2/
+#l #Hind #H cases(divides_times_to_divides … primep H) /2/
+qed.
+
+theorem divides_exp_to_eq:
+∀p,q,m:nat. prime p → prime q →
+ p ∣ q^m → p = q.
+#p #q #m #H * #lt1q #primeq #H @primeq /2/
+qed.
+
+(* relative primes *)
+theorem eq_gcd_times_1: ∀p,n,m:nat. O < n → O < m →
+ gcd p n = 1 → gcd p m = 1 → gcd p (n*m) = 1.
+#p #n #m #posn #posm #primepn #primepm
+@le_to_le_to_eq [|@lt_O_gcd >(times_n_O 0) @lt_times //]
+@not_lt_to_le % #lt1gcd
+cut (smallest_factor (gcd p (n*m)) ∣ n ∨
+ smallest_factor (gcd p (n*m)) ∣ m)
+ [@divides_times_to_divides
+ [@prime_smallest_factor_n //
+ |@(transitive_divides ? (gcd p (n*m))) //
+ @divides_smallest_factor_n /2/
+ ]
+ |* #H
+ [@(absurd ?? (lt_to_not_le …(lt_SO_smallest_factor … lt1gcd)))
+ <primepn @divides_to_le // @divides_d_gcd //
+ @(transitive_divides … (divides_smallest_factor_n …))
+ [@lt_O_gcd >(times_n_O 0) @lt_times // | //]
+ |@(absurd ?? (lt_to_not_le … (lt_SO_smallest_factor …lt1gcd)))
+ <primepm @divides_to_le // @divides_d_gcd //
+ @(transitive_divides … (divides_smallest_factor_n …))
+ [@lt_O_gcd >(times_n_O 0) @lt_times // | //]
+ ]
+qed.
+
+
+theorem gcd_1_to_divides_times_to_divides: ∀p,n,m:nat. O < p →
+gcd p n = 1 → p ∣ (n*m) → p ∣ m.
+#p #m #n #posn #gcd1 * #c #nm
+cases(eq_minus_gcd m p) #a * #b * #H >gcd1 in H #H
+ [@(quotient ?? (a*n-c*b)) >distributive_times_minus <associative_times
+ <associative_times <nm >(commutative_times m) >commutative_times
+ >associative_times <distributive_times_minus //
+ |@(quotient ?? (c*b-a*n)) >distributive_times_minus <associative_times
+ <associative_times <nm >(commutative_times m) <(commutative_times n)
+ >associative_times <distributive_times_minus //
+ ]
+qed.
+
+(*
+theorem divides_to_divides_times1: \forall p,q,n. prime p \to prime q \to p \neq q \to
+divides p n \to divides q n \to divides (p*q) n.
+intros.elim H3.
+rewrite > H5 in H4.
+elim (divides_times_to_divides ? ? ? H1 H4)
+ [elim H.apply False_ind.
+ apply H2.apply sym_eq.apply H8
+ [assumption
+ |apply prime_to_lt_SO.assumption
+ ]
+ |elim H6.
+ apply (witness ? ? n1).
+ rewrite > assoc_times.
+ rewrite < H7.assumption
+ ]
+qed.
+*)
+
+theorem divides_to_divides_times: ∀p,q,n. prime p → p ∤ q →
+ p ∣ n → q ∣ n → p*q ∣ n.
+#p #q #n #primep #notdivpq #divpn * #b #eqn (>eqn in divpn)
+#divpn cases(divides_times_to_divides ??? primep divpn) #H
+ [@False_ind /2/
+ |cases H #c #eqb @(quotient ?? c) >eqb <associative_times //
+ ]
+qed.
\ No newline at end of file
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| A.Asperti, C.Sacerdoti Coen, *)
+(* ||A|| E.Tassi, S.Zacchiroli *)
+(* \ / *)
+(* \ / Matita is distributed under the terms of the *)
+(* v GNU Lesser General Public License Version 2.1 *)
+(* *)
+(**************************************************************************)
+
+(*
+include "datatypes/constructors.ma".
+include "nat/minimization.ma".
+include "nat/relevant_equations.ma".
+include "nat/primes.ma".
+include "nat/iteration2.ma".
+include "nat/div_and_mod_diseq.ma".
+
+definition log \def \lambda p,n.
+max n (\lambda x.leb (exp p x) n).
+
+theorem le_exp_log: \forall p,n. O < n \to
+exp p (log p n) \le n.
+intros.
+apply leb_true_to_le.
+unfold log.
+apply (f_max_true (\lambda x.leb (exp p x) n)).
+apply (ex_intro ? ? O).
+split
+ [apply le_O_n
+ |apply le_to_leb_true.simplify.assumption
+ ]
+qed.
+
+theorem log_SO: \forall n. S O < n \to log n (S O) = O.
+intros.
+apply sym_eq.apply le_n_O_to_eq.
+apply (le_exp_to_le n)
+ [assumption
+ |simplify in ⊢ (? ? %).
+ apply le_exp_log.
+ apply le_n
+ ]
+qed.
+
+theorem lt_to_log_O: \forall n,m. O < m \to m < n \to log n m = O.
+intros.
+apply sym_eq.apply le_n_O_to_eq.
+apply le_S_S_to_le.
+apply (lt_exp_to_lt n)
+ [apply (le_to_lt_to_lt ? m);assumption
+ |simplify in ⊢ (? ? %).
+ rewrite < times_n_SO.
+ apply (le_to_lt_to_lt ? m)
+ [apply le_exp_log.assumption
+ |assumption
+ ]
+ ]
+qed.
+
+theorem lt_log_n_n: \forall p, n. S O < p \to O < n \to log p n < n.
+intros.
+cut (log p n \le n)
+ [elim (le_to_or_lt_eq ? ? Hcut)
+ [assumption
+ |absurd (exp p n \le n)
+ [rewrite < H2 in ⊢ (? (? ? %) ?).
+ apply le_exp_log.
+ assumption
+ |apply lt_to_not_le.
+ apply lt_m_exp_nm.
+ assumption
+ ]
+ ]
+ |unfold log.apply le_max_n
+ ]
+qed.
+
+theorem lt_O_log: \forall p,n. O < n \to p \le n \to O < log p n.
+intros.
+unfold log.
+apply not_lt_to_le.
+intro.
+apply (leb_false_to_not_le ? ? ? H1).
+rewrite > (exp_n_SO p).
+apply (lt_max_to_false ? ? ? H2).
+assumption.
+qed.
+
+theorem le_log_n_n: \forall p,n. S O < p \to log p n \le n.
+intros.
+cases n
+ [apply le_n
+ |apply lt_to_le.
+ apply lt_log_n_n
+ [assumption|apply lt_O_S]
+ ]
+qed.
+
+theorem lt_exp_log: \forall p,n. S O < p \to n < exp p (S (log p n)).
+intros.cases n
+ [simplify.rewrite < times_n_SO.apply lt_to_le.assumption
+ |apply not_le_to_lt.
+ apply leb_false_to_not_le.
+ apply (lt_max_to_false ? (S n1) (S (log p (S n1))))
+ [apply le_S_S.apply le_n
+ |apply lt_log_n_n
+ [assumption|apply lt_O_S]
+ ]
+ ]
+qed.
+
+theorem log_times1: \forall p,n,m. S O < p \to O < n \to O < m \to
+log p (n*m) \le S(log p n+log p m).
+intros.
+unfold in ⊢ (? (% ? ?) ?).
+apply f_false_to_le_max
+ [apply (ex_intro ? ? O).
+ split
+ [apply le_O_n
+ |apply le_to_leb_true.
+ simplify.
+ rewrite > times_n_SO.
+ apply le_times;assumption
+ ]
+ |intros.
+ apply lt_to_leb_false.
+ apply (lt_to_le_to_lt ? ((exp p (S(log p n)))*(exp p (S(log p m)))))
+ [apply lt_times;apply lt_exp_log;assumption
+ |rewrite < exp_plus_times.
+ apply le_exp
+ [apply lt_to_le.assumption
+ |simplify.
+ rewrite < plus_n_Sm.
+ assumption
+ ]
+ ]
+ ]
+qed.
+
+theorem log_times: \forall p,n,m.S O < p \to log p (n*m) \le S(log p n+log p m).
+intros.
+cases n
+ [apply le_O_n
+ |cases m
+ [rewrite < times_n_O.
+ apply le_O_n
+ |apply log_times1
+ [assumption
+ |apply lt_O_S
+ |apply lt_O_S
+ ]
+ ]
+ ]
+qed.
+
+theorem log_times_l: \forall p,n,m.O < n \to O < m \to S O < p \to
+log p n+log p m \le log p (n*m) .
+intros.
+unfold log in ⊢ (? ? (% ? ?)).
+apply f_m_to_le_max
+ [elim H
+ [rewrite > log_SO
+ [simplify.
+ rewrite < plus_n_O.
+ apply le_log_n_n.
+ assumption
+ |assumption
+ ]
+ |elim H1
+ [rewrite > log_SO
+ [rewrite < plus_n_O.
+ rewrite < times_n_SO.
+ apply le_log_n_n.
+ assumption
+ |assumption
+ ]
+ |apply (trans_le ? (S n1 + S n2))
+ [apply le_plus;apply le_log_n_n;assumption
+ |simplify.
+ apply le_S_S.
+ rewrite < plus_n_Sm.
+ change in ⊢ (? % ?) with ((S n1)+n2).
+ rewrite > sym_plus.
+ apply le_plus_r.
+ change with (n1 < n1*S n2).
+ rewrite > times_n_SO in ⊢ (? % ?).
+ apply lt_times_r1
+ [assumption
+ |apply le_S_S.assumption
+ ]
+ ]
+ ]
+ ]
+ |apply le_to_leb_true.
+ rewrite > exp_plus_times.
+ apply le_times;apply le_exp_log;assumption
+ ]
+qed.
+
+theorem log_exp: \forall p,n,m.S O < p \to O < m \to
+log p ((exp p n)*m)=n+log p m.
+intros.
+unfold log in ⊢ (? ? (% ? ?) ?).
+apply max_spec_to_max.
+unfold max_spec.
+split
+ [split
+ [elim n
+ [simplify.
+ rewrite < plus_n_O.
+ apply le_log_n_n.
+ assumption
+ |simplify.
+ rewrite > assoc_times.
+ apply (trans_le ? ((S(S O))*(p\sup n1*m)))
+ [apply le_S_times_SSO
+ [rewrite > (times_n_O O) in ⊢ (? % ?).
+ apply lt_times
+ [apply lt_O_exp.
+ apply lt_to_le.
+ assumption
+ |assumption
+ ]
+ |assumption
+ ]
+ |apply le_times
+ [assumption
+ |apply le_n
+ ]
+ ]
+ ]
+ |simplify.
+ apply le_to_leb_true.
+ rewrite > exp_plus_times.
+ apply le_times_r.
+ apply le_exp_log.
+ assumption
+ ]
+ |intros.
+ simplify.
+ apply lt_to_leb_false.
+ apply (lt_to_le_to_lt ? ((exp p n)*(exp p (S(log p m)))))
+ [apply lt_times_r1
+ [apply lt_O_exp.apply lt_to_le.assumption
+ |apply lt_exp_log.assumption
+ ]
+ |rewrite < exp_plus_times.
+ apply le_exp
+ [apply lt_to_le.assumption
+ |rewrite < plus_n_Sm.
+ assumption
+ ]
+ ]
+ ]
+qed.
+
+theorem eq_log_exp: \forall p,n.S O < p \to
+log p (exp p n)=n.
+intros.
+rewrite > times_n_SO in ⊢ (? ? (? ? %) ?).
+rewrite > log_exp
+ [rewrite > log_SO
+ [rewrite < plus_n_O.reflexivity
+ |assumption
+ ]
+ |assumption
+ |apply le_n
+ ]
+qed.
+
+theorem log_exp1: \forall p,n,m.S O < p \to
+log p (exp n m) \le m*S(log p n).
+intros.elim m
+ [simplify in ⊢ (? (? ? %) ?).
+ rewrite > log_SO
+ [apply le_O_n
+ |assumption
+ ]
+ |simplify.
+ apply (trans_le ? (S (log p n+log p (n\sup n1))))
+ [apply log_times.assumption
+ |apply le_S_S.
+ apply le_plus_r.
+ assumption
+ ]
+ ]
+qed.
+
+theorem log_exp2: \forall p,n,m.S O < p \to O < n \to
+m*(log p n) \le log p (exp n m).
+intros.
+apply le_S_S_to_le.
+apply (lt_exp_to_lt p)
+ [assumption
+ |rewrite > sym_times.
+ rewrite < exp_exp_times.
+ apply (le_to_lt_to_lt ? (exp n m))
+ [elim m
+ [simplify.apply le_n
+ |simplify.apply le_times
+ [apply le_exp_log.
+ assumption
+ |assumption
+ ]
+ ]
+ |apply lt_exp_log.
+ assumption
+ ]
+ ]
+qed.
+
+lemma le_log_plus: \forall p,n.S O < p \to log p n \leq log p (S n).
+intros;apply (bool_elim ? (leb (p*(exp p n)) (S n)))
+ [simplify;intro;rewrite > H1;simplify;apply (trans_le ? n)
+ [apply le_log_n_n;assumption
+ |apply le_n_Sn]
+ |intro;unfold log;simplify;rewrite > H1;simplify;apply le_max_f_max_g;
+ intros;apply le_to_leb_true;constructor 2;apply leb_true_to_le;assumption]
+qed.
+
+theorem le_log: \forall p,n,m. S O < p \to n \le m \to
+log p n \le log p m.
+intros.elim H1
+ [constructor 1
+ |apply (trans_le ? ? ? H3);apply le_log_plus;assumption]
+qed.
+
+theorem log_div: \forall p,n,m. S O < p \to O < m \to m \le n \to
+log p (n/m) \le log p n -log p m.
+intros.
+apply le_plus_to_minus_r.
+apply (trans_le ? (log p ((n/m)*m)))
+ [apply log_times_l
+ [apply le_times_to_le_div
+ [assumption
+ |rewrite < times_n_SO.
+ assumption
+ ]
+ |assumption
+ |assumption
+ ]
+ |apply le_log
+ [assumption
+ |rewrite > (div_mod n m) in ⊢ (? ? %)
+ [apply le_plus_n_r
+ |assumption
+ ]
+ ]
+ ]
+qed.
+
+theorem log_n_n: \forall n. S O < n \to log n n = S O.
+intros.
+rewrite > exp_n_SO in ⊢ (? ? (? ? %) ?).
+rewrite > times_n_SO in ⊢ (? ? (? ? %) ?).
+rewrite > log_exp
+ [rewrite > log_SO
+ [reflexivity
+ |assumption
+ ]
+ |assumption
+ |apply le_n
+ ]
+qed.
+
+theorem log_i_SSOn: \forall n,i. S O < n \to n < i \to i \le ((S(S O))*n) \to
+log i ((S(S O))*n) = S O.
+intros.
+apply antisymmetric_le
+ [apply not_lt_to_le.intro.
+ apply (lt_to_not_le ((S(S O)) * n) (exp i (S(S O))))
+ [rewrite > exp_SSO.
+ apply lt_times
+ [apply (le_to_lt_to_lt ? n);assumption
+ |assumption
+ ]
+ |apply (trans_le ? (exp i (log i ((S(S O))*n))))
+ [apply le_exp
+ [apply (ltn_to_ltO ? ? H1)
+ |assumption
+ ]
+ |apply le_exp_log.
+ rewrite > (times_n_O O) in ⊢ (? % ?).
+ apply lt_times
+ [apply lt_O_S
+ |apply lt_to_le.assumption
+ ]
+ ]
+ ]
+ |apply (trans_le ? (log i i))
+ [rewrite < (log_n_n i) in ⊢ (? % ?)
+ [apply le_log
+ [apply (trans_lt ? n);assumption
+ |apply le_n
+ ]
+ |apply (trans_lt ? n);assumption
+ ]
+ |apply le_log
+ [apply (trans_lt ? n);assumption
+ |assumption
+ ]
+ ]
+ ]
+qed.
+
+theorem exp_n_O: \forall n. O < n \to exp O n = O.
+intros.apply (lt_O_n_elim ? H).intros.
+simplify.reflexivity.
+qed.
+
+(*
+theorem tech1: \forall n,i.O < n \to
+(exp (S n) (S(S i)))/(exp n (S i)) \le ((exp n i) + (exp (S n) (S i)))/(exp n i).
+intros.
+simplify in ⊢ (? (? ? %) ?).
+rewrite < eq_div_div_div_times
+ [apply monotonic_div
+ [apply lt_O_exp.assumption
+ |apply le_S_S_to_le.
+ apply lt_times_to_lt_div.
+ change in ⊢ (? % ?) with ((exp (S n) (S i)) + n*(exp (S n) (S i))).
+
+
+ |apply (trans_le ? ((n)\sup(i)*(S n)\sup(S i)/(n)\sup(S i)))
+ [apply le_times_div_div_times.
+ apply lt_O_exp.assumption
+ |apply le_times_to_le_div2
+ [apply lt_O_exp.assumption
+ |simplify.
+
+theorem tech1: \forall a,b,n,m.O < m \to
+n/m \le b \to (a*n)/m \le a*b.
+intros.
+apply le_times_to_le_div2
+ [assumption
+ |
+
+theorem tech2: \forall n,m. O < n \to
+(exp (S n) m) / (exp n m) \le (n + m)/n.
+intros.
+elim m
+ [rewrite < plus_n_O.simplify.
+ rewrite > div_n_n.apply le_n
+ |apply le_times_to_le_div
+ [assumption
+ |apply (trans_le ? (n*(S n)\sup(S n1)/(n)\sup(S n1)))
+ [apply le_times_div_div_times.
+ apply lt_O_exp
+ |simplify in ⊢ (? (? ? %) ?).
+ rewrite > sym_times in ⊢ (? (? ? %) ?).
+ rewrite < eq_div_div_div_times
+ [apply le_times_to_le_div2
+ [assumption
+ |
+
+
+theorem le_log_sigma_p:\forall n,m,p. O < m \to S O < p \to
+log p (exp n m) \le sigma_p n (\lambda i.true) (\lambda i. (m / i)).
+intros.
+elim n
+ [rewrite > exp_n_O
+ [simplify.apply le_n
+ |assumption
+ ]
+ |rewrite > true_to_sigma_p_Sn
+ [apply (trans_le ? (m/n1+(log p (exp n1 m))))
+ [
+*)
+*)
[#n #leSO @False_ind /2/
|#n #m #Hind #leSS #b
(cases (true_or_false (f b))) #fb
- [lapply (true_min …fb) //
+ [lapply (true_min …fb) #H >H >H //
|>false_min // >false_min // @Hind /2/
]
]
qed.
theorem f_min_true : ∀ f.∀n,b.
-(∃i:nat. b ≤ i ∧ i < n ∧ f i = true) → f (min n b f) = true.
+(∃i:nat. b ≤ i ∧ i < n + b ∧ f i = true) → f (min n b f) = true.
#f #n #b cases(min_to_min_spec f n b (min n b f) (refl …)) //
#Hall * #x * * #leb #ltx #fx @False_ind @(absurd … fx) >Hall /2/
qed.
lemma times_times: ∀x,y,z. x*(y*z) = y*(x*z).
// qed.
+theorem times_n_1 : ∀n:nat. n = n * 1.
+#n // qed.
+
(* ci servono questi risultati?
theorem times_O_to_O: ∀n,m:nat.n*m=O → n=O ∨ m=O.
napply nat_elim2 /2/
qed.
(* some properties of functions *)
-(*
-definition increasing \def \lambda f:nat \to nat.
-\forall n:nat. f n < f (S n).
-
-theorem increasing_to_monotonic: \forall f:nat \to nat.
-increasing f \to monotonic nat lt f.
-unfold monotonic.unfold lt.unfold increasing.unfold lt.intros.elim H1.apply H.
-apply (trans_le ? (f n1)).
-assumption.apply (trans_le ? (S (f n1))).
-apply le_n_Sn.
-apply H.
+
+definition increasing ≝ λf:nat → nat. ∀n:nat. f n < f (S n).
+
+theorem increasing_to_monotonic: ∀f:nat → nat.
+ increasing f → monotonic nat lt f.
+#f #incr #n #m #ltnm (elim ltnm) /2/
qed.
-theorem le_n_fn: \forall f:nat \to nat. (increasing f)
-\to \forall n:nat. n \le (f n).
-intros.elim n.
-apply le_O_n.
-apply (trans_le ? (S (f n1))).
-apply le_S_S.apply H1.
-simplify in H. unfold increasing in H.unfold lt in H.apply H.
+theorem le_n_fn: ∀f:nat → nat.
+ increasing f → ∀n:nat. n ≤ f n.
+#f #incr #n (elim n) /2/
qed.
-theorem increasing_to_le: \forall f:nat \to nat. (increasing f)
-\to \forall m:nat. \exists i. m \le (f i).
-intros.elim m.
-apply (ex_intro ? ? O).apply le_O_n.
-elim H1.
-apply (ex_intro ? ? (S a)).
-apply (trans_le ? (S (f a))).
-apply le_S_S.assumption.
-simplify in H.unfold increasing in H.unfold lt in H.
-apply H.
+theorem increasing_to_le: ∀f:nat → nat.
+ increasing f → ∀m:nat.∃i.m ≤ f i.
+#f #incr #m (elim m) /2/#n * #a #lenfa
+@(ex_intro ?? (S a)) /2/
qed.
-theorem increasing_to_le2: \forall f:nat \to nat. (increasing f)
-\to \forall m:nat. (f O) \le m \to
-\exists i. (f i) \le m \land m <(f (S i)).
-intros.elim H1.
-apply (ex_intro ? ? O).
-split.apply le_n.apply H.
-elim H3.elim H4.
-cut ((S n1) < (f (S a)) \lor (S n1) = (f (S a))).
-elim Hcut.
-apply (ex_intro ? ? a).
-split.apply le_S. assumption.assumption.
-apply (ex_intro ? ? (S a)).
-split.rewrite < H7.apply le_n.
-rewrite > H7.
-apply H.
-apply le_to_or_lt_eq.apply H6.
+theorem increasing_to_le2: ∀f:nat → nat. increasing f →
+ ∀m:nat. f 0 ≤ m → ∃i. f i ≤ m ∧ m < f (S i).
+#f #incr #m #lem (elim lem)
+ [@(ex_intro ? ? O) /2/
+ |#n #len * #a * #len #ltnr (cases(le_to_or_lt_eq … ltnr)) #H
+ [@(ex_intro ? ? a) % /2/
+ |@(ex_intro ? ? (S a)) % //
+ ]
+ ]
+qed.
+
+theorem increasing_to_injective: ∀f:nat → nat.
+ increasing f → injective nat nat f.
+#f #incr #n #m cases(decidable_le n m)
+ [#lenm cases(le_to_or_lt_eq … lenm) //
+ #lenm #eqf @False_ind @(absurd … eqf) @lt_to_not_eq
+ @increasing_to_monotonic //
+ |#nlenm #eqf @False_ind @(absurd … eqf) @sym_not_eq
+ @lt_to_not_eq @increasing_to_monotonic /2/
+ ]
qed.
-*)
(*********************** monotonicity ***************************)
theorem monotonic_le_plus_r:
apply lt_plus.assumption.assumption.
qed. *)
-theorem monotonic_lt_times_l:
- ∀c:nat. O < c → monotonic nat lt (λt.(t*c)).
+theorem monotonic_lt_times_r:
+ ∀c:nat. O < c → monotonic nat lt (λt.(c*t)).
#c #posc #n #m #ltnm
(elim ltnm) normalize
[/2/
]
qed.
-theorem monotonic_lt_times_r:
- ∀c:nat. O < c → monotonic nat lt (λt.(c*t)).
-/2/ qed.
+theorem monotonic_lt_times_l:
+ ∀c:nat. O < c → monotonic nat lt (λt.(t*c)).
+/2/
+qed.
theorem lt_to_le_to_lt_times:
∀n,m,p,q:nat. n < m → p ≤ q → O < q → n*p < m*q.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| A.Asperti, C.Sacerdoti Coen, *)
+(* ||A|| E.Tassi, S.Zacchiroli *)
+(* \ / *)
+(* \ / Matita is distributed under the terms of the *)
+(* v GNU Lesser General Public License Version 2.1 *)
+(* *)
+(**************************************************************************)
+
+include "nat/primes.ma".
+include "nat/lt_arith.ma".
+
+(* upper bound by Bertrand's conjecture. *)
+(* Too difficult to prove.
+let rec nth_prime n \def
+match n with
+ [ O \Rightarrow (S(S O))
+ | (S p) \Rightarrow
+ let previous_prime \def S (nth_prime p) in
+ min_aux previous_prime ((S(S O))*previous_prime) primeb].
+
+theorem example8 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
+normalize.reflexivity.
+qed.
+
+theorem example9 : nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))).
+normalize.reflexivity.
+qed.
+
+theorem example10 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
+normalize.reflexivity.
+qed. *)
+
+theorem smallest_factor_fact: \forall n:nat.
+n < smallest_factor (S n!).
+intros.
+apply not_le_to_lt.unfold Not.
+intro.
+apply (not_divides_S_fact n (smallest_factor(S n!))).
+apply lt_SO_smallest_factor.
+unfold lt.apply le_S_S.apply le_SO_fact.
+assumption.
+apply divides_smallest_factor_n.
+unfold lt.apply le_S_S.apply le_O_n.
+qed.
+
+theorem ex_prime: \forall n. (S O) \le n \to \exists m.
+n < m \land m \le S n! \land (prime m).
+intros.
+elim H.
+apply (ex_intro nat ? (S(S O))).
+split.split.apply (le_n (S(S O))).
+apply (le_n (S(S O))).apply (primeb_to_Prop (S(S O))).
+apply (ex_intro nat ? (smallest_factor (S (S n1)!))).
+split.split.
+apply smallest_factor_fact.
+apply le_smallest_factor_n.
+(* Andrea: ancora hint non lo trova *)
+apply prime_smallest_factor_n.unfold lt.
+apply le_S.apply le_SSO_fact.
+unfold lt.apply le_S_S.assumption.
+qed.
+
+let rec nth_prime n \def
+match n with
+ [ O \Rightarrow (S(S O))
+ | (S p) \Rightarrow
+ let previous_prime \def (nth_prime p) in
+ let upper_bound \def S previous_prime! in
+ min_aux upper_bound (S previous_prime) primeb].
+
+(* it works
+theorem example11 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
+normalize.reflexivity.
+qed.
+
+theorem example12: nth_prime (S(S(S O))) = (S(S(S(S(S(S(S O))))))).
+normalize.reflexivity.
+qed.
+
+theorem example13 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
+normalize.reflexivity.
+qed.
+
+alias num (instance 0) = "natural number".
+theorem example14 : nth_prime 18 = 67.
+normalize.reflexivity.
+qed.
+*)
+
+theorem prime_nth_prime : \forall n:nat.prime (nth_prime n).
+intro.
+apply (nat_case n).simplify.
+apply (primeb_to_Prop (S(S O))).
+intro.
+change with
+(let previous_prime \def (nth_prime m) in
+let upper_bound \def S previous_prime! in
+prime (min_aux upper_bound (S previous_prime) primeb)).
+apply primeb_true_to_prime.
+apply f_min_aux_true.
+apply (ex_intro nat ? (smallest_factor (S (nth_prime m)!))).
+split.split.
+apply smallest_factor_fact.
+apply transitive_le;
+ [2: apply le_smallest_factor_n
+ | skip
+ | apply (le_plus_n_r (S (nth_prime m)) (S (fact (nth_prime m))))
+ ].
+apply prime_to_primeb_true.
+apply prime_smallest_factor_n.unfold lt.
+apply le_S_S.apply le_SO_fact.
+qed.
+
+(* properties of nth_prime *)
+theorem increasing_nth_prime: increasing nth_prime.
+unfold increasing.
+intros.
+change with
+(let previous_prime \def (nth_prime n) in
+let upper_bound \def S previous_prime! in
+(S previous_prime) \le min_aux upper_bound (S previous_prime) primeb).
+intros.
+apply le_min_aux.
+qed.
+
+variant lt_nth_prime_n_nth_prime_Sn :\forall n:nat.
+(nth_prime n) < (nth_prime (S n)) \def increasing_nth_prime.
+
+theorem injective_nth_prime: injective nat nat nth_prime.
+apply increasing_to_injective.
+apply increasing_nth_prime.
+qed.
+
+theorem lt_SO_nth_prime_n : \forall n:nat. (S O) \lt nth_prime n.
+intros. elim n.unfold lt.apply le_n.
+apply (trans_lt ? (nth_prime n1)).
+assumption.apply lt_nth_prime_n_nth_prime_Sn.
+qed.
+
+theorem lt_O_nth_prime_n : \forall n:nat. O \lt nth_prime n.
+intros.apply (trans_lt O (S O)).
+unfold lt. apply le_n.apply lt_SO_nth_prime_n.
+qed.
+
+theorem lt_n_nth_prime_n : \forall n:nat. n \lt nth_prime n.
+intro.
+elim n
+ [apply lt_O_nth_prime_n
+ |apply (lt_to_le_to_lt ? (S (nth_prime n1)))
+ [unfold.apply le_S_S.assumption
+ |apply lt_nth_prime_n_nth_prime_Sn
+ ]
+ ]
+qed.
+
+theorem ex_m_le_n_nth_prime_m:
+\forall n: nat. nth_prime O \le n \to
+\exists m. nth_prime m \le n \land n < nth_prime (S m).
+intros.
+apply increasing_to_le2.
+exact lt_nth_prime_n_nth_prime_Sn.assumption.
+qed.
+
+theorem lt_nth_prime_to_not_prime: \forall n,m. nth_prime n < m \to m < nth_prime (S n)
+\to \lnot (prime m).
+intros.
+apply primeb_false_to_not_prime.
+letin previous_prime \def (nth_prime n).
+letin upper_bound \def (S previous_prime!).
+apply (lt_min_aux_to_false primeb (S previous_prime) upper_bound m).
+assumption.
+unfold lt.
+apply (transitive_le (S m) (nth_prime (S n)) (min_aux (S (fact (nth_prime n))) (S (nth_prime n)) primeb) ? ?);
+ [apply (H1).
+ |apply (le_n (min_aux (S (fact (nth_prime n))) (S (nth_prime n)) primeb)).
+ ]
+qed.
+
+(* nth_prime enumerates all primes *)
+theorem prime_to_nth_prime : \forall p:nat. prime p \to
+\exists i. nth_prime i = p.
+intros.
+cut (\exists m. nth_prime m \le p \land p < nth_prime (S m)).
+elim Hcut.elim H1.
+cut (nth_prime a < p \lor nth_prime a = p).
+elim Hcut1.
+absurd (prime p).
+assumption.
+apply (lt_nth_prime_to_not_prime a).assumption.assumption.
+apply (ex_intro nat ? a).assumption.
+apply le_to_or_lt_eq.assumption.
+apply ex_m_le_n_nth_prime_m.
+simplify.unfold prime in H.elim H.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/factorial.ma".
+include "arithmetics/minimization.ma".
+
+inductive divides (n,m:nat) : Prop ≝
+quotient: ∀q:nat.m = times n q → divides n m.
+
+interpretation "divides" 'divides n m = (divides n m).
+interpretation "not divides" 'ndivides n m = (Not (divides n m)).
+
+theorem reflexive_divides : reflexive nat divides.
+/2/ qed.
+
+theorem divides_to_div_mod_spec :
+∀n,m. O < n → n ∣ m → div_mod_spec m n (m / n) O.
+#n #m #posn * #q #eqm % // >eqm
+>commutative_times >div_times //
+qed.
+
+theorem div_mod_spec_to_divides :
+∀n,m,q. div_mod_spec m n q O → n ∣ m.
+#n #m #q * #posn #eqm /2/
+qed.
+
+theorem divides_to_mod_O:
+∀n,m. O < n → n ∣ m → (m \mod n) = O.
+#n #m #posn #divnm
+@(div_mod_spec_to_eq2 m n (m / n) (m \mod n) (m / n) O) /2/
+qed.
+
+theorem mod_O_to_divides:
+∀n,m. O < n → (m \mod n) = O → n ∣ m.
+/2/ qed.
+
+theorem divides_n_O: ∀n:nat. n ∣ O.
+/2/ qed.
+
+theorem divides_n_n: ∀n:nat. n ∣ n.
+/2/ qed.
+
+theorem divides_SO_n: ∀n:nat. 1 ∣ n.
+/2/ qed.
+
+theorem divides_plus: ∀n,p,q:nat.
+n ∣ p → n ∣ q → n ∣ p+q.
+#n #p #q * #d1 #H * #d2 #H1 @(quotient ?? (d1+d2))
+>H >H1 //
+qed.
+
+theorem divides_minus: ∀n,p,q:nat.
+n ∣ p → n ∣ q → n ∣ (p-q).
+#n #p #q * #d1 #H * #d2 #H1 @(quotient ?? (d1-d2))
+>H >H1 //
+qed.
+
+theorem divides_times: ∀n,m,p,q:nat.
+n ∣ p → m ∣ q → n*m ∣ p*q.
+#n #m #p #q * #d1 #H * #d2 #H1 @(quotient ?? (d1*d2))
+>H >associative_times >associative_times @eq_f //
+qed.
+
+theorem transitive_divides: transitive ? divides.
+#a #b #c * #d1 #H * #d2 #H1 @(quotient ?? (d1*d2))
+>H1 >H //
+qed.
+
+theorem eq_mod_to_divides: ∀n,m,q. O < q →
+ mod n q = mod m q → q ∣ (n-m).
+#n #m #q #posq #eqmod @(leb_elim n m) #nm
+ [cut (n-m=O) /2/
+ |@(quotient ?? ((div n q)-(div m q)))
+ >distributive_times_minus >commutative_times
+ >(commutative_times q) cut((n/q)*q = n - (n \mod q)) [//] #H
+ >H >minus_minus >eqmod >commutative_plus
+ <div_mod //
+ ]
+qed.
+
+theorem divides_to_le : ∀n,m. O < m → n ∣ m → n ≤ m.
+#n #m #posm * #d (cases d)
+ [#eqm @False_ind /2/ |#p #eqm >eqm // ]
+qed.
+
+theorem antisymmetric_divides: ∀n,m. n ∣ m → m ∣ n → n = m.
+#n #m #divnm #divmn (cases (le_to_or_lt_eq … (le_O_n n))) #Hn
+ [(cases (le_to_or_lt_eq … (le_O_n m))) #Hm
+ [@le_to_le_to_eq @divides_to_le //
+ |<Hm (cases divmn) //
+ ]
+ |<Hn (cases divnm) //
+ ]
+qed.
+
+theorem divides_to_lt_O : ∀n,m. O < m → n ∣ m → O < n.
+#n #m #posm (cases (le_to_or_lt_eq … (le_O_n n))) //
+#eqn0 * #d <eqn0 #eqm @False_ind @(absurd …posm)
+@le_to_not_lt > eqm //
+qed.
+
+(*a variant of or_div_mod *)
+theorem or_div_mod1: ∀n,q. O < q →
+ q ∣ S n ∧ S n = S (n/q) * q ∨
+ q ∤ S n ∧ S n= (div n q) * q + S (n\mod q).
+#n #q #posq cases(or_div_mod n q posq) * #H1 #H2
+ [%1 % /2/
+ |%2 % // @(not_to_not ? ? (divides_to_mod_O … posq))
+ cut (S n \mod q = S(n \mod q))
+ [@(div_mod_spec_to_eq2 (S n) q (S n/q) (S n \mod q) (n/q) (S (n \mod q))) /2/]
+ #Hcut >Hcut % /2/
+ ]
+qed.
+
+theorem divides_to_div: ∀n,m.n ∣m → m/n*n = m.
+#n #m #divnm (cases (le_to_or_lt_eq O n (le_O_n n))) #H
+ [>(plus_n_O (m/n*n)) <(divides_to_mod_O ?? H divnm) //
+ |(cases divnm) #d <H //
+ ]
+qed.
+
+theorem divides_div: ∀d,n. d ∣ n → n/d ∣ n.
+#d #n #divdn @(quotient ?? d) @sym_eq /2/
+qed.
+
+theorem div_div: ∀n,d:nat. O < n → d ∣ n → n/(n/d) = d.
+#n #d #posn #divdn @(injective_times_l (n/d))
+ [@(lt_times_n_to_lt_l d) >divides_to_div //
+ |>divides_to_div
+ [>commutative_times >divides_to_div //
+ |@(quotient ? ? d) @sym_eq /2/
+ ]
+ ]
+qed.
+
+theorem times_div: ∀a,b,c:nat.
+ O < b → c ∣ b → a * (b /c) = (a*b)/c.
+#a #b #c #posb #divcb
+cut(O < c) [@(divides_to_lt_O … posb divcb)] #posc
+(cases divcb) #d #eqb >eqb
+>(commutative_times c d) >(div_times d c posc) <associative_times
+>(div_times (a * d) c posc) //
+qed.
+
+theorem plus_div: ∀n,m,d. O < d →
+ d ∣ n → d ∣ m → (n + m) / d = n/d + m/d.
+#n #m #d #posd #divdn #divdm
+(cases divdn) #a #eqn (cases divdm) #b #eqm
+>eqn >eqm <distributive_times_plus >commutative_times
+>div_times // >commutative_times >div_times //
+>commutative_times >div_times //
+qed.
+
+(* boolean divides *)
+definition dividesb : nat → nat → bool ≝
+λn,m :nat. (eqb (m \mod n) O).
+
+theorem dividesb_true_to_divides:
+∀n,m:nat. dividesb n m = true → n ∣ m.
+#n #m (cases (le_to_or_lt_eq … (le_O_n n)))
+ [#posn #divbnm @mod_O_to_divides // @eqb_true_to_eq @divbnm
+ |#eqnO <eqnO normalize #eqbmO >(eqb_true_to_eq … eqbmO) //
+ ]
+qed.
+
+theorem dividesb_false_to_not_divides:
+∀n,m:nat. dividesb n m = false → n ∤ m.
+#n #m (cases (le_to_or_lt_eq … (le_O_n n)))
+ [#posn #ndivbnm @(not_to_not ?? (divides_to_mod_O … posn))
+ @eqb_false_to_not_eq @ndivbnm
+ |#eqnO <eqnO normalize
+ @(nat_case m) [normalize /2/ |#a #_ #_ % * /2/]
+ ]
+qed.
+
+theorem decidable_divides: ∀n,m:nat. decidable (n ∣ m).
+#n #m cases(true_or_false (dividesb n m)) /3/
+qed.
+
+theorem divides_to_dividesb_true : ∀n,m:nat. O < n →
+ n ∣m → dividesb n m = true.
+#n #m #posn #divnm cases(true_or_false (dividesb n m)) //
+#ndivbnm @False_ind @(absurd … divnm) /2/
+qed.
+
+theorem divides_to_dividesb_true1 : ∀n,m:nat.O < m →
+ n ∣m → dividesb n m = true.
+#n #m #posn cases (le_to_or_lt_eq O n (le_O_n n)) /2/
+#eqn0 <eqn0 * #q #eqm @False_ind /2/
+qed.
+
+theorem not_divides_to_dividesb_false: ∀n,m:nat. O < n →
+ n ∤ m → dividesb n m = false.
+#n #m #posn cases(true_or_false (dividesb n m)) /2/
+#divbnm #ndivnm @False_ind @(absurd ?? ndivnm) /2/
+qed.
+
+theorem dividesb_div_true:
+∀d,n. O < n →
+ dividesb d n = true → dividesb (n/d) n = true.
+#d #n #posn #divbdn @divides_to_dividesb_true1 //
+@divides_div /2/
+qed.
+
+theorem dividesb_true_to_lt_O: ∀n,m.
+ O < n → m ∣ n → O < m.
+#n #m #posn * #d cases (le_to_or_lt_eq ? ? (le_O_n m)) //
+qed.
+
+(* divides and pi move away ??
+theorem divides_f_pi_f : ∀f:nat → nat.∀n,i:nat.
+ i < n → f i ∣ \big[times,0]_{x < n | true}(f x).
+#f #n #i (elim n)
+ [#ltiO @False_ind /2/
+ |#n #Hind #lti >bigop_Strue //
+ cases(le_to_or_lt_eq …(le_S_S_to_le … lti)) /3/
+ ]
+*)
+
+(* prime *)
+definition prime : nat → Prop ≝
+λn:nat. 1 < n ∧ (∀m:nat. m ∣ n → 1 < m → m = n).
+
+theorem not_prime_O: ¬ (prime O).
+% * #lt10 /2/
+qed.
+
+theorem not_prime_SO: ¬ (prime 1).
+% * #lt11 /2/
+qed.
+
+theorem prime_to_lt_O: ∀p. prime p → O < p.
+#p * #lt1p /2/
+qed.
+
+theorem prime_to_lt_SO: ∀p. prime p → 1 < p.
+#p * #lt1p /2/
+qed.
+
+(* smallest factor *)
+definition smallest_factor : nat → nat ≝
+λn:nat. if_then_else ? (leb n 1) n
+ (min n 2 (λm.(eqb (n \mod m) O))).
+
+theorem smallest_factor_to_min : ∀n. 1 < n →
+smallest_factor n = (min n 2 (λm.(eqb (n \mod m) O))).
+#n #lt1n normalize >lt_to_leb_false //
+qed.
+
+(* it works !
+theorem example1 : smallest_factor 3 = 3.
+normalize //
+qed.
+
+theorem example2: smallest_factor 4 = 2.
+normalize //
+qed.
+
+theorem example3 : smallest_factor 7 = 7.
+normalize //
+qed. *)
+
+theorem le_SO_smallest_factor: ∀n:nat.
+ n ≤ 1 → smallest_factor n = n.
+#n #le1n normalize >le_to_leb_true //
+qed.
+
+theorem lt_SO_smallest_factor: ∀n:nat.
+ 1 < n → 1 < smallest_factor n.
+#n #lt1n >smallest_factor_to_min //
+qed.
+
+theorem lt_O_smallest_factor: ∀n:nat.
+ O < n → O < (smallest_factor n).
+#n #posn (cases posn)
+ [>le_SO_smallest_factor //
+ |#m #posm @le_S_S_to_le @le_S @lt_SO_smallest_factor @le_S_S //
+ ]
+qed.
+
+theorem divides_smallest_factor_n : ∀n:nat. 0 < n →
+ smallest_factor n ∣ n.
+#n #posn (cases (le_to_or_lt_eq … posn))
+ [#lt1n @mod_O_to_divides [@lt_O_smallest_factor //]
+ >smallest_factor_to_min // @eqb_true_to_eq @f_min_true
+ @(ex_intro … n) % /2/ @eq_to_eqb_true /2/
+ |#H <H //
+ ]
+qed.
+
+theorem le_smallest_factor_n : ∀n.
+ smallest_factor n ≤ n.
+#n (cases n) // #m @divides_to_le /2/
+qed.
+
+theorem lt_smallest_factor_to_not_divides: ∀n,i:nat.
+1 < n → 1 < i → i < smallest_factor n → i ∤ n.
+#n #i #ltn #lti >smallest_factor_to_min // #ltmin
+@(not_to_not ? (n \mod i = 0))
+ [#divin @divides_to_mod_O /2/
+ |@eqb_false_to_not_eq @(lt_min_to_false … lti ltmin)
+ ]
+qed.
+
+theorem prime_smallest_factor_n : ∀n. 1 < n →
+ prime (smallest_factor n).
+#n #lt1n (cut (0<n)) [/2/] #posn % /2/ #m #divmmin #lt1m
+@le_to_le_to_eq
+ [@divides_to_le // @lt_O_smallest_factor //
+ |>smallest_factor_to_min // @true_to_le_min //
+ @eq_to_eqb_true @divides_to_mod_O /2/
+ @(transitive_divides … divmmin) @divides_smallest_factor_n //
+ ]
+qed.
+
+theorem prime_to_smallest_factor: ∀n. prime n →
+ smallest_factor n = n.
+#n * #lt1n #primen @primen
+ [@divides_smallest_factor_n /2/
+ |@lt_SO_smallest_factor //
+ ]
+qed.
+
+theorem smallest_factor_to_prime: ∀n. 1 < n →
+ smallest_factor n = n → prime n.
+#n #lt1n #H <H /2/
+qed.
+
+(* a number n > O is prime iff its smallest factor is n *)
+definition primeb ≝ λn:nat.
+ (leb 2 n) ∧ (eqb (smallest_factor n) n).
+
+(* it works! *)
+theorem example4 : primeb 3 = true.
+normalize // qed.
+
+theorem example5 : primeb 6 = false.
+normalize // qed.
+
+theorem example6 : primeb 11 = true.
+normalize // qed.
+
+theorem example7 : primeb 17 = true.
+normalize // qed.
+
+theorem primeb_true_to_prime : ∀n:nat.
+ primeb n = true → prime n.
+#n #primebn @smallest_factor_to_prime
+ [@leb_true_to_le @(andb_true_l … primebn)
+ |@eqb_true_to_eq @( andb_true_r … primebn)
+ ]
+qed.
+
+theorem primeb_false_to_not_prime : ∀n:nat.
+ primeb n = false → ¬ (prime n).
+#n #H cut ((leb 2 n ∧ (eqb (smallest_factor n) n)) = false) [>H //]
+@leb_elim
+ [#_ #H1 @(not_to_not … (prime_to_smallest_factor … ))
+ @eqb_false_to_not_eq @H1
+ |#len1 #_ @(not_to_not … len1) * //
+ ]
+qed.
+
+theorem decidable_prime : ∀n:nat.decidable (prime n).
+#n cases(true_or_false (primeb n)) #H
+ [%1 /2/ |%2 /2/]
+qed.
+
+theorem prime_to_primeb_true: ∀n:nat.
+ prime n → primeb n = true.
+#n #primen (cases (true_or_false (primeb n))) //
+#H @False_ind @(absurd … primen) /2/
+qed.
+
+theorem not_prime_to_primeb_false: ∀n:nat.
+ ¬(prime n) → primeb n = false.
+#n #np (cases (true_or_false (primeb n))) //
+#p @False_ind @(absurd (prime n) (primeb_true_to_prime …) np) //
+qed.
+
+(* enumeration of all primes *)
+
+theorem divides_fact : ∀n,i:nat. O < i →
+ i ≤ n → i ∣ n!.
+#n #i #ltOi (elim n)
+ [#leiO @False_ind @(absurd … ltOi) /2/
+ |#n #Hind #lei normalize cases(le_to_or_lt_eq … lei)
+ [#ltiS @(transitive_divides ? n!) [@Hind /2/ | /2/]
+ |#eqi >eqi /2/
+ ]
+ ]
+qed.
+
+theorem mod_S_fact: ∀n,i:nat.
+ 1 < i → i ≤ n → (S n!) \mod i = 1.
+#n #i #lt1i #lein
+cut(O<i) [/2/] #posi
+cut (n! \mod i = O) [@divides_to_mod_O // @divides_fact //] #Hcut
+<Hcut @mod_S //
+qed.
+
+theorem not_divides_S_fact: ∀n,i:nat.
+ 1 < i → i ≤ n → i ∤ S n!.
+#n #i #lt1i #lein @(not_to_not … (divides_to_mod_O i (S n!) ?)) /2/
+>mod_S_fact // @eqb_false_to_not_eq //
+qed.
+
+theorem smallest_factor_fact: ∀n:nat.
+ n < smallest_factor (S n!).
+#n @not_le_to_lt @(not_to_not ? ((smallest_factor (S n!)) ∤ (S n!)))
+ [@not_divides_S_fact @lt_SO_smallest_factor @le_S_S //
+ |% * #H @H @divides_smallest_factor_n @le_S_S //
+ ]
+qed.
+
+theorem ex_prime: ∀n. 1 ≤ n →∃m.
+ n < m ∧ m ≤ S n! ∧ (prime m).
+#n #lein (cases lein)
+ [@(ex_intro nat ? 2) % [/2/|@primeb_true_to_prime //]
+ |#m #leim @(ex_intro nat ? (smallest_factor (S (S m)!)))
+ % [% [@smallest_factor_fact |@le_smallest_factor_n ]
+ |@prime_smallest_factor_n @le_S_S //
+ ]
+ ]
+qed.
+
+let rec nth_prime n ≝ match n with
+ [ O ⇒ 2
+ | S p ⇒
+ let previous_prime ≝ nth_prime p in
+ let upper_bound ≝ S previous_prime! in
+ min upper_bound (S previous_prime) primeb].
+
+lemma nth_primeS: ∀n.nth_prime (S n) =
+ let previous_prime ≝ nth_prime n in
+ let upper_bound ≝ S previous_prime! in
+ min upper_bound (S previous_prime) primeb.
+// qed.
+
+(* it works *)
+theorem example11 : nth_prime 2 = 5.
+normalize // qed.
+
+theorem example12: nth_prime 3 = 7.
+normalize //
+qed.
+
+theorem example13 : nth_prime 4 = 11.
+normalize // qed.
+
+(* done in 13.1369330883s -- qualcosa non va: // lentissimo
+theorem example14 : nth_prime 18 = 67.
+normalize // (* @refl *)
+qed.
+*)
+
+theorem prime_nth_prime : ∀n:nat.prime (nth_prime n).
+#n (cases n)
+ [@primeb_true_to_prime //
+ |#m >nth_primeS @primeb_true_to_prime @f_min_true
+ @(ex_intro nat ? (smallest_factor (S (nth_prime m)!)))
+ % [% // @le_S_S @(transitive_le … (le_smallest_factor_n …))
+ <plus_n_Sm @le_plus_n_r
+ ]
+ @prime_to_primeb_true @prime_smallest_factor_n @le_S_S //
+ ]
+qed.
+
+(* properties of nth_prime *)
+theorem increasing_nth_prime: ∀n. nth_prime n < nth_prime (S n).
+#n
+change with
+(let previous_prime ≝ (nth_prime n) in
+ let upper_bound ≝ S previous_prime! in
+ S previous_prime ≤ min upper_bound (S previous_prime) primeb)
+apply le_min_l
+qed.
+
+theorem lt_SO_nth_prime_n : ∀n:nat. 1 < nth_prime n.
+#n @prime_to_lt_SO //
+qed.
+
+theorem lt_O_nth_prime_n : ∀n:nat. O < nth_prime n.
+#n @prime_to_lt_O //
+qed.
+
+theorem lt_n_nth_prime_n : ∀n:nat. n < nth_prime n.
+#n (elim n)
+ [@lt_O_nth_prime_n
+ |#m #ltm @(le_to_lt_to_lt … ltm) //
+ ]
+qed.
+
+(*
+theorem ex_m_le_n_nth_prime_m:
+∀n.nth_prime O ≤ n →
+∃m. nth_prime m ≤ n ∧ n < nth_prime (S m).
+intros.
+apply increasing_to_le2.
+exact lt_nth_prime_n_nth_prime_Sn.assumption.
+qed. *)
+
+theorem lt_nth_prime_to_not_prime: ∀n,m.
+ nth_prime n < m → m < nth_prime (S n) → ¬ (prime m).
+#n #m #ltml >nth_primeS #ltmr @primeb_false_to_not_prime
+@(lt_min_to_false ? (S (nth_prime n)!) m (S (nth_prime n))) //
+qed.
+
+(* nth_prime enumerates all primes *)
+theorem prime_to_nth_prime : ∀p:nat.
+ prime p → ∃i.nth_prime i = p.
+#p #primep
+cut (∃m. nth_prime m ≤ p ∧ p < nth_prime (S m))
+ [@(increasing_to_le2 nth_prime ?) // @prime_to_lt_SO //
+ |* #n * #lepl #ltpr cases(le_to_or_lt_eq … lepl)
+ [#ltpl @False_ind @(absurd … primep)
+ @(lt_nth_prime_to_not_prime n p ltpl ltpr)
+ |#eqp @(ex_intro … n) //
+ ]
+ ]
+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 "basics/relations.ma".
+
+(********** bool **********)
+inductive bool: Type[0] ≝
+ | true : bool
+ | false : bool.
+
+(* destruct does not work *)
+theorem not_eq_true_false : true ≠ false.
+@nmk #Heq change with match true with [true ⇒ False|false ⇒ True]
+>Heq // qed.
+
+definition notb : bool → bool ≝
+λ b:bool. match b with [true ⇒ false|false ⇒ true ].
+
+interpretation "boolean not" 'not x = (notb x).
+
+theorem notb_elim: ∀ b:bool.∀ P:bool → Prop.
+match b with
+[ true ⇒ P false
+| false ⇒ P true] → P (notb b).
+#b #P elim b normalize // qed.
+
+theorem notb_notb: ∀b:bool. notb (notb b) = b.
+#b elim b // qed.
+
+theorem injective_notb: injective bool bool notb.
+#b1 #b2 #H // qed.
+
+definition andb : bool → bool → bool ≝
+λb1,b2:bool. match b1 with [ true ⇒ b2 | false ⇒ false ].
+
+interpretation "boolean and" 'and x y = (andb x y).
+
+theorem andb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop.
+match b1 with [ true ⇒ P b2 | false ⇒ P false] → P (b1 ∧ b2).
+#b1 #b2 #P (elim b1) normalize // qed.
+
+theorem andb_true_l: ∀ b1,b2. (b1 ∧ b2) = true → b1 = true.
+#b1 (cases b1) normalize // qed.
+
+theorem andb_true_r: ∀b1,b2. (b1 ∧ b2) = true → b2 = true.
+#b1 #b2 (cases b1) normalize // (cases b2) // qed.
+
+definition orb : bool → bool → bool ≝
+λb1,b2:bool.match b1 with [ true ⇒ true | false ⇒ b2].
+
+interpretation "boolean or" 'or x y = (orb x y).
+
+theorem orb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop.
+match b1 with [ true ⇒ P true | false ⇒ P b2] → P (orb b1 b2).
+#b1 #b2 #P (elim b1) normalize // qed.
+
+definition if_then_else: ∀A:Type[0]. bool → A → A → A ≝
+λA.λb.λ P,Q:A. match b with [ true ⇒ P | false ⇒ Q].
+
+theorem bool_to_decidable_eq:
+ ∀b1,b2:bool. decidable (b1=b2).
+#b1 #b2 (cases b1) (cases b2) /2/ %2 /3/ qed.
+
+theorem true_or_false:
+∀b:bool. b = true ∨ b = false.
+#b (cases b) /2/ qed.
+
+
--- /dev/null
+(* exists *******************************************************************)
+
+notation "hvbox(∃ _ break . p)"
+ with precedence 20
+for @{'exists $p }.
+
+notation < "hvbox(\exists ident i : ty break . p)"
+ right associative with precedence 20
+for @{'exists (\lambda ${ident i} : $ty. $p) }.
+
+notation < "hvbox(\exists ident i break . p)"
+ with precedence 20
+for @{'exists (\lambda ${ident i}. $p) }.
+
+(*
+notation < "hvbox(\exists ident i opt (: ty) break . p)"
+ right associative with precedence 20
+for @{ 'exists ${default
+ @{\lambda ${ident i} : $ty. $p}
+ @{\lambda ${ident i} . $p}}}.
+*)
+
+notation > "\exists list1 ident x sep , opt (: T). term 19 Px"
+ with precedence 20
+ for ${ default
+ @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}:$T.$acc)} } }
+ @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } }
+ }.
+
+(* sigma ********************************************************************)
+
+notation < "hvbox(\Sigma ident i : ty break . p)"
+ left associative with precedence 20
+for @{'sigma (\lambda ${ident i} : $ty. $p) }.
+
+notation < "hvbox(\Sigma ident i break . p)"
+ with precedence 20
+for @{'sigma (\lambda ${ident i}. $p) }.
+
+(*
+notation < "hvbox(\Sigma ident i opt (: ty) break . p)"
+ right associative with precedence 20
+for @{ 'sigma ${default
+ @{\lambda ${ident i} : $ty. $p}
+ @{\lambda ${ident i} . $p}}}.
+*)
+
+notation > "\Sigma list1 ident x sep , opt (: T). term 19 Px"
+ with precedence 20
+ for ${ default
+ @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}:$T.$acc)} } }
+ @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}.$acc)} } }
+ }.
+
+(* equality, conguence ******************************************************)
+
+notation > "hvbox(a break = b)"
+ non associative with precedence 45
+for @{ 'eq ? $a $b }.
+
+notation < "hvbox(term 46 a break maction (=) (=\sub t) term 46 b)"
+ non associative with precedence 45
+for @{ 'eq $t $a $b }.
+
+notation > "hvbox(n break (≅ \sub term 90 p) m)"
+ non associative with precedence 45
+for @{ 'congruent $n $m $p }.
+
+notation < "hvbox(term 46 n break ≅ \sub p term 46 m)"
+ non associative with precedence 45
+for @{ 'congruent $n $m $p }.
+
+(* other notations **********************************************************)
+
+notation "hvbox(\langle term 19 a, break term 19 b\rangle)"
+with precedence 90 for @{ 'pair $a $b}.
+
+notation "hvbox(x break \times y)" with precedence 70
+for @{ 'product $x $y}.
+
+notation < "\fst \nbsp term 90 x" with precedence 69 for @{'pi1a $x}.
+notation < "\snd \nbsp term 90 x" with precedence 69 for @{'pi2a $x}.
+
+notation < "\fst \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi1b $x $y}.
+notation < "\snd \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi2b $x $y}.
+
+notation > "\fst" with precedence 90 for @{'pi1}.
+notation > "\snd" with precedence 90 for @{'pi2}.
+
+notation "hvbox(a break \to b)"
+ right associative with precedence 20
+for @{ \forall $_:$a.$b }.
+
+notation < "hvbox(a break \to b)"
+ right associative with precedence 20
+for @{ \Pi $_:$a.$b }.
+
+notation "hvbox(a break \leq b)"
+ non associative with precedence 45
+for @{ 'leq $a $b }.
+
+notation "hvbox(a break \geq b)"
+ non associative with precedence 45
+for @{ 'geq $a $b }.
+
+notation "hvbox(a break \lt b)"
+ non associative with precedence 45
+for @{ 'lt $a $b }.
+
+notation "hvbox(a break \gt b)"
+ non associative with precedence 45
+for @{ 'gt $a $b }.
+
+notation > "hvbox(a break \neq b)"
+ non associative with precedence 45
+for @{ 'neq ? $a $b }.
+
+notation < "hvbox(a break maction (\neq) (\neq\sub t) b)"
+ non associative with precedence 45
+for @{ 'neq $t $a $b }.
+
+notation "hvbox(a break \nleq b)"
+ non associative with precedence 45
+for @{ 'nleq $a $b }.
+
+notation "hvbox(a break \ngeq b)"
+ non associative with precedence 45
+for @{ 'ngeq $a $b }.
+
+notation "hvbox(a break \nless b)"
+ non associative with precedence 45
+for @{ 'nless $a $b }.
+
+notation "hvbox(a break \ngtr b)"
+ non associative with precedence 45
+for @{ 'ngtr $a $b }.
+
+notation "hvbox(a break \divides b)"
+ non associative with precedence 45
+for @{ 'divides $a $b }.
+
+notation "hvbox(a break \ndivides b)"
+ non associative with precedence 45
+for @{ 'ndivides $a $b }.
+
+notation "hvbox(a break + b)"
+ left associative with precedence 50
+for @{ 'plus $a $b }.
+
+notation "hvbox(a break - b)"
+ left associative with precedence 50
+for @{ 'minus $a $b }.
+
+notation "hvbox(a break * b)"
+ left associative with precedence 55
+for @{ 'times $a $b }.
+
+notation "hvbox(a break \middot b)"
+ left associative with precedence 55
+ for @{ 'middot $a $b }.
+
+notation "hvbox(a break \mod b)"
+ left associative with precedence 55
+for @{ 'module $a $b }.
+
+notation < "a \frac b"
+ non associative with precedence 90
+for @{ 'divide $a $b }.
+
+notation "a \over b"
+ left associative with precedence 55
+for @{ 'divide $a $b }.
+
+notation "hvbox(a break / b)"
+ left associative with precedence 55
+for @{ 'divide $a $b }.
+
+notation "- term 60 a" with precedence 60
+for @{ 'uminus $a }.
+
+notation "a !"
+ non associative with precedence 80
+for @{ 'fact $a }.
+
+notation "\sqrt a"
+ non associative with precedence 60
+for @{ 'sqrt $a }.
+
+notation "hvbox(a break \lor b)"
+ left associative with precedence 30
+for @{ 'or $a $b }.
+
+notation "hvbox(a break \land b)"
+ left associative with precedence 35
+for @{ 'and $a $b }.
+
+notation "hvbox(\lnot a)"
+ non associative with precedence 40
+for @{ 'not $a }.
+
+notation > "hvbox(a break \liff b)"
+ left associative with precedence 25
+for @{ 'iff $a $b }.
+
+notation "hvbox(a break \leftrightarrow b)"
+ left associative with precedence 25
+for @{ 'iff $a $b }.
+
+
+notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 90
+for @{ 'powerset $A }.
+notation > "hvbox(\Omega ^ term 90 A)" non associative with precedence 90
+for @{ 'powerset $A }.
+
+notation < "hvbox({ ident i | term 19 p })" with precedence 90
+for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
+
+notation > "hvbox({ ident i | term 19 p })" with precedence 90
+for @{ 'subset (\lambda ${ident i}. $p)}.
+
+notation < "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
+for @{ 'comprehension $s (\lambda ${ident i} : $nonexistent . $p)}.
+
+notation > "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
+for @{ 'comprehension $s (\lambda ${ident i}. $p)}.
+
+notation "hvbox(a break ∈ b)" non associative with precedence 45
+for @{ 'mem $a $b }.
+
+notation "hvbox(a break ≬ b)" non associative with precedence 45
+for @{ 'overlaps $a $b }. (* \between *)
+
+notation "hvbox(a break ⊆ b)" non associative with precedence 45
+for @{ 'subseteq $a $b }. (* \subseteq *)
+
+notation "hvbox(a break ∩ b)" left associative with precedence 55
+for @{ 'intersects $a $b }. (* \cap *)
+
+notation "hvbox(a break ∪ b)" left associative with precedence 50
+for @{ 'union $a $b }. (* \cup *)
+
+notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
+
+notation "hvbox(a break \approx b)" non associative with precedence 45
+ for @{ 'napart $a $b}.
+
+notation "hvbox(a break # b)" non associative with precedence 45
+ for @{ 'apart $a $b}.
+
+notation "hvbox(a break \circ b)"
+ left associative with precedence 55
+for @{ 'compose $a $b }.
+
+notation < "↓ \ensp a" with precedence 55 for @{ 'downarrow $a }.
+notation > "↓ a" with precedence 55 for @{ 'downarrow $a }.
+
+notation "hvbox(U break ↓ V)" non associative with precedence 55 for @{ 'fintersects $U $V }.
+
+notation "↑a" with precedence 55 for @{ 'uparrow $a }.
+
+notation "hvbox(a break ↑ b)" with precedence 55 for @{ 'funion $a $b }.
+
+notation < "term 76 a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
+notation > "a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
+notation > "a ^ term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
+notation "s \sup (-1)" non associative with precedence 75 for @{ 'invert $s }.
+notation > "s ^ (-1)" non associative with precedence 75 for @{ 'invert $s }.
+notation < "s \sup (-1) x" non associative with precedence 90 for @{ 'invert_appl $s $x}.
+
+notation "| term 19 C |" with precedence 70 for @{ 'card $C }.
+
+notation "\naturals" non associative with precedence 90 for @{'N}.
+notation "\rationals" non associative with precedence 90 for @{'Q}.
+notation "\reals" non associative with precedence 90 for @{'R}.
+notation "\integers" non associative with precedence 90 for @{'Z}.
+notation "\complexes" non associative with precedence 90 for @{'C}.
+
+notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *)
+
+notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}.
+notation > "x ⊩⎽ term 90 c y" with precedence 45 for @{'Vdash2 $x $y $c}.
+notation "x (⊩ \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}.
+notation > "⊩ " with precedence 60 for @{'Vdash ?}.
+notation "(⊩ \sub term 90 c) " with precedence 60 for @{'Vdash $c}.
+
+notation < "maction (mstyle color #ff0000 (…)) (t)"
+non associative with precedence 90 for @{'hide $t}.
\ No newline at end of file
--- /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 "basics/logic.ma".
+
+inductive Sigma: Type[1] ≝
+ mk_Sigma: ∀p1: Type[0]. p1 → Sigma.
+
+definition p1: Sigma → Type[0].
+ #S cases S #Y #_ @Y
+qed.
+
+definition p2: ∀S:Sigma. p1 S.
+ #S cases S #Y #x @x
+qed.
+
+inductive jmeq (A:Type[0]) (x:A) : ∀B:Type[0]. B →Prop ≝
+jmrefl : jmeq A x A x.
+
+definition eqProp ≝ λA:Prop.eq A.
+
+lemma K : ∀A.∀x:A.∀h:x=x. eqProp ? h (refl A x).
+#A #x #h @(refl ? h: eqProp ? ? ?).
+qed.
+
+definition cast:
+ ∀A,B:Type[0].∀E:A=B. A → B.
+ #A #B #E cases E #X @X
+qed.
+
+lemma tech1:
+ ∀Aa,Bb:Sigma.∀E:Aa=Bb.
+ cast (p1 Aa) (p1 Bb) ? (p2 Aa) = p2 Bb.
+ [2: >E %
+ | #Aa #Bb #E >E cases Bb #B #b normalize % ]
+qed.
+
+lemma gral: ∀A.∀x,y:A.
+ mk_Sigma A x = mk_Sigma A y → x=y.
+ #A #x #y #E lapply (tech1 ?? E)
+ generalize in ⊢ (??(???%?)? → ?) #E1
+ normalize in E1; >(K ?? E1) normalize
+ #H @H
+qed.
+
+axiom daemon: False.
+
+lemma jm_to_eq_sigma:
+ ∀A,x,y. jmeq A x A y → mk_Sigma A x = mk_Sigma A y.
+ #A #x #y #E cases E in ⊢ (???%); %
+qed.
+
+definition curry:
+ ∀A,x.
+ (∀y. jmeq A x A y → Type[0]) →
+ (∀y. mk_Sigma A x = mk_Sigma A y → Type[0]).
+ #A #x #f #y #E @(f y) >(gral ??? E) %
+qed.
+
+lemma G : ∀A.∀x:A.∀P:∀y:A.mk_Sigma A x = mk_Sigma A y →Type[0].
+ P x (refl ? (mk_Sigma A x)) → ∀y.∀h:mk_Sigma A x = mk_Sigma A y.
+ P y h.
+ #A #x #P #H #y #E lapply (gral ??? E) #G generalize in match E;
+ @(match G
+ return λy.λ_. ∀e:mk_Sigma A x = mk_Sigma A y. P y e
+ with
+ [refl ⇒ ?])
+ #E <(sym_eq ??? (K ?? E)) @H
+qed.
+
+definition PP: ∀A:Prop.∀P:A → Type[0]. A → Type[0].
+ #A #P #a @(P a)
+qed.
+
+lemma E : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0].
+ PP ? (P x) (jmrefl A x) → ∀y.∀h:jmeq A x A y.PP ? (P y) h.
+ #A #a #P #H #b #E letin F ≝ (jm_to_eq_sigma ??? E)
+ lapply (G ?? (curry ?? P) ?? F)
+ [ normalize //
+ | #H whd in H; @(H : PP ? (P b) ?) ]
+qed.
+
+lemma jmeq_elim : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0].
+ P x (jmrefl A x) → ∀y.∀h:jmeq A x A y.P y h ≝ E.
--- /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 "basics/types.ma".
+include "basics/bool.ma".
+
+inductive list (A:Type[0]) : Type[0] :=
+ | nil: list A
+ | cons: A -> list A -> list A.
+
+notation "hvbox(hd break :: tl)"
+ right associative with precedence 47
+ for @{'cons $hd $tl}.
+
+notation "[ list0 x sep ; ]"
+ non associative with precedence 90
+ for ${fold right @'nil rec acc @{'cons $x $acc}}.
+
+notation "hvbox(l1 break @ l2)"
+ right associative with precedence 47
+ for @{'append $l1 $l2 }.
+
+interpretation "nil" 'nil = (nil ?).
+interpretation "cons" 'cons hd tl = (cons ? hd tl).
+
+definition not_nil: ∀A:Type[0].list A → Prop ≝
+ λA.λl.match l with [ nil ⇒ True | cons hd tl ⇒ False ].
+
+theorem nil_cons:
+ ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
+ #A #l #a @nmk #Heq (change with (not_nil ? (a::l))) >Heq //
+qed.
+
+(*
+let rec id_list A (l: list A) on l :=
+ match l with
+ [ nil => []
+ | (cons hd tl) => hd :: id_list A tl ]. *)
+
+let rec append A (l1: list A) l2 on l1 ≝
+ match l1 with
+ [ nil ⇒ l2
+ | cons hd tl ⇒ hd :: append A tl l2 ].
+
+definition hd ≝ λA.λl: list A.λd:A.
+ match l with [ nil ⇒ d | cons a _ ⇒ a].
+
+definition tail ≝ λA.λl: list A.
+ match l with [ nil ⇒ [] | cons hd tl ⇒ tl].
+
+interpretation "append" 'append l1 l2 = (append ? l1 l2).
+
+theorem append_nil: ∀A.∀l:list A.l @ [] = l.
+#A #l (elim l) normalize // qed.
+
+theorem associative_append:
+ ∀A.associative (list A) (append A).
+#A #l1 #l2 #l3 (elim l1) normalize // qed.
+
+(* deleterio per auto
+ntheorem cons_append_commute:
+ ∀A:Type.∀l1,l2:list A.∀a:A.
+ a :: (l1 @ l2) = (a :: l1) @ l2.
+//; nqed. *)
+
+theorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
+/2/ qed.
+
+theorem nil_append_elim: ∀A.∀l1,l2: list A.∀P:?→?→Prop.
+ l1@l2=[] → P (nil A) (nil A) → P l1 l2.
+#A #l1 #l2 #P (cases l1) normalize //
+#a #l3 #heq destruct
+qed.
+
+theorem nil_to_nil: ∀A.∀l1,l2:list A.
+ l1@l2 = [] → l1 = [] ∧ l2 = [].
+#A #l1 #l2 #isnil @(nil_append_elim A l1 l2) /2/
+qed.
+
+(* iterators *)
+
+let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝
+ match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)].
+
+let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝
+ match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
+
+definition filter ≝
+ λT.λp:T → bool.
+ foldr T (list T) (λx,l0.if_then_else ? (p x) (x::l0) l0) (nil T).
+
+lemma filter_true : ∀A,l,a,p. p a = true →
+ filter A p (a::l) = a :: filter A p l.
+#A #l #a #p #pa (elim l) normalize >pa normalize // qed.
+
+lemma filter_false : ∀A,l,a,p. p a = false →
+ filter A p (a::l) = filter A p l.
+#A #l #a #p #pa (elim l) normalize >pa normalize // qed.
+
+theorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
+#A #B #f #g #l #eqfg (elim l) normalize // qed.
+
+let rec dprodl (A:Type[0]) (f:A→Type[0]) (l1:list A) (g:(∀a:A.list (f a))) on l1 ≝
+match l1 with
+ [ nil ⇒ nil ?
+ | cons a tl ⇒ (map ??(dp ?? a) (g a)) @ dprodl A f tl g
+ ].
+
+(**************************** fold *******************************)
+
+let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→bool) (f:A→B) (l:list A) on l :B ≝
+ match l with
+ [ nil ⇒ b
+ | cons a l ⇒ if_then_else ? (p a) (op (f a) (fold A B op b p f l))
+ (fold A B op b p f l)].
+
+notation "\fold [ op , nil ]_{ ident i ∈ l | p} f"
+ with precedence 80
+for @{'fold $op $nil (λ${ident i}. $p) (λ${ident i}. $f) $l}.
+
+notation "\fold [ op , nil ]_{ident i ∈ l } f"
+ with precedence 80
+for @{'fold $op $nil (λ${ident i}.true) (λ${ident i}. $f) $l}.
+
+interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l).
+
+theorem fold_true:
+∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a = true →
+ \fold[op,nil]_{i ∈ a::l| p i} (f i) =
+ op (f a) \fold[op,nil]_{i ∈ l| p i} (f i).
+#A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
+
+theorem fold_false:
+∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f.
+p a = false → \fold[op,nil]_{i ∈ a::l| p i} (f i) =
+ \fold[op,nil]_{i ∈ l| p i} (f i).
+#A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
+
+theorem fold_filter:
+∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B.
+ \fold[op,nil]_{i ∈ l| p i} (f i) =
+ \fold[op,nil]_{i ∈ (filter A p l)} (f i).
+#A #B #a #l #p #op #nil #f elim l //
+#a #tl #Hind cases(true_or_false (p a)) #pa
+ [ >filter_true // > fold_true // >fold_true //
+ | >filter_false // >fold_false // ]
+qed.
+
+record Aop (A:Type[0]) (nil:A) : Type[0] ≝
+ {op :2> A → A → A;
+ nill:∀a. op nil a = a;
+ nilr:∀a. op a nil = a;
+ assoc: ∀a,b,c.op a (op b c) = op (op a b) c
+ }.
+
+theorem fold_sum: ∀A,B. ∀I,J:list A.∀nil.∀op:Aop B nil.∀f.
+ op (\fold[op,nil]_{i∈I} (f i)) (\fold[op,nil]_{i∈J} (f i)) =
+ \fold[op,nil]_{i∈(I@J)} (f i).
+#A #B #I #J #nil #op #f (elim I) normalize
+ [>nill //|#a #tl #Hind <assoc //]
+qed.
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basics/list.ma".
+include "arithmetics/nat.ma".
+
+nlet rec length (A:Type) (l:list A) on l ≝
+ match l with
+ [ nil ⇒ 0
+ | cons a tl ⇒ S (length A tl)].
+
+notation "|M|" non associative with precedence 60 for @{'norm $M}.
+interpretation "norm" 'norm l = (length ? l).
+
+nlet rec nth n (A:Type) (l:list A) (d:A) ≝
+ match n with
+ [O ⇒ hd A l d
+ |S m ⇒ nth m A (tail A l) d].
+
--- /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 "basics/pts.ma".
+include "hints_declaration.ma".
+
+(* propositional equality *)
+
+inductive eq (A:Type[1]) (x:A) : A → Prop ≝
+ refl: eq A x x.
+
+interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
+
+lemma eq_rect_r:
+ ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → P x p.
+ #A #a #x #p (cases p) // qed.
+
+lemma eq_ind_r :
+ ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+ #A #a #P #p #x0 #p0; @(eq_rect_r ? ? ? p0) //; qed.
+
+lemma eq_rect_Type2_r:
+ ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+ #A #a #P #H #x #p (generalize in match H) (generalize in match P)
+ cases p; //; qed.
+
+theorem rewrite_l: ∀A:Type[1].∀x.∀P:A → Type[1]. P x → ∀y. x = y → P y.
+#A #x #P #Hx #y #Heq (cases Heq); //; qed.
+
+theorem sym_eq: ∀A.∀x,y:A. x = y → y = x.
+#A #x #y #Heq @(rewrite_l A x (λz.z=x)); //; qed.
+
+theorem rewrite_r: ∀A:Type[1].∀x.∀P:A → Type[1]. P x → ∀y. y = x → P y.
+#A #x #P #Hx #y #Heq (cases (sym_eq ? ? ? Heq)); //; qed.
+
+theorem eq_coerc: ∀A,B:Type[0].A→(A=B)→B.
+#A #B #Ha #Heq (elim Heq); //; qed.
+
+theorem trans_eq : ∀A.∀x,y,z:A. x = y → y = z → x = z.
+#A #x #y #z #H1 #H2 >H1; //; qed.
+
+theorem eq_f: ∀A,B.∀f:A→B.∀x,y:A. x=y → f x = f y.
+#A #B #f #x #y #H >H; //; qed.
+
+(* deleterio per auto? *)
+theorem eq_f2: ∀A,B,C.∀f:A→B→C.
+∀x1,x2:A.∀y1,y2:B. x1=x2 → y1=y2 → f x1 y1 = f x2 y2.
+#A #B #C #f #x1 #x2 #y1 #y2 #E1 #E2 >E1; >E2; //; qed.
+
+(* hint to genereric equality
+definition eq_equality: equality ≝
+ mk_equality eq refl rewrite_l rewrite_r.
+
+
+unification hint 0 ≔ T,a,b;
+ X ≟ eq_equality
+(*------------------------------------*) ⊢
+ equal X T a b ≡ eq T a b.
+*)
+
+(********** connectives ********)
+
+inductive True: Prop ≝
+I : True.
+
+inductive False: Prop ≝ .
+
+(* ndefinition Not: Prop → Prop ≝
+λA. A → False. *)
+
+inductive Not (A:Prop): Prop ≝
+nmk: (A → False) → Not A.
+
+interpretation "logical not" 'not x = (Not x).
+
+theorem absurd : ∀A:Prop. A → ¬A → False.
+#A #H #Hn (elim Hn); /2/; qed.
+
+(*
+ntheorem absurd : ∀ A,C:Prop. A → ¬A → C.
+#A; #C; #H; #Hn; nelim (Hn H).
+nqed. *)
+
+theorem not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
+/4/; qed.
+
+(* inequality *)
+interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
+
+theorem sym_not_eq: ∀A.∀x,y:A. x ≠ y → y ≠ x.
+/3/; qed.
+
+(* and *)
+inductive And (A,B:Prop) : Prop ≝
+ conj : A → B → And A B.
+
+interpretation "logical and" 'and x y = (And x y).
+
+theorem proj1: ∀A,B:Prop. A ∧ B → A.
+#A #B #AB (elim AB) //; qed.
+
+theorem proj2: ∀ A,B:Prop. A ∧ B → B.
+#A #B #AB (elim AB) //; qed.
+
+(* or *)
+inductive Or (A,B:Prop) : Prop ≝
+ or_introl : A → (Or A B)
+ | or_intror : B → (Or A B).
+
+interpretation "logical or" 'or x y = (Or x y).
+
+definition decidable : Prop → Prop ≝
+λ A:Prop. A ∨ ¬ A.
+
+(* exists *)
+inductive ex (A:Type[0]) (P:A → Prop) : Prop ≝
+ ex_intro: ∀ x:A. P x → ex A P.
+
+interpretation "exists" 'exists x = (ex ? x).
+
+inductive ex2 (A:Type[0]) (P,Q:A →Prop) : Prop ≝
+ ex_intro2: ∀ x:A. P x → Q x → ex2 A P Q.
+
+(* iff *)
+definition iff :=
+ λ A,B. (A → B) ∧ (B → A).
+
+interpretation "iff" 'iff a b = (iff a b).
+
+(* cose per destruct: da rivedere *)
+
+definition R0 ≝ λT:Type[0].λt:T.t.
+
+definition R1 ≝ eq_rect_Type0.
+
+(*
+definition R2 :
+ ∀T0:Type[0].
+ ∀a0:T0.
+ ∀T1:∀x0:T0. a0=x0 → Type[0].
+ ∀a1:T1 a0 (refl ? a0).
+ ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
+ ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
+ ∀b0:T0.
+ ∀e0:a0 = b0.
+ ∀b1: T1 b0 e0.
+ ∀e1:R1 ?? T1 a1 ? e0 = b1.
+ T2 b0 e0 b1 e1.
+#T0;#a0;#T1;#a1;#T2;#a2;#b0;#e0;#b1;#e1;
+napply (eq_rect_Type0 ????? e1);
+napply (R1 ?? ? ?? e0);
+napply a2;
+nqed.
+
+ndefinition R3 :
+ ∀T0:Type[0].
+ ∀a0:T0.
+ ∀T1:∀x0:T0. a0=x0 → Type[0].
+ ∀a1:T1 a0 (refl ? a0).
+ ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
+ ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
+ ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
+ ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
+ ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).
+ ∀b0:T0.
+ ∀e0:a0 = b0.
+ ∀b1: T1 b0 e0.
+ ∀e1:R1 ?? T1 a1 ? e0 = b1.
+ ∀b2: T2 b0 e0 b1 e1.
+ ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
+ T3 b0 e0 b1 e1 b2 e2.
+#T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#b0;#e0;#b1;#e1;#b2;#e2;
+napply (eq_rect_Type0 ????? e2);
+napply (R2 ?? ? ???? e0 ? e1);
+napply a3;
+nqed.
+
+ndefinition R4 :
+ ∀T0:Type[0].
+ ∀a0:T0.
+ ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
+ ∀a1:T1 a0 (refl T0 a0).
+ ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
+ ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
+ ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
+ ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
+ ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
+ a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2).
+ ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
+ ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
+ ∀x3:T3 x0 p0 x1 p1 x2 p2.∀p3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 x0 p0 x1 p1 x2 p2) x3.
+ Type[0].
+ ∀a4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
+ a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2)
+ a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
+ a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2))
+ a3).
+ ∀b0:T0.
+ ∀e0:eq (T0 …) a0 b0.
+ ∀b1: T1 b0 e0.
+ ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
+ ∀b2: T2 b0 e0 b1 e1.
+ ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
+ ∀b3: T3 b0 e0 b1 e1 b2 e2.
+ ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
+ T4 b0 e0 b1 e1 b2 e2 b3 e3.
+#T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#T4;#a4;#b0;#e0;#b1;#e1;#b2;#e2;#b3;#e3;
+napply (eq_rect_Type0 ????? e3);
+napply (R3 ????????? e0 ? e1 ? e2);
+napply a4;
+nqed.
+
+naxiom streicherK : ∀T:Type[2].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p. *)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basics/core_notation.ma".
+
+universe constraint Type[0] < Type[1].
+universe constraint Type[1] < Type[2].
+universe constraint Type[2] < Type[3].
+universe constraint Type[3] < Type[4].
--- /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 "basics/logic.ma".
+
+(********** relations **********)
+definition relation : Type[0] → Type[0]
+≝ λA.A→A→Prop.
+
+definition reflexive: ∀A.∀R :relation A.Prop
+≝ λA.λR.∀x:A.R x x.
+
+definition symmetric: ∀A.∀R: relation A.Prop
+≝ λA.λR.∀x,y:A.R x y → R y x.
+
+definition transitive: ∀A.∀R:relation A.Prop
+≝ λA.λR.∀x,y,z:A.R x y → R y z → R x z.
+
+definition irreflexive: ∀A.∀R:relation A.Prop
+≝ λA.λR.∀x:A.¬(R x x).
+
+definition cotransitive: ∀A.∀R:relation A.Prop
+≝ λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
+
+definition tight_apart: ∀A.∀eq,ap:relation A.Prop
+≝ λA.λeq,ap.∀x,y:A. (¬(ap x y) → eq x y) ∧
+(eq x y → ¬(ap x y)).
+
+definition antisymmetric: ∀A.∀R:relation A.Prop
+≝ λA.λR.∀x,y:A. R x y → ¬(R y x).
+
+(********** functions **********)
+
+definition compose ≝
+ λA,B,C:Type[0].λf:B→C.λg:A→B.λx:A.f (g x).
+
+interpretation "function composition" 'compose f g = (compose ? ? ? f g).
+
+definition injective: ∀A,B:Type[0].∀ f:A→B.Prop
+≝ λA,B.λf.∀x,y:A.f x = f y → x=y.
+
+definition surjective: ∀A,B:Type[0].∀f:A→B.Prop
+≝λA,B.λf.∀z:B.∃x:A.z = f x.
+
+definition commutative: ∀A:Type[0].∀f:A→A→A.Prop
+≝ λA.λf.∀x,y.f x y = f y x.
+
+definition commutative2: ∀A,B:Type[0].∀f:A→A→B.Prop
+≝ λA,B.λf.∀x,y.f x y = f y x.
+
+definition associative: ∀A:Type[0].∀f:A→A→A.Prop
+≝ λA.λf.∀x,y,z.f (f x y) z = f x (f y z).
+
+(* functions and relations *)
+definition monotonic : ∀A:Type[0].∀R:A→A→Prop.
+∀f:A→A.Prop ≝
+λA.λR.λf.∀x,y:A.R x y → R (f x) (f y).
+
+(* functions and functions *)
+definition distributive: ∀A:Type[0].∀f,g:A→A→A.Prop
+≝ λA.λf,g.∀x,y,z:A. f x (g y z) = g (f x y) (f x z).
+
+definition distributive2: ∀A,B:Type[0].∀f:A→B→B.∀g:B→B→B.Prop
+≝ λA,B.λf,g.∀x:A.∀y,z:B. f x (g y z) = g (f x y) (f x z).
+
+lemma injective_compose : ∀A,B,C,f,g.
+injective A B f → injective B C g → injective A C (λx.g (f x)).
+/3/; qed.
+
+(* extensional equality *)
+
+definition exteqP: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝
+λA.λP,Q.∀a.iff (P a) (Q a).
+
+definition exteqR: ∀A,B:Type[0].∀R,S:A→B→Prop.Prop ≝
+λA,B.λR,S.∀a.∀b.iff (R a b) (S a b).
+
+definition exteqF: ∀A,B:Type[0].∀f,g:A→B.Prop ≝
+λA,B.λf,g.∀a.f a = g a.
+
+notation " x \eqP y " non associative with precedence 45
+for @{'eqP A $x $y}.
+
+interpretation "functional extentional equality"
+'eqP A x y = (exteqP A x y).
+
+notation "x \eqR y" non associative with precedence 45
+for @{'eqR ? ? x y}.
+
+interpretation "functional extentional equality"
+'eqR A B R S = (exteqR A B R S).
+
+notation " f \eqF g " non associative with precedence 45
+for @{'eqF ? ? f g}.
+
+interpretation "functional extentional equality"
+'eqF A B f g = (exteqF A B f g).
+
--- /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 "basics/logic.ma".
+
+(* void *)
+inductive void : Type[0] ≝.
+
+(* unit *)
+inductive unit : Type[0] ≝ it: unit.
+
+(* Prod *)
+inductive Prod (A,B:Type[0]) : Type[0] ≝
+pair : A → B → Prod A B.
+
+interpretation "Pair construction" 'pair x y = (pair ? ? x y).
+
+interpretation "Product" 'product x y = (Prod x y).
+
+definition fst ≝ λA,B.λp:A × B.
+ match p with [pair a b ⇒ a].
+
+definition snd ≝ λA,B.λp:A × B.
+ match p with [pair a b ⇒ b].
+
+interpretation "pair pi1" 'pi1 = (fst ? ?).
+interpretation "pair pi2" 'pi2 = (snd ? ?).
+interpretation "pair pi1" 'pi1a x = (fst ? ? x).
+interpretation "pair pi2" 'pi2a x = (snd ? ? x).
+interpretation "pair pi1" 'pi1b x y = (fst ? ? x y).
+interpretation "pair pi2" 'pi2b x y = (snd ? ? x y).
+
+theorem eq_pair_fst_snd: ∀A,B.∀p:A × B.
+ p = 〈 \fst p, \snd p 〉.
+#A #B #p (cases p) // qed.
+
+(* sum *)
+inductive Sum (A,B:Type[0]) : Type[0] ≝
+ inl : A → Sum A B
+| inr : B → Sum A B.
+
+interpretation "Disjoint union" 'plus A B = (Sum A B).
+
+(* option *)
+inductive option (A:Type[0]) : Type[0] ≝
+ None : option A
+ | Some : A → option A.
+
+(* sigma *)
+inductive Sig (A:Type[0]) (f:A→Type[0]) : Type[0] ≝
+ dp: ∀a:A.(f a)→Sig A f.
\ No newline at end of file
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(*
+
+Notation for hint declaration
+==============================
+
+The idea is to write a context, with abstraction first, then
+recursive calls (let-in) and finally the two equivalent terms.
+The context can be empty. Note the ; to begin the second part of
+the context (necessary even if the first part is empty).
+
+ unification hint PREC \coloneq
+ ID : TY, ..., ID : TY
+ ; ID \equest T, ..., ID \equest T
+ \vdash T1 \equiv T2
+
+With unidoce and some ASCII art it looks like the following:
+
+ unification hint PREC ≔ ID : TY, ..., ID : TY;
+ ID ≟ T, ..., ID ≟ T
+ (*---------------------*) ⊢
+ T1 ≡ T2
+
+The order of premises is relevant, since they are processed in order
+(left to right).
+
+*)
+
+(* it seems unbelivable, but it works! *)
+notation > "≔ (list0 ( (list1 (ident x) sep , ) opt (: T) ) sep ,) opt (; (list1 (ident U ≟ term 19 V ) sep ,)) ⊢ term 19 Px ≡ term 19 Py"
+ with precedence 90
+ for @{ ${ fold right
+ @{ ${ default
+ @{ ${ fold right
+ @{ 'hint_decl $Px $Py }
+ rec acc1 @{ let ( ${ident U} : ?) ≝ $V in $acc1} } }
+ @{ 'hint_decl $Px $Py }
+ }
+ }
+ rec acc @{
+ ${ fold right @{ $acc } rec acc2
+ @{ ∀${ident x}:${ default @{ $T } @{ ? } }.$acc2 } }
+ }
+ }}.
+
+include "basics/pts.ma".
+
+definition hint_declaration_Type0 ≝ λA:Type[0] .λa,b:A.Prop.
+definition hint_declaration_Type1 ≝ λA:Type[1].λa,b:A.Prop.
+definition hint_declaration_Type2 ≝ λa,b:Type[2].Prop.
+definition hint_declaration_CProp0 ≝ λA:CProp[0].λa,b:A.Prop.
+definition hint_declaration_CProp1 ≝ λA:CProp[1].λa,b:A.Prop.
+definition hint_declaration_CProp2 ≝ λa,b:CProp[2].Prop.
+
+interpretation "hint_decl_Type2" 'hint_decl a b = (hint_declaration_Type2 a b).
+interpretation "hint_decl_CProp2" 'hint_decl a b = (hint_declaration_CProp2 a b).
+interpretation "hint_decl_Type1" 'hint_decl a b = (hint_declaration_Type1 ? a b).
+interpretation "hint_decl_CProp1" 'hint_decl a b = (hint_declaration_CProp1 ? a b).
+interpretation "hint_decl_CProp0" 'hint_decl a b = (hint_declaration_CProp0 ? a b).
+interpretation "hint_decl_Type0" 'hint_decl a b = (hint_declaration_Type0 ? a b).
+
+(* Non uniform coercions support
+record lock2 (S : Type[2]) (s : S) : Type[3] ≝ {
+ force2 : Type[2];
+ lift2 : force2
+}.
+
+record lock1 (S : Type[1]) (s : S) : Type[2] ≝ {
+ force1 : Type[1];
+ lift1 : force1
+}.
+
+coercion zzzlift1 : ∀S:Type[1].∀s:S.∀l:lock1 S s. force1 S s l ≝ lift1
+ on s : ? to force1 ???.
+
+coercion zzzlift2 : ∀S:Type[2].∀s:S.∀l:lock2 S s. force2 S s l ≝ lift2
+ on s : ? to force2 ???.
+
+(* Example of a non uniform coercion declaration
+
+ Type[0] setoid
+ >--->
+ MR R
+
+ provided MR = carr R
+
+unification hint 0 ≔ R : setoid;
+ MR ≟ carr R,
+ lock ≟ mk_lock1 Type[0] MR setoid R
+(* ---------------------------------------- *) ⊢
+ setoid ≡ force1 ? MR lock.
+
+*)
+*)
\ No newline at end of file
--- /dev/null
+baseuri=cic:/matita/
projects / helm.git / commitdiff