From b7503f874120f581c9679deabe45bd3c333f1b0c Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 19 Feb 2007 14:11:14 +0000 Subject: [PATCH] Unified-Sub: lift_comm completed --- .../LAMBDA-TYPES/Unified-Sub/Lift/defs.ma | 6 +- .../LAMBDA-TYPES/Unified-Sub/Lift/fun.ma | 20 ++- .../LAMBDA-TYPES/Unified-Sub/Lift/inv.ma | 70 ++++++---- .../LAMBDA-TYPES/Unified-Sub/Lift/props.ma | 126 ++++++------------ .../Unified-Sub/datatypes/Term.ma | 9 +- .../matita/contribs/RELATIONAL/NLE/inv.ma | 4 +- .../matita/contribs/RELATIONAL/NLE/props.ma | 2 +- .../matita/contribs/RELATIONAL/NPlus/fun.ma | 8 +- .../matita/contribs/RELATIONAL/NPlus/inv.ma | 121 ++++++----------- .../contribs/RELATIONAL/NPlus/monoid.ma | 44 ++++-- 10 files changed, 184 insertions(+), 226 deletions(-) diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma index d8ee64fe5..b8a4e2a85 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma @@ -22,12 +22,12 @@ include "datatypes/Term.ma". inductive Lift (l: Nat): Nat \to Term \to Term \to Prop \def | lift_sort : \forall i,h. - Lift l i (leaf (sort h)) (leaf (sort h)) + Lift l i (sort h) (sort h) | lift_lref_gt: \forall i,j. i > j \to - Lift l i (leaf (lref j)) (leaf (lref j)) + Lift l i (lref j) (lref j) | lift_lref_le: \forall i,j1. i <= j1 \to \forall j2. (l + j1 == j2) \to - Lift l i (leaf (lref j1)) (leaf (lref j2)) + Lift l i (lref j1) (lref j2) | lift_bind : \forall i,u1,u2. Lift l i u1 u2 \to \forall t1,t2. Lift l (succ i) t1 t2 \to \forall r. Lift l i (intb r u1 t1) (intb r u2 t2) diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fun.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fun.ma index fd794fe9b..cfddffd3d 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fun.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fun.ma @@ -17,18 +17,26 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/fun". include "Lift/inv.ma". (* Functional properties ****************************************************) -(* + theorem lift_total: \forall l, t, i. \exists u. Lift l i t u. intros 2. elim t; clear t; - [ -*) + [ auto + | lapply (nle_gt_or_le n i). decompose; + [ auto + | lapply (nplus_total l n). decompose. auto + ] + | lapply (H i1). lapply (H1 (succ i1)). decompose. auto + | lapply (H i1). lapply (H1 i1). decompose. auto + ]. +qed. + theorem lift_mono: \forall l,i,t,t1. Lift l i t t1 \to \forall t2. Lift l i t t2 \to t1 = t2. intros 5. elim H; clear H i t t1; [ lapply linear lift_inv_sort_1 to H1 | lapply linear lift_inv_lref_1_gt to H2, H1 - | lapply linear lift_inv_lref_1_le to H3, H1, H2 + | lapply linear lift_inv_lref_1_le_nplus to H3, H1, H2 | lapply linear lift_inv_bind_1 to H5. decompose | lapply linear lift_inv_flat_1 to H5. decompose ]; subst; auto. @@ -40,9 +48,9 @@ theorem lift_inj: \forall l,i,t1,t. Lift l i t1 t \to intros 5. elim H; clear H i t1 t; [ lapply linear lift_inv_sort_2 to H1 | lapply linear lift_inv_lref_2_gt to H2, H1 - | lapply nle_nplus to H2 as H. (**) + | lapply nle_nplus to H2 as H. lapply linear nle_trans to H1, H as H0. - lapply lift_inv_lref_2_le to H3, H0, H2 + lapply lift_inv_lref_2_le_nplus to H3, H0, H2 | lapply linear lift_inv_bind_2 to H5. decompose | lapply linear lift_inv_flat_2 to H5. decompose ]; subst; auto. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma index d664e5f07..a4b218f44 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma @@ -19,8 +19,8 @@ include "Lift/defs.ma". (* Inversion properties *****************************************************) theorem lift_inv_sort_1: \forall l, i, h, x. - Lift l i (leaf (sort h)) x \to - x = leaf (sort h). + Lift l i (sort h) x \to + x = sort h. intros. inversion H; clear H; intros; [ auto | destruct H2 @@ -31,10 +31,10 @@ theorem lift_inv_sort_1: \forall l, i, h, x. qed. theorem lift_inv_lref_1: \forall l, i, j1, x. - Lift l i (leaf (lref j1)) x \to - (i > j1 \land x = leaf (lref j1)) \lor + Lift l i (lref j1) x \to + (i > j1 \land x = lref j1) \lor (i <= j1 \land - \exists j2. (l + j1 == j2) \land x = leaf (lref j2) + \exists j2. (l + j1 == j2) \land x = lref j2 ). intros. inversion H; clear H; intros; [ destruct H1 @@ -76,8 +76,8 @@ theorem lift_inv_flat_1: \forall l, i, r, u1, t1, x. qed. theorem lift_inv_sort_2: \forall l, i, x, h. - Lift l i x (leaf (sort h)) \to - x = leaf (sort h). + Lift l i x (sort h) \to + x = sort h. intros. inversion H; clear H; intros; [ auto | destruct H3 @@ -88,10 +88,10 @@ theorem lift_inv_sort_2: \forall l, i, x, h. qed. theorem lift_inv_lref_2: \forall l, i, x, j2. - Lift l i x (leaf (lref j2)) \to - (i > j2 \land x = leaf (lref j2)) \lor + Lift l i x (lref j2) \to + (i > j2 \land x = lref j2) \lor (i <= j2 \land - \exists j1. (l + j1 == j2) \land x = leaf (lref j1) + \exists j1. (l + j1 == j2) \land x = lref j1 ). intros. inversion H; clear H; intros; [ destruct H2 @@ -135,20 +135,30 @@ qed. (* Corollaries of inversion properties ***************************************) theorem lift_inv_lref_1_gt: \forall l, i, j1, x. - Lift l i (leaf (lref j1)) x \to - i > j1 \to x = leaf (lref j1). - intros 5. + Lift l i (lref j1) x \to + i > j1 \to x = lref j1. + intros. lapply linear lift_inv_lref_1 to H. decompose; subst; [ auto | lapply linear nle_false to H2, H1. decompose ]. - qed. +qed. theorem lift_inv_lref_1_le: \forall l, i, j1, x. - Lift l i (leaf (lref j1)) x \to - i <= j1 \to \forall j2. (l + j1 == j2) \to - x = leaf (lref j2). - intros 5. + Lift l i (lref j1) x \to i <= j1 \to + \exists j2. (l + j1 == j2) \land x = lref j2. + intros. + lapply linear lift_inv_lref_1 to H. decompose; subst; + [ lapply linear nle_false to H1, H2. decompose + | auto + ]. +qed. + +theorem lift_inv_lref_1_le_nplus: \forall l, i, j1, x. + Lift l i (lref j1) x \to + i <= j1 \to \forall j2. (l + j1 == j2) \to + x = lref j2. + intros. lapply linear lift_inv_lref_1 to H. decompose; subst; [ lapply linear nle_false to H1, H3. decompose | lapply linear nplus_mono to H2, H4. subst. auto @@ -156,9 +166,9 @@ theorem lift_inv_lref_1_le: \forall l, i, j1, x. qed. theorem lift_inv_lref_2_gt: \forall l, i, x, j2. - Lift l i x (leaf (lref j2)) \to - i > j2 \to x = leaf (lref j2). - intros 5. + Lift l i x (lref j2) \to + i > j2 \to x = lref j2. + intros. lapply linear lift_inv_lref_2 to H. decompose; subst; [ auto | lapply linear nle_false to H2, H1. decompose @@ -166,10 +176,20 @@ theorem lift_inv_lref_2_gt: \forall l, i, x, j2. qed. theorem lift_inv_lref_2_le: \forall l, i, x, j2. - Lift l i x (leaf (lref j2)) \to - i <= j2 \to \forall j1. (l + j1 == j2) \to - x = leaf (lref j1). - intros 5. + Lift l i x (lref j2) \to i <= j2 \to + \exists j1. (l + j1 == j2) \land x = lref j1. + intros. + lapply linear lift_inv_lref_2 to H. decompose; subst; + [ lapply linear nle_false to H1, H2. decompose + | auto + ]. +qed. + +theorem lift_inv_lref_2_le_nplus: \forall l, i, x, j2. + Lift l i x (lref j2) \to + i <= j2 \to \forall j1. (l + j1 == j2) \to + x = lref j1. + intros. lapply linear lift_inv_lref_2 to H. decompose; subst; [ lapply linear nle_false to H1, H3. decompose | lapply linear nplus_inj_2 to H2, H4. subst. auto diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma index a5c566dab..34964a5b1 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma @@ -16,108 +16,64 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/props". include "Lift/fun.ma". -theorem lift_comp_ge_1: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to - \forall l2,i2,u1. Lift l2 i2 t1 u1 \to - \forall u2. Lift l2 i2 t2 u2 \to - i1 >= i2 \to \forall i. (l2 + i1 == i) \to - Lift l1 i u1 u2. +(* NOTE: this holds because of nplus_comm_1 *) +theorem lift_comp: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to + \forall l2,i2,u1. Lift l2 i2 t1 u1 \to + \forall x. Lift l2 i2 t2 x \to + \forall i,y. Lift l1 i u1 y \to + i1 >= i2 \to (l2 + i1 == i) \to x = y. intros 5. elim H; clear H i1 t1 t2; - [ lapply lift_conf to H1, H2. clear H2. subst. - lapply linear lift_inv_sort_1 to H1. - subst. auto - | lapply lift_conf to H2, H3. clear H3. subst. + [ lapply lift_mono to H1, H2. clear H2. subst. + lapply linear lift_inv_sort_1 to H1. subst. + lapply linear lift_inv_sort_1 to H3. subst. auto + | lapply lift_mono to H2, H3. clear H3. subst. lapply linear lift_inv_lref_1 to H2. - decompose; subst; clear H2 H4 i2; - [ lapply linear nle_nplus to H5 as H0. clear l2. (**) - lapply linear nle_trans to H1, H0. - auto - | lapply nle_nplus_comp_lt_2 to H3, H5; auto. - ] - | lapply linear lift_inv_lref_1 to H3. - decompose; subst; - [ clear H2 H4 H6 n3 l2. - lapply linear nle_trans to H3, H5 as H0. - lapply linear nle_false to H1, H0. decompose - | lapply linear lift_inv_lref_1 to H4. - decompose; subst; - [ clear H1 H5 H6 H7 n1. - lapply linear nle_nplus to H2 as H0. (**) - lapply linear nle_trans to H3, H0 as H2. - lapply linear nle_false to H2, H4. decompose - | clear H3 H4 H5. - lapply nle_nplus_comp to H6, H7; auto. - ] - ] + decompose; subst; clear H2 H5; + lapply linear lift_inv_lref_1_gt to H4; subst; auto width = 4 + | lapply lift_inv_lref_1_le to H3; [ 2: auto ]. clear H3. + lapply lift_inv_lref_1_le to H4; [ 2: auto ]. clear H4. + decompose. subst. clear H6 i2. + lapply lift_inv_lref_1_le to H5; [ 2: auto depth = 4 width = 4 ]. + decompose. subst. clear H5 H1 H7 i. auto depth = 4 | clear H1 H3. lapply linear lift_inv_bind_1 to H5. - lapply linear lift_inv_bind_1 to H6. - decompose. subst. auto width = 4 + lapply linear lift_inv_bind_1 to H6. decompose. subst. + lapply linear lift_inv_bind_1 to H7. decompose. subst. + auto width = 5 | clear H1 H3. lapply linear lift_inv_flat_1 to H5. - lapply linear lift_inv_flat_1 to H6. - decompose. subst. auto width = 4 + lapply linear lift_inv_flat_1 to H6. decompose. subst. + lapply linear lift_inv_flat_1 to H7. decompose. subst. + auto width = 5 ]. qed. -theorem lift_comp_ge_2: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to - \forall l2,i2,u1. Lift l2 i2 t1 u1 \to - \forall i,u2. Lift l2 i t2 u2 \to - i2 >= i1 \to (l1 + i2 == i) \to - Lift l1 i1 u1 u2. - intros 5. elim H; clear H i1 t1 t2; - [ lapply linear lift_inv_sort_1 to H1. - lapply linear lift_inv_sort_1 to H2. - subst. auto - | lapply linear lift_inv_lref_1 to H2. - lapply linear lift_inv_lref_1 to H3. - decompose; subst; (* clear H2 H4 i2; *) - [ clear H H3 H4 H5. auto - | clear H1 H4 H7. - lapply linear nle_nplus to H5 as H0. (**) - lapply linear nle_trans to H3, H0 as H2. - lapply nle_false to H, H2. decompose - | clear H H5 H6. - lapply linear nle_trans to H4, H3 as H. - lapply nle_false to H, H1. decompose - | clear H H2 H5 H7. - lapply linear nle_trans to H4, H3 as H. - lapply nle_false to H, H1. decompose - ] -(* - | lapply linear lift_inv_lref_1 to H3. - decompose; subst; - [ clear H2 H4 H6 n3 l2. - lapply linear nle_trans to H3, H5 as H0. - lapply linear nle_false to H1, H0. decompose - | lapply linear lift_inv_lref_1 to H4. - decompose; subst; - [ clear H1 H5 H6 H7 n1. - lapply linear nle_nplus to H2 as H0. (**) - lapply linear nle_trans to H3, H0 as H2. - lapply linear nle_false to H2, H4. decompose - | clear H3 H4 H5. - lapply nle_nplus_comp to H6, H7; auto. - ] - ] - | clear H1 H3. - lapply linear lift_inv_bind_1 to H5. - lapply linear lift_inv_bind_1 to H6. - decompose. subst. auto width = 4 - | clear H1 H3. - lapply linear lift_inv_flat_1 to H5. - lapply linear lift_inv_flat_1 to H6. - decompose. subst. auto width = 4 - ]. +theorem lift_comp_rew_dx: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to + \forall l2,i2,u1. Lift l2 i2 t1 u1 \to + \forall u2. Lift l2 i2 t2 u2 \to + i1 >= i2 \to \forall i. (l2 + i1 == i) \to + Lift l1 i u1 u2. + intros. + lapply (lift_total l1 u1 i). decompose. + lapply lift_comp to H, H1, H2, H5, H3, H4. subst. auto. qed. - +theorem lift_comp_rew_sx: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to + \forall l2,i2,u1. Lift l2 i2 t1 u1 \to + \forall i,u2. Lift l2 i t2 u2 \to + i2 >= i1 \to (l1 + i2 == i) \to + Lift l1 i1 u1 u2. + intros. + lapply (lift_total l1 u1 i1). decompose. + lapply lift_comp to H1, H, H5, H2, H3, H4. subst. auto. +qed. (* theorem lift_trans_le: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to \forall l2,i2,z. Lift l2 i2 t2 t3 \to i1 <= i2 \to \forall i. \to i2 <= i \to (l1 + i1 == i) \to \forall l. (l1 + l2 == l) \to Lift l i1 t1 t3. -*) + axiom lift_conf_back_ge: \forall l1,i1,u1,u2. Lift l1 i1 u1 u2 \to \forall l2,i,t2. Lift l2 i t2 u2 \to \forall i2. i2 >= i1 \to (l1 + i2 == i) \to diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Term.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Term.ma index ba37390d9..8c2fb6ec6 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Term.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Term.ma @@ -18,7 +18,6 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/datatypes/Term". - Naming policy: - natural numbers : sorts h k, local references i j, lengths l o - boolean values : p q - - generic leaf items : m n - generic binding items: r s - generic flat items : r s - generic head items : m n @@ -27,11 +26,6 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/datatypes/Term". include "preamble.ma". -inductive Leaf: Set \def - | sort: Nat \to Leaf - | lref: Nat \to Leaf -. - inductive Bind: Set \def | abbr: Bind | abst: Bind @@ -52,7 +46,8 @@ inductive IntF: Set \def . inductive Term: Set \def - | leaf: Leaf \to Term + | sort: Nat \to Term + | lref: Nat \to Term | intb: IntB \to Term \to Term \to Term | intf: IntF \to Term \to Term \to Term . diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/inv.ma b/helm/software/matita/contribs/RELATIONAL/NLE/inv.ma index e42eecde3..67a18d820 100644 --- a/helm/software/matita/contribs/RELATIONAL/NLE/inv.ma +++ b/helm/software/matita/contribs/RELATIONAL/NLE/inv.ma @@ -18,9 +18,9 @@ include "NPlus/inv.ma". include "NLE/defs.ma". theorem nle_inv_succ_1: \forall x,y. x < y \to - \exists z. y = succ z \land x <= z. + \exists z. y = succ z \land x <= z. intros. elim H. - lapply linear nplus_gen_succ_2 to H1. + lapply linear nplus_inv_succ_2 to H1. decompose. subst. auto depth = 4. qed. diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/props.ma b/helm/software/matita/contribs/RELATIONAL/NLE/props.ma index eccc2f9db..a6d0ca7a8 100644 --- a/helm/software/matita/contribs/RELATIONAL/NLE/props.ma +++ b/helm/software/matita/contribs/RELATIONAL/NLE/props.ma @@ -65,7 +65,7 @@ theorem nle_lt_or_eq: \forall y,x. x <= y \to x < y \lor x = y. ]. qed. -theorem nat_dec_lt_ge: \forall x,y. x < y \lor y <= x. +theorem nle_gt_or_le: \forall x,y. y > x \lor y <= x. intros 2; elim y; clear y; [ auto | decompose; diff --git a/helm/software/matita/contribs/RELATIONAL/NPlus/fun.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/fun.ma index d2d686c51..4b31c570f 100644 --- a/helm/software/matita/contribs/RELATIONAL/NPlus/fun.ma +++ b/helm/software/matita/contribs/RELATIONAL/NPlus/fun.ma @@ -26,15 +26,15 @@ qed. theorem nplus_mono: \forall p,q,r1. (p + q == r1) \to \forall r2. (p + q == r2) \to r1 = r2. intros 4. elim H; clear H q r1; - [ lapply linear nplus_gen_zero_2 to H1 - | lapply linear nplus_gen_succ_2 to H3. decompose + [ lapply linear nplus_inv_zero_2 to H1 + | lapply linear nplus_inv_succ_2 to H3. decompose ]; subst; auto. qed. theorem nplus_inj_1: \forall p1, q, r. (p1 + q == r) \to \forall p2. (p2 + q == r) \to p2 = p1. intros 4. elim H; clear H q r; - [ lapply linear nplus_gen_zero_2 to H1 - | lapply linear nplus_gen_succ_2_3 to H3 + [ lapply linear nplus_inv_zero_2 to H1 + | lapply linear nplus_inv_succ_2_3 to H3 ]; auto. qed. diff --git a/helm/software/matita/contribs/RELATIONAL/NPlus/inv.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/inv.ma index 68043c84a..99bf3a9ee 100644 --- a/helm/software/matita/contribs/RELATIONAL/NPlus/inv.ma +++ b/helm/software/matita/contribs/RELATIONAL/NPlus/inv.ma @@ -16,119 +16,78 @@ set "baseuri" "cic:/matita/RELATIONAL/NPlus/inv". include "NPlus/defs.ma". -(* primitive generation lemmas proved by elimination and inversion *) +(* Inversion lemmas *********************************************************) -theorem nplus_gen_zero_1: \forall q,r. (zero + q == r) \to q = r. - intros. elim H; clear H q r; intros; - [ reflexivity - | clear H1. auto new timeout=30 - ]. +theorem nplus_inv_zero_1: \forall q,r. (zero + q == r) \to q = r. + intros. elim H; clear H q r; auto. qed. -theorem nplus_gen_succ_1: \forall p,q,r. ((succ p) + q == r) \to +theorem nplus_inv_succ_1: \forall p,q,r. ((succ p) + q == r) \to \exists s. r = (succ s) \land p + q == s. intros. elim H; clear H q r; intros; - [ - | clear H1. - decompose. - subst. - ]; apply ex_intro; [| auto new timeout=30 || auto new timeout=30 ]. (**) + [ auto depth = 4 + | clear H1. decompose. subst. auto depth = 4 + ] qed. -theorem nplus_gen_zero_2: \forall p,r. (p + zero == r) \to p = r. +theorem nplus_inv_zero_2: \forall p,r. (p + zero == r) \to p = r. intros. inversion H; clear H; intros; - [ auto new timeout=30 - | clear H H1. - destruct H2. + [ auto. + | clear H H1. destruct H2. ]. qed. -theorem nplus_gen_succ_2: \forall p,q,r. (p + (succ q) == r) \to +theorem nplus_inv_succ_2: \forall p,q,r. (p + (succ q) == r) \to \exists s. r = (succ s) \land p + q == s. intros. inversion H; clear H; intros; [ destruct H. - | clear H1 H3 r. - destruct H2; clear H2. - subst. - apply ex_intro; [| auto new timeout=30 ] (**) + | clear H1 H3 r. destruct H2; clear H2. subst. auto depth = 4. ]. qed. -theorem nplus_gen_zero_3: \forall p,q. (p + q == zero) \to +theorem nplus_inv_zero_3: \forall p,q. (p + q == zero) \to p = zero \land q = zero. intros. inversion H; clear H; intros; - [ subst. auto new timeout=30 - | clear H H1. - destruct H3. + [ subst. auto + | clear H H1. destruct H3. ]. qed. -theorem nplus_gen_succ_3: \forall p,q,r. (p + q == (succ r)) \to +theorem nplus_inv_succ_3: \forall p,q,r. (p + q == (succ r)) \to \exists s. p = succ s \land (s + q == r) \lor q = succ s \land p + s == r. intros. inversion H; clear H; intros; - [ subst. - | clear H1. - destruct H3. clear H3. - subst. - ]; apply ex_intro; [| auto new timeout=30 || auto new timeout=30 ] (**) + [ subst + | clear H1. destruct H3. clear H3. subst. + ]; auto depth = 4. qed. -(* -(* alternative proofs invoking nplus_gen_2 *) -variant nplus_gen_zero_3_alt: \forall p,q. (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. - subst. auto new timeout=30 - | 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. +(* Corollaries to inversion lemmas ******************************************) -variant nplus_gen_succ_3_alt: \forall p,q,r. (p + q == (succ r)) \to - \exists s. p = succ s \land (s + q == r) \lor - q = succ s \land p + s == r. - intros 2. elim q; clear q; intros; - [ lapply linear nplus_gen_zero_2 to H as H0. - subst - | clear H. - lapply linear nplus_gen_succ_2 to H1 as H0. - decompose. - lapply linear eq_gen_succ_succ to H1 as H0. - subst - ]; apply ex_intro; [| auto new timeout=30 || auto new timeout=30 ]. (**) +theorem nplus_inv_succ_2_3: \forall p,q,r. + (p + (succ q) == (succ r)) \to p + q == r. + intros. + lapply linear nplus_inv_succ_2 to H. decompose. subst. + destruct H1. clear H1. subst. auto. qed. -*) -(* other simplification lemmas *) -theorem nplus_gen_eq_2_3: \forall p,q. (p + q == q) \to p = zero. - intros 2. elim q; clear q; intros; - [ lapply linear nplus_gen_zero_2 to H as H0. - subst - | lapply linear nplus_gen_succ_2 to H1 as H0. - decompose. - destruct H2. clear H2. - subst - ]; auto new timeout=30. +theorem nplus_inv_succ_1_3: \forall p,q,r. + ((succ p) + q == (succ r)) \to p + q == r. + intros. + lapply linear nplus_inv_succ_1 to H. decompose. subst. + destruct H1. clear H1. subst. auto. qed. -theorem nplus_gen_eq_1_3: \forall p,q. (p + q == p) \to q = zero. - intros 1. elim p; clear p; intros; - [ lapply linear nplus_gen_zero_1 to H as H0. - subst - | lapply linear nplus_gen_succ_1 to H1 as H0. - decompose. - destruct H2. clear H2. - subst - ]; auto new timeout=30. +theorem nplus_inv_eq_2_3: \forall p,q. (p + q == q) \to p = zero. + intros 2. elim q; clear q; + [ lapply linear nplus_inv_zero_2 to H + | lapply linear nplus_inv_succ_2_3 to H1 + ]; auto. qed. -theorem nplus_gen_succ_2_3: \forall p,q,r. - (p + (succ q) == (succ r)) \to p + q == r. - intros. - lapply linear nplus_gen_succ_2 to H. decompose. subst. - destruct H1. clear H1. subst. auto. +theorem nplus_inv_eq_1_3: \forall p,q. (p + q == p) \to q = zero. + intros 1. elim p; clear p; + [ lapply linear nplus_inv_zero_1 to H + | lapply linear nplus_inv_succ_1_3 to H1. + ]; auto. qed. diff --git a/helm/software/matita/contribs/RELATIONAL/NPlus/monoid.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/monoid.ma index 804485e54..a7d56eeb3 100644 --- a/helm/software/matita/contribs/RELATIONAL/NPlus/monoid.ma +++ b/helm/software/matita/contribs/RELATIONAL/NPlus/monoid.ma @@ -27,6 +27,14 @@ theorem nplus_succ_1: \forall p,q,r. NPlus p q r \to intros. elim H; clear H q r; auto. qed. +theorem nplus_comm: \forall p, q, x. (p + q == x) \to + \forall y. (q + p == y) \to x = y. + intros 4; elim H; clear H q x; + [ lapply linear nplus_inv_zero_1 to H1 + | lapply linear nplus_inv_succ_1 to H3. decompose + ]; subst; auto. +qed. + theorem nplus_comm_rew: \forall p,q,r. (p + q == r) \to q + p == r. intros. elim H; clear H q r; auto. qed. @@ -40,13 +48,26 @@ qed. (* Corollaries of nonoidal properties ***************************************) +theorem nplus_comm_1: \forall p1, q, r1. (p1 + q == r1) \to + \forall p2, r2. (p2 + q == r2) \to + \forall x. (p2 + r1 == x) \to + \forall y. (p1 + r2 == y) \to + x = y. + intros 4. elim H; clear H q r1; + [ lapply linear nplus_inv_zero_2 to H1 + | lapply linear nplus_inv_succ_2 to H3. + lapply linear nplus_inv_succ_2 to H4. decompose. subst. + lapply linear nplus_inv_succ_2 to H5. decompose + ]; subst; auto. +qed. + theorem nplus_comm_1_rew: \forall p1,q,r1. (p1 + q == r1) \to \forall p2,r2. (p2 + q == r2) \to \forall s. (p1 + r2 == s) \to (p2 + r1 == s). intros 4. elim H; clear H q r1; - [ lapply linear nplus_gen_zero_2 to H1. subst - | lapply linear nplus_gen_succ_2 to H3. decompose. subst. - lapply linear nplus_gen_succ_2 to H4. decompose. subst + [ lapply linear nplus_inv_zero_2 to H1. subst + | lapply linear nplus_inv_succ_2 to H3. decompose. subst. + lapply linear nplus_inv_succ_2 to H4. decompose. subst ]; auto. qed. @@ -54,14 +75,14 @@ qed. theorem nplus_shift_succ_sx: \forall p,q,r. (p + (succ q) == r) \to (succ p) + q == r. intros. - lapply linear nplus_gen_succ_2 to H as H0. + lapply linear nplus_inv_succ_2 to H as H0. decompose. subst. auto new timeout=100. qed. theorem nplus_shift_succ_dx: \forall p,q,r. ((succ p) + q == r) \to p + (succ q) == r. intros. - lapply linear nplus_gen_succ_1 to H as H0. + lapply linear nplus_inv_succ_1 to H as H0. decompose. subst. auto new timeout=100. qed. @@ -69,11 +90,11 @@ theorem nplus_trans_1: \forall p,q1,r1. (p + q1 == r1) \to \forall q2,r2. (r1 + q2 == r2) \to \exists q. (q1 + q2 == q) \land p + q == r2. intros 2; elim q1; clear q1; intros; - [ lapply linear nplus_gen_zero_2 to H as H0. + [ lapply linear nplus_inv_zero_2 to H as H0. subst. - | lapply linear nplus_gen_succ_2 to H1 as H0. + | lapply linear nplus_inv_succ_2 to H1 as H0. decompose. subst. - lapply linear nplus_gen_succ_1 to H2 as H0. + lapply linear nplus_inv_succ_1 to H2 as H0. decompose. subst. lapply linear H to H4, H3 as H0. decompose. @@ -84,15 +105,14 @@ theorem nplus_trans_2: \forall p1,q,r1. (p1 + q == r1) \to \forall p2,r2. (p2 + r1 == r2) \to \exists p. (p1 + p2 == p) \land p + q == r2. intros 2; elim q; clear q; intros; - [ lapply linear nplus_gen_zero_2 to H as H0. + [ lapply linear nplus_inv_zero_2 to H as H0. subst - | lapply linear nplus_gen_succ_2 to H1 as H0. + | lapply linear nplus_inv_succ_2 to H1 as H0. decompose. subst. - lapply linear nplus_gen_succ_2 to H2 as H0. + lapply linear nplus_inv_succ_2 to H2 as H0. decompose. subst. lapply linear H to H4, H3 as H0. decompose. ]; apply ex_intro; [| auto new timeout=100 || auto new timeout=100 ]. (**) qed. *) - -- 2.39.2