From 00f04989b1a7792a7cf34deed1a4305d290808d0 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 1 Jul 2005 17:21:13 +0000 Subject: [PATCH] * match.ma removed (it is now splitted in several files in library/*.ma) * Makefile.tests removed (redundant with tests/Makefile) * make tests and make tests.opt now call the same targets in library and tests --- helm/matita/Makefile.tests | 40 --- helm/matita/matita.ml | 4 +- helm/matita/tests/match.ma | 634 ------------------------------------- 3 files changed, 2 insertions(+), 676 deletions(-) delete mode 100644 helm/matita/Makefile.tests delete mode 100644 helm/matita/tests/match.ma diff --git a/helm/matita/Makefile.tests b/helm/matita/Makefile.tests deleted file mode 100644 index cab67026a..000000000 --- a/helm/matita/Makefile.tests +++ /dev/null @@ -1,40 +0,0 @@ -TODO=\ - tests/apply.moo\ - tests/auto.moo\ - tests/baseuri.moo\ - tests/coercions.moo\ - tests/comments.moo\ - tests/fguidi.moo\ - tests/first.moo\ - tests/fix_betareduction.moo\ - tests/inversion.moo\ - tests/letrec.moo\ - tests/match.moo\ - tests/match_inference.moo\ - tests/mysql_escaping.moo\ - tests/record.moo\ - tests/replace.moo\ - tests/rewrite.moo\ - tests/second.moo\ - tests/simpl.moo\ - tests/test2.moo\ - tests/test3.moo\ - tests/test4.moo\ - tests/third.moo - -DEPEND_NAME=.depend.moo - -all: $(TODO) - -clean: - rm -f $(DEPEND_NAME) $(TODO) - ./matitaclean all - -%.moo:%.ma - [ ! -e $@ ] || ./matitaclean $< - ./matitac $< || ./matitaclean $< - -$(DEPEND_NAME): $(TODO:%.moo=%.ma) - ./matitadep $^ > $@ - -include $(DEPEND_NAME) diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 6e2fe2526..93441ed83 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -35,8 +35,8 @@ let _ = Helm_registry.load_from "matita.conf.xml"; (* read conf *) Http_getter.init (); MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); - MatitaDb.clean_owner_environment (); - MatitaDb.create_owner_environment (); +(* MatitaDb.clean_owner_environment (); + MatitaDb.create_owner_environment (); *) GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *) ignore (GMain.Main.init ()); diff --git a/helm/matita/tests/match.ma b/helm/matita/tests/match.ma deleted file mode 100644 index f006a7045..000000000 --- a/helm/matita/tests/match.ma +++ /dev/null @@ -1,634 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| A.Asperti, C.Sacerdoti Coen, *) -(* ||A|| E.Tassi, S.Zacchiroli *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU Lesser General Public License Version 2.1 *) -(* *) -(**************************************************************************) - -set "baseuri" "cic:/matita/tests/match/". - - -inductive True: Prop \def -I : True. - -inductive False: Prop \def . - -definition Not: Prop \to Prop \def -\lambda A. (A \to False). - -theorem absurd : \forall A,C:Prop. A \to Not A \to C. -intros. elim (H1 H). -qed. - -inductive And (A,B:Prop) : Prop \def - conj : A \to B \to (And A B). - -theorem proj1: \forall A,B:Prop. (And A B) \to A. -intros. elim H. assumption. -qed. - -theorem proj2: \forall A,B:Prop. (And A B) \to A. -intros. elim H. assumption. -qed. - -inductive Or (A,B:Prop) : Prop \def - or_introl : A \to (Or A B) - | or_intror : B \to (Or A B). - -inductive ex (A:Type) (P:A \to Prop) : Prop \def - ex_intro: \forall x:A. P x \to ex A P. - -inductive ex2 (A:Type) (P,Q:A \to Prop) : Prop \def - ex_intro2: \forall x:A. P x \to Q x \to ex2 A P Q. - -inductive eq (A:Type) (x:A) : A \to Prop \def - refl_equal : eq A x x. - -theorem sym_eq : \forall A:Type.\forall x,y:A. eq A x y \to eq A y x. -intros. elim H. apply refl_equal. -qed. - -theorem trans_eq : \forall A:Type. -\forall x,y,z:A. eq A x y \to eq A y z \to eq A x z. -intros.elim H1.assumption. -qed. - -theorem f_equal: \forall A,B:Type.\forall f:A\to B. -\forall x,y:A. eq A x y \to eq B (f x) (f y). -intros.elim H.apply refl_equal. -qed. - -theorem f_equal2: \forall A,B,C:Type.\forall f:A\to B \to C. -\forall x1,x2:A. \forall y1,y2:B. -eq A x1 x2\to eq B y1 y2\to eq C (f x1 y1) (f x2 y2). -intros.elim H1.elim H.apply refl_equal. -qed. - -inductive nat : Set \def - | O : nat - | S : nat \to nat. - -definition pred: nat \to nat \def -\lambda n:nat. match n with -[ O \Rightarrow O -| (S u) \Rightarrow u ]. - -theorem pred_Sn : \forall n:nat. -(eq nat n (pred (S n))). -intros.apply refl_equal. -qed. - -theorem injective_S : \forall n,m:nat. -(eq nat (S n) (S m)) \to (eq nat n m). -intros.(elim (sym_eq ? ? ? (pred_Sn n))).(elim (sym_eq ? ? ? (pred_Sn m))). -apply f_equal. assumption. -qed. - -theorem not_eq_S : \forall n,m:nat. -Not (eq nat n m) \to Not (eq nat (S n) (S m)). -intros. simplify.intros. -apply H.apply injective_S.assumption. -qed. - -definition not_zero : nat \to Prop \def -\lambda n: nat. - match n with - [ O \Rightarrow False - | (S p) \Rightarrow True ]. - -theorem O_S : \forall n:nat. Not (eq nat O (S n)). -intros.simplify.intros. -cut (not_zero O).exact Hcut.elim (sym_eq ? ? ? H). -exact I. -qed. - -theorem n_Sn : \forall n:nat. Not (eq nat n (S n)). -intros.elim n.apply O_S.apply not_eq_S.assumption. -qed. - - -let rec plus n m \def - match n with - [ O \Rightarrow m - | (S p) \Rightarrow S (plus p m) ]. - -theorem plus_n_O: \forall n:nat. eq nat n (plus n O). -intros.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption. -qed. - -theorem plus_n_Sm : \forall n,m:nat. eq nat (S (plus n m)) (plus n (S m)). -intros.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption. -qed. - -theorem sym_plus: \forall n,m:nat. eq nat (plus n m) (plus m n). -intros.elim n.simplify.apply plus_n_O. -simplify.elim (sym_eq ? ? ? H).apply plus_n_Sm. -qed. - -theorem assoc_plus: -\forall n,m,p:nat. eq nat (plus (plus n m) p) (plus n (plus m p)). -intros.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption. -qed. - -let rec times n m \def - match n with - [ O \Rightarrow O - | (S p) \Rightarrow (plus m (times p m)) ]. - -theorem times_n_O: \forall n:nat. eq nat O (times n O). -intros.elim n.simplify.apply refl_equal.simplify.assumption. -qed. - -theorem times_n_Sm : -\forall n,m:nat. eq nat (plus n (times n m)) (times n (S m)). -intros.elim n.simplify.apply refl_equal. -simplify.apply f_equal.elim H. -apply trans_eq ? ? (plus (plus e m) (times e m)).apply sym_eq. -apply assoc_plus.apply trans_eq ? ? (plus (plus m e) (times e m)). -apply f_equal2. -apply sym_plus.apply refl_equal.apply assoc_plus. -qed. - -theorem sym_times : -\forall n,m:nat. eq nat (times n m) (times m n). -intros.elim n.simplify.apply times_n_O. -simplify.elim (sym_eq ? ? ? H).apply times_n_Sm. -qed. - -let rec minus n m \def - match n with - [ O \Rightarrow O - | (S p) \Rightarrow - match m with - [O \Rightarrow (S p) - | (S q) \Rightarrow minus p q ]]. - -theorem nat_case : -\forall n:nat.\forall P:nat \to Prop. -P O \to (\forall m:nat. P (S m)) \to P n. -intros.elim n.assumption.apply H1. -qed. - -theorem nat_double_ind : -\forall R:nat \to nat \to Prop. -(\forall n:nat. R O n) \to -(\forall n:nat. R (S n) O) \to -(\forall n,m:nat. R n m \to R (S n) (S m)) \to \forall n,m:nat. R n m. -intros.cut \forall m:nat.R n m.apply Hcut.elim n.apply H. -apply nat_case m1.apply H1.intros.apply H2. apply H3. -qed. - -inductive bool : Set \def - | true : bool - | false : bool. - -definition notn : bool \to bool \def -\lambda b:bool. - match b with - [ true \Rightarrow false - | false \Rightarrow true ]. - -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] - | false \Rightarrow false ]. - -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 ]. - -definition if_then_else : bool \to Prop \to Prop \to Prop \def -\lambda b:bool.\lambda P,Q:Prop. -match b with -[ true \Rightarrow P -| false \Rightarrow Q]. - -inductive le (n:nat) : nat \to Prop \def - | le_n : le n n - | le_S : \forall m:nat. le n m \to le n (S m). - -theorem trans_le: \forall n,m,p:nat. le n m \to le m p \to le n p. -intros. -elim H1.assumption. -apply le_S.assumption. -qed. - -theorem le_n_S: \forall n,m:nat. le n m \to le (S n) (S m). -intros.elim H. -apply le_n.apply le_S.assumption. -qed. - -theorem le_O_n : \forall n:nat. le O n. -intros.elim n.apply le_n.apply le_S. assumption. -qed. - -theorem le_n_Sn : \forall n:nat. le n (S n). -intros. apply le_S.apply le_n. -qed. - -theorem le_pred_n : \forall n:nat. le (pred n) n. -intros.elim n.simplify.apply le_n.simplify. -apply le_n_Sn. -qed. - -theorem not_zero_le : \forall n,m:nat. (le (S n) m ) \to not_zero m. -intros.elim H.exact I.exact I. -qed. - -theorem le_Sn_O: \forall n:nat. Not (le (S n) O). -intros.simplify.intros.apply not_zero_le ? O H. -qed. - -theorem le_n_O_eq : \forall n:nat. (le n O) \to (eq nat O n). -intros.cut (le n O) \to (eq nat O n).apply Hcut. assumption. -elim n.apply refl_equal.apply False_ind.apply (le_Sn_O ? H2). -qed. - -theorem le_S_n : \forall n,m:nat. le (S n) (S m) \to le n m. -intros.cut le (pred (S n)) (pred (S m)).exact Hcut. -elim H.apply le_n.apply trans_le ? (pred x).assumption. -apply le_pred_n. -qed. - -theorem le_Sn_n : \forall n:nat. Not (le (S n) n). -intros.elim n.apply le_Sn_O.simplify.intros. -cut le (S e) e.apply H.assumption.apply le_S_n.assumption. -qed. - -theorem le_antisym : \forall n,m:nat. (le n m) \to (le m n) \to (eq nat n m). -intros.cut (le n m) \to (le m n) \to (eq nat n m).exact Hcut H H1. -apply nat_double_ind (\lambda n,m.((le n m) \to (le m n) \to eq nat n m)). -intros.whd.intros. -apply le_n_O_eq.assumption. -intros.whd.intros.apply sym_eq.apply le_n_O_eq.assumption. -intros.whd.intros.apply f_equal.apply H2. -apply le_S_n.assumption. -apply le_S_n.assumption. -qed. - -let rec leb n m \def - match n with - [ O \Rightarrow true - | (S p) \Rightarrow - match m with - [ O \Rightarrow false - | (S q) \Rightarrow leb p q]]. - -theorem le_dec: \forall n,m:nat. if_then_else (leb n m) (le n m) (Not (le n m)). -intros. -apply (nat_double_ind -(\lambda n,m:nat.if_then_else (leb n m) (le n m) (Not (le n m))) ? ? ? n m). -simplify.intros.apply le_O_n. -simplify.exact le_Sn_O. -intros 2.simplify.elim (leb n1 m1). -simplify.apply le_n_S.apply H. -simplify.intros.apply H.apply le_S_n.assumption. -qed. - -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