(**************************************************************************)
-(* ___ *)
+(* __ *)
(* ||M|| *)
(* ||A|| A project by Andrea Asperti *)
(* ||T|| *)
set "baseuri" "cic:/matita/Z/times".
+include "nat/lt_arith.ma".
include "Z/z.ma".
definition Ztimes :Z \to Z \to Z \def
simplify.reflexivity.
qed.
-(*CSC: da qui in avanti niente notazione *)
-(*
theorem symmetric_Ztimes : symmetric Z Ztimes.
change with \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x).
intros.elim x.rewrite > Ztimes_z_OZ.reflexivity.
elim y.simplify.reflexivity.
-change with eq Z (pos (pred (times (S e1) (S e)))) (pos (pred (times (S e) (S e1)))).
+change with eq Z (pos (pred (times (S n) (S n1)))) (pos (pred (times (S n1) (S n)))).
rewrite < sym_times.reflexivity.
-change with eq Z (neg (pred (times (S e1) (S e2)))) (neg (pred (times (S e2) (S e1)))).
+change with eq Z (neg (pred (times (S n) (S n1)))) (neg (pred (times (S n1) (S n)))).
rewrite < sym_times.reflexivity.
elim y.simplify.reflexivity.
-change with eq Z (neg (pred (times (S e2) (S e1)))) (neg (pred (times (S e1) (S e2)))).
+change with eq Z (neg (pred (times (S n) (S n1)))) (neg (pred (times (S n1) (S n)))).
rewrite < sym_times.reflexivity.
-change with eq Z (pos (pred (times (S e2) (S e)))) (pos (pred (times (S e) (S e2)))).
+change with eq Z (pos (pred (times (S n) (S n1)))) (pos (pred (times (S n1) (S n)))).
rewrite < sym_times.reflexivity.
qed.
elim y.simplify.reflexivity.
elim z.simplify.reflexivity.
change with
-eq Z (neg (pred (times (S (pred (times (S e1) (S e)))) (S e2))))
- (neg (pred (times (S e1) (S (pred (times (S e) (S e2))))))).
-rewrite < S_pred_S.
-
-theorem Zpred_Zplus_neg_O : \forall z:Z. eq Z (Zpred z) (Zplus (neg O) z).
-intros.elim z.
-simplify.reflexivity.
-simplify.reflexivity.
-elim e2.simplify.reflexivity.
-simplify.reflexivity.
-qed.
-
-theorem Zsucc_Zplus_pos_O : \forall z:Z. eq Z (Zsucc z) (Zplus (pos O) z).
-intros.elim z.
-simplify.reflexivity.
-elim e1.simplify.reflexivity.
-simplify.reflexivity.
-simplify.reflexivity.
-qed.
-
-theorem Zplus_pos_pos:
-\forall n,m. eq Z (Zplus (pos n) (pos m)) (Zplus (Zsucc (pos n)) (Zpred (pos m))).
-intros.
-elim n.elim m.
-simplify.reflexivity.
-simplify.reflexivity.
-elim m.
+eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
+ (neg (pred (times (S n) (S (pred (times (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
+eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
+ (pos (pred (times (S n) (S (pred (times (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
+eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
+ (pos(pred (times (S n) (S (pred (times (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
+eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
+ (neg (pred (times (S n) (S (pred (times (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.simplify.reflexivity.
+elim z.simplify.reflexivity.
+change with
+eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
+ (pos (pred (times (S n) (S (pred (times (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
+eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
+ (neg (pred (times (S n) (S (pred (times (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
+eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
+ (neg(pred (times (S n) (S (pred (times (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
+eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
+ (pos (pred (times (S n) (S (pred (times (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.
+
+variant assoc_Ztimes : \forall x,y,z:Z.
+eq Z (Ztimes (Ztimes x y) z) (Ztimes x (Ztimes y z)) \def
+associative_Ztimes.
+
+
+theorem distributive_Ztimes: distributive Z Ztimes Zplus.
+change with \forall x,y,z:Z.
+eq Z (Ztimes x (Zplus y z)) (Zplus (Ztimes x y) (Ztimes x z)).
+intros.elim x.
+simplify.reflexivity.
+(* case x = neg n *)
+elim y.reflexivity.
+elim z.reflexivity.
+change with
+eq Z (pos (pred (times (S n) (plus (S n1) (S n2)))))
+ (pos (pred (plus (times (S n) (S n1))(times (S n) (S n2))))).
+rewrite < times_plus_distr.reflexivity.
+simplify. (* problemi di naming su n *)
+(* sintassi della change ??? *)
+cut \forall n,m:nat.eq nat (plus m (times n (S m))) (pred (times (S n) (S m))).
+rewrite > Hcut.
+rewrite > Hcut.
+rewrite < nat_compare_pred_pred ? ? ? ?.
+rewrite < nat_compare_times_l.
+rewrite < nat_compare_S_S.
+apply nat_compare_elim n1 n2.
+intro.
+(* per ricavare questo change ci ho messo un'ora;
+LA GESTIONE DELLA RIDUZIONE NON VA *)
+change with (eq Z (neg (pred (times (S n) (S (pred (minus (S n2) (S n1)))))))
+ (neg (pred (minus (pred (times (S n) (S n2)))
+ (pred (times (S n) (S n1))))))).
+rewrite < S_pred ? ?.
+rewrite > minus_pred_pred ? ? ? ?.
+rewrite < distr_times_minus.
+reflexivity.
+(* we start closing stupid positivity conditions *)
+apply lt_O_times_S_S.
+apply lt_O_times_S_S.
simplify.
-rewrite < plus_n_O.reflexivity.
+apply le_SO_minus. exact H.
+intro.rewrite < H.simplify.reflexivity.
+intro.
+change with (eq Z (pos (pred (times (S n) (S (pred (minus (S n1) (S n2)))))))
+ (pos (pred (minus (pred (times (S n) (S n1)))
+ (pred (times (S n) (S n2))))))).
+rewrite < S_pred ? ?.
+rewrite > minus_pred_pred ? ? ? ?.
+rewrite < distr_times_minus.
+reflexivity.
+(* we start closing stupid positivity conditions *)
+apply lt_O_times_S_S.
+apply lt_O_times_S_S.
simplify.
-rewrite < plus_n_Sm.reflexivity.
-qed.
-
-theorem Zplus_pos_neg:
-\forall n,m. eq Z (Zplus (pos n) (neg m)) (Zplus (Zsucc (pos n)) (Zpred (neg m))).
-intros.reflexivity.
-qed.
-
-theorem Zplus_neg_pos :
-\forall n,m. eq Z (Zplus (neg n) (pos m)) (Zplus (Zsucc (neg n)) (Zpred (pos m))).
-intros.
-elim n.elim m.
-simplify.reflexivity.
-simplify.reflexivity.
-elim m.
-simplify.reflexivity.
-simplify.reflexivity.
-qed.
-
-theorem Zplus_neg_neg:
-\forall n,m. eq Z (Zplus (neg n) (neg m)) (Zplus (Zsucc (neg n)) (Zpred (neg m))).
-intros.
-elim n.elim m.
-simplify.reflexivity.
-simplify.reflexivity.
-elim m.
-simplify.rewrite < plus_n_Sm.reflexivity.
-simplify.rewrite > plus_n_Sm.reflexivity.
-qed.
-
-theorem Zplus_Zsucc_Zpred:
-\forall x,y. eq Z (Zplus x y) (Zplus (Zsucc x) (Zpred y)).
-intros.
-elim x. elim y.
-simplify.reflexivity.
-simplify.reflexivity.
-rewrite < Zsucc_Zplus_pos_O.
-rewrite > Zsucc_Zpred.reflexivity.
-elim y.rewrite < sym_Zplus.rewrite < sym_Zplus (Zpred OZ).
-rewrite < Zpred_Zplus_neg_O.
-rewrite > Zpred_Zsucc.
-simplify.reflexivity.
-rewrite < Zplus_neg_neg.reflexivity.
-apply Zplus_neg_pos.
-elim y.simplify.reflexivity.
-apply Zplus_pos_neg.
-apply Zplus_pos_pos.
-qed.
-
-theorem Zplus_Zsucc_pos_pos :
-\forall n,m. eq Z (Zplus (Zsucc (pos n)) (pos m)) (Zsucc (Zplus (pos n) (pos m))).
+apply le_SO_minus. exact H.
+(* questi non so neppure da dove vengano *)
+apply lt_O_times_S_S.
+apply lt_O_times_S_S.
+(* adesso chiudo il cut stupido *)
intros.reflexivity.
-qed.
-
-theorem Zplus_Zsucc_pos_neg:
-\forall n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m))).
-intros.
-apply nat_elim2
-(\lambda n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m)))).intro.
-intros.elim n1.
-simplify. reflexivity.
-elim e1.simplify. reflexivity.
-simplify. reflexivity.
-intros. elim n1.
-simplify. reflexivity.
-simplify.reflexivity.
-intros.
-rewrite < (Zplus_pos_neg ? m1).
-elim H.reflexivity.
-qed.
-
-theorem Zplus_Zsucc_neg_neg :
-\forall n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m))).
-intros.
-apply nat_elim2
-(\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m)))).intro.
-intros.elim n1.
-simplify. reflexivity.
-elim e1.simplify. reflexivity.
-simplify. reflexivity.
-intros. elim n1.
-simplify. reflexivity.
-simplify.reflexivity.
-intros.
-rewrite < (Zplus_neg_neg ? m1).
-reflexivity.
-qed.
-
-theorem Zplus_Zsucc_neg_pos:
-\forall n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m))).
-intros.
-apply nat_elim2
-(\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m)))).
-intros.elim n1.
-simplify. reflexivity.
-elim e1.simplify. reflexivity.
-simplify. reflexivity.
-intros. elim n1.
-simplify. reflexivity.
-simplify.reflexivity.
-intros.
-rewrite < H.
-rewrite < (Zplus_neg_pos ? (S m1)).
-reflexivity.
-qed.
-
-theorem Zplus_Zsucc : \forall x,y:Z. eq Z (Zplus (Zsucc x) y) (Zsucc (Zplus x y)).
-intros.elim x.elim y.
-simplify. reflexivity.
-rewrite < Zsucc_Zplus_pos_O.reflexivity.
-simplify.reflexivity.
-elim y.rewrite < sym_Zplus.rewrite < sym_Zplus OZ.simplify.reflexivity.
-apply Zplus_Zsucc_neg_neg.
-apply Zplus_Zsucc_neg_pos.
-elim y.
-rewrite < sym_Zplus OZ.reflexivity.
-apply Zplus_Zsucc_pos_neg.
-apply Zplus_Zsucc_pos_pos.
-qed.
-
-theorem Zplus_Zpred: \forall x,y:Z. eq Z (Zplus (Zpred x) y) (Zpred (Zplus x y)).
-intros.
-cut eq Z (Zpred (Zplus x y)) (Zpred (Zplus (Zsucc (Zpred x)) y)).
+elim z.reflexivity.
+simplify.
+cut \forall n,m:nat.eq nat (plus m (times n (S m))) (pred (times (S n) (S m))).
rewrite > Hcut.
-rewrite > Zplus_Zsucc.
-rewrite > Zpred_Zsucc.
-reflexivity.
-rewrite > Zsucc_Zpred.
-reflexivity.
-qed.
-
-
-theorem associative_Zplus: associative Z Zplus.
-change with \forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z)).
-
-intros.elim x.simplify.reflexivity.
-elim e1.rewrite < (Zpred_Zplus_neg_O (Zplus y z)).
-rewrite < (Zpred_Zplus_neg_O y).
-rewrite < Zplus_Zpred.
-reflexivity.
-rewrite > Zplus_Zpred (neg e).
-rewrite > Zplus_Zpred (neg e).
-rewrite > Zplus_Zpred (Zplus (neg e) y).
-apply eq_f.assumption.
-elim e2.rewrite < Zsucc_Zplus_pos_O.
-rewrite < Zsucc_Zplus_pos_O.
-rewrite > Zplus_Zsucc.
+rewrite > Hcut.
+rewrite < nat_compare_pred_pred ? ? ? ?.
+rewrite < nat_compare_times_l.
+rewrite < nat_compare_S_S.
+apply nat_compare_elim n1 n2.
+intro.
+(* per ricavare questo change ci ho messo un'ora;
+LA GESTIONE DELLA RIDUZIONE NON VA *)
+change with (eq Z (pos (pred (times (S n) (S (pred (minus (S n2) (S n1)))))))
+ (pos (pred (minus (pred (times (S n) (S n2)))
+ (pred (times (S n) (S n1))))))).
+rewrite < S_pred ? ?.
+rewrite > minus_pred_pred ? ? ? ?.
+rewrite < distr_times_minus.
+reflexivity.
+(* we start closing stupid positivity conditions *)
+apply lt_O_times_S_S.
+apply lt_O_times_S_S.
+simplify.
+apply le_SO_minus. exact H.
+intro.rewrite < H.simplify.reflexivity.
+intro.
+change with (eq Z (neg (pred (times (S n) (S (pred (minus (S n1) (S n2)))))))
+ (neg (pred (minus (pred (times (S n) (S n1)))
+ (pred (times (S n) (S n2))))))).
+rewrite < S_pred ? ?.
+rewrite > minus_pred_pred ? ? ? ?.
+rewrite < distr_times_minus.
+reflexivity.
+(* we start closing stupid positivity conditions *)
+apply lt_O_times_S_S.
+apply lt_O_times_S_S.
+simplify.
+apply le_SO_minus. exact H.
+(* questi non so neppure da dove vengano *)
+apply lt_O_times_S_S.
+apply lt_O_times_S_S.
+(* adesso chiudo il cut stupido *)
+intros.reflexivity.
+change with
+eq Z (neg (pred (times (S n) (plus (S n1) (S n2)))))
+ (neg (pred (plus (times (S n) (S n1))(times (S n) (S n2))))).
+rewrite < times_plus_distr.
reflexivity.
-rewrite > Zplus_Zsucc (pos e1).
-rewrite > Zplus_Zsucc (pos e1).
-rewrite > Zplus_Zsucc (Zplus (pos e1) y).
-apply eq_f.assumption.
-qed.
-
-variant assoc_Zplus : \forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z))
-\def associative_Zplus.
-*)
+(* and now the case x = pos n *)
projects / helm.git / blobdiff