--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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].
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 ].
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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)).
+
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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).
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
+
+
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
+
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
+
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
projects / helm.git / commitdiff