From 28b6f4150bea6fc07c8cde8a94b097bde62ad457 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 20 Aug 2006 20:05:44 +0000 Subject: [PATCH] new naming --- .../{Plus.ma => NPlus.ma} | 8 +-- .../{Plus_fwd.ma => NPlus_fwd.ma} | 54 ++++++++-------- .../{Plus_props.ma => NPlus_props.ma} | 64 +++++++++---------- 3 files changed, 63 insertions(+), 63 deletions(-) rename helm/software/matita/contribs/RELATIONAL-ARITHMETICS/{Plus.ma => NPlus.ma} (82%) rename helm/software/matita/contribs/RELATIONAL-ARITHMETICS/{Plus_fwd.ma => NPlus_fwd.ma} (63%) rename helm/software/matita/contribs/RELATIONAL-ARITHMETICS/{Plus_props.ma => NPlus_props.ma} (55%) diff --git a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Plus.ma b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/NPlus.ma similarity index 82% rename from helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Plus.ma rename to helm/software/matita/contribs/RELATIONAL-ARITHMETICS/NPlus.ma index 5b86bf749..8531c766b 100644 --- a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Plus.ma +++ b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/NPlus.ma @@ -12,12 +12,12 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/Plus". +set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/NPlus". 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). +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/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Plus_fwd.ma b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/NPlus_fwd.ma similarity index 63% rename from helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Plus_fwd.ma rename to helm/software/matita/contribs/RELATIONAL-ARITHMETICS/NPlus_fwd.ma index 8f3e20a3c..bb73113e3 100644 --- a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Plus_fwd.ma +++ b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/NPlus_fwd.ma @@ -12,22 +12,22 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/Plus_fwd". +set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/NPlus_fwd". include "Nat_fwd.ma". -include "Plus.ma". +include "NPlus.ma". (* primitive generation lemmas proved by elimination and inversion *) -theorem Plus_gen_zero_1: \forall q,r. Plus zero q r \to q = r. +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 Plus_gen_succ_1: \forall p,q,r. Plus (succ p) q r \to - \exists s. r = (succ s) \land Plus p q s. +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. @@ -36,7 +36,7 @@ theorem Plus_gen_succ_1: \forall p,q,r. Plus (succ p) q r \to ]; apply ex_intro; [| auto || auto ]. (**) qed. -theorem Plus_gen_zero_2: \forall p,r. Plus p zero r \to p = r. +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. @@ -44,8 +44,8 @@ theorem Plus_gen_zero_2: \forall p,r. Plus p zero r \to p = r. ]. 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. +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. @@ -55,7 +55,7 @@ theorem Plus_gen_succ_2: \forall p,q,r. Plus p (succ q) r \to ]. qed. -theorem Plus_gen_zero_3: \forall p,q. Plus p q zero \to p = zero \land q = zero. +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 @@ -64,9 +64,9 @@ theorem Plus_gen_zero_3: \forall p,q. Plus p q zero \to p = zero \land q = zero. ]. 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. +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. @@ -75,28 +75,28 @@ theorem Plus_gen_succ_3: \forall p,q,r. Plus p q (succ r) \to ]; apply ex_intro; [| auto || auto ] (**) qed. (* -(* alternative proofs invoking Plus_gen_2 *) +(* alternative proofs invoking NPlus_gen_2 *) -variant Plus_gen_zero_3_alt: \forall p,q. Plus p q zero \to p = zero \land q = zero. +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 Plus_gen_zero_2 to H as H0. + [ lapply linear NPlus_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. + 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 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. +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 Plus_gen_zero_2 to H as H0. + [ lapply linear NPlus_gen_zero_2 to H as H0. rewrite > H0. clear H0 p | clear H. - lapply linear Plus_gen_succ_2 to H1 as H0. + 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. @@ -105,22 +105,22 @@ qed. *) (* other simplification lemmas *) -theorem Plus_gen_eq_2_3: \forall p,q. Plus p q q \to p = zero. +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 Plus_gen_zero_2 to H as H0. + [ lapply linear NPlus_gen_zero_2 to H as H0. rewrite > H0. clear H0 p - | lapply linear Plus_gen_succ_2 to H1 as H0. + | 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 Plus_gen_eq_1_3: \forall p,q. Plus p q p \to q = zero. +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 Plus_gen_zero_1 to H as H0. + [ lapply linear NPlus_gen_zero_1 to H as H0. rewrite > H0. clear H0 q - | lapply linear Plus_gen_succ_1 to H1 as H0. + | 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 diff --git a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Plus_props.ma b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/NPlus_props.ma similarity index 55% rename from helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Plus_props.ma rename to helm/software/matita/contribs/RELATIONAL-ARITHMETICS/NPlus_props.ma index b2608397c..de0de1b8a 100644 --- a/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/Plus_props.ma +++ b/helm/software/matita/contribs/RELATIONAL-ARITHMETICS/NPlus_props.ma @@ -12,62 +12,62 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICsucc/Plus_props". +set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/NPlus_props". -include "Plus_fwd.ma". +include "NPlus_fwd.ma". -theorem Plus_zero_1: \forall q. Plus zero q q. +theorem NPlus_zero_1: \forall q. NPlus 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). +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 Plus_gen_zero_2 to H as H0. + [ lapply linear NPlus_gen_zero_2 to H as H0. rewrite > H0. clear H0 p - | lapply linear Plus_gen_succ_2 to H1 as H0. + | lapply linear NPlus_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. +theorem NPlus_sym: \forall p,q,r. NPlus p q r \to NPlus q p r. intros 2. elim q; clear q; - [ lapply linear Plus_gen_zero_2 to H as H0. + [ lapply linear NPlus_gen_zero_2 to H as H0. rewrite > H0. clear H0 p - | lapply linear Plus_gen_succ_2 to H1 as H0. + | lapply linear NPlus_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. +theorem NPlus_shift_succ_sx: \forall p,q,r. + NPlus p (succ q) r \to NPlus (succ p) q r. intros. - lapply linear Plus_gen_succ_2 to H as H0. + lapply linear NPlus_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. +theorem NPlus_shift_succ_dx: \forall p,q,r. + NPlus (succ p) q r \to NPlus p (succ q) r. intros. - lapply linear Plus_gen_succ_1 to H as H0. + lapply linear NPlus_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. +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 Plus_gen_zero_2 to H as H0. + [ lapply linear NPlus_gen_zero_2 to H as H0. rewrite > H0. clear H0 p - | lapply linear Plus_gen_succ_2 to H1 as H0. + | lapply linear NPlus_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. + lapply linear NPlus_gen_succ_1 to H2 as H0. decompose. rewrite > H2. clear H2 r2. lapply linear H to H4, H3 as H0. @@ -75,16 +75,16 @@ theorem Plus_trans_1: \forall p,q1,r1. Plus p q1 r1 \to ]; 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. +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 Plus_gen_zero_2 to H as H0. + [ lapply linear NPlus_gen_zero_2 to H as H0. rewrite > H0. clear H0 p1 - | lapply linear Plus_gen_succ_2 to H1 as H0. + | lapply linear NPlus_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. + lapply linear NPlus_gen_succ_2 to H2 as H0. decompose. rewrite > H2. clear H2 r2. lapply linear H to H4, H3 as H0. @@ -92,15 +92,15 @@ theorem Plus_trans_2: \forall p1,q,r1. Plus p1 q r1 \to ]; 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. +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 Plus_gen_zero_2 to H as H0. + [ lapply linear NPlus_gen_zero_2 to H as H0. rewrite > H0 in H1. clear H0 p - | lapply linear Plus_gen_succ_2 to H1 as H0. + | lapply linear NPlus_gen_succ_2 to H1 as H0. decompose. rewrite > H3. clear H3 r1. - lapply linear Plus_gen_succ_2 to H2 as H0. + lapply linear NPlus_gen_succ_2 to H2 as H0. decompose. rewrite > H2. clear H2 r2. ]; auto. -- 2.39.2