From: Andrea Asperti Date: Mon, 22 Aug 2005 08:05:32 +0000 (+0000) Subject: The library grows... X-Git-Tag: working_equations_only~26 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=03fcee16d9c262aad38a47d0a409b684a965cc3f;p=helm.git The library grows... --- diff --git a/helm/matita/library/Z/orders.ma b/helm/matita/library/Z/orders.ma index 756d02271..bc5ffdb51 100644 --- a/helm/matita/library/Z/orders.ma +++ b/helm/matita/library/Z/orders.ma @@ -15,6 +15,7 @@ set "baseuri" "cic:/matita/Z/orders". include "Z/z.ma". +include "nat/orders.ma". definition Zle : Z \to Z \to Prop \def \lambda x,y:Z. @@ -72,25 +73,6 @@ qed. theorem irrefl_Zlt: irreflexive Z Zlt \def irreflexive_Zlt. -definition Z_compare : Z \to Z \to compare \def -\lambda x,y:Z. - match x with - [ OZ \Rightarrow - match y with - [ OZ \Rightarrow EQ - | (pos m) \Rightarrow LT - | (neg m) \Rightarrow GT ] - | (pos n) \Rightarrow - match y with - [ OZ \Rightarrow GT - | (pos m) \Rightarrow (nat_compare n m) - | (neg m) \Rightarrow GT] - | (neg n) \Rightarrow - match y with - [ OZ \Rightarrow LT - | (pos m) \Rightarrow LT - | (neg m) \Rightarrow nat_compare m n ]]. - (*CSC: qui uso lt perche' ho due istanze diverse di < *) theorem Zlt_neg_neg_to_lt: \forall n,m:nat. neg n < neg m \to lt m n. @@ -115,54 +97,6 @@ intros. simplify.apply H. qed. -theorem Z_compare_to_Prop : -\forall x,y:Z. match (Z_compare x y) with -[ LT \Rightarrow x < y -| EQ \Rightarrow x=y -| GT \Rightarrow y < x]. -intros. -elim x. elim y. -simplify.apply refl_eq. -simplify.exact I. -simplify.exact I. -elim y. simplify.exact I. -simplify. -(*CSC: qui uso le perche' altrimenti ci sono troppe scelte - per via delle coercions! *) -cut match (nat_compare n1 n) with -[ LT \Rightarrow n1 Ztimes_z_OZ.reflexivity. @@ -120,108 +128,110 @@ 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. -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))))))). +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 < S_pred ? ?. rewrite > minus_pred_pred ? ? ? ?. rewrite < distr_times_minus. -reflexivity. -(* we start closing stupid positivity conditions *) +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. -(* 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. -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 > Hcut. +qed. + +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. +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 n1 n2. +apply nat_compare_elim p q. 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. +(* 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 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. +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. -(* adesso chiudo il cut stupido *) -intros.reflexivity. +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 < sym_Zplus. +rewrite > Ztimes_Zplus_pos_neg_pos. +apply sym_Zplus. +qed. + +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. +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 < times_plus_distr. +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. + +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. + +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. +rewrite > Ztimes_neg_Zopp. +rewrite > distr_Ztimes_Zplus_pos. +rewrite > Zopp_Zplus. +rewrite < Ztimes_neg_Zopp. rewrite < Ztimes_neg_Zopp. reflexivity. -(* and now the case x = pos n *) +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 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 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 diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma index cdc0e44d7..a5e0fba8f 100644 --- a/helm/matita/library/Z/z.ma +++ b/helm/matita/library/Z/z.ma @@ -14,8 +14,7 @@ set "baseuri" "cic:/matita/Z/z". -include "nat/compare.ma". -include "nat/minus.ma". +include "nat/nat.ma". include "higher_order_defs/functions.ma". inductive Z : Set \def @@ -69,6 +68,82 @@ cut match pos n with apply Hcut. rewrite > H.simplify.exact I. qed. +(* discrimination *) +theorem injective_pos: injective nat Z pos. +simplify. +intros. +change with abs (pos x) = abs (pos y). +apply eq_f.assumption. +qed. + +variant inj_pos : \forall n,m:nat. pos n = pos m \to n = m +\def injective_pos. + +theorem injective_neg: injective nat Z neg. +simplify. +intros. +change with abs (neg x) = abs (neg y). +apply eq_f.assumption. +qed. + +variant inj_neg : \forall n,m:nat. neg n = neg m \to n = m +\def injective_neg. + +theorem not_eq_OZ_pos: \forall n:nat. \lnot (OZ = (pos n)). +simplify.intros. +change with + match pos n with + [ OZ \Rightarrow True + | (pos n) \Rightarrow False + | (neg n) \Rightarrow False]. +rewrite < H. +simplify.exact I. +qed. + +theorem not_eq_OZ_neg :\forall n:nat. \lnot (OZ = (neg n)). +simplify.intros. +change with + match neg n with + [ OZ \Rightarrow True + | (pos n) \Rightarrow False + | (neg n) \Rightarrow False]. +rewrite < H. +simplify.exact I. +qed. + +theorem not_eq_pos_neg :\forall n,m:nat. \lnot ((pos n) = (neg m)). +simplify.intros. +change with + match neg m with + [ OZ \Rightarrow False + | (pos n) \Rightarrow True + | (neg n) \Rightarrow False]. +rewrite < H. +simplify.exact I. +qed. + +theorem decidable_eq_Z : \forall x,y:Z. decidable (x=y). +intros.simplify. +elim x.elim y. +left.reflexivity. +right.apply not_eq_OZ_neg. +right.apply not_eq_OZ_pos. +elim y.right.intro. +apply not_eq_OZ_neg n ?.apply sym_eq.assumption. +elim (decidable_eq_nat n n1:(Or (n=n1) ((n=n1) \to False))). +left.apply eq_f.assumption. +right.intro.apply H.apply injective_neg.assumption. +right.intro.apply not_eq_pos_neg n1 n ?.apply sym_eq.assumption. +elim y.right.intro. +apply not_eq_OZ_pos n ?.apply sym_eq.assumption. +right.apply not_eq_pos_neg. +elim (decidable_eq_nat n n1:(Or (n=n1) ((n=n1) \to False))). +left.apply eq_f.assumption. +right.intro.apply H.apply injective_pos.assumption. +qed. + +(* end discrimination *) + definition Zsucc \def \lambda z. match z with [ OZ \Rightarrow pos O @@ -101,260 +176,3 @@ elim n.reflexivity. reflexivity. qed. -definition Zplus :Z \to Z \to Z \def -\lambda x,y. - match x with - [ OZ \Rightarrow y - | (pos m) \Rightarrow - match y with - [ OZ \Rightarrow x - | (pos n) \Rightarrow (pos (pred ((S m)+(S n)))) - | (neg n) \Rightarrow - match nat_compare m n with - [ LT \Rightarrow (neg (pred (n-m))) - | EQ \Rightarrow OZ - | GT \Rightarrow (pos (pred (m-n)))]] - | (neg m) \Rightarrow - match y with - [ OZ \Rightarrow x - | (pos n) \Rightarrow - match nat_compare m n with - [ LT \Rightarrow (pos (pred (n-m))) - | EQ \Rightarrow OZ - | GT \Rightarrow (neg (pred (m-n)))] - | (neg n) \Rightarrow (neg (pred ((S m)+(S n))))]]. - -(*CSC: the URI must disappear: there is a bug now *) -interpretation "integer plus" 'plus x y = (cic:/matita/Z/z/Zplus.con x y). - -theorem Zplus_z_OZ: \forall z:Z. 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. x+y = y+x. -intros.elim x.rewrite > Zplus_z_OZ.reflexivity. -elim y.simplify.reflexivity. -simplify. -rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity. -simplify. -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_n_m_m_n. -simplify.elim nat_compare ? ?.simplify.reflexivity. -simplify. reflexivity. -simplify. reflexivity. -simplify.rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity. -qed. - -theorem Zpred_Zplus_neg_O : \forall z:Z. Zpred z = (neg O)+z. -intros.elim z. -simplify.reflexivity. -simplify.reflexivity. -elim n.simplify.reflexivity. -simplify.reflexivity. -qed. - -theorem Zsucc_Zplus_pos_O : \forall z:Z. Zsucc z = (pos O)+z. -intros.elim z. -simplify.reflexivity. -elim n.simplify.reflexivity. -simplify.reflexivity. -simplify.reflexivity. -qed. - -theorem Zplus_pos_pos: -\forall n,m. (pos n)+(pos m) = (Zsucc (pos n))+(Zpred (pos m)). -intros. -elim n.elim m. -simplify.reflexivity. -simplify.reflexivity. -elim m. -simplify.rewrite < plus_n_Sm. -rewrite < plus_n_O.reflexivity. -simplify.rewrite < plus_n_Sm. -rewrite < plus_n_Sm.reflexivity. -qed. - -theorem Zplus_pos_neg: -\forall n,m. (pos n)+(neg m) = (Zsucc (pos n))+(Zpred (neg m)). -intros.reflexivity. -qed. - -theorem Zplus_neg_pos : -\forall n,m. (neg n)+(pos m) = (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. (neg n)+(neg m) = (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. x+y = (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. (Zsucc (pos n))+(pos m) = Zsucc ((pos n)+(pos m)). -intros.reflexivity. -qed. - -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. -intros.elim n1. -simplify. reflexivity. -elim n2.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. (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. -intros.elim n1. -simplify. reflexivity. -elim n2.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. 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))). -intros.elim n1. -simplify. reflexivity. -elim n2.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. (Zsucc x)+y = Zsucc (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. (Zpred x)+y = Zpred (x+y). -intros. -cut Zpred (x+y) = Zpred ((Zsucc (Zpred x))+y). -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. (x + y) + z = x + (y + z). -(* simplify. *) -intros.elim x.simplify.reflexivity. -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. -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. -qed. - -variant assoc_Zplus : \forall x,y,z:Z. (x+y)+z = x+(y+z) -\def associative_Zplus. - -(* Zopp *) -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) ]. - -(*CSC: the URI must disappear: there is a bug now *) -interpretation "integer unary minus" 'uminus x = (cic:/matita/Z/z/Zopp.con x). - -theorem Zplus_Zopp: \forall x:Z. x+ -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. - diff --git a/helm/matita/library/datatypes/bool.ma b/helm/matita/library/datatypes/bool.ma index cac5ebbe9..d99456dc8 100644 --- a/helm/matita/library/datatypes/bool.ma +++ b/helm/matita/library/datatypes/bool.ma @@ -12,17 +12,35 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/bool/". +set "baseuri" "cic:/matita/datatypes/bool/". + +include "logic/equality.ma". inductive bool : Set \def | true : bool | false : bool. + +theorem not_eq_true_false : \lnot true = false. +simplify.intro. +change with +match true with +[ true \Rightarrow False +| flase \Rightarrow True]. +rewrite > H.simplify.exact I. +qed. definition notb : bool \to bool \def \lambda b:bool. match b with [ true \Rightarrow false | false \Rightarrow true ]. + +theorem notb_elim: \forall b:bool.\forall P:bool \to Prop. +match b with +[ true \Rightarrow P false +| false \Rightarrow P true] \to P (notb b). +intros 2.elim b.exact H. exact H. +qed. (*CSC: the URI must disappear: there is a bug now *) interpretation "boolean not" 'not x = (cic:/matita/datatypes/bool/notb.con x). @@ -30,19 +48,31 @@ interpretation "boolean not" 'not x = (cic:/matita/datatypes/bool/notb.con x). definition andb : bool \to bool \to bool\def \lambda b1,b2:bool. match b1 with - [ true \Rightarrow - match b2 with [true \Rightarrow true | false \Rightarrow false] + [ true \Rightarrow b2 | false \Rightarrow false ]. +theorem andb_elim: \forall b1,b2:bool. \forall P:bool \to Prop. +match b1 with +[ true \Rightarrow P b2 +| false \Rightarrow P false] \to P (andb b1 b2). +intros 3.elim b1.exact H. exact H. +qed. + (*CSC: the URI must disappear: there is a bug now *) interpretation "boolean and" 'and x y = (cic:/matita/datatypes/bool/andb.con x y). definition orb : bool \to bool \to bool\def \lambda b1,b2:bool. match b1 with - [ true \Rightarrow - match b2 with [true \Rightarrow true | false \Rightarrow false] - | false \Rightarrow false ]. + [ true \Rightarrow true + | false \Rightarrow b2]. + +theorem orb_elim: \forall b1,b2:bool. \forall P:bool \to Prop. +match b1 with +[ true \Rightarrow P true +| false \Rightarrow P b2] \to P (orb b1 b2). +intros 3.elim b1.exact H. exact H. +qed. (*CSC: the URI must disappear: there is a bug now *) interpretation "boolean or" 'or x y = (cic:/matita/datatypes/bool/orb.con x y). diff --git a/helm/matita/library/datatypes/compare.ma b/helm/matita/library/datatypes/compare.ma index 3e0271d59..c4fd119a5 100644 --- a/helm/matita/library/datatypes/compare.ma +++ b/helm/matita/library/datatypes/compare.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/compare/". +set "baseuri" "cic:/matita/datatypes/compare/". inductive compare :Set \def | LT : compare diff --git a/helm/matita/library/higher_order_defs/functions.ma b/helm/matita/library/higher_order_defs/functions.ma index e8fbb6dd9..71b6d8459 100644 --- a/helm/matita/library/higher_order_defs/functions.ma +++ b/helm/matita/library/higher_order_defs/functions.ma @@ -29,6 +29,9 @@ definition surjective: \forall A,B:Type.\forall f:A \to B.Prop definition symmetric: \forall A:Type.\forall f:A \to A\to A.Prop \def \lambda A.\lambda f.\forall x,y.f x y = f y x. +definition symmetric2: \forall A,B:Type.\forall f:A \to A\to B.Prop +\def \lambda A,B.\lambda f.\forall x,y.f x y = f y x. + definition associative: \forall A:Type.\forall f:A \to A\to A.Prop \def \lambda A.\lambda f.\forall x,y,z.f (f x y) z = f x (f y z). @@ -41,4 +44,6 @@ definition monotonic : \forall A:Type.\forall R:A \to A \to Prop. definition distributive: \forall A:Type.\forall f,g:A \to A \to A.Prop \def \lambda A.\lambda f,g.\forall x,y,z:A. f x (g y z) = g (f x y) (f x z). - +definition distributive2: \forall A,B:Type.\forall f:A \to B \to B. +\forall g: B\to B\to B. Prop +\def \lambda A,B.\lambda f,g.\forall x:A.\forall y,z:B. f x (g y z) = g (f x y) (f x z). diff --git a/helm/matita/library/nat/compare.ma b/helm/matita/library/nat/compare.ma index 3a8e4a87c..194b38d84 100644 --- a/helm/matita/library/nat/compare.ma +++ b/helm/matita/library/nat/compare.ma @@ -1,5 +1,5 @@ (**************************************************************************) -(* ___ *) +(* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) @@ -18,6 +18,52 @@ include "nat/orders.ma". include "datatypes/bool.ma". include "datatypes/compare.ma". +let rec eqb n m \def +match n with + [ O \Rightarrow + match m with + [ O \Rightarrow true + | (S q) \Rightarrow false] + | (S p) \Rightarrow + match m with + [ O \Rightarrow false + | (S q) \Rightarrow eqb p q]]. + +theorem eqb_to_Prop: \forall n,m:nat. +match (eqb n m) with +[ true \Rightarrow n = m +| false \Rightarrow \lnot (n = m)]. +intros. +apply nat_elim2 +(\lambda n,m:nat.match (eqb n m) with +[ true \Rightarrow n = m +| false \Rightarrow \lnot (n = 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. +intros.simplify. +generalize in match H. +elim (eqb n1 m1). +simplify.apply eq_f.apply H1. +simplify.intro.apply H1.apply inj_S.assumption. +qed. + +theorem eqb_elim : \forall n,m:nat.\forall P:bool \to Prop. +(n=m \to (P true)) \to (\lnot n=m \to (P false)) \to (P (eqb n m)). +intros. +cut +match (eqb n m) with +[ true \Rightarrow n = m +| false \Rightarrow \lnot (n = m)] \to (P (eqb n m)). +apply Hcut.apply eqb_to_Prop. +elim eqb n m. +apply (H H2). +apply (H1 H2). +qed. + let rec leb n m \def match n with [ O \Rightarrow true diff --git a/helm/matita/library/nat/div_and_mod.ma b/helm/matita/library/nat/div_and_mod.ma index 619ba6815..8c1e0e953 100644 --- a/helm/matita/library/nat/div_and_mod.ma +++ b/helm/matita/library/nat/div_and_mod.ma @@ -175,12 +175,23 @@ apply lt_to_le. apply H6. qed. +theorem div_mod_spec_to_eq2 :\forall a,b,q,r,q1,r1. +(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). +rewrite < H3. +rewrite > div_mod_spec_to_eq a b q r q1 r1 H H1. +assumption. +qed. + theorem div_mod_spec_times : \forall n,m:nat.div_mod_spec ((S n)*m) (S n) m O. intros.constructor 1. simplify.apply le_S_S.apply le_O_n. rewrite < plus_n_O.rewrite < sym_times.reflexivity. qed. +(* some properties of div and mod *) theorem div_times: \forall n,m:nat. div ((S n)*m) (S n) = m. intros. apply div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O. @@ -189,6 +200,34 @@ simplify.apply le_S_S.apply le_O_n. apply div_mod_spec_times. qed. +theorem div_n_n: \forall n:nat. O < n \to div n n = S O. +intros. +apply div_mod_spec_to_eq n n (div n n) (mod n n) (S O) O. +apply div_mod_spec_div_mod.assumption. +constructor 1.assumption. +rewrite < plus_n_O.simplify.rewrite < plus_n_O.reflexivity. +qed. + +theorem mod_n_n: \forall n:nat. O < n \to mod n n = O. +intros. +apply div_mod_spec_to_eq2 n n (div n n) (mod n n) (S O) O. +apply div_mod_spec_div_mod.assumption. +constructor 1.assumption. +rewrite < plus_n_O.simplify.rewrite < plus_n_O.reflexivity. +qed. + +theorem mod_S: \forall n,m:nat. O < m \to S (mod n m) < m \to +(mod (S n) m) = S (mod n m). +intros. +apply div_mod_spec_to_eq2 (S n) m (div (S n) m) (mod (S n) m) (div n m) (S (mod n m)). +apply div_mod_spec_div_mod.assumption. +constructor 1.assumption.rewrite < plus_n_Sm. +apply eq_f. +apply div_mod. +assumption. +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. intros. diff --git a/helm/matita/library/nat/exp.ma b/helm/matita/library/nat/exp.ma index c0d363773..6fcd9da0e 100644 --- a/helm/matita/library/nat/exp.ma +++ b/helm/matita/library/nat/exp.ma @@ -37,7 +37,7 @@ theorem exp_n_SO : \forall n:nat. eq nat n (exp n (S O)). intro.simplify.rewrite < times_n_SO.reflexivity. qed. -theorem bad : \forall n,p,q:nat. +theorem exp_exp_times : \forall n,p,q:nat. eq nat (exp (exp n p) q) (exp n (times p q)). intros. elim q.simplify.rewrite < times_n_O.simplify.reflexivity. diff --git a/helm/matita/library/nat/lt_arith.ma b/helm/matita/library/nat/lt_arith.ma index 5bef22371..9494a28d7 100644 --- a/helm/matita/library/nat/lt_arith.ma +++ b/helm/matita/library/nat/lt_arith.ma @@ -160,3 +160,4 @@ apply inj_times_r n.assumption. apply lt_to_not_eq.assumption. intro.reflexivity. qed. + diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma index 1b7900314..7945a76e0 100644 --- a/helm/matita/library/nat/minus.ma +++ b/helm/matita/library/nat/minus.ma @@ -131,15 +131,80 @@ apply le_S.assumption. apply lt_to_le.assumption. qed. -(* -theorem le_plus_minus: \forall n,m,p. n+m \leq p \to n \leq p-m. -intros 3. -elim p.simplify.apply trans_le ? (n+m) ?. -elim sym_plus ? ?. -apply plus_le.assumption. -apply le_n_Sm_elim ? ? H1. +theorem minus_le_S_minus_S: \forall n,m:nat. m-n \leq S (m-(S n)). +intros.apply nat_elim2 (\lambda n,m.m-n \leq S (m-(S n))). +intro.elim n1.simplify.apply le_n_Sn. +simplify.rewrite < minus_n_O.apply le_n. +intros.simplify.apply le_n_Sn. +intros.simplify.apply H. +qed. + +theorem lt_minus_S_n_to_le_minus_n : \forall n,m,p:nat. m-(S n) < p \to m-n \leq p. +intros 3.simplify.intro. +apply trans_le (m-n) (S (m-(S n))) p. +apply minus_le_S_minus_S. +assumption. +qed. + +theorem le_minus_m: \forall n,m:nat. n-m \leq n. +intros.apply nat_elim2 (\lambda m,n. n-m \leq n). +intros.rewrite < minus_n_O.apply le_n. +intros.simplify.apply le_n. +intros.simplify.apply le_S.assumption. +qed. + +theorem minus_le_O_to_le: \forall n,m:nat. n-m \leq O \to n \leq m. +intros 2. +apply nat_elim2 (\lambda n,m:nat.n-m \leq O \to n \leq m). +intros.apply le_O_n. +simplify.intros. assumption. +simplify.intros.apply le_S_S.apply H.assumption. +qed. + +(* 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. +intros.rewrite < minus_n_O. +apply le_minus_m. +intros.elim a.simplify.apply le_n. +simplify.apply H.apply le_S_S_to_le.assumption. +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.apply le_O_n. +simplify.intros.rewrite < plus_n_O.assumption. intros. -*) +rewrite < plus_n_Sm. +apply le_S_S.apply H. +exact H1. +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.simplify.apply le_O_n. +intros 2.rewrite < plus_n_O.intro.simplify.assumption. +intros.simplify.apply H. +apply le_S_S_to_le.rewrite > plus_n_Sm.assumption. +qed. + +(* 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))). +intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption. +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)). +rewrite < sym_plus. +apply le_plus_n.assumption. +intros.simplify. +apply H.apply le_S_S_to_le. +rewrite > plus_n_Sm.assumption. +qed. + theorem distributive_times_minus: distributive nat times minus. simplify. @@ -149,7 +214,7 @@ 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 < times_plus_distr. +rewrite < distr_times_plus. rewrite < plus_minus_m_m ? ? H.reflexivity. rewrite < plus_minus_m_m ? ? ?.reflexivity. apply le_times_r. @@ -167,8 +232,3 @@ qed. theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p \def distributive_times_minus. -theorem le_minus_m: \forall n,m:nat. n-m \leq n. -intro.elim n.simplify.apply le_n. -elim m.simplify.apply le_n. -simplify.apply le_S.apply H. -qed. diff --git a/helm/matita/library/nat/nat.ma b/helm/matita/library/nat/nat.ma index 194cf1273..df045daa7 100644 --- a/helm/matita/library/nat/nat.ma +++ b/helm/matita/library/nat/nat.ma @@ -16,6 +16,7 @@ set "baseuri" "cic:/matita/nat/nat". include "logic/equality.ma". include "logic/connectives.ma". +include "datatypes/bool.ma". include "higher_order_defs/functions.ma". inductive nat : Set \def @@ -84,3 +85,17 @@ 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))). +intro.elim n1. +left.reflexivity. +right.apply not_eq_O_S. +intro.right.intro. +apply not_eq_O_S n1 ?. +apply sym_eq.assumption. +intros.elim H. +left.apply eq_f. assumption. +right.intro.apply H1.apply inj_S.assumption. +qed. + diff --git a/helm/matita/library/nat/orders.ma b/helm/matita/library/nat/orders.ma index 4ec4dfc5b..122aebcfa 100644 --- a/helm/matita/library/nat/orders.ma +++ b/helm/matita/library/nat/orders.ma @@ -104,6 +104,14 @@ apply H.assumption. apply le_S_S_to_le.assumption. qed. +(* le to lt or eq *) +theorem le_to_or_lt_eq : \forall n,m:nat. +n \leq m \to n < m \lor n = m. +intros.elim H. +right.reflexivity. +left.simplify.apply le_S_S.assumption. +qed. + (* not eq *) theorem lt_to_not_eq : \forall n,m:nat. n assoc_plus.reflexivity. qed. -variant times_plus_distr: \forall n,m,p:nat. n*(m+p) = n*m + n*p +variant distr_times_plus: \forall n,m,p:nat. n*(m+p) = n*m + n*p \def distributive_times_plus. theorem associative_times: associative nat times. simplify.intros. elim x.simplify.apply refl_eq. simplify.rewrite < sym_times. -rewrite > times_plus_distr. +rewrite > distr_times_plus. rewrite < sym_times. rewrite < sym_times (times n y) z. rewrite < H.apply refl_eq.