From: Andrea Asperti Date: Mon, 11 Jul 2005 07:01:16 +0000 (+0000) Subject: Removed the old library. X-Git-Tag: pre_notation~60 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=98e40a03f92d6715db7f53460e761455621346f2;p=helm.git Removed the old library. --- diff --git a/helm/matita/library/Z.ma b/helm/matita/library/Z.ma deleted file mode 100644 index ba1084720..000000000 --- a/helm/matita/library/Z.ma +++ /dev/null @@ -1,321 +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/Z/". - -include "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/bool.ma b/helm/matita/library/bool.ma deleted file mode 100644 index fdb376c60..000000000 --- a/helm/matita/library/bool.ma +++ /dev/null @@ -1,45 +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/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/compare.ma b/helm/matita/library/compare.ma deleted file mode 100644 index 3e0271d59..000000000 --- a/helm/matita/library/compare.ma +++ /dev/null @@ -1,27 +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/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/equality.ma b/helm/matita/library/equality.ma deleted file mode 100644 index 90ce050e3..000000000 --- a/helm/matita/library/equality.ma +++ /dev/null @@ -1,52 +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/equality/". - -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 eq_ind_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.letin H1' \def sym_eq ? ? ? H1.clearbody H1'. -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.reflexivity. -qed. - -default "equality" - cic:/matita/equality/eq.ind - cic:/matita/equality/sym_eq.con - cic:/matita/equality/trans_eq.con - cic:/matita/equality/eq_ind.con - cic:/matita/equality/eq_ind_r.con. - -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.reflexivity. -qed. diff --git a/helm/matita/library/logic.ma b/helm/matita/library/logic.ma deleted file mode 100644 index fd3744396..000000000 --- a/helm/matita/library/logic.ma +++ /dev/null @@ -1,55 +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/logic/". - - -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 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. diff --git a/helm/matita/library/nat.ma b/helm/matita/library/nat.ma deleted file mode 100644 index c125e6775..000000000 --- a/helm/matita/library/nat.ma +++ /dev/null @@ -1,245 +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/nat/". - -include "equality.ma". -include "logic.ma". -include "bool.ma". -include "compare.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 u) \Rightarrow u ]. - -theorem pred_Sn : \forall n:nat. -(eq nat n (pred (S n))). -intros; reflexivity. -qed. - -theorem injective_S : \forall n,m:nat. -(eq nat (S n) (S m)) \to (eq nat n m). -intros; -rewrite > pred_Sn; -rewrite > 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 | rewrite > 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;reflexivity - | 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.reflexivity. -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.rewrite > 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.reflexivity. -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.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 f_equal.rewrite < H. -transitivity (plus (plus e1 m) (times e1 m)).symmetry. -apply assoc_plus.transitivity (plus (plus m e1) (times e1 m)). -apply f_equal2. -apply sym_plus.reflexivity.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.rewrite > 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 5.elim n.apply H. -apply nat_case m.apply H1.intros.apply H2. apply H3. -qed. - -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.reflexivity. -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.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 le_Sn_n : \forall n:nat. Not (le (S n) n). -intros.elim n.apply le_Sn_O.simplify.intros. -cut le (S e1) e1.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.symmetry.apply le_n_O_eq.assumption. -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. - -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]]. - -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.reflexivity. -simplify.reflexivity. -intro.elim n1.simplify.reflexivity. -simplify.reflexivity. -intros.simplify.elim H.simplify.reflexivity. -qed. -