From: Ferruccio Guidi Date: Sun, 20 Aug 2006 20:05:44 +0000 (+0000) Subject: new naming X-Git-Tag: 0.4.95@7852~1130 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7236ac50c5aa6b7a18c5191374d2d4d073650fbc;p=helm.git new naming --- diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/NPlus.ma b/matita/contribs/RELATIONAL-ARITHMETICS/NPlus.ma new file mode 100644 index 000000000..8531c766b --- /dev/null +++ b/matita/contribs/RELATIONAL-ARITHMETICS/NPlus.ma @@ -0,0 +1,23 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/NPlus". + +include "logic/equality.ma". + +include "Nat.ma". + +inductive NPlus (p:Nat): Nat \to Nat \to Prop \def + | NPlus_zero_2: NPlus p zero p + | NPlus_succ_2: \forall q, r. NPlus p q r \to NPlus p (succ q) (succ r). diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/NPlus_fwd.ma b/matita/contribs/RELATIONAL-ARITHMETICS/NPlus_fwd.ma new file mode 100644 index 000000000..bb73113e3 --- /dev/null +++ b/matita/contribs/RELATIONAL-ARITHMETICS/NPlus_fwd.ma @@ -0,0 +1,128 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/NPlus_fwd". + +include "Nat_fwd.ma". +include "NPlus.ma". + +(* primitive generation lemmas proved by elimination and inversion *) + +theorem NPlus_gen_zero_1: \forall q,r. NPlus zero q r \to q = r. + intros. elim H; clear H q r; intros; + [ reflexivity + | clear H1. auto + ]. +qed. + +theorem NPlus_gen_succ_1: \forall p,q,r. NPlus (succ p) q r \to + \exists s. r = (succ s) \land NPlus p q s. + intros. elim H; clear H q r; intros; + [ + | clear H1. + decompose. + rewrite > H1. clear H1 n2 + ]; apply ex_intro; [| auto || auto ]. (**) +qed. + +theorem NPlus_gen_zero_2: \forall p,r. NPlus p zero r \to p = r. + intros. inversion H; clear H; intros; + [ auto + | clear H H1. + lapply eq_gen_zero_succ to H2 as H0. apply H0 + ]. +qed. + +theorem NPlus_gen_succ_2: \forall p,q,r. NPlus p (succ q) r \to + \exists s. r = (succ s) \land NPlus p q s. + intros. inversion H; clear H; intros; + [ lapply eq_gen_succ_zero to H as H0. apply H0 + | clear H1 H3 r. + lapply linear eq_gen_succ_succ to H2 as H0. + rewrite > H0. clear H0 q. + apply ex_intro; [| auto ] (**) + ]. +qed. + +theorem NPlus_gen_zero_3: \forall p,q. NPlus p q zero \to p = zero \land q = zero. + intros. inversion H; clear H; intros; + [ rewrite < H1. clear H1 p. + auto + | clear H H1. + lapply eq_gen_zero_succ to H3 as H0. apply H0 + ]. +qed. + +theorem NPlus_gen_succ_3: \forall p,q,r. NPlus p q (succ r) \to + \exists s. p = succ s \land NPlus s q r \lor + q = succ s \land NPlus p s r. + intros. inversion H; clear H; intros; + [ rewrite < H1. clear H1 p + | clear H1. + lapply linear eq_gen_succ_succ to H3 as H0. + rewrite > H0. clear H0 r. + ]; apply ex_intro; [| auto || auto ] (**) +qed. +(* +(* alternative proofs invoking NPlus_gen_2 *) + +variant NPlus_gen_zero_3_alt: \forall p,q. NPlus p q zero \to p = zero \land q = zero. + intros 2. elim q; clear q; intros; + [ lapply linear NPlus_gen_zero_2 to H as H0. + rewrite > H0. clear H0 p. + auto + | clear H. + lapply linear NPlus_gen_succ_2 to H1 as H0. + decompose. + lapply linear eq_gen_zero_succ to H1 as H0. apply H0 + ]. +qed. + +variant NPlus_gen_succ_3_alt: \forall p,q,r. NPlus p q (succ r) \to + \exists s. p = succ s \land NPlus s q r \lor + q = succ s \land NPlus p s r. + intros 2. elim q; clear q; intros; + [ lapply linear NPlus_gen_zero_2 to H as H0. + rewrite > H0. clear H0 p + | clear H. + lapply linear NPlus_gen_succ_2 to H1 as H0. + decompose. + lapply linear eq_gen_succ_succ to H1 as H0. + rewrite > H0. clear H0 r. + ]; apply ex_intro; [| auto || auto ]. (**) +qed. +*) +(* other simplification lemmas *) + +theorem NPlus_gen_eq_2_3: \forall p,q. NPlus p q q \to p = zero. + intros 2. elim q; clear q; intros; + [ lapply linear NPlus_gen_zero_2 to H as H0. + rewrite > H0. clear H0 p + | lapply linear NPlus_gen_succ_2 to H1 as H0. + decompose. + lapply linear eq_gen_succ_succ to H2 as H0. + rewrite < H0 in H3. clear H0 a + ]; auto. +qed. + +theorem NPlus_gen_eq_1_3: \forall p,q. NPlus p q p \to q = zero. + intros 1. elim p; clear p; intros; + [ lapply linear NPlus_gen_zero_1 to H as H0. + rewrite > H0. clear H0 q + | lapply linear NPlus_gen_succ_1 to H1 as H0. + decompose. + lapply linear eq_gen_succ_succ to H2 as H0. + rewrite < H0 in H3. clear H0 a + ]; auto. +qed. diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/NPlus_props.ma b/matita/contribs/RELATIONAL-ARITHMETICS/NPlus_props.ma new file mode 100644 index 000000000..de0de1b8a --- /dev/null +++ b/matita/contribs/RELATIONAL-ARITHMETICS/NPlus_props.ma @@ -0,0 +1,107 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/NPlus_props". + +include "NPlus_fwd.ma". + +theorem NPlus_zero_1: \forall q. NPlus zero q q. + intros. elim q; clear q; auto. +qed. + +theorem NPlus_succ_1: \forall p,q,r. NPlus p q r \to NPlus (succ p) q (succ r). + intros 2. elim q; clear q; + [ lapply linear NPlus_gen_zero_2 to H as H0. + rewrite > H0. clear H0 p + | lapply linear NPlus_gen_succ_2 to H1 as H0. + decompose. + rewrite > H2. clear H2 r + ]; auto. +qed. + +theorem NPlus_sym: \forall p,q,r. NPlus p q r \to NPlus q p r. + intros 2. elim q; clear q; + [ lapply linear NPlus_gen_zero_2 to H as H0. + rewrite > H0. clear H0 p + | lapply linear NPlus_gen_succ_2 to H1 as H0. + decompose. + rewrite > H2. clear H2 r + ]; auto. +qed. + +theorem NPlus_shift_succ_sx: \forall p,q,r. + NPlus p (succ q) r \to NPlus (succ p) q r. + intros. + lapply linear NPlus_gen_succ_2 to H as H0. + decompose. + rewrite > H1. clear H1 r. + auto. +qed. + +theorem NPlus_shift_succ_dx: \forall p,q,r. + NPlus (succ p) q r \to NPlus p (succ q) r. + intros. + lapply linear NPlus_gen_succ_1 to H as H0. + decompose. + rewrite > H1. clear H1 r. + auto. +qed. + +theorem NPlus_trans_1: \forall p,q1,r1. NPlus p q1 r1 \to + \forall q2,r2. NPlus r1 q2 r2 \to + \exists q. NPlus q1 q2 q \land NPlus p q r2. + intros 2; elim q1; clear q1; intros; + [ lapply linear NPlus_gen_zero_2 to H as H0. + rewrite > H0. clear H0 p + | lapply linear NPlus_gen_succ_2 to H1 as H0. + decompose. + rewrite > H3. rewrite > H3 in H2. clear H3 r1. + lapply linear NPlus_gen_succ_1 to H2 as H0. + decompose. + rewrite > H2. clear H2 r2. + lapply linear H to H4, H3 as H0. + decompose. + ]; apply ex_intro; [| auto || auto ]. (**) +qed. + +theorem NPlus_trans_2: \forall p1,q,r1. NPlus p1 q r1 \to + \forall p2,r2. NPlus p2 r1 r2 \to + \exists p. NPlus p1 p2 p \land NPlus p q r2. + intros 2; elim q; clear q; intros; + [ lapply linear NPlus_gen_zero_2 to H as H0. + rewrite > H0. clear H0 p1 + | lapply linear NPlus_gen_succ_2 to H1 as H0. + decompose. + rewrite > H3. rewrite > H3 in H2. clear H3 r1. + lapply linear NPlus_gen_succ_2 to H2 as H0. + decompose. + rewrite > H2. clear H2 r2. + lapply linear H to H4, H3 as H0. + decompose. + ]; apply ex_intro; [| auto || auto ]. (**) +qed. + +theorem NPlus_conf: \forall p,q,r1. NPlus p q r1 \to + \forall r2. NPlus p q r2 \to r1 = r2. + intros 2. elim q; clear q; intros; + [ lapply linear NPlus_gen_zero_2 to H as H0. + rewrite > H0 in H1. clear H0 p + | lapply linear NPlus_gen_succ_2 to H1 as H0. + decompose. + rewrite > H3. clear H3 r1. + lapply linear NPlus_gen_succ_2 to H2 as H0. + decompose. + rewrite > H2. clear H2 r2. + ]; auto. +qed. diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/Plus.ma b/matita/contribs/RELATIONAL-ARITHMETICS/Plus.ma deleted file mode 100644 index 5b86bf749..000000000 --- a/matita/contribs/RELATIONAL-ARITHMETICS/Plus.ma +++ /dev/null @@ -1,23 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/Plus". - -include "logic/equality.ma". - -include "Nat.ma". - -inductive Plus (p:Nat): Nat \to Nat \to Prop \def - | Plus_zero_2: Plus p zero p - | Plus_succ_2: \forall q, r. Plus p q r \to Plus p (succ q) (succ r). diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/Plus_fwd.ma b/matita/contribs/RELATIONAL-ARITHMETICS/Plus_fwd.ma deleted file mode 100644 index 8f3e20a3c..000000000 --- a/matita/contribs/RELATIONAL-ARITHMETICS/Plus_fwd.ma +++ /dev/null @@ -1,128 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/Plus_fwd". - -include "Nat_fwd.ma". -include "Plus.ma". - -(* primitive generation lemmas proved by elimination and inversion *) - -theorem Plus_gen_zero_1: \forall q,r. Plus zero q r \to q = r. - intros. elim H; clear H q r; intros; - [ reflexivity - | clear H1. auto - ]. -qed. - -theorem Plus_gen_succ_1: \forall p,q,r. Plus (succ p) q r \to - \exists s. r = (succ s) \land Plus p q s. - intros. elim H; clear H q r; intros; - [ - | clear H1. - decompose. - rewrite > H1. clear H1 n2 - ]; apply ex_intro; [| auto || auto ]. (**) -qed. - -theorem Plus_gen_zero_2: \forall p,r. Plus p zero r \to p = r. - intros. inversion H; clear H; intros; - [ auto - | clear H H1. - lapply eq_gen_zero_succ to H2 as H0. apply H0 - ]. -qed. - -theorem Plus_gen_succ_2: \forall p,q,r. Plus p (succ q) r \to - \exists s. r = (succ s) \land Plus p q s. - intros. inversion H; clear H; intros; - [ lapply eq_gen_succ_zero to H as H0. apply H0 - | clear H1 H3 r. - lapply linear eq_gen_succ_succ to H2 as H0. - rewrite > H0. clear H0 q. - apply ex_intro; [| auto ] (**) - ]. -qed. - -theorem Plus_gen_zero_3: \forall p,q. Plus p q zero \to p = zero \land q = zero. - intros. inversion H; clear H; intros; - [ rewrite < H1. clear H1 p. - auto - | clear H H1. - lapply eq_gen_zero_succ to H3 as H0. apply H0 - ]. -qed. - -theorem Plus_gen_succ_3: \forall p,q,r. Plus p q (succ r) \to - \exists s. p = succ s \land Plus s q r \lor - q = succ s \land Plus p s r. - intros. inversion H; clear H; intros; - [ rewrite < H1. clear H1 p - | clear H1. - lapply linear eq_gen_succ_succ to H3 as H0. - rewrite > H0. clear H0 r. - ]; apply ex_intro; [| auto || auto ] (**) -qed. -(* -(* alternative proofs invoking Plus_gen_2 *) - -variant Plus_gen_zero_3_alt: \forall p,q. Plus p q zero \to p = zero \land q = zero. - intros 2. elim q; clear q; intros; - [ lapply linear Plus_gen_zero_2 to H as H0. - rewrite > H0. clear H0 p. - auto - | clear H. - lapply linear Plus_gen_succ_2 to H1 as H0. - decompose. - lapply linear eq_gen_zero_succ to H1 as H0. apply H0 - ]. -qed. - -variant Plus_gen_succ_3_alt: \forall p,q,r. Plus p q (succ r) \to - \exists s. p = succ s \land Plus s q r \lor - q = succ s \land Plus p s r. - intros 2. elim q; clear q; intros; - [ lapply linear Plus_gen_zero_2 to H as H0. - rewrite > H0. clear H0 p - | clear H. - lapply linear Plus_gen_succ_2 to H1 as H0. - decompose. - lapply linear eq_gen_succ_succ to H1 as H0. - rewrite > H0. clear H0 r. - ]; apply ex_intro; [| auto || auto ]. (**) -qed. -*) -(* other simplification lemmas *) - -theorem Plus_gen_eq_2_3: \forall p,q. Plus p q q \to p = zero. - intros 2. elim q; clear q; intros; - [ lapply linear Plus_gen_zero_2 to H as H0. - rewrite > H0. clear H0 p - | lapply linear Plus_gen_succ_2 to H1 as H0. - decompose. - lapply linear eq_gen_succ_succ to H2 as H0. - rewrite < H0 in H3. clear H0 a - ]; auto. -qed. - -theorem Plus_gen_eq_1_3: \forall p,q. Plus p q p \to q = zero. - intros 1. elim p; clear p; intros; - [ lapply linear Plus_gen_zero_1 to H as H0. - rewrite > H0. clear H0 q - | lapply linear Plus_gen_succ_1 to H1 as H0. - decompose. - lapply linear eq_gen_succ_succ to H2 as H0. - rewrite < H0 in H3. clear H0 a - ]; auto. -qed. diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/Plus_props.ma b/matita/contribs/RELATIONAL-ARITHMETICS/Plus_props.ma deleted file mode 100644 index b2608397c..000000000 --- a/matita/contribs/RELATIONAL-ARITHMETICS/Plus_props.ma +++ /dev/null @@ -1,107 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICsucc/Plus_props". - -include "Plus_fwd.ma". - -theorem Plus_zero_1: \forall q. Plus zero q q. - intros. elim q; clear q; auto. -qed. - -theorem Plus_succ_1: \forall p,q,r. Plus p q r \to Plus (succ p) q (succ r). - intros 2. elim q; clear q; - [ lapply linear Plus_gen_zero_2 to H as H0. - rewrite > H0. clear H0 p - | lapply linear Plus_gen_succ_2 to H1 as H0. - decompose. - rewrite > H2. clear H2 r - ]; auto. -qed. - -theorem Plus_sym: \forall p,q,r. Plus p q r \to Plus q p r. - intros 2. elim q; clear q; - [ lapply linear Plus_gen_zero_2 to H as H0. - rewrite > H0. clear H0 p - | lapply linear Plus_gen_succ_2 to H1 as H0. - decompose. - rewrite > H2. clear H2 r - ]; auto. -qed. - -theorem Plus_shift_succ_sx: \forall p,q,r. - Plus p (succ q) r \to Plus (succ p) q r. - intros. - lapply linear Plus_gen_succ_2 to H as H0. - decompose. - rewrite > H1. clear H1 r. - auto. -qed. - -theorem Plus_shift_succ_dx: \forall p,q,r. - Plus (succ p) q r \to Plus p (succ q) r. - intros. - lapply linear Plus_gen_succ_1 to H as H0. - decompose. - rewrite > H1. clear H1 r. - auto. -qed. - -theorem Plus_trans_1: \forall p,q1,r1. Plus p q1 r1 \to - \forall q2,r2. Plus r1 q2 r2 \to - \exists q. Plus q1 q2 q \land Plus p q r2. - intros 2; elim q1; clear q1; intros; - [ lapply linear Plus_gen_zero_2 to H as H0. - rewrite > H0. clear H0 p - | lapply linear Plus_gen_succ_2 to H1 as H0. - decompose. - rewrite > H3. rewrite > H3 in H2. clear H3 r1. - lapply linear Plus_gen_succ_1 to H2 as H0. - decompose. - rewrite > H2. clear H2 r2. - lapply linear H to H4, H3 as H0. - decompose. - ]; apply ex_intro; [| auto || auto ]. (**) -qed. - -theorem Plus_trans_2: \forall p1,q,r1. Plus p1 q r1 \to - \forall p2,r2. Plus p2 r1 r2 \to - \exists p. Plus p1 p2 p \land Plus p q r2. - intros 2; elim q; clear q; intros; - [ lapply linear Plus_gen_zero_2 to H as H0. - rewrite > H0. clear H0 p1 - | lapply linear Plus_gen_succ_2 to H1 as H0. - decompose. - rewrite > H3. rewrite > H3 in H2. clear H3 r1. - lapply linear Plus_gen_succ_2 to H2 as H0. - decompose. - rewrite > H2. clear H2 r2. - lapply linear H to H4, H3 as H0. - decompose. - ]; apply ex_intro; [| auto || auto ]. (**) -qed. - -theorem Plus_conf: \forall p,q,r1. Plus p q r1 \to - \forall r2. Plus p q r2 \to r1 = r2. - intros 2. elim q; clear q; intros; - [ lapply linear Plus_gen_zero_2 to H as H0. - rewrite > H0 in H1. clear H0 p - | lapply linear Plus_gen_succ_2 to H1 as H0. - decompose. - rewrite > H3. clear H3 r1. - lapply linear Plus_gen_succ_2 to H2 as H0. - decompose. - rewrite > H2. clear H2 r2. - ]; auto. -qed.