From: Andrea Asperti Date: Mon, 11 Jul 2005 07:20:13 +0000 (+0000) Subject: New version of the library, a bit more structured. X-Git-Tag: pre_notation~59 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=244d65f63ca6a736b871f9f91328fe8c5524ff05;p=helm.git New version of the library, a bit more structured. --- diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma new file mode 100644 index 000000000..d7b378c00 --- /dev/null +++ b/helm/matita/library/Z/z.ma @@ -0,0 +1,321 @@ +(**************************************************************************) +(* ___ *) +(* ||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/Z/". + +include "../nat/nat.ma". + +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.reflexivity. +simplify.intros. +cut match neg e1 with +[ OZ \Rightarrow True +| (pos n) \Rightarrow False +| (neg n) \Rightarrow False]. +apply Hcut.rewrite > H.simplify.exact I. +simplify.intros. +cut match pos e2 with +[ OZ \Rightarrow True +| (pos n) \Rightarrow False +| (neg n) \Rightarrow False]. +apply Hcut. rewrite > 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.reflexivity. +elim e1.reflexivity. +reflexivity. +reflexivity. +qed. + +theorem Zsucc_pred: \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 + 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.reflexivity. +simplify.reflexivity. +simplify.reflexivity. +qed. + +theorem sym_Zplus : \forall x,y:Z. eq Z (Zplus x y) (Zplus y x). +intros.elim x.simplify.rewrite > Zplus_z_O.reflexivity. +elim y.simplify.reflexivity. +simplify. +rewrite < sym_plus.reflexivity. +simplify. +rewrite > nat_compare_invert. +simplify.elim nat_compare ? ?.simplify.reflexivity. +simplify. reflexivity. +simplify. reflexivity. +elim y.simplify.reflexivity. +simplify.rewrite > nat_compare_invert. +simplify.elim nat_compare ? ?.simplify.reflexivity. +simplify. reflexivity. +simplify. reflexivity. +simplify.elim (sym_plus ? ?).reflexivity. +qed. + +theorem Zpred_neg : \forall z:Z. eq Z (Zpred z) (Zplus (neg O) z). +intros.elim z. +simplify.reflexivity. +simplify.reflexivity. +elim e2.simplify.reflexivity. +simplify.reflexivity. +qed. + +theorem Zsucc_pos : \forall z:Z. eq Z (Zsucc z) (Zplus (pos O) z). +intros.elim z. +simplify.reflexivity. +elim e1.simplify.reflexivity. +simplify.reflexivity. +simplify.reflexivity. +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.reflexivity. +simplify.reflexivity. +elim m. +simplify. +rewrite < plus_n_O.reflexivity. +simplify. +rewrite < plus_n_Sm.reflexivity. +qed. + +theorem Zplus_succ_pred_pn : +\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 : +\forall n,m. eq Z (Zplus (neg n) (pos m)) (Zplus (Zsucc (neg n)) (Zpred (pos m))). +intros. +elim n.elim m. +simplify.reflexivity. +simplify.reflexivity. +elim m. +simplify.reflexivity. +simplify.reflexivity. +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.reflexivity. +simplify.reflexivity. +elim m. +simplify.rewrite < plus_n_Sm.reflexivity. +simplify.rewrite > plus_n_Sm.reflexivity. +qed. + +theorem Zplus_succ_pred: +\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. +elim y.rewrite < sym_Zplus.rewrite < sym_Zplus (Zpred OZ). +rewrite < Zpred_neg.rewrite > Zpred_succ. +simplify.reflexivity. +rewrite < Zplus_succ_pred_nn.reflexivity. +apply Zplus_succ_pred_np. +elim y.simplify.reflexivity. +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.reflexivity. +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. reflexivity. +elim e1.simplify. reflexivity. +simplify. reflexivity. +intros. elim n1. +simplify. reflexivity. +simplify.reflexivity. +intros. +rewrite < (Zplus_succ_pred_pn ? m1). +elim H.reflexivity. +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. reflexivity. +elim e1.simplify. reflexivity. +simplify. reflexivity. +intros. elim n1. +simplify. reflexivity. +simplify.reflexivity. +intros. +rewrite < (Zplus_succ_pred_nn ? m1). +reflexivity. +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. reflexivity. +elim e1.simplify. reflexivity. +simplify. reflexivity. +intros. elim n1. +simplify. reflexivity. +simplify.reflexivity. +intros. +rewrite < H. +rewrite < (Zplus_succ_pred_np ? (S m1)). +reflexivity. +qed. + + +theorem Zsucc_plus : \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. +simplify.reflexivity. +elim y.rewrite < sym_Zplus.rewrite < sym_Zplus OZ.simplify.reflexivity. +apply Zsucc_plus_nn. +apply Zsucc_plus_np. +elim y. +rewrite < sym_Zplus OZ.reflexivity. +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)). +rewrite > Hcut. +rewrite > Zsucc_plus. +rewrite > Zpred_succ. +reflexivity. +rewrite > Zsucc_pred. +reflexivity. +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. +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. +reflexivity. +rewrite > Zsucc_plus (pos e1). +rewrite > Zsucc_plus (pos e1). +rewrite > Zsucc_plus (Zplus (pos e1) y). +apply f_equal.assumption. +qed. diff --git a/helm/matita/library/datatypes/bool.ma b/helm/matita/library/datatypes/bool.ma new file mode 100644 index 000000000..fdb376c60 --- /dev/null +++ b/helm/matita/library/datatypes/bool.ma @@ -0,0 +1,45 @@ +(**************************************************************************) +(* ___ *) +(* ||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/bool/". + +inductive bool : Set \def + | true : bool + | false : bool. + +definition notb : 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]. diff --git a/helm/matita/library/datatypes/compare.ma b/helm/matita/library/datatypes/compare.ma new file mode 100644 index 000000000..3e0271d59 --- /dev/null +++ b/helm/matita/library/datatypes/compare.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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/compare/". + +inductive compare :Set \def +| LT : compare +| EQ : compare +| GT : compare. + +definition compare_invert: compare \to compare \def + \lambda c. + match c with + [ LT \Rightarrow GT + | EQ \Rightarrow EQ + | GT \Rightarrow LT ]. diff --git a/helm/matita/library/higher_order_defs/functions.ma b/helm/matita/library/higher_order_defs/functions.ma new file mode 100644 index 000000000..bdea562ce --- /dev/null +++ b/helm/matita/library/higher_order_defs/functions.ma @@ -0,0 +1,44 @@ +(**************************************************************************) +(* ___ *) +(* ||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/higher_order_defs/functions/". + +include "logic/equality.ma". +include "logic/connectives.ma". + +definition injective: \forall A,B:Type.\forall f:A \to B.Prop +\def \lambda A,B.\lambda f. + \forall x,y:A.eq B (f x) (f y) \to (eq A x y). + +(* we have still to attach exists *) +definition surjective: \forall A,B:Type.\forall f:A \to B.Prop +\def \lambda A,B.\lambda f. + \forall z:B.ex A (\lambda x:A.(eq B z (f x))). + +definition symmetric: \forall A:Type.\forall f:A \to A\to A.Prop +\def \lambda A.\lambda f.\forall x,y.eq A (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.eq A (f (f x y) z) (f x (f y z)). + +(* functions and relations *) +definition monotonic : \forall A:Type.\forall R:A \to A \to Prop. +\forall f:A \to A.Prop \def +\lambda A. \lambda R. \lambda f. \forall x,y:A.R x y \to R (f x) (f y). + +(* functions and functions *) +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.eq A (f x (g y z)) (g (f x y) (f x z)). + + diff --git a/helm/matita/library/higher_order_defs/ordering.ma b/helm/matita/library/higher_order_defs/ordering.ma new file mode 100644 index 000000000..a945805da --- /dev/null +++ b/helm/matita/library/higher_order_defs/ordering.ma @@ -0,0 +1,22 @@ +(**************************************************************************) +(* ___ *) +(* ||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/higher_order_defs/ordering/". + +include "logic/equality.ma". + +definition antisymmetric: \forall A:Type.\forall R:A \to A \to Prop.Prop +\def +\lambda A.\lambda R.\forall x,y:A.R x y \to R y x \to (eq A x y). + diff --git a/helm/matita/library/higher_order_defs/relations.ma b/helm/matita/library/higher_order_defs/relations.ma new file mode 100644 index 000000000..ff75c9d95 --- /dev/null +++ b/helm/matita/library/higher_order_defs/relations.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||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/higher_order_defs/relations/". + +include "logic/connectives.ma". + +definition reflexive: \forall A:Type.\forall R:A \to A \to Prop.Prop +\def +\lambda A.\lambda R.\forall x:A.R x x. + +definition symmetric: \forall A:Type.\forall R:A \to A \to Prop.Prop +\def +\lambda A.\lambda R.\forall x,y:A.R x y \to R y x. + +definition transitive: \forall A:Type.\forall R:A \to A \to Prop.Prop +\def +\lambda A.\lambda R.\forall x,y,z:A.R x y \to R y z \to R x z. + diff --git a/helm/matita/library/logic/connectives.ma b/helm/matita/library/logic/connectives.ma new file mode 100644 index 000000000..835bb6873 --- /dev/null +++ b/helm/matita/library/logic/connectives.ma @@ -0,0 +1,56 @@ +(**************************************************************************) +(* ___ *) +(* ||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/connectives/". + +inductive True: Prop \def +I : True. + +default "true" cic:/matita/logic/True.ind. + +inductive False: Prop \def . + +default "false" cic:/matita/logic/False.ind. + +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. + +default "absurd" cic:/matita/logic/absurd.ind. + +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 B. +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). + +definition decidable : Prop \to Prop \def \lambda A:Prop. Or A (Not A). + +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. diff --git a/helm/matita/library/logic/equality.ma b/helm/matita/library/logic/equality.ma new file mode 100644 index 000000000..fb7e66edf --- /dev/null +++ b/helm/matita/library/logic/equality.ma @@ -0,0 +1,62 @@ +(**************************************************************************) +(* ___ *) +(* ||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/logic/equality/". + +include "higher_order_defs/relations.ma". + +inductive eq (A:Type) (x:A) : A \to Prop \def + refl_eq : eq A x x. + +theorem reflexive_eq : \forall A:Type. reflexive A (eq A). +simplify.intros.apply refl_eq. +qed. + +theorem symmetric_eq: \forall A:Type. symmetric A (eq A). +simplify.intros.elim H. apply refl_eq. +qed. + +theorem sym_eq : \forall A:Type.\forall x,y:A. eq A x y \to eq A y x +\def symmetric_eq. + +theorem transitive_eq : \forall A:Type. transitive A (eq A). +simplify.intros.elim H1.assumption. +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 +\def transitive_eq. + +theorem eq_elim_r: + \forall A:Type.\forall x:A. \forall P: A \to Prop. + P x \to \forall y:A. eq A y x \to P y. +intros. elim sym_eq ? ? ? H1.assumption. +qed. + +default "equality" + cic:/matita/logic/equality/eq.ind + cic:/matita/logic/equality/sym_eq.con + cic:/matita/logic/equality/trans_eq.con + cic:/matita/logic/equality/eq_ind.con + cic:/matita/logic/equality/eq_elim_r.con. + +theorem eq_f: \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.reflexivity. +qed. + +theorem eq_f2: \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.reflexivity. +qed. \ No newline at end of file diff --git a/helm/matita/library/nat/compare.ma b/helm/matita/library/nat/compare.ma new file mode 100644 index 000000000..af3ca38f8 --- /dev/null +++ b/helm/matita/library/nat/compare.ma @@ -0,0 +1,59 @@ +(**************************************************************************) +(* ___ *) +(* ||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/nat/compare.ma". + +include "nat/orders.ma". +include "datatypes/bool.ma". + +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 leb_to_Prop: \forall n,m:nat. +match (leb n m) with +[ true \Rightarrow (le n m) +| false \Rightarrow (Not (le n m))]. +intros. +apply nat_elim2 +(\lambda n,m:nat.match (leb n m) with +[ true \Rightarrow (le n m) +| false \Rightarrow (Not (le n m))]). +simplify.exact le_O_n. +simplify.exact not_le_Sn_O. +intros 2.simplify.elim (leb n1 m1). +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. +((le n m) \to (P true)) \to ((Not (le n m)) \to (P false)) \to +P (leb n m). +intros. +cut +match (leb n m) with +[ true \Rightarrow (le n m) +| false \Rightarrow (Not (le n m))] \to (P (leb n m)). +apply Hcut.apply leb_to_Prop. +elim leb n m. +apply (H H2). +apply (H1 H2). +qed. + + + diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma new file mode 100644 index 000000000..4fa85a6bb --- /dev/null +++ b/helm/matita/library/nat/minus.ma @@ -0,0 +1,160 @@ +(**************************************************************************) +(* ___ *) +(* ||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/nat/minus.ma". + +include "nat/orders_op.ma". +include "nat/times.ma". + +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 minus_n_O: \forall n:nat.eq nat n (minus n O). +intros.elim n.simplify.reflexivity. +simplify.reflexivity. +qed. + +theorem minus_n_n: \forall n:nat.eq nat O (minus n n). +intros.elim n.simplify. +reflexivity. +simplify.apply H. +qed. + +theorem minus_Sn_n: \forall n:nat.eq nat (S O) (minus (S n) n). +intro.elim n. +simplify.reflexivity. +elim H.reflexivity. +qed. + +theorem minus_Sn_m: \forall n,m:nat. +le m n \to eq nat (minus (S n) m) (S (minus n m)). +intros 2. +apply nat_elim2 +(\lambda n,m.le m n \to eq nat (minus (S n) m) (S (minus n m))). +intros.apply le_n_O_elim n1 H. +simplify.reflexivity. +intros.simplify.reflexivity. +intros.rewrite < H.reflexivity. +apply le_S_S_to_le. assumption. +qed. + +theorem plus_minus: +\forall n,m,p:nat. le m n \to eq nat (plus (minus n m) p) (minus (plus n p) m). +intros 2. +apply nat_elim2 +(\lambda n,m.\forall p:nat.le m n \to eq nat (plus (minus n m) p) (minus (plus n p) m)). +intros.apply le_n_O_elim ? H. +simplify.rewrite < minus_n_O.reflexivity. +intros.simplify.reflexivity. +intros.simplify.apply H.apply le_S_S_to_le.assumption. +qed. + +theorem plus_minus_m_m: \forall n,m:nat. +le m n \to eq nat n (plus (minus n m) m). +intros 2. +apply nat_elim2 (\lambda n,m.le m n \to eq nat n (plus (minus n m) m)). +intros.apply le_n_O_elim n1 H. +reflexivity. +intros.simplify.rewrite < plus_n_O.reflexivity. +intros.simplify.rewrite < sym_plus.simplify. +apply eq_f.rewrite < sym_plus.apply H. +apply le_S_S_to_le.assumption. +qed. + +theorem minus_to_plus :\forall n,m,p:nat.le m n \to eq nat (minus n m) p \to +eq nat n (plus m p). +intros.apply trans_eq ? ? (plus (minus n m) m) ?. +apply plus_minus_m_m. +apply H.elim H1. +apply sym_plus. +qed. + +theorem plus_to_minus :\forall n,m,p:nat.le m n \to +eq nat n (plus m p) \to eq nat (minus n m) p. +intros. +apply inj_plus_r m. +rewrite < H1. +rewrite < sym_plus. +symmetry. +apply plus_minus_m_m.assumption. +qed. + +theorem minus_ge_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). +intros.simplify.reflexivity. +intros.apply False_ind. +(* ancora problemi con il not *) +apply not_le_Sn_O n1 H. +intros. +simplify.apply H.apply le_S_S_to_le. apply H1. +qed. + +theorem le_SO_minus: \forall n,m:nat.le (S n) m \to le (S O) (minus m n). +intros.elim H.elim minus_Sn_n n.apply le_n. +rewrite > minus_Sn_m. +apply le_S.assumption. +apply lt_to_le.assumption. +qed. + +(* +theorem le_plus_minus: \forall n,m,p. (le (plus n m) p) \to (le n (minus p m)). +intros 3. +elim p.simplify.apply trans_le ? (plus n m) ?. +elim sym_plus ? ?. +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)). +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). +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. +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. +qed. + +theorem minus_le: \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. +qed. diff --git a/helm/matita/library/nat/nat.ma b/helm/matita/library/nat/nat.ma new file mode 100644 index 000000000..ff41ba62e --- /dev/null +++ b/helm/matita/library/nat/nat.ma @@ -0,0 +1,88 @@ +(**************************************************************************) +(* ___ *) +(* ||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/nat/nat". + +include "logic/equality.ma". +include "logic/connectives.ma". +include "higher_order_defs/functions.ma". + +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 p) \Rightarrow p ]. + +theorem pred_Sn : \forall n:nat. +(eq nat n (pred (S n))). +intros; reflexivity. +qed. + +theorem injective_S : injective nat nat S. +simplify. +intros. +rewrite > pred_Sn. +rewrite > pred_Sn y. +apply eq_f. assumption. +qed. + +theorem inj_S : \forall n,m:nat. +(eq nat (S n) (S m)) \to (eq nat n m) +\def injective_S. + +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 not_eq_O_S : \forall n:nat. Not (eq nat O (S n)). +intros. simplify. intros. +cut (not_zero O). +exact Hcut. +rewrite > H.exact I. +qed. + +theorem not_eq_n_Sn : \forall n:nat. Not (eq nat n (S n)). +intros.elim n. +apply not_eq_O_S. +apply not_eq_S.assumption. +qed. + +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_elim2 : +\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 5.elim n. +apply H. +apply nat_case m.apply H1. +intros.apply H2. apply H3. +qed. + diff --git a/helm/matita/library/nat/orders.ma b/helm/matita/library/nat/orders.ma new file mode 100644 index 000000000..4c1b1a0c4 --- /dev/null +++ b/helm/matita/library/nat/orders.ma @@ -0,0 +1,158 @@ +(**************************************************************************) +(* ___ *) +(* ||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/nat/orders.ma". + +include "logic/connectives.ma". +include "logic/equality.ma". +include "nat/nat.ma". +include "nat/plus.ma". +include "higher_order_defs/ordering.ma". + +(* definitions *) +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). + +definition lt: nat \to nat \to Prop \def +\lambda n,m:nat.le (S n) m. + +definition ge: nat \to nat \to Prop \def +\lambda n,m:nat.le m n. + +definition gt: nat \to nat \to Prop \def +\lambda n,m:nat.lt m n. + +theorem transitive_le : transitive nat le. +simplify.intros.elim H1. +assumption. +apply le_S.assumption. +qed. + +theorem trans_le: \forall n,m,p:nat. le n m \to le m p \to le n p +\def transitive_le. + +theorem le_S_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 le_S_S_to_le : \forall n,m:nat. le (S n) (S m) \to le n m. +intros.change with le (pred (S n)) (pred (S m)). +elim H.apply le_n.apply trans_le ? (pred x).assumption. +apply le_pred_n. +qed. + +theorem leS_to_not_zero : \forall n,m:nat. (le (S n) m ) \to not_zero m. +intros.elim H.exact I.exact I. +qed. + +(* not le *) +theorem not_le_Sn_O: \forall n:nat. Not (le (S n) O). +intros.simplify.intros.apply leS_to_not_zero ? ? H. +qed. + +theorem not_le_Sn_n: \forall n:nat. Not (le (S n) n). +intros.elim n.apply not_le_Sn_O.simplify.intros.cut le (S e1) e1. +apply H.assumption. +apply le_S_S_to_le.assumption. +qed. + +(* le vs. lt *) +theorem lt_to_le : \forall n,m:nat. lt n m \to le n m. +simplify.intros.elim H. +apply le_S. apply le_n. +apply le_S. assumption. +qed. + +theorem not_le_to_lt: \forall n,m:nat. Not (le n m) \to lt m n. +intros 2. +apply nat_elim2 (\lambda n,m.Not (le n m) \to lt m n). +intros.apply absurd (le O n1).apply le_O_n.assumption. +simplify.intros.apply le_S_S.apply le_O_n. +simplify.intros.apply le_S_S.apply H.intros.apply H1.apply le_S_S. +assumption. +qed. + +theorem lt_to_not_le: \forall n,m:nat. lt n m \to Not (le m n). +simplify.intros 3.elim H. +apply not_le_Sn_n n H1. +apply H2.apply lt_to_le. apply H3. +qed. + +(* le elimination *) +theorem le_n_O_to_eq : \forall n:nat. (le n O) \to (eq nat O n). +intro.elim n.reflexivity. +apply False_ind. +(* non si applica not_le_Sn_O *) +apply (not_le_Sn_O ? H1). +qed. + +theorem le_n_O_elim: \forall n:nat.le n O \to \forall P: nat \to Prop. +P O \to P n. +intro.elim n. +assumption. +apply False_ind. +apply (not_le_Sn_O ? H1). +qed. + +theorem le_n_Sm_elim : \forall n,m:nat.le n (S m) \to +\forall P:Prop. (le (S n) (S m) \to P) \to (eq nat n (S m) \to P) \to P. +intros 4.elim H. +apply H2.reflexivity. +apply H3. apply le_S_S. assumption. +qed. + +(* other abstract properties *) +theorem antisymmetric_le : antisymmetric nat le. +simplify.intros 2. +apply nat_elim2 (\lambda n,m.((le n m) \to (le m n) \to eq nat n m)). +intros.apply le_n_O_to_eq.assumption. +intros.apply False_ind.apply not_le_Sn_O ? H. +intros.apply eq_f.apply H. +apply le_S_S_to_le.assumption. +apply le_S_S_to_le.assumption. +qed. + +theorem antisym_le: \forall n,m:nat. le n m \to le m n \to eq nat n m +\def antisymmetric_le. + +theorem decidable_le: \forall n,m:nat. decidable (le n m). +intros. +apply nat_elim2 (\lambda n,m.decidable (le n m)). +intros.simplify.left.apply le_O_n. +intros.simplify.right.exact not_le_Sn_O n1. +intros 2.simplify.intro.elim H. +left.apply le_S_S.assumption. +right.intro.apply H1.apply le_S_S_to_le.assumption. +qed. + + diff --git a/helm/matita/library/nat/orders_op.ma b/helm/matita/library/nat/orders_op.ma new file mode 100644 index 000000000..dbd48fa88 --- /dev/null +++ b/helm/matita/library/nat/orders_op.ma @@ -0,0 +1,99 @@ +(**************************************************************************) +(* ___ *) +(* ||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/nat/orders_op.ma". + +include "higher_order_defs/functions.ma". +include "nat/times.ma". +include "nat/orders.ma". + +(* plus *) +theorem monotonic_le_plus_r: +\forall n:nat.monotonic nat le (\lambda m.plus n m). +simplify.intros.elim n. +simplify.assumption. +simplify.apply le_S_S.assumption. +qed. + +theorem le_plus_r: \forall p,n,m:nat. le n m \to le (plus p n) (plus p m) +\def monotonic_le_plus_r. + +theorem monotonic_le_plus_l: +\forall m:nat.monotonic nat le (\lambda n.plus n m). +simplify.intros. +rewrite < sym_plus.rewrite < sym_plus m. +apply le_plus_r.assumption. +qed. + +theorem le_plus_l: \forall p,n,m:nat. le n m \to le (plus n p) (plus m p) +\def monotonic_le_plus_l. + +theorem le_plus: \forall n1,n2,m1,m2:nat. le n1 n2 \to le m1 m2 +\to le (plus n1 m1) (plus n2 m2). +intros. +apply trans_le ? (plus n2 m1). +apply le_plus_l.assumption. +apply le_plus_r.assumption. +qed. + +theorem le_plus_n :\forall n,m:nat. le m (plus n m). +intros.change with le (plus O m) (plus n m). +apply le_plus_l.apply le_O_n. +qed. + +theorem eq_plus_to_le: \forall n,m,p:nat.eq nat n (plus m p) +\to le m n. +intros.rewrite > H. +rewrite < sym_plus. +apply le_plus_n. +qed. + +(* times *) +theorem monotonic_le_times_r: +\forall n:nat.monotonic nat le (\lambda m.times n m). +simplify.intros.elim n. +simplify.apply le_O_n. +simplify.apply le_plus. +assumption. +assumption. +qed. + +theorem le_times_r: \forall p,n,m:nat. le n m \to le (times p n) (times p m) +\def monotonic_le_times_r. + +theorem monotonic_le_times_l: +\forall m:nat.monotonic nat le (\lambda n.times n m). +simplify.intros. +rewrite < sym_times.rewrite < sym_times m. +apply le_times_r.assumption. +qed. + +theorem le_times_l: \forall p,n,m:nat. le n m \to le (times n p) (times m p) +\def monotonic_le_times_l. + +theorem le_times: \forall n1,n2,m1,m2:nat. le n1 n2 \to le m1 m2 +\to le (times n1 m1) (times n2 m2). +intros. +apply trans_le ? (times n2 m1). +apply le_times_l.assumption. +apply le_times_r.assumption. +qed. + +theorem le_n_nm: \forall n,m:nat.le (S O) n \to le m (times n m). +intros.elim H.simplify. +elim (plus_n_O ?).apply le_n. +simplify.rewrite < sym_plus.apply le_plus_n. +qed. + + diff --git a/helm/matita/library/nat/plus.ma b/helm/matita/library/nat/plus.ma new file mode 100644 index 000000000..1a43e216f --- /dev/null +++ b/helm/matita/library/nat/plus.ma @@ -0,0 +1,76 @@ +(**************************************************************************) +(* ___ *) +(* ||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/nat/plus.ma". + +include "logic/equality.ma". +include "nat/nat.ma". + +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.reflexivity. +simplify.apply eq_f.assumption. +qed. + +theorem plus_n_Sm : \forall n,m:nat. eq nat (S (plus n m)) (plus n (S m)). +intros.elim n. +simplify.reflexivity. +simplify.apply eq_f.assumption. +qed. + +(* some problem here: confusion between relations/symmetric +and functions/symmetric; functions symmetric is not in +functions.moo why? +theorem symmetric_plus: symmetric nat plus. *) + +theorem sym_plus: \forall n,m:nat. eq nat (plus n m) (plus m n). +intros.elim n. +simplify.apply plus_n_O. +simplify.rewrite > H.apply plus_n_Sm. +qed. + +theorem associative_plus : associative nat plus. +simplify.intros.elim x. +simplify.reflexivity. +simplify.apply eq_f.assumption. +qed. + +theorem assoc_plus : \forall n,m,p:nat. eq nat (plus (plus n m) p) (plus n (plus m p)) +\def associative_plus. + +theorem injective_plus_r: \forall n:nat.injective nat nat (\lambda m.plus n m). +intro.simplify.intros 2.elim n. +exact H. +apply H.apply inj_S.apply H1. +qed. + +theorem inj_plus_r: \forall p,n,m:nat.eq nat (plus p n) (plus p m) \to (eq nat n m) +\def injective_plus_r. + +theorem injective_plus_l: \forall m:nat.injective nat nat (\lambda n.plus n m). +intro.simplify.intros. +(* qui vorrei applicare injective_plus_r *) +apply inj_plus_r m. +rewrite < sym_plus. +rewrite < sym_plus y. +assumption. +qed. + +theorem inj_plus_l: \forall p,n,m:nat.eq nat (plus n p) (plus m p) \to (eq nat n m) +\def injective_plus_l. \ No newline at end of file diff --git a/helm/matita/library/nat/times.ma b/helm/matita/library/nat/times.ma new file mode 100644 index 000000000..f9c731bb0 --- /dev/null +++ b/helm/matita/library/nat/times.ma @@ -0,0 +1,62 @@ +(**************************************************************************) +(* ___ *) +(* ||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/nat/times.ma". + +include "logic/equality.ma". +include "nat/nat.ma". +include "nat/plus.ma". + +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.reflexivity. +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.reflexivity. +simplify.apply eq_f.rewrite < H. +transitivity (plus (plus e1 m) (times e1 m)).symmetry.apply assoc_plus. +transitivity (plus (plus m e1) (times e1 m)). +apply eq_f2. +apply sym_plus. +reflexivity. +apply assoc_plus. +qed. + +(* same problem with symmetric: see plus +theorem symmetric_times : symmetric nat times. *) + +theorem sym_times : +\forall n,m:nat. eq nat (times n m) (times m n). +intros.elim n. +simplify.apply times_n_O. +simplify.rewrite > H.apply times_n_Sm. +qed. + +theorem times_plus_distr: \forall n,m,p:nat. +eq nat (times n (plus m p)) (plus (times n m) (times n p)). +intros.elim n. +simplify.reflexivity. +simplify.rewrite > H. rewrite > assoc_plus.rewrite > assoc_plus. +apply eq_f.rewrite < assoc_plus. rewrite < sym_plus ? p. +rewrite > assoc_plus.reflexivity. +qed.