From 5158d99efec8b0ace3dfb694faa9112c664d4813 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 23 Jun 2005 15:29:02 +0000 Subject: [PATCH] Added Z, Zplus and its properties. --- helm/matita/tests/match.ma | 347 +++++++++++++++++++++++++++++++++++-- 1 file changed, 335 insertions(+), 12 deletions(-) diff --git a/helm/matita/tests/match.ma b/helm/matita/tests/match.ma index bc8caa223..036cc393b 100644 --- a/helm/matita/tests/match.ma +++ b/helm/matita/tests/match.ma @@ -295,15 +295,338 @@ simplify.apply le_n_S.apply H. simplify.intros.apply H.apply le_S_n.assumption. qed. -(*CSC: this requires too much time -theorem prova : -let three \def (S (S (S O))) in -let nine \def (times three three) in -let eightyone \def (times nine nine) in -let square \def (times eightyone eightyone) in -(eq nat square O). -intro. -intro. -intro.intro. -normalize goal at (? ? % ?). -*) \ No newline at end of file +inductive Z : Set \def + OZ : Z +| pos : nat \to Z +| neg : nat \to Z. + +definition Z_of_nat \def +\lambda n. match n with +[ O \Rightarrow OZ +| (S n)\Rightarrow pos n]. + +coercion Z_of_nat. + +definition neg_Z_of_nat \def +\lambda n. match n with +[ O \Rightarrow OZ +| (S n)\Rightarrow neg n]. + +definition absZ \def +\lambda z. + match z with +[ OZ \Rightarrow O +| (pos n) \Rightarrow n +| (neg n) \Rightarrow n]. + +definition OZ_testb \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.apply refl_equal. +simplify.intros. +cut match neg e with +[ OZ \Rightarrow True +| (pos n) \Rightarrow False +| (neg n) \Rightarrow False]. +apply Hcut. elim (sym_eq ? ? ? H).simplify.exact I. +simplify.intros. +cut match pos e with +[ OZ \Rightarrow True +| (pos n) \Rightarrow False +| (neg n) \Rightarrow False]. +apply Hcut. elim (sym_eq ? ? ? H).simplify.exact I. +qed. + +definition Zsucc \def +\lambda z. match z with +[ OZ \Rightarrow pos O +| (pos n) \Rightarrow pos (S n) +| (neg n) \Rightarrow + match n with + [ O \Rightarrow OZ + | (S p) \Rightarrow neg p]]. + +definition Zpred \def +\lambda z. match z with +[ OZ \Rightarrow neg O +| (pos n) \Rightarrow + match n with + [ O \Rightarrow OZ + | (S p) \Rightarrow pos p] +| (neg n) \Rightarrow neg (S n)]. + +theorem Zpred_succ: \forall z:Z. eq Z (Zpred (Zsucc z)) z. +intros.elim z.apply refl_equal. +elim e.apply refl_equal. +apply refl_equal. +apply refl_equal. +qed. + +theorem Zsucc_pred: \forall z:Z. eq Z (Zsucc (Zpred z)) z. +intros.elim z.apply refl_equal. +apply refl_equal. +elim e.apply refl_equal. +apply refl_equal. +qed. + +inductive compare :Set \def +| LT : compare +| EQ : compare +| GT : compare. + +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]]. + +definition compare_invert: compare \to compare \def + \lambda c. + match c with + [ LT \Rightarrow GT + | EQ \Rightarrow EQ + | GT \Rightarrow LT ]. + +theorem nat_compare_invert: \forall n,m:nat. +eq compare (nat_compare n m) (compare_invert (nat_compare m n)). +intros. +apply nat_double_ind (\lambda n,m.eq compare (nat_compare n m) (compare_invert (nat_compare m n))). +intros.elim n1.simplify.apply refl_equal. +simplify.apply refl_equal. +intro.elim n1.simplify.apply refl_equal. +simplify.apply refl_equal. +intros.simplify.elim H.apply refl_equal. +qed. + +let rec Zplus x y : Z \def + match x with + [ OZ \Rightarrow y + | (pos m) \Rightarrow + match y with + [ OZ \Rightarrow x + | (pos n) \Rightarrow (pos (S (plus m n))) + | (neg n) \Rightarrow + match nat_compare m n with + [ LT \Rightarrow (neg (pred (minus n m))) + | EQ \Rightarrow OZ + | GT \Rightarrow (pos (pred (minus m n)))]] + | (neg m) \Rightarrow + match y with + [ OZ \Rightarrow x + | (pos n) \Rightarrow + match nat_compare m n with + [ LT \Rightarrow (pos (pred (minus n m))) + | EQ \Rightarrow OZ + | 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. +intro.elim z. +simplify.apply refl_equal. +simplify.apply refl_equal. +simplify.apply refl_equal. +qed. + +theorem sym_Zplus : \forall x,y:Z. eq Z (Zplus x y) (Zplus y x). +intros.elim x.simplify.elim (sym_eq ? ? ? (Zplus_z_O y)).apply refl_equal. +elim y.simplify.reflexivity. +simplify.elim (sym_plus e e1).apply refl_equal. +simplify.elim (sym_eq ? ? ?(nat_compare_invert e e1)). +simplify.elim nat_compare e1 e.simplify.apply refl_equal. +simplify. apply refl_equal. +simplify. apply refl_equal. +elim y.simplify.reflexivity. +simplify.elim (sym_eq ? ? ?(nat_compare_invert e e1)). +simplify.elim nat_compare e1 e.simplify.apply refl_equal. +simplify. apply refl_equal. +simplify. apply refl_equal. +simplify.elim (sym_plus e1 e).apply refl_equal. +qed. + +theorem Zpred_neg : \forall z:Z. eq Z (Zpred z) (Zplus (neg O) z). +intros.elim z. +simplify.apply refl_equal. +simplify.apply refl_equal. +elim e.simplify.apply refl_equal. +simplify.apply refl_equal. +qed. + +theorem Zsucc_pos : \forall z:Z. eq Z (Zsucc z) (Zplus (pos O) z). +intros.elim z. +simplify.apply refl_equal. +elim e.simplify.apply refl_equal. +simplify.apply refl_equal. +simplify.apply refl_equal. +qed. + +theorem Zplus_succ_pred_pp : +\forall n,m. eq Z (Zplus (pos n) (pos m)) (Zplus (Zsucc (pos n)) (Zpred (pos m))). +intros. +elim n.elim m. +simplify.apply refl_equal. +simplify.apply refl_equal. +elim m. +simplify.elim (plus_n_O ?).apply refl_equal. +simplify.elim (plus_n_Sm ? ?).apply refl_equal. +qed. + +theorem Zplus_succ_pred_pn : +\forall n,m. eq Z (Zplus (pos n) (neg m)) (Zplus (Zsucc (pos n)) (Zpred (neg m))). +intros.apply refl_equal. +qed. + +theorem Zplus_succ_pred_np : +\forall n,m. eq Z (Zplus (neg n) (pos m)) (Zplus (Zsucc (neg n)) (Zpred (pos m))). +intros. +elim n.elim m. +simplify.apply refl_equal. +simplify.apply refl_equal. +elim m. +simplify.apply refl_equal. +simplify.apply refl_equal. +qed. + +theorem Zplus_succ_pred_nn: +\forall n,m. eq Z (Zplus (neg n) (neg m)) (Zplus (Zsucc (neg n)) (Zpred (neg m))). +intros. +elim n.elim m. +simplify.apply refl_equal. +simplify.apply refl_equal. +elim m. +simplify.elim (plus_n_Sm ? ?).apply refl_equal. +simplify.elim (sym_eq ? ? ? (plus_n_Sm ? ?)).apply refl_equal. +qed. + +theorem Zplus_succ_pred: +\forall x,y. eq Z (Zplus x y) (Zplus (Zsucc x) (Zpred y)). +intros. +elim x. elim y. +simplify.apply refl_equal. +simplify.apply refl_equal. +elim (Zsucc_pos ?).elim (sym_eq ? ? ? (Zsucc_pred ?)).apply refl_equal. +elim y.elim sym_Zplus ? ?.elim sym_Zplus (Zpred OZ) ?. +elim (Zpred_neg ?).elim (sym_eq ? ? ? (Zpred_succ ?)). +simplify.apply refl_equal. +apply Zplus_succ_pred_nn. +apply Zplus_succ_pred_np. +elim y.simplify.apply refl_equal. +apply Zplus_succ_pred_pn. +apply Zplus_succ_pred_pp. +qed. + +theorem Zsucc_plus_pp : +\forall n,m. eq Z (Zplus (Zsucc (pos n)) (pos m)) (Zsucc (Zplus (pos n) (pos m))). +intros.apply refl_equal. +qed. + +theorem Zsucc_plus_pn : +\forall n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m))). +intros. +apply nat_double_ind +(\lambda n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m)))).intro. +intros.elim n1. +simplify. apply refl_equal. +elim e.simplify. apply refl_equal. +simplify. apply refl_equal. +intros. elim n1. +simplify. apply refl_equal. +simplify.apply refl_equal. +intros. +elim (Zplus_succ_pred_pn ? m1). +elim H.apply refl_equal. +qed. + +theorem Zsucc_plus_nn : +\forall n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m))). +intros. +apply nat_double_ind +(\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m)))).intro. +intros.elim n1. +simplify. apply refl_equal. +elim e.simplify. apply refl_equal. +simplify. apply refl_equal. +intros. elim n1. +simplify. apply refl_equal. +simplify.apply refl_equal. +intros. +elim (Zplus_succ_pred_nn ? m1). +apply refl_equal. +qed. + +theorem Zsucc_plus_np : +\forall n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m))). +intros. +apply nat_double_ind +(\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m)))). +intros.elim n1. +simplify. apply refl_equal. +elim e.simplify. apply refl_equal. +simplify. apply refl_equal. +intros. elim n1. +simplify. apply refl_equal. +simplify.apply refl_equal. +intros. +elim H. +elim (Zplus_succ_pred_np ? (S m1)). +apply refl_equal. +qed. + + +theorem Zsucc_plus : \forall x,y:Z. eq Z (Zplus (Zsucc x) y) (Zsucc (Zplus x y)). +intros.elim x.elim y. +simplify. apply refl_equal. +elim (Zsucc_pos ?).apply refl_equal. +simplify.apply refl_equal. +elim y.elim sym_Zplus ? ?.elim sym_Zplus OZ ?.simplify.apply refl_equal. +apply Zsucc_plus_nn. +apply Zsucc_plus_np. +elim y. +elim (sym_Zplus OZ ?).apply refl_equal. +apply Zsucc_plus_pn. +apply Zsucc_plus_pp. +qed. + +theorem Zpred_plus : \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 (sym_eq ? ? ? Hcut). +elim (sym_eq ? ? ? (Zsucc_plus ? ?)). +elim (sym_eq ? ? ? (Zpred_succ ?)). +apply refl_equal. +elim (sym_eq ? ? ? (Zsucc_pred ?)). +apply refl_equal. +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.apply refl_equal. +elim e.elim (Zpred_neg (Zplus y z)). +elim (Zpred_neg y). +elim (Zpred_plus ? ?). +apply refl_equal. +elim (sym_eq ? ? ? (Zpred_plus (neg e1) ?)). +elim (sym_eq ? ? ? (Zpred_plus (neg e1) ?)). +elim (sym_eq ? ? ? (Zpred_plus (Zplus (neg e1) y) ?)). +apply f_equal.assumption. +elim e.elim (Zsucc_pos ?). +elim (Zsucc_pos ?). +apply (sym_eq ? ? ? (Zsucc_plus ? ?)) . +elim (sym_eq ? ? ? (Zsucc_plus (pos e1) ?)). +elim (sym_eq ? ? ? (Zsucc_plus (pos e1) ?)). +elim (sym_eq ? ? ? (Zsucc_plus (Zplus (pos e1) y) ?)). +apply f_equal.assumption. +qed. + + + -- 2.39.2