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.
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.
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<n
-| EQ \Rightarrow n1=n
-| GT \Rightarrow n<n1] \to
-match (nat_compare n1 n) with
-[ LT \Rightarrow (le (S n1) n)
-| EQ \Rightarrow neg n = neg n1
-| GT \Rightarrow (le (S n) n1)].
-apply Hcut. apply nat_compare_to_Prop.
-elim (nat_compare n1 n).
-simplify.exact H.
-simplify.exact H.
-simplify.apply eq_f.apply sym_eq.exact H.
-simplify.exact I.
-elim y.simplify.exact I.
-simplify.exact I.
-simplify.
-(*CSC: qui uso le perche' altrimenti ci sono troppe scelte
- per via delle coercions! *)
-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 (le (S n) n1)
-| EQ \Rightarrow pos n = pos n1
-| GT \Rightarrow (le (S n1) n)].
-apply Hcut. apply nat_compare_to_Prop.
-elim (nat_compare n n1).
-simplify.exact H.
-simplify.exact H.
-simplify.apply eq_f.exact H.
-qed.
-
theorem Zlt_to_Zle: \forall x,y:Z. x < y \to Zsucc x \leq y.
intros 2.elim x.
cut OZ < y \to Zsucc OZ \leq y.
set "baseuri" "cic:/matita/Z/times".
include "nat/lt_arith.ma".
-include "Z/z.ma".
+include "Z/plus.ma".
+include "higher_order_defs/functions.ma".
definition Ztimes :Z \to Z \to Z \def
\lambda x,y.
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.
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
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
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
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.
-
(* *)
(**************************************************************************)
-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).
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).
(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/compare/".
+set "baseuri" "cic:/matita/datatypes/compare/".
inductive compare :Set \def
| LT : compare
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).
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).
(**************************************************************************)
-(* ___ *)
+(* ___ *)
(* ||M|| *)
(* ||A|| A project by Andrea Asperti *)
(* ||T|| *)
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
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.
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.
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.
apply lt_to_not_eq.assumption.
intro.reflexivity.
qed.
+
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.
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.
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.
include "logic/equality.ma".
include "logic/connectives.ma".
+include "datatypes/bool.ma".
include "higher_order_defs/functions.ma".
inductive nat : Set \def
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.
+
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<m \to \lnot (n=m).
simplify.intros.cut (le (S n) m) \to False.
theorem decidable_lt: \forall n,m:nat. decidable (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.
+apply H.
+intros.apply False_ind.apply not_le_Sn_O p H2.
+apply H.intros.apply H1.
+cut p < S n1.
+apply lt_S_to_le.assumption.
+apply lt_to_le_to_lt p q (S n1) H3 H2.
+qed.
+
rewrite > 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.
projects / helm.git / commitdiff