--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department of the University of Bologna, Italy.
+ ||I||
+ ||T||
+ ||A|| This file is distributed under the terms of the
+ \ / GNU General Public License Version 2
+ \ /
+ V_______________________________________________________________ *)
+
+include "arithmetics/nat.ma".
+
+let rec bigop' (n:nat) (filter: nat → bool) (A:Type[0]) (f: nat → A)
+ (nil: A) (op: A → A → A) ≝
+ match n with
+ [ O ⇒ nil
+ | S k ⇒
+ match filter k with
+ [true ⇒ op (f k) (bigop' k filter A f nil op)
+ |false ⇒ bigop' k filter A f nil op]
+ ].
+
+record range (A:Type[0]): Type[0] ≝
+ {h:nat→A; upto:nat; filter:nat→bool}.
+
+definition same_upto: nat → ∀A.relation (range A) ≝
+λk.λA.λI,J.
+ ∀i. i < k →
+ ((filter A I i) = (filter A J i) ∧
+ ((filter A I i) = true → (h A I i) = (h A J i))).
+
+definition same: ∀A.relation (range A) ≝
+λA.λI,J. (upto A I = upto A J) ∧ same_upto (upto A I) A I J.
+
+definition pad: ∀A.nat→range A→range A ≝
+ λA.λk.λI.mk_range A (h A I) k
+ (λi.if_then_else ? (leb (upto A I) i) false (filter A I i)).
+
+definition same1: ∀A.relation (range A) ≝
+λA.λI,J.
+ let maxIJ ≝ (max (upto A I) (upto A J)) in
+ same_upto maxIJ A (pad A maxIJ I) (pad A maxIJ J).
+
+(*
+definition same: ∀A.relation (range A) ≝
+λA.λI,J.
+ ∀i. i < max (upto A I) (upto A J) →
+ ((filter A I i) = (filter A J i) ∧
+ ((filter A I i) = true → (h A I i) = (h A J i))). *)
+
+definition bigop: ∀A,B:Type[0].(range A)→B→(B→B→B)→(A→B)→B ≝
+ λA,B.λI.λnil.λop.λf.
+ bigop' (upto A I) (filter A I) B (λx.f(h A I x)) nil op.
+
+theorem same_bigop: ∀A,B.∀I,J:range A. ∀nil.∀op.∀f.
+ same A I J → bigop A B I nil op f = bigop A B J nil op f.
+#A #B #I #J #nil #op #f * #equp normalize <equp #same
+@(le_gen ? (upto A I)) #i (elim i) // #i #Hind #lti
+(lapply (same i lti)) * #eqfilter
+(lapply (Hind (transitive_le … (le_n_Sn i) (lti)))) #eqbigop
+normalize <eqfilter (cases (filter A I i)) normalize //
+#H (lapply (H (refl ??))) // qed.
+
+theorem pad_bigog: ∀A,B.∀I:range A. ∀nil.∀op.∀f.∀k.
+ upto A I ≤ k → bigop A B I nil op f = bigop A B (pad A k I) nil op f.
+#A #B #I #nil #op #f #k #lek (elim lek)
+[@same_bigop % // #i #lti % // normalize
+ >(not_le_to_leb_false …) // @lt_to_not_le //
+|#n #leup #Hind normalize <Hind >(le_to_leb_true … leup) normalize //
+] qed.
+
+theorem iter_p_gen_false: \forall A:Type. \forall g: nat \to A. \forall baseA:A.
+\forall plusA: A \to A \to A. \forall n.
+iter_p_gen n (\lambda x.false) A g baseA plusA = baseA.
+intros.
+elim n
+[ reflexivity
+| simplify.
+ assumption
+]
+qed.
+
+theorem iter_p_gen_plusA: \forall A:Type. \forall n,k:nat.\forall p:nat \to bool.
+\forall g: nat \to A. \forall baseA:A. \forall plusA: A \to A \to A.
+(symmetric A plusA) \to (\forall a:A. (plusA a baseA) = a) \to (associative A plusA)
+\to
+iter_p_gen (k + n) p A g baseA plusA
+= (plusA (iter_p_gen k (\lambda x.p (x+n)) A (\lambda x.g (x+n)) baseA plusA)
+ (iter_p_gen n p A g baseA plusA)).
+intros.
+
+elim k
+[ simplify.
+ rewrite > H in \vdash (? ? ? %).
+ rewrite > (H1 ?).
+ reflexivity
+| apply (bool_elim ? (p (n1+n)))
+ [ intro.
+ rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
+ rewrite > (true_to_iter_p_gen_Sn n1 (\lambda x.p (x+n)) ? ? ? ? H4).
+ rewrite > (H2 (g (n1 + n)) ? ?).
+ rewrite < H3.
+ reflexivity
+ | intro.
+ rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
+ rewrite > (false_to_iter_p_gen_Sn n1 (\lambda x.p (x+n)) ? ? ? ? H4).
+ assumption
+ ]
+]
+qed.
+
+theorem false_to_eq_iter_p_gen: \forall A:Type. \forall n,m:nat.\forall p:nat \to bool.
+\forall g: nat \to A. \forall baseA:A. \forall plusA: A \to A \to A.
+n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false)
+\to iter_p_gen m p A g baseA plusA = iter_p_gen n p A g baseA plusA.
+intros 8.
+elim H
+[ reflexivity
+| simplify.
+ rewrite > H3
+ [ simplify.
+ apply H2.
+ intros.
+ apply H3
+ [ apply H4
+ | apply le_S.
+ assumption
+ ]
+ | assumption
+ |apply le_n
+ ]
+]
+qed.
+
+(* a therem slightly more general than the previous one *)
+theorem or_false_eq_baseA_to_eq_iter_p_gen: \forall A:Type. \forall n,m:nat.\forall p:nat \to bool.
+\forall g: nat \to A. \forall baseA:A. \forall plusA: A \to A \to A.
+(\forall a. plusA baseA a = a) \to
+n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false \lor g i = baseA)
+\to iter_p_gen m p A g baseA plusA = iter_p_gen n p A g baseA plusA.
+intros 9.
+elim H1
+[reflexivity
+|apply (bool_elim ? (p n1));intro
+ [elim (H4 n1)
+ [apply False_ind.
+ apply not_eq_true_false.
+ rewrite < H5.
+ rewrite < H6.
+ reflexivity
+ |rewrite > true_to_iter_p_gen_Sn
+ [rewrite > H6.
+ rewrite > H.
+ apply H3.intros.
+ apply H4
+ [assumption
+ |apply le_S.assumption
+ ]
+ |assumption
+ ]
+ |assumption
+ |apply le_n
+ ]
+ |rewrite > false_to_iter_p_gen_Sn
+ [apply H3.intros.
+ apply H4
+ [assumption
+ |apply le_S.assumption
+ ]
+ |assumption
+ ]
+ ]
+]
+qed.
+
+theorem iter_p_gen2 :
+\forall n,m:nat.
+\forall p1,p2:nat \to bool.
+\forall A:Type.
+\forall g: nat \to nat \to A.
+\forall baseA: A.
+\forall plusA: A \to A \to A.
+(symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a baseA) = a)
+\to
+iter_p_gen (n*m)
+ (\lambda x.andb (p1 (div x m)) (p2 (mod x m)))
+ A
+ (\lambda x.g (div x m) (mod x m))
+ baseA
+ plusA =
+iter_p_gen n p1 A
+ (\lambda x.iter_p_gen m p2 A (g x) baseA plusA)
+ baseA plusA.
+intros.
+elim n
+[ simplify.
+ reflexivity
+| apply (bool_elim ? (p1 n1))
+ [ intro.
+ rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
+ simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
+ rewrite > iter_p_gen_plusA
+ [ rewrite < H3.
+ apply eq_f2
+ [ apply eq_iter_p_gen
+ [ intros.
+ rewrite > sym_plus.
+ rewrite > (div_plus_times ? ? ? H5).
+ rewrite > (mod_plus_times ? ? ? H5).
+ rewrite > H4.
+ simplify.
+ reflexivity
+ | intros.
+ rewrite > sym_plus.
+ rewrite > (div_plus_times ? ? ? H5).
+ rewrite > (mod_plus_times ? ? ? H5).
+ reflexivity.
+ ]
+ | reflexivity
+ ]
+ | assumption
+ | assumption
+ | assumption
+ ]
+ | intro.
+ rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
+ simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
+ rewrite > iter_p_gen_plusA
+ [ rewrite > H3.
+ apply (trans_eq ? ? (plusA baseA
+ (iter_p_gen n1 p1 A (\lambda x:nat.iter_p_gen m p2 A (g x) baseA plusA) baseA plusA )))
+ [ apply eq_f2
+ [ rewrite > (eq_iter_p_gen ? (\lambda x.false) A ? (\lambda x:nat.g ((x+n1*m)/m) ((x+n1*m)\mod m)))
+ [ apply iter_p_gen_false
+ | intros.
+ rewrite > sym_plus.
+ rewrite > (div_plus_times ? ? ? H5).
+ rewrite > (mod_plus_times ? ? ? H5).
+ rewrite > H4.
+ simplify.reflexivity
+ | intros.reflexivity.
+ ]
+ | reflexivity
+ ]
+ | rewrite < H.
+ rewrite > H2.
+ reflexivity.
+ ]
+ | assumption
+ | assumption
+ | assumption
+ ]
+ ]
+]
+qed.
+
+theorem iter_p_gen2':
+\forall n,m:nat.
+\forall p1: nat \to bool.
+\forall p2: nat \to nat \to bool.
+\forall A:Type.
+\forall g: nat \to nat \to A.
+\forall baseA: A.
+\forall plusA: A \to A \to A.
+(symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a baseA) = a)
+\to
+iter_p_gen (n*m)
+ (\lambda x.andb (p1 (div x m)) (p2 (div x m)(mod x m)))
+ A
+ (\lambda x.g (div x m) (mod x m))
+ baseA
+ plusA =
+iter_p_gen n p1 A
+ (\lambda x.iter_p_gen m (p2 x) A (g x) baseA plusA)
+ baseA plusA.
+intros.
+elim n
+[ simplify.
+ reflexivity
+| apply (bool_elim ? (p1 n1))
+ [ intro.
+ rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
+ simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
+ rewrite > iter_p_gen_plusA
+ [ rewrite < H3.
+ apply eq_f2
+ [ apply eq_iter_p_gen
+ [ intros.
+ rewrite > sym_plus.
+ rewrite > (div_plus_times ? ? ? H5).
+ rewrite > (mod_plus_times ? ? ? H5).
+ rewrite > H4.
+ simplify.
+ reflexivity
+ | intros.
+ rewrite > sym_plus.
+ rewrite > (div_plus_times ? ? ? H5).
+ rewrite > (mod_plus_times ? ? ? H5).
+ reflexivity.
+ ]
+ | reflexivity
+ ]
+ | assumption
+ | assumption
+ | assumption
+ ]
+ | intro.
+ rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H4).
+ simplify in \vdash (? ? (? % ? ? ? ? ?) ?).
+ rewrite > iter_p_gen_plusA
+ [ rewrite > H3.
+ apply (trans_eq ? ? (plusA baseA
+ (iter_p_gen n1 p1 A (\lambda x:nat.iter_p_gen m (p2 x) A (g x) baseA plusA) baseA plusA )))
+ [ apply eq_f2
+ [ rewrite > (eq_iter_p_gen ? (\lambda x.false) A ? (\lambda x:nat.g ((x+n1*m)/m) ((x+n1*m)\mod m)))
+ [ apply iter_p_gen_false
+ | intros.
+ rewrite > sym_plus.
+ rewrite > (div_plus_times ? ? ? H5).
+ rewrite > (mod_plus_times ? ? ? H5).
+ rewrite > H4.
+ simplify.reflexivity
+ | intros.reflexivity.
+ ]
+ | reflexivity
+ ]
+ | rewrite < H.
+ rewrite > H2.
+ reflexivity.
+ ]
+ | assumption
+ | assumption
+ | assumption
+ ]
+ ]
+]
+qed.
+
+lemma iter_p_gen_gi:
+\forall A:Type.
+\forall g: nat \to A.
+\forall baseA:A.
+\forall plusA: A \to A \to A.
+\forall n,i:nat.
+\forall p:nat \to bool.
+(symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a baseA) = a)
+ \to
+
+i < n \to p i = true \to
+(iter_p_gen n p A g baseA plusA) =
+(plusA (g i) (iter_p_gen n (\lambda x:nat. andb (p x) (notb (eqb x i))) A g baseA plusA)).
+intros 5.
+elim n
+[ apply False_ind.
+ apply (not_le_Sn_O i).
+ assumption
+| apply (bool_elim ? (p n1));intro
+ [ elim (le_to_or_lt_eq i n1)
+ [ rewrite > true_to_iter_p_gen_Sn
+ [ rewrite > true_to_iter_p_gen_Sn
+ [ rewrite < (H2 (g i) ? ?).
+ rewrite > (H1 (g i) (g n1)).
+ rewrite > (H2 (g n1) ? ?).
+ apply eq_f2
+ [ reflexivity
+ | apply H
+ [ assumption
+ | assumption
+ | assumption
+ | assumption
+ | assumption
+ ]
+ ]
+ | rewrite > H6.simplify.
+ change with (notb (eqb n1 i) = notb false).
+ apply eq_f.
+ apply not_eq_to_eqb_false.
+ unfold Not.intro.
+ apply (lt_to_not_eq ? ? H7).
+ apply sym_eq.assumption
+ ]
+ | assumption
+ ]
+ | rewrite > true_to_iter_p_gen_Sn
+ [ rewrite > H7.
+ apply eq_f2
+ [ reflexivity
+ | rewrite > false_to_iter_p_gen_Sn
+ [ apply eq_iter_p_gen
+ [ intros.
+ elim (p x)
+ [ simplify.
+ change with (notb false = notb (eqb x n1)).
+ apply eq_f.
+ apply sym_eq.
+ apply not_eq_to_eqb_false.
+ apply (lt_to_not_eq ? ? H8)
+ | reflexivity
+ ]
+ | intros.
+ reflexivity
+ ]
+ | rewrite > H6.
+ rewrite > (eq_to_eqb_true ? ? (refl_eq ? n1)).
+ reflexivity
+ ]
+ ]
+ | assumption
+ ]
+ | apply le_S_S_to_le.
+ assumption
+ ]
+ | rewrite > false_to_iter_p_gen_Sn
+ [ elim (le_to_or_lt_eq i n1)
+ [ rewrite > false_to_iter_p_gen_Sn
+ [ apply H
+ [ assumption
+ | assumption
+ | assumption
+ | assumption
+ | assumption
+ ]
+ | rewrite > H6.reflexivity
+ ]
+ | apply False_ind.
+ apply not_eq_true_false.
+ rewrite < H5.
+ rewrite > H7.
+ assumption
+ | apply le_S_S_to_le.
+ assumption
+ ]
+ | assumption
+ ]
+ ]
+]
+qed.
+
+(* invariance under permutation; single sum *)
+theorem eq_iter_p_gen_gh:
+\forall A:Type.
+\forall baseA: A.
+\forall plusA: A \to A \to A.
+(symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a baseA) = a) \to
+\forall g: nat \to A.
+\forall h,h1: nat \to nat.
+\forall n,n1:nat.
+\forall p1,p2:nat \to bool.
+(\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to
+(\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to
+(\forall i. i < n \to p1 i = true \to h i < n1) \to
+(\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
+(\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to
+(\forall j. j < n1 \to p2 j = true \to h1 j < n) \to
+
+iter_p_gen n p1 A (\lambda x.g(h x)) baseA plusA =
+iter_p_gen n1 p2 A g baseA plusA.
+intros 10.
+elim n
+[ generalize in match H8.
+ elim n1
+ [ reflexivity
+ | apply (bool_elim ? (p2 n2));intro
+ [ apply False_ind.
+ apply (not_le_Sn_O (h1 n2)).
+ apply H10
+ [ apply le_n
+ | assumption
+ ]
+ | rewrite > false_to_iter_p_gen_Sn
+ [ apply H9.
+ intros.
+ apply H10
+ [ apply le_S.
+ apply H12
+ | assumption
+ ]
+ | assumption
+ ]
+ ]
+ ]
+| apply (bool_elim ? (p1 n1));intro
+ [ rewrite > true_to_iter_p_gen_Sn
+ [ rewrite > (iter_p_gen_gi A g baseA plusA n2 (h n1))
+ [ apply eq_f2
+ [ reflexivity
+ | apply H3
+ [ intros.
+ rewrite > H4
+ [ simplify.
+ change with ((\not eqb (h i) (h n1))= \not false).
+ apply eq_f.
+ apply not_eq_to_eqb_false.
+ unfold Not.
+ intro.
+ apply (lt_to_not_eq ? ? H11).
+ rewrite < H5
+ [ rewrite < (H5 n1)
+ [ apply eq_f.
+ assumption
+ | apply le_n
+ | assumption
+ ]
+ | apply le_S.
+ assumption
+ | assumption
+ ]
+ | apply le_S.assumption
+ | assumption
+ ]
+ | intros.
+ apply H5
+ [ apply le_S.
+ assumption
+ | assumption
+ ]
+ | intros.
+ apply H6
+ [ apply le_S.assumption
+ | assumption
+ ]
+ | intros.
+ apply H7
+ [ assumption
+ | generalize in match H12.
+ elim (p2 j)
+ [ reflexivity
+ | assumption
+ ]
+ ]
+ | intros.
+ apply H8
+ [ assumption
+ | generalize in match H12.
+ elim (p2 j)
+ [ reflexivity
+ | assumption
+ ]
+ ]
+ | intros.
+ elim (le_to_or_lt_eq (h1 j) n1)
+ [ assumption
+ | generalize in match H12.
+ elim (p2 j)
+ [ simplify in H13.
+ absurd (j = (h n1))
+ [ rewrite < H13.
+ rewrite > H8
+ [ reflexivity
+ | assumption
+ | apply andb_true_true; [2: apply H12]
+ ]
+ | apply eqb_false_to_not_eq.
+ generalize in match H14.
+ elim (eqb j (h n1))
+ [ apply sym_eq.assumption
+ | reflexivity
+ ]
+ ]
+ | simplify in H14.
+ apply False_ind.
+ apply not_eq_true_false.
+ apply sym_eq.assumption
+ ]
+ | apply le_S_S_to_le.
+ apply H9
+ [ assumption
+ | generalize in match H12.
+ elim (p2 j)
+ [ reflexivity
+ | assumption
+ ]
+ ]
+ ]
+ ]
+ ]
+ | assumption
+ | assumption
+ | assumption
+ | apply H6
+ [ apply le_n
+ | assumption
+ ]
+ | apply H4
+ [ apply le_n
+ | assumption
+ ]
+ ]
+ | assumption
+ ]
+ | rewrite > false_to_iter_p_gen_Sn
+ [ apply H3
+ [ intros.
+ apply H4[apply le_S.assumption|assumption]
+ | intros.
+ apply H5[apply le_S.assumption|assumption]
+ | intros.
+ apply H6[apply le_S.assumption|assumption]
+ | intros.
+ apply H7[assumption|assumption]
+ | intros.
+ apply H8[assumption|assumption]
+ | intros.
+ elim (le_to_or_lt_eq (h1 j) n1)
+ [ assumption
+ | absurd (j = (h n1))
+ [ rewrite < H13.
+ rewrite > H8
+ [ reflexivity
+ | assumption
+ | assumption
+ ]
+ | unfold Not.intro.
+ apply not_eq_true_false.
+ rewrite < H10.
+ rewrite < H13.
+ rewrite > H7
+ [ reflexivity
+ | assumption
+ | assumption
+ ]
+ ]
+ | apply le_S_S_to_le.
+ apply H9
+ [ assumption
+ | assumption
+ ]
+ ]
+ ]
+ | assumption
+ ]
+ ]
+]
+qed.
+
+theorem eq_iter_p_gen_pred:
+\forall A:Type.
+\forall baseA: A.
+\forall plusA: A \to A \to A.
+\forall n,p,g.
+p O = true \to
+(symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a baseA) = a) \to
+iter_p_gen (S n) (\lambda i.p (pred i)) A (\lambda i.g(pred i)) baseA plusA =
+plusA (iter_p_gen n p A g baseA plusA) (g O).
+intros.
+elim n
+ [rewrite > true_to_iter_p_gen_Sn
+ [simplify.apply H1
+ |assumption
+ ]
+ |apply (bool_elim ? (p n1));intro
+ [rewrite > true_to_iter_p_gen_Sn
+ [rewrite > true_to_iter_p_gen_Sn in ⊢ (? ? ? %)
+ [rewrite > H2 in ⊢ (? ? ? %).
+ apply eq_f.assumption
+ |assumption
+ ]
+ |assumption
+ ]
+ |rewrite > false_to_iter_p_gen_Sn
+ [rewrite > false_to_iter_p_gen_Sn in ⊢ (? ? ? %);assumption
+ |assumption
+ ]
+ ]
+ ]
+qed.
+
+definition p_ord_times \def
+\lambda p,m,x.
+ match p_ord x p with
+ [pair q r \Rightarrow r*m+q].
+
+theorem eq_p_ord_times: \forall p,m,x.
+p_ord_times p m x = (ord_rem x p)*m+(ord x p).
+intros.unfold p_ord_times. unfold ord_rem.
+unfold ord.
+elim (p_ord x p).
+reflexivity.
+qed.
+
+theorem div_p_ord_times:
+\forall p,m,x. ord x p < m \to p_ord_times p m x / m = ord_rem x p.
+intros.rewrite > eq_p_ord_times.
+apply div_plus_times.
+assumption.
+qed.
+
+theorem mod_p_ord_times:
+\forall p,m,x. ord x p < m \to p_ord_times p m x \mod m = ord x p.
+intros.rewrite > eq_p_ord_times.
+apply mod_plus_times.
+assumption.
+qed.
+
+lemma lt_times_to_lt_O: \forall i,n,m:nat. i < n*m \to O < m.
+intros.
+elim (le_to_or_lt_eq O ? (le_O_n m))
+ [assumption
+ |apply False_ind.
+ rewrite < H1 in H.
+ rewrite < times_n_O in H.
+ apply (not_le_Sn_O ? H)
+ ]
+qed.
+
+theorem iter_p_gen_knm:
+\forall A:Type.
+\forall baseA: A.
+\forall plusA: A \to A \to A.
+(symmetric A plusA) \to
+(associative A plusA) \to
+(\forall a:A.(plusA a baseA) = a)\to
+\forall g: nat \to A.
+\forall h2:nat \to nat \to nat.
+\forall h11,h12:nat \to nat.
+\forall k,n,m.
+\forall p1,p21:nat \to bool.
+\forall p22:nat \to nat \to bool.
+(\forall x. x < k \to p1 x = true \to
+p21 (h11 x) = true \land p22 (h11 x) (h12 x) = true
+\land h2 (h11 x) (h12 x) = x
+\land (h11 x) < n \land (h12 x) < m) \to
+(\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to
+p1 (h2 i j) = true \land
+h11 (h2 i j) = i \land h12 (h2 i j) = j
+\land h2 i j < k) \to
+iter_p_gen k p1 A g baseA plusA =
+iter_p_gen n p21 A (\lambda x:nat.iter_p_gen m (p22 x) A (\lambda y. g (h2 x y)) baseA plusA) baseA plusA.
+intros.
+rewrite < (iter_p_gen2' n m p21 p22 ? ? ? ? H H1 H2).
+apply sym_eq.
+apply (eq_iter_p_gen_gh A baseA plusA H H1 H2 g ? (\lambda x.(h11 x)*m+(h12 x)))
+ [intros.
+ elim (H4 (i/m) (i \mod m));clear H4
+ [elim H7.clear H7.
+ elim H4.clear H4.
+ assumption
+ |apply (lt_times_to_lt_div ? ? ? H5)
+ |apply lt_mod_m_m.
+ apply (lt_times_to_lt_O ? ? ? H5)
+ |apply (andb_true_true ? ? H6)
+ |apply (andb_true_true_r ? ? H6)
+ ]
+ |intros.
+ elim (H4 (i/m) (i \mod m));clear H4
+ [elim H7.clear H7.
+ elim H4.clear H4.
+ rewrite > H10.
+ rewrite > H9.
+ apply sym_eq.
+ apply div_mod.
+ apply (lt_times_to_lt_O ? ? ? H5)
+ |apply (lt_times_to_lt_div ? ? ? H5)
+ |apply lt_mod_m_m.
+ apply (lt_times_to_lt_O ? ? ? H5)
+ |apply (andb_true_true ? ? H6)
+ |apply (andb_true_true_r ? ? H6)
+ ]
+ |intros.
+ elim (H4 (i/m) (i \mod m));clear H4
+ [elim H7.clear H7.
+ elim H4.clear H4.
+ assumption
+ |apply (lt_times_to_lt_div ? ? ? H5)
+ |apply lt_mod_m_m.
+ apply (lt_times_to_lt_O ? ? ? H5)
+ |apply (andb_true_true ? ? H6)
+ |apply (andb_true_true_r ? ? H6)
+ ]
+ |intros.
+ elim (H3 j H5 H6).
+ elim H7.clear H7.
+ elim H9.clear H9.
+ elim H7.clear H7.
+ rewrite > div_plus_times
+ [rewrite > mod_plus_times
+ [rewrite > H9.
+ rewrite > H12.
+ reflexivity.
+ |assumption
+ ]
+ |assumption
+ ]
+ |intros.
+ elim (H3 j H5 H6).
+ elim H7.clear H7.
+ elim H9.clear H9.
+ elim H7.clear H7.
+ rewrite > div_plus_times
+ [rewrite > mod_plus_times
+ [assumption
+ |assumption
+ ]
+ |assumption
+ ]
+ |intros.
+ elim (H3 j H5 H6).
+ elim H7.clear H7.
+ elim H9.clear H9.
+ elim H7.clear H7.
+ apply (lt_to_le_to_lt ? ((h11 j)*m+m))
+ [apply monotonic_lt_plus_r.
+ assumption
+ |rewrite > sym_plus.
+ change with ((S (h11 j)*m) \le n*m).
+ apply monotonic_le_times_l.
+ assumption
+ ]
+ ]
+qed.
+
+theorem iter_p_gen_divides:
+\forall A:Type.
+\forall baseA: A.
+\forall plusA: A \to A \to A.
+\forall n,m,p:nat.O < n \to prime p \to Not (divides p n) \to
+\forall g: nat \to A.
+(symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a baseA) = a)
+
+\to
+
+iter_p_gen (S (n*(exp p m))) (\lambda x.divides_b x (n*(exp p m))) A g baseA plusA =
+iter_p_gen (S n) (\lambda x.divides_b x n) A
+ (\lambda x.iter_p_gen (S m) (\lambda y.true) A (\lambda y.g (x*(exp p y))) baseA plusA) baseA plusA.
+intros.
+cut (O < p)
+ [rewrite < (iter_p_gen2 ? ? ? ? ? ? ? ? H3 H4 H5).
+ apply (trans_eq ? ?
+ (iter_p_gen (S n*S m) (\lambda x:nat.divides_b (x/S m) n) A
+ (\lambda x:nat.g (x/S m*(p)\sup(x\mod S m))) baseA plusA) )
+ [apply sym_eq.
+ apply (eq_iter_p_gen_gh ? ? ? ? ? ? g ? (p_ord_times p (S m)))
+ [ assumption
+ | assumption
+ | assumption
+ |intros.
+ lapply (divides_b_true_to_lt_O ? ? H H7).
+ apply divides_to_divides_b_true
+ [rewrite > (times_n_O O).
+ apply lt_times
+ [assumption
+ |apply lt_O_exp.assumption
+ ]
+ |apply divides_times
+ [apply divides_b_true_to_divides.assumption
+ |apply (witness ? ? (p \sup (m-i \mod (S m)))).
+ rewrite < exp_plus_times.
+ apply eq_f.
+ rewrite > sym_plus.
+ apply plus_minus_m_m.
+ autobatch by le_S_S_to_le, lt_mod_m_m, lt_O_S;
+ ]
+ ]
+ |intros.
+ lapply (divides_b_true_to_lt_O ? ? H H7).
+ unfold p_ord_times.
+ rewrite > (p_ord_exp1 p ? (i \mod (S m)) (i/S m))
+ [change with ((i/S m)*S m+i \mod S m=i).
+ apply sym_eq.
+ apply div_mod.
+ apply lt_O_S
+ |assumption
+ |unfold Not.intro.
+ apply H2.
+ apply (trans_divides ? (i/ S m))
+ [assumption|
+ apply divides_b_true_to_divides;assumption]
+ |apply sym_times.
+ ]
+ |intros.
+ apply le_S_S.
+ apply le_times
+ [apply le_S_S_to_le.
+ change with ((i/S m) < S n).
+ apply (lt_times_to_lt_l m).
+ apply (le_to_lt_to_lt ? i);[2:assumption]
+ autobatch by eq_plus_to_le, div_mod, lt_O_S.
+ |apply le_exp
+ [assumption
+ |apply le_S_S_to_le.
+ apply lt_mod_m_m.
+ apply lt_O_S
+ ]
+ ]
+ |intros.
+ cut (ord j p < S m)
+ [rewrite > div_p_ord_times
+ [apply divides_to_divides_b_true
+ [apply lt_O_ord_rem
+ [elim H1.assumption
+ |apply (divides_b_true_to_lt_O ? ? ? H7).
+ rewrite > (times_n_O O).
+ apply lt_times
+ [assumption|apply lt_O_exp.assumption]
+ ]
+ |cut (n = ord_rem (n*(exp p m)) p)
+ [rewrite > Hcut2.
+ apply divides_to_divides_ord_rem
+ [apply (divides_b_true_to_lt_O ? ? ? H7).
+ rewrite > (times_n_O O).
+ apply lt_times
+ [assumption|apply lt_O_exp.assumption]
+ |rewrite > (times_n_O O).
+ apply lt_times
+ [assumption|apply lt_O_exp.assumption]
+ |assumption
+ |apply divides_b_true_to_divides.
+ assumption
+ ]
+ |unfold ord_rem.
+ rewrite > (p_ord_exp1 p ? m n)
+ [reflexivity
+ |assumption
+ |assumption
+ |apply sym_times
+ ]
+ ]
+ ]
+ |assumption
+ ]
+ |cut (m = ord (n*(exp p m)) p)
+ [apply le_S_S.
+ rewrite > Hcut1.
+ apply divides_to_le_ord
+ [apply (divides_b_true_to_lt_O ? ? ? H7).
+ rewrite > (times_n_O O).
+ apply lt_times
+ [assumption|apply lt_O_exp.assumption]
+ |rewrite > (times_n_O O).
+ apply lt_times
+ [assumption|apply lt_O_exp.assumption]
+ |assumption
+ |apply divides_b_true_to_divides.
+ assumption
+ ]
+ |unfold ord.
+ rewrite > (p_ord_exp1 p ? m n)
+ [reflexivity
+ |assumption
+ |assumption
+ |apply sym_times
+ ]
+ ]
+ ]
+ |intros.
+ cut (ord j p < S m)
+ [rewrite > div_p_ord_times
+ [rewrite > mod_p_ord_times
+ [rewrite > sym_times.
+ apply sym_eq.
+ apply exp_ord
+ [elim H1.assumption
+ |apply (divides_b_true_to_lt_O ? ? ? H7).
+ rewrite > (times_n_O O).
+ apply lt_times
+ [assumption|apply lt_O_exp.assumption]
+ ]
+ |cut (m = ord (n*(exp p m)) p)
+ [apply le_S_S.
+ rewrite > Hcut2.
+ apply divides_to_le_ord
+ [apply (divides_b_true_to_lt_O ? ? ? H7).
+ rewrite > (times_n_O O).
+ apply lt_times
+ [assumption|apply lt_O_exp.assumption]
+ |rewrite > (times_n_O O).
+ apply lt_times
+ [assumption|apply lt_O_exp.assumption]
+ |assumption
+ |apply divides_b_true_to_divides.
+ assumption
+ ]
+ |unfold ord.
+ rewrite > (p_ord_exp1 p ? m n)
+ [reflexivity
+ |assumption
+ |assumption
+ |apply sym_times
+ ]
+ ]
+ ]
+ |assumption
+ ]
+ |cut (m = ord (n*(exp p m)) p)
+ [apply le_S_S.
+ rewrite > Hcut1.
+ apply divides_to_le_ord
+ [apply (divides_b_true_to_lt_O ? ? ? H7).
+ rewrite > (times_n_O O).
+ apply lt_times
+ [assumption|apply lt_O_exp.assumption]
+ |rewrite > (times_n_O O).
+ apply lt_times
+ [assumption|apply lt_O_exp.assumption]
+ |assumption
+ |apply divides_b_true_to_divides.
+ assumption
+ ]
+ |unfold ord.
+ rewrite > (p_ord_exp1 p ? m n)
+ [reflexivity
+ |assumption
+ |assumption
+ |apply sym_times
+ ]
+ ]
+ ]
+ |intros.
+ rewrite > eq_p_ord_times.
+ rewrite > sym_plus.
+ apply (lt_to_le_to_lt ? (S m +ord_rem j p*S m))
+ [apply lt_plus_l.
+ apply le_S_S.
+ cut (m = ord (n*(p \sup m)) p)
+ [rewrite > Hcut1.
+ apply divides_to_le_ord
+ [apply (divides_b_true_to_lt_O ? ? ? H7).
+ rewrite > (times_n_O O).
+ apply lt_times
+ [assumption|apply lt_O_exp.assumption]
+ |rewrite > (times_n_O O).
+ apply lt_times
+ [assumption|apply lt_O_exp.assumption]
+ |assumption
+ |apply divides_b_true_to_divides.
+ assumption
+ ]
+ |unfold ord.
+ rewrite > sym_times.
+ rewrite > (p_ord_exp1 p ? m n)
+ [reflexivity
+ |assumption
+ |assumption
+ |reflexivity
+ ]
+ ]
+ |change with (S (ord_rem j p)*S m \le S n*S m).
+ apply le_times_l.
+ apply le_S_S.
+ cut (n = ord_rem (n*(p \sup m)) p)
+ [rewrite > Hcut1.
+ apply divides_to_le
+ [apply lt_O_ord_rem
+ [elim H1.assumption
+ |rewrite > (times_n_O O).
+ apply lt_times
+ [assumption|apply lt_O_exp.assumption]
+ ]
+ |apply divides_to_divides_ord_rem
+ [apply (divides_b_true_to_lt_O ? ? ? H7).
+ rewrite > (times_n_O O).
+ apply lt_times
+ [assumption|apply lt_O_exp.assumption]
+ |rewrite > (times_n_O O).
+ apply lt_times
+ [assumption|apply lt_O_exp.assumption]
+ |assumption
+ |apply divides_b_true_to_divides.
+ assumption
+ ]
+ ]
+ |unfold ord_rem.
+ rewrite > sym_times.
+ rewrite > (p_ord_exp1 p ? m n)
+ [reflexivity
+ |assumption
+ |assumption
+ |reflexivity
+ ]
+ ]
+ ]
+ ]
+ |apply eq_iter_p_gen
+
+ [intros.
+ elim (divides_b (x/S m) n);reflexivity
+ |intros.reflexivity
+ ]
+ ]
+|elim H1.apply lt_to_le.assumption
+]
+qed.
+
+(*distributive property for iter_p_gen*)
+theorem distributive_times_plus_iter_p_gen: \forall A:Type.
+\forall plusA: A \to A \to A. \forall basePlusA: A.
+\forall timesA: A \to A \to A.
+\forall n:nat. \forall k:A. \forall p:nat \to bool. \forall g:nat \to A.
+(symmetric A plusA) \to (associative A plusA) \to (\forall a:A.(plusA a basePlusA) = a) \to
+(symmetric A timesA) \to (distributive A timesA plusA) \to
+(\forall a:A. (timesA a basePlusA) = basePlusA)
+
+ \to
+
+((timesA k (iter_p_gen n p A g basePlusA plusA)) =
+ (iter_p_gen n p A (\lambda i:nat.(timesA k (g i))) basePlusA plusA)).
+intros.
+elim n
+[ simplify.
+ apply H5
+| cut( (p n1) = true \lor (p n1) = false)
+ [ elim Hcut
+ [ rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H7).
+ rewrite > (true_to_iter_p_gen_Sn ? ? ? ? ? ? H7) in \vdash (? ? ? %).
+ rewrite > (H4).
+ rewrite > (H3 k (g n1)).
+ apply eq_f.
+ assumption
+ | rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H7).
+ rewrite > (false_to_iter_p_gen_Sn ? ? ? ? ? ? H7) in \vdash (? ? ? %).
+ assumption
+ ]
+ | elim ((p n1))
+ [ left.
+ reflexivity
+ | right.
+ reflexivity
+ ]
+ ]
+]
+qed.
+
+(* old version - proved without theorem iter_p_gen_knm
+theorem iter_p_gen_2_eq:
+\forall A:Type.
+\forall baseA: A.
+\forall plusA: A \to A \to A.
+(symmetric A plusA) \to
+(associative A plusA) \to
+(\forall a:A.(plusA a baseA) = a)\to
+\forall g: nat \to nat \to A.
+\forall h11,h12,h21,h22: nat \to nat \to nat.
+\forall n1,m1,n2,m2.
+\forall p11,p21:nat \to bool.
+\forall p12,p22:nat \to nat \to bool.
+(\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to
+p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
+\land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
+\land h11 i j < n1 \land h12 i j < m1) \to
+(\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to
+p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
+\land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
+\land (h21 i j) < n2 \land (h22 i j) < m2) \to
+iter_p_gen n1 p11 A
+ (\lambda x:nat .iter_p_gen m1 (p12 x) A (\lambda y. g x y) baseA plusA)
+ baseA plusA =
+iter_p_gen n2 p21 A
+ (\lambda x:nat .iter_p_gen m2 (p22 x) A (\lambda y. g (h11 x y) (h12 x y)) baseA plusA )
+ baseA plusA.
+intros.
+rewrite < (iter_p_gen2' ? ? ? ? ? ? ? ? H H1 H2).
+rewrite < (iter_p_gen2' ? ? ? ? ? ? ? ? H H1 H2).
+apply sym_eq.
+letin h := (\lambda x.(h11 (x/m2) (x\mod m2))*m1 + (h12 (x/m2) (x\mod m2))).
+letin h1 := (\lambda x.(h21 (x/m1) (x\mod m1))*m2 + (h22 (x/m1) (x\mod m1))).
+apply (trans_eq ? ?
+ (iter_p_gen (n2*m2) (\lambda x:nat.p21 (x/m2)\land p22 (x/m2) (x\mod m2)) A
+ (\lambda x:nat.g ((h x)/m1) ((h x)\mod m1)) baseA plusA ))
+ [clear h.clear h1.
+ apply eq_iter_p_gen1
+ [intros.reflexivity
+ |intros.
+ cut (O < m2)
+ [cut (x/m2 < n2)
+ [cut (x \mod m2 < m2)
+ [elim (and_true ? ? H6).
+ elim (H3 ? ? Hcut1 Hcut2 H7 H8).
+ elim H9.clear H9.
+ elim H11.clear H11.
+ elim H9.clear H9.
+ elim H11.clear H11.
+ apply eq_f2
+ [apply sym_eq.
+ apply div_plus_times.
+ assumption
+ | apply sym_eq.
+ apply mod_plus_times.
+ assumption
+ ]
+ |apply lt_mod_m_m.
+ assumption
+ ]
+ |apply (lt_times_n_to_lt m2)
+ [assumption
+ |apply (le_to_lt_to_lt ? x)
+ [apply (eq_plus_to_le ? ? (x \mod m2)).
+ apply div_mod.
+ assumption
+ |assumption
+ ]
+ ]
+ ]
+ |apply not_le_to_lt.unfold.intro.
+ generalize in match H5.
+ apply (le_n_O_elim ? H7).
+ rewrite < times_n_O.
+ apply le_to_not_lt.
+ apply le_O_n
+ ]
+ ]
+ |apply (eq_iter_p_gen_gh ? ? ? H H1 H2 ? h h1);intros
+ [cut (O < m2)
+ [cut (i/m2 < n2)
+ [cut (i \mod m2 < m2)
+ [elim (and_true ? ? H6).
+ elim (H3 ? ? Hcut1 Hcut2 H7 H8).
+ elim H9.clear H9.
+ elim H11.clear H11.
+ elim H9.clear H9.
+ elim H11.clear H11.
+ cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))/m1 =
+ h11 (i/m2) (i\mod m2))
+ [cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))\mod m1 =
+ h12 (i/m2) (i\mod m2))
+ [rewrite > Hcut3.
+ rewrite > Hcut4.
+ rewrite > H9.
+ rewrite > H15.
+ reflexivity
+ |apply mod_plus_times.
+ assumption
+ ]
+ |apply div_plus_times.
+ assumption
+ ]
+ |apply lt_mod_m_m.
+ assumption
+ ]
+ |apply (lt_times_n_to_lt m2)
+ [assumption
+ |apply (le_to_lt_to_lt ? i)
+ [apply (eq_plus_to_le ? ? (i \mod m2)).
+ apply div_mod.
+ assumption
+ |assumption
+ ]
+ ]
+ ]
+ |apply not_le_to_lt.unfold.intro.
+ generalize in match H5.
+ apply (le_n_O_elim ? H7).
+ rewrite < times_n_O.
+ apply le_to_not_lt.
+ apply le_O_n
+ ]
+ |cut (O < m2)
+ [cut (i/m2 < n2)
+ [cut (i \mod m2 < m2)
+ [elim (and_true ? ? H6).
+ elim (H3 ? ? Hcut1 Hcut2 H7 H8).
+ elim H9.clear H9.
+ elim H11.clear H11.
+ elim H9.clear H9.
+ elim H11.clear H11.
+ cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))/m1 =
+ h11 (i/m2) (i\mod m2))
+ [cut ((h11 (i/m2) (i\mod m2)*m1+h12 (i/m2) (i\mod m2))\mod m1 =
+ h12 (i/m2) (i\mod m2))
+ [rewrite > Hcut3.
+ rewrite > Hcut4.
+ rewrite > H13.
+ rewrite > H14.
+ apply sym_eq.
+ apply div_mod.
+ assumption
+ |apply mod_plus_times.
+ assumption
+ ]
+ |apply div_plus_times.
+ assumption
+ ]
+ |apply lt_mod_m_m.
+ assumption
+ ]
+ |apply (lt_times_n_to_lt m2)
+ [assumption
+ |apply (le_to_lt_to_lt ? i)
+ [apply (eq_plus_to_le ? ? (i \mod m2)).
+ apply div_mod.
+ assumption
+ |assumption
+ ]
+ ]
+ ]
+ |apply not_le_to_lt.unfold.intro.
+ generalize in match H5.
+ apply (le_n_O_elim ? H7).
+ rewrite < times_n_O.
+ apply le_to_not_lt.
+ apply le_O_n
+ ]
+ |cut (O < m2)
+ [cut (i/m2 < n2)
+ [cut (i \mod m2 < m2)
+ [elim (and_true ? ? H6).
+ elim (H3 ? ? Hcut1 Hcut2 H7 H8).
+ elim H9.clear H9.
+ elim H11.clear H11.
+ elim H9.clear H9.
+ elim H11.clear H11.
+ apply lt_times_plus_times
+ [assumption|assumption]
+ |apply lt_mod_m_m.
+ assumption
+ ]
+ |apply (lt_times_n_to_lt m2)
+ [assumption
+ |apply (le_to_lt_to_lt ? i)
+ [apply (eq_plus_to_le ? ? (i \mod m2)).
+ apply div_mod.
+ assumption
+ |assumption
+ ]
+ ]
+ ]
+ |apply not_le_to_lt.unfold.intro.
+ generalize in match H5.
+ apply (le_n_O_elim ? H7).
+ rewrite < times_n_O.
+ apply le_to_not_lt.
+ apply le_O_n
+ ]
+ |cut (O < m1)
+ [cut (j/m1 < n1)
+ [cut (j \mod m1 < m1)
+ [elim (and_true ? ? H6).
+ elim (H4 ? ? Hcut1 Hcut2 H7 H8).
+ elim H9.clear H9.
+ elim H11.clear H11.
+ elim H9.clear H9.
+ elim H11.clear H11.
+ cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))/m2 =
+ h21 (j/m1) (j\mod m1))
+ [cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))\mod m2 =
+ h22 (j/m1) (j\mod m1))
+ [rewrite > Hcut3.
+ rewrite > Hcut4.
+ rewrite > H9.
+ rewrite > H15.
+ reflexivity
+ |apply mod_plus_times.
+ assumption
+ ]
+ |apply div_plus_times.
+ assumption
+ ]
+ |apply lt_mod_m_m.
+ assumption
+ ]
+ |apply (lt_times_n_to_lt m1)
+ [assumption
+ |apply (le_to_lt_to_lt ? j)
+ [apply (eq_plus_to_le ? ? (j \mod m1)).
+ apply div_mod.
+ assumption
+ |assumption
+ ]
+ ]
+ ]
+ |apply not_le_to_lt.unfold.intro.
+ generalize in match H5.
+ apply (le_n_O_elim ? H7).
+ rewrite < times_n_O.
+ apply le_to_not_lt.
+ apply le_O_n
+ ]
+ |cut (O < m1)
+ [cut (j/m1 < n1)
+ [cut (j \mod m1 < m1)
+ [elim (and_true ? ? H6).
+ elim (H4 ? ? Hcut1 Hcut2 H7 H8).
+ elim H9.clear H9.
+ elim H11.clear H11.
+ elim H9.clear H9.
+ elim H11.clear H11.
+ cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))/m2 =
+ h21 (j/m1) (j\mod m1))
+ [cut ((h21 (j/m1) (j\mod m1)*m2+h22 (j/m1) (j\mod m1))\mod m2 =
+ h22 (j/m1) (j\mod m1))
+ [rewrite > Hcut3.
+ rewrite > Hcut4.
+ rewrite > H13.
+ rewrite > H14.
+ apply sym_eq.
+ apply div_mod.
+ assumption
+ |apply mod_plus_times.
+ assumption
+ ]
+ |apply div_plus_times.
+ assumption
+ ]
+ |apply lt_mod_m_m.
+ assumption
+ ]
+ |apply (lt_times_n_to_lt m1)
+ [assumption
+ |apply (le_to_lt_to_lt ? j)
+ [apply (eq_plus_to_le ? ? (j \mod m1)).
+ apply div_mod.
+ assumption
+ |assumption
+ ]
+ ]
+ ]
+ |apply not_le_to_lt.unfold.intro.
+ generalize in match H5.
+ apply (le_n_O_elim ? H7).
+ rewrite < times_n_O.
+ apply le_to_not_lt.
+ apply le_O_n
+ ]
+ |cut (O < m1)
+ [cut (j/m1 < n1)
+ [cut (j \mod m1 < m1)
+ [elim (and_true ? ? H6).
+ elim (H4 ? ? Hcut1 Hcut2 H7 H8).
+ elim H9.clear H9.
+ elim H11.clear H11.
+ elim H9.clear H9.
+ elim H11.clear H11.
+ apply (lt_times_plus_times ? ? ? m2)
+ [assumption|assumption]
+ |apply lt_mod_m_m.
+ assumption
+ ]
+ |apply (lt_times_n_to_lt m1)
+ [assumption
+ |apply (le_to_lt_to_lt ? j)
+ [apply (eq_plus_to_le ? ? (j \mod m1)).
+ apply div_mod.
+ assumption
+ |assumption
+ ]
+ ]
+ ]
+ |apply not_le_to_lt.unfold.intro.
+ generalize in match H5.
+ apply (le_n_O_elim ? H7).
+ rewrite < times_n_O.
+ apply le_to_not_lt.
+ apply le_O_n
+ ]
+ ]
+ ]
+qed.*)
+
+
+theorem iter_p_gen_2_eq:
+\forall A:Type.
+\forall baseA: A.
+\forall plusA: A \to A \to A.
+(symmetric A plusA) \to
+(associative A plusA) \to
+(\forall a:A.(plusA a baseA) = a)\to
+\forall g: nat \to nat \to A.
+\forall h11,h12,h21,h22: nat \to nat \to nat.
+\forall n1,m1,n2,m2.
+\forall p11,p21:nat \to bool.
+\forall p12,p22:nat \to nat \to bool.
+(\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to
+p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
+\land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
+\land h11 i j < n1 \land h12 i j < m1) \to
+(\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to
+p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
+\land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
+\land (h21 i j) < n2 \land (h22 i j) < m2) \to
+iter_p_gen n1 p11 A
+ (\lambda x:nat .iter_p_gen m1 (p12 x) A (\lambda y. g x y) baseA plusA)
+ baseA plusA =
+iter_p_gen n2 p21 A
+ (\lambda x:nat .iter_p_gen m2 (p22 x) A (\lambda y. g (h11 x y) (h12 x y)) baseA plusA )
+ baseA plusA.
+
+intros.
+rewrite < (iter_p_gen2' ? ? ? ? ? ? ? ? H H1 H2).
+letin ha:= (\lambda x,y.(((h11 x y)*m1) + (h12 x y))).
+letin ha12:= (\lambda x.(h21 (x/m1) (x \mod m1))).
+letin ha22:= (\lambda x.(h22 (x/m1) (x \mod m1))).
+
+apply (trans_eq ? ?
+(iter_p_gen n2 p21 A (\lambda x:nat. iter_p_gen m2 (p22 x) A
+ (\lambda y:nat.(g (((h11 x y)*m1+(h12 x y))/m1) (((h11 x y)*m1+(h12 x y))\mod m1))) baseA plusA ) baseA plusA))
+[
+ apply (iter_p_gen_knm A baseA plusA H H1 H2 (\lambda e. (g (e/m1) (e \mod m1))) ha ha12 ha22);intros
+ [ elim (and_true ? ? H6).
+ cut(O \lt m1)
+ [ cut(x/m1 < n1)
+ [ cut((x \mod m1) < m1)
+ [ elim (H4 ? ? Hcut1 Hcut2 H7 H8).
+ elim H9.clear H9.
+ elim H11.clear H11.
+ elim H9.clear H9.
+ elim H11.clear H11.
+ split
+ [ split
+ [ split
+ [ split
+ [ assumption
+ | assumption
+ ]
+ | unfold ha.
+ unfold ha12.
+ unfold ha22.
+ rewrite > H14.
+ rewrite > H13.
+ apply sym_eq.
+ apply div_mod.
+ assumption
+ ]
+ | assumption
+ ]
+ | assumption
+ ]
+ | apply lt_mod_m_m.
+ assumption
+ ]
+ | apply (lt_times_n_to_lt m1)
+ [ assumption
+ | apply (le_to_lt_to_lt ? x)
+ [ apply (eq_plus_to_le ? ? (x \mod m1)).
+ apply div_mod.
+ assumption
+ | assumption
+ ]
+ ]
+ ]
+ | apply not_le_to_lt.unfold.intro.
+ generalize in match H5.
+ apply (le_n_O_elim ? H9).
+ rewrite < times_n_O.
+ apply le_to_not_lt.
+ apply le_O_n.
+ ]
+ | elim (H3 ? ? H5 H6 H7 H8).
+ elim H9.clear H9.
+ elim H11.clear H11.
+ elim H9.clear H9.
+ elim H11.clear H11.
+ cut(((h11 i j)*m1 + (h12 i j))/m1 = (h11 i j))
+ [ cut(((h11 i j)*m1 + (h12 i j)) \mod m1 = (h12 i j))
+ [ split
+ [ split
+ [ split
+ [ apply true_to_true_to_andb_true
+ [ rewrite > Hcut.
+ assumption
+ | rewrite > Hcut1.
+ rewrite > Hcut.
+ assumption
+ ]
+ | unfold ha.
+ unfold ha12.
+ rewrite > Hcut1.
+ rewrite > Hcut.
+ assumption
+ ]
+ | unfold ha.
+ unfold ha22.
+ rewrite > Hcut1.
+ rewrite > Hcut.
+ assumption
+ ]
+ | cut(O \lt m1)
+ [ cut(O \lt n1)
+ [ apply (lt_to_le_to_lt ? ((h11 i j)*m1 + m1) )
+ [ unfold ha.
+ apply (lt_plus_r).
+ assumption
+ | rewrite > sym_plus.
+ rewrite > (sym_times (h11 i j) m1).
+ rewrite > times_n_Sm.
+ rewrite > sym_times.
+ apply (le_times_l).
+ assumption
+ ]
+ | apply not_le_to_lt.unfold.intro.
+ generalize in match H12.
+ apply (le_n_O_elim ? H11).
+ apply le_to_not_lt.
+ apply le_O_n
+ ]
+ | apply not_le_to_lt.unfold.intro.
+ generalize in match H10.
+ apply (le_n_O_elim ? H11).
+ apply le_to_not_lt.
+ apply le_O_n
+ ]
+ ]
+ | rewrite > (mod_plus_times m1 (h11 i j) (h12 i j)).
+ reflexivity.
+ assumption
+ ]
+ | rewrite > (div_plus_times m1 (h11 i j) (h12 i j)).
+ reflexivity.
+ assumption
+ ]
+ ]
+| apply (eq_iter_p_gen1)
+ [ intros. reflexivity
+ | intros.
+ apply (eq_iter_p_gen1)
+ [ intros. reflexivity
+ | intros.
+ rewrite > (div_plus_times)
+ [ rewrite > (mod_plus_times)
+ [ reflexivity
+ | elim (H3 x x1 H5 H7 H6 H8).
+ assumption
+ ]
+ | elim (H3 x x1 H5 H7 H6 H8).
+ assumption
+ ]
+ ]
+ ]
+]
+qed.
+
+theorem iter_p_gen_iter_p_gen:
+\forall A:Type.
+\forall baseA: A.
+\forall plusA: A \to A \to A.
+(symmetric A plusA) \to
+(associative A plusA) \to
+(\forall a:A.(plusA a baseA) = a)\to
+\forall g: nat \to nat \to A.
+\forall n,m.
+\forall p11,p21:nat \to bool.
+\forall p12,p22:nat \to nat \to bool.
+(\forall x,y. x < n \to y < m \to
+ (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to
+iter_p_gen n p11 A
+ (\lambda x:nat.iter_p_gen m (p12 x) A (\lambda y. g x y) baseA plusA)
+ baseA plusA =
+iter_p_gen m p21 A
+ (\lambda y:nat.iter_p_gen n (p22 y) A (\lambda x. g x y) baseA plusA )
+ baseA plusA.
+intros.
+apply (iter_p_gen_2_eq A baseA plusA H H1 H2 (\lambda x,y. g x y) (\lambda x,y.y) (\lambda x,y.x) (\lambda x,y.y) (\lambda x,y.x)
+ n m m n p11 p21 p12 p22)
+ [intros.split
+ [split
+ [split
+ [split
+ [split
+ [apply (andb_true_true ? (p12 j i)).
+ rewrite > H3
+ [rewrite > H6.rewrite > H7.reflexivity
+ |assumption
+ |assumption
+ ]
+ |apply (andb_true_true_r (p11 j)).
+ rewrite > H3
+ [rewrite > H6.rewrite > H7.reflexivity
+ |assumption
+ |assumption
+ ]
+ ]
+ |reflexivity
+ ]
+ |reflexivity
+ ]
+ |assumption
+ ]
+ |assumption
+ ]
+ |intros.split
+ [split
+ [split
+ [split
+ [split
+ [apply (andb_true_true ? (p22 j i)).
+ rewrite < H3
+ [rewrite > H6.rewrite > H7.reflexivity
+ |assumption
+ |assumption
+ ]
+ |apply (andb_true_true_r (p21 j)).
+ rewrite < H3
+ [rewrite > H6.rewrite > H7.reflexivity
+ |assumption
+ |assumption
+ ]
+ ]
+ |reflexivity
+ ]
+ |reflexivity
+ ]
+ |assumption
+ ]
+ |assumption
+ ]
+ ]
+qed.
\ 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 "arithmetics/nat.ma".
+
+let rec mod_aux p m n: nat ≝
+match p with
+ [ O ⇒ m
+ | S q ⇒ match (leb m n) with
+ [ true ⇒ m
+ | false ⇒ mod_aux q (m-(S n)) n]].
+
+definition mod : nat → nat → nat ≝
+λn,m. match m with
+ [ O ⇒ n
+ | S p ⇒ mod_aux n n p].
+
+interpretation "natural remainder" 'module x y = (mod x y).
+
+let rec div_aux p m n : nat ≝
+match p with
+ [ O ⇒ O
+ | S q ⇒ match (leb m n) with
+ [ true ⇒ O
+ | false ⇒ S (div_aux q (m-(S n)) n)]].
+
+definition div : nat → nat → nat ≝
+λn,m.match m with
+ [ O ⇒ S n
+ | S p ⇒ div_aux n n p].
+
+interpretation "natural divide" 'divide x y = (div x y).
+
+theorem le_mod_aux_m_m:
+∀p,n,m. n ≤ p → mod_aux p n m ≤ m.
+#p (elim p)
+[ normalize #n #m #lenO @(le_n_O_elim …lenO) //
+| #q #Hind #n #m #len normalize
+ @(leb_elim n m) normalize //
+ #notlenm @Hind @le_plus_to_minus
+ @(transitive_le … len) /2/
+qed.
+
+theorem lt_mod_m_m: ∀n,m. O < m → n \mod m < m.
+#n #m (cases m)
+ [#abs @False_ind /2/
+ |#p #_ normalize @le_S_S /2/
+ ]
+qed.
+
+theorem div_aux_mod_aux: ∀p,n,m:nat.
+n=(div_aux p n m)*(S m) + (mod_aux p n m).
+#p (elim p)
+ [#n #m normalize //
+ |#q #Hind #n #m normalize
+ @(leb_elim n m) #lenm normalize //
+ >(associative_plus ???) <(Hind (n-(S m)) m)
+ applyS plus_minus_m_m (* bello *) /2/
+qed.
+
+theorem div_mod: ∀n,m:nat. n=(n / m)*m+(n \mod m).
+#n #m (cases m) normalize //
+qed.
+
+theorem eq_times_div_minus_mod:
+∀a,b:nat. (a / b) * b = a - (a \mod b).
+#a #b (applyS minus_plus_m_m) qed.
+
+inductive div_mod_spec (n,m,q,r:nat) : Prop ≝
+div_mod_spec_intro: r < m → n=q*m+r → div_mod_spec n m q r.
+
+theorem div_mod_spec_to_not_eq_O:
+ ∀n,m,q,r.div_mod_spec n m q r → m ≠ O.
+#n #m #q #r * /2/
+qed.
+
+theorem div_mod_spec_div_mod:
+ ∀n,m. O < m → div_mod_spec n m (n / m) (n \mod m).
+#n #m #posm % /2/ qed.
+
+theorem div_mod_spec_to_eq :∀ a,b,q,r,q1,r1.
+div_mod_spec a b q r → div_mod_spec a b q1 r1 → q = q1.
+#a #b #q #r #q1 #r1 * #ltrb #spec * #ltr1b #spec1
+@(leb_elim q q1) #leqq1
+ [(elim (le_to_or_lt_eq … leqq1)) //
+ #ltqq1 @False_ind @(absurd ?? (not_le_Sn_n a))
+ @(lt_to_le_to_lt ? ((S q)*b) ?)
+ [>spec (applyS (monotonic_lt_plus_r … ltrb))
+ |@(transitive_le ? (q1*b)) /2/
+ ]
+ (* this case is symmetric *)
+ |@False_ind @(absurd ?? (not_le_Sn_n a))
+ @(lt_to_le_to_lt ? ((S q1)*b) ?)
+ [>spec1 (applyS (monotonic_lt_plus_r … ltr1b))
+ |cut (q1 < q) [/2/] #ltq1q @(transitive_le ? (q*b)) /2/
+ ]
+ ]
+qed.
+
+theorem div_mod_spec_to_eq2: ∀a,b,q,r,q1,r1.
+ div_mod_spec a b q r → div_mod_spec a b q1 r1 → r = r1.
+#a #b #q #r #q1 #r1 #spec #spec1
+cut (q=q1) [@(div_mod_spec_to_eq … spec spec1)]
+#eqq (elim spec) #_ #eqa (elim spec1) #_ #eqa1
+@(injective_plus_r (q*b)) //
+qed.
+
+(* boh
+theorem div_mod_spec_times : ∀ n,m:nat.div_mod_spec ((S n)*m) (S n) m O.
+intros.constructor 1.
+unfold lt.apply le_S_S.apply le_O_n. demodulate. reflexivity.
+(*rewrite < plus_n_O.rewrite < sym_times.reflexivity.*)
+qed. *)
+
+lemma div_plus_times: ∀m,q,r:nat. r < m → (q*m+r)/ m = q.
+#m #q #r #ltrm
+@(div_mod_spec_to_eq … (div_mod_spec_div_mod ???)) /2/
+qed.
+
+lemma mod_plus_times: ∀m,q,r:nat. r < m → (q*m+r) \mod m = r.
+#m #q #r #ltrm
+@(div_mod_spec_to_eq2 … (div_mod_spec_div_mod ???)) /2/
+qed.
+
+(* some properties of div and mod *)
+theorem div_times: ∀a,b:nat. O < b → a*b/b = a.
+#a #b #posb
+@(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 eq_div_O: ∀n,m. n < m → n / m = O.
+#n #m #ltnm
+@(div_mod_spec_to_eq n m (n/m) … n (div_mod_spec_div_mod …))
+/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. *)
+
+theorem mod_S: ∀n,m:nat. O < m → S (n \mod m) < m →
+((S n) \mod m) = S (n \mod m).
+#n #m #posm #H
+@(div_mod_spec_to_eq2 (S n) m … (n / m) ? (div_mod_spec_div_mod …))
+// @div_mod_spec_intro// (applyS eq_f) //
+qed.
+
+theorem mod_O_n: ∀n:nat.O \mod n = O.
+/2/ qed.
+
+theorem lt_to_eq_mod: ∀n,m:nat. n < m → n \mod m = n.
+#n #m #ltnm
+@(div_mod_spec_to_eq2 n m (n/m) … O n (div_mod_spec_div_mod …))
+/2/ qed.
+
+(*
+theorem mod_1: ∀n:nat. mod n 1 = O.
+#n @sym_eq @le_n_O_to_eq
+@le_S_S_to_le /2/ qed.
+
+theorem div_1: ∀n:nat. div n 1 = n.
+#n @sym_eq napplyS (div_mod n 1) qed. *)
+
+theorem or_div_mod: ∀n,q. O < q →
+ ((S (n \mod q)=q) ∧ S n = (S (div n q)) * q ∨
+ ((S (n \mod q)<q) ∧ S n = (div n q) * q + S (n\mod q))).
+#n #q #posq
+(elim (le_to_or_lt_eq ?? (lt_mod_m_m n q posq))) #H
+ [%2 % // (applyS eq_f) //
+ |%1 % // /demod/ <H in ⊢(? ? ? (? % ?)) @eq_f//
+ ]
+qed.
+
+(* injectivity *)
+theorem injective_times_r:
+ ∀n:nat. O < n → injective nat nat (λm:nat.n*m).
+#n #posn #a #b #eqn
+<(div_times a n posn) <(div_times b n posn) //
+qed.
+
+theorem injective_times_l:
+ ∀n:nat. O < n → injective nat nat (λm:nat.m*n).
+/2/ qed.
+
+(* n_divides computes the pair (div,mod)
+(* p is just an upper bound, acc is an accumulator *)
+let rec n_divides_aux p n m acc \def
+ match n \mod m with
+ [ O \Rightarrow
+ match p with
+ [ O \Rightarrow pair nat nat acc n
+ | (S p) \Rightarrow n_divides_aux p (n / m) m (S acc)]
+ | (S a) \Rightarrow pair nat nat acc n].
+
+(* n_divides n m = <q,r> if m divides n q times, with remainder r *)
+definition n_divides \def \lambda n,m:nat.n_divides_aux n n m O. *)
+
+(* inequalities *)
+
+theorem lt_div_S: ∀n,m. O < m → n < S(n / m)*m.
+#n #m #posm (change with (n < m +(n/m)*m))
+>(div_mod n m) in ⊢ (? % ?) >(commutative_plus ? ?)
+@monotonic_lt_plus_l @lt_mod_m_m //
+qed.
+
+theorem le_div: ∀n,m. O < n → m/n ≤ m.
+#n #m #posn
+>(div_mod m n) in \vdash (? ? %) @(transitive_le ? (m/n*n)) /2/
+qed.
+
+theorem le_plus_mod: ∀m,n,q. O < q →
+(m+n) \mod q ≤ m \mod q + n \mod q .
+#m #n #q #posq
+(elim (decidable_le q (m \mod q + n \mod q))) #Hle
+ [@(transitive_le … Hle) @le_S_S_to_le @le_S /2/
+ |cut ((m+n)\mod q = m\mod q+n\mod q) //
+ @(div_mod_spec_to_eq2 … (m/q + n/q) ? (div_mod_spec_div_mod … posq)).
+ @div_mod_spec_intro
+ [@not_le_to_lt //
+ |>(div_mod n q) in ⊢ (? ? (? ? %) ?)
+ (applyS (eq_f … (λx.plus x (n \mod q))))
+ >(div_mod m q) in ⊢ (? ? (? % ?) ?)
+ (applyS (eq_f … (λx.plus x (m \mod q)))) //
+ ]
+ ]
+qed.
+
+theorem le_plus_div: ∀m,n,q. O < q →
+ m/q + n/q \le (m+n)/q.
+#m #n #q #posq @(le_times_to_le … posq)
+@(le_plus_to_le_r ((m+n) \mod q))
+(* bruttino *)
+>(commutative_times …) in ⊢ (? ? %) <(div_mod …)
+>(div_mod m q) in ⊢ (? ? (? % ?)) >(div_mod n q) in ⊢ (? ? (? ? %))
+>(commutative_plus …) in ⊢ (? ? (? % ?)) >(associative_plus …) in ⊢ (? ? %)
+<(associative_plus …) in ⊢ (? ? (? ? %)) (applyS monotonic_le_plus_l) /2/
+qed.
+
+theorem le_times_to_le_div: ∀a,b,c:nat.
+ O < b → b*c ≤ a → c ≤ a/b.
+#a #b #c #posb #Hle
+@le_S_S_to_le @(lt_times_n_to_lt_l b) @(le_to_lt_to_lt ? a)/2/
+qed.
+
+theorem le_times_to_le_div2: ∀m,n,q. O < q →
+ n ≤ m*q → n/q ≤ m.
+#m #n #q #posq #Hle
+@(le_times_to_le q ? ? posq) @(le_plus_to_le (n \mod q)) /2/
+qed.
+
+(* da spostare
+theorem lt_m_nm: ∀n,m. O < m → 1 < n → m < n*m.
+/2/ qed. *)
+
+theorem lt_times_to_lt_div: ∀m,n,q. n < m*q → n/q < m.
+#m #n #q #Hlt
+@(lt_times_n_to_lt_l q …) @(lt_plus_to_lt_l (n \mod q)) /2/
+qed.
+
+(*
+theorem lt_div: ∀n,m. O < m → 1 < n → m/n < m.
+#n #m #posm #lt1n
+@lt_times_to_lt_div (applyS lt_m_nm) //.
+qed.
+
+theorem le_div_plus_S: ∀m,n,q. O < q →
+(m+n)/q \le S(m/q + n/q).
+#m #n #q #posq
+@le_S_S_to_le @lt_times_to_lt_div
+@(lt_to_le_to_lt … (lt_plus … (lt_div_S m … posq) (lt_div_S n … posq)))
+//
+qed. *)
+
+theorem le_div_S_S_div: ∀n,m. O < m → (S n)/m ≤ S (n /m).
+#n #m #posm @le_times_to_le_div2 /2/
+qed.
+
+theorem le_times_div_div_times: ∀a,n,m.O < m →
+a*(n/m) ≤ a*n/m.
+#a #n #m #posm @le_times_to_le_div /2/
+qed.
+
+theorem monotonic_div: ∀n.O < n →
+ monotonic nat le (λm.div m n).
+#n #posn #a #b #leab @le_times_to_le_div/2/
+qed.
+
+theorem pos_div: ∀n,m:nat. O < m → O < n → n \mod m = O →
+ O < n / m.
+#n #m #posm #posn #mod0
+@(lt_times_n_to_lt_l m)// (* MITICO *)
+qed.
+
+(*
+theorem lt_div_n_m_n: ∀n,m:nat. 1 < m → O < n → n / m < n.
+#n #m #ltm #posn
+@(leb_elim 1 (n / m))/2/ (* MITICO *)
+qed. *)
+
+theorem eq_div_div_div_times: ∀n,m,q. O < n → O < m →
+ q/n/m = q/(n*m).
+#n #m #q #posn #posm
+@(div_mod_spec_to_eq … (q\mod n+n*(q/n\mod m)) … (div_mod_spec_div_mod …)) /2/
+@div_mod_spec_intro // @(lt_to_le_to_lt ? (n*(S (q/n\mod m))))
+ [(applyS monotonic_lt_plus_l) /2/
+ |@monotonic_le_times_r/2/
+ ]
+qed.
+
+theorem eq_div_div_div_div: ∀n,m,q. O < n → O < m →
+q/n/m = q/m/n.
+#n #m #q #posn #posm
+@(trans_eq ? ? (q/(n*m)))
+ [/2/
+ |@sym_eq (applyS eq_div_div_div_times) //
+ ]
+qed.
+
+(*
+theorem SSO_mod: \forall n,m. O < m \to (S(S O))*n/m = (n/m)*(S(S O)) + mod ((S(S O))*n/m) (S(S O)).
+intros.
+rewrite < (lt_O_to_div_times n (S(S O))) in ⊢ (? ? ? (? (? (? % ?) ?) ?))
+ [rewrite > eq_div_div_div_div
+ [rewrite > sym_times in ⊢ (? ? ? (? (? (? (? % ?) ?) ?) ?)).
+ apply div_mod.
+ apply lt_O_S
+ |apply lt_O_S
+ |assumption
+ ]
+ |apply lt_O_S
+ ]
+qed. *)
+(* Forall a,b : N. 0 < b \to b * (a/b) <= a < b * (a/b +1) *)
+(* The theorem is shown in two different parts: *)
+(*
+theorem lt_to_div_to_and_le_times_lt_S: \forall a,b,c:nat.
+O \lt b \to a/b = c \to (b*c \le a \land a \lt b*(S c)).
+intros.
+split
+[ rewrite < H1.
+ rewrite > sym_times.
+ rewrite > eq_times_div_minus_mod
+ [ apply (le_minus_m a (a \mod b))
+ | assumption
+ ]
+| rewrite < (times_n_Sm b c).
+ rewrite < H1.
+ rewrite > sym_times.
+ rewrite > (div_mod a b) in \vdash (? % ?)
+ [ rewrite > (sym_plus b ((a/b)*b)).
+ apply lt_plus_r.
+ apply lt_mod_m_m.
+ assumption
+ | assumption
+ ]
+]
+qed. *)
+
+theorem le_plus_to_minus_r: ∀a,b,c. a + b \le c → a \le c -b.
+#a #b #c #H @(le_plus_to_le_r … b) /2/
+qed.
+
+theorem le_minus_to_plus_r: ∀a,b,c. c ≤ b → a ≤ b - c → a + c ≤ b.
+#a #b #c #Hlecb #H >(plus_minus_m_m … Hlecb) /2/
+qed.
+
+theorem lt_minus_to_plus: ∀a,b,c. a - b < c → a < c + b.
+#a #b #c #H @not_le_to_lt
+@(not_to_not … (lt_to_not_le …H)) /2/
+qed.
+
+theorem lt_minus_to_plus_r: ∀a,b,c. c ≤ a →
+ a < b + c → a - c < b.
+#a #b #c #lea #H @not_le_to_lt
+@(not_to_not … (lt_to_not_le …H)) /2/
+qed.
+
+theorem lt_to_le_times_to_lt_S_to_div: ∀a,c,b:nat.
+O < b → (b*c) ≤ a → a < (b*(S c)) → a/b = c.
+#a #c #b #posb#lea #lta
+@(div_mod_spec_to_eq … (a-b*c) (div_mod_spec_div_mod … posb …))
+@div_mod_spec_intro [@lt_minus_to_plus_r // |/2/]
+qed.
+
+theorem div_times_times: ∀a,b,c:nat. O < c → O < b →
+ (a/b) = (a*c)/(b*c).
+#a #b #c #posc #posb
+>(commutative_times b c) <(eq_div_div_div_times … )//
+>(div_times … posc)//
+qed.
+
+theorem times_mod: ∀a,b,c:nat.
+O < c → O < b → (a*c) \mod (b*c) = c*(a\mod b).
+#a #b #c #posc #posb
+@(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 posb …) @div_mod_spec_div_mod /2/
+ |@div_mod_spec_intro
+ [(applyS monotonic_lt_times_l) /2/
+ |(applyS (eq_f …(λx.x*c))) //
+ ]
+ ]
+qed.
+
+theorem le_div_times_m: ∀a,i,m. O < i → O < m →
+ (a * (m / i)) / m ≤ a / i.
+#a #i #m #posi #posm
+@(transitive_le ? ((a*m/i)/m))
+ [@monotonic_div /2/
+ |>(eq_div_div_div_div … posi posm) >(div_times …) //
+ ]
+qed.
+
+(* serve ?
+theorem le_div_times_Sm: ∀a,i,m. O < i → O < m →
+a / i ≤ (a * S (m / i))/m.
+intros.
+apply (trans_le ? ((a * S (m/i))/((S (m/i))*i)))
+ [rewrite < (eq_div_div_div_times ? i)
+ [rewrite > lt_O_to_div_times
+ [apply le_n
+ |apply lt_O_S
+ ]
+ |apply lt_O_S
+ |assumption
+ ]
+ |apply le_times_to_le_div
+ [assumption
+ |apply (trans_le ? (m*(a*S (m/i))/(S (m/i)*i)))
+ [apply le_times_div_div_times.
+ rewrite > (times_n_O O).
+ apply lt_times
+ [apply lt_O_S
+ |assumption
+ ]
+ |rewrite > sym_times.
+ apply le_times_to_le_div2
+ [rewrite > (times_n_O O).
+ apply lt_times
+ [apply lt_O_S
+ |assumption
+ ]
+ |apply le_times_r.
+ apply lt_to_le.
+ apply lt_div_S.
+ 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/nat.ma".
+
+(* maximization *)
+
+let rec max' i f d ≝
+ match i with
+ [ O ⇒ d
+ | S j ⇒
+ match (f j) with
+ [ true ⇒ j
+ | false ⇒ max' j f d]].
+
+definition max ≝ λn.λf.max' n f O.
+
+theorem max_O: ∀f. max O f = O.
+// qed.
+
+theorem max_cases: ∀f.∀n.
+ (f n = true ∧ max (S n) f = n) ∨
+ (f n = false ∧ max (S n) f = max n f).
+#f #n normalize cases (f n) normalize /3/ qed.
+
+theorem le_max_n: ∀f.∀n. max n f ≤ n.
+#f #n (elim n) // #m #Hind
+normalize (cases (f m)) normalize @le_S //
+(* non trova Hind *)
+@Hind
+qed.
+
+theorem lt_max_n : ∀f.∀n. O < n → max n f < n.
+#f #n #posn @(lt_O_n_elim ? posn) #m
+normalize (cases (f m)) normalize apply le_S_S //
+@le_max_n qed.
+
+theorem le_to_le_max : ∀f.∀n,m.
+n ≤ m → max n f ≤ max m f.
+#f #n #m #H (elim H) //
+#i #leni #Hind @(transitive_le … Hind)
+(cases (max_cases f i)) * #_ /2/
+qed.
+
+theorem true_to_le_max: ∀f.∀n,m.
+ m < n → f m = true → m ≤ max n f.
+#f #n (elim n)
+ [#m #ltmO @False_ind /2/
+ |#i #Hind #m #ltm
+ (cases (le_to_or_lt_eq … (le_S_S_to_le … ltm)))
+ [#ltm #fm @(transitive_le ? (max i f))
+ [@Hind /2/ | @le_to_le_max //]
+ |#eqm >eqm #eqf normalize >eqf //
+ ]
+qed.
+
+theorem lt_max_to_false: ∀f.∀n,m.
+ m < n → max n f < m → f m = false.
+#f #n #m #ltnm #eqf cases(true_or_false (f m)) //
+#fm @False_ind @(absurd … eqf) @(le_to_not_lt) @true_to_le_max //
+qed.
+
+lemma max_exists: ∀f.∀n,m.m < n → f m =true →
+ (∀i. m < i → i < n → f i = false) → max n f = m.
+#f #n (elim n) #m
+ [#ltO @False_ind /2/
+ |#Hind #max #ltmax #fmax #ismax
+ cases (le_to_or_lt_eq …(le_S_S_to_le …(ltmax …)))
+ #ltm normalize
+ [>(ismax m …) // normalize @(Hind max ltm fmax)
+ #i #Hl #Hr @ismax // @le_S //
+ |<ltm >fmax //
+ ]
+ ]
+qed.
+
+lemma max_not_exists: ∀f.∀n.
+ (∀i. i < n → f i = false) → max n f = O.
+#f #n #ffalse @(le_gen ? n) #i (elim i) // #j #Hind #ltj
+normalize >(ffalse j …) // @Hind /2/
+qed.
+
+lemma fmax_false: ∀f.∀n,m.max n f = m → f m = false → m = O.
+#f #n #m (elim n) //
+#i #Hind normalize cases(true_or_false … (f i)) #fi >fi
+normalize
+ [#eqm #fm @False_ind @(absurd … fi) // |@Hind]
+qed.
+
+inductive max_spec (n:nat) (f:nat→bool) : nat→Prop ≝
+ | found : ∀m:nat.m < n → f m =true →
+ (∀i. m < i → i < n → f i = false) → max_spec n f m
+ | not_found: (∀i.i < n → f i = false) → max_spec n f O.
+
+theorem max_spec_to_max: ∀f.∀n,m.
+ max_spec n f m → max n f = m.
+#f #n #m #spec (cases spec)
+ [#max #ltmax #fmax #ismax @max_exists // @ismax
+ |#ffalse @max_not_exists @ffalse
+ ]
+qed.
+
+theorem max_to_max_spec: ∀f.∀n,m.
+ max n f = m → max_spec n f m.
+#f #n #m (cases n)
+ [#eqm <eqm %2 #i #ltiO @False_ind /2/
+ |#n #eqm cases(true_or_false (f m)) #fm
+ (* non trova max_to_false *)
+ [%1 /2/
+ |lapply (fmax_false ??? eqm fm) #eqmO >eqmO
+ %2 #i (cases i) // #j #ltj @(lt_max_to_false … ltj) //
+qed.
+
+theorem max_f_g: ∀f,g,n.(∀i. i < n → f i = g i) →
+ max n f = max n g.
+#f #g #n (elim n) //
+#m #Hind #ext normalize >(ext … (le_n …)) >(Hind …) //
+#i #ltim @ext /2/
+qed.
+
+theorem le_max_f_max_g: ∀f,g,n. (∀i. i < n → f i = true → g i =true) →
+max n f ≤ max n g.
+#f #g #n (elim n) //
+#m #Hind #ext normalize (cases (true_or_false (f m))) #Heq >Heq
+ [>(ext m …) //
+ |(cases (g m)) normalize [@le_max_n] @Hind #i #ltim @ext /2/
+qed.
+
+theorem f_max_true : ∀ f.∀n.
+(∃i:nat. i < n ∧ f i = true) → f (max n f) = true.
+#f #n cases(max_to_max_spec f n (max n f) (refl …)) //
+#Hall * #x * #ltx #fx @False_ind @(absurd … fx) >(Hall x ?) /2/
+qed.
+
+(* minimization *)
+
+(* min k b f is the minimun i, b ≤ i < b + k s.t. f i;
+ returns b + k otherwise *)
+
+let rec min k b f ≝
+ match k with
+ [ O ⇒ b
+ | S p ⇒
+ match f b with
+ [ true ⇒ b
+ | false ⇒ min p (S b) f]].
+
+definition min0 ≝ λn.λf. min n 0 f.
+
+theorem min_O_f : ∀f.∀b. min O b f = b.
+// qed.
+
+theorem true_min: ∀f.∀b.
+ f b = true → ∀n.min n b f = b.
+#f #b #fb #n (cases n) // #n normalize >fb normalize //
+qed.
+
+theorem false_min: ∀f.∀n,b.
+ f b = false → min (S n) b f = min n (S b) f.
+#f #n #b #fb normalize >fb normalize //
+qed.
+
+(*
+theorem leb_to_le_min : ∀f.∀n,b1,b2.
+b1 ≤ b2 → min n b1 f ≤ min n b2 f.
+#f #n #b1 #b2 #leb (elim n) //
+#m #Hind normalize (cases (f m)) normalize *)
+
+theorem le_min_r: ∀f.∀n,b. min n b f ≤ n + b.
+#f #n normalize (elim n) // #m #Hind #b
+normalize (cases (f b)) normalize //
+qed.
+
+theorem le_min_l: ∀f.∀n,b. b ≤ min n b f.
+#f #n normalize (elim n) // #m #Hind #b
+normalize (cases (f b)) normalize /2/
+qed.
+
+theorem le_to_le_min : ∀f.∀n,m.
+n ≤ m → ∀b.min n b f ≤ min m b f.
+#f @nat_elim2 //
+ [#n #leSO @False_ind /2/
+ |#n #m #Hind #leSS #b
+ (cases (true_or_false (f b))) #fb
+ [lapply (true_min …fb) //
+ |>(false_min f n b fb) >(false_min f m b fb) @Hind /2/
+ ]
+ ]
+qed.
+
+theorem true_to_le_min: ∀f.∀n,m,b.
+ b ≤ m → f m = true → min n b f ≤ m.
+#f #n (elim n) //
+#i #Hind #m #b #leb (cases (le_to_or_lt_eq … leb))
+ [#ltm #fm normalize (cases (f b)) normalize // @Hind //
+ |#eqm <eqm #eqb normalize >eqb normalize //
+ ]
+qed.
+
+theorem lt_min_to_false: ∀f.∀n,m,b.
+ b ≤ m → m < min n b f → f m = false.
+#f #n #m #b #lebm #ltm cases(true_or_false (f m)) //
+#fm @False_ind @(absurd … ltm) @(le_to_not_lt) @true_to_le_min //
+qed.
+
+theorem fmin_true: ∀f.∀n,m,b.
+ m = min n b f → m < n + b → f m = true.
+#f #n (elim n)
+ [#m #b normalize #eqmb >eqmb #leSb @(False_ind)
+ @(absurd … leSb) //
+ |#n #Hind #m #b (cases (true_or_false (f b))) #caseb
+ [>(true_min f b caseb (S n)) //
+ |>(false_min … caseb) #eqm #ltm @(Hind m (S b)) /2/
+ ]
+ ]
+qed.
+
+lemma min_exists: ∀f.∀t,m. m < t → f m = true →
+∀k,b.b ≤ m → (∀i. b ≤ i → i < m → f i = false) → t = k + b →
+ min k b f = m.
+#f #t #m #ltmt #fm #k (elim k)
+ [#b #lebm #ismin #eqtb @False_ind @(absurd … lebm) <eqtb
+ @lt_to_not_le //
+ |#d #Hind #b #lebm #ismin #eqt cases(le_to_or_lt_eq …lebm)
+ [#ltbm >(false_min …) /2/ @Hind //
+ [#i #H #H1 @ismin /2/ | >eqt normalize //]
+ |#eqbm >(true_min …) //
+ ]
+ ]
+qed.
+
+lemma min_not_exists: ∀f.∀n,b.
+ (∀i. b ≤ i → i < n + b → f i = false) → min n b f = n + b.
+#f #n (elim n) //
+#p #Hind #b #ffalse >(false_min …)
+ [>(Hind …) // #i #H #H1 @ffalse /2/
+ |@ffalse //
+ ]
+qed.
+
+lemma fmin_false: ∀f.∀n,b.let m ≝ min n b f in
+ f m = false → m = n+b.
+#f #n (elim n) //
+#i #Hind #b normalize cases(true_or_false … (f b)) #fb >fb
+normalize
+ [#eqm @False_ind @(absurd … fb) //
+ |>(plus_n_Sm …) @Hind]
+qed.
+
+inductive min_spec (n,b:nat) (f:nat→bool) : nat→Prop ≝
+ | found : ∀m:nat. b ≤ m → m < n + b → f m =true →
+ (∀i. b ≤ i → i < m → f i = false) → min_spec n b f m
+ | not_found: (∀i.b ≤ i → i < (n + b) → f i = false) → min_spec n b f (n+b).
+
+theorem min_spec_to_min: ∀f.∀n,b,m.
+ min_spec n b f m → min n b f = m.
+#f #n #b #m #spec (cases spec)
+ [#m #lem #ltm #fm #ismin @(min_exists f (n+b)) // @ismin
+ |#ffalse @min_not_exists @ffalse
+ ]
+qed.
+
+theorem min_to_min_spec: ∀f.∀n,b,m.
+ min n b f = m → min_spec n b f m.
+#f #n #b #m (cases n)
+ [#eqm <eqm %2 #i #lei #lti @False_ind @(absurd … lti) /2/
+ |#n #eqm (* (cases (le_to_or_lt_eq … (le_min_r …))) Stack overflow! *)
+ lapply (le_min_r f (S n) b) >eqm #lem
+ (cases (le_to_or_lt_eq … lem)) #mcase
+ [%1 /2/ #i #H #H1 @(lt_min_to_false f (S n) i b) //
+ |>mcase %2 #i #lebi #lti @(lt_min_to_false f (S n) i b) //
+ ]
+ ]
+qed.
+
+theorem min_f_g: ∀f,g,n,b.(∀i. b ≤ i → i < n + b → f i = g i) →
+ min n b f = min n b g.
+#f #g #n (elim n) //
+#m #Hind #b #ext normalize >(ext b (le_n b) ?) // >(Hind …) //
+#i #ltib #ltim @ext /2/
+qed.
+
+theorem le_min_f_min_g: ∀f,g,n,b. (∀i. b ≤ i → i < n +b → f i = true → g i =true) →
+min n b g ≤ min n b f.
+#f #g #n (elim n) //
+#m #Hind #b #ext normalize (cases (true_or_false (f b))) #Heq >Heq
+ [>(ext b …) //
+ |(cases (g b)) normalize /2/ @Hind #i #ltb #ltim #fi
+ @ext /2/
+qed.
+
+theorem f_min_true : ∀ f.∀n,b.
+(∃i:nat. b ≤ i ∧ i < n ∧ 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 x ??) /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 "basics/relations.ma".
+
+inductive nat : Type[0] ≝
+ | O : nat
+ | S : nat → nat.
+
+interpretation "Natural numbers" 'N = nat.
+
+alias num (instance 0) = "natural number".
+
+definition pred ≝
+ λn. match n with [ O ⇒ O | S p ⇒ p].
+
+theorem pred_Sn : ∀n. n = pred (S n).
+// qed.
+
+theorem injective_S : injective nat nat S.
+// qed.
+
+(*
+theorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m.
+//. qed. *)
+
+theorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m.
+/2/ qed.
+
+definition not_zero: nat → Prop ≝
+ λn: nat. match n with [ O ⇒ False | (S p) ⇒ True ].
+
+theorem not_eq_O_S : ∀n:nat. O ≠ S n.
+#n @nmk #eqOS (change with (not_zero O)) >eqOS // qed.
+
+theorem not_eq_n_Sn: ∀n:nat. n ≠ S n.
+#n (elim n) /2/ qed.
+
+theorem nat_case:
+ ∀n:nat.∀P:nat → Prop.
+ (n=O → P O) → (∀m:nat. n= S m → P (S m)) → P n.
+#n #P (elim n) /2/ qed.
+
+theorem nat_elim2 :
+ ∀R:nat → nat → Prop.
+ (∀n:nat. R O n)
+ → (∀n:nat. R (S n) O)
+ → (∀n,m:nat. R n m → R (S n) (S m))
+ → ∀n,m:nat. R n m.
+#R #ROn #RSO #RSS #n (elim n) // #n0 #Rn0m #m (cases m) /2/ qed.
+
+theorem decidable_eq_nat : ∀n,m:nat.decidable (n=m).
+@nat_elim2 #n [ (cases n) /2/ | /3/ | #m #Hind (cases Hind) /3/]
+qed.
+
+(*************************** plus ******************************)
+
+let rec plus n m ≝
+ match n with [ O ⇒ m | S p ⇒ S (plus p m) ].
+
+interpretation "natural plus" 'plus x y = (plus x y).
+
+theorem plus_O_n: ∀n:nat. n = O+n.
+// qed.
+
+(*
+theorem plus_Sn_m: ∀n,m:nat. S (n + m) = S n + m.
+// qed.
+*)
+
+theorem plus_n_O: ∀n:nat. n = n+O.
+#n (elim n) normalize // qed.
+
+theorem plus_n_Sm : ∀n,m:nat. S (n+m) = n + S m.
+#n (elim n) normalize // qed.
+
+(*
+theorem plus_Sn_m1: ∀n,m:nat. S m + n = n + S m.
+#n (elim n) normalize // qed.
+*)
+
+(* deleterio?
+theorem plus_n_1 : ∀n:nat. S n = n+1.
+// qed.
+*)
+
+theorem commutative_plus: commutative ? plus.
+#n (elim n) normalize // qed.
+
+theorem associative_plus : associative nat plus.
+#n (elim n) normalize // qed.
+
+theorem assoc_plus1: ∀a,b,c. c + (b + a) = b + c + a.
+// qed.
+
+theorem injective_plus_r: ∀n:nat.injective nat nat (λm.n+m).
+#n (elim n) normalize /3/ qed.
+
+(* theorem inj_plus_r: \forall p,n,m:nat. p+n = p+m \to n=m
+\def injective_plus_r.
+
+theorem injective_plus_l: ∀m:nat.injective nat nat (λn.n+m).
+/2/ qed. *)
+
+(* theorem inj_plus_l: \forall p,n,m:nat. n+p = m+p \to n=m
+\def injective_plus_l. *)
+
+(*************************** times *****************************)
+
+let rec times n m ≝
+ match n with [ O ⇒ O | S p ⇒ m+(times p m) ].
+
+interpretation "natural times" 'times x y = (times x y).
+
+theorem times_Sn_m: ∀n,m:nat. m+n*m = S n*m.
+// qed.
+
+theorem times_O_n: ∀n:nat. O = O*n.
+// qed.
+
+theorem times_n_O: ∀n:nat. O = n*O.
+#n (elim n) // qed.
+
+theorem times_n_Sm : ∀n,m:nat. n+(n*m) = n*(S m).
+#n (elim n) normalize // qed.
+
+theorem commutative_times : commutative nat times.
+#n (elim n) normalize // qed.
+
+(* variant sym_times : \forall n,m:nat. n*m = m*n \def
+symmetric_times. *)
+
+theorem distributive_times_plus : distributive nat times plus.
+#n (elim n) normalize // qed.
+
+theorem distributive_times_plus_r :
+ ∀a,b,c:nat. (b+c)*a = b*a + c*a.
+// qed.
+
+theorem associative_times: associative nat times.
+#n (elim n) normalize // qed.
+
+lemma times_times: ∀x,y,z. x*(y*z) = y*(x*z).
+// qed.
+
+(* ci servono questi risultati?
+theorem times_O_to_O: ∀n,m:nat.n*m=O → n=O ∨ m=O.
+napply nat_elim2 /2/
+#n #m #H normalize #H1 napply False_ind napply not_eq_O_S
+// qed.
+
+theorem times_n_SO : ∀n:nat. n = n * S O.
+#n // qed.
+
+theorem times_SSO_n : ∀n:nat. n + n = (S(S O)) * n.
+normalize // qed.
+
+nlemma times_SSO: \forall n.(S(S O))*(S n) = S(S((S(S O))*n)).
+// qed.
+
+theorem or_eq_eq_S: \forall n.\exists m.
+n = (S(S O))*m \lor n = S ((S(S O))*m).
+#n (elim n)
+ ##[@ /2/
+ ##|#a #H nelim H #b#ornelim or#aeq
+ ##[@ b @ 2 //
+ ##|@ (S b) @ 1 /2/
+ ##]
+qed.
+*)
+
+(******************** ordering relations ************************)
+
+inductive le (n:nat) : nat → Prop ≝
+ | le_n : le n n
+ | le_S : ∀ m:nat. le n m → le n (S m).
+
+interpretation "natural 'less or equal to'" 'leq x y = (le x y).
+
+interpretation "natural 'neither less nor equal to'" 'nleq x y = (Not (le x y)).
+
+definition lt: nat → nat → Prop ≝ λn,m. S n ≤ m.
+
+interpretation "natural 'less than'" 'lt x y = (lt x y).
+interpretation "natural 'not less than'" 'nless x y = (Not (lt x y)).
+
+(* lemma eq_lt: ∀n,m. (n < m) = (S n ≤ m).
+// qed. *)
+
+definition ge: nat → nat → Prop ≝ λn,m.m ≤ n.
+
+interpretation "natural 'greater or equal to'" 'geq x y = (ge x y).
+
+definition gt: nat → nat → Prop ≝ λn,m.m<n.
+
+interpretation "natural 'greater than'" 'gt x y = (gt x y).
+interpretation "natural 'not greater than'" 'ngtr x y = (Not (gt x y)).
+
+theorem transitive_le : transitive nat le.
+#a #b #c #leab #lebc (elim lebc) /2/
+qed.
+
+(*
+theorem trans_le: \forall n,m,p:nat. n \leq m \to m \leq p \to n \leq p
+\def transitive_le. *)
+
+theorem transitive_lt: transitive nat lt.
+#a #b #c #ltab #ltbc (elim ltbc) /2/qed.
+
+(*
+theorem trans_lt: \forall n,m,p:nat. lt n m \to lt m p \to lt n p
+\def transitive_lt. *)
+
+theorem le_S_S: ∀n,m:nat. n ≤ m → S n ≤ S m.
+#n #m #lenm (elim lenm) /2/ qed.
+
+theorem le_O_n : ∀n:nat. O ≤ n.
+#n (elim n) /2/ qed.
+
+theorem le_n_Sn : ∀n:nat. n ≤ S n.
+/2/ qed.
+
+theorem le_pred_n : ∀n:nat. pred n ≤ n.
+#n (elim n) // qed.
+
+theorem monotonic_pred: monotonic ? le pred.
+#n #m #lenm (elim lenm) /2/ qed.
+
+theorem le_S_S_to_le: ∀n,m:nat. S n ≤ S m → n ≤ m.
+(* demo *)
+/2/ qed.
+
+(* this are instances of the le versions
+theorem lt_S_S_to_lt: ∀n,m. S n < S m → n < m.
+/2/ qed.
+
+theorem lt_to_lt_S_S: ∀n,m. n < m → S n < S m.
+/2/ qed. *)
+
+theorem lt_to_not_zero : ∀n,m:nat. n < m → not_zero m.
+#n #m #Hlt (elim Hlt) // qed.
+
+(* lt vs. le *)
+theorem not_le_Sn_O: ∀ n:nat. S n ≰ O.
+#n @nmk #Hlen0 @(lt_to_not_zero ?? Hlen0) qed.
+
+theorem not_le_to_not_le_S_S: ∀ n,m:nat. n ≰ m → S n ≰ S m.
+/3/ qed.
+
+theorem not_le_S_S_to_not_le: ∀ n,m:nat. S n ≰ S m → n ≰ m.
+/3/ qed.
+
+theorem decidable_le: ∀n,m. decidable (n≤m).
+@nat_elim2 #n /2/ #m * /3/ qed.
+
+theorem decidable_lt: ∀n,m. decidable (n < m).
+#n #m @decidable_le qed.
+
+theorem not_le_Sn_n: ∀n:nat. S n ≰ n.
+#n (elim n) /2/ qed.
+
+(* this is le_S_S_to_le
+theorem lt_S_to_le: ∀n,m:nat. n < S m → n ≤ m.
+/2/ qed.
+*)
+
+lemma le_gen: ∀P:nat → Prop.∀n.(∀i. i ≤ n → P i) → P n.
+/2/ qed.
+
+theorem not_le_to_lt: ∀n,m. n ≰ m → m < n.
+@nat_elim2 #n
+ [#abs @False_ind /2/
+ |/2/
+ |#m #Hind #HnotleSS @le_S_S /3/
+ ]
+qed.
+
+theorem lt_to_not_le: ∀n,m. n < m → m ≰ n.
+#n #m #Hltnm (elim Hltnm) /3/ qed.
+
+theorem not_lt_to_le: ∀n,m:nat. n ≮ m → m ≤ n.
+/4/ qed.
+
+theorem le_to_not_lt: ∀n,m:nat. n ≤ m → m ≮ n.
+#n #m #H @lt_to_not_le /2/ (* /3/ *) qed.
+
+(* lt and le trans *)
+
+theorem lt_to_le_to_lt: ∀n,m,p:nat. n < m → m ≤ p → n < p.
+#n #m #p #H #H1 (elim H1) /2/ qed.
+
+theorem le_to_lt_to_lt: ∀n,m,p:nat. n ≤ m → m < p → n < p.
+#n #m #p #H (elim H) /3/ qed.
+
+theorem lt_S_to_lt: ∀n,m. S n < m → n < m.
+/2/ qed.
+
+theorem ltn_to_ltO: ∀n,m:nat. n < m → O < m.
+/2/ qed.
+
+(*
+theorem lt_SO_n_to_lt_O_pred_n: \forall n:nat.
+(S O) \lt n \to O \lt (pred n).
+intros.
+apply (ltn_to_ltO (pred (S O)) (pred n) ?).
+ apply (lt_pred (S O) n)
+ [ apply (lt_O_S O)
+ | assumption
+ ]
+qed. *)
+
+theorem lt_O_n_elim: ∀n:nat. O < n →
+ ∀P:nat → Prop.(∀m:nat.P (S m)) → P n.
+#n (elim n) // #abs @False_ind /2/
+qed.
+
+(*
+theorem lt_pred: \forall n,m.
+ O < n \to n < m \to pred n < pred m.
+apply nat_elim2
+ [intros.apply False_ind.apply (not_le_Sn_O ? H)
+ |intros.apply False_ind.apply (not_le_Sn_O ? H1)
+ |intros.simplify.unfold.apply le_S_S_to_le.assumption
+ ]
+qed.
+
+theorem S_pred: \forall n:nat.lt O n \to eq nat n (S (pred n)).
+intro.elim n.apply False_ind.exact (not_le_Sn_O O H).
+apply eq_f.apply pred_Sn.
+qed.
+
+theorem le_pred_to_le:
+ ∀n,m. O < m → pred n ≤ pred m → n ≤ m.
+intros 2
+elim n
+[ apply le_O_n
+| simplify in H2
+ rewrite > (S_pred m)
+ [ apply le_S_S
+ assumption
+ | assumption
+ ]
+].
+qed.
+
+*)
+
+(* le to lt or eq *)
+theorem le_to_or_lt_eq: ∀n,m:nat. n ≤ m → n < m ∨ n = m.
+#n #m #lenm (elim lenm) /3/ qed.
+
+(* not eq *)
+theorem lt_to_not_eq : ∀n,m:nat. n < m → n ≠ m.
+#n #m #H @not_to_not /2/ qed.
+
+(*not lt
+theorem eq_to_not_lt: ∀a,b:nat. a = b → a ≮ b.
+intros.
+unfold Not.
+intros.
+rewrite > H in H1.
+apply (lt_to_not_eq b b)
+[ assumption
+| reflexivity
+]
+qed.
+
+theorem lt_n_m_to_not_lt_m_Sn: ∀n,m. n < m → m ≮ S n.
+intros
+unfold Not
+intro
+unfold lt in H
+unfold lt in H1
+generalize in match (le_S_S ? ? H)
+intro
+generalize in match (transitive_le ? ? ? H2 H1)
+intro
+apply (not_le_Sn_n ? H3).
+qed. *)
+
+theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n<m.
+#n #m #Hneq #Hle cases (le_to_or_lt_eq ?? Hle) //
+#Heq /3/ qed.
+(*
+nelim (Hneq Heq) qed. *)
+
+(* le elimination *)
+theorem le_n_O_to_eq : ∀n:nat. n ≤ O → O=n.
+#n (cases n) // #a #abs @False_ind /2/ qed.
+
+theorem le_n_O_elim: ∀n:nat. n ≤ O → ∀P: nat →Prop. P O → P n.
+#n (cases n) // #a #abs @False_ind /2/ qed.
+
+theorem le_n_Sm_elim : ∀n,m:nat.n ≤ S m →
+∀P:Prop. (S n ≤ S m → P) → (n=S m → P) → P.
+#n #m #Hle #P (elim Hle) /3/ qed.
+
+(* le and eq *)
+
+theorem le_to_le_to_eq: ∀n,m. n ≤ m → m ≤ n → n = m.
+@nat_elim2 /4/
+qed.
+
+theorem lt_O_S : ∀n:nat. O < S n.
+/2/ qed.
+
+(*
+(* other abstract properties *)
+theorem antisymmetric_le : antisymmetric nat le.
+unfold antisymmetric.intros 2.
+apply (nat_elim2 (\lambda n,m.(n \leq m \to m \leq n \to n=m))).
+intros.apply le_n_O_to_eq.assumption.
+intros.apply False_ind.apply (not_le_Sn_O ? H).
+intros.apply eq_f.apply H.
+apply le_S_S_to_le.assumption.
+apply le_S_S_to_le.assumption.
+qed.
+
+theorem antisym_le: \forall n,m:nat. n \leq m \to m \leq n \to n=m
+\def antisymmetric_le.
+
+theorem le_n_m_to_lt_m_Sn_to_eq_n_m: ∀n,m. n ≤ m → m < S n → n=m.
+intros
+unfold lt in H1
+generalize in match (le_S_S_to_le ? ? H1)
+intro
+apply antisym_le
+assumption.
+qed.
+*)
+
+(* well founded induction principles *)
+
+theorem nat_elim1 : ∀n:nat.∀P:nat → Prop.
+(∀m.(∀p. p < m → P p) → P m) → P n.
+#n #P #H
+cut (∀q:nat. q ≤ n → P q) /2/
+(elim n)
+ [#q #HleO (* applica male *)
+ @(le_n_O_elim ? HleO)
+ @H #p #ltpO @False_ind /2/ (* 3 *)
+ |#p #Hind #q #HleS
+ @H #a #lta @Hind @le_S_S_to_le /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.
+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.
+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.
+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.
+qed.
+*)
+
+(*********************** monotonicity ***************************)
+theorem monotonic_le_plus_r:
+∀n:nat.monotonic nat le (λm.n + m).
+#n #a #b (elim n) normalize //
+#m #H #leab @le_S_S /2/ qed.
+
+(*
+theorem le_plus_r: ∀p,n,m:nat. n ≤ m → p + n ≤ p + m
+≝ monotonic_le_plus_r. *)
+
+theorem monotonic_le_plus_l:
+∀m:nat.monotonic nat le (λn.n + m).
+/2/ qed.
+
+(*
+theorem le_plus_l: \forall p,n,m:nat. n \le m \to n + p \le m + p
+\def monotonic_le_plus_l. *)
+
+theorem le_plus: ∀n1,n2,m1,m2:nat. n1 ≤ n2 → m1 ≤ m2
+→ n1 + m1 ≤ n2 + m2.
+#n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1+m2))
+/2/ qed.
+
+theorem le_plus_n :∀n,m:nat. m ≤ n + m.
+/2/ qed.
+
+lemma le_plus_a: ∀a,n,m. n ≤ m → n ≤ a + m.
+/2/ qed.
+
+lemma le_plus_b: ∀b,n,m. n + b ≤ m → n ≤ m.
+/2/ qed.
+
+theorem le_plus_n_r :∀n,m:nat. m ≤ m + n.
+/2/ qed.
+
+theorem eq_plus_to_le: ∀n,m,p:nat.n=m+p → m ≤ n.
+// qed.
+
+theorem le_plus_to_le: ∀a,n,m. a + n ≤ a + m → n ≤ m.
+#a (elim a) normalize /3/ qed.
+
+theorem le_plus_to_le_r: ∀a,n,m. n + a ≤ m +a → n ≤ m.
+/2/ qed.
+
+(* plus & lt *)
+
+theorem monotonic_lt_plus_r:
+∀n:nat.monotonic nat lt (λm.n+m).
+/2/ qed.
+
+(*
+variant lt_plus_r: \forall n,p,q:nat. p < q \to n + p < n + q \def
+monotonic_lt_plus_r. *)
+
+theorem monotonic_lt_plus_l:
+∀n:nat.monotonic nat lt (λm.m+n).
+/2/ qed.
+
+(*
+variant lt_plus_l: \forall n,p,q:nat. p < q \to p + n < q + n \def
+monotonic_lt_plus_l. *)
+
+theorem lt_plus: ∀n,m,p,q:nat. n < m → p < q → n + p < m + q.
+#n #m #p #q #ltnm #ltpq
+@(transitive_lt ? (n+q))/2/ qed.
+
+theorem lt_plus_to_lt_l :∀n,p,q:nat. p+n < q+n → p<q.
+/2/ qed.
+
+theorem lt_plus_to_lt_r :∀n,p,q:nat. n+p < n+q → p<q.
+/2/ qed.
+
+(*
+theorem le_to_lt_to_lt_plus: ∀a,b,c,d:nat.
+a ≤ c → b < d → a + b < c+d.
+(* bello /2/ un po' lento *)
+#a #b #c #d #leac #lebd
+normalize napplyS le_plus // qed.
+*)
+
+(* times *)
+theorem monotonic_le_times_r:
+∀n:nat.monotonic nat le (λm. n * m).
+#n #x #y #lexy (elim n) normalize//(* lento /2/*)
+#a #lea @le_plus //
+qed.
+
+(*
+theorem le_times_r: \forall p,n,m:nat. n \le m \to p*n \le p*m
+\def monotonic_le_times_r. *)
+
+(*
+theorem monotonic_le_times_l:
+∀m:nat.monotonic nat le (λn.n*m).
+/2/ qed.
+*)
+
+(*
+theorem le_times_l: \forall p,n,m:nat. n \le m \to n*p \le m*p
+\def monotonic_le_times_l. *)
+
+theorem le_times: ∀n1,n2,m1,m2:nat.
+n1 ≤ n2 → m1 ≤ m2 → n1*m1 ≤ n2*m2.
+#n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1*m2)) /2/
+qed.
+
+(* interessante *)
+theorem lt_times_n: ∀n,m:nat. O < n → m ≤ n*m.
+#n #m #H /2/ qed.
+
+theorem le_times_to_le:
+∀a,n,m. O < a → a * n ≤ a * m → n ≤ m.
+#a @nat_elim2 normalize
+ [//
+ |#n #H1 #H2
+ @(transitive_le ? (a*S n)) /2/
+ |#n #m #H #lta #le
+ @le_S_S @H /2/
+ ]
+qed.
+
+(*
+theorem le_S_times_2: ∀n,m.O < m → n ≤ m → S n ≤ 2*m.
+#n #m #posm #lenm (* interessante *)
+applyS (le_plus n m) // qed. *)
+
+(* times & lt *)
+(*
+theorem lt_O_times_S_S: ∀n,m:nat.O < (S n)*(S m).
+intros.simplify.unfold lt.apply le_S_S.apply le_O_n.
+qed. *)
+
+(*
+theorem lt_times_eq_O: \forall a,b:nat.
+O < a → a * b = O → b = O.
+intros.
+apply (nat_case1 b)
+[ intros.
+ reflexivity
+| intros.
+ rewrite > H2 in H1.
+ rewrite > (S_pred a) in H1
+ [ apply False_ind.
+ apply (eq_to_not_lt O ((S (pred a))*(S m)))
+ [ apply sym_eq.
+ assumption
+ | apply lt_O_times_S_S
+ ]
+ | assumption
+ ]
+]
+qed.
+
+theorem O_lt_times_to_O_lt: \forall a,c:nat.
+O \lt (a * c) \to O \lt a.
+intros.
+apply (nat_case1 a)
+[ intros.
+ rewrite > H1 in H.
+ simplify in H.
+ assumption
+| intros.
+ apply lt_O_S
+]
+qed.
+
+lemma lt_times_to_lt_O: \forall i,n,m:nat. i < n*m \to O < m.
+intros.
+elim (le_to_or_lt_eq O ? (le_O_n m))
+ [assumption
+ |apply False_ind.
+ rewrite < H1 in H.
+ rewrite < times_n_O in H.
+ apply (not_le_Sn_O ? H)
+ ]
+qed. *)
+
+(*
+theorem monotonic_lt_times_r:
+∀n:nat.monotonic nat lt (λm.(S n)*m).
+/2/
+simplify.
+intros.elim n.
+simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption.
+apply lt_plus.assumption.assumption.
+qed. *)
+
+theorem monotonic_lt_times_l:
+ ∀c:nat. O < c → monotonic nat lt (λt.(t*c)).
+#c #posc #n #m #ltnm
+(elim ltnm) normalize
+ [/2/
+ |#a #_ #lt1 @(transitive_le … lt1) //
+ ]
+qed.
+
+theorem monotonic_lt_times_r:
+ ∀c:nat. O < c → monotonic nat lt (λt.(c*t)).
+/2/ qed.
+
+theorem lt_to_le_to_lt_times:
+∀n,m,p,q:nat. n < m → p ≤ q → O < q → n*p < m*q.
+#n #m #p #q #ltnm #lepq #posq
+@(le_to_lt_to_lt ? (n*q))
+ [@monotonic_le_times_r //
+ |@monotonic_lt_times_l //
+ ]
+qed.
+
+theorem lt_times:∀n,m,p,q:nat. n<m → p<q → n*p < m*q.
+#n #m #p #q #ltnm #ltpq @lt_to_le_to_lt_times/2/
+qed.
+
+theorem lt_times_n_to_lt_l:
+∀n,p,q:nat. p*n < q*n → p < q.
+#n #p #q #Hlt (elim (decidable_lt p q)) //
+#nltpq @False_ind @(absurd ? ? (lt_to_not_le ? ? Hlt))
+applyS monotonic_le_times_r /2/
+qed.
+
+theorem lt_times_n_to_lt_r:
+∀n,p,q:nat. n*p < n*q → p < q.
+/2/ qed.
+
+(*
+theorem nat_compare_times_l : \forall n,p,q:nat.
+nat_compare p q = nat_compare ((S n) * p) ((S n) * q).
+intros.apply nat_compare_elim.intro.
+apply nat_compare_elim.
+intro.reflexivity.
+intro.absurd (p=q).
+apply (inj_times_r n).assumption.
+apply lt_to_not_eq. assumption.
+intro.absurd (q<p).
+apply (lt_times_to_lt_r n).assumption.
+apply le_to_not_lt.apply lt_to_le.assumption.
+intro.rewrite < H.rewrite > nat_compare_n_n.reflexivity.
+intro.apply nat_compare_elim.intro.
+absurd (p<q).
+apply (lt_times_to_lt_r n).assumption.
+apply le_to_not_lt.apply lt_to_le.assumption.
+intro.absurd (q=p).
+symmetry.
+apply (inj_times_r n).assumption.
+apply lt_to_not_eq.assumption.
+intro.reflexivity.
+qed. *)
+
+(* times and plus
+theorem lt_times_plus_times: \forall a,b,n,m:nat.
+a < n \to b < m \to a*m + b < n*m.
+intros 3.
+apply (nat_case n)
+ [intros.apply False_ind.apply (not_le_Sn_O ? H)
+ |intros.simplify.
+ rewrite < sym_plus.
+ unfold.
+ change with (S b+a*m1 \leq m1+m*m1).
+ apply le_plus
+ [assumption
+ |apply le_times
+ [apply le_S_S_to_le.assumption
+ |apply le_n
+ ]
+ ]
+ ]
+qed. *)
+
+(************************** minus ******************************)
+
+let rec minus n m ≝
+ match n with
+ [ O ⇒ O
+ | S p ⇒
+ match m with
+ [ O ⇒ S p
+ | S q ⇒ minus p q ]].
+
+interpretation "natural minus" 'minus x y = (minus x y).
+
+theorem minus_S_S: ∀n,m:nat.S n - S m = n -m.
+// qed.
+
+theorem minus_O_n: ∀n:nat.O=O-n.
+#n (cases n) // qed.
+
+theorem minus_n_O: ∀n:nat.n=n-O.
+#n (cases n) // qed.
+
+theorem minus_n_n: ∀n:nat.O=n-n.
+#n (elim n) // qed.
+
+theorem minus_Sn_n: ∀n:nat. S O = (S n)-n.
+#n (elim n) normalize // qed.
+
+theorem minus_Sn_m: ∀m,n:nat. m ≤ n → S n -m = S (n-m).
+(* qualcosa da capire qui
+#n #m #lenm nelim lenm napplyS refl_eq. *)
+@nat_elim2
+ [//
+ |#n #abs @False_ind /2/
+ |#n #m #Hind #c applyS Hind /2/
+ ]
+qed.
+
+(*
+theorem not_eq_to_le_to_le_minus:
+ ∀n,m.n ≠ m → n ≤ m → n ≤ m - 1.
+#n * #m (cases m// #m normalize
+#H #H1 napply le_S_S_to_le
+napplyS (not_eq_to_le_to_lt n (S m) H H1)
+qed. *)
+
+theorem eq_minus_S_pred: ∀n,m. n - (S m) = pred(n -m).
+@nat_elim2 normalize // qed.
+
+theorem plus_minus:
+∀m,n,p:nat. m ≤ n → (n-m)+p = (n+p)-m.
+@nat_elim2
+ [//
+ |#n #p #abs @False_ind /2/
+ |normalize/3/
+ ]
+qed.
+
+theorem minus_plus_m_m: ∀n,m:nat.n = (n+m)-m.
+/2/ qed.
+
+theorem plus_minus_m_m: ∀n,m:nat.
+ m ≤ n → n = (n-m)+m.
+#n #m #lemn @sym_eq /2/ qed.
+
+theorem le_plus_minus_m_m: ∀n,m:nat. n ≤ (n-m)+m.
+#n (elim n) // #a #Hind #m (cases m) // normalize #n/2/
+qed.
+
+theorem minus_to_plus :∀n,m,p:nat.
+ m ≤ n → n-m = p → n = m+p.
+#n #m #p #lemn #eqp (applyS plus_minus_m_m) //
+qed.
+
+theorem plus_to_minus :∀n,m,p:nat.n = m+p → n-m = p.
+#n #m #p #eqp @sym_eq (applyS (minus_plus_m_m p m))
+qed.
+
+theorem minus_pred_pred : ∀n,m:nat. O < n → O < m →
+pred n - pred m = n - m.
+#n #m #posn #posm @(lt_O_n_elim n posn) @(lt_O_n_elim m posm) //.
+qed.
+
+(*
+
+theorem le_SO_minus: \forall n,m:nat.S n \leq m \to S O \leq m-n.
+intros.elim H.elim (minus_Sn_n n).apply le_n.
+rewrite > minus_Sn_m.
+apply le_S.assumption.
+apply lt_to_le.assumption.
+qed.
+
+theorem minus_le_S_minus_S: \forall n,m:nat. m-n \leq S (m-(S n)).
+intros.
+apply (nat_elim2 (\lambda n,m.m-n \leq S (m-(S n)))).
+intro.elim n1.simplify.apply le_n_Sn.
+simplify.rewrite < minus_n_O.apply le_n.
+intros.simplify.apply le_n_Sn.
+intros.simplify.apply H.
+qed.
+
+theorem lt_minus_S_n_to_le_minus_n : \forall n,m,p:nat. m-(S n) < p \to m-n \leq p.
+intros 3.intro.
+(* autobatch *)
+(* end auto($Revision: 9739 $) proof: TIME=1.33 SIZE=100 DEPTH=100 *)
+apply (trans_le (m-n) (S (m-(S n))) p).
+apply minus_le_S_minus_S.
+assumption.
+qed.
+
+theorem le_minus_m: \forall n,m:nat. n-m \leq n.
+intros.apply (nat_elim2 (\lambda m,n. n-m \leq n)).
+intros.rewrite < minus_n_O.apply le_n.
+intros.simplify.apply le_n.
+intros.simplify.apply le_S.assumption.
+qed.
+
+theorem lt_minus_m: \forall n,m:nat. O < n \to O < m \to n-m \lt n.
+intros.apply (lt_O_n_elim n H).intro.
+apply (lt_O_n_elim m H1).intro.
+simplify.unfold lt.apply le_S_S.apply le_minus_m.
+qed.
+
+theorem minus_le_O_to_le: \forall n,m:nat. n-m \leq O \to n \leq m.
+intros 2.
+apply (nat_elim2 (\lambda n,m:nat.n-m \leq O \to n \leq m)).
+intros.apply le_O_n.
+simplify.intros. assumption.
+simplify.intros.apply le_S_S.apply H.assumption.
+qed.
+*)
+
+(* monotonicity and galois *)
+
+theorem monotonic_le_minus_l:
+∀p,q,n:nat. q ≤ p → q-n ≤ p-n.
+@nat_elim2 #p #q
+ [#lePO @(le_n_O_elim ? lePO) //
+ |//
+ |#Hind #n (cases n) // #a #leSS @Hind /2/
+ ]
+qed.
+
+theorem le_minus_to_plus: ∀n,m,p. n-m ≤ p → n≤ p+m.
+#n #m #p #lep @transitive_le
+ [|@le_plus_minus_m_m | @monotonic_le_plus_l // ]
+qed.
+
+theorem le_plus_to_minus: ∀n,m,p. n ≤ p+m → n-m ≤ p.
+#n #m #p #lep /2/ qed.
+
+theorem monotonic_le_minus_r:
+∀p,q,n:nat. q ≤ p → n-p ≤ n-q.
+#p #q #n #lepq @le_plus_to_minus
+@(transitive_le … (le_plus_minus_m_m ? q)) /2/
+qed.
+
+theorem eq_minus_O: ∀n,m:nat.
+ n ≤ m → n-m = O.
+#n #m #lenm @(le_n_O_elim (n-m)) /2/
+qed.
+
+theorem distributive_times_minus: distributive ? times minus.
+#a #b #c
+(cases (decidable_lt b c)) #Hbc
+ [>(eq_minus_O …) /2/ >(eq_minus_O …) //
+ @monotonic_le_times_r /2/
+ |@sym_eq (applyS plus_to_minus) <(distributive_times_plus …)
+ (* STRANO *)
+ @(eq_f …b) (applyS plus_minus_m_m) /2/
+qed.
+
+(*********************** boolean arithmetics ********************)
+include "basics/bool.ma".
+
+let rec eqb n m ≝
+match n with
+ [ O ⇒ match m with [ O ⇒ true | S q ⇒ false]
+ | S p ⇒ match m with [ O ⇒ false | S q ⇒ eqb p q]
+ ].
+
+theorem eqb_elim : ∀ n,m:nat.∀ P:bool → Prop.
+(n=m → (P true)) → (n ≠ m → (P false)) → (P (eqb n m)).
+@nat_elim2
+ [#n (cases n) normalize /3/
+ |normalize /3/
+ |normalize /4/
+ ]
+qed.
+
+theorem eqb_n_n: ∀n. eqb n n = true.
+#n (elim n) normalize // qed.
+
+theorem eqb_true_to_eq: ∀n,m:nat. eqb n m = true → n = m.
+#n #m @(eqb_elim n m) // #_ #abs @False_ind /2/ qed.
+
+theorem eqb_false_to_not_eq: ∀n,m:nat. eqb n m = false → n ≠ m.
+#n #m @(eqb_elim n m) /2/ qed.
+
+theorem eq_to_eqb_true: ∀n,m:nat.n = m → eqb n m = true.
+// qed.
+
+theorem not_eq_to_eqb_false: ∀n,m:nat.
+ n ≠ m → eqb n m = false.
+#n #m #noteq @eqb_elim// #Heq @False_ind /2/ qed.
+
+let rec leb n m ≝
+match n with
+ [ O ⇒ true
+ | (S p) ⇒
+ match m with
+ [ O ⇒ false
+ | (S q) ⇒ leb p q]].
+
+theorem leb_elim: ∀n,m:nat. ∀P:bool → Prop.
+(n ≤ m → P true) → (n ≰ m → P false) → P (leb n m).
+@nat_elim2 normalize
+ [/2/
+ |/3/
+ |#n #m #Hind #P #Pt #Pf @Hind
+ [#lenm @Pt @le_S_S // |#nlenm @Pf /2/ ]
+ ]
+qed.
+
+theorem leb_true_to_le:∀n,m.leb n m = true → n ≤ m.
+#n #m @leb_elim // #_ #abs @False_ind /2/ qed.
+
+theorem leb_false_to_not_le:∀n,m.
+ leb n m = false → n ≰ m.
+#n #m @leb_elim // #_ #abs @False_ind /2/ qed.
+
+theorem le_to_leb_true: ∀n,m. n ≤ m → leb n m = true.
+#n #m @leb_elim // #H #H1 @False_ind /2/ qed.
+
+theorem not_le_to_leb_false: ∀n,m. n ≰ m → leb n m = false.
+#n #m @leb_elim // #H #H1 @False_ind /2/ qed.
+
+theorem lt_to_leb_false: ∀n,m. m < n → leb n m = false.
+/3/ qed.
+
+(* serve anche ltb?
+ndefinition ltb ≝λn,m. leb (S n) m.
+
+theorem ltb_elim: ∀n,m:nat. ∀P:bool → Prop.
+(n < m → P true) → (n ≮ m → P false) → P (ltb n m).
+#n #m #P #Hlt #Hnlt
+napply leb_elim /3/ qed.
+
+theorem ltb_true_to_lt:∀n,m.ltb n m = true → n < m.
+#n #m #Hltb napply leb_true_to_le nassumption
+qed.
+
+theorem ltb_false_to_not_lt:∀n,m.
+ ltb n m = false → n ≮ m.
+#n #m #Hltb napply leb_false_to_not_le nassumption
+qed.
+
+theorem lt_to_ltb_true: ∀n,m. n < m → ltb n m = true.
+#n #m #Hltb napply le_to_leb_true nassumption
+qed.
+
+theorem le_to_ltb_false: ∀n,m. m \le n → ltb n m = false.
+#n #m #Hltb napply lt_to_leb_false /2/
+qed. *)
+
+(* min e max *)
+definition min: nat →nat →nat ≝
+λn.λm. if_then_else ? (leb n m) n m.
+
+definition max: nat →nat →nat ≝
+λn.λm. if_then_else ? (leb n m) m n.
+
+lemma commutative_min: commutative ? min.
+#n #m normalize @leb_elim
+ [@leb_elim normalize /2/
+ |#notle >(le_to_leb_true …) // @(transitive_le ? (S m)) /2/
+ ] qed.
+
+lemma le_minr: ∀i,n,m. i ≤ min n m → i ≤ m.
+#i #n #m normalize @leb_elim normalize /2/ qed.
+
+lemma le_minl: ∀i,n,m. i ≤ min n m → i ≤ n.
+/2/ qed.
+
+lemma to_min: ∀i,n,m. i ≤ n → i ≤ m → i ≤ min n m.
+#i #n #m #lein #leim normalize (cases (leb n m))
+normalize // qed.
+
+lemma commutative_max: commutative ? max.
+#n #m normalize @leb_elim
+ [@leb_elim normalize /2/
+ |#notle >(le_to_leb_true …) // @(transitive_le ? (S m)) /2/
+ ] qed.
+
+lemma le_maxl: ∀i,n,m. max n m ≤ i → n ≤ i.
+#i #n #m normalize @leb_elim normalize /2/ qed.
+
+lemma le_maxr: ∀i,n,m. max n m ≤ i → m ≤ i.
+/2/ qed.
+
+lemma to_max: ∀i,n,m. n ≤ i → m ≤ i → max n m ≤ i.
+#i #n #m #leni #lemi normalize (cases (leb n m))
+normalize // qed.
+
projects / helm.git / commitdiff