From b5ab291cf2ad1431128dd0b1ab629169a3cdeb50 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 13 Jul 2005 10:09:01 +0000 Subject: [PATCH] New version of the library. --- helm/matita/library/Z/z.ma | 158 +++++++++++++++++------------ helm/matita/library/nat/compare.ma | 68 ++++++++++++- helm/matita/library/nat/minus.ma | 51 +++++----- 3 files changed, 188 insertions(+), 89 deletions(-) diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma index 6ba305d98..f59d7b369 100644 --- a/helm/matita/library/Z/z.ma +++ b/helm/matita/library/Z/z.ma @@ -14,8 +14,9 @@ set "baseuri" "cic:/matita/Z/". -include "nat/nat.ma". -include "datatypes/bool.ma". +include "nat/compare.ma". +include "nat/minus.ma". +include "higher_order_defs/functions.ma". inductive Z : Set \def OZ : Z @@ -34,23 +35,26 @@ definition neg_Z_of_nat \def [ O \Rightarrow OZ | (S n)\Rightarrow neg n]. -definition absZ \def +definition abs \def \lambda z. match z with [ OZ \Rightarrow O | (pos n) \Rightarrow n | (neg n) \Rightarrow n]. -definition OZ_testb \def +definition OZ_test \def \lambda z. match z with [ OZ \Rightarrow true | (pos n) \Rightarrow false | (neg n) \Rightarrow false]. -theorem OZ_discr : -\forall z. if_then_else (OZ_testb z) (eq Z z OZ) (Not (eq Z z OZ)). -intros.elim z.simplify.reflexivity. +theorem OZ_test_to_Prop :\forall z:Z. +match OZ_test z with +[true \Rightarrow eq Z z OZ +|false \Rightarrow Not (eq Z z OZ)]. +intros.elim z. +simplify.reflexivity. simplify.intros. cut match neg e1 with [ OZ \Rightarrow True @@ -83,21 +87,22 @@ definition Zpred \def | (S p) \Rightarrow pos p] | (neg n) \Rightarrow neg (S n)]. -theorem Zpred_succ: \forall z:Z. eq Z (Zpred (Zsucc z)) z. +theorem Zpred_Zsucc: \forall z:Z. eq Z (Zpred (Zsucc z)) z. intros.elim z.reflexivity. elim e1.reflexivity. reflexivity. reflexivity. qed. -theorem Zsucc_pred: \forall z:Z. eq Z (Zsucc (Zpred z)) z. +theorem Zsucc_Zpred: \forall z:Z. eq Z (Zsucc (Zpred z)) z. intros.elim z.reflexivity. reflexivity. elim e2.reflexivity. reflexivity. qed. -let rec Zplus x y : Z \def +definition Zplus :Z \to Z \to Z \def +\lambda x,y. match x with [ OZ \Rightarrow y | (pos m) \Rightarrow @@ -119,32 +124,34 @@ let rec Zplus x y : Z \def | GT \Rightarrow (neg (pred (minus m n)))] | (neg n) \Rightarrow (neg (S (plus m n)))]]. -theorem Zplus_z_O: \forall z:Z. eq Z (Zplus z OZ) z. +theorem Zplus_z_OZ: \forall z:Z. eq Z (Zplus z OZ) z. intro.elim z. simplify.reflexivity. simplify.reflexivity. simplify.reflexivity. qed. +(* theorem symmetric_Zplus: symmetric Z Zplus. *) + theorem sym_Zplus : \forall x,y:Z. eq Z (Zplus x y) (Zplus y x). -intros.elim x.simplify.rewrite > Zplus_z_O.reflexivity. +intros.elim x.rewrite > Zplus_z_OZ.reflexivity. elim y.simplify.reflexivity. simplify. rewrite < sym_plus.reflexivity. simplify. -rewrite > nat_compare_invert. +rewrite > nat_compare_n_m_m_n. simplify.elim nat_compare ? ?.simplify.reflexivity. simplify. reflexivity. simplify. reflexivity. elim y.simplify.reflexivity. -simplify.rewrite > nat_compare_invert. +simplify.rewrite > nat_compare_n_m_m_n. simplify.elim nat_compare ? ?.simplify.reflexivity. simplify. reflexivity. simplify. reflexivity. -simplify.elim (sym_plus ? ?).reflexivity. +simplify.rewrite < sym_plus.reflexivity. qed. -theorem Zpred_neg : \forall z:Z. eq Z (Zpred z) (Zplus (neg O) z). +theorem Zpred_Zplus_neg_O : \forall z:Z. eq Z (Zpred z) (Zplus (neg O) z). intros.elim z. simplify.reflexivity. simplify.reflexivity. @@ -152,7 +159,7 @@ elim e2.simplify.reflexivity. simplify.reflexivity. qed. -theorem Zsucc_pos : \forall z:Z. eq Z (Zsucc z) (Zplus (pos O) z). +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. @@ -160,7 +167,7 @@ simplify.reflexivity. simplify.reflexivity. qed. -theorem Zplus_succ_pred_pp : +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. @@ -173,12 +180,12 @@ simplify. rewrite < plus_n_Sm.reflexivity. qed. -theorem Zplus_succ_pred_pn : +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_succ_pred_np : +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. @@ -189,7 +196,7 @@ simplify.reflexivity. simplify.reflexivity. qed. -theorem Zplus_succ_pred_nn: +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. @@ -200,32 +207,34 @@ simplify.rewrite < plus_n_Sm.reflexivity. simplify.rewrite > plus_n_Sm.reflexivity. qed. -theorem Zplus_succ_pred: +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_pos.rewrite > Zsucc_pred.reflexivity. +rewrite < Zsucc_Zplus_pos_O. +rewrite > Zsucc_Zpred.reflexivity. elim y.rewrite < sym_Zplus.rewrite < sym_Zplus (Zpred OZ). -rewrite < Zpred_neg.rewrite > Zpred_succ. +rewrite < Zpred_Zplus_neg_O. +rewrite > Zpred_Zsucc. simplify.reflexivity. -rewrite < Zplus_succ_pred_nn.reflexivity. -apply Zplus_succ_pred_np. +rewrite < Zplus_neg_neg.reflexivity. +apply Zplus_neg_pos. elim y.simplify.reflexivity. -apply Zplus_succ_pred_pn. -apply Zplus_succ_pred_pp. +apply Zplus_pos_neg. +apply Zplus_pos_pos. qed. -theorem Zsucc_plus_pp : +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. -theorem Zsucc_plus_pn : +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_double_ind +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. @@ -235,14 +244,14 @@ intros. elim n1. simplify. reflexivity. simplify.reflexivity. intros. -rewrite < (Zplus_succ_pred_pn ? m1). +rewrite < (Zplus_pos_neg ? m1). elim H.reflexivity. qed. -theorem Zsucc_plus_nn : +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_double_ind +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. @@ -252,14 +261,14 @@ intros. elim n1. simplify. reflexivity. simplify.reflexivity. intros. -rewrite < (Zplus_succ_pred_nn ? m1). +rewrite < (Zplus_neg_neg ? m1). reflexivity. qed. -theorem Zsucc_plus_np : +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_double_ind +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. @@ -270,53 +279,76 @@ simplify. reflexivity. simplify.reflexivity. intros. rewrite < H. -rewrite < (Zplus_succ_pred_np ? (S m1)). +rewrite < (Zplus_neg_pos ? (S m1)). reflexivity. qed. - -theorem Zsucc_plus : \forall x,y:Z. eq Z (Zplus (Zsucc x) y) (Zsucc (Zplus x y)). +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_pos.reflexivity. +rewrite < Zsucc_Zplus_pos_O.reflexivity. simplify.reflexivity. elim y.rewrite < sym_Zplus.rewrite < sym_Zplus OZ.simplify.reflexivity. -apply Zsucc_plus_nn. -apply Zsucc_plus_np. +apply Zplus_Zsucc_neg_neg. +apply Zplus_Zsucc_neg_pos. elim y. rewrite < sym_Zplus OZ.reflexivity. -apply Zsucc_plus_pn. -apply Zsucc_plus_pp. +apply Zplus_Zsucc_pos_neg. +apply Zplus_Zsucc_pos_pos. qed. -theorem Zpred_plus : \forall x,y:Z. eq Z (Zplus (Zpred x) y) (Zpred (Zplus x y)). +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)). rewrite > Hcut. -rewrite > Zsucc_plus. -rewrite > Zpred_succ. +rewrite > Zplus_Zsucc. +rewrite > Zpred_Zsucc. +reflexivity. +rewrite > Zsucc_Zpred. +reflexivity. +qed. + + +theorem associative_Zplus: associative Z Zplus. +(* change with (\forall x,y,z. eq ?(Zplus (Zplus x y) z) (Zplus x (Zplus y z))).*) +simplify. +intros.elim x.simplify.reflexivity. +elim e1.rewrite < (Zpred_Zplus_neg_O (Zplus y z)). +drop. +rewrite < (Zpred_Zplus_neg_O y). +rewrite < Zplus_Zpred. reflexivity. -rewrite > Zsucc_pred. +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. qed. theorem assoc_Zplus : \forall x,y,z:Z. eq Z (Zplus x (Zplus y z)) (Zplus (Zplus x y) z). intros.elim x.simplify.reflexivity. -elim e1.rewrite < (Zpred_neg (Zplus y z)). -rewrite < (Zpred_neg y). -rewrite < Zpred_plus. +elim e1.rewrite < (Zpred_Zplus_neg_O (Zplus y z)). +rewrite < (Zpred_Zplus_neg_O y). +rewrite < Zplus_Zpred. reflexivity. -rewrite > Zpred_plus (neg e). -rewrite > Zpred_plus (neg e). -rewrite > Zpred_plus (Zplus (neg e) y). -apply f_equal.assumption. -elim e2.rewrite < Zsucc_pos. -rewrite < Zsucc_pos. -rewrite > Zsucc_plus. +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 > Zsucc_plus (pos e1). -rewrite > Zsucc_plus (pos e1). -rewrite > Zsucc_plus (Zplus (pos e1) y). -apply f_equal.assumption. +rewrite > Zplus_Zsucc (pos e1). +rewrite > Zplus_Zsucc (pos e1). +rewrite > Zplus_Zsucc (Zplus (pos e1) y). +apply eq_f.assumption. qed. diff --git a/helm/matita/library/nat/compare.ma b/helm/matita/library/nat/compare.ma index d148dfd31..fec46ae2f 100644 --- a/helm/matita/library/nat/compare.ma +++ b/helm/matita/library/nat/compare.ma @@ -16,6 +16,7 @@ set "baseuri" "cic:/matita/nat/compare". include "nat/orders.ma". include "datatypes/bool.ma". +include "datatypes/compare.ma". let rec leb n m \def match n with @@ -41,7 +42,7 @@ simplify.apply le_S_S.apply H. simplify.intros.apply H.apply le_S_S_to_le.assumption. qed. -theorem le_elim: \forall n,m:nat. \forall P:bool \to Prop. +theorem leb_elim: \forall n,m:nat. \forall P:bool \to Prop. ((le n m) \to (P true)) \to ((Not (le n m)) \to (P false)) \to P (leb n m). intros. @@ -55,5 +56,70 @@ apply (H H2). apply (H1 H2). qed. +let rec nat_compare n m: compare \def +match n with +[ O \Rightarrow + match m with + [ O \Rightarrow EQ + | (S q) \Rightarrow LT ] +| (S p) \Rightarrow + match m with + [ O \Rightarrow GT + | (S q) \Rightarrow nat_compare p q]]. +theorem nat_compare_n_n: \forall n:nat.(eq compare (nat_compare n n) EQ). +intro.elim n. +simplify.reflexivity. +simplify.assumption. +qed. + +theorem nat_compare_S_S: \forall n,m:nat. +eq compare (nat_compare n m) (nat_compare (S n) (S m)). +intros.simplify.reflexivity. +qed. +theorem nat_compare_to_Prop: \forall n,m:nat. +match (nat_compare n m) with + [ LT \Rightarrow (lt n m) + | EQ \Rightarrow (eq nat n m) + | GT \Rightarrow (lt m n) ]. +intros. +apply nat_elim2 (\lambda n,m.match (nat_compare n m) with + [ LT \Rightarrow (lt n m) + | EQ \Rightarrow (eq nat n m) + | GT \Rightarrow (lt 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). +simplify. apply le_S_S.apply H. +simplify. apply le_S_S.apply H. +simplify. apply eq_f. apply H. +qed. + +theorem nat_compare_n_m_m_n: \forall n,m:nat. +eq compare (nat_compare n m) (compare_invert (nat_compare m n)). +intros. +apply nat_elim2 (\lambda n,m.eq compare (nat_compare n m) (compare_invert (nat_compare m n))). +intros.elim n1.simplify.reflexivity. +simplify.reflexivity. +intro.elim n1.simplify.reflexivity. +simplify.reflexivity. +intros.simplify.elim H.reflexivity. +qed. + +theorem nat_compare_elim : \forall n,m:nat. \forall P:compare \to Prop. +((lt n m) \to (P LT)) \to ((eq nat n m) \to (P EQ)) \to ((lt m n) \to (P GT)) \to +(P (nat_compare n m)). +intros. +cut match (nat_compare n m) with +[ LT \Rightarrow (lt n m) +| EQ \Rightarrow (eq nat n m) +| GT \Rightarrow (lt m n)] \to +(P (nat_compare n m)). +apply Hcut.apply nat_compare_to_Prop. +elim (nat_compare n m). +apply (H H3). +apply (H2 H3). +apply (H1 H3). +qed. diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma index 0091cb9b0..b6e7fc5e2 100644 --- a/helm/matita/library/nat/minus.ma +++ b/helm/matita/library/nat/minus.ma @@ -12,10 +12,11 @@ (* *) (**************************************************************************) + set "baseuri" "cic:/matita/nat/minus". include "nat/orders_op.ma". -include "nat/times.ma". +include "nat/compare.ma". let rec minus n m \def match n with @@ -96,7 +97,7 @@ symmetry. apply plus_minus_m_m.assumption. qed. -theorem minus_ge_O: \forall n,m:nat. +theorem eq_minus_n_m_O: \forall n,m:nat. le n m \to eq nat (minus n m) O. intros 2. apply nat_elim2 (\lambda n,m.le n m \to eq nat (minus n m) O). @@ -124,36 +125,36 @@ apply plus_le.assumption. apply le_n_Sm_elim ? ? H1. intros. *) -check distributive. -theorem times_minus_distr: \forall n,m,p:nat. -eq nat (times n (minus m p)) (minus (times n m) (times n p)). +theorem distributive_times_minus: distributive nat times minus. +simplify. intros. -apply (leb_ind p m).intro. -cut eq nat (plus (times n (minus m p)) (times n p)) (plus (minus (times n m) (times n p)) (times n p)). -apply plus_injective_right ? ? (times n p). +apply (leb_elim z y).intro. +cut eq nat (plus (times x (minus y z)) (times x z)) + (plus (minus (times x y) (times x z)) (times x z)). +apply inj_plus_l (times x z). assumption. -apply trans_eq nat ? (times n m). -elim (times_plus_distr ? ? ?). -elim (minus_plus ? ? H).apply refl_equal. -elim (minus_plus ? ? ?).apply refl_equal. -apply times_le_monotony_left. +apply trans_eq nat ? (times x y). +rewrite < times_plus_distr. +rewrite < plus_minus_m_m ? ? H.reflexivity. +rewrite < plus_minus_m_m ? ? ?.reflexivity. +apply le_times_r. assumption. intro. -elim sym_eq ? ? ? (minus_ge_O ? ? ?). -elim sym_eq ? ? ? (minus_ge_O ? ? ?). -elim (sym_times ? ?).simplify.apply refl_equal. -simplify. -apply times_le_monotony_left. -cut (lt m p) \to (le m p). -apply Hcut.simplify.apply not_le_lt ? ? H. -intro.apply lt_le.apply H1. -cut (lt m p) \to (le m p). -apply Hcut.simplify.apply not_le_lt ? ? H. -intro.apply lt_le.apply H1. +rewrite > eq_minus_n_m_O. +rewrite > eq_minus_n_m_O (times x y). +rewrite < sym_times.simplify.reflexivity. +apply lt_to_le. +apply not_le_to_lt.assumption. +apply le_times_r.apply lt_to_le. +apply not_le_to_lt.assumption. qed. -theorem minus_le: \forall n,m:nat. le (minus n m) n. +theorem distr_times_minus: \forall n,m,p:nat. +eq nat (times n (minus m p)) (minus (times n m) (times n p)) +\def distributive_times_minus. + +theorem le_minus_m: \forall n,m:nat. le (minus n m) n. intro.elim n.simplify.apply le_n. elim m.simplify.apply le_n. simplify.apply le_S.apply H. -- 2.39.2