From e02d5abb4dbe1f8da09eae51b5a1818fba8d9727 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 20 Aug 2006 12:19:55 +0000 Subject: [PATCH] new naming --- .../{nat_defs.ma => Nat.ma} | 8 +- .../{nat_fwd.ma => Nat_fwd.ma} | 10 +-- .../{add_defs.ma => Plus.ma} | 10 +-- .../{add_fwd.ma => Plus_fwd.ma} | 74 +++++++++---------- .../{add_props.ma => Plus_props.ma} | 62 ++++++++-------- 5 files changed, 83 insertions(+), 81 deletions(-) rename matita/contribs/RELATIONAL-ARITHMETICS/{nat_defs.ma => Nat.ma} (89%) rename matita/contribs/RELATIONAL-ARITHMETICS/{nat_fwd.ma => Nat_fwd.ma} (78%) rename matita/contribs/RELATIONAL-ARITHMETICS/{add_defs.ma => Plus.ma} (81%) rename matita/contribs/RELATIONAL-ARITHMETICS/{add_fwd.ma => Plus_fwd.ma} (53%) rename matita/contribs/RELATIONAL-ARITHMETICS/{add_props.ma => Plus_props.ma} (56%) diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/nat_defs.ma b/matita/contribs/RELATIONAL-ARITHMETICS/Nat.ma similarity index 89% rename from matita/contribs/RELATIONAL-ARITHMETICS/nat_defs.ma rename to matita/contribs/RELATIONAL-ARITHMETICS/Nat.ma index 30d6cfb5c..bc0624140 100644 --- a/matita/contribs/RELATIONAL-ARITHMETICS/nat_defs.ma +++ b/matita/contribs/RELATIONAL-ARITHMETICS/Nat.ma @@ -12,10 +12,10 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/nat_defs". +set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/Nat". include "logic/equality.ma". -inductive nat: Set \def - | O: nat - | S: nat \to nat. +inductive Nat: Set \def + | zero: Nat + | succ: Nat \to Nat. diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/nat_fwd.ma b/matita/contribs/RELATIONAL-ARITHMETICS/Nat_fwd.ma similarity index 78% rename from matita/contribs/RELATIONAL-ARITHMETICS/nat_fwd.ma rename to matita/contribs/RELATIONAL-ARITHMETICS/Nat_fwd.ma index 952a8cbf0..ede85286a 100644 --- a/matita/contribs/RELATIONAL-ARITHMETICS/nat_fwd.ma +++ b/matita/contribs/RELATIONAL-ARITHMETICS/Nat_fwd.ma @@ -12,18 +12,18 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/nat_fwd". +set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/Nat_fwd". -include "nat_defs.ma". +include "Nat.ma". -theorem eq_gen_O_S: \forall (P:Prop). \forall m2. O = S m2 \to P. +theorem eq_gen_zero_succ: \forall (P:Prop). \forall m2. zero = succ m2 \to P. intros. discriminate H. qed. -theorem eq_gen_S_O: \forall (P:Prop). \forall m1. S m1 = O \to P. +theorem eq_gen_succ_zero: \forall (P:Prop). \forall m1. succ m1 = zero \to P. intros. discriminate H. qed. -theorem eq_gen_S_S: \forall m1,m2. S m1 = S m2 \to m1 = m2. +theorem eq_gen_succ_succ: \forall m1,m2. succ m1 = succ m2 \to m1 = m2. intros. injection H. assumption. qed. diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/add_defs.ma b/matita/contribs/RELATIONAL-ARITHMETICS/Plus.ma similarity index 81% rename from matita/contribs/RELATIONAL-ARITHMETICS/add_defs.ma rename to matita/contribs/RELATIONAL-ARITHMETICS/Plus.ma index 77d6921a9..5d8f4f3ec 100644 --- a/matita/contribs/RELATIONAL-ARITHMETICS/add_defs.ma +++ b/matita/contribs/RELATIONAL-ARITHMETICS/Plus.ma @@ -12,10 +12,10 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/add_defs". +set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/Plus". -include "nat_defs.ma". +include "Nat.ma". -inductive add (p:nat): nat \to nat \to Prop \def - | add_O_2: add p O p - | add_S_2: \forall q, r. add p q r \to add p (S q) (S r). +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/add_fwd.ma b/matita/contribs/RELATIONAL-ARITHMETICS/Plus_fwd.ma similarity index 53% rename from matita/contribs/RELATIONAL-ARITHMETICS/add_fwd.ma rename to matita/contribs/RELATIONAL-ARITHMETICS/Plus_fwd.ma index c630d3dfe..8f3e20a3c 100644 --- a/matita/contribs/RELATIONAL-ARITHMETICS/add_fwd.ma +++ b/matita/contribs/RELATIONAL-ARITHMETICS/Plus_fwd.ma @@ -12,22 +12,22 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/add_fwd". +set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/Plus_fwd". -include "nat_fwd.ma". -include "add_defs.ma". +include "Nat_fwd.ma". +include "Plus.ma". (* primitive generation lemmas proved by elimination and inversion *) -theorem add_gen_O_1: \forall q,r. add O q r \to q = r. +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 add_gen_S_1: \forall p,q,r. add (S p) q r \to - \exists s. r = (S s) \land add p q s. +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. @@ -36,93 +36,93 @@ theorem add_gen_S_1: \forall p,q,r. add (S p) q r \to ]; apply ex_intro; [| auto || auto ]. (**) qed. -theorem add_gen_O_2: \forall p,r. add p O r \to p = r. +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_O_S to H2 as H0. apply H0 + lapply eq_gen_zero_succ to H2 as H0. apply H0 ]. qed. -theorem add_gen_S_2: \forall p,q,r. add p (S q) r \to - \exists s. r = (S s) \land add p q s. +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_S_O to H as H0. apply H0 + [ lapply eq_gen_succ_zero to H as H0. apply H0 | clear H1 H3 r. - lapply linear eq_gen_S_S to H2 as H0. + lapply linear eq_gen_succ_succ to H2 as H0. rewrite > H0. clear H0 q. apply ex_intro; [| auto ] (**) ]. qed. -theorem add_gen_O_3: \forall p,q. add p q O \to p = O \land q = O. +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_O_S to H3 as H0. apply H0 + lapply eq_gen_zero_succ to H3 as H0. apply H0 ]. qed. -theorem add_gen_S_3: \forall p,q,r. add p q (S r) \to - \exists s. p = S s \land add s q r \lor - q = S s \land add p s r. +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_S_S to H3 as H0. + lapply linear eq_gen_succ_succ to H3 as H0. rewrite > H0. clear H0 r. ]; apply ex_intro; [| auto || auto ] (**) qed. (* -(* alternative proofs invoking add_gen_2 *) +(* alternative proofs invoking Plus_gen_2 *) -variant add_gen_O_3_alt: \forall p,q. add p q O \to p = O \land q = O. +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 add_gen_O_2 to H as H0. + [ lapply linear Plus_gen_zero_2 to H as H0. rewrite > H0. clear H0 p. auto | clear H. - lapply linear add_gen_S_2 to H1 as H0. + lapply linear Plus_gen_succ_2 to H1 as H0. decompose. - lapply linear eq_gen_O_S to H1 as H0. apply H0 + lapply linear eq_gen_zero_succ to H1 as H0. apply H0 ]. qed. -variant add_gen_S_3_alt: \forall p,q,r. add p q (S r) \to - \exists s. p = S s \land add s q r \lor - q = S s \land add p s r. +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 add_gen_O_2 to H as H0. + [ lapply linear Plus_gen_zero_2 to H as H0. rewrite > H0. clear H0 p | clear H. - lapply linear add_gen_S_2 to H1 as H0. + lapply linear Plus_gen_succ_2 to H1 as H0. decompose. - lapply linear eq_gen_S_S to H1 as H0. + 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 add_gen_eq_2_3: \forall p,q. add p q q \to p = O. +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 add_gen_O_2 to H as H0. + [ lapply linear Plus_gen_zero_2 to H as H0. rewrite > H0. clear H0 p - | lapply linear add_gen_S_2 to H1 as H0. + | lapply linear Plus_gen_succ_2 to H1 as H0. decompose. - lapply linear eq_gen_S_S to H2 as H0. + lapply linear eq_gen_succ_succ to H2 as H0. rewrite < H0 in H3. clear H0 a ]; auto. qed. -theorem add_gen_eq_1_3: \forall p,q. add p q p \to q = O. +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 add_gen_O_1 to H as H0. + [ lapply linear Plus_gen_zero_1 to H as H0. rewrite > H0. clear H0 q - | lapply linear add_gen_S_1 to H1 as H0. + | lapply linear Plus_gen_succ_1 to H1 as H0. decompose. - lapply linear eq_gen_S_S to H2 as H0. + 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/add_props.ma b/matita/contribs/RELATIONAL-ARITHMETICS/Plus_props.ma similarity index 56% rename from matita/contribs/RELATIONAL-ARITHMETICS/add_props.ma rename to matita/contribs/RELATIONAL-ARITHMETICS/Plus_props.ma index dd360676b..b2608397c 100644 --- a/matita/contribs/RELATIONAL-ARITHMETICS/add_props.ma +++ b/matita/contribs/RELATIONAL-ARITHMETICS/Plus_props.ma @@ -12,60 +12,62 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/add_props". +set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICsucc/Plus_props". -include "add_fwd.ma". +include "Plus_fwd.ma". -theorem add_O_1: \forall q. add O q q. +theorem Plus_zero_1: \forall q. Plus zero q q. intros. elim q; clear q; auto. qed. -theorem add_S_1: \forall p,q,r. add p q r \to add (S p) q (S r). +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 add_gen_O_2 to H as H0. + [ lapply linear Plus_gen_zero_2 to H as H0. rewrite > H0. clear H0 p - | lapply linear add_gen_S_2 to H1 as H0. + | lapply linear Plus_gen_succ_2 to H1 as H0. decompose. rewrite > H2. clear H2 r ]; auto. qed. -theorem add_sym: \forall p,q,r. add p q r \to add q p r. +theorem Plus_sym: \forall p,q,r. Plus p q r \to Plus q p r. intros 2. elim q; clear q; - [ lapply linear add_gen_O_2 to H as H0. + [ lapply linear Plus_gen_zero_2 to H as H0. rewrite > H0. clear H0 p - | lapply linear add_gen_S_2 to H1 as H0. + | lapply linear Plus_gen_succ_2 to H1 as H0. decompose. rewrite > H2. clear H2 r ]; auto. qed. -theorem add_shift_S_sx: \forall p,q,r. add p (S q) r \to add (S p) q r. +theorem Plus_shift_succ_sx: \forall p,q,r. + Plus p (succ q) r \to Plus (succ p) q r. intros. - lapply linear add_gen_S_2 to H as H0. + lapply linear Plus_gen_succ_2 to H as H0. decompose. rewrite > H1. clear H1 r. auto. qed. -theorem add_shift_S_dx: \forall p,q,r. add (S p) q r \to add p (S q) r. +theorem Plus_shift_succ_dx: \forall p,q,r. + Plus (succ p) q r \to Plus p (succ q) r. intros. - lapply linear add_gen_S_1 to H as H0. + lapply linear Plus_gen_succ_1 to H as H0. decompose. rewrite > H1. clear H1 r. auto. qed. -theorem add_trans_1: \forall p,q1,r1. add p q1 r1 \to - \forall q2,r2. add r1 q2 r2 \to - \exists q. add q1 q2 q \land add p q r2. +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 add_gen_O_2 to H as H0. + [ lapply linear Plus_gen_zero_2 to H as H0. rewrite > H0. clear H0 p - | lapply linear add_gen_S_2 to H1 as H0. + | lapply linear Plus_gen_succ_2 to H1 as H0. decompose. rewrite > H3. rewrite > H3 in H2. clear H3 r1. - lapply linear add_gen_S_1 to H2 as H0. + lapply linear Plus_gen_succ_1 to H2 as H0. decompose. rewrite > H2. clear H2 r2. lapply linear H to H4, H3 as H0. @@ -73,16 +75,16 @@ theorem add_trans_1: \forall p,q1,r1. add p q1 r1 \to ]; apply ex_intro; [| auto || auto ]. (**) qed. -theorem add_trans_2: \forall p1,q,r1. add p1 q r1 \to - \forall p2,r2. add p2 r1 r2 \to - \exists p. add p1 p2 p \land add p q r2. +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 add_gen_O_2 to H as H0. + [ lapply linear Plus_gen_zero_2 to H as H0. rewrite > H0. clear H0 p1 - | lapply linear add_gen_S_2 to H1 as H0. + | lapply linear Plus_gen_succ_2 to H1 as H0. decompose. rewrite > H3. rewrite > H3 in H2. clear H3 r1. - lapply linear add_gen_S_2 to H2 as H0. + lapply linear Plus_gen_succ_2 to H2 as H0. decompose. rewrite > H2. clear H2 r2. lapply linear H to H4, H3 as H0. @@ -90,15 +92,15 @@ theorem add_trans_2: \forall p1,q,r1. add p1 q r1 \to ]; apply ex_intro; [| auto || auto ]. (**) qed. -theorem add_conf: \forall p,q,r1. add p q r1 \to - \forall r2. add p q r2 \to r1 = r2. +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 add_gen_O_2 to H as H0. + [ lapply linear Plus_gen_zero_2 to H as H0. rewrite > H0 in H1. clear H0 p - | lapply linear add_gen_S_2 to H1 as H0. + | lapply linear Plus_gen_succ_2 to H1 as H0. decompose. rewrite > H3. clear H3 r1. - lapply linear add_gen_S_2 to H2 as H0. + lapply linear Plus_gen_succ_2 to H2 as H0. decompose. rewrite > H2. clear H2 r2. ]; auto. -- 2.39.2