(**************************************************************************)
-(* ___ *)
+(* __ *)
(* ||M|| *)
(* ||A|| A project by Andrea Asperti *)
(* ||T|| *)
set "baseuri" "cic:/matita/Z/times".
-include "Z/z.ma".
+include "nat/lt_arith.ma".
+include "Z/plus.ma".
+include "higher_order_defs/functions.ma".
definition Ztimes :Z \to Z \to Z \def
\lambda x,y.
| (pos n) \Rightarrow (neg (pred (times (S m) (S n))))
| (neg n) \Rightarrow (pos (pred (times (S m) (S n))))]].
-theorem Ztimes_z_OZ: \forall z:Z. eq Z (Ztimes z OZ) OZ.
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "integer times" 'times x y = (cic:/matita/Z/times/Ztimes.con x y).
+
+theorem Ztimes_z_OZ: \forall z:Z. z*OZ = OZ.
intro.elim z.
simplify.reflexivity.
simplify.reflexivity.
simplify.reflexivity.
qed.
-
-(*
+theorem Ztimes_neg_Zopp: \forall n:nat.\forall x:Z.
+eq Z (Ztimes (neg n) x) (Zopp (Ztimes (pos n) x)).
+intros.elim x.
+simplify.reflexivity.
+simplify.reflexivity.
+simplify.reflexivity.
+qed.
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.
-simplify.
-rewrite < plus_n_O.reflexivity.
-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.
+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.
-apply Zplus_pos_neg.
-apply Zplus_pos_pos.
+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.
-theorem Zplus_Zsucc_pos_pos :
-\forall n,m. eq Z (Zplus (Zsucc (pos n)) (pos m)) (Zsucc (Zplus (pos n) (pos m))).
-intros.reflexivity.
-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 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.
+lemma times_minus1: \forall n,p,q:nat. lt q p \to
+eq nat (times (S n) (S (pred (minus (S p) (S q)))))
+ (minus (pred (times (S n) (S p)))
+ (pred (times (S n) (S q)))).
intros.
-rewrite < (Zplus_pos_neg ? m1).
-elim H.reflexivity.
+rewrite < S_pred ? ?.
+rewrite > minus_pred_pred ? ? ? ?.
+rewrite < distr_times_minus.
+reflexivity.
+(* we now close all positivity conditions *)
+apply lt_O_times_S_S.
+apply lt_O_times_S_S.
+simplify.
+apply le_SO_minus. exact H.
qed.
-theorem Zplus_Zsucc_neg_neg :
-\forall n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m))).
+lemma Ztimes_Zplus_pos_neg_pos: \forall n,p,q:nat.
+(pos n)*((neg p)+(pos q)) = (pos n)*(neg p)+ (pos n)*(pos q).
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.
+simplify.
+change in match (plus p (times n (S p))) with (pred (times (S n) (S p))).
+change in match (plus q (times n (S q))) with (pred (times (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.
+intro.
+(* uff *)
+change with (eq Z (pos (pred (times (S n) (S (pred (minus (S q) (S p)))))))
+ (pos (pred (minus (pred (times (S n) (S q)))
+ (pred (times (S n) (S p))))))).
+rewrite < times_minus1 n q p H.reflexivity.
+intro.rewrite < H.simplify.reflexivity.
+intro.
+change with (eq Z (neg (pred (times (S n) (S (pred (minus (S p) (S q)))))))
+ (neg (pred (minus (pred (times (S n) (S p)))
+ (pred (times (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.
+qed.
+
+lemma Ztimes_Zplus_pos_pos_neg: \forall n,p,q:nat.
+(pos n)*((pos p)+(neg q)) = (pos n)*(pos p)+ (pos n)*(neg q).
intros.
-rewrite < (Zplus_neg_neg ? m1).
-reflexivity.
+rewrite < sym_Zplus.
+rewrite > Ztimes_Zplus_pos_neg_pos.
+apply sym_Zplus.
qed.
-theorem Zplus_Zsucc_neg_pos:
-\forall n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m))).
+lemma distributive2_Ztimes_pos_Zplus:
+distributive2 nat Z (\lambda n,z. Ztimes (pos n) z) Zplus.
+change with \forall n,y,z.
+eq Z (Ztimes (pos n) (Zplus y z)) (Zplus (Ztimes (pos n) y) (Ztimes (pos n) z)).
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)).
+elim y.reflexivity.
+elim z.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 < distr_times_plus.reflexivity.
+apply Ztimes_Zplus_pos_neg_pos.
+elim z.reflexivity.
+apply Ztimes_Zplus_pos_pos_neg.
+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 < distr_times_plus.
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.
+variant distr_Ztimes_Zplus_pos: \forall n,y,z.
+eq Z (Ztimes (pos n) (Zplus y z)) (Zplus (Ztimes (pos n) y) (Ztimes (pos n) z)) \def
+distributive2_Ztimes_pos_Zplus.
-theorem Zplus_Zpred: \forall x,y:Z. eq Z (Zplus (Zpred x) y) (Zpred (Zplus x y)).
+lemma distributive2_Ztimes_neg_Zplus :
+distributive2 nat Z (\lambda n,z. Ztimes (neg n) z) Zplus.
+change with \forall n,y,z.
+eq Z (Ztimes (neg n) (Zplus y z)) (Zplus (Ztimes (neg n) y) (Ztimes (neg n) z)).
intros.
-cut eq Z (Zpred (Zplus x y)) (Zpred (Zplus (Zsucc (Zpred x)) y)).
-rewrite > Hcut.
-rewrite > Zplus_Zsucc.
-rewrite > Zpred_Zsucc.
-reflexivity.
-rewrite > Zsucc_Zpred.
+rewrite > Ztimes_neg_Zopp.
+rewrite > distr_Ztimes_Zplus_pos.
+rewrite > Zopp_Zplus.
+rewrite < Ztimes_neg_Zopp. rewrite < Ztimes_neg_Zopp.
reflexivity.
qed.
+variant distr_Ztimes_Zplus_neg: \forall n,y,z.
+eq Z (Ztimes (neg n) (Zplus y z)) (Zplus (Ztimes (neg n) y) (Ztimes (neg n) z)) \def
+distributive2_Ztimes_neg_Zplus.
-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.
-reflexivity.
-rewrite > Zplus_Zsucc (pos e1).
-rewrite > Zplus_Zsucc (pos e1).
-rewrite > Zplus_Zsucc (Zplus (pos e1) y).
-apply eq_f.assumption.
+theorem distributive_Ztimes_Zplus: 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.
+(* case x = OZ *)
+simplify.reflexivity.
+(* case x = neg n *)
+apply distr_Ztimes_Zplus_neg.
+(* case x = pos n *)
+apply distr_Ztimes_Zplus_pos.
qed.
-variant assoc_Zplus : \forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z))
-\def associative_Zplus.
-
-definition Zopp : Z \to Z \def
-\lambda x:Z. match x with
-[ OZ \Rightarrow OZ
-| (pos n) \Rightarrow (neg n)
-| (neg n) \Rightarrow (pos n) ].
-
-theorem Zplus_Zopp: \forall x:Z. (eq Z (Zplus x (Zopp x)) OZ).
-intro.elim x.
-apply refl_eq.
-simplify.
-rewrite > nat_compare_n_n.
-simplify.apply refl_eq.
-simplify.
-rewrite > nat_compare_n_n.
-simplify.apply refl_eq.
-qed.
-*)
+variant distr_Ztimes_Zplus: \forall x,y,z.
+eq Z (Ztimes x (Zplus y z)) (Zplus (Ztimes x y) (Ztimes x z)) \def
+distributive_Ztimes_Zplus.
\ No newline at end of file
projects / helm.git / blobdiff