theorem injective_pp : injective nat fraction pp.
simplify.intros.
-change with (aux (pp x)) = (aux (pp y)).
+change with ((aux (pp x)) = (aux (pp y))).
apply eq_f.assumption.
qed.
theorem injective_nn : injective nat fraction nn.
simplify.intros.
-change with (aux (nn x)) = (aux (nn y)).
+change with ((aux (nn x)) = (aux (nn y))).
apply eq_f.assumption.
qed.
theorem eq_cons_to_eq1: \forall f,g:fraction.\forall x,y:Z.
(cons x f) = (cons y g) \to x = y.
intros.
-change with (fhd (cons x f)) = (fhd (cons y g)).
+change with ((fhd (cons x f)) = (fhd (cons y g))).
apply eq_f.assumption.
qed.
theorem eq_cons_to_eq2: \forall x,y:Z.\forall f,g:fraction.
(cons x f) = (cons y g) \to f = g.
intros.
-change with (ftl (cons x f)) = (ftl (cons y g)).
+change with ((ftl (cons x f)) = (ftl (cons y g))).
apply eq_f.assumption.
qed.
theorem decidable_eq_fraction: \forall f,g:fraction.
decidable (f = g).
intros.simplify.
-apply fraction_elim2 (\lambda f,g. f=g \lor (f=g \to False)).
+apply (fraction_elim2 (\lambda f,g. f=g \lor (f=g \to False))).
intros.elim g1.
elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False)).
left.apply eq_f. assumption.
right.apply not_eq_pp_nn.
right.apply not_eq_pp_cons.
intros. elim g1.
- right.intro.apply not_eq_pp_nn n1 n.apply sym_eq. assumption.
+ right.intro.apply (not_eq_pp_nn n1 n).apply sym_eq. assumption.
elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False)).
left. apply eq_f. assumption.
right.intro.apply H.apply injective_nn.assumption.
right.apply not_eq_nn_cons.
- intros.right.intro.apply not_eq_pp_cons m x f1.apply sym_eq.assumption.
- intros.right.intro.apply not_eq_nn_cons m x f1.apply sym_eq.assumption.
+ intros.right.intro.apply (not_eq_pp_cons m x f1).apply sym_eq.assumption.
+ intros.right.intro.apply (not_eq_nn_cons m x f1).apply sym_eq.assumption.
intros.elim H.
elim ((decidable_eq_Z x y) : x=y \lor (x=y \to False)).
left.apply eq_f2.assumption.
assumption.
- right.intro.apply H2.apply eq_cons_to_eq1 f1 g1.assumption.
- right.intro.apply H1.apply eq_cons_to_eq2 x y f1 g1.assumption.
+ right.intro.apply H2.apply (eq_cons_to_eq1 f1 g1).assumption.
+ right.intro.apply H1.apply (eq_cons_to_eq2 x y f1 g1).assumption.
qed.
theorem eqfb_to_Prop: \forall f,g:fraction.
match (eqfb f g) with
[true \Rightarrow f=g
|false \Rightarrow f \neq g].
-intros.apply fraction_elim2
+intros.apply (fraction_elim2
(\lambda f,g.match (eqfb f g) with
[true \Rightarrow f=g
-|false \Rightarrow f \neq g]).
+|false \Rightarrow f \neq g])).
intros.elim g1.
simplify.apply eqb_elim.
intro.simplify.apply eq_f.assumption.
simplify.apply not_eq_pp_nn.
simplify.apply not_eq_pp_cons.
intros.elim g1.
- simplify.intro.apply not_eq_pp_nn n1 n.apply sym_eq. assumption.
+ simplify.intro.apply (not_eq_pp_nn n1 n).apply sym_eq. assumption.
simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption.
intro.simplify.intro.apply H.apply injective_nn.assumption.
simplify.apply not_eq_nn_cons.
- intros.simplify.intro.apply not_eq_pp_cons m x f1.apply sym_eq. assumption.
- intros.simplify.intro.apply not_eq_nn_cons m x f1.apply sym_eq. assumption.
+ intros.simplify.intro.apply (not_eq_pp_cons m x f1).apply sym_eq. assumption.
+ intros.simplify.intro.apply (not_eq_nn_cons m x f1).apply sym_eq. assumption.
intros.
change in match (eqfb (cons x f1) (cons y g1))
with (andb (eqZb x y) (eqfb f1 g1)).
intro.generalize in match H.elim (eqfb f1 g1).
simplify.apply eq_f2.assumption.
apply H2.
- simplify.intro.apply H2.apply eq_cons_to_eq2 x y.assumption.
- intro.simplify.intro.apply H1.apply eq_cons_to_eq1 f1 g1.assumption.
+ simplify.intro.apply H2.apply (eq_cons_to_eq2 x y).assumption.
+ intro.simplify.intro.apply H1.apply (eq_cons_to_eq1 f1 g1).assumption.
qed.
let rec finv f \def
| (frac h) \Rightarrow frac (cons (x + y) h)]]].
theorem symmetric2_ftimes: symmetric2 fraction ratio ftimes.
-simplify. intros.apply fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f).
+simplify. intros.apply (fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f)).
intros.elim g.
- change with Z_to_ratio (pos n + pos n1) = Z_to_ratio (pos n1 + pos n).
+ change with (Z_to_ratio (pos n + pos n1) = Z_to_ratio (pos n1 + pos n)).
apply eq_f.apply sym_Zplus.
- change with Z_to_ratio (pos n + neg n1) = Z_to_ratio (neg n1 + pos n).
+ change with (Z_to_ratio (pos n + neg n1) = Z_to_ratio (neg n1 + pos n)).
apply eq_f.apply sym_Zplus.
- change with frac (cons (pos n + z) f) = frac (cons (z + pos n) f).
+ change with (frac (cons (pos n + z) f) = frac (cons (z + pos n) f)).
rewrite < sym_Zplus.reflexivity.
intros.elim g.
- change with Z_to_ratio (neg n + pos n1) = Z_to_ratio (pos n1 + neg n).
+ change with (Z_to_ratio (neg n + pos n1) = Z_to_ratio (pos n1 + neg n)).
apply eq_f.apply sym_Zplus.
- change with Z_to_ratio (neg n + neg n1) = Z_to_ratio (neg n1 + neg n).
+ change with (Z_to_ratio (neg n + neg n1) = Z_to_ratio (neg n1 + neg n)).
apply eq_f.apply sym_Zplus.
- change with frac (cons (neg n + z) f) = frac (cons (z + neg n) f).
+ change with (frac (cons (neg n + z) f) = frac (cons (z + neg n) f)).
rewrite < sym_Zplus.reflexivity.
- intros.change with frac (cons (x1 + pos m) f) = frac (cons (pos m + x1) f).
+ intros.change with (frac (cons (x1 + pos m) f) = frac (cons (pos m + x1) f)).
rewrite < sym_Zplus.reflexivity.
- intros.change with frac (cons (x1 + neg m) f) = frac (cons (neg m + x1) f).
+ intros.change with (frac (cons (x1 + neg m) f) = frac (cons (neg m + x1) f)).
rewrite < sym_Zplus.reflexivity.
intros.
change with
- match ftimes f g with
+ (match ftimes f g with
[ one \Rightarrow Z_to_ratio (x1 + y1)
| (frac h) \Rightarrow frac (cons (x1 + y1) h)] =
match ftimes g f with
[ one \Rightarrow Z_to_ratio (y1 + x1)
- | (frac h) \Rightarrow frac (cons (y1 + x1) h)].
+ | (frac h) \Rightarrow frac (cons (y1 + x1) h)]).
rewrite < H.rewrite < sym_Zplus.reflexivity.
qed.
theorem ftimes_finv : \forall f:fraction. ftimes f (finv f) = one.
intro.elim f.
- change with Z_to_ratio (pos n + - (pos n)) = one.
+ change with (Z_to_ratio (pos n + - (pos n)) = one).
rewrite > Zplus_Zopp.reflexivity.
- change with Z_to_ratio (neg n + - (neg n)) = one.
+ change with (Z_to_ratio (neg n + - (neg n)) = one).
rewrite > Zplus_Zopp.reflexivity.
(* again: we would need something to help finding the right change *)
change with
- match ftimes f1 (finv f1) with
+ (match ftimes f1 (finv f1) with
[ one \Rightarrow Z_to_ratio (z + - z)
- | (frac h) \Rightarrow frac (cons (z + - z) h)] = one.
+ | (frac h) \Rightarrow frac (cons (z + - z) h)] = one).
rewrite > H.rewrite > Zplus_Zopp.reflexivity.
qed.
| (frac g) \Rightarrow ftimes f g]].
theorem symmetric_rtimes : symmetric ratio rtimes.
-change with \forall r,s:ratio. rtimes r s = rtimes s r.
+change with (\forall r,s:ratio. rtimes r s = rtimes s r).
intros.
elim r. elim s.
reflexivity.
simplify.apply not_eq_OZ_pos.
simplify.apply not_eq_OZ_neg.
elim y.
- simplify.intro.apply not_eq_OZ_pos n.apply sym_eq.assumption.
+ simplify.intro.apply (not_eq_OZ_pos n).apply sym_eq.assumption.
simplify.apply eqb_elim.
intro.simplify.apply eq_f.assumption.
intro.simplify.intro.apply H.apply inj_pos.assumption.
simplify.apply not_eq_pos_neg.
elim y.
- simplify.intro.apply not_eq_OZ_neg n.apply sym_eq.assumption.
- simplify.intro.apply not_eq_pos_neg n1 n.apply sym_eq.assumption.
+ simplify.intro.apply (not_eq_OZ_neg n).apply sym_eq.assumption.
+ simplify.intro.apply (not_eq_pos_neg n1 n).apply sym_eq.assumption.
simplify.apply eqb_elim.
intro.simplify.apply eq_f.assumption.
intro.simplify.intro.apply H.apply inj_neg.assumption.
(x=y \to (P true)) \to (x \neq y \to (P false)) \to P (eqZb x y).
intros.
cut
-match (eqZb x y) with
+(match (eqZb x y) with
[ true \Rightarrow x=y
-| false \Rightarrow x \neq y] \to P (eqZb x y).
+| false \Rightarrow x \neq y] \to P (eqZb x y)).
apply Hcut.
apply eqZb_to_Prop.
elim (eqZb).
-apply H H2.
-apply H1 H2.
+apply (H H2).
+apply (H1 H2).
qed.
definition Z_compare : Z \to Z \to compare \def
elim y.
simplify.exact I.
simplify.
- cut match (nat_compare n n1) with
+ cut (match (nat_compare n n1) with
[ LT \Rightarrow n<n1
| EQ \Rightarrow n=n1
| GT \Rightarrow n1<n] \to
match (nat_compare n n1) with
[ LT \Rightarrow (S n) \leq n1
| EQ \Rightarrow pos n = pos n1
- | GT \Rightarrow (S n1) \leq n].
+ | GT \Rightarrow (S n1) \leq n]).
apply Hcut.apply nat_compare_to_Prop.
elim (nat_compare n n1).
simplify.exact H.
simplify.exact I.
simplify.exact I.
simplify.
- cut match (nat_compare n1 n) with
+ cut (match (nat_compare n1 n) with
[ LT \Rightarrow n1<n
| EQ \Rightarrow n1=n
| GT \Rightarrow n<n1] \to
match (nat_compare n1 n) with
[ LT \Rightarrow (S n1) \leq n
| EQ \Rightarrow neg n = neg n1
- | GT \Rightarrow (S n) \leq n1].
+ | GT \Rightarrow (S n) \leq n1]).
apply Hcut. apply nat_compare_to_Prop.
elim (nat_compare n1 n).
simplify.exact H.
(cic:/matita/logic/connectives/Not.con (cic:/matita/Z/orders/Zlt.con x y)).
theorem irreflexive_Zlt: irreflexive Z Zlt.
-change with \forall x:Z. x < x \to False.
+change with (\forall x:Z. x < x \to False).
intro.elim x.exact H.
-cut neg n < neg n \to False.
+cut (neg n < neg n \to False).
apply Hcut.apply H.simplify.apply not_le_Sn_n.
-cut pos n < pos n \to False.
+cut (pos n < pos n \to False).
apply Hcut.apply H.simplify.apply not_le_Sn_n.
qed.
intros 2.
elim x.
(* goal: x=OZ *)
- cut OZ < y \to Zsucc OZ \leq y.
+ cut (OZ < y \to Zsucc OZ \leq y).
apply Hcut. assumption.
simplify.elim y.
simplify.exact H1.
(* goal: x=pos *)
exact H.
(* goal: x=neg *)
- cut neg n < y \to Zsucc (neg n) \leq y.
+ cut (neg n < y \to Zsucc (neg n) \leq y).
apply Hcut. assumption.
elim n.
- cut neg O < y \to Zsucc (neg O) \leq y.
+ cut (neg O < y \to Zsucc (neg O) \leq y).
apply Hcut. assumption.
simplify.elim y.
simplify.exact I.
simplify.exact I.
- simplify.apply not_le_Sn_O n1 H2.
- cut neg (S n1) < y \to (Zsucc (neg (S n1))) \leq y.
+ simplify.apply (not_le_Sn_O n1 H2).
+ cut (neg (S n1) < y \to (Zsucc (neg (S n1))) \leq y).
apply Hcut. assumption.simplify.
elim y.
simplify.exact I.
simplify.exact I.
- simplify.apply le_S_S_to_le n2 n1 H3.
+ simplify.apply (le_S_S_to_le n2 n1 H3).
qed.
apply Zplus_pos_pos.
apply Zplus_pos_neg.
elim y.
- rewrite < sym_Zplus.rewrite < sym_Zplus (Zpred OZ).
+ rewrite < sym_Zplus.rewrite < (sym_Zplus (Zpred OZ)).
rewrite < Zpred_Zplus_neg_O.rewrite > Zpred_Zsucc.simplify.reflexivity.
apply Zplus_neg_pos.
rewrite < Zplus_neg_neg.reflexivity.
theorem Zplus_Zsucc_pos_neg:
\forall n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))).
intros.
-apply nat_elim2
-(\lambda n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m)))).intro.
+apply (nat_elim2
+(\lambda n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))))).intro.
intros.elim n1.
simplify. reflexivity.
elim n2.simplify. reflexivity.
theorem Zplus_Zsucc_neg_neg :
\forall n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m).
intros.
-apply nat_elim2
-(\lambda n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m)).intro.
+apply (nat_elim2
+(\lambda n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m))).intro.
intros.elim n1.
simplify. reflexivity.
elim n2.simplify. reflexivity.
theorem Zplus_Zsucc_neg_pos:
\forall n,m. Zsucc (neg n)+(pos m) = Zsucc ((neg n)+(pos m)).
intros.
-apply nat_elim2
-(\lambda n,m. Zsucc (neg n) + (pos m) = Zsucc (neg n + pos m)).
+apply (nat_elim2
+(\lambda n,m. Zsucc (neg n) + (pos m) = Zsucc (neg n + pos m))).
intros.elim n1.
simplify. reflexivity.
elim n2.simplify. reflexivity.
simplify.reflexivity.
rewrite < Zsucc_Zplus_pos_O.reflexivity.
elim y.
- rewrite < sym_Zplus OZ.reflexivity.
+ rewrite < (sym_Zplus OZ).reflexivity.
apply Zplus_Zsucc_pos_pos.
apply Zplus_Zsucc_pos_neg.
elim y.
- rewrite < sym_Zplus.rewrite < sym_Zplus OZ.simplify.reflexivity.
+ rewrite < sym_Zplus.rewrite < (sym_Zplus OZ).simplify.reflexivity.
apply Zplus_Zsucc_neg_pos.
apply Zplus_Zsucc_neg_neg.
qed.
theorem Zplus_Zpred: \forall x,y:Z. (Zpred x)+y = Zpred (x+y).
intros.
-cut Zpred (x+y) = Zpred ((Zsucc (Zpred x))+y).
+cut (Zpred (x+y) = Zpred ((Zsucc (Zpred x))+y)).
rewrite > Hcut.
rewrite > Zplus_Zsucc.
rewrite > Zpred_Zsucc.
theorem associative_Zplus: associative Z Zplus.
-change with \forall x,y,z:Z. (x + y) + z = x + (y + z).
+change with (\forall x,y,z:Z. (x + y) + z = x + (y + z)).
(* simplify. *)
intros.elim x.
simplify.reflexivity.
elim n.
rewrite < Zsucc_Zplus_pos_O.rewrite < Zsucc_Zplus_pos_O.
rewrite > Zplus_Zsucc.reflexivity.
- rewrite > Zplus_Zsucc (pos n1).rewrite > Zplus_Zsucc (pos n1).
- rewrite > Zplus_Zsucc ((pos n1)+y).apply eq_f.assumption.
+ rewrite > (Zplus_Zsucc (pos n1)).rewrite > (Zplus_Zsucc (pos n1)).
+ rewrite > (Zplus_Zsucc ((pos n1)+y)).apply eq_f.assumption.
elim n.
rewrite < (Zpred_Zplus_neg_O (y+z)).rewrite < (Zpred_Zplus_neg_O y).
rewrite < Zplus_Zpred.reflexivity.
- rewrite > Zplus_Zpred (neg n1).rewrite > Zplus_Zpred (neg n1).
- rewrite > Zplus_Zpred ((neg n1)+y).apply eq_f.assumption.
+ rewrite > (Zplus_Zpred (neg n1)).rewrite > (Zplus_Zpred (neg n1)).
+ rewrite > (Zplus_Zpred ((neg n1)+y)).apply eq_f.assumption.
qed.
variant assoc_Zplus : \forall x,y,z:Z. (x+y)+z = x+(y+z)
simplify.reflexivity.
qed.
theorem symmetric_Ztimes : symmetric Z Ztimes.
-change with \forall x,y:Z. x*y = y*x.
+change with (\forall x,y:Z. x*y = y*x).
intros.elim x.rewrite > Ztimes_z_OZ.reflexivity.
elim y.simplify.reflexivity.
-change with pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n))).
+change with (pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n)))).
rewrite < sym_times.reflexivity.
-change with neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n))).
+change with (neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n)))).
rewrite < sym_times.reflexivity.
elim y.simplify.reflexivity.
-change with neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n))).
+change with (neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n)))).
rewrite < sym_times.reflexivity.
-change with pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n))).
+change with (pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n)))).
rewrite < sym_times.reflexivity.
qed.
\def symmetric_Ztimes.
theorem associative_Ztimes: associative Z Ztimes.
-change with \forall x,y,z:Z. (x*y)*z = x*(y*z).
+change with (\forall x,y,z:Z. (x*y)*z = x*(y*z)).
intros.elim x.
simplify.reflexivity.
elim y.
elim z.
simplify.reflexivity.
change with
- pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
- pos (pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+ (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
change with
- neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
- neg (pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+ (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
elim z.
simplify.reflexivity.
change with
- neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
- neg (pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+ (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
change with
- pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
- pos(pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+ (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ pos(pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
elim y.
elim z.
simplify.reflexivity.
change with
- neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
- neg (pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+ (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
change with
- pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
- pos (pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+ (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
elim z.
simplify.reflexivity.
change with
- pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
- pos (pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+ (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
change with
- neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
- neg(pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+ (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ neg(pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
qed.
(pos n)*((neg p)+(pos q)) = (pos n)*(neg p)+ (pos n)*(pos q).
intros.
simplify.
-change in match p + n * (S p) with pred ((S n) * (S p)).
-change in match q + n * (S q) with pred ((S n) * (S q)).
+change in match p + n * (S p) with (pred ((S n) * (S p))).
+change in match q + n * (S q) with (pred ((S n) * (S q))).
rewrite < nat_compare_pred_pred.
rewrite < nat_compare_times_l.
rewrite < nat_compare_S_S.
-apply nat_compare_elim p q.
+apply (nat_compare_elim p q).
intro.
(* uff *)
-change with pos (pred ((S n) * (S (pred ((S q) - (S p)))))) =
- pos (pred ((pred ((S n) * (S q))) - (pred ((S n) * (S p))))).
-rewrite < times_minus1 n q p H.reflexivity.
+change with (pos (pred ((S n) * (S (pred ((S q) - (S p)))))) =
+ pos (pred ((pred ((S n) * (S q))) - (pred ((S n) * (S p)))))).
+rewrite < (times_minus1 n q p H).reflexivity.
intro.rewrite < H.simplify.reflexivity.
intro.
-change with neg (pred ((S n) * (S (pred ((S p) - (S q)))))) =
- neg (pred ((pred ((S n) * (S p))) - (pred ((S n) * (S q))))).
-rewrite < times_minus1 n p q H.reflexivity.
+change with (neg (pred ((S n) * (S (pred ((S p) - (S q)))))) =
+ neg (pred ((pred ((S n) * (S p))) - (pred ((S n) * (S q)))))).
+rewrite < (times_minus1 n p q H).reflexivity.
(* two more positivity conditions from nat_compare_pred_pred *)
apply lt_O_times_S_S.
apply lt_O_times_S_S.
lemma distributive2_Ztimes_pos_Zplus:
distributive2 nat Z (\lambda n,z. (pos n) * z) Zplus.
-change with \forall n,y,z.
-(pos n) * (y + z) = (pos n) * y + (pos n) * z.
+change with (\forall n,y,z.
+(pos n) * (y + z) = (pos n) * y + (pos n) * z).
intros.elim y.
reflexivity.
elim z.
reflexivity.
change with
- pos (pred ((S n) * ((S n1) + (S n2)))) =
- pos (pred ((S n) * (S n1) + (S n) * (S n2))).
+ (pos (pred ((S n) * ((S n1) + (S n2)))) =
+ pos (pred ((S n) * (S n1) + (S n) * (S n2)))).
rewrite < distr_times_plus.reflexivity.
apply Ztimes_Zplus_pos_pos_neg.
elim z.
reflexivity.
apply Ztimes_Zplus_pos_neg_pos.
change with
- neg (pred ((S n) * ((S n1) + (S n2)))) =
- neg (pred ((S n) * (S n1) + (S n) * (S n2))).
+ (neg (pred ((S n) * ((S n1) + (S n2)))) =
+ neg (pred ((S n) * (S n1) + (S n) * (S n2)))).
rewrite < distr_times_plus.reflexivity.
qed.
lemma distributive2_Ztimes_neg_Zplus :
distributive2 nat Z (\lambda n,z. (neg n) * z) Zplus.
-change with \forall n,y,z.
-(neg n) * (y + z) = (neg n) * y + (neg n) * z.
+change with (\forall n,y,z.
+(neg n) * (y + z) = (neg n) * y + (neg n) * z).
intros.
rewrite > Ztimes_neg_Zopp.
rewrite > distr_Ztimes_Zplus_pos.
distributive2_Ztimes_neg_Zplus.
theorem distributive_Ztimes_Zplus: distributive Z Ztimes Zplus.
-change with \forall x,y,z:Z. x * (y + z) = x*y + x*z.
+change with (\forall x,y,z:Z. x * (y + z) = x*y + x*z).
intros.elim x.
(* case x = OZ *)
simplify.reflexivity.
|false \Rightarrow z \neq OZ].
intros.elim z.
simplify.reflexivity.
-simplify.intros [H].
+simplify.intros (H).
discriminate H.
-simplify.intros [H].
+simplify.intros (H).
discriminate H.
qed.
theorem injective_pos: injective nat Z pos.
simplify.
intros.
-change with abs (pos x) = abs (pos y).
+change with (abs (pos x) = abs (pos y)).
apply eq_f.assumption.
qed.
theorem injective_neg: injective nat Z neg.
simplify.
intros.
-change with abs (neg x) = abs (neg y).
+change with (abs (neg x) = abs (neg y)).
apply eq_f.assumption.
qed.
\def injective_neg.
theorem not_eq_OZ_pos: \forall n:nat. OZ \neq pos n.
-simplify.intros [n; H].
+simplify.intros (n H).
discriminate H.
qed.
theorem not_eq_OZ_neg :\forall n:nat. OZ \neq neg n.
-simplify.intros [n; H].
+simplify.intros (n H).
discriminate H.
qed.
theorem not_eq_pos_neg :\forall n,m:nat. pos n \neq neg m.
-simplify.intros [n; m; H].
+simplify.intros (n m H).
discriminate H.
qed.
elim y.
(* goal: x=pos y=OZ *)
right.intro.
- apply not_eq_OZ_pos n. symmetry. assumption.
+ apply (not_eq_OZ_pos n). symmetry. assumption.
(* goal: x=pos y=pos *)
elim (decidable_eq_nat n n1:((n=n1) \lor ((n=n1) \to False))).
left.apply eq_f.assumption.
- right.intros [H_inj].apply H. injection H_inj. assumption.
+ right.intros (H_inj).apply H. injection H_inj. assumption.
(* goal: x=pos y=neg *)
- right.intro.apply not_eq_pos_neg n n1. assumption.
+ right.intro.apply (not_eq_pos_neg n n1). assumption.
(* goal: x=neg *)
elim y.
(* goal: x=neg y=OZ *)
right.intro.
- apply not_eq_OZ_neg n. symmetry. assumption.
+ apply (not_eq_OZ_neg n). symmetry. assumption.
(* goal: x=neg y=pos *)
- right. intro. apply not_eq_pos_neg n1 n. symmetry. assumption.
+ right. intro. apply (not_eq_pos_neg n1 n). symmetry. assumption.
(* goal: x=neg y=neg *)
elim (decidable_eq_nat n n1:((n=n1) \lor ((n=n1) \to False))).
left.apply eq_f.assumption.
theorem eq_elim_r:
\forall A:Type.\forall x:A. \forall P: A \to Prop.
P x \to \forall y:A. y=x \to P y.
-intros. elim sym_eq ? ? ? H1.assumption.
+intros. elim (sym_eq ? ? ? H1).assumption.
qed.
default "equality"
x1=x2 \to y1=y2 \to f x1 y1 = f x2 y2.
intros.elim H1.elim H.reflexivity.
qed.
+
+(*
+theorem a:\forall x.x=x\land True.
+[
+2:intros;
+ split;
+ [
+ exact (refl_eq Prop x);
+ |
+ exact I;
+ ]
+1:
+ skip
+]
+qed.
+*)
+
[ true \Rightarrow n = m
| false \Rightarrow n \neq m].
intros.
-apply nat_elim2
+apply (nat_elim2
(\lambda n,m:nat.match (eqb n m) with
[ true \Rightarrow n = m
-| false \Rightarrow n \neq m]).
+| false \Rightarrow n \neq m])).
intro.elim n1.
simplify.reflexivity.
simplify.apply not_eq_O_S.
intro.
simplify.
-intro. apply not_eq_O_S n1.apply sym_eq.assumption.
+intro. apply (not_eq_O_S n1).apply sym_eq.assumption.
intros.simplify.
generalize in match H.
-elim (eqb n1 m1).
+elim ((eqb n1 m1)).
simplify.apply eq_f.apply H1.
simplify.intro.apply H1.apply inj_S.assumption.
qed.
(n=m \to (P true)) \to (n \neq m \to (P false)) \to (P (eqb n m)).
intros.
cut
-match (eqb n m) with
+(match (eqb n m) with
[ true \Rightarrow n = m
-| false \Rightarrow n \neq m] \to (P (eqb n m)).
+| false \Rightarrow n \neq m] \to (P (eqb n m))).
apply Hcut.apply eqb_to_Prop.
-elim eqb n m.
-apply (H H2).
-apply (H1 H2).
+elim (eqb n m).
+apply ((H H2)).
+apply ((H1 H2)).
qed.
theorem eqb_n_n: \forall n. eqb n n = true.
theorem eq_to_eqb_true: \forall n,m:nat.
n = m \to eqb n m = true.
-intros.apply eqb_elim n m.
+intros.apply (eqb_elim n m).
intros. reflexivity.
-intros.apply False_ind.apply H1 H.
+intros.apply False_ind.apply (H1 H).
qed.
theorem not_eq_to_eqb_false: \forall n,m:nat.
\lnot (n = m) \to eqb n m = false.
-intros.apply eqb_elim n m.
-intros. apply False_ind.apply H H1.
+intros.apply (eqb_elim n m).
+intros. apply False_ind.apply (H H1).
intros.reflexivity.
qed.
[ true \Rightarrow n \leq m
| false \Rightarrow n \nleq m].
intros.
-apply nat_elim2
+apply (nat_elim2
(\lambda n,m:nat.match (leb n m) with
[ true \Rightarrow n \leq m
-| false \Rightarrow n \nleq m]).
+| false \Rightarrow n \nleq m])).
simplify.exact le_O_n.
simplify.exact not_le_Sn_O.
-intros 2.simplify.elim (leb n1 m1).
+intros 2.simplify.elim ((leb n1 m1)).
simplify.apply le_S_S.apply H.
simplify.intros.apply H.apply le_S_S_to_le.assumption.
qed.
P (leb n m).
intros.
cut
-match (leb n m) with
+(match (leb n m) with
[ true \Rightarrow n \leq m
-| false \Rightarrow n \nleq m] \to (P (leb n m)).
+| false \Rightarrow n \nleq m] \to (P (leb n m))).
apply Hcut.apply leb_to_Prop.
-elim leb n m.
-apply (H H2).
-apply (H1 H2).
+elim (leb n m).
+apply ((H H2)).
+apply ((H1 H2)).
qed.
let rec nat_compare n m: compare \def
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.
+intro.elim n.apply False_ind.exact (not_le_Sn_O O H).
apply eq_f.apply pred_Sn.
qed.
\forall n,m:nat.lt O n \to lt O m \to
eq compare (nat_compare n m) (nat_compare (pred n) (pred m)).
intros.
-apply lt_O_n_elim n H.
-apply lt_O_n_elim m H1.
+apply (lt_O_n_elim n H).
+apply (lt_O_n_elim m H1).
intros.
simplify.reflexivity.
qed.
| EQ \Rightarrow n=m
| GT \Rightarrow m < n ].
intros.
-apply nat_elim2 (\lambda n,m.match (nat_compare n m) with
+apply (nat_elim2 (\lambda n,m.match (nat_compare n m) with
[ LT \Rightarrow n < m
| EQ \Rightarrow n=m
- | GT \Rightarrow m < n ]).
+ | GT \Rightarrow m < n ])).
intro.elim n1.simplify.reflexivity.
simplify.apply le_S_S.apply le_O_n.
intro.simplify.apply le_S_S. apply le_O_n.
-intros 2.simplify.elim (nat_compare n1 m1).
+intros 2.simplify.elim ((nat_compare n1 m1)).
simplify. apply le_S_S.apply H.
simplify. apply eq_f. apply H.
simplify. apply le_S_S.apply H.
theorem nat_compare_n_m_m_n: \forall n,m:nat.
nat_compare n m = compare_invert (nat_compare m n).
intros.
-apply nat_elim2 (\lambda n,m. nat_compare n m = compare_invert (nat_compare m n)).
+apply (nat_elim2 (\lambda n,m. nat_compare n m = compare_invert (nat_compare m n))).
intros.elim n1.simplify.reflexivity.
simplify.reflexivity.
intro.elim n1.simplify.reflexivity.
(n < m \to P LT) \to (n=m \to P EQ) \to (m < n \to P GT) \to
(P (nat_compare n m)).
intros.
-cut match (nat_compare n m) with
+cut (match (nat_compare n m) with
[ LT \Rightarrow n < m
| EQ \Rightarrow n=m
| GT \Rightarrow m < n] \to
-(P (nat_compare n m)).
+(P (nat_compare n m))).
apply Hcut.apply nat_compare_to_Prop.
-elim (nat_compare n m).
-apply (H H3).
-apply (H1 H3).
-apply (H2 H3).
+elim ((nat_compare n m)).
+apply ((H H3)).
+apply ((H1 H3)).
+apply ((H2 H3)).
qed.
theorem transitive_congruent: \forall p:nat. transitive nat
(\lambda n,m. congruent n m p).
intros.unfold transitive.unfold congruent.intros.
-whd.apply trans_eq ? ? (y \mod p).
+whd.apply (trans_eq ? ? (y \mod p)).
apply H.apply H1.
qed.
theorem le_to_mod: \forall n,m:nat. n \lt m \to n = n \mod m.
intros.
-apply div_mod_spec_to_eq2 n m O n (n/m) (n \mod m).
+apply (div_mod_spec_to_eq2 n m O n (n/m) (n \mod m)).
constructor 1.assumption.simplify.reflexivity.
apply div_mod_spec_div_mod.
-apply le_to_lt_to_lt O n m.apply le_O_n.assumption.
+apply (le_to_lt_to_lt O n m).apply le_O_n.assumption.
qed.
theorem mod_mod : \forall n,p:nat. O<p \to n \mod p = (n \mod p) \mod p.
intros.
-rewrite > div_mod (n \mod p) p in \vdash (? ? % ?).
-rewrite > eq_div_O ? p.reflexivity.
+rewrite > (div_mod (n \mod p) p) in \vdash (? ? % ?).
+rewrite > (eq_div_O ? p).reflexivity.
(* uffa: hint non lo trova lt vs. le*)
apply lt_mod_m_m.
assumption.
theorem eq_times_plus_to_congruent: \forall n,m,p,r:nat. O< p \to
n = r*p+m \to congruent n m p.
intros.unfold congruent.
-apply div_mod_spec_to_eq2 n p (div n p) (mod n p) (r +(div m p)) (mod m p).
+apply (div_mod_spec_to_eq2 n p (div n p) (mod n p) (r +(div m p)) (mod m p)).
apply div_mod_spec_div_mod.assumption.
constructor 1.
apply lt_mod_m_m.assumption.
rewrite > sym_times.
rewrite > distr_times_plus.
rewrite > sym_times.
-rewrite > sym_times p.
+rewrite > (sym_times p).
rewrite > assoc_plus.
rewrite < div_mod.
assumption.assumption.
theorem divides_to_congruent: \forall n,m,p:nat. O < p \to m \le n \to
divides p (n - m) \to congruent n m p.
intros.elim H2.
-apply eq_times_plus_to_congruent n m p n2.
+apply (eq_times_plus_to_congruent n m p n2).
assumption.
rewrite < sym_plus.
apply minus_to_plus.assumption.
theorem congruent_to_divides: \forall n,m,p:nat.
O < p \to congruent n m p \to divides p (n - m).
intros.unfold congruent in H1.
-apply witness ? ? ((n / p)-(m / p)).
+apply (witness ? ? ((n / p)-(m / p))).
rewrite > sym_times.
-rewrite > div_mod n p in \vdash (? ? % ?).
-rewrite > div_mod m p in \vdash (? ? % ?).
-rewrite < sym_plus (m \mod p).
+rewrite > (div_mod n p) in \vdash (? ? % ?).
+rewrite > (div_mod m p) in \vdash (? ? % ?).
+rewrite < (sym_plus (m \mod p)).
rewrite < H1.
-rewrite < eq_minus_minus_minus_plus ? (n \mod p).
+rewrite < (eq_minus_minus_minus_plus ? (n \mod p)).
rewrite < minus_plus_m_m.
apply sym_eq.
apply times_minus_l.
theorem mod_times: \forall n,m,p:nat.
O < p \to mod (n*m) p = mod ((mod n p)*(mod m p)) p.
intros.
-change with congruent (n*m) ((mod n p)*(mod m p)) p.
-apply eq_times_plus_to_congruent ? ? p
-((n / p)*p*(m / p) + (n / p)*(m \mod p) + (n \mod p)*(m / p)).
+change with (congruent (n*m) ((mod n p)*(mod m p)) p).
+apply (eq_times_plus_to_congruent ? ? p
+((n / p)*p*(m / p) + (n / p)*(m \mod p) + (n \mod p)*(m / p))).
assumption.
-apply trans_eq ? ? (((n/p)*p+(n \mod p))*((m/p)*p+(m \mod p))).
+apply (trans_eq ? ? (((n/p)*p+(n \mod p))*((m/p)*p+(m \mod p)))).
apply eq_f2.
apply div_mod.assumption.
apply div_mod.assumption.
-apply 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)).
+apply (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))).
apply times_plus_plus.
apply eq_f2.
rewrite < assoc_times.
-rewrite > assoc_times (n/p) p (m \mod p).
-rewrite > sym_times p (m \mod p).
-rewrite < assoc_times (n/p) (m \mod p) p.
+rewrite > (assoc_times (n/p) p (m \mod p)).
+rewrite > (sym_times p (m \mod p)).
+rewrite < (assoc_times (n/p) (m \mod p) p).
rewrite < times_plus_l.
-rewrite < assoc_times (n \mod p).
+rewrite < (assoc_times (n \mod p)).
rewrite < times_plus_l.
apply eq_f2.
apply eq_f2.reflexivity.
congruent m m1 p \to congruent (n*m) (n1*m1) p.
unfold congruent.
intros.
-rewrite > mod_times n m p H.
+rewrite > (mod_times n m p H).
rewrite > H1.
rewrite > H2.
apply sym_eq.
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.change with congruent (f m) (f m \mod p) p.
+elim n.change with (congruent (f m) (f m \mod p) p).
apply congruent_n_mod_n.assumption.
-change with congruent ((f (S n1+m))*(pi n1 f m))
-(((f (S n1+m))\mod p)*(pi n1 (\lambda m.(f m) \mod p) m)) p.
+change with (congruent ((f (S n1+m))*(pi n1 f m))
+(((f (S n1+m))\mod p)*(pi n1 (\lambda m.(f m) \mod p) m)) p).
apply congruent_times.
assumption.
apply congruent_n_mod_n.assumption.
assumption.
-qed.
\ No newline at end of file
+qed.
theorem le_mod_aux_m_m:
\forall p,n,m. n \leq p \to (mod_aux p n m) \leq m.
intro.elim p.
-apply le_n_O_elim n H (\lambda n.(mod_aux O n m) \leq m).
+apply (le_n_O_elim n H (\lambda n.(mod_aux O n m) \leq m)).
simplify.apply le_O_n.
simplify.
-apply leb_elim n1 m.
+apply (leb_elim n1 m).
simplify.intro.assumption.
simplify.intro.apply H.
-cut n1 \leq (S n) \to n1-(S m) \leq n.
+cut (n1 \leq (S n) \to n1-(S m) \leq n).
apply Hcut.assumption.
elim n1.
simplify.apply le_O_n.
-simplify.apply trans_le ? n2 n.
+simplify.apply (trans_le ? n2 n).
apply le_minus_m.apply le_S_S_to_le.assumption.
qed.
theorem lt_mod_m_m: \forall n,m. O < m \to (n \mod m) < m.
intros 2.elim m.apply False_ind.
-apply not_le_Sn_O O H.
+apply (not_le_Sn_O O H).
simplify.apply le_S_S.apply le_mod_aux_m_m.
apply le_n.
qed.
theorem div_aux_mod_aux: \forall p,n,m:nat.
(n=(div_aux p n m)*(S m) + (mod_aux p n m)).
intro.elim p.
-simplify.elim leb n m.
+simplify.elim (leb n m).
simplify.apply refl_eq.
simplify.apply refl_eq.
simplify.
-apply leb_elim n1 m.
+apply (leb_elim n1 m).
simplify.intro.apply refl_eq.
simplify.intro.
rewrite > assoc_plus.
change with (n1=(S m)+(n1-(S m))).
rewrite < sym_plus.
apply plus_minus_m_m.
-change with m < n1.
+change with (m < n1).
apply not_le_to_lt.exact H1.
qed.
*)
theorem div_mod_spec_to_not_eq_O: \forall n,m,q,r.(div_mod_spec n m q r) \to m \neq O.
-intros 4.simplify.intros.elim H.absurd le (S r) O.
+intros 4.simplify.intros.elim H.absurd (le (S r) O).
rewrite < H1.assumption.
-exact not_le_Sn_O r.
+exact (not_le_Sn_O r).
qed.
theorem div_mod_spec_div_mod:
(div_mod_spec a b q r) \to (div_mod_spec a b q1 r1) \to
(eq nat q q1).
intros.elim H.elim H1.
-apply nat_compare_elim q q1.intro.
+apply (nat_compare_elim q q1).intro.
apply False_ind.
-cut eq nat ((q1-q)*b+r1) r.
-cut b \leq (q1-q)*b+r1.
-cut b \leq r.
-apply lt_to_not_le r b H2 Hcut2.
+cut (eq nat ((q1-q)*b+r1) r).
+cut (b \leq (q1-q)*b+r1).
+cut (b \leq r).
+apply (lt_to_not_le r b H2 Hcut2).
elim Hcut.assumption.
-apply trans_le ? ((q1-q)*b).
+apply (trans_le ? ((q1-q)*b)).
apply le_times_n.
apply le_SO_minus.exact H6.
rewrite < sym_plus.
(* the following case is symmetric *)
intro.
apply False_ind.
-cut eq nat ((q-q1)*b+r) r1.
-cut b \leq (q-q1)*b+r.
-cut b \leq r1.
-apply lt_to_not_le r1 b H4 Hcut2.
+cut (eq nat ((q-q1)*b+r) r1).
+cut (b \leq (q-q1)*b+r).
+cut (b \leq r1).
+apply (lt_to_not_le r1 b H4 Hcut2).
elim Hcut.assumption.
-apply trans_le ? ((q-q1)*b).
+apply (trans_le ? ((q-q1)*b)).
apply le_times_n.
apply le_SO_minus.exact H6.
rewrite < sym_plus.
(div_mod_spec a b q r) \to (div_mod_spec a b q1 r1) \to
(eq nat r r1).
intros.elim H.elim H1.
-apply inj_plus_r (q*b).
+apply (inj_plus_r (q*b)).
rewrite < H3.
-rewrite > div_mod_spec_to_eq a b q r q1 r1 H H1.
+rewrite > (div_mod_spec_to_eq a b q r q1 r1 H H1).
assumption.
qed.
(* some properties of div and mod *)
theorem div_times: \forall n,m:nat. ((S n)*m) / (S n) = m.
intros.
-apply div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O.
+apply (div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O).
goal 15. (* ?11 is closed with the following tactics *)
apply div_mod_spec_div_mod.
simplify.apply le_S_S.apply le_O_n.
theorem div_n_n: \forall n:nat. O < n \to n / n = S O.
intros.
-apply div_mod_spec_to_eq n n (n / n) (n \mod n) (S O) O.
+apply (div_mod_spec_to_eq n n (n / n) (n \mod n) (S O) O).
apply div_mod_spec_div_mod.assumption.
constructor 1.assumption.
rewrite < plus_n_O.simplify.rewrite < plus_n_O.reflexivity.
theorem eq_div_O: \forall n,m. n < m \to n / m = O.
intros.
-apply div_mod_spec_to_eq n m (n/m) (n \mod m) O n.
+apply (div_mod_spec_to_eq n m (n/m) (n \mod m) O n).
apply div_mod_spec_div_mod.
-apply le_to_lt_to_lt O n m.
+apply (le_to_lt_to_lt O n m).
apply le_O_n.assumption.
constructor 1.assumption.reflexivity.
qed.
theorem mod_n_n: \forall n:nat. O < n \to n \mod n = O.
intros.
-apply div_mod_spec_to_eq2 n n (n / n) (n \mod n) (S O) O.
+apply (div_mod_spec_to_eq2 n n (n / n) (n \mod n) (S O) O).
apply div_mod_spec_div_mod.assumption.
constructor 1.assumption.
rewrite < plus_n_O.simplify.rewrite < plus_n_O.reflexivity.
theorem mod_S: \forall n,m:nat. O < m \to S (n \mod m) < m \to
((S n) \mod m) = S (n \mod m).
intros.
-apply div_mod_spec_to_eq2 (S n) m ((S n) / m) ((S n) \mod m) (n / m) (S (n \mod m)).
+apply (div_mod_spec_to_eq2 (S n) m ((S n) / m) ((S n) \mod m) (n / m) (S (n \mod m))).
apply div_mod_spec_div_mod.assumption.
constructor 1.assumption.rewrite < plus_n_Sm.
apply eq_f.
theorem lt_to_eq_mod:\forall n,m:nat. n < m \to n \mod m = n.
intros.
-apply div_mod_spec_to_eq2 n m (n/m) (n \mod m) O n.
+apply (div_mod_spec_to_eq2 n m (n/m) (n \mod m) O n).
apply div_mod_spec_div_mod.
-apply le_to_lt_to_lt O n m.apply le_O_n.assumption.
+apply (le_to_lt_to_lt O n m).apply le_O_n.assumption.
constructor 1.
assumption.reflexivity.
qed.
(* injectivity *)
theorem injective_times_r: \forall n:nat.injective nat nat (\lambda m:nat.(S n)*m).
-change with \forall n,p,q:nat.(S n)*p = (S n)*q \to p=q.
+change with (\forall n,p,q:nat.(S n)*p = (S n)*q \to p=q).
intros.
-rewrite < div_times n.
-rewrite < div_times n q.
+rewrite < (div_times n).
+rewrite < (div_times n q).
apply eq_f2.assumption.
reflexivity.
qed.
injective_times_r.
theorem lt_O_to_injective_times_r: \forall n:nat. O < n \to injective nat nat (\lambda m:nat.n*m).
-change with \forall n. O < n \to \forall p,q:nat.n*p = n*q \to p=q.
+change with (\forall n. O < n \to \forall p,q:nat.n*p = n*q \to p=q).
intros 4.
-apply lt_O_n_elim n H.intros.
-apply inj_times_r m.assumption.
+apply (lt_O_n_elim n H).intros.
+apply (inj_times_r m).assumption.
qed.
variant inj_times_r1:\forall n. O < n \to \forall p,q:nat.n*p = n*q \to p=q
\def lt_O_to_injective_times_r.
theorem injective_times_l: \forall n:nat.injective nat nat (\lambda m:nat.m*(S n)).
-change with \forall n,p,q:nat.p*(S n) = q*(S n) \to p=q.
+change with (\forall n,p,q:nat.p*(S n) = q*(S n) \to p=q).
intros.
-apply inj_times_r n p q.
+apply (inj_times_r n p q).
rewrite < sym_times.
-rewrite < sym_times q.
+rewrite < (sym_times q).
assumption.
qed.
injective_times_l.
theorem lt_O_to_injective_times_l: \forall n:nat. O < n \to injective nat nat (\lambda m:nat.m*n).
-change with \forall n. O < n \to \forall p,q:nat.p*n = q*n \to p=q.
+change with (\forall n. O < n \to \forall p,q:nat.p*n = q*n \to p=q).
intros 4.
-apply lt_O_n_elim n H.intros.
-apply inj_times_l m.assumption.
+apply (lt_O_n_elim n H).intros.
+apply (inj_times_l m).assumption.
qed.
variant inj_times_l1:\forall n. O < n \to \forall p,q:nat.p*n = q*n \to p=q
theorem lt_m_exp_nm: \forall n,m:nat. (S O) < n \to m < n \sup m.
intros.elim m.simplify.reflexivity.
simplify.
-apply trans_le ? ((S(S O))*(S n1)).
+apply (trans_le ? ((S(S O))*(S n1))).
simplify.
rewrite < plus_n_Sm.apply le_S_S.apply le_S_S.
rewrite < sym_plus.
theorem exp_to_eq_O: \forall n,m:nat. (S O) < n
\to n \sup m = (S O) \to m = O.
intros.apply antisym_le.apply le_S_S_to_le.
-rewrite < H1.change with m < n \sup m.
+rewrite < H1.change with (m < n \sup m).
apply lt_m_exp_nm.assumption.
apply le_O_n.
qed.
theorem injective_exp_r: \forall n:nat. (S O) < n \to
injective nat nat (\lambda m:nat. n \sup m).
simplify.intros 4.
-apply nat_elim2 (\lambda x,y.n \sup x = n \sup y \to x = y).
-intros.apply sym_eq.apply exp_to_eq_O n.assumption.
+apply (nat_elim2 (\lambda x,y.n \sup x = n \sup y \to x = y)).
+intros.apply sym_eq.apply (exp_to_eq_O n).assumption.
rewrite < H1.reflexivity.
-intros.apply exp_to_eq_O n.assumption.assumption.
+intros.apply (exp_to_eq_O n).assumption.assumption.
intros.apply eq_f.
apply H1.
(* esprimere inj_times senza S *)
-cut \forall a,b:nat.O < n \to n*a=n*b \to a=b.
+cut (\forall a,b:nat.O < n \to n*a=n*b \to a=b).
apply Hcut.simplify. apply le_S_S_to_le. apply le_S. assumption.
assumption.
intros 2.
-apply nat_case n.
-intros.apply False_ind.apply not_le_Sn_O O H3.
+apply (nat_case n).
+intros.apply False_ind.apply (not_le_Sn_O O H3).
intros.
-apply inj_times_r m1.assumption.
+apply (inj_times_r m1).assumption.
qed.
variant inj_exp_r: \forall p:nat. (S O) < p \to \forall n,m:nat.
theorem le_SO_fact : \forall n. (S O) \le n!.
intro.elim n.simplify.apply le_n.
-change with (S O) \le (S n1)*n1!.
-apply trans_le ? ((S n1)*(S O)).simplify.
+change with ((S O) \le (S n1)*n1!).
+apply (trans_le ? ((S n1)*(S O))).simplify.
apply le_S_S.apply le_O_n.
apply le_times_r.assumption.
qed.
theorem le_SSO_fact : \forall n. (S O) < n \to (S(S O)) \le n!.
-intro.apply nat_case n.intro.apply False_ind.apply not_le_Sn_O (S O) H.
-intros.change with (S (S O)) \le (S m)*m!.
-apply trans_le ? ((S(S O))*(S O)).apply le_n.
+intro.apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_O (S O) H).
+intros.change with ((S (S O)) \le (S m)*m!).
+apply (trans_le ? ((S(S O))*(S O))).apply le_n.
apply le_times.exact H.apply le_SO_fact.
qed.
theorem le_n_fact_n: \forall n. n \le n!.
intro. elim n.apply le_O_n.
-change with S n1 \le (S n1)*n1!.
-apply trans_le ? ((S n1)*(S O)).
+change with (S n1 \le (S n1)*n1!).
+apply (trans_le ? ((S n1)*(S O))).
rewrite < times_n_SO.apply le_n.
apply le_times.apply le_n.
apply le_SO_fact.
qed.
theorem lt_n_fact_n: \forall n. (S(S O)) < n \to n < n!.
-intro.apply nat_case n.intro.apply False_ind.apply not_le_Sn_O (S(S O)) H.
-intros.change with (S m) < (S m)*m!.
-apply lt_to_le_to_lt ? ((S m)*(S (S O))).
+intro.apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_O (S(S O)) H).
+intros.change with ((S m) < (S m)*m!).
+apply (lt_to_le_to_lt ? ((S m)*(S (S O)))).
rewrite < sym_times.
simplify.
apply le_S_S.rewrite < plus_n_O.
nth_prime (max_prime_factor n) \divides n.
intros.apply divides_b_true_to_divides.
apply lt_O_nth_prime_n.
-apply f_max_true (\lambda p:nat.eqb (n \mod (nth_prime p)) O) n.
-cut \exists i. nth_prime i = smallest_factor n.
+apply (f_max_true (\lambda p:nat.eqb (n \mod (nth_prime p)) O) n).
+cut (\exists i. nth_prime i = smallest_factor n).
elim Hcut.
-apply ex_intro nat ? a.
+apply (ex_intro nat ? a).
split.
-apply trans_le a (nth_prime a).
+apply (trans_le a (nth_prime a)).
apply le_n_fn.
exact lt_nth_prime_n_nth_prime_Sn.
rewrite > H1. apply le_smallest_factor_n.
rewrite > H1.
-change with divides_b (smallest_factor n) n = true.
+change with (divides_b (smallest_factor n) n = true).
apply divides_to_divides_b_true.
-apply trans_lt ? (S O).simplify. apply le_n.
+apply (trans_lt ? (S O)).simplify. apply le_n.
apply lt_SO_smallest_factor.assumption.
apply divides_smallest_factor_n.
-apply trans_lt ? (S O). simplify. apply le_n. assumption.
+apply (trans_lt ? (S O)). simplify. apply le_n. assumption.
apply prime_to_nth_prime.
apply prime_smallest_factor_n.assumption.
qed.
theorem divides_to_max_prime_factor : \forall n,m. (S O) < n \to O < m \to n \divides m \to
max_prime_factor n \le max_prime_factor m.
intros.change with
-(max n (\lambda p:nat.eqb (n \mod (nth_prime p)) O)) \le
-(max m (\lambda p:nat.eqb (m \mod (nth_prime p)) O)).
+((max n (\lambda p:nat.eqb (n \mod (nth_prime p)) O)) \le
+(max m (\lambda p:nat.eqb (m \mod (nth_prime p)) O))).
apply f_m_to_le_max.
-apply trans_le ? n.
+apply (trans_le ? n).
apply le_max_n.apply divides_to_le.assumption.assumption.
-change with divides_b (nth_prime (max_prime_factor n)) m = true.
+change with (divides_b (nth_prime (max_prime_factor n)) m = true).
apply divides_to_divides_b_true.
-cut prime (nth_prime (max_prime_factor n)).
+cut (prime (nth_prime (max_prime_factor n))).
apply lt_O_nth_prime_n.apply prime_nth_prime.
-cut nth_prime (max_prime_factor n) \divides n.
-apply transitive_divides ? n.
+cut (nth_prime (max_prime_factor n) \divides n).
+apply (transitive_divides ? n).
apply divides_max_prime_factor_n.
assumption.assumption.
apply divides_b_true_to_divides.
(S O) < r \to max_prime_factor r < p.
intros.
rewrite > H1.
-cut max_prime_factor r \lt max_prime_factor n \lor
- max_prime_factor r = max_prime_factor n.
+cut (max_prime_factor r \lt max_prime_factor n \lor
+ max_prime_factor r = max_prime_factor n).
elim Hcut.assumption.
-absurd nth_prime (max_prime_factor n) \divides r.
+absurd (nth_prime (max_prime_factor n) \divides r).
rewrite < H4.
apply divides_max_prime_factor_n.
assumption.
-change with nth_prime (max_prime_factor n) \divides r \to False.
+change with (nth_prime (max_prime_factor n) \divides r \to False).
intro.
-cut r \mod (nth_prime (max_prime_factor n)) \neq O.
+cut (r \mod (nth_prime (max_prime_factor n)) \neq O).
apply Hcut1.apply divides_to_mod_O.
apply lt_O_nth_prime_n.assumption.
-apply p_ord_aux_to_not_mod_O n n ? q r.
+apply (p_ord_aux_to_not_mod_O n n ? q r).
apply lt_SO_nth_prime_n.assumption.
apply le_n.
rewrite < H1.assumption.
-apply le_to_or_lt_eq (max_prime_factor r) (max_prime_factor n).
+apply (le_to_or_lt_eq (max_prime_factor r) (max_prime_factor n)).
apply divides_to_max_prime_factor.
assumption.assumption.
-apply witness r n ((nth_prime p) \sup q).
+apply (witness r n ((nth_prime p) \sup q)).
rewrite < sym_times.
-apply p_ord_aux_to_exp n n ? q r.
+apply (p_ord_aux_to_exp n n ? q r).
apply lt_O_nth_prime_n.assumption.
qed.
(pair nat nat q r) = p_ord n (nth_prime p) \to
(S O) < r \to max_prime_factor r < p.
intros.
-cut max_prime_factor n < p \lor max_prime_factor n = p.
-elim Hcut.apply le_to_lt_to_lt ? (max_prime_factor n).
+cut (max_prime_factor n < p \lor max_prime_factor n = p).
+elim Hcut.apply (le_to_lt_to_lt ? (max_prime_factor n)).
apply divides_to_max_prime_factor.assumption.assumption.
-apply witness r n ((nth_prime p) \sup q).
+apply (witness r n ((nth_prime p) \sup q)).
rewrite > sym_times.
-apply p_ord_aux_to_exp n n.
+apply (p_ord_aux_to_exp n n).
apply lt_O_nth_prime_n.
assumption.assumption.
-apply p_ord_to_lt_max_prime_factor n ? q.
+apply (p_ord_to_lt_max_prime_factor n ? q).
assumption.apply sym_eq.assumption.assumption.assumption.
-apply le_to_or_lt_eq ? p H1.
+apply (le_to_or_lt_eq ? p H1).
qed.
(* datatypes and functions *)
intro.elim f.simplify.
rewrite > times_n_SO.
apply le_times.
-change with O < nth_prime i.
+change with (O < nth_prime i).
apply lt_O_nth_prime_n.
-change with O < exp (nth_prime i) n.
+change with (O < exp (nth_prime i) n).
apply lt_O_exp.
apply lt_O_nth_prime_n.
simplify.
rewrite > times_n_SO.
apply le_times.
-change with O < exp (nth_prime i) n.
+change with (O < exp (nth_prime i) n).
apply lt_O_exp.
apply lt_O_nth_prime_n.
-change with O < defactorize_aux n1 (S i).
+change with (O < defactorize_aux n1 (S i)).
apply H.
qed.
intro.elim f.simplify.
rewrite > times_n_SO.
apply le_times.
-change with S O < nth_prime i.
+change with (S O < nth_prime i).
apply lt_SO_nth_prime_n.
-change with O < exp (nth_prime i) n.
+change with (O < exp (nth_prime i) n).
apply lt_O_exp.
apply lt_O_nth_prime_n.
simplify.
rewrite > times_n_SO.
rewrite > sym_times.
apply le_times.
-change with O < exp (nth_prime i) n.
+change with (O < exp (nth_prime i) n).
apply lt_O_exp.
apply lt_O_nth_prime_n.
-change with S O < defactorize_aux n1 (S i).
+change with (S O < defactorize_aux n1 (S i)).
apply H.
qed.
intro.elim p.simplify.
elim H1.elim H2.rewrite > H3.
rewrite > sym_times. apply times_n_SO.
-apply False_ind.apply not_le_Sn_O (max_prime_factor n) H2.
+apply False_ind.apply (not_le_Sn_O (max_prime_factor n) H2).
simplify.
(* generalizing the goal: I guess there exists a better way *)
-cut \forall q,r.(pair nat nat q r) = (p_ord_aux n1 n1 (nth_prime n)) \to
+cut (\forall q,r.(pair nat nat q r) = (p_ord_aux n1 n1 (nth_prime n)) \to
defactorize_aux match (p_ord_aux n1 n1 (nth_prime n)) with
[(pair q r) \Rightarrow (factorize_aux n r (nf_cons q acc))] O =
-n1*defactorize_aux acc (S n).
-apply Hcut (fst ? ? (p_ord_aux n1 n1 (nth_prime n)))
-(snd ? ? (p_ord_aux n1 n1 (nth_prime n))).
+n1*defactorize_aux acc (S n)).
+apply (Hcut (fst ? ? (p_ord_aux n1 n1 (nth_prime n)))
+(snd ? ? (p_ord_aux n1 n1 (nth_prime n)))).
apply sym_eq.apply eq_pair_fst_snd.
intros.
rewrite < H3.
simplify.
-cut n1 = r * (nth_prime n) \sup q.
+cut (n1 = r * (nth_prime n) \sup q).
rewrite > H.
simplify.rewrite < assoc_times.
rewrite < Hcut.reflexivity.
-cut O < r \lor O = r.
-elim Hcut1.assumption.absurd n1 = O.
+cut (O < r \lor O = r).
+elim Hcut1.assumption.absurd (n1 = O).
rewrite > Hcut.rewrite < H4.reflexivity.
-simplify. intro.apply not_le_Sn_O O.
+simplify. intro.apply (not_le_Sn_O O).
rewrite < H5 in \vdash (? ? %).assumption.
apply le_to_or_lt_eq.apply le_O_n.
-cut (S O) < r \lor (S O) \nlt r.
+cut ((S O) < r \lor (S O) \nlt r).
elim Hcut1.
right.
-apply p_ord_to_lt_max_prime_factor1 n1 ? q r.
+apply (p_ord_to_lt_max_prime_factor1 n1 ? q r).
assumption.elim H2.
elim H5.
apply False_ind.
-apply not_eq_O_S n.apply sym_eq.assumption.
+apply (not_eq_O_S n).apply sym_eq.assumption.
apply le_S_S_to_le.
exact H5.
assumption.assumption.
-cut r=(S O).
-apply nat_case n.
+cut (r=(S O)).
+apply (nat_case n).
left.split.assumption.reflexivity.
intro.right.rewrite > Hcut2.
simplify.apply le_S_S.apply le_O_n.
-cut r \lt (S O) \or r=(S O).
-elim Hcut2.absurd O=r.
+cut (r \lt (S O) \or r=(S O)).
+elim Hcut2.absurd (O=r).
apply le_n_O_to_eq.apply le_S_S_to_le.exact H5.
simplify.intro.
-cut O=n1.
-apply not_le_Sn_O O.
+cut (O=n1).
+apply (not_le_Sn_O O).
rewrite > Hcut3 in \vdash (? ? %).
assumption.rewrite > Hcut.
rewrite < H6.reflexivity.
assumption.
-apply le_to_or_lt_eq r (S O).
+apply (le_to_or_lt_eq r (S O)).
apply not_lt_to_le.assumption.
-apply decidable_lt (S O) r.
+apply (decidable_lt (S O) r).
rewrite > sym_times.
-apply p_ord_aux_to_exp n1 n1.
+apply (p_ord_aux_to_exp n1 n1).
apply lt_O_nth_prime_n.assumption.
qed.
theorem defactorize_factorize: \forall n:nat.defactorize (factorize n) = n.
intro.
-apply nat_case n.reflexivity.
-intro.apply nat_case m.reflexivity.
+apply (nat_case n).reflexivity.
+intro.apply (nat_case m).reflexivity.
intro.change with
-let p \def (max (S(S m1)) (\lambda p:nat.eqb ((S(S m1)) \mod (nth_prime p)) O)) in
+(let p \def (max (S(S m1)) (\lambda p:nat.eqb ((S(S m1)) \mod (nth_prime p)) O)) in
defactorize (match p_ord (S(S m1)) (nth_prime p) with
[ (pair q r) \Rightarrow
- nfa_proper (factorize_aux p r (nf_last (pred q)))])=(S(S m1)).
+ nfa_proper (factorize_aux p r (nf_last (pred q)))])=(S(S m1))).
intro.
(* generalizing the goal; find a better way *)
-cut \forall q,r.(pair nat nat q r) = (p_ord (S(S m1)) (nth_prime p)) \to
+cut (\forall q,r.(pair nat nat q r) = (p_ord (S(S m1)) (nth_prime p)) \to
defactorize (match p_ord (S(S m1)) (nth_prime p) with
[ (pair q r) \Rightarrow
- nfa_proper (factorize_aux p r (nf_last (pred q)))])=(S(S m1)).
-apply Hcut (fst ? ? (p_ord (S(S m1)) (nth_prime p)))
-(snd ? ? (p_ord (S(S m1)) (nth_prime p))).
+ nfa_proper (factorize_aux p r (nf_last (pred q)))])=(S(S m1))).
+apply (Hcut (fst ? ? (p_ord (S(S m1)) (nth_prime p)))
+(snd ? ? (p_ord (S(S m1)) (nth_prime p)))).
apply sym_eq.apply eq_pair_fst_snd.
intros.
rewrite < H.
change with
-defactorize_aux (factorize_aux p r (nf_last (pred q))) O = (S(S m1)).
-cut (S(S m1)) = (nth_prime p) \sup q *r.
-cut O <r.
+(defactorize_aux (factorize_aux p r (nf_last (pred q))) O = (S(S m1))).
+cut ((S(S m1)) = (nth_prime p) \sup q *r).
+cut (O<r).
rewrite > defactorize_aux_factorize_aux.
-change with r*(nth_prime p) \sup (S (pred q)) = (S(S m1)).
-cut (S (pred q)) = q.
+change with (r*(nth_prime p) \sup (S (pred q)) = (S(S m1))).
+cut ((S (pred q)) = q).
rewrite > Hcut2.
rewrite > sym_times.
apply sym_eq.
-apply p_ord_aux_to_exp (S(S m1)).
+apply (p_ord_aux_to_exp (S(S m1))).
apply lt_O_nth_prime_n.
assumption.
(* O < q *)
apply sym_eq. apply S_pred.
-cut O < q \lor O = q.
+cut (O < q \lor O = q).
elim Hcut2.assumption.
-absurd nth_prime p \divides S (S m1).
-apply divides_max_prime_factor_n (S (S m1)).
+absurd (nth_prime p \divides S (S m1)).
+apply (divides_max_prime_factor_n (S (S m1))).
simplify.apply le_S_S.apply le_S_S. apply le_O_n.
-cut (S(S m1)) = r.
+cut ((S(S m1)) = r).
rewrite > Hcut3 in \vdash (? (? ? %)).
-change with nth_prime p \divides r \to False.
+change with (nth_prime p \divides r \to False).
intro.
-apply p_ord_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r.
+apply (p_ord_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r).
apply lt_SO_nth_prime_n.
simplify.apply le_S_S.apply le_O_n.apply le_n.
assumption.
apply divides_to_mod_O.apply lt_O_nth_prime_n.assumption.
rewrite > times_n_SO in \vdash (? ? ? %).
rewrite < sym_times.
-rewrite > exp_n_O (nth_prime p).
+rewrite > (exp_n_O (nth_prime p)).
rewrite > H1 in \vdash (? ? ? (? (? ? %) ?)).
assumption.
apply le_to_or_lt_eq.apply le_O_n.assumption.
(* e adesso l'ultimo goal. TASSI: che ora non e' piu' l'ultimo :P *)
-cut (S O) < r \lor S O \nlt r.
+cut ((S O) < r \lor S O \nlt r).
elim Hcut2.
right.
-apply p_ord_to_lt_max_prime_factor1 (S(S m1)) ? q r.
+apply (p_ord_to_lt_max_prime_factor1 (S(S m1)) ? q r).
simplify.apply le_S_S. apply le_O_n.
apply le_n.
assumption.assumption.
-cut r=(S O).
-apply nat_case p.
+cut (r=(S O)).
+apply (nat_case p).
left.split.assumption.reflexivity.
intro.right.rewrite > Hcut3.
simplify.apply le_S_S.apply le_O_n.
-cut r \lt (S O) \or r=(S O).
-elim Hcut3.absurd O=r.
+cut (r \lt (S O) \or r=(S O)).
+elim Hcut3.absurd (O=r).
apply le_n_O_to_eq.apply le_S_S_to_le.exact H2.
simplify.intro.
-apply not_le_Sn_O O.
+apply (not_le_Sn_O O).
rewrite > H3 in \vdash (? ? %).assumption.assumption.
-apply le_to_or_lt_eq r (S O).
+apply (le_to_or_lt_eq r (S O)).
apply not_lt_to_le.assumption.
-apply decidable_lt (S O) r.
+apply (decidable_lt (S O) r).
(* O < r *)
-cut O < r \lor O = r.
+cut (O < r \lor O = r).
elim Hcut1.assumption.
apply False_ind.
-apply not_eq_O_S (S m1).
+apply (not_eq_O_S (S m1)).
rewrite > Hcut.rewrite < H1.rewrite < times_n_O.reflexivity.
apply le_to_or_lt_eq.apply le_O_n.
(* prova del cut *)
goal 20.
-apply p_ord_aux_to_exp (S(S m1)).
+apply (p_ord_aux_to_exp (S(S m1))).
apply lt_O_nth_prime_n.
assumption.
(* fine prova cut *)
theorem divides_max_p_defactorize: \forall f:nat_fact.\forall i:nat.
nth_prime ((max_p f)+i) \divides defactorize_aux f i.
intro.
-elim f.simplify.apply witness ? ? ((nth_prime i) \sup n).
+elim f.simplify.apply (witness ? ? ((nth_prime i) \sup n)).
reflexivity.
change with
-nth_prime (S(max_p n1)+i) \divides
-(nth_prime i) \sup n *(defactorize_aux n1 (S i)).
-elim H (S i).
+(nth_prime (S(max_p n1)+i) \divides
+(nth_prime i) \sup n *(defactorize_aux n1 (S i))).
+elim (H (S i)).
rewrite > H1.
rewrite < sym_times.
rewrite > assoc_times.
rewrite < plus_n_Sm.
-apply witness ? ? (n2* (nth_prime i) \sup n).
+apply (witness ? ? (n2* (nth_prime i) \sup n)).
reflexivity.
qed.
\forall p,n,m:nat. prime p \to
p \divides n \sup m \to p \divides n.
intros 3.elim m.simplify in H1.
-apply transitive_divides p (S O).assumption.
+apply (transitive_divides p (S O)).assumption.
apply divides_SO_n.
-cut p \divides n \lor p \divides n \sup n1.
+cut (p \divides n \lor p \divides n \sup n1).
elim Hcut.assumption.
apply H.assumption.assumption.
apply divides_times_to_divides.assumption.
intros.
simplify in H1.
elim H1.apply H4.
-apply divides_exp_to_divides p q m.
+apply (divides_exp_to_divides p q m).
assumption.assumption.
simplify in H.elim H.assumption.
qed.
i < j \to nth_prime i \ndivides defactorize_aux f j.
intro.elim f.
change with
-nth_prime i \divides (nth_prime j) \sup (S n) \to False.
-intro.absurd (nth_prime i) = (nth_prime j).
-apply divides_exp_to_eq ? ? (S n).
+(nth_prime i \divides (nth_prime j) \sup (S n) \to False).
+intro.absurd ((nth_prime i) = (nth_prime j)).
+apply (divides_exp_to_eq ? ? (S n)).
apply prime_nth_prime.apply prime_nth_prime.
assumption.
-change with (nth_prime i) = (nth_prime j) \to False.
-intro.cut i = j.
-apply not_le_Sn_n i.rewrite > Hcut in \vdash (? ? %).assumption.
-apply injective_nth_prime ? ? H2.
+change with ((nth_prime i) = (nth_prime j) \to False).
+intro.cut (i = j).
+apply (not_le_Sn_n i).rewrite > Hcut in \vdash (? ? %).assumption.
+apply (injective_nth_prime ? ? H2).
change with
-nth_prime i \divides (nth_prime j) \sup n *(defactorize_aux n1 (S j)) \to False.
+(nth_prime i \divides (nth_prime j) \sup n *(defactorize_aux n1 (S j)) \to False).
intro.
-cut nth_prime i \divides (nth_prime j) \sup n
-\lor nth_prime i \divides defactorize_aux n1 (S j).
+cut (nth_prime i \divides (nth_prime j) \sup n
+\lor nth_prime i \divides defactorize_aux n1 (S j)).
elim Hcut.
-absurd (nth_prime i) = (nth_prime j).
-apply divides_exp_to_eq ? ? n.
+absurd ((nth_prime i) = (nth_prime j)).
+apply (divides_exp_to_eq ? ? n).
apply prime_nth_prime.apply prime_nth_prime.
assumption.
-change with (nth_prime i) = (nth_prime j) \to False.
+change with ((nth_prime i) = (nth_prime j) \to False).
intro.
-cut i = j.
-apply not_le_Sn_n i.rewrite > Hcut1 in \vdash (? ? %).assumption.
-apply injective_nth_prime ? ? H4.
-apply H i (S j).
-apply trans_lt ? j.assumption.simplify.apply le_n.
+cut (i = j).
+apply (not_le_Sn_n i).rewrite > Hcut1 in \vdash (? ? %).assumption.
+apply (injective_nth_prime ? ? H4).
+apply (H i (S j)).
+apply (trans_lt ? j).assumption.simplify.apply le_n.
assumption.
apply divides_times_to_divides.
apply prime_nth_prime.assumption.
\lnot (defactorize_aux (nf_last n) i= defactorize_aux (nf_cons m g) i).
intros.
change with
-exp (nth_prime i) (S n) = defactorize_aux (nf_cons m g) i \to False.
+(exp (nth_prime i) (S n) = defactorize_aux (nf_cons m g) i \to False).
intro.
-cut S(max_p g)+i= i.
-apply not_le_Sn_n i.
+cut (S(max_p g)+i= i).
+apply (not_le_Sn_n i).
rewrite < Hcut in \vdash (? ? %).
simplify.apply le_S_S.
apply le_plus_n.
apply injective_nth_prime.
(* uffa, perche' semplifica ? *)
-change with nth_prime (S(max_p g)+i)= nth_prime i.
-apply divides_exp_to_eq ? ? (S n).
+change with (nth_prime (S(max_p g)+i)= nth_prime i).
+apply (divides_exp_to_eq ? ? (S n)).
apply prime_nth_prime.apply prime_nth_prime.
rewrite > H.
-change with divides (nth_prime ((max_p (nf_cons m g))+i))
-(defactorize_aux (nf_cons m g) i).
+change with (divides (nth_prime ((max_p (nf_cons m g))+i))
+(defactorize_aux (nf_cons m g) i)).
apply divides_max_p_defactorize.
qed.
intros.
simplify.rewrite < plus_n_O.
intro.
-apply not_divides_defactorize_aux f i (S i) ?.
+apply (not_divides_defactorize_aux f i (S i) ?).
simplify.apply le_n.
rewrite > H.
rewrite > assoc_times.
-apply witness ? ? ((exp (nth_prime i) n)*(defactorize_aux g (S i))).
+apply (witness ? ? ((exp (nth_prime i) n)*(defactorize_aux g (S i)))).
reflexivity.
qed.
generalize in match H.
elim g.
apply eq_f.
-apply inj_S. apply inj_exp_r (nth_prime i).
+apply inj_S. apply (inj_exp_r (nth_prime i)).
apply lt_SO_nth_prime_n.
assumption.
apply False_ind.
-apply not_eq_nf_last_nf_cons n2 n n1 i H2.
+apply (not_eq_nf_last_nf_cons n2 n n1 i H2).
generalize in match H1.
elim g.
apply False_ind.
-apply not_eq_nf_last_nf_cons n1 n2 n i.
+apply (not_eq_nf_last_nf_cons n1 n2 n i).
apply sym_eq. assumption.
simplify in H3.
generalize in match H3.
-apply nat_elim2 (\lambda n,n2.
+apply (nat_elim2 (\lambda n,n2.
((nth_prime i) \sup n)*(defactorize_aux n1 (S i)) =
((nth_prime i) \sup n2)*(defactorize_aux n3 (S i)) \to
-nf_cons n n1 = nf_cons n2 n3).
+nf_cons n n1 = nf_cons n2 n3)).
intro.
elim n4. apply eq_f.
-apply H n3 (S i).
+apply (H n3 (S i)).
simplify in H4.
rewrite > plus_n_O.
-rewrite > plus_n_O (defactorize_aux n3 (S i)).assumption.
+rewrite > (plus_n_O (defactorize_aux n3 (S i))).assumption.
apply False_ind.
-apply not_eq_nf_cons_O_nf_cons n1 n3 n5 i.assumption.
+apply (not_eq_nf_cons_O_nf_cons n1 n3 n5 i).assumption.
intros.
apply False_ind.
-apply not_eq_nf_cons_O_nf_cons n3 n1 n4 i.
+apply (not_eq_nf_cons_O_nf_cons n3 n1 n4 i).
apply sym_eq.assumption.
intros.
-cut nf_cons n4 n1 = nf_cons m n3.
-cut n4=m.
-cut n1=n3.
+cut (nf_cons n4 n1 = nf_cons m n3).
+cut (n4=m).
+cut (n1=n3).
rewrite > Hcut1.rewrite > Hcut2.reflexivity.
change with
-match nf_cons n4 n1 with
+(match nf_cons n4 n1 with
[ (nf_last m) \Rightarrow n1
-| (nf_cons m g) \Rightarrow g ] = n3.
+| (nf_cons m g) \Rightarrow g ] = n3).
rewrite > Hcut.simplify.reflexivity.
change with
-match nf_cons n4 n1 with
+(match nf_cons n4 n1 with
[ (nf_last m) \Rightarrow m
-| (nf_cons m g) \Rightarrow m ] = m.
+| (nf_cons m g) \Rightarrow m ] = m).
rewrite > Hcut.simplify.reflexivity.
apply H4.simplify in H5.
-apply inj_times_r1 (nth_prime i).
+apply (inj_times_r1 (nth_prime i)).
apply lt_O_nth_prime_n.
rewrite < assoc_times.rewrite < assoc_times.assumption.
qed.
theorem injective_defactorize_aux: \forall i:nat.
injective nat_fact nat (\lambda f.defactorize_aux f i).
-change with \forall i:nat.\forall f,g:nat_fact.
-defactorize_aux f i = defactorize_aux g i \to f = g.
+change with (\forall i:nat.\forall f,g:nat_fact.
+defactorize_aux f i = defactorize_aux g i \to f = g).
intros.
-apply eq_defactorize_aux_to_eq f g i H.
+apply (eq_defactorize_aux_to_eq f g i H).
qed.
theorem injective_defactorize:
injective nat_fact_all nat defactorize.
-change with \forall f,g:nat_fact_all.
-defactorize f = defactorize g \to f = g.
+change with (\forall f,g:nat_fact_all.
+defactorize f = defactorize g \to f = g).
intro.elim f.
generalize in match H.elim g.
(* zero - zero *)
(* zero - one *)
simplify in H1.
apply False_ind.
-apply not_eq_O_S O H1.
+apply (not_eq_O_S O H1).
(* zero - proper *)
simplify in H1.
apply False_ind.
-apply not_le_Sn_n O.
+apply (not_le_Sn_n O).
rewrite > H1 in \vdash (? ? %).
-change with O < defactorize_aux n O.
+change with (O < defactorize_aux n O).
apply lt_O_defactorize_aux.
generalize in match H.
elim g.
(* one - zero *)
simplify in H1.
apply False_ind.
-apply not_eq_O_S O.apply sym_eq. assumption.
+apply (not_eq_O_S O).apply sym_eq. assumption.
(* one - one *)
reflexivity.
(* one - proper *)
simplify in H1.
apply False_ind.
-apply not_le_Sn_n (S O).
+apply (not_le_Sn_n (S O)).
rewrite > H1 in \vdash (? ? %).
-change with (S O) < defactorize_aux n O.
+change with ((S O) < defactorize_aux n O).
apply lt_SO_defactorize_aux.
generalize in match H.elim g.
(* proper - zero *)
simplify in H1.
apply False_ind.
-apply not_le_Sn_n O.
+apply (not_le_Sn_n O).
rewrite < H1 in \vdash (? ? %).
-change with O < defactorize_aux n O.
+change with (O < defactorize_aux n O).
apply lt_O_defactorize_aux.
(* proper - one *)
simplify in H1.
apply False_ind.
-apply not_le_Sn_n (S O).
+apply (not_le_Sn_n (S O)).
rewrite < H1 in \vdash (? ? %).
-change with (S O) < defactorize_aux n O.
+change with ((S O) < defactorize_aux n O).
apply lt_SO_defactorize_aux.
(* proper - proper *)
apply eq_f.
-apply injective_defactorize_aux O.
+apply (injective_defactorize_aux O).
exact H1.
qed.
intros.
apply injective_defactorize.
(* uffa: perche' semplifica ??? *)
-change with defactorize(factorize (defactorize f)) = (defactorize f).
+change with (defactorize(factorize (defactorize f)) = (defactorize f)).
apply defactorize_factorize.
qed.
intro.unfold permut.split.intros.
unfold S_mod.
apply le_S_S_to_le.
-change with (S i) \mod (S n) < S n.
+change with ((S i) \mod (S n) < S n).
apply lt_mod_m_m.
simplify.apply le_S_S.apply le_O_n.
unfold injn.intros.
apply inj_S.
-rewrite < lt_to_eq_mod i (S n).
-rewrite < lt_to_eq_mod j (S n).
-cut i < n \lor i = n.
-cut j < n \lor j = n.
+rewrite < (lt_to_eq_mod i (S n)).
+rewrite < (lt_to_eq_mod j (S n)).
+cut (i < n \lor i = n).
+cut (j < n \lor j = n).
elim Hcut.
elim Hcut1.
(* i < n, j< n *)
unfold S_mod in H2.
simplify.
apply False_ind.
-apply not_eq_O_S (i \mod (S n)).
+apply (not_eq_O_S (i \mod (S n))).
apply sym_eq.
-rewrite < mod_n_n (S n).
+rewrite < (mod_n_n (S n)).
rewrite < H4 in \vdash (? ? ? (? %?)).
rewrite < mod_S.assumption.
simplify.apply le_S_S.apply le_O_n.
(* i = n, j < n *)
elim Hcut1.
apply False_ind.
-apply not_eq_O_S (j \mod (S n)).
-rewrite < mod_n_n (S n).
+apply (not_eq_O_S (j \mod (S n))).
+rewrite < (mod_n_n (S n)).
rewrite < H3 in \vdash (? ? (? %?) ?).
rewrite < mod_S.assumption.
simplify.apply le_S_S.apply le_O_n.
change with (S n1)*n1!=(S_mod m n1)*(pi n1 (S_mod m)).
unfold S_mod in \vdash (? ? ? (? % ?)).
rewrite > lt_to_eq_mod.
-apply eq_f.apply H.apply trans_lt ? (S n1).
+apply eq_f.apply H.apply (trans_lt ? (S n1)).
simplify. apply le_n.assumption.assumption.
qed.
*)
theorem prime_to_not_divides_fact: \forall p:nat. prime p \to \forall n:nat.
n \lt p \to \not divides p n!.
intros 3.elim n.simplify.intros.
-apply lt_to_not_le (S O) p.
+apply (lt_to_not_le (S O) p).
unfold prime in H.elim H.
assumption.apply divides_to_le.simplify.apply le_n.
assumption.
-change with (divides p ((S n1)*n1!)) \to False.
+change with (divides p ((S n1)*n1!) \to False).
intro.
-cut divides p (S n1) \lor divides p n1!.
-elim Hcut.apply lt_to_not_le (S n1) p.
+cut (divides p (S n1) \lor divides p n1!).
+elim Hcut.apply (lt_to_not_le (S n1) p).
assumption.
apply divides_to_le.simplify.apply le_S_S.apply le_O_n.
assumption.apply H1.
-apply trans_lt ? (S n1).simplify. apply le_n.
+apply (trans_lt ? (S n1)).simplify. apply le_n.
assumption.assumption.
apply divides_times_to_divides.
assumption.assumption.
\lnot divides p a\to permut (\lambda n.(mod (a*n) p)) (pred p).
unfold permut.intros.
split.intros.apply le_S_S_to_le.
-apply trans_le ? p.
-change with mod (a*i) p < p.
+apply (trans_le ? p).
+change with (mod (a*i) p < p).
apply lt_mod_m_m.
simplify in H.elim H.
-simplify.apply trans_le ? (S (S O)).
+simplify.apply (trans_le ? (S (S O))).
apply le_n_Sn.assumption.
rewrite < S_pred.apply le_n.
unfold prime in H.
elim H.
-apply trans_lt ? (S O).simplify.apply le_n.assumption.
+apply (trans_lt ? (S O)).simplify.apply le_n.assumption.
unfold injn.intros.
-apply nat_compare_elim i j.
+apply (nat_compare_elim i j).
(* i < j *)
intro.
-absurd j-i \lt p.
+absurd (j-i \lt p).
simplify.
-rewrite > S_pred p.
+rewrite > (S_pred p).
apply le_S_S.
apply le_plus_to_minus.
-apply trans_le ? (pred p).assumption.
+apply (trans_le ? (pred p)).assumption.
rewrite > sym_plus.
apply le_plus_n.
unfold prime in H.
elim H.
-apply trans_lt ? (S O).simplify.apply le_n.assumption.
-apply le_to_not_lt p (j-i).
+apply (trans_lt ? (S O)).simplify.apply le_n.assumption.
+apply (le_to_not_lt p (j-i)).
apply divides_to_le.simplify.
apply le_SO_minus.assumption.
-cut divides p a \lor divides p (j-i).
+cut (divides p a \lor divides p (j-i)).
elim Hcut.apply False_ind.apply H1.assumption.assumption.
apply divides_times_to_divides.assumption.
rewrite > distr_times_minus.
apply eq_mod_to_divides.
unfold prime in H.
elim H.
-apply trans_lt ? (S O).simplify.apply le_n.assumption.
+apply (trans_lt ? (S O)).simplify.apply le_n.assumption.
apply sym_eq.
apply H4.
(* i = j *)
intro. assumption.
(* j < i *)
intro.
-absurd i-j \lt p.
+absurd (i-j \lt p).
simplify.
-rewrite > S_pred p.
+rewrite > (S_pred p).
apply le_S_S.
apply le_plus_to_minus.
-apply trans_le ? (pred p).assumption.
+apply (trans_le ? (pred p)).assumption.
rewrite > sym_plus.
apply le_plus_n.
unfold prime in H.
elim H.
-apply trans_lt ? (S O).simplify.apply le_n.assumption.
-apply le_to_not_lt p (i-j).
+apply (trans_lt ? (S O)).simplify.apply le_n.assumption.
+apply (le_to_not_lt p (i-j)).
apply divides_to_le.simplify.
apply le_SO_minus.assumption.
-cut divides p a \lor divides p (i-j).
+cut (divides p a \lor divides p (i-j)).
elim Hcut.apply False_ind.apply H1.assumption.assumption.
apply divides_times_to_divides.assumption.
rewrite > distr_times_minus.
apply eq_mod_to_divides.
unfold prime in H.
elim H.
-apply trans_lt ? (S O).simplify.apply le_n.assumption.
+apply (trans_lt ? (S O)).simplify.apply le_n.assumption.
apply H4.
qed.
theorem congruent_exp_pred_SO: \forall p,a:nat. prime p \to \lnot divides p a \to
congruent (exp a (pred p)) (S O) p.
intros.
-cut O < a.
-cut O < p.
-cut O < pred p.
+cut (O < a).
+cut (O < p).
+cut (O < pred p).
apply divides_to_congruent.
assumption.
-change with O < exp a (pred p).
+change with (O < exp a (pred p)).
apply lt_O_exp.assumption.
-cut divides p (exp a (pred p)-(S O)) \lor divides p (pred p)!.
+cut (divides p (exp a (pred p)-(S O)) \lor divides p (pred p)!).
elim Hcut3.
assumption.
apply False_ind.
-apply prime_to_not_divides_fact p H (pred p).
-change with S (pred p) \le p.
+apply (prime_to_not_divides_fact p H (pred p)).
+change with (S (pred p) \le p).
rewrite < S_pred.apply le_n.
assumption.assumption.
apply divides_times_to_divides.
assumption.
rewrite > times_minus_l.
-rewrite > sym_times (S O).
+rewrite > (sym_times (S O)).
rewrite < times_n_SO.
-rewrite > S_pred (pred p).
+rewrite > (S_pred (pred p)).
rewrite > eq_fact_pi.
(* in \vdash (? ? (? % ?)). *)
rewrite > exp_pi_l.
apply congruent_to_divides.
assumption.
-apply transitive_congruent p ?
-(pi (pred (pred p)) (\lambda m. a*m \mod p) (S O)).
-apply congruent_pi (\lambda m. a*m).
+apply (transitive_congruent p ?
+(pi (pred (pred p)) (\lambda m. a*m \mod p) (S O))).
+apply (congruent_pi (\lambda m. a*m)).
assumption.
-cut pi (pred(pred p)) (\lambda m.m) (S O)
-= pi (pred(pred p)) (\lambda m.a*m \mod p) (S O).
+cut (pi (pred(pred p)) (\lambda m.m) (S O)
+= pi (pred(pred p)) (\lambda m.a*m \mod p) (S O)).
rewrite > Hcut3.apply congruent_n_n.
rewrite < eq_map_iter_i_pi.
rewrite < eq_map_iter_i_pi.
rewrite < S_pred.
apply permut_mod.assumption.
assumption.assumption.
-intros.cut m=O.
+intros.cut (m=O).
rewrite > Hcut3.rewrite < times_n_O.
apply mod_O_n.apply sym_eq.apply le_n_O_to_eq.
apply le_S_S_to_le.assumption.
assumption.
-change with (S O) \le pred p.
+change with ((S O) \le pred p).
apply le_S_S_to_le.rewrite < S_pred.
unfold prime in H.elim H.assumption.assumption.
-unfold prime in H.elim H.apply trans_lt ? (S O).
+unfold prime in H.elim H.apply (trans_lt ? (S O)).
simplify.apply le_n.assumption.
-cut O < a \lor O = a.
+cut (O < a \lor O = a).
elim Hcut.assumption.
apply False_ind.apply H1.
rewrite < H2.
-apply witness ? ? O.apply times_n_O.
+apply (witness ? ? O).apply times_n_O.
apply le_to_or_lt_eq.
apply le_O_n.
qed.
theorem divides_mod: \forall p,m,n:nat. O < n \to p \divides m \to p \divides n \to
p \divides (m \mod n).
intros.elim H1.elim H2.
-apply witness ? ? (n2 - n1*(m / n)).
+apply (witness ? ? (n2 - n1*(m / n))).
rewrite > distr_times_minus.
rewrite < H3.
rewrite < assoc_times.
theorem divides_mod_to_divides: \forall p,m,n:nat. O < n \to
p \divides (m \mod n) \to p \divides n \to p \divides m.
intros.elim H1.elim H2.
-apply witness p m ((n1*(m / n))+n2).
+apply (witness p m ((n1*(m / n))+n2)).
rewrite > distr_times_plus.
rewrite < H3.
rewrite < assoc_times.
theorem divides_gcd_aux_mn: \forall p,m,n. O < n \to n \le m \to n \le p \to
gcd_aux p m n \divides m \land gcd_aux p m n \divides n.
intro.elim p.
-absurd O < n.assumption.apply le_to_not_lt.assumption.
-cut (n1 \divides m) \lor (n1 \ndivides m).
+absurd (O < n).assumption.apply le_to_not_lt.assumption.
+cut ((n1 \divides m) \lor (n1 \ndivides m)).
change with
-(match divides_b n1 m with
+((match divides_b n1 m with
[ true \Rightarrow n1
| false \Rightarrow gcd_aux n n1 (m \mod n1)]) \divides m \land
(match divides_b n1 m with
[ true \Rightarrow n1
-| false \Rightarrow gcd_aux n n1 (m \mod n1)]) \divides n1.
+| false \Rightarrow gcd_aux n n1 (m \mod n1)]) \divides n1).
elim Hcut.rewrite > divides_to_divides_b_true.
simplify.
-split.assumption.apply witness n1 n1 (S O).apply times_n_SO.
+split.assumption.apply (witness n1 n1 (S O)).apply times_n_SO.
assumption.assumption.
rewrite > not_divides_to_divides_b_false.
change with
-gcd_aux n n1 (m \mod n1) \divides m \land
-gcd_aux n n1 (m \mod n1) \divides n1.
-cut gcd_aux n n1 (m \mod n1) \divides n1 \land
-gcd_aux n n1 (m \mod n1) \divides mod m n1.
+(gcd_aux n n1 (m \mod n1) \divides m \land
+gcd_aux n n1 (m \mod n1) \divides n1).
+cut (gcd_aux n n1 (m \mod n1) \divides n1 \land
+gcd_aux n n1 (m \mod n1) \divides mod m n1).
elim Hcut1.
-split.apply divides_mod_to_divides ? ? n1.
+split.apply (divides_mod_to_divides ? ? n1).
assumption.assumption.assumption.assumption.
apply H.
-cut O \lt m \mod n1 \lor O = mod m n1.
+cut (O \lt m \mod n1 \lor O = mod m n1).
elim Hcut1.assumption.
apply False_ind.apply H4.apply mod_O_to_divides.
assumption.apply sym_eq.assumption.
apply lt_to_le.
apply lt_mod_m_m.assumption.
apply le_S_S_to_le.
-apply trans_le ? n1.
-change with m \mod n1 < n1.
+apply (trans_le ? n1).
+change with (m \mod n1 < n1).
apply lt_mod_m_m.assumption.assumption.
assumption.assumption.
-apply decidable_divides n1 m.assumption.
+apply (decidable_divides n1 m).assumption.
qed.
theorem divides_gcd_nm: \forall n,m.
gcd n m \divides m \land gcd n m \divides n.
intros.
change with
-match leb n m with
+(match leb n m with
[ true \Rightarrow
match n with
[ O \Rightarrow m
| false \Rightarrow
match m with
[ O \Rightarrow n
- | (S p) \Rightarrow gcd_aux (S p) n (S p) ] ] \divides n.
-apply leb_elim n m.
-apply nat_case1 n.
+ | (S p) \Rightarrow gcd_aux (S p) n (S p) ] ] \divides n).
+apply (leb_elim n m).
+apply (nat_case1 n).
simplify.intros.split.
-apply witness m m (S O).apply times_n_SO.
-apply witness m O O.apply times_n_O.
+apply (witness m m (S O)).apply times_n_SO.
+apply (witness m O O).apply times_n_O.
intros.change with
-gcd_aux (S m1) m (S m1) \divides m
+(gcd_aux (S m1) m (S m1) \divides m
\land
-gcd_aux (S m1) m (S m1) \divides (S m1).
+gcd_aux (S m1) m (S m1) \divides (S m1)).
apply divides_gcd_aux_mn.
simplify.apply le_S_S.apply le_O_n.
assumption.apply le_n.
simplify.intro.
-apply nat_case1 m.
+apply (nat_case1 m).
simplify.intros.split.
-apply witness n O O.apply times_n_O.
-apply witness n n (S O).apply times_n_SO.
+apply (witness n O O).apply times_n_O.
+apply (witness n n (S O)).apply times_n_SO.
intros.change with
-gcd_aux (S m1) n (S m1) \divides (S m1)
+(gcd_aux (S m1) n (S m1) \divides (S m1)
\land
-gcd_aux (S m1) n (S m1) \divides n.
-cut gcd_aux (S m1) n (S m1) \divides n
+gcd_aux (S m1) n (S m1) \divides n).
+cut (gcd_aux (S m1) n (S m1) \divides n
\land
-gcd_aux (S m1) n (S m1) \divides S m1.
+gcd_aux (S m1) n (S m1) \divides S m1).
elim Hcut.split.assumption.assumption.
apply divides_gcd_aux_mn.
simplify.apply le_S_S.apply le_O_n.
apply not_lt_to_le.simplify.intro.apply H.
-rewrite > H1.apply trans_le ? (S n).
+rewrite > H1.apply (trans_le ? (S n)).
apply le_n_Sn.assumption.apply le_n.
qed.
theorem divides_gcd_n: \forall n,m. gcd n m \divides n.
intros.
-exact proj2 ? ? (divides_gcd_nm n m).
+exact (proj2 ? ? (divides_gcd_nm n m)).
qed.
theorem divides_gcd_m: \forall n,m. gcd n m \divides m.
intros.
-exact proj1 ? ? (divides_gcd_nm n m).
+exact (proj1 ? ? (divides_gcd_nm n m)).
qed.
theorem divides_gcd_aux: \forall p,m,n,d. O < n \to n \le m \to n \le p \to
d \divides m \to d \divides n \to d \divides gcd_aux p m n.
intro.elim p.
-absurd O < n.assumption.apply le_to_not_lt.assumption.
+absurd (O < n).assumption.apply le_to_not_lt.assumption.
change with
-d \divides
+(d \divides
(match divides_b n1 m with
[ true \Rightarrow n1
-| false \Rightarrow gcd_aux n n1 (m \mod n1)]).
-cut n1 \divides m \lor n1 \ndivides m.
+| false \Rightarrow gcd_aux n n1 (m \mod n1)])).
+cut (n1 \divides m \lor n1 \ndivides m).
elim Hcut.
rewrite > divides_to_divides_b_true.
simplify.assumption.
assumption.assumption.
rewrite > not_divides_to_divides_b_false.
-change with d \divides gcd_aux n n1 (m \mod n1).
+change with (d \divides gcd_aux n n1 (m \mod n1)).
apply H.
-cut O \lt m \mod n1 \lor O = m \mod n1.
+cut (O \lt m \mod n1 \lor O = m \mod n1).
elim Hcut1.assumption.
-absurd n1 \divides m.apply mod_O_to_divides.
+absurd (n1 \divides m).apply mod_O_to_divides.
assumption.apply sym_eq.assumption.assumption.
apply le_to_or_lt_eq.apply le_O_n.
apply lt_to_le.
apply lt_mod_m_m.assumption.
apply le_S_S_to_le.
-apply trans_le ? n1.
-change with m \mod n1 < n1.
+apply (trans_le ? n1).
+change with (m \mod n1 < n1).
apply lt_mod_m_m.assumption.assumption.
assumption.
apply divides_mod.assumption.assumption.assumption.
assumption.assumption.
-apply decidable_divides n1 m.assumption.
+apply (decidable_divides n1 m).assumption.
qed.
theorem divides_d_gcd: \forall m,n,d.
d \divides m \to d \divides n \to d \divides gcd n m.
intros.
change with
-d \divides
+(d \divides
match leb n m with
[ true \Rightarrow
match n with
| false \Rightarrow
match m with
[ O \Rightarrow n
- | (S p) \Rightarrow gcd_aux (S p) n (S p) ]].
-apply leb_elim n m.
-apply nat_case1 n.simplify.intros.assumption.
+ | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]).
+apply (leb_elim n m).
+apply (nat_case1 n).simplify.intros.assumption.
intros.
-change with d \divides gcd_aux (S m1) m (S m1).
+change with (d \divides gcd_aux (S m1) m (S m1)).
apply divides_gcd_aux.
simplify.apply le_S_S.apply le_O_n.assumption.apply le_n.assumption.
rewrite < H2.assumption.
-apply nat_case1 m.simplify.intros.assumption.
+apply (nat_case1 m).simplify.intros.assumption.
intros.
-change with d \divides gcd_aux (S m1) n (S m1).
+change with (d \divides gcd_aux (S m1) n (S m1)).
apply divides_gcd_aux.
simplify.apply le_S_S.apply le_O_n.
apply lt_to_le.apply not_le_to_lt.assumption.apply le_n.assumption.
\exists a,b. a*n - b*m = gcd_aux p m n \lor b*m - a*n = gcd_aux p m n.
intro.
elim p.
-absurd O < n.assumption.apply le_to_not_lt.assumption.
-cut O < m.
-cut n1 \divides m \lor n1 \ndivides m.
+absurd (O < n).assumption.apply le_to_not_lt.assumption.
+cut (O < m).
+cut (n1 \divides m \lor n1 \ndivides m).
change with
-\exists a,b.
+(\exists a,b.
a*n1 - b*m = match divides_b n1 m with
[ true \Rightarrow n1
| false \Rightarrow gcd_aux n n1 (m \mod n1)]
\lor
b*m - a*n1 = match divides_b n1 m with
[ true \Rightarrow n1
-| false \Rightarrow gcd_aux n n1 (m \mod n1)].
+| false \Rightarrow gcd_aux n n1 (m \mod n1)]).
elim Hcut1.
rewrite > divides_to_divides_b_true.
simplify.
-apply ex_intro ? ? (S O).
-apply ex_intro ? ? O.
+apply (ex_intro ? ? (S O)).
+apply (ex_intro ? ? O).
left.simplify.rewrite < plus_n_O.
apply sym_eq.apply minus_n_O.
assumption.assumption.
rewrite > not_divides_to_divides_b_false.
change with
-\exists a,b.
+(\exists a,b.
a*n1 - b*m = gcd_aux n n1 (m \mod n1)
\lor
-b*m - a*n1 = gcd_aux n n1 (m \mod n1).
+b*m - a*n1 = gcd_aux n n1 (m \mod n1)).
cut
-\exists a,b.
+(\exists a,b.
a*(m \mod n1) - b*n1= gcd_aux n n1 (m \mod n1)
\lor
-b*n1 - a*(m \mod n1) = gcd_aux n n1 (m \mod n1).
+b*n1 - a*(m \mod n1) = gcd_aux n n1 (m \mod n1)).
elim Hcut2.elim H5.elim H6.
(* first case *)
rewrite < H7.
-apply ex_intro ? ? (a1+a*(m / n1)).
-apply ex_intro ? ? a.
+apply (ex_intro ? ? (a1+a*(m / n1))).
+apply (ex_intro ? ? a).
right.
rewrite < sym_plus.
-rewrite < sym_times n1.
+rewrite < (sym_times n1).
rewrite > distr_times_plus.
-rewrite > sym_times n1.
-rewrite > sym_times n1.
-rewrite > div_mod m n1 in \vdash (? ? (? % ?) ?).
+rewrite > (sym_times n1).
+rewrite > (sym_times n1).
+rewrite > (div_mod m n1) in \vdash (? ? (? % ?) ?).
rewrite > assoc_times.
rewrite < sym_plus.
rewrite > distr_times_plus.
assumption.
(* second case *)
rewrite < H7.
-apply ex_intro ? ? (a1+a*(m / n1)).
-apply ex_intro ? ? a.
+apply (ex_intro ? ? (a1+a*(m / n1))).
+apply (ex_intro ? ? a).
left.
(* clear Hcut2.clear H5.clear H6.clear H. *)
rewrite > sym_times.
rewrite > distr_times_plus.
rewrite > sym_times.
-rewrite > sym_times n1.
-rewrite > div_mod m n1 in \vdash (? ? (? ? %) ?).
+rewrite > (sym_times n1).
+rewrite > (div_mod m n1) in \vdash (? ? (? ? %) ?).
rewrite > distr_times_plus.
rewrite > assoc_times.
rewrite < eq_minus_minus_minus_plus.
rewrite < minus_n_n.reflexivity.
apply le_n.
assumption.
-apply H n1 (m \mod n1).
-cut O \lt m \mod n1 \lor O = m \mod n1.
+apply (H n1 (m \mod n1)).
+cut (O \lt m \mod n1 \lor O = m \mod n1).
elim Hcut2.assumption.
-absurd n1 \divides m.apply mod_O_to_divides.
+absurd (n1 \divides m).apply mod_O_to_divides.
assumption.
symmetry.assumption.assumption.
apply le_to_or_lt_eq.apply le_O_n.
apply lt_to_le.
apply lt_mod_m_m.assumption.
apply le_S_S_to_le.
-apply trans_le ? n1.
-change with m \mod n1 < n1.
+apply (trans_le ? n1).
+change with (m \mod n1 < n1).
apply lt_mod_m_m.
assumption.assumption.assumption.assumption.
-apply decidable_divides n1 m.assumption.
-apply lt_to_le_to_lt ? n1.assumption.assumption.
+apply (decidable_divides n1 m).assumption.
+apply (lt_to_le_to_lt ? n1).assumption.assumption.
qed.
theorem eq_minus_gcd:
\forall m,n.\exists a,b.a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m).
intros.
unfold gcd.
-apply leb_elim n m.
-apply nat_case1 n.
+apply (leb_elim n m).
+apply (nat_case1 n).
simplify.intros.
-apply ex_intro ? ? O.
-apply ex_intro ? ? (S O).
+apply (ex_intro ? ? O).
+apply (ex_intro ? ? (S O)).
right.simplify.
rewrite < plus_n_O.
apply sym_eq.apply minus_n_O.
intros.
change with
-\exists a,b.
+(\exists a,b.
a*(S m1) - b*m = (gcd_aux (S m1) m (S m1))
-\lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1)).
+\lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1))).
apply eq_minus_gcd_aux.
simplify. apply le_S_S.apply le_O_n.
assumption.apply le_n.
-apply nat_case1 m.
+apply (nat_case1 m).
simplify.intros.
-apply ex_intro ? ? (S O).
-apply ex_intro ? ? O.
+apply (ex_intro ? ? (S O)).
+apply (ex_intro ? ? O).
left.simplify.
rewrite < plus_n_O.
apply sym_eq.apply minus_n_O.
intros.
change with
-\exists a,b.
+(\exists a,b.
a*n - b*(S m1) = (gcd_aux (S m1) n (S m1))
-\lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1)).
+\lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1))).
cut
-\exists a,b.
+(\exists a,b.
a*(S m1) - b*n = (gcd_aux (S m1) n (S m1))
\lor
-b*n - a*(S m1) = (gcd_aux (S m1) n (S m1)).
+b*n - a*(S m1) = (gcd_aux (S m1) n (S m1))).
elim Hcut.elim H2.elim H3.
-apply ex_intro ? ? a1.
-apply ex_intro ? ? a.
+apply (ex_intro ? ? a1).
+apply (ex_intro ? ? a).
right.assumption.
-apply ex_intro ? ? a1.
-apply ex_intro ? ? a.
+apply (ex_intro ? ? a1).
+apply (ex_intro ? ? a).
left.assumption.
apply eq_minus_gcd_aux.
simplify. apply le_S_S.apply le_O_n.
theorem gcd_O_to_eq_O:\forall m,n:nat. (gcd m n) = O \to
m = O \land n = O.
-intros.cut O \divides n \land O \divides m.
+intros.cut (O \divides n \land O \divides m).
elim Hcut.elim H2.split.
assumption.elim H1.assumption.
rewrite < H.
theorem symmetric_gcd: symmetric nat gcd.
change with
-\forall n,m:nat. gcd n m = gcd m n.
+(\forall n,m:nat. gcd n m = gcd m n).
intros.
-cut O < (gcd n m) \lor O = (gcd n m).
+cut (O < (gcd n m) \lor O = (gcd n m)).
elim Hcut.
-cut O < (gcd m n) \lor O = (gcd m n).
+cut (O < (gcd m n) \lor O = (gcd m n)).
elim Hcut1.
apply antisym_le.
apply divides_to_le.assumption.
apply divides_to_le.assumption.
apply divides_d_gcd.apply divides_gcd_n.apply divides_gcd_m.
rewrite < H1.
-cut m=O \land n=O.
+cut (m=O \land n=O).
elim Hcut2.rewrite > H2.rewrite > H3.reflexivity.
apply gcd_O_to_eq_O.apply sym_eq.assumption.
apply le_to_or_lt_eq.apply le_O_n.
rewrite < H.
-cut n=O \land m=O.
+cut (n=O \land m=O).
elim Hcut1.rewrite > H1.rewrite > H2.reflexivity.
apply gcd_O_to_eq_O.apply sym_eq.assumption.
apply le_to_or_lt_eq.apply le_O_n.
intro.
apply antisym_le.apply divides_to_le.simplify.apply le_n.
apply divides_gcd_n.
-cut O < gcd (S O) n \lor O = gcd (S O) n.
+cut (O < gcd (S O) n \lor O = gcd (S O) n).
elim Hcut.assumption.
apply False_ind.
-apply not_eq_O_S O.
-cut (S O)=O \land n=O.
+apply (not_eq_O_S O).
+cut ((S O)=O \land n=O).
elim Hcut1.apply sym_eq.assumption.
apply gcd_O_to_eq_O.apply sym_eq.assumption.
apply le_to_or_lt_eq.apply le_O_n.
theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to n \ndivides m \to
gcd n m = (S O).
-intros.simplify in H.change with gcd n m = (S O).
+intros.simplify in H.change with (gcd n m = (S O)).
elim H.
apply antisym_le.
apply not_lt_to_le.
-change with (S (S O)) \le gcd n m \to False.intro.
-apply H1.rewrite < H3 (gcd n m).
+change with ((S (S O)) \le gcd n m \to False).intro.
+apply H1.rewrite < (H3 (gcd n m)).
apply divides_gcd_m.
apply divides_gcd_n.assumption.
-cut O < gcd n m \lor O = gcd n m.
+cut (O < gcd n m \lor O = gcd n m).
elim Hcut.assumption.
apply False_ind.
-apply not_le_Sn_O (S O).
-cut n=O \land m=O.
+apply (not_le_Sn_O (S O)).
+cut (n=O \land m=O).
elim Hcut1.rewrite < H5 in \vdash (? ? %).assumption.
apply gcd_O_to_eq_O.apply sym_eq.assumption.
apply le_to_or_lt_eq.apply le_O_n.
theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to n \divides p*q \to
n \divides p \lor n \divides q.
intros.
-cut n \divides p \lor n \ndivides p.
+cut (n \divides p \lor n \ndivides p).
elim Hcut.
left.assumption.
right.
-cut \exists a,b. a*n - b*p = (S O) \lor b*p - a*n = (S O).
+cut (\exists a,b. a*n - b*p = (S O) \lor b*p - a*n = (S O)).
elim Hcut1.elim H3.elim H4.
(* first case *)
-rewrite > times_n_SO q.rewrite < H5.
+rewrite > (times_n_SO q).rewrite < H5.
rewrite > distr_times_minus.
-rewrite > sym_times q (a1*p).
-rewrite > assoc_times a1.
+rewrite > (sym_times q (a1*p)).
+rewrite > (assoc_times a1).
elim H1.rewrite > H6.
-rewrite < sym_times n.rewrite < assoc_times.
-rewrite > sym_times q.rewrite > assoc_times.
-rewrite < assoc_times a1.rewrite < sym_times n.
-rewrite > assoc_times n.
+rewrite < (sym_times n).rewrite < assoc_times.
+rewrite > (sym_times q).rewrite > assoc_times.
+rewrite < (assoc_times a1).rewrite < (sym_times n).
+rewrite > (assoc_times n).
rewrite < distr_times_minus.
-apply witness ? ? (q*a-a1*n2).reflexivity.
+apply (witness ? ? (q*a-a1*n2)).reflexivity.
(* second case *)
-rewrite > times_n_SO q.rewrite < H5.
+rewrite > (times_n_SO q).rewrite < H5.
rewrite > distr_times_minus.
-rewrite > sym_times q (a1*p).
-rewrite > assoc_times a1.
+rewrite > (sym_times q (a1*p)).
+rewrite > (assoc_times a1).
elim H1.rewrite > H6.
rewrite < sym_times.rewrite > assoc_times.
-rewrite < assoc_times q.
-rewrite < sym_times n.
+rewrite < (assoc_times q).
+rewrite < (sym_times n).
rewrite < distr_times_minus.
-apply witness ? ? (n2*a1-q*a).reflexivity.
+apply (witness ? ? (n2*a1-q*a)).reflexivity.
(* end second case *)
-rewrite < prime_to_gcd_SO n p.
+rewrite < (prime_to_gcd_SO n p).
apply eq_minus_gcd.
assumption.assumption.
-apply decidable_divides n p.
-apply trans_lt ? (S O).simplify.apply le_n.
+apply (decidable_divides n p).
+apply (trans_lt ? (S O)).simplify.apply le_n.
simplify in H.elim H. assumption.
qed.
theorem monotonic_le_plus_l:
\forall m:nat.monotonic nat le (\lambda n.n + m).
simplify.intros.
-rewrite < sym_plus.rewrite < sym_plus m.
+rewrite < sym_plus.rewrite < (sym_plus m).
apply le_plus_r.assumption.
qed.
theorem le_plus: \forall n1,n2,m1,m2:nat. n1 \le n2 \to m1 \le m2
\to n1 + m1 \le n2 + m2.
intros.
-apply trans_le ? (n2 + m1).
+apply (trans_le ? (n2 + m1)).
apply le_plus_l.assumption.
apply le_plus_r.assumption.
qed.
theorem le_plus_n :\forall n,m:nat. m \le n + m.
-intros.change with O+m \le n+m.
+intros.change with (O+m \le n+m).
apply le_plus_l.apply le_O_n.
qed.
theorem monotonic_le_times_l:
\forall m:nat.monotonic nat le (\lambda n.n*m).
simplify.intros.
-rewrite < sym_times.rewrite < sym_times m.
+rewrite < sym_times.rewrite < (sym_times m).
apply le_times_r.assumption.
qed.
theorem le_times: \forall n1,n2,m1,m2:nat. n1 \le n2 \to m1 \le m2
\to n1*m1 \le n2*m2.
intros.
-apply trans_le ? (n2*m1).
+apply (trans_le ? (n2*m1)).
apply le_times_l.assumption.
apply le_times_r.assumption.
qed.
elim (plus_n_O ?).apply le_n.
simplify.rewrite < sym_plus.apply le_plus_n.
qed.
-
theorem monotonic_lt_plus_l:
\forall n:nat.monotonic nat lt (\lambda m.m+n).
-change with \forall n,p,q:nat. p < q \to p + n < q + n.
+change with (\forall n,p,q:nat. p < q \to p + n < q + n).
intros.
-rewrite < sym_plus. rewrite < sym_plus n.
+rewrite < sym_plus. rewrite < (sym_plus n).
apply lt_plus_r.assumption.
qed.
theorem lt_plus: \forall n,m,p,q:nat. n < m \to p < q \to n + p < m + q.
intros.
-apply trans_lt ? (n + q).
+apply (trans_lt ? (n + q)).
apply lt_plus_r.assumption.
apply lt_plus_l.assumption.
qed.
theorem lt_plus_to_lt_l :\forall n,p,q:nat. p+n < q+n \to p<q.
intro.elim n.
rewrite > plus_n_O.
-rewrite > plus_n_O q.assumption.
+rewrite > (plus_n_O q).assumption.
apply H.
simplify.apply le_S_S_to_le.
rewrite > plus_n_Sm.
-rewrite > plus_n_Sm q.
+rewrite > (plus_n_Sm q).
exact H1.
qed.
theorem lt_plus_to_lt_r :\forall n,p,q:nat. n+p < n+q \to p<q.
-intros.apply lt_plus_to_lt_l n.
+intros.apply (lt_plus_to_lt_l n).
rewrite > sym_plus.
-rewrite > sym_plus q.assumption.
+rewrite > (sym_plus q).assumption.
qed.
(* times and zero *)
(* times *)
theorem monotonic_lt_times_r:
\forall n:nat.monotonic nat lt (\lambda m.(S n)*m).
-change with \forall n,p,q:nat. p < q \to (S n) * p < (S n) * q.
+change with (\forall n,p,q:nat. p < q \to (S n) * p < (S n) * q).
intros.elim n.
simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption.
-change with p + (S n1) * p < q + (S n1) * q.
+change with (p + (S n1) * p < q + (S n1) * q).
apply lt_plus.assumption.assumption.
qed.
theorem monotonic_lt_times_l:
\forall m:nat.monotonic nat lt (\lambda n.n * (S m)).
change with
-\forall n,p,q:nat. p < q \to p*(S n) < q*(S n).
+(\forall n,p,q:nat. p < q \to p*(S n) < q*(S n)).
intros.
-rewrite < sym_times.rewrite < sym_times (S n).
+rewrite < sym_times.rewrite < (sym_times (S n)).
apply lt_times_r.assumption.
qed.
theorem lt_times:\forall n,m,p,q:nat. n<m \to p<q \to n*p < m*q.
intro.
elim n.
-apply lt_O_n_elim m H.
+apply (lt_O_n_elim m H).
intro.
-cut lt O q.
-apply lt_O_n_elim q Hcut.
-intro.change with O < (S m1)*(S m2).
+cut (lt O q).
+apply (lt_O_n_elim q Hcut).
+intro.change with (O < (S m1)*(S m2)).
apply lt_O_times_S_S.
-apply ltn_to_ltO p q H1.
-apply trans_lt ? ((S n1)*q).
+apply (ltn_to_ltO p q H1).
+apply (trans_lt ? ((S n1)*q)).
apply lt_times_r.assumption.
-cut lt O q.
-apply lt_O_n_elim q Hcut.
+cut (lt O q).
+apply (lt_O_n_elim q Hcut).
intro.
apply lt_times_l.
assumption.
-apply ltn_to_ltO p q H2.
+apply (ltn_to_ltO p q H2).
qed.
theorem lt_times_to_lt_l:
\forall n,p,q:nat. p*(S n) < q*(S n) \to p < q.
intros.
-cut p < q \lor p \nlt q.
+cut (p < q \lor p \nlt q).
elim Hcut.
assumption.
-absurd p * (S n) < q * (S n).
+absurd (p * (S n) < q * (S n)).
assumption.
apply le_to_not_lt.
apply le_times_l.
apply not_lt_to_le.
assumption.
-exact decidable_lt p q.
+exact (decidable_lt p q).
qed.
theorem lt_times_to_lt_r:
\forall n,p,q:nat. (S n)*p < (S n)*q \to lt p q.
intros.
-apply lt_times_to_lt_l n.
+apply (lt_times_to_lt_l n).
rewrite < sym_times.
-rewrite < sym_times (S n).
+rewrite < (sym_times (S n)).
assumption.
qed.
intros.apply nat_compare_elim.intro.
apply nat_compare_elim.
intro.reflexivity.
-intro.absurd p=q.
-apply inj_times_r n.assumption.
+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.
+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.
+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.
+intro.absurd (q=p).
symmetry.
-apply inj_times_r n.assumption.
+apply (inj_times_r n).assumption.
apply lt_to_not_eq.assumption.
intro.reflexivity.
qed.
(* div *)
theorem eq_mod_O_to_lt_O_div: \forall n,m:nat. O < m \to O < n\to n \mod m = O \to O < n / m.
-intros 4.apply lt_O_n_elim m H.intros.
-apply lt_times_to_lt_r m1.
+intros 4.apply (lt_O_n_elim m H).intros.
+apply (lt_times_to_lt_r m1).
rewrite < times_n_O.
-rewrite > plus_n_O ((S m1)*(n / (S m1))).
+rewrite > (plus_n_O ((S m1)*(n / (S m1)))).
rewrite < H2.
rewrite < sym_times.
rewrite < div_mod.
theorem lt_div_n_m_n: \forall n,m:nat. (S O) < m \to O < n \to n / m \lt n.
intros.
-apply nat_case1 (n / m).intro.
+apply (nat_case1 (n / m)).intro.
assumption.intros.rewrite < H2.
rewrite > (div_mod n m) in \vdash (? ? %).
-apply lt_to_le_to_lt ? ((n / m)*m).
-apply lt_to_le_to_lt ? ((n / m)*(S (S O))).
+apply (lt_to_le_to_lt ? ((n / m)*m)).
+apply (lt_to_le_to_lt ? ((n / m)*(S (S O)))).
rewrite < sym_times.
rewrite > H2.
simplify.
assumption.
rewrite < sym_plus.
apply le_plus_n.
-apply trans_lt ? (S O).
+apply (trans_lt ? (S O)).
simplify. apply le_n.assumption.
qed.
theorem monotonic_to_injective: \forall f:nat\to nat.
monotonic nat lt f \to injective nat nat f.
simplify.intros.
-apply nat_compare_elim x y.
-intro.apply False_ind.apply not_le_Sn_n (f x).
+apply (nat_compare_elim x y).
+intro.apply False_ind.apply (not_le_Sn_n (f x)).
rewrite > H1 in \vdash (? ? %).apply H.apply H2.
intros.assumption.
-intro.apply False_ind.apply not_le_Sn_n (f y).
+intro.apply False_ind.apply (not_le_Sn_n (f y)).
rewrite < H1 in \vdash (? ? %).apply H.apply H2.
qed.
theorem max_O_f : \forall f: nat \to bool. max O f = O.
intro. simplify.
-elim f O.
+elim (f O).
simplify.reflexivity.
simplify.reflexivity.
qed.
n\le m \to max n f \le max m f.
intros.elim H.
apply le_n.
-apply trans_le ? (max n1 f).apply H2.
-cut (f (S n1) = true \land max (S n1) f = (S n1)) \lor
-(f (S n1) = false \land max (S n1) f = max n1 f).
+apply (trans_le ? (max n1 f)).apply H2.
+cut ((f (S n1) = true \land max (S n1) f = (S n1)) \lor
+(f (S n1) = false \land max (S n1) f = max n1 f)).
elim Hcut.elim H3.
rewrite > H5.
apply le_S.apply le_max_n.
theorem f_m_to_le_max: \forall f: nat \to bool. \forall n,m:nat.
m\le n \to f m = true \to m \le max n f.
-intros 3.elim n.apply le_n_O_elim m H.
+intros 3.elim n.apply (le_n_O_elim m H).
apply le_O_n.
-apply le_n_Sm_elim m n1 H1.
-intro.apply trans_le ? (max n1 f).
+apply (le_n_Sm_elim m n1 H1).
+intro.apply (trans_le ? (max n1 f)).
apply H.apply le_S_S_to_le.assumption.assumption.
apply le_to_le_max.apply le_n_Sn.
intro.simplify.rewrite < H3.
(\exists i:nat. le i n \land f i = true) \to f (max n f) = true.
intros 2.
elim n.elim H.elim H1.generalize in match H3.
-apply le_n_O_elim a H2.intro.simplify.rewrite > H4.
+apply (le_n_O_elim a H2).intro.simplify.rewrite > H4.
simplify.assumption.
simplify.
-apply bool_ind (\lambda b:bool.
+apply (bool_ind (\lambda b:bool.
(f (S n1) = b) \to (f ([\lambda b:bool.nat] match b in bool with
[ true \Rightarrow (S n1)
-| false \Rightarrow (max n1 f)])) = true).
+| false \Rightarrow (max n1 f)])) = true)).
simplify.intro.assumption.
simplify.intro.apply H.
elim H1.elim H3.generalize in match H5.
-apply le_n_Sm_elim a n1 H4.
+apply (le_n_Sm_elim a n1 H4).
intros.
-apply ex_intro nat ? a.
+apply (ex_intro nat ? a).
split.apply le_S_S_to_le.assumption.assumption.
intros.apply False_ind.apply not_eq_true_false.
rewrite < H2.rewrite < H7.rewrite > H6. reflexivity.
theorem lt_max_to_false : \forall f:nat \to bool.
\forall n,m:nat. (max n f) < m \to m \leq n \to f m = false.
intros 2.
-elim n.absurd le m O.assumption.
-cut O < m.apply lt_O_n_elim m Hcut.exact not_le_Sn_O.
-rewrite < max_O_f f.assumption.
+elim n.absurd (le m O).assumption.
+cut (O < m).apply (lt_O_n_elim m Hcut).exact not_le_Sn_O.
+rewrite < (max_O_f f).assumption.
generalize in match H1.
-elim max_S_max f n1.
+elim (max_S_max f n1).
elim H3.
-absurd m \le S n1.assumption.
+absurd (m \le S n1).assumption.
apply lt_to_not_le.rewrite < H6.assumption.
elim H3.
-apply le_n_Sm_elim m n1 H2.
+apply (le_n_Sm_elim m n1 H2).
intro.
apply H.rewrite < H6.assumption.
apply le_S_S_to_le.assumption.
theorem min_aux_O_f: \forall f:nat \to bool. \forall i :nat.
min_aux O i f = i.
intros.simplify.rewrite < minus_n_O.
-elim f i.
-simplify.reflexivity.
+elim (f i).reflexivity.
simplify.reflexivity.
qed.
theorem min_O_f : \forall f:nat \to bool.
min O f = O.
-intro.apply min_aux_O_f f O.
+intro.apply (min_aux_O_f f O).
qed.
theorem min_aux_S : \forall f: nat \to bool. \forall i,n:nat.
f (min_aux off m f) = true.
intros 2.
elim off.elim H.elim H1.elim H2.
-cut a = m.
-rewrite > min_aux_O_f f.rewrite < Hcut.assumption.
-apply antisym_le a m .assumption.rewrite > minus_n_O m.assumption.
+cut (a = m).
+rewrite > (min_aux_O_f f).rewrite < Hcut.assumption.
+apply (antisym_le a m).assumption.rewrite > (minus_n_O m).assumption.
simplify.
-apply bool_ind (\lambda b:bool.
+apply (bool_ind (\lambda b:bool.
(f (m-(S n)) = b) \to (f ([\lambda b:bool.nat] match b in bool with
[ true \Rightarrow m-(S n)
-| false \Rightarrow (min_aux n m f)])) = true).
+| false \Rightarrow (min_aux n m f)])) = true)).
simplify.intro.assumption.
simplify.intro.apply H.
elim H1.elim H3.elim H4.
elim (le_to_or_lt_eq (m-(S n)) a H6).
-apply ex_intro nat ? a.
+apply (ex_intro nat ? a).
split.split.
apply lt_minus_S_n_to_le_minus_n.assumption.
assumption.assumption.
-absurd f a = false.rewrite < H8.assumption.
+absurd (f a = false).rewrite < H8.assumption.
rewrite > H5.
apply not_eq_true_false.
reflexivity.
theorem lt_min_aux_to_false : \forall f:nat \to bool.
\forall n,off,m:nat. (n-off) \leq m \to m < (min_aux off n f) \to f m = false.
intros 3.
-elim off.absurd le n m.rewrite > minus_n_O.assumption.
-apply lt_to_not_le.rewrite < min_aux_O_f f n.assumption.
+elim off.absurd (le n m).rewrite > minus_n_O.assumption.
+apply lt_to_not_le.rewrite < (min_aux_O_f f n).assumption.
generalize in match H1.
-elim min_aux_S f n1 n.
+elim (min_aux_S f n1 n).
elim H3.
-absurd n - S n1 \le m.assumption.
+absurd (n - S n1 \le m).assumption.
apply lt_to_not_le.rewrite < H6.assumption.
elim H3.
-elim le_to_or_lt_eq (n -(S n1)) m.
+elim (le_to_or_lt_eq (n -(S n1)) m).
apply H.apply lt_minus_S_n_to_le_minus_n.assumption.
rewrite < H6.assumption.
rewrite < H7.assumption.
\forall n,off:nat. (n-off) \leq (min_aux off n f).
intros 3.
elim off.rewrite < minus_n_O.
-rewrite > min_aux_O_f f n.apply le_n.
-elim min_aux_S f n1 n.
+rewrite > (min_aux_O_f f n).apply le_n.
+elim (min_aux_S f n1 n).
elim H1.rewrite > H3.apply le_n.
elim H1.rewrite > H3.
-apply trans_le (n-(S n1)) (n-n1).
+apply (trans_le (n-(S n1)) (n-n1)).
apply monotonic_le_minus_r.
apply le_n_Sn.
assumption.
theorem minus_Sn_m: \forall n,m:nat. m \leq n \to (S n)-m = S (n-m).
intros 2.
-apply nat_elim2
-(\lambda n,m.m \leq n \to (S n)-m = S (n-m)).
-intros.apply le_n_O_elim n1 H.
+apply (nat_elim2
+(\lambda n,m.m \leq n \to (S n)-m = S (n-m))).
+intros.apply (le_n_O_elim n1 H).
simplify.reflexivity.
intros.simplify.reflexivity.
intros.rewrite < H.reflexivity.
theorem plus_minus:
\forall n,m,p:nat. m \leq n \to (n-m)+p = (n+p)-m.
intros 2.
-apply nat_elim2
-(\lambda n,m.\forall p:nat.m \leq n \to (n-m)+p = (n+p)-m).
-intros.apply le_n_O_elim ? H.
+apply (nat_elim2
+(\lambda n,m.\forall p:nat.m \leq n \to (n-m)+p = (n+p)-m)).
+intros.apply (le_n_O_elim ? H).
simplify.rewrite < minus_n_O.reflexivity.
intros.simplify.reflexivity.
intros.simplify.apply H.apply le_S_S_to_le.assumption.
elim n2.simplify.
apply minus_n_n.
rewrite < plus_n_Sm.
-change with S n3 = (S n3 + n1)-n1.
+change with (S n3 = (S n3 + n1)-n1).
apply H.
qed.
theorem plus_minus_m_m: \forall n,m:nat.
m \leq n \to n = (n-m)+m.
intros 2.
-apply nat_elim2 (\lambda n,m.m \leq n \to n = (n-m)+m).
-intros.apply le_n_O_elim n1 H.
+apply (nat_elim2 (\lambda n,m.m \leq n \to n = (n-m)+m)).
+intros.apply (le_n_O_elim n1 H).
reflexivity.
intros.simplify.rewrite < plus_n_O.reflexivity.
intros.simplify.rewrite < sym_plus.simplify.
theorem minus_to_plus :\forall n,m,p:nat.m \leq n \to n-m = p \to
n = m+p.
-intros.apply trans_eq ? ? ((n-m)+m).
+intros.apply (trans_eq ? ? ((n-m)+m)).
apply plus_minus_m_m.
apply H.elim H1.
apply sym_plus.
theorem plus_to_minus :\forall n,m,p:nat.
n = m+p \to n-m = p.
intros.
-apply inj_plus_r m.
+apply (inj_plus_r m).
rewrite < H.
rewrite < sym_plus.
symmetry.
theorem minus_pred_pred : \forall n,m:nat. lt O n \to lt O m \to
eq nat (minus (pred n) (pred m)) (minus n m).
intros.
-apply lt_O_n_elim n H.intro.
-apply lt_O_n_elim m H1.intro.
+apply (lt_O_n_elim n H).intro.
+apply (lt_O_n_elim m H1).intro.
simplify.reflexivity.
qed.
theorem eq_minus_n_m_O: \forall n,m:nat.
n \leq m \to n-m = O.
intros 2.
-apply nat_elim2 (\lambda n,m.n \leq m \to n-m = O).
+apply (nat_elim2 (\lambda n,m.n \leq m \to n-m = O)).
intros.simplify.reflexivity.
intros.apply False_ind.
apply not_le_Sn_O.
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.
+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))).
+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.
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.simplify.intro.
-apply trans_le (m-n) (S (m-(S n))) p.
+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.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.
+intros.apply (lt_O_n_elim n H).intro.
+apply (lt_O_n_elim m H1).intro.
simplify.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).
+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.
(* galois *)
theorem monotonic_le_minus_r:
\forall p,q,n:nat. q \leq p \to n-p \le n-q.
-simplify.intros 2.apply nat_elim2
-(\lambda p,q.\forall a.q \leq p \to a-p \leq a-q).
-intros.apply le_n_O_elim n H.apply le_n.
+simplify.intros 2.apply (nat_elim2
+(\lambda p,q.\forall a.q \leq p \to a-p \leq a-q)).
+intros.apply (le_n_O_elim n H).apply le_n.
intros.rewrite < minus_n_O.
apply le_minus_m.
intros.elim a.simplify.apply le_n.
qed.
theorem le_minus_to_plus: \forall n,m,p. (le (n-m) p) \to (le n (p+m)).
-intros 2.apply nat_elim2 (\lambda n,m.\forall p.(le (n-m) p) \to (le n (p+m))).
+intros 2.apply (nat_elim2 (\lambda n,m.\forall p.(le (n-m) p) \to (le n (p+m)))).
intros.apply le_O_n.
simplify.intros.rewrite < plus_n_O.assumption.
intros.
qed.
theorem le_plus_to_minus: \forall n,m,p. (le n (p+m)) \to (le (n-m) p).
-intros 2.apply nat_elim2 (\lambda n,m.\forall p.(le n (p+m)) \to (le (n-m) p)).
+intros 2.apply (nat_elim2 (\lambda n,m.\forall p.(le n (p+m)) \to (le (n-m) p))).
intros.simplify.apply le_O_n.
intros 2.rewrite < plus_n_O.intro.simplify.assumption.
intros.simplify.apply H.
(* the converse of le_plus_to_minus does not hold *)
theorem le_plus_to_minus_r: \forall n,m,p. (le (n+m) p) \to (le n (p-m)).
-intros 3.apply nat_elim2 (\lambda m,p.(le (n+m) p) \to (le n (p-m))).
+intros 3.apply (nat_elim2 (\lambda m,p.(le (n+m) p) \to (le n (p-m)))).
intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption.
-intro.intro.cut n=O.rewrite > Hcut.apply le_O_n.
+intro.intro.cut (n=O).rewrite > Hcut.apply le_O_n.
apply sym_eq. apply le_n_O_to_eq.
-apply trans_le ? (n+(S n1)).
+apply (trans_le ? (n+(S n1))).
rewrite < sym_plus.
apply le_plus_n.assumption.
intros.simplify.
theorem distributive_times_minus: distributive nat times minus.
simplify.
intros.
-apply (leb_elim z y).
- intro.cut x*(y-z)+x*z = (x*y-x*z)+x*z.
- apply inj_plus_l (x*z).assumption.
- apply trans_eq nat ? (x*y).
- rewrite < distr_times_plus.rewrite < plus_minus_m_m ? ? H.reflexivity.
+apply ((leb_elim z y)).
+ intro.cut (x*(y-z)+x*z = (x*y-x*z)+x*z).
+ apply (inj_plus_l (x*z)).assumption.
+ apply (trans_eq nat ? (x*y)).
+ rewrite < distr_times_plus.rewrite < (plus_minus_m_m ? ? H).reflexivity.
rewrite < plus_minus_m_m.
reflexivity.
apply le_times_r.assumption.
intro.rewrite > eq_minus_n_m_O.
- rewrite > eq_minus_n_m_O (x*y).
+ rewrite > (eq_minus_n_m_O (x*y)).
rewrite < sym_times.simplify.reflexivity.
apply le_times_r.apply lt_to_le.apply not_le_to_lt.assumption.
apply lt_to_le.apply not_le_to_lt.assumption.
theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).
intros.
-cut m+p \le n \or m+p \nleq n.
+cut (m+p \le n \or m+p \nleq n).
elim Hcut.
symmetry.apply plus_to_minus.
- rewrite > assoc_plus.rewrite > sym_plus p.rewrite < plus_minus_m_m.
+ rewrite > assoc_plus.rewrite > (sym_plus p).rewrite < plus_minus_m_m.
rewrite > sym_plus.rewrite < plus_minus_m_m.
reflexivity.
- apply trans_le ? (m+p).
+ apply (trans_le ? (m+p)).
rewrite < sym_plus.apply le_plus_n.
assumption.
apply le_plus_to_minus_r.rewrite > sym_plus.assumption.
- rewrite > eq_minus_n_m_O n (m+p).
- rewrite > eq_minus_n_m_O (n-m) p.
+ rewrite > (eq_minus_n_m_O n (m+p)).
+ rewrite > (eq_minus_n_m_O (n-m) p).
reflexivity.
apply le_plus_to_minus.apply lt_to_le. rewrite < sym_plus.
apply not_le_to_lt. assumption.
apply lt_to_le.apply not_le_to_lt.assumption.
- apply decidable_le (m+p) n.
+ apply (decidable_le (m+p) n).
qed.
theorem eq_plus_minus_minus_minus: \forall n,m,p:nat. p \le m \to m \le n \to
simplify.
intros.
rewrite > pred_Sn.
-rewrite > pred_Sn y.
+rewrite > (pred_Sn y).
apply eq_f. assumption.
qed.
(\forall n,m:nat. R n m \to R (S n) (S m)) \to \forall n,m:nat. R n m.
intros 5.elim n.
apply H.
-apply nat_case m.apply H1.
+apply (nat_case m).apply H1.
intros.apply H2. apply H3.
qed.
theorem decidable_eq_nat : \forall n,m:nat.decidable (n=m).
intros.simplify.
-apply nat_elim2 (\lambda n,m.(Or (n=m) ((n=m) \to False))).
+apply (nat_elim2 (\lambda n,m.(Or (n=m) ((n=m) \to False)))).
intro.elim n1.
left.reflexivity.
right.apply not_eq_O_S.
intro.right.intro.
-apply not_eq_O_S n1.
+apply (not_eq_O_S n1).
apply sym_eq.assumption.
intros.elim H.
left.apply eq_f. assumption.
n < smallest_factor (S n!).
intros.
apply not_le_to_lt.
-change with smallest_factor (S n!) \le n \to False.intro.
-apply not_divides_S_fact n (smallest_factor(S n!)).
+change with (smallest_factor (S n!) \le n \to False).intro.
+apply (not_divides_S_fact n (smallest_factor(S n!))).
apply lt_SO_smallest_factor.
simplify.apply le_S_S.apply le_SO_fact.
assumption.
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)!)).
+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.
-change with (S(S O)) \le S (S n1)!.
+change with ((S(S O)) \le S (S n1)!).
apply le_S.apply le_SSO_fact.
simplify.apply le_S_S.assumption.
qed.
theorem prime_nth_prime : \forall n:nat.prime (nth_prime n).
intro.
-apply nat_case n.
-change with prime (S(S O)).
-apply primeb_to_Prop (S(S O)).
+apply (nat_case n).
+change with (prime (S(S O))).
+apply (primeb_to_Prop (S(S O))).
intro.
change with
-let previous_prime \def (nth_prime m) in
+(let previous_prime \def (nth_prime m) in
let upper_bound \def S previous_prime! in
-prime (min_aux (upper_bound - (S previous_prime)) upper_bound primeb).
+prime (min_aux (upper_bound - (S previous_prime)) upper_bound primeb)).
apply primeb_true_to_prime.
apply f_min_aux_true.
-apply ex_intro nat ? (smallest_factor (S (nth_prime m)!)).
+apply (ex_intro nat ? (smallest_factor (S (nth_prime m)!))).
split.split.
-cut S (nth_prime m)!-(S (nth_prime m)! - (S (nth_prime m))) = (S (nth_prime m)).
-rewrite > Hcut.exact smallest_factor_fact (nth_prime m).
+cut (S (nth_prime m)!-(S (nth_prime m)! - (S (nth_prime m))) = (S (nth_prime m))).
+rewrite > Hcut.exact (smallest_factor_fact (nth_prime m)).
(* maybe we could factorize this proof *)
apply plus_to_minus.
apply plus_minus_m_m.
apply le_smallest_factor_n.
apply prime_to_primeb_true.
apply prime_smallest_factor_n.
-change with (S(S O)) \le S (nth_prime m)!.
+change with ((S(S O)) \le S (nth_prime m)!).
apply le_S_S.apply le_SO_fact.
qed.
(* properties of nth_prime *)
theorem increasing_nth_prime: increasing nth_prime.
-change with \forall n:nat. (nth_prime n) < (nth_prime (S n)).
+change with (\forall n:nat. (nth_prime n) < (nth_prime (S n))).
intros.
change with
-let previous_prime \def (nth_prime n) in
+(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)) upper_bound primeb.
+(S previous_prime) \le min_aux (upper_bound - (S previous_prime)) upper_bound primeb).
intros.
-cut upper_bound - (upper_bound -(S previous_prime)) = (S previous_prime).
+cut (upper_bound - (upper_bound -(S previous_prime)) = (S previous_prime)).
rewrite < Hcut in \vdash (? % ?).
apply le_min_aux.
apply plus_to_minus.
theorem lt_SO_nth_prime_n : \forall n:nat. (S O) \lt nth_prime n.
intros. elim n.simplify.apply le_n.
-apply trans_lt ? (nth_prime n1).
+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).
+intros.apply (trans_lt O (S O)).
simplify. apply le_n.apply lt_SO_nth_prime_n.
qed.
\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 upper_bound (upper_bound - (S previous_prime)) m.
-cut S (nth_prime n)!-(S (nth_prime n)! - (S (nth_prime n))) = (S (nth_prime n)).
+letin previous_prime \def (nth_prime n).
+letin upper_bound \def (S previous_prime!).
+apply (lt_min_aux_to_false primeb upper_bound (upper_bound - (S previous_prime)) m).
+cut (S (nth_prime n)!-(S (nth_prime n)! - (S (nth_prime n))) = (S (nth_prime n))).
rewrite > Hcut.assumption.
apply plus_to_minus.
apply plus_minus_m_m.
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).
+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.
+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 (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.simplify in H.elim H.assumption.
| (S a) \Rightarrow pair nat nat O n] )
with
[ (pair q r) \Rightarrow n = m \sup q * r ].
-apply nat_case (n \mod m).
+apply (nat_case (n \mod m)).
simplify.apply plus_n_O.
intros.
simplify.apply plus_n_O.
| (S a) \Rightarrow pair nat nat O n1] )
with
[ (pair q r) \Rightarrow n1 = m \sup q * r].
-apply nat_case1 (n1 \mod m).intro.
+apply (nat_case1 (n1 \mod m)).intro.
change with
match (
match (p_ord_aux n (n1 / m) m) with
with
[ (pair q r) \Rightarrow n1 = m \sup q * r].
generalize in match (H (n1 / m) m).
-elim p_ord_aux n (n1 / m) m.
+elim (p_ord_aux n (n1 / m) m).
simplify.
rewrite > assoc_times.
-rewrite < H3.rewrite > plus_n_O (m*(n1 / m)).
+rewrite < H3.rewrite > (plus_n_O (m*(n1 / m))).
rewrite < H2.
rewrite > sym_times.
rewrite < div_mod.reflexivity.
elim i.
simplify.
rewrite < plus_n_O.
-apply nat_case p.
+apply (nat_case p).
change with
- match n \mod m with
+ (match n \mod m with
[ O \Rightarrow pair nat nat O n
| (S a) \Rightarrow pair nat nat O n]
- = pair nat nat O n.
+ = pair nat nat O n).
elim (n \mod m).simplify.reflexivity.simplify.reflexivity.
intro.
change with
- match n \mod m with
+ (match n \mod m with
[ O \Rightarrow
match (p_ord_aux m1 (n / m) m) with
[ (pair q r) \Rightarrow pair nat nat (S q) r]
| (S a) \Rightarrow pair nat nat O n]
- = pair nat nat O n.
-cut O < n \mod m \lor O = n \mod m.
-elim Hcut.apply lt_O_n_elim (n \mod m) H3.
+ = pair nat nat O n).
+cut (O < n \mod m \lor O = n \mod m).
+elim Hcut.apply (lt_O_n_elim (n \mod m) H3).
intros. simplify.reflexivity.
apply False_ind.
apply H1.apply sym_eq.assumption.
apply le_to_or_lt_eq.apply le_O_n.
generalize in match H3.
-apply nat_case p.intro.apply False_ind.apply not_le_Sn_O n1 H4.
+apply (nat_case p).intro.apply False_ind.apply (not_le_Sn_O n1 H4).
intros.
change with
- match ((m \sup (S n1) *n) \mod m) with
+ (match ((m \sup (S n1) *n) \mod m) with
[ O \Rightarrow
match (p_ord_aux m1 ((m \sup (S n1) *n) / m) m) with
[ (pair q r) \Rightarrow pair nat nat (S q) r]
| (S a) \Rightarrow pair nat nat O (m \sup (S n1) *n)]
- = pair nat nat (S n1) n.
-cut ((m \sup (S n1)*n) \mod m) = O.
+ = pair nat nat (S n1) n).
+cut (((m \sup (S n1)*n) \mod m) = O).
rewrite > Hcut.
change with
-match (p_ord_aux m1 ((m \sup (S n1)*n) / m) m) with
+(match (p_ord_aux m1 ((m \sup (S n1)*n) / m) m) with
[ (pair q r) \Rightarrow pair nat nat (S q) r]
- = pair nat nat (S n1) n.
-cut (m \sup (S n1) *n) / m = m \sup n1 *n.
+ = pair nat nat (S n1) n).
+cut ((m \sup (S n1) *n) / m = m \sup n1 *n).
rewrite > Hcut1.
-rewrite > H2 m1. simplify.reflexivity.
+rewrite > (H2 m1). simplify.reflexivity.
apply le_S_S_to_le.assumption.
(* div_exp *)
-change with (m* m \sup n1 *n) / m = m \sup n1 * n.
+change with ((m* m \sup n1 *n) / m = m \sup n1 * n).
rewrite > assoc_times.
-apply lt_O_n_elim m H.
+apply (lt_O_n_elim m H).
intro.apply div_times.
(* mod_exp = O *)
apply divides_to_mod_O.
assumption.
simplify.rewrite > assoc_times.
-apply witness ? ? (m \sup n1 *n).reflexivity.
+apply (witness ? ? (m \sup n1 *n)).reflexivity.
qed.
theorem p_ord_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to
match p_ord_aux p n m with
[ (pair q r) \Rightarrow r \mod m \neq O].
-intro.elim p.absurd O < n.assumption.
+intro.elim p.absurd (O < n).assumption.
apply le_to_not_lt.assumption.
change with
match
| (S a) \Rightarrow pair nat nat O n1])
with
[ (pair q r) \Rightarrow r \mod m \neq O].
-apply nat_case1 (n1 \mod m).intro.
+apply (nat_case1 (n1 \mod m)).intro.
generalize in match (H (n1 / m) m).
elim (p_ord_aux n (n1 / m) m).
apply H5.assumption.
apply eq_mod_O_to_lt_O_div.
-apply trans_lt ? (S O).simplify.apply le_n.
+apply (trans_lt ? (S O)).simplify.apply le_n.
assumption.assumption.assumption.
apply le_S_S_to_le.
-apply trans_le ? n1.change with n1 / m < n1.
+apply (trans_le ? n1).change with (n1 / m < n1).
apply lt_div_n_m_n.assumption.assumption.assumption.
intros.
-change with n1 \mod m \neq O.
+change with (n1 \mod m \neq O).
rewrite > H4.
(* Andrea: META NOT FOUND !!!
rewrite > sym_eq. *)
simplify.intro.
-apply not_eq_O_S m1.
+apply (not_eq_O_S m1).
rewrite > H5.reflexivity.
qed.
qed.
theorem le_S_S_to_le : \forall n,m:nat. S n \leq S m \to n \leq m.
-intros.change with pred (S n) \leq pred (S m).
-elim H.apply le_n.apply trans_le ? (pred n1).assumption.
+intros.change with (pred (S n) \leq pred (S m)).
+elim H.apply le_n.apply (trans_le ? (pred n1)).assumption.
apply le_pred_n.
qed.
(* not le *)
theorem not_le_Sn_O: \forall n:nat. S n \nleq O.
-intros.simplify.intros.apply leS_to_not_zero ? ? H.
+intros.simplify.intros.apply (leS_to_not_zero ? ? H).
qed.
theorem not_le_Sn_n: \forall n:nat. S n \nleq n.
-intros.elim n.apply not_le_Sn_O.simplify.intros.cut S n1 \leq n1.
+intros.elim n.apply not_le_Sn_O.simplify.intros.cut (S n1 \leq n1).
apply H.assumption.
apply le_S_S_to_le.assumption.
qed.
(* not eq *)
theorem lt_to_not_eq : \forall n,m:nat. n<m \to n \neq m.
-simplify.intros.cut (le (S n) m) \to False.
+simplify.intros.cut ((le (S n) m) \to False).
apply Hcut.assumption.rewrite < H1.
apply not_le_Sn_n.
qed.
theorem not_le_to_lt: \forall n,m:nat. n \nleq m \to m<n.
intros 2.
-apply nat_elim2 (\lambda n,m.n \nleq m \to m<n).
-intros.apply absurd (O \leq n1).apply le_O_n.assumption.
+apply (nat_elim2 (\lambda n,m.n \nleq m \to m<n)).
+intros.apply (absurd (O \leq n1)).apply le_O_n.assumption.
simplify.intros.apply le_S_S.apply le_O_n.
simplify.intros.apply le_S_S.apply H.intros.apply H1.apply le_S_S.
assumption.
theorem lt_to_not_le: \forall n,m:nat. n<m \to m \nleq n.
simplify.intros 3.elim H.
-apply not_le_Sn_n n H1.
+apply (not_le_Sn_n n H1).
apply H2.apply lt_to_le. apply H3.
qed.
theorem le_to_not_lt: \forall n,m:nat. le n m \to Not (lt m n).
intros.
-change with Not (le (S m) n).
+change with (Not (le (S m) n)).
apply lt_to_not_le.simplify.
apply le_S_S.assumption.
qed.
qed.
theorem ltn_to_ltO: \forall n,m:nat. lt n m \to lt O m.
-intros.apply le_to_lt_to_lt O n.
+intros.apply (le_to_lt_to_lt O n).
apply le_O_n.assumption.
qed.
theorem lt_O_n_elim: \forall n:nat. lt O n \to
\forall P:nat\to Prop. (\forall m:nat.P (S m)) \to P n.
-intro.elim n.apply False_ind.exact not_le_Sn_O O H.
+intro.elim n.apply False_ind.exact (not_le_Sn_O O H).
apply H2.
qed.
(* other abstract properties *)
theorem antisymmetric_le : antisymmetric nat le.
simplify.intros 2.
-apply nat_elim2 (\lambda n,m.(n \leq m \to m \leq n \to n=m)).
+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 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.
theorem decidable_le: \forall n,m:nat. decidable (n \leq m).
intros.
-apply nat_elim2 (\lambda n,m.decidable (n \leq m)).
+apply (nat_elim2 (\lambda n,m.decidable (n \leq m))).
intros.simplify.left.apply le_O_n.
-intros.simplify.right.exact not_le_Sn_O n1.
+intros.simplify.right.exact (not_le_Sn_O n1).
intros 2.simplify.intro.elim H.
left.apply le_S_S.assumption.
right.intro.apply H1.apply le_S_S_to_le.assumption.
qed.
theorem decidable_lt: \forall n,m:nat. decidable (n < m).
-intros.exact decidable_le (S n) m.
+intros.exact (decidable_le (S n) m).
qed.
(* well founded induction principles *)
theorem nat_elim1 : \forall n:nat.\forall P:nat \to Prop.
(\forall m.(\forall p. (p \lt m) \to P p) \to P m) \to P n.
-intros.cut \forall q:nat. q \le n \to P q.
-apply Hcut n.apply le_n.
-elim n.apply le_n_O_elim q H1.
+intros.cut (\forall q:nat. q \le n \to P q).
+apply (Hcut n).apply le_n.
+elim n.apply (le_n_O_elim q H1).
apply H.
-intros.apply False_ind.apply not_le_Sn_O p H2.
+intros.apply False_ind.apply (not_le_Sn_O p H2).
apply H.intros.apply H1.
-cut p < S n1.
+cut (p < S n1).
apply lt_S_to_le.assumption.
-apply lt_to_le_to_lt p q (S n1) H3 H2.
+apply (lt_to_le_to_lt p q (S n1) H3 H2).
qed.
(* some properties of functions *)
theorem increasing_to_monotonic: \forall f:nat \to nat.
increasing f \to monotonic nat lt f.
simplify.intros.elim H1.apply H.
-apply trans_le ? (f n1).
-assumption.apply trans_le ? (S (f n1)).
+apply (trans_le ? (f n1)).
+assumption.apply (trans_le ? (S (f n1))).
apply le_n_Sn.
apply H.
qed.
\to \forall n:nat. n \le (f n).
intros.elim n.
apply le_O_n.
-apply trans_le ? (S (f n1)).
+apply (trans_le ? (S (f n1))).
apply le_S_S.apply H1.
simplify 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.
+apply (ex_intro ? ? O).apply le_O_n.
elim H1.
-apply ex_intro ? ? (S a).
-apply trans_le ? (S (f a)).
+apply (ex_intro ? ? (S a)).
+apply (trans_le ? (S (f a))).
apply le_S_S.assumption.
simplify in H.
apply H.
\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.
+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)).
+cut ((S n1) < (f (S a)) \lor (S n1) = (f (S a))).
elim Hcut.
-apply ex_intro ? ? a.
+apply (ex_intro ? ? a).
split.apply le_S. assumption.assumption.
-apply ex_intro ? ? (S a).
+apply (ex_intro ? ? (S a)).
split.rewrite < H7.apply le_n.
rewrite > H7.
apply H.
unfold permut.intros.
elim H.
split.intros.
-cut f i < S m \lor f i = S m.
+cut (f i < S m \lor f i = S m).
elim Hcut.
apply le_S_S_to_le.assumption.
apply False_ind.
-apply not_le_Sn_n m.
-cut (S m) = i.
+apply (not_le_Sn_n m).
+cut ((S m) = i).
rewrite > Hcut1.assumption.
apply H3.apply le_n.apply le_S.assumption.
rewrite > H5.assumption.
apply le_to_or_lt_eq.apply H2.apply le_S.assumption.
-apply injn_Sn_n f m H3.
+apply (injn_Sn_n f m H3).
qed.
(* transpositions *)
lemma transpose_i_j_i: \forall i,j:nat. transpose i j i = j.
intros.unfold transpose.
-rewrite > eqb_n_n i.simplify. reflexivity.
+rewrite > (eqb_n_n i).simplify. reflexivity.
qed.
lemma transpose_i_j_j: \forall i,j:nat. transpose i j j = i.
intros.unfold transpose.
-apply eqb_elim j i.simplify.intro.assumption.
-rewrite > eqb_n_n j.simplify.
+apply (eqb_elim j i).simplify.intro.assumption.
+rewrite > (eqb_n_n j).simplify.
intros. reflexivity.
qed.
theorem transpose_i_i: \forall i,n:nat. (transpose i i n) = n.
intros.unfold transpose.
-apply eqb_elim n i.
+apply (eqb_elim n i).
intro.simplify.apply sym_eq. assumption.
intro.simplify.reflexivity.
qed.
theorem transpose_i_j_j_i: \forall i,j,n:nat.
transpose i j n = transpose j i n.
intros.unfold transpose.
-apply eqb_elim n i.
-apply eqb_elim n j.
+apply (eqb_elim n i).
+apply (eqb_elim n j).
intros. simplify.rewrite < H. rewrite < H1.
reflexivity.
intros.simplify.reflexivity.
-apply eqb_elim n j.
+apply (eqb_elim n j).
intros.simplify.reflexivity.
intros.simplify.reflexivity.
qed.
theorem transpose_transpose: \forall i,j,n:nat.
(transpose i j (transpose i j n)) = n.
intros.unfold transpose. unfold transpose.
-apply eqb_elim n i.simplify.
+apply (eqb_elim n i).simplify.
intro.
-apply eqb_elim j i.
+apply (eqb_elim j i).
simplify.intros.rewrite > H. rewrite > H1.reflexivity.
-rewrite > eqb_n_n j.simplify.intros.
+rewrite > (eqb_n_n j).simplify.intros.
apply sym_eq.
assumption.
-apply eqb_elim n j.simplify.
-rewrite > eqb_n_n i.intros.simplify.
+apply (eqb_elim n j).simplify.
+rewrite > (eqb_n_n i).intros.simplify.
apply sym_eq. assumption.
simplify.intros.
-rewrite > not_eq_to_eqb_false n i H1.
-rewrite > not_eq_to_eqb_false n j H.
+rewrite > (not_eq_to_eqb_false n i H1).
+rewrite > (not_eq_to_eqb_false n j H).
simplify.reflexivity.
qed.
injective nat nat (transpose i j).
unfold injective.
intros.
-rewrite < transpose_transpose i j x.
-rewrite < transpose_transpose i j y.
+rewrite < (transpose_transpose i j x).
+rewrite < (transpose_transpose i j y).
apply eq_f.assumption.
qed.
unfold permut.intros.
split.unfold transpose.
intros.
-elim eqb i1 i.simplify.assumption.
-elim eqb i1 j.simplify.assumption.
+elim (eqb i1 i).simplify.assumption.
+elim (eqb i1 j).simplify.assumption.
simplify.assumption.
-apply injective_to_injn (transpose i j) n.
+apply (injective_to_injn (transpose i j) n).
apply injective_transpose.
qed.
theorem permut_transpose_l:
\forall f:nat \to nat. \forall m,i,j:nat.
i \le m \to j \le m \to permut f m \to permut (\lambda n.transpose i j (f n)) m.
-intros.apply permut_fg (transpose i j) f m ? ?.
+intros.apply (permut_fg (transpose i j) f m ? ?).
apply permut_transpose.assumption.assumption.
assumption.
qed.
theorem permut_transpose_r:
\forall f:nat \to nat. \forall m,i,j:nat.
i \le m \to j \le m \to permut f m \to permut (\lambda n.f (transpose i j n)) m.
-intros.apply permut_fg f (transpose i j) m ? ?.
+intros.apply (permut_fg f (transpose i j) m ? ?).
assumption.apply permut_transpose.assumption.assumption.
qed.
transpose i j n = transpose i k (transpose k j (transpose i k n)).
(* uffa: triplo unfold? *)
intros.unfold transpose.unfold transpose.unfold transpose.
-apply eqb_elim n i.intro.
-simplify.rewrite > eqb_n_n k.
-simplify.rewrite > not_eq_to_eqb_false j i H.
-rewrite > not_eq_to_eqb_false j k H2.
+apply (eqb_elim n i).intro.
+simplify.rewrite > (eqb_n_n k).
+simplify.rewrite > (not_eq_to_eqb_false j i H).
+rewrite > (not_eq_to_eqb_false j k H2).
reflexivity.
-intro.apply eqb_elim n j.
+intro.apply (eqb_elim n j).
intro.
-cut \lnot n = k.
-cut \lnot n = i.
-rewrite > not_eq_to_eqb_false n k Hcut.
+cut (\lnot n = k).
+cut (\lnot n = i).
+rewrite > (not_eq_to_eqb_false n k Hcut).
simplify.
-rewrite > not_eq_to_eqb_false n k Hcut.
-rewrite > eq_to_eqb_true n j H4.
+rewrite > (not_eq_to_eqb_false n k Hcut).
+rewrite > (eq_to_eqb_true n j H4).
simplify.
-rewrite > not_eq_to_eqb_false k i.
-rewrite > eqb_n_n k.
+rewrite > (not_eq_to_eqb_false k i).
+rewrite > (eqb_n_n k).
simplify.reflexivity.
simplify.intro.apply H1.apply sym_eq.assumption.
assumption.
-simplify.intro.apply H2.apply trans_eq ? ? n.
+simplify.intro.apply H2.apply (trans_eq ? ? n).
apply sym_eq.assumption.assumption.
-intro.apply eqb_elim n k.intro.
+intro.apply (eqb_elim n k).intro.
simplify.
-rewrite > not_eq_to_eqb_false i k H1.
-rewrite > not_eq_to_eqb_false i j.
+rewrite > (not_eq_to_eqb_false i k H1).
+rewrite > (not_eq_to_eqb_false i j).
simplify.
-rewrite > eqb_n_n i.
+rewrite > (eqb_n_n i).
simplify.assumption.
simplify.intro.apply H.apply sym_eq.assumption.
intro.simplify.
-rewrite > not_eq_to_eqb_false n k H5.
-rewrite > not_eq_to_eqb_false n j H4.
+rewrite > (not_eq_to_eqb_false n k H5).
+rewrite > (not_eq_to_eqb_false n j H4).
simplify.
-rewrite > not_eq_to_eqb_false n i H3.
-rewrite > not_eq_to_eqb_false n k H5.
+rewrite > (not_eq_to_eqb_false n i H3).
+rewrite > (not_eq_to_eqb_false n k H5).
simplify.reflexivity.
qed.
unfold permut.intros.
elim H.
split.intros.simplify.
-apply eqb_elim (f i) (f (S m)).simplify.
+apply (eqb_elim (f i) (f (S m))).
intro.apply False_ind.
-cut i = (S m).
-apply not_le_Sn_n m.
+cut (i = (S m)).
+apply (not_le_Sn_n m).
rewrite < Hcut.assumption.
apply H2.apply le_S.assumption.apply le_n.assumption.
intro.simplify.
-apply eqb_elim (f i) (S m).simplify.
+apply (eqb_elim (f i) (S m)).
intro.
-cut f (S m) \lt (S m) \lor f (S m) = (S m).
+cut (f (S m) \lt (S m) \lor f (S m) = (S m)).
elim Hcut.apply le_S_S_to_le.assumption.
apply False_ind.apply H4.rewrite > H6.assumption.
apply le_to_or_lt_eq.apply H1.apply le_n.
intro.simplify.
-cut f i \lt (S m) \lor f i = (S m).
+cut (f i \lt (S m) \lor f i = (S m)).
elim Hcut.apply le_S_S_to_le.assumption.
apply False_ind.apply H5.assumption.
apply le_to_or_lt_eq.apply H1.apply le_S.assumption.
unfold injn.intros.
apply H2.apply le_S.assumption.apply le_S.assumption.
-apply inj_transpose (f (S m)) (S m).
+apply (inj_transpose (f (S m)) (S m)).
apply H5.
qed.
(\forall i:nat. i \le n \to (f i) = (g i)) \to
bijn f n \to bijn g n.
intros 4.unfold bijn.
-intros.elim H1 m.
-apply ex_intro ? ? a.
-rewrite < H a.assumption.
+intros.elim (H1 m).
+apply (ex_intro ? ? a).
+rewrite < (H a).assumption.
elim H3.assumption.assumption.
qed.
theorem bijn_Sn_n: \forall f:nat \to nat. \forall n:nat.
bijn f (S n) \to f (S n) = (S n) \to bijn f n.
-unfold bijn.intros.elim H m.
+unfold bijn.intros.elim (H m).
elim H3.
-apply ex_intro ? ? a.split.
-cut a < S n \lor a = S n.
+apply (ex_intro ? ? a).split.
+cut (a < S n \lor a = S n).
elim Hcut.apply le_S_S_to_le.assumption.
apply False_ind.
-apply not_le_Sn_n n.
+apply (not_le_Sn_n n).
rewrite < H1.rewrite < H6.rewrite > H5.assumption.
apply le_to_or_lt_eq.assumption.assumption.
apply le_S.assumption.
theorem bijn_n_Sn: \forall f:nat \to nat. \forall n:nat.
bijn f n \to f (S n) = (S n) \to bijn f (S n).
unfold bijn.intros.
-cut m < S n \lor m = S n.
+cut (m < S n \lor m = S n).
elim Hcut.
-elim H m.
+elim (H m).
elim H4.
-apply ex_intro ? ? a.split.
+apply (ex_intro ? ? a).split.
apply le_S.assumption.assumption.
apply le_S_S_to_le.assumption.
-apply ex_intro ? ? (S n).
+apply (ex_intro ? ? (S n)).
split.apply le_n.
rewrite > H3.assumption.
apply le_to_or_lt_eq.assumption.
bijn f n \to bijn g n \to bijn (\lambda p.f(g p)) n.
unfold bijn.
intros.simplify.
-elim H m.elim H3.
-elim H1 a.elim H6.
-apply ex_intro ? ? a1.
+elim (H m).elim H3.
+elim (H1 a).elim H6.
+apply (ex_intro ? ? a1).
split.assumption.
rewrite > H8.assumption.
assumption.assumption.
theorem bijn_transpose : \forall n,i,j. i \le n \to j \le n \to
bijn (transpose i j) n.
intros.simplify.intros.
-cut m = i \lor \lnot m = i.
+cut (m = i \lor \lnot m = i).
elim Hcut.
-apply ex_intro ? ? j.
+apply (ex_intro ? ? j).
split.assumption.
-apply eqb_elim j i.
+apply (eqb_elim j i).
intro.simplify.rewrite > H3.rewrite > H4.reflexivity.
-rewrite > eqb_n_n j.simplify.
+rewrite > (eqb_n_n j).simplify.
intros. apply sym_eq.assumption.
-cut m = j \lor \lnot m = j.
+cut (m = j \lor \lnot m = j).
elim Hcut1.
-apply ex_intro ? ? i.
+apply (ex_intro ? ? i).
split.assumption.
-rewrite > eqb_n_n i.simplify.
+rewrite > (eqb_n_n i).simplify.
apply sym_eq. assumption.
-apply ex_intro ? ? m.
+apply (ex_intro ? ? m).
split.assumption.
-rewrite > not_eq_to_eqb_false m i.
-rewrite > not_eq_to_eqb_false m j.
+rewrite > (not_eq_to_eqb_false m i).
+rewrite > (not_eq_to_eqb_false m j).
simplify. reflexivity.
assumption.
assumption.
-apply decidable_eq_nat m j.
-apply decidable_eq_nat m i.
+apply (decidable_eq_nat m j).
+apply (decidable_eq_nat m i).
qed.
theorem bijn_transpose_r: \forall f:nat\to nat.\forall n,i,j. i \le n \to j \le n \to
bijn f n \to bijn (\lambda p.f (transpose i j p)) n.
intros.
-apply bijn_fg f ?.assumption.
-apply bijn_transpose n i j.assumption.assumption.
+apply (bijn_fg f ?).assumption.
+apply (bijn_transpose n i j).assumption.assumption.
qed.
theorem bijn_transpose_l: \forall f:nat\to nat.\forall n,i,j. i \le n \to j \le n \to
bijn f n \to bijn (\lambda p.transpose i j (f p)) n.
intros.
-apply bijn_fg ? f.
-apply bijn_transpose n i j.assumption.assumption.
+apply (bijn_fg ? f).
+apply (bijn_transpose n i j).assumption.assumption.
assumption.
qed.
-
theorem permut_to_bijn: \forall n:nat.\forall f:nat\to nat.
permut f n \to bijn f n.
intro.
elim n.simplify.intros.
-apply ex_intro ? ? m.
+apply (ex_intro ? ? m).
split.assumption.
-apply le_n_O_elim m ? (\lambda p. f p = p).
+apply (le_n_O_elim m ? (\lambda p. f p = p)).
assumption.unfold permut in H.
elim H.apply sym_eq. apply le_n_O_to_eq.apply H2.apply le_n.
-apply eq_to_bijn (\lambda p.
-(transpose (f (S n1)) (S n1)) (transpose (f (S n1)) (S n1) (f p))) f.
+apply (eq_to_bijn (\lambda p.
+(transpose (f (S n1)) (S n1)) (transpose (f (S n1)) (S n1) (f p))) f).
intros.apply transpose_transpose.
-apply bijn_fg (transpose (f (S n1)) (S n1)).
+apply (bijn_fg (transpose (f (S n1)) (S n1))).
apply bijn_transpose.
unfold permut in H1.
elim H1.apply H2.apply le_n.apply le_n.
apply H.
apply permut_S_to_permut_transpose.
assumption.simplify.
-rewrite > eqb_n_n (f (S n1)).simplify.reflexivity.
+rewrite > (eqb_n_n (f (S n1))).simplify.reflexivity.
qed.
let rec invert_permut n f m \def
m \le n \to injn f n\to invert_permut n f (f m) = m.
intros 4.
elim H.
-apply nat_case1 m.
+apply (nat_case1 m).
intro.simplify.
-rewrite > eqb_n_n (f O).simplify.reflexivity.
+rewrite > (eqb_n_n (f O)).simplify.reflexivity.
intros.simplify.
-rewrite > eqb_n_n (f (S m1)).simplify.reflexivity.
+rewrite > (eqb_n_n (f (S m1))).simplify.reflexivity.
simplify.
-rewrite > not_eq_to_eqb_false (f m) (f (S n1)).
+rewrite > (not_eq_to_eqb_false (f m) (f (S n1))).
simplify.apply H2.
apply injn_Sn_n. assumption.
-simplify.intro.absurd m = S n1.
+simplify.intro.absurd (m = S n1).
apply H3.apply le_S.assumption.apply le_n.assumption.
simplify.intro.
-apply not_le_Sn_n n1.rewrite < H5.assumption.
+apply (not_le_Sn_n n1).rewrite < H5.assumption.
qed.
theorem injective_invert_permut: \forall f:nat \to nat. \forall n:nat.
permut f n \to injn (invert_permut n f) n.
intros.
unfold injn.intros.
-cut bijn f n.
+cut (bijn f n).
unfold bijn in Hcut.
-generalize in match Hcut i H1.intro.
-generalize in match Hcut j H2.intro.
+generalize in match (Hcut i H1).intro.
+generalize in match (Hcut j H2).intro.
elim H4.elim H6.
elim H5.elim H9.
rewrite < H8.
rewrite < H11.
apply eq_f.
-rewrite < invert_permut_f f n a.
-rewrite < invert_permut_f f n a1.
+rewrite < (invert_permut_f f n a).
+rewrite < (invert_permut_f f n a1).
rewrite > H8.
rewrite > H11.
assumption.assumption.
permut f n \to permut (invert_permut n f) n.
intros.unfold permut.split.
intros.simplify.elim n.
-simplify.elim eqb i (f O).simplify.apply le_n.simplify.apply le_n.
-simplify.elim eqb i (f (S n1)).simplify.apply le_n.
+simplify.elim (eqb i (f O)).simplify.apply le_n.simplify.apply le_n.
+simplify.elim (eqb i (f (S n1))).simplify.apply le_n.
simplify.apply le_S. assumption.
apply injective_invert_permut.assumption.
qed.
theorem f_invert_permut: \forall f:nat \to nat. \forall n,m:nat.
m \le n \to permut f n\to f (invert_permut n f m) = m.
intros.
-apply injective_invert_permut f n H1.
+apply (injective_invert_permut f n H1).
unfold permut in H1.elim H1.
apply H2.
-cut permut (invert_permut n f) n.unfold permut in Hcut.
+cut (permut (invert_permut n f) n).unfold permut in Hcut.
elim Hcut.apply H4.assumption.
apply permut_invert_permut.assumption.assumption.
(* uffa: lo ha espanso troppo *)
-change with invert_permut n f (f (invert_permut n f m)) = invert_permut n f m.
+change with (invert_permut n f (f (invert_permut n f m)) = invert_permut n f m).
apply invert_permut_f.
-cut permut (invert_permut n f) n.unfold permut in Hcut.
+cut (permut (invert_permut n f) n).unfold permut in Hcut.
elim Hcut.apply H2.assumption.
apply permut_invert_permut.assumption.
unfold permut in H1.elim H1.assumption.
theorem permut_n_to_eq_n: \forall h:nat \to nat.\forall n:nat.
permut h n \to (\forall m:nat. m < n \to h m = m) \to h n = n.
intros.unfold permut in H.elim H.
-cut invert_permut n h n < n \lor invert_permut n h n = n.
+cut (invert_permut n h n < n \lor invert_permut n h n = n).
elim Hcut.
-rewrite < f_invert_permut h n n in \vdash (? ? ? %).
+rewrite < (f_invert_permut h n n) in \vdash (? ? ? %).
apply eq_f.
-rewrite < f_invert_permut h n n in \vdash (? ? % ?).
+rewrite < (f_invert_permut h n n) in \vdash (? ? % ?).
apply H1.assumption.apply le_n.assumption.apply le_n.assumption.
rewrite < H4 in \vdash (? ? % ?).
-apply f_invert_permut h.apply le_n.assumption.
+apply (f_invert_permut h).apply le_n.assumption.
apply le_to_or_lt_eq.
-cut permut (invert_permut n h) n.
+cut (permut (invert_permut n h) n).
unfold permut in Hcut.elim Hcut.
apply H4.apply le_n.
apply permut_invert_permut.assumption.
k \le n \to permut h n \to (\forall m:nat. m < k \to h m = m) \to
\forall j. k \le j \to j \le n \to k \le h j.
intros.unfold permut in H1.elim H1.
-cut h j < k \lor \not(h j < k).
-elim Hcut.absurd k \le j.assumption.
+cut (h j < k \lor \not(h j < k)).
+elim Hcut.absurd (k \le j).assumption.
apply lt_to_not_le.
-cut h j = j.rewrite < Hcut1.assumption.
+cut (h j = j).rewrite < Hcut1.assumption.
apply H6.apply H5.assumption.assumption.
apply H2.assumption.
apply not_lt_to_le.assumption.
-apply decidable_lt (h j) k.
+apply (decidable_lt (h j) k).
qed.
(* applications *)
intros.elim n.
simplify.reflexivity.
change with
-((S n1)+(S O))*(map_iter_i n1 (\lambda m.m) times (S O)) = (S(S n1))*(S n1)!.
+(((S n1)+(S O))*(map_iter_i n1 (\lambda m.m) times (S O)) = (S(S n1))*(S n1)!).
rewrite < plus_n_Sm.rewrite < plus_n_O.
apply eq_f.assumption.
qed.
theorem eq_map_iter_i_transpose_l : \forall f:nat\to nat \to nat.associative nat f \to
symmetric2 nat nat f \to \forall g:nat \to nat. \forall n,k:nat.
map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose (k+n) (S k+n) m)) f n.
-intros.apply nat_case1 k.
+intros.apply (nat_case1 k).
intros.simplify.
change with
-f (g (S n)) (g n) =
-f (g (transpose n (S n) (S n))) (g (transpose n (S n) n)).
+(f (g (S n)) (g n) =
+f (g (transpose n (S n) (S n))) (g (transpose n (S n) n))).
rewrite > transpose_i_j_i.
rewrite > transpose_i_j_j.
apply H1.
intros.
change with
-f (g (S (S (m+n)))) (f (g (S (m+n))) (map_iter_i m g f n)) =
+(f (g (S (S (m+n)))) (f (g (S (m+n))) (map_iter_i m g f n)) =
f (g (transpose (S m + n) (S (S m) + n) (S (S m)+n)))
(f (g (transpose (S m + n) (S (S m) + n) (S m+n)))
-(map_iter_i m (\lambda m1. g (transpose (S m+n) (S (S m)+n) m1)) f n)).
+(map_iter_i m (\lambda m1. g (transpose (S m+n) (S (S m)+n) m1)) f n))).
rewrite > transpose_i_j_i.
rewrite > transpose_i_j_j.
rewrite < H.
rewrite < H.
-rewrite < H1 (g (S m + n)).
+rewrite < (H1 (g (S m + n))).
apply eq_f.
apply eq_map_iter_i.
intros.unfold transpose.
-rewrite > not_eq_to_eqb_false m1 (S m+n).
-rewrite > not_eq_to_eqb_false m1 (S (S m)+n).
+rewrite > (not_eq_to_eqb_false m1 (S m+n)).
+rewrite > (not_eq_to_eqb_false m1 (S (S m)+n)).
simplify.
reflexivity.
-apply lt_to_not_eq m1 (S (S m)+n).
+apply (lt_to_not_eq m1 (S (S m)+n)).
simplify.apply le_S_S.apply le_S.assumption.
-apply lt_to_not_eq m1 (S m+n).
+apply (lt_to_not_eq m1 (S m+n)).
simplify.apply le_S_S.assumption.
qed.
theorem eq_map_iter_i_transpose_i_Si : \forall f:nat\to nat \to nat.associative nat f \to
symmetric2 nat nat f \to \forall g:nat \to nat. \forall n,k,i:nat. n \le i \to i \le k+n \to
map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i (S i) m)) f n.
-intros 6.elim k.cut i=n.
+intros 6.elim k.cut (i=n).
rewrite > Hcut.
-apply eq_map_iter_i_transpose_l f H H1 g n O.
+apply (eq_map_iter_i_transpose_l f H H1 g n O).
apply antisymmetric_le.assumption.assumption.
-cut i < S n1 + n \lor i = S n1 + n.
+cut (i < S n1 + n \lor i = S n1 + n).
elim Hcut.
change with
-f (g (S (S n1)+n)) (map_iter_i (S n1) g f n) =
-f (g (transpose i (S i) (S (S n1)+n))) (map_iter_i (S n1) (\lambda m. g (transpose i (S i) m)) f n).
+(f (g (S (S n1)+n)) (map_iter_i (S n1) g f n) =
+f (g (transpose i (S i) (S (S n1)+n))) (map_iter_i (S n1) (\lambda m. g (transpose i (S i) m)) f n)).
apply eq_f2.unfold transpose.
-rewrite > not_eq_to_eqb_false (S (S n1)+n) i.
-rewrite > not_eq_to_eqb_false (S (S n1)+n) (S i).
+rewrite > (not_eq_to_eqb_false (S (S n1)+n) i).
+rewrite > (not_eq_to_eqb_false (S (S n1)+n) (S i)).
simplify.reflexivity.
simplify.intro.
-apply lt_to_not_eq i (S n1+n).assumption.
+apply (lt_to_not_eq i (S n1+n)).assumption.
apply inj_S.apply sym_eq. assumption.
simplify.intro.
-apply lt_to_not_eq i (S (S n1+n)).simplify.
+apply (lt_to_not_eq i (S (S n1+n))).simplify.
apply le_S_S.assumption.
apply sym_eq. assumption.
apply H2.assumption.apply le_S_S_to_le.
assumption.
rewrite > H5.
-apply eq_map_iter_i_transpose_l f H H1 g n (S n1).
+apply (eq_map_iter_i_transpose_l f H H1 g n (S n1)).
apply le_to_or_lt_eq.assumption.
qed.
\forall g:nat \to nat. \forall i:nat. n \le i \to S (o + i) \le S k+n \to
map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i (S(o + i)) m)) f n.
intros 6.
-apply nat_elim1 o.
+apply (nat_elim1 o).
intro.
-apply nat_case m ?.
+apply (nat_case m ?).
intros.
-apply eq_map_iter_i_transpose_i_Si ? H H1.
+apply (eq_map_iter_i_transpose_i_Si ? H H1).
exact H3.apply le_S_S_to_le.assumption.
intros.
-apply trans_eq ? ? (map_iter_i (S k) (\lambda m. g (transpose i (S(m1 + i)) m)) f n).
+apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g (transpose i (S(m1 + i)) m)) f n)).
apply H2.
simplify. apply le_n.assumption.
-apply trans_le ? (S(S (m1+i))).
+apply (trans_le ? (S(S (m1+i)))).
apply le_S.apply le_n.assumption.
-apply trans_eq ? ? (map_iter_i (S k) (\lambda m. g
-(transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) m))) f n).
-apply H2 O ? ? (S(m1+i)).
+apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g
+(transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) m))) f n)).
+apply (H2 O ? ? (S(m1+i))).
simplify.apply le_S_S.apply le_O_n.
-apply trans_le ? i.assumption.
-change with i \le (S m1)+i.apply le_plus_n.
+apply (trans_le ? i).assumption.
+change with (i \le (S m1)+i).apply le_plus_n.
exact H4.
-apply trans_eq ? ? (map_iter_i (S k) (\lambda m. g
+apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g
(transpose i (S(m1 + i))
(transpose (S(m1 + i)) (S(S(m1 + i)))
-(transpose i (S(m1 + i)) m)))) f n).
-apply H2 m1.
+(transpose i (S(m1 + i)) m)))) f n)).
+apply (H2 m1).
simplify. apply le_n.assumption.
-apply trans_le ? (S(S (m1+i))).
+apply (trans_le ? (S(S (m1+i)))).
apply le_S.apply le_n.assumption.
apply eq_map_iter_i.
intros.apply eq_f.
apply sym_eq. apply eq_transpose.
simplify. intro.
-apply not_le_Sn_n i.
+apply (not_le_Sn_n i).
rewrite < H7 in \vdash (? ? %).
apply le_S_S.apply le_S.
apply le_plus_n.
simplify. intro.
-apply not_le_Sn_n i.
+apply (not_le_Sn_n i).
rewrite > H7 in \vdash (? ? %).
apply le_S_S.
apply le_plus_n.
simplify. intro.
-apply not_eq_n_Sn (S m1+i).
+apply (not_eq_n_Sn (S m1+i)).
apply sym_eq.assumption.
qed.
map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i j m)) f n.
intros.
simplify in H3.
-cut (S i) < j \lor (S i) = j.
+cut ((S i) < j \lor (S i) = j).
elim Hcut.
-cut j = S ((j - (S i)) + i).
+cut (j = S ((j - (S i)) + i)).
rewrite > Hcut1.
-apply eq_map_iter_i_transpose f H H1 n k (j - (S i)) g i.
+apply (eq_map_iter_i_transpose f H H1 n k (j - (S i)) g i).
assumption.
rewrite < Hcut1.assumption.
rewrite > plus_n_Sm.
apply plus_minus_m_m.apply lt_to_le.assumption.
rewrite < H5.
-apply eq_map_iter_i_transpose_i_Si f H H1 g.
+apply (eq_map_iter_i_transpose_i_Si f H H1 g).
simplify.
assumption.apply le_S_S_to_le.
-apply trans_le ? j.assumption.assumption.
+apply (trans_le ? j).assumption.assumption.
apply le_to_or_lt_eq.assumption.
qed.
\forall g:nat \to nat. n \le i \to i \le (S k+n) \to n \le j \to j \le (S k+n) \to
map_iter_i (S k) g f n = map_iter_i (S k) (\lambda m. g (transpose i j m)) f n.
intros.
-apply nat_compare_elim i j.
-intro.apply eq_map_iter_i_transpose1 f H H1 n k i j g H2 H6 H5.
+apply (nat_compare_elim i j).
+intro.apply (eq_map_iter_i_transpose1 f H H1 n k i j g H2 H6 H5).
intro.rewrite > H6.
apply eq_map_iter_i.intros.
-rewrite > transpose_i_i j.reflexivity.
+rewrite > (transpose_i_i j).reflexivity.
intro.
-apply trans_eq ? ? (map_iter_i (S k) (\lambda m:nat.g (transpose j i m)) f n).
-apply eq_map_iter_i_transpose1 f H H1 n k j i g H4 H6 H3.
+apply (trans_eq ? ? (map_iter_i (S k) (\lambda m:nat.g (transpose j i m)) f n)).
+apply (eq_map_iter_i_transpose1 f H H1 n k j i g H4 H6 H3).
apply eq_map_iter_i.
intros.apply eq_f.apply transpose_i_j_j_i.
qed.
permut h (k+n) \to (\forall m:nat. m \lt n \to h m = m) \to
map_iter_i k g f n = map_iter_i k (\lambda m.g(h m)) f n.
intros 4.elim k.
-simplify.rewrite > permut_n_to_eq_n h.reflexivity.assumption.assumption.
-apply trans_eq ? ? (map_iter_i (S n) (\lambda m.g ((transpose (h (S n+n1)) (S n+n1)) m)) f n1).
+simplify.rewrite > (permut_n_to_eq_n h).reflexivity.assumption.assumption.
+apply (trans_eq ? ? (map_iter_i (S n) (\lambda m.g ((transpose (h (S n+n1)) (S n+n1)) m)) f n1)).
unfold permut in H3.
elim H3.
-apply eq_map_iter_i_transpose2 f H H1 n1 n ? ? g.
-apply permut_n_to_le h n1 (S n+n1).
+apply (eq_map_iter_i_transpose2 f H H1 n1 n ? ? g).
+apply (permut_n_to_le h n1 (S n+n1)).
apply le_plus_n.assumption.assumption.apply le_plus_n.apply le_n.
apply H5.apply le_n.apply le_plus_n.apply le_n.
-apply trans_eq ? ? (map_iter_i (S n) (\lambda m.
+apply (trans_eq ? ? (map_iter_i (S n) (\lambda m.
(g(transpose (h (S n+n1)) (S n+n1)
-(transpose (h (S n+n1)) (S n+n1) (h m)))) )f n1).
+(transpose (h (S n+n1)) (S n+n1) (h m)))) )f n1)).
change with
-f (g (transpose (h (S n+n1)) (S n+n1) (S n+n1)))
+(f (g (transpose (h (S n+n1)) (S n+n1) (S n+n1)))
(map_iter_i n (\lambda m.
g (transpose (h (S n+n1)) (S n+n1) m)) f n1)
=
(map_iter_i n
(\lambda m.
(g(transpose (h (S n+n1)) (S n+n1)
-(transpose (h (S n+n1)) (S n+n1) (h m))))) f n1).
+(transpose (h (S n+n1)) (S n+n1) (h m))))) f n1)).
apply eq_f2.apply eq_f.
rewrite > transpose_i_j_j.
rewrite > transpose_i_j_i.
rewrite > transpose_i_j_j.reflexivity.
-apply H2 n1 (\lambda m.(g(transpose (h (S n+n1)) (S n+n1) m))).
+apply (H2 n1 (\lambda m.(g(transpose (h (S n+n1)) (S n+n1) m)))).
apply permut_S_to_permut_transpose.
assumption.
intros.
unfold transpose.
-rewrite > not_eq_to_eqb_false (h m) (h (S n+n1)).
-rewrite > not_eq_to_eqb_false (h m) (S n+n1).
+rewrite > (not_eq_to_eqb_false (h m) (h (S n+n1))).
+rewrite > (not_eq_to_eqb_false (h m) (S n+n1)).
simplify.apply H4.assumption.
rewrite > H4.
-apply lt_to_not_eq.apply trans_lt ? n1.assumption.
+apply lt_to_not_eq.apply (trans_lt ? n1).assumption.
simplify.apply le_S_S.apply le_plus_n.assumption.
unfold permut in H3.elim H3.
simplify.intro.
-apply lt_to_not_eq m (S n+n1).apply trans_lt ? n1.assumption.
+apply (lt_to_not_eq m (S n+n1)).apply (trans_lt ? n1).assumption.
simplify.apply le_S_S.apply le_plus_n.
unfold injn in H7.
-apply H7 m (S n+n1).apply trans_le ? n1.
+apply (H7 m (S n+n1)).apply (trans_le ? n1).
apply lt_to_le.assumption.apply le_plus_n.apply le_n.
assumption.
apply eq_map_iter_i.intros.
rewrite > transpose_transpose.reflexivity.
-qed.
-
+qed.
\ No newline at end of file
theorem injective_plus_l: \forall m:nat.injective nat nat (\lambda n.n+m).
intro.simplify.intros.
-apply injective_plus_r m.
+apply (injective_plus_r m).
rewrite < sym_plus.
-rewrite < sym_plus y.
+rewrite < (sym_plus y).
assumption.
qed.
theorem reflexive_divides : reflexive nat divides.
simplify.
intros.
-exact witness x x (S O) (times_n_SO x).
+exact (witness x x (S O) (times_n_SO x)).
qed.
theorem divides_to_div_mod_spec :
\forall n,m. O < n \to n \divides m \to div_mod_spec m n (m / n) O.
intros.elim H1.rewrite > H2.
constructor 1.assumption.
-apply lt_O_n_elim n H.intros.
+apply (lt_O_n_elim n H).intros.
rewrite < plus_n_O.
rewrite > div_times.apply sym_times.
qed.
theorem div_mod_spec_to_divides :
\forall n,m,p. div_mod_spec m n p O \to n \divides m.
intros.elim H.
-apply witness n m p.
+apply (witness n m p).
rewrite < sym_times.
-rewrite > plus_n_O (p*n).assumption.
+rewrite > (plus_n_O (p*n)).assumption.
qed.
theorem divides_to_mod_O:
\forall n,m. O < n \to n \divides m \to (m \mod n) = O.
-intros.apply div_mod_spec_to_eq2 m n (m / n) (m \mod n) (m / n) O.
+intros.apply (div_mod_spec_to_eq2 m n (m / n) (m \mod n) (m / n) O).
apply div_mod_spec_div_mod.assumption.
apply divides_to_div_mod_spec.assumption.assumption.
qed.
theorem mod_O_to_divides:
\forall n,m. O< n \to (m \mod n) = O \to n \divides m.
intros.
-apply witness n m (m / n).
-rewrite > plus_n_O (n * (m / n)).
+apply (witness n m (m / n)).
+rewrite > (plus_n_O (n * (m / n))).
rewrite < H1.
rewrite < sym_times.
(* Andrea: perche' hint non lo trova ?*)
qed.
theorem divides_n_O: \forall n:nat. n \divides O.
-intro. apply witness n O O.apply times_n_O.
+intro. apply (witness n O O).apply times_n_O.
qed.
theorem divides_n_n: \forall n:nat. n \divides n.
-intro. apply witness n n (S O).apply times_n_SO.
+intro. apply (witness n n (S O)).apply times_n_SO.
qed.
theorem divides_SO_n: \forall n:nat. (S O) \divides n.
-intro. apply witness (S O) n n. simplify.apply plus_n_O.
+intro. apply (witness (S O) n n). simplify.apply plus_n_O.
qed.
theorem divides_plus: \forall n,p,q:nat.
n \divides p \to n \divides q \to n \divides p+q.
intros.
-elim H.elim H1. apply witness n (p+q) (n2+n1).
+elim H.elim H1. apply (witness n (p+q) (n2+n1)).
rewrite > H2.rewrite > H3.apply sym_eq.apply distr_times_plus.
qed.
theorem divides_minus: \forall n,p,q:nat.
divides n p \to divides n q \to divides n (p-q).
intros.
-elim H.elim H1. apply witness n (p-q) (n2-n1).
+elim H.elim H1. apply (witness n (p-q) (n2-n1)).
rewrite > H2.rewrite > H3.apply sym_eq.apply distr_times_minus.
qed.
theorem divides_times: \forall n,m,p,q:nat.
n \divides p \to m \divides q \to n*m \divides p*q.
intros.
-elim H.elim H1. apply witness (n*m) (p*q) (n2*n1).
+elim H.elim H1. apply (witness (n*m) (p*q) (n2*n1)).
rewrite > H2.rewrite > H3.
-apply trans_eq nat ? (n*(m*(n2*n1))).
-apply trans_eq nat ? (n*(n2*(m*n1))).
+apply (trans_eq nat ? (n*(m*(n2*n1)))).
+apply (trans_eq nat ? (n*(n2*(m*n1)))).
apply assoc_times.
apply eq_f.
-apply trans_eq nat ? ((n2*m)*n1).
+apply (trans_eq nat ? ((n2*m)*n1)).
apply sym_eq. apply assoc_times.
-rewrite > sym_times n2 m.apply assoc_times.
+rewrite > (sym_times n2 m).apply assoc_times.
apply sym_eq. apply assoc_times.
qed.
theorem transitive_divides: transitive ? divides.
unfold.
intros.
-elim H.elim H1. apply witness x z (n2*n).
+elim H.elim H1. apply (witness x z (n2*n)).
rewrite > H3.rewrite > H2.
apply assoc_times.
qed.
theorem eq_mod_to_divides:\forall n,m,p. O< p \to
mod n p = mod m p \to divides p (n-m).
intros.
-cut n \le m \or \not n \le m.
+cut (n \le m \or \not n \le m).
elim Hcut.
-cut n-m=O.
+cut (n-m=O).
rewrite > Hcut1.
-apply witness p O O.
+apply (witness p O O).
apply times_n_O.
apply eq_minus_n_m_O.
assumption.
-apply witness p (n-m) ((div n p)-(div m p)).
+apply (witness p (n-m) ((div n p)-(div m p))).
rewrite > distr_times_minus.
rewrite > sym_times.
-rewrite > sym_times p.
-cut (div n p)*p = n - (mod n p).
+rewrite > (sym_times p).
+cut ((div n p)*p = n - (mod n p)).
rewrite > Hcut1.
rewrite > eq_minus_minus_minus_plus.
rewrite > sym_plus.
rewrite > sym_plus.
apply div_mod.
assumption.
-apply decidable_le n m.
+apply (decidable_le n m).
qed.
(* divides le *)
theorem divides_to_le : \forall n,m. O < m \to n \divides m \to n \le m.
-intros. elim H1.rewrite > H2.cut O < n2.
-apply lt_O_n_elim n2 Hcut.intro.rewrite < sym_times.
+intros. elim H1.rewrite > H2.cut (O < n2).
+apply (lt_O_n_elim n2 Hcut).intro.rewrite < sym_times.
simplify.rewrite < sym_plus.
apply le_plus_n.
-elim le_to_or_lt_eq O n2.
+elim (le_to_or_lt_eq O n2).
assumption.
-absurd O<m.assumption.
+absurd (O<m).assumption.
rewrite > H2.rewrite < H3.rewrite < times_n_O.
-apply not_le_Sn_n O.
+apply (not_le_Sn_n O).
apply le_O_n.
qed.
theorem divides_to_lt_O : \forall n,m. O < m \to n \divides m \to O < n.
intros.elim H1.
-elim le_to_or_lt_eq O n (le_O_n n).
+elim (le_to_or_lt_eq O n (le_O_n n)).
assumption.
-rewrite < H3.absurd O < m.assumption.
+rewrite < H3.absurd (O < m).assumption.
rewrite > H2.rewrite < H3.
-simplify.exact not_le_Sn_n O.
+simplify.exact (not_le_Sn_n O).
qed.
(* boolean divides *)
theorem decidable_divides: \forall n,m:nat.O < n \to
decidable (n \divides m).
-intros.change with (n \divides m) \lor n \ndivides m.
+intros.change with ((n \divides m) \lor n \ndivides m).
cut
-match divides_b n m with
+(match divides_b n m with
[ true \Rightarrow n \divides m
-| false \Rightarrow n \ndivides m] \to n \divides m \lor n \ndivides m.
+| false \Rightarrow n \ndivides m] \to n \divides m \lor n \ndivides m).
apply Hcut.apply divides_b_to_Prop.assumption.
elim (divides_b n m).left.apply H1.right.apply H1.
qed.
theorem divides_to_divides_b_true : \forall n,m:nat. O < n \to
n \divides m \to divides_b n m = true.
intros.
-cut match (divides_b n m) with
+cut (match (divides_b n m) with
[ true \Rightarrow n \divides m
-| false \Rightarrow n \ndivides m] \to ((divides_b n m) = true).
+| false \Rightarrow n \ndivides m] \to ((divides_b n m) = true)).
apply Hcut.apply divides_b_to_Prop.assumption.
-elim divides_b n m.reflexivity.
+elim (divides_b n m).reflexivity.
absurd (n \divides m).assumption.assumption.
qed.
theorem not_divides_to_divides_b_false: \forall n,m:nat. O < n \to
\lnot(n \divides m) \to (divides_b n m) = false.
intros.
-cut match (divides_b n m) with
+cut (match (divides_b n m) with
[ true \Rightarrow n \divides m
-| false \Rightarrow n \ndivides m] \to ((divides_b n m) = false).
+| false \Rightarrow n \ndivides m] \to ((divides_b n m) = false)).
apply Hcut.apply divides_b_to_Prop.assumption.
-elim divides_b n m.
+elim (divides_b n m).
absurd (n \divides m).assumption.assumption.
reflexivity.
qed.
theorem divides_f_pi_f : \forall f:nat \to nat.\forall n,m,i:nat.
m \le i \to i \le n+m \to f i \divides pi n f m.
intros 5.elim n.simplify.
-cut i = m.rewrite < Hcut.apply divides_n_n.
+cut (i = m).rewrite < Hcut.apply divides_n_n.
apply antisymmetric_le.assumption.assumption.
simplify.
-cut i < S n1+m \lor i = S n1 + m.
+cut (i < S n1+m \lor i = S n1 + m).
elim Hcut.
-apply transitive_divides ? (pi n1 f m).
+apply (transitive_divides ? (pi n1 f m)).
apply H1.apply le_S_S_to_le. assumption.
-apply witness ? ? (f (S n1+m)).apply sym_times.
+apply (witness ? ? (f (S n1+m))).apply sym_times.
rewrite > H3.
-apply witness ? ? (pi n1 f m).reflexivity.
+apply (witness ? ? (pi n1 f m)).reflexivity.
apply le_to_or_lt_eq.assumption.
qed.
(* divides and fact *)
theorem divides_fact : \forall n,i:nat.
O < i \to i \le n \to i \divides n!.
-intros 3.elim n.absurd O<i.assumption.apply le_n_O_elim i H1.
-apply not_le_Sn_O O.
-change with i \divides (S n1)*n1!.
-apply le_n_Sm_elim i n1 H2.
+intros 3.elim n.absurd (O<i).assumption.apply (le_n_O_elim i H1).
+apply (not_le_Sn_O O).
+change with (i \divides (S n1)*n1!).
+apply (le_n_Sm_elim i n1 H2).
intro.
-apply transitive_divides ? n1!.
+apply (transitive_divides ? n1!).
apply H1.apply le_S_S_to_le. assumption.
-apply witness ? ? (S n1).apply sym_times.
+apply (witness ? ? (S n1)).apply sym_times.
intro.
rewrite > H3.
-apply witness ? ? n1!.reflexivity.
+apply (witness ? ? n1!).reflexivity.
qed.
theorem mod_S_fact: \forall n,i:nat.
(S O) < i \to i \le n \to (S n!) \mod i = (S O).
-intros.cut n! \mod i = O.
+intros.cut (n! \mod i = O).
rewrite < Hcut.
-apply mod_S.apply trans_lt O (S O).apply le_n (S O).assumption.
+apply mod_S.apply (trans_lt O (S O)).apply (le_n (S O)).assumption.
rewrite > Hcut.assumption.
-apply divides_to_mod_O.apply trans_lt O (S O).apply le_n (S O).assumption.
-apply divides_fact.apply trans_lt O (S O).apply le_n (S O).assumption.
+apply divides_to_mod_O.apply (trans_lt O (S O)).apply (le_n (S O)).assumption.
+apply divides_fact.apply (trans_lt O (S O)).apply (le_n (S O)).assumption.
assumption.
qed.
(S O) < i \to i \le n \to i \ndivides S n!.
intros.
apply divides_b_false_to_not_divides.
-apply trans_lt O (S O).apply le_n (S O).assumption.
-change with (eqb ((S n!) \mod i) O) = false.
+apply (trans_lt O (S O)).apply (le_n (S O)).assumption.
+change with ((eqb ((S n!) \mod i) O) = false).
rewrite > mod_S_fact.simplify.reflexivity.
assumption.assumption.
qed.
(\forall m:nat. m \divides n \to (S O) < m \to m = n).
theorem not_prime_O: \lnot (prime O).
-simplify.intro.elim H.apply not_le_Sn_O (S O) H1.
+simplify.intro.elim H.apply (not_le_Sn_O (S O) H1).
qed.
theorem not_prime_SO: \lnot (prime (S O)).
-simplify.intro.elim H.apply not_le_Sn_n (S O) H1.
+simplify.intro.elim H.apply (not_le_Sn_n (S O) H1).
qed.
(* smallest factor *)
theorem lt_SO_smallest_factor:
\forall n:nat. (S O) < n \to (S O) < (smallest_factor n).
intro.
-apply nat_case n.intro.apply False_ind.apply not_le_Sn_O (S O) H.
-intro.apply nat_case m.intro. apply False_ind.apply not_le_Sn_n (S O) H.
+apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_O (S O) H).
+intro.apply (nat_case m).intro. apply False_ind.apply (not_le_Sn_n (S O) H).
intros.
change with
-S O < min_aux m1 (S(S m1)) (\lambda m.(eqb ((S(S m1)) \mod m) O)).
-apply lt_to_le_to_lt ? (S (S O)).
-apply le_n (S(S O)).
-cut (S(S O)) = (S(S m1)) - m1.
+(S O < min_aux m1 (S(S m1)) (\lambda m.(eqb ((S(S m1)) \mod m) O))).
+apply (lt_to_le_to_lt ? (S (S O))).
+apply (le_n (S(S O))).
+cut ((S(S O)) = (S(S m1)) - m1).
rewrite > Hcut.
apply le_min_aux.
apply sym_eq.apply plus_to_minus.
theorem lt_O_smallest_factor: \forall n:nat. O < n \to O < (smallest_factor n).
intro.
-apply nat_case n.intro.apply False_ind.apply not_le_Sn_n O H.
-intro.apply nat_case m.intro.
+apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_n O H).
+intro.apply (nat_case m).intro.
simplify.apply le_n.
-intros.apply trans_lt ? (S O).
+intros.apply (trans_lt ? (S O)).
simplify. apply le_n.
apply lt_SO_smallest_factor.simplify. apply le_S_S.
apply le_S_S.apply le_O_n.
theorem divides_smallest_factor_n :
\forall n:nat. O < n \to smallest_factor n \divides n.
intro.
-apply nat_case n.intro.apply False_ind.apply not_le_Sn_O O H.
-intro.apply nat_case m.intro. simplify.
-apply witness ? ? (S O). simplify.reflexivity.
+apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_O O H).
+intro.apply (nat_case m).intro. simplify.
+apply (witness ? ? (S O)). simplify.reflexivity.
intros.
apply divides_b_true_to_divides.
-apply lt_O_smallest_factor ? H.
+apply (lt_O_smallest_factor ? H).
change with
-eqb ((S(S m1)) \mod (min_aux m1 (S(S m1))
- (\lambda m.(eqb ((S(S m1)) \mod m) O)))) O = true.
+(eqb ((S(S m1)) \mod (min_aux m1 (S(S m1))
+ (\lambda m.(eqb ((S(S m1)) \mod m) O)))) O = true).
apply f_min_aux_true.
-apply ex_intro nat ? (S(S m1)).
+apply (ex_intro nat ? (S(S m1))).
split.split.
apply le_minus_m.apply le_n.
rewrite > mod_n_n.reflexivity.
-apply trans_lt ? (S O).apply le_n (S O).simplify.
+apply (trans_lt ? (S O)).apply (le_n (S O)).simplify.
apply le_S_S.apply le_S_S.apply le_O_n.
qed.
theorem le_smallest_factor_n :
\forall n:nat. smallest_factor n \le n.
-intro.apply nat_case n.simplify.reflexivity.
-intro.apply nat_case m.simplify.reflexivity.
+intro.apply (nat_case n).simplify.reflexivity.
+intro.apply (nat_case m).simplify.reflexivity.
intro.apply divides_to_le.
simplify.apply le_S_S.apply le_O_n.
apply divides_smallest_factor_n.
theorem lt_smallest_factor_to_not_divides: \forall n,i:nat.
(S O) < n \to (S O) < i \to i < (smallest_factor n) \to i \ndivides n.
intros 2.
-apply nat_case n.intro.apply False_ind.apply not_le_Sn_O (S O) H.
-intro.apply nat_case m.intro. apply False_ind.apply not_le_Sn_n (S O) H.
+apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_O (S O) H).
+intro.apply (nat_case m).intro. apply False_ind.apply (not_le_Sn_n (S O) H).
intros.
apply divides_b_false_to_not_divides.
-apply trans_lt O (S O).apply le_n (S O).assumption.
-change with (eqb ((S(S m1)) \mod i) O) = false.
-apply lt_min_aux_to_false
-(\lambda i:nat.eqb ((S(S m1)) \mod i) O) (S(S m1)) m1 i.
-cut (S(S O)) = (S(S m1)-m1).
+apply (trans_lt O (S O)).apply (le_n (S O)).assumption.
+change with ((eqb ((S(S m1)) \mod i) O) = false).
+apply (lt_min_aux_to_false
+(\lambda i:nat.eqb ((S(S m1)) \mod i) O) (S(S m1)) m1 i).
+cut ((S(S O)) = (S(S m1)-m1)).
rewrite < Hcut.exact H1.
apply sym_eq. apply plus_to_minus.
rewrite < sym_plus.simplify.reflexivity.
theorem prime_smallest_factor_n :
\forall n:nat. (S O) < n \to prime (smallest_factor n).
-intro. change with (S(S O)) \le n \to (S O) < (smallest_factor n) \land
-(\forall m:nat. m \divides smallest_factor n \to (S O) < m \to m = (smallest_factor n)).
+intro. change with ((S(S O)) \le n \to (S O) < (smallest_factor n) \land
+(\forall m:nat. m \divides smallest_factor n \to (S O) < m \to m = (smallest_factor n))).
intro.split.
apply lt_SO_smallest_factor.assumption.
intros.
-cut le m (smallest_factor n).
-elim le_to_or_lt_eq m (smallest_factor n) Hcut.
-absurd m \divides n.
-apply transitive_divides m (smallest_factor n).
+cut (le m (smallest_factor n)).
+elim (le_to_or_lt_eq m (smallest_factor n) Hcut).
+absurd (m \divides n).
+apply (transitive_divides m (smallest_factor n)).
assumption.
apply divides_smallest_factor_n.
-apply trans_lt ? (S O). simplify. apply le_n. exact H.
+apply (trans_lt ? (S O)). simplify. apply le_n. exact H.
apply lt_smallest_factor_to_not_divides.
exact H.assumption.assumption.assumption.
apply divides_to_le.
-apply trans_lt O (S O).
-apply le_n (S O).
+apply (trans_lt O (S O)).
+apply (le_n (S O)).
apply lt_SO_smallest_factor.
exact H.
assumption.
theorem prime_to_smallest_factor: \forall n. prime n \to
smallest_factor n = n.
-intro.apply nat_case n.intro.apply False_ind.apply not_prime_O H.
-intro.apply nat_case m.intro.apply False_ind.apply not_prime_SO H.
+intro.apply (nat_case n).intro.apply False_ind.apply (not_prime_O H).
+intro.apply (nat_case m).intro.apply False_ind.apply (not_prime_SO H).
intro.
change with
-(S O) < (S(S m1)) \land
+((S O) < (S(S m1)) \land
(\forall m:nat. m \divides S(S m1) \to (S O) < m \to m = (S(S m1))) \to
-smallest_factor (S(S m1)) = (S(S m1)).
+smallest_factor (S(S m1)) = (S(S m1))).
intro.elim H.apply H2.
apply divides_smallest_factor_n.
-apply trans_lt ? (S O).simplify. apply le_n.assumption.
+apply (trans_lt ? (S O)).simplify. apply le_n.assumption.
apply lt_SO_smallest_factor.
assumption.
qed.
[ true \Rightarrow prime n
| false \Rightarrow \lnot (prime n)].
intro.
-apply nat_case n.simplify.intro.elim H.apply not_le_Sn_O (S O) H1.
-intro.apply nat_case m.simplify.intro.elim H.apply not_le_Sn_n (S O) H1.
+apply (nat_case n).simplify.intro.elim H.apply (not_le_Sn_O (S O) H1).
+intro.apply (nat_case m).simplify.intro.elim H.apply (not_le_Sn_n (S O) H1).
intro.
change with
match eqb (smallest_factor (S(S m1))) (S(S m1)) with
[ true \Rightarrow prime (S(S m1))
| false \Rightarrow \lnot (prime (S(S m1)))].
-apply eqb_elim (smallest_factor (S(S m1))) (S(S m1)).
-intro.change with prime (S(S m1)).
+apply (eqb_elim (smallest_factor (S(S m1))) (S(S m1))).
+intro.change with (prime (S(S m1))).
rewrite < H.
apply prime_smallest_factor_n.
simplify.apply le_S_S.apply le_S_S.apply le_O_n.
-intro.change with \lnot (prime (S(S m1))).
-change with prime (S(S m1)) \to False.
+intro.change with (\lnot (prime (S(S m1)))).
+change with (prime (S(S m1)) \to False).
intro.apply H.
apply prime_to_smallest_factor.
assumption.
qed.
theorem decidable_prime : \forall n:nat.decidable (prime n).
-intro.change with (prime n) \lor \lnot (prime n).
+intro.change with ((prime n) \lor \lnot (prime n)).
cut
-match primeb n with
+(match primeb n with
[ true \Rightarrow prime n
-| false \Rightarrow \lnot (prime n)] \to (prime n) \lor \lnot (prime n).
+| false \Rightarrow \lnot (prime n)] \to (prime n) \lor \lnot (prime n)).
apply Hcut.apply primeb_to_Prop.
elim (primeb n).left.apply H.right.apply H.
qed.
theorem prime_to_primeb_true: \forall n:nat.
prime n \to primeb n = true.
intros.
-cut match (primeb n) with
+cut (match (primeb n) with
[ true \Rightarrow prime n
-| false \Rightarrow \lnot (prime n)] \to ((primeb n) = true).
+| false \Rightarrow \lnot (prime n)] \to ((primeb n) = true)).
apply Hcut.apply primeb_to_Prop.
-elim primeb n.reflexivity.
+elim (primeb n).reflexivity.
absurd (prime n).assumption.assumption.
qed.
theorem not_prime_to_primeb_false: \forall n:nat.
\lnot(prime n) \to primeb n = false.
intros.
-cut match (primeb n) with
+cut (match (primeb n) with
[ true \Rightarrow prime n
-| false \Rightarrow \lnot (prime n)] \to ((primeb n) = false).
+| false \Rightarrow \lnot (prime n)] \to ((primeb n) = false)).
apply Hcut.apply primeb_to_Prop.
-elim primeb n.
+elim (primeb n).
absurd (prime n).assumption.assumption.
reflexivity.
qed.
theorem times_plus_l: \forall n,m,p:nat. (n+m)*p = n*p + m*p.
intros.
-apply trans_eq ? ? (p*(n+m)).
+apply (trans_eq ? ? (p*(n+m))).
apply sym_times.
-apply trans_eq ? ? (p*n+p*m).
+apply (trans_eq ? ? (p*n+p*m)).
apply distr_times_plus.
apply eq_f2.
apply sym_times.
theorem times_minus_l: \forall n,m,p:nat. (n-m)*p = n*p - m*p.
intros.
-apply trans_eq ? ? (p*(n-m)).
+apply (trans_eq ? ? (p*(n-m))).
apply sym_times.
-apply trans_eq ? ? (p*n-p*m).
+apply (trans_eq ? ? (p*n-p*m)).
apply distr_times_minus.
apply eq_f2.
apply sym_times.
theorem times_plus_plus: \forall n,m,p,q:nat. (n + m)*(p + q) =
n*p + n*q + m*p + m*q.
intros.
-apply trans_eq nat ? ((n*(p+q) + m*(p+q))).
+apply (trans_eq nat ? ((n*(p+q) + m*(p+q)))).
apply times_plus_l.
rewrite > distr_times_plus.
rewrite > distr_times_plus.
simplify.apply H.apply le_n.rewrite < plus_n_O.apply le_n.
simplify.
apply eq_f2.apply H1.
-change with m \le (S n1)+m.apply le_plus_n.
-rewrite > sym_plus m.apply le_n.
+change with (m \le (S n1)+m).apply le_plus_n.
+rewrite > (sym_plus m).apply le_n.
apply H.intros.apply H1.assumption.
rewrite < plus_n_Sm.
apply le_S.assumption.
simplify.apply H.apply le_n.rewrite < plus_n_O.apply le_n.
simplify.
apply eq_f2.apply H1.
-change with m \le (S n1)+m.apply le_plus_n.
-rewrite > sym_plus m.apply le_n.
+change with (m \le (S n1)+m).apply le_plus_n.
+rewrite > (sym_plus m).apply le_n.
apply H.intros.apply H1.assumption.
rewrite < plus_n_Sm.
apply le_S.assumption.
theorem eq_fact_pi: \forall n. (S n)! = pi n (\lambda m.m) (S O).
intro.elim n.
simplify.reflexivity.
-change with (S(S n1))*(S n1)! = ((S n1)+(S O))*(pi n1 (\lambda m.m) (S O)).
+change with ((S(S n1))*(S n1)! = ((S n1)+(S O))*(pi n1 (\lambda m.m) (S O))).
rewrite < plus_n_Sm.rewrite < plus_n_O.
apply eq_f.assumption.
qed.
intros.elim x.
simplify.reflexivity.
simplify.rewrite > H. rewrite > assoc_plus.rewrite > assoc_plus.
-apply eq_f.rewrite < assoc_plus. rewrite < sym_plus ? z.
+apply eq_f.rewrite < assoc_plus. rewrite < (sym_plus ? z).
rewrite > assoc_plus.reflexivity.
qed.
simplify.rewrite < sym_times.
rewrite > distr_times_plus.
rewrite < sym_times.
-rewrite < sym_times (times n y) z.
+rewrite < (sym_times (times n y) z).
rewrite < H.apply refl_eq.
qed.
alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
theorem t: (\forall x:nat. x=x) \to True.
intro H.
- change in match x in H : \forall _.% with 0+x.
+ change in match x in H : \forall _.% with (0+x).
change in H: \forall _.(? ? ? (? % ?)) with 0.
constructor 1.
qed.
\forall a: True.
\forall b: 0 = 0.
0 = 0.
-intros 1 [H] .
+intros 1 (H).
clear H.
-intros 1 [H].
+intros 1 (H).
exact H.
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 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/test/continuationals/".
+include "coq.ma".
+
+alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
+alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
+alias id "trans_equal" = "cic:/Coq/Init/Logic/trans_equal.con".
+alias id "refl_equal" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)".
+alias id "Z" = "cic:/Coq/ZArith/BinInt/Z.ind#xpointer(1/1)".
+
+theorem semicolon: \forall p:Prop.p\to p\land p.
+intros (p); split; assumption.
+qed.
+
+theorem branch:\forall x:nat.x=x.
+intros (n);
+elim n
+[ reflexivity;
+| reflexivity ].
+qed.
+
+theorem pos:\forall x:Z.x=x.
+intros (n);
+elim n;
+[ 3: reflexivity;
+| 2: reflexivity;
+| reflexivity ]
+qed.
+
+theorem dot:\forall x:Z.x=x.
+intros (x).
+elim x.
+reflexivity. reflexivity. reflexivity.
+qed.
+
+theorem dot_slice:\forall x:Z.x=x.
+intros (x).
+elim x;
+[ elim x. reflexivity. reflexivity. reflexivity;
+| reflexivity
+| reflexivity ];
+qed.
+
+theorem focus:\forall x:Z.x=x.
+intros (x); elim x.
+focus 16 17;
+ reflexivity;
+unfocus.
+reflexivity.
+qed.
+
+theorem skip:\forall x:nat.x=x.
+intros (x).
+apply trans_equal;
+[ 2: apply (refl_equal nat x);
+| skip
+| reflexivity
+]
+qed.
+
+theorem skip_focus:\forall x:nat.x=x.
+intros (x).
+apply trans_equal;
+[ focus 18; apply (refl_equal nat x); unfocus;
+| skip
+| reflexivity ]
+qed.
alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
theorem stupid: 3 = 3.
- cut 3 = 3.
+ cut (3 = 3).
assumption.
reflexivity.
- qed.
+qed.
theorem test_inversion: \forall n. le n O \to n=O.
intros.
(* inversion begins *)
- cut O=O.
- (* goal 2: 0 = 0 *)
- goal 7. reflexivity.
- (* goal 1 *)
- generalize in match Hcut.
- apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H).
- (* first goal (left open) *)
- intro. rewrite < H1.
- clear Hcut.
- (* second goal (closed) *)
- goal 14.
- simplify. intros.
- discriminate H3.
- (* inversion ends *)
+ cut (O=O);
+ [ 2: reflexivity;
+ | generalize in match Hcut.
+ apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H);
+ [ intro. rewrite < H1. clear Hcut.
+ | simplify. intros. discriminate H3.
+ ]
reflexivity.
+ ]
qed.
(* Piu' semplice e non lascia l'ipotesi inutile Hcut *)
intros.
(* inversion begins *)
generalize in match (refl_equal nat O).
- apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H).
- (* first goal (left open) *)
- intro. rewrite < H1.
- (* second goal (closed) *)
- goal 13.
- simplify. intros.
- discriminate H3.
- (* inversion ends *)
+ apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H);
+ [ intro. rewrite < H1.
+ | simplify. intros. discriminate H3.
+ ]
reflexivity.
qed.
\forall P:Prop.
\forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
1 = 1 \land 1 = 0 \land 2 = 2.
- intros. split. split.
- goal 13.
- rewrite > H; [reflexivity | exact nat | exact 0=0 | exact Type].
- reflexivity.
- reflexivity.
+ intros. split; split;
+ [ reflexivity
+ | rewrite > H;
+ [ reflexivity | exact nat | exact (0=0) | exact Type ]
+ ]
qed.
theorem th2 :
\forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
1 = 1 \land 1 = 0 \land 3 = 3.
intros. split. split.
- goal 13.
- rewrite > H ?; [reflexivity | exact nat | exact 0=0 | exact Type].
+ focus 13.
+ rewrite > (H ?); [reflexivity | exact nat | exact (0=0) | exact Type].
+ unfocus.
reflexivity.
reflexivity.
qed.
\forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
1 = 1 \land 1 = 0 \land 4 = 4.
intros. split. split.
- goal 13.
- rewrite > H ? ?; [reflexivity | exact nat | exact 0=0 | exact Type].
+ focus 13.
+ rewrite > (H ? ?); [reflexivity | exact nat | exact (0=0) | exact Type].
+ unfocus.
reflexivity.
reflexivity.
qed.
\forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
1 = 1 \land 1 = 0 \land 5 = 5.
intros. split. split.
- goal 13.
- rewrite > H ? ? ?; [reflexivity | exact nat | exact 0=0 | exact Type].
+ focus 13.
+ rewrite > (H ? ? ?); [reflexivity | exact nat | exact (0=0) | exact Type].
+ unfocus.
reflexivity.
reflexivity.
qed.
\forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
1 = 1 \land 1 = 0 \land 6 = 6.
intros. split. split.
- goal 13.
- apply H; [exact nat | exact 0=0 | exact Type].
+ focus 13.
+ apply H; [exact nat | exact (0=0) | exact Type].
+ unfocus.
reflexivity.
reflexivity.
qed.
\forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
1 = 1 \land 1 = 0 \land 7 = 7.
intros. split. split.
- goal 13.
- apply H ?; [exact nat | exact 0=0 | exact Type].
+ focus 13.
+ apply (H ?); [exact nat | exact (0=0) | exact Type].
+ unfocus.
reflexivity.
reflexivity.
qed.
\forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
1 = 1 \land 1 = 0 \land 8 = 8.
intros. split. split.
- goal 13.
- apply H ? ?; [exact nat | exact 0=0 | exact Type].
+ focus 13.
+ apply (H ? ?); [exact nat | exact (0=0) | exact Type].
+ unfocus.
reflexivity.
reflexivity.
qed.
\forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
1 = 1 \land 1 = 0 \land 9 = 9.
intros. split. split.
- goal 13.
- apply H ? ? ?; [exact nat | exact 0=0 | exact Type].
+ focus 13.
+ apply (H ? ? ?); [exact nat | exact (0=0) | exact Type].
+ unfocus.
reflexivity.
reflexivity.
qed.
theorem th9:
\forall P,Q,R,S : Prop. R \to S \to \forall E:(R \to S \to P \land Q). P \land Q.
- intros [P; Q; R; S; r; s; H].
- elim H ? ?; [split; assumption | exact r | exact s].
+ intros (P Q R S r s H).
+ elim (H ? ?); [split; assumption | exact r | exact s].
qed.
theorem th10:
\forall P,Q,R,S : Prop. R \to S \to \forall E:(R \to S \to P \land Q). P \land Q.
- intros [P; Q; R; S; r; s; H].
- elim H ?; [split; assumption | exact r | exact s].
+ intros (P Q R S r s H).
+ elim (H ?); [split; assumption | exact r | exact s].
qed.
theorem th11:
\forall P,Q,R,S : Prop. R \to S \to \forall E:(R \to S \to P \land Q). P \land Q.
- intros [P; Q; R; S; r; s; H].
+ intros (P Q R S r s H).
elim H; [split; assumption | exact r | exact s].
qed.
-
-
-
-
-
-
-
-
-
-
\ No newline at end of file
intro.
replace in \vdash (? ? (? ? %) (? % %)) with x.
reflexivity.
- rewrite < mult_n_O x.
- rewrite < plus_n_O x.
+ rewrite < (mult_n_O x).
+ rewrite < (plus_n_O x).
reflexivity.
reflexivity.
auto.
(* This test tests "replace in match t" where t contains some metavariables *)
theorem t2: 2 + (3 * 4) = (5 + 5) + 2 * 2.
- replace in match 5+? with 6 + 4; [reflexivity | reflexivity].
+ replace in match 5+? with (6 + 4); [reflexivity | reflexivity].
qed.
alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
alias id "not" = "cic:/Coq/Init/Logic/not.con".
-
+alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
+alias id "plus_comm" = "cic:/Coq/Arith/Plus/plus_comm.con".
theorem a :
\forall A:Set.
intros. simplify. change in \vdash (? ? (? %) ?) with O.
reflexivity. qed.
+
theorem X: \forall x:nat. let myplus \def plus x in myplus (S O) = S x.
- intros. simplify. change in \vdash (? ? (% ?) ?) with plus x.
- rewrite > plus_comm. reflexivity. qed.
+ intros. simplify. change in \vdash (? ? (% ?) ?) with (plus x).
+
+rewrite > plus_comm. reflexivity. qed.
theorem R: \forall x:nat. let uno \def x + O in S O + uno = 1 + x.
intros. simplify.
- change in \vdash (? ? (? %) ?) with x + O.
+ change in \vdash (? ? (? %) ?) with (x + O).
rewrite > plus_comm. reflexivity. qed.
alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
theorem a:\forall x.x=x.
alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
-exact nat.
-intro.
-reflexivity.
+[ exact nat.
+| intro. reflexivity.
+]
qed.
alias num (instance 0) = "natural number".
alias symbol "times" (instance 0) = "Coq's natural times".
projects / helm.git / commitdiff