From ac7831c825d6c3227053f3e339a53b10e3e7118f Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 14 Feb 2007 19:54:52 +0000 Subject: [PATCH] some improvements --- .../LAMBDA-TYPES/Unified-Sub/Context/defs.ma | 2 +- .../LAMBDA-TYPES/Unified-Sub/Lift/defs.ma | 37 +++----- .../LAMBDA-TYPES/Unified-Sub/Lift/fwd.ma | 87 +++++++++---------- .../LAMBDA-TYPES/Unified-Sub/Lift/props.ma | 69 ++++++++------- .../LAMBDA-TYPES/Unified-Sub/Term/defs.ma | 12 ++- .../LAMBDA-TYPES/Unified-Sub/preamble.ma | 11 +++ matita/contribs/RELATIONAL/NLE/dec.ma | 8 +- matita/contribs/RELATIONAL/NLE/defs.ma | 17 +++- matita/contribs/RELATIONAL/NLE/fwd.ma | 39 ++++----- matita/contribs/RELATIONAL/NLE/nplus.ma | 21 +++++ matita/contribs/RELATIONAL/NLE/props.ma | 53 +++++++---- 11 files changed, 201 insertions(+), 155 deletions(-) create mode 100644 matita/contribs/RELATIONAL/NLE/nplus.ma diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Context/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Context/defs.ma index 7aca13a59..4da3c95d7 100644 --- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Context/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Context/defs.ma @@ -23,5 +23,5 @@ include "Term/defs.ma". inductive Context: Set \def | leaf: Context - | head: Context \to Bind \to Term \to Context + | intb: Context \to IntB \to Term \to Context . diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma index eac00ae35..131d65133 100644 --- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma @@ -20,27 +20,18 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/defs". include "Term/defs.ma". -inductive Lift: Bool \to Nat \to Nat \to Term \to Term \to Prop \def - | lift_sort : \forall l,q,i,h. - Lift q l i (leaf (sort h)) (leaf (sort h)) - | lift_lref : \forall l,i,j. - Lift false l i (leaf (lref j)) (leaf (lref j)) - | lift_lref_lt: \forall l,i,j. j < i \to - Lift true l i (leaf (lref j)) (leaf (lref j)) - | lift_lref_ge: \forall l,i,j1. i <= j1 \to - \forall j2. (j1 + l == j2) \to - Lift true l i (leaf (lref j1)) (leaf (lref j2)) - | lift_bind : \forall l,i,u1,u2. Lift true l i u1 u2 \to - \forall q,t1,t2. Lift q l (succ i) t1 t2 \to - \forall r. - Lift q l i (head q (bind r) u1 t1) (head q (bind r) u2 t2) - | lift_flat : \forall l,i,u1,u2. Lift true l i u1 u2 \to - \forall q,t1,t2. Lift q l i t1 t2 \to - \forall r. - Lift q l i (head q (flat r) u1 t1) (head q (flat r) u2 t2) - | lift_head : \forall l,q,p. (p = q \to False) \to - \forall i,u1,u2. Lift false l i u1 u2 \to - \forall t1,t2. Lift q l i t1 t2 \to - \forall z. - Lift q l i (head p z u1 t1) (head p z u2 t2) +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_lref_gt: \forall i,j. i > j \to + Lift l i (leaf (lref j)) (leaf (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_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) + | lift_flat : \forall i,u1,u2. Lift l i u1 u2 \to + \forall t1,t2. Lift l i t1 t2 \to + \forall r. Lift l i (intf r u1 t1) (intf r u2 t2) . diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fwd.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fwd.ma index 9caab5d2f..59e33fb6e 100644 --- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fwd.ma +++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fwd.ma @@ -16,64 +16,59 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/fwd". include "Lift/defs.ma". -theorem lift_sort_1: \forall q, h, d, k, x. - Lift q h d (leaf (sort k)) x \to - x = leaf (sort k). +theorem lift_inv_sort_1: \forall l, i, h, x. + Lift l i (leaf (sort h)) x \to + x = leaf (sort h). intros. inversion H; clear H; intros; [ auto + | destruct H2 | destruct H3 - | destruct H4 | destruct H5 - | destruct H7 - | destruct H7 - | destruct H8 + | destruct H5 ]. qed. -theorem lift_lref_1: \forall q, h, d, k, x. - Lift q h d (leaf (lref k)) x \to - (q = false \land x = leaf (lref k)) \lor - (q = true \land k < d \land x = leaf (lref k)) \lor - (q = true \land d <= k \land - \exists e. (k + h == e) \land x = leaf (lref e) - ). +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 + (i <= j1 \land + \exists j2. (l + j1 == j2) \land x = leaf (lref j2) + ). intros. inversion H; clear H; intros; - [ destruct H3 - | destruct H3. clear H3. subst. auto depth = 4 - | destruct H4. clear H4. subst. auto depth = 5 - | destruct H5. clear H5. subst. auto depth = 5 - | destruct H7 - | destruct H7 - | destruct H8 + [ destruct H1 + | destruct H2. clear H2. subst. auto + | destruct H3. clear H3. subst. auto depth = 5 + | destruct H5 + | destruct H5 ]. qed. -theorem lift_head_1: \forall q, l, i, p, z, u1, t1, x. - Lift q l i (head p z u1 t1) x \to - (p = q \land - \exists r, u2, t2. - z = bind r \land - Lift true l i u1 u2 \land Lift q l (succ i) t1 t2 \land - x = head p z u2 t2 - ) \lor - (p = q \land - \exists r,u2,t2. - z = flat r \land - Lift true l i u1 u2 \land Lift q l i t1 t2 \land - x = head p z u2 t2 - ) \lor - ((p = q \to False) \land - \exists u2,t2. - Lift true l i u1 u2 \land Lift q l i t1 t2 \land - x = head p z u2 t2 - ). +theorem lift_inv_bind_1: \forall l, i, r, u1, t1, x. + Lift l i (intb r u1 t1) x \to + \exists u2, t2. + Lift l i u1 u2 \land + Lift l (succ i) t1 t2 \land + x = intb r u2 t2. intros. inversion H; clear H; intros; - [ destruct H3 + [ destruct H1 + | destruct H2 | destruct H3 - | destruct H4 + | destruct H5. clear H5 H1 H3. subst. auto depth = 5 | destruct H5 - | destruct H7. clear H7 H1 H3. subst. auto depth = 10 - | destruct H7. clear H7 H1 H3. subst. auto depth = 10 - | destruct H8. clear H8 H2 H4. subst. auto depth = 7 ]. -qed. \ No newline at end of file +qed. + +theorem lift_inv_flat_1: \forall l, i, r, u1, t1, x. + Lift l i (intf r u1 t1) x \to + \exists u2, t2. + Lift l i u1 u2 \land + Lift l i t1 t2 \land + x = intf r u2 t2. + intros. inversion H; clear H; intros; + [ destruct H1 + | destruct H2 + | destruct H3 + | destruct H5 + | destruct H5. clear H5 H1 H3. subst. auto depth = 5 + ]. +qed. diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma index 599aaeebb..9d8749aa5 100644 --- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma +++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma @@ -16,43 +16,46 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/props". include "Lift/fwd.ma". -alias id "nplus_conf" = "cic:/matita/RELATIONAL/NPlus/props/nplus_conf.con". - -axiom pippo: \forall x,y. x < y \to y <= x \to False. - -theorem lift_conf: \forall q,h,d,t,x. Lift q h d t x \to - \forall y. Lift q h d t y \to +theorem lift_conf: \forall l,i,t,x. Lift l i t x \to + \forall y. Lift l i t y \to x = y. - intros 6. elim H; clear H q h d t x; - [ lapply linear lift_sort_fwd to H1. + intros 5. elim H; clear H i t x; + [ lapply linear lift_inv_sort_1 to H1. subst. auto - | lapply linear lift_lref_fwd to H1. - decompose; subst; - [ auto | destruct H1 | destruct H ] - | lapply linear lift_lref_fwd to H2. + | lapply linear lift_inv_lref_1 to H2. decompose; subst; - [ destruct H | auto | lapply pippo to H1, H4. decompose ] - | lapply linear lift_lref_fwd to H3. + [ auto | lapply nle_false to H2, H1. decompose ] + | lapply linear lift_inv_lref_1 to H3. decompose; subst; - [ destruct H - | lapply linear pippo to H5, H1. decompose - | lapply linear nplus_conf to H2, H4. subst. auto + [ lapply linear nle_false to H1, H3. decompose + | lapply linear nplus_conf to H2, H4. subst. auto ] + | lapply linear lift_inv_bind_1 to H5. + decompose. subst. auto. + | lapply linear lift_inv_flat_1 to H5. + decompose. subst. auto. + ]. +qed. + +alias id "nle_trans" = "cic:/matita/RELATIONAL/NLE/props/nle_trans.con". +alias id "pippo" = "cic:/matita/RELATIONAL/NLE/nplus/pippo.con". +alias id "nle_refl" = "cic:/matita/RELATIONAL/NLE/props/nle_refl.con". -(* -theorem lift_ct_le: \forall q,h,d,t,y. (Lift q h d t y) \to - \forall k,e,x. (Lift q k e t x) \to - \forall z. (Lift q k e y z) \to - e <= d \to \forall d'. (k + d == d') \to - (Lift q h d' x z). - intros 6. elim H; clear H q h d t y; - [ lapply linear lift_sort_fwd to H1. - lapply linear lift_sort_fwd to H2. +theorem lift_ct_le: \forall l1,i1,t,y. (Lift l1 i1 t y) \to + \forall l2,i2,x. (Lift l2 i2 t x) \to + \forall z. (Lift l2 i2 y z) \to + i2 <= i1 \to \forall i. (l2 + i1 == i) \to + (Lift l1 i x z). + intros 5. elim H; clear H i1 t y; + [ lapply lift_conf to H1, H2. clear H2. subst. + lapply linear lift_inv_sort_1 to H1. subst. auto - | lapply linear lift_lref_fwd to H1. - lapply linear lift_lref_fwd to H2. - decompose; subst; - [ auto - | auto - | - *) \ No newline at end of file + | lapply lift_conf 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 H. clear l2. (**) + lapply linear nle_trans to H1, H. + auto + | lapply pippo to H3, H5; [ auto | apply nle_refl | auto ]. (**) + ] + | \ No newline at end of file diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Term/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Term/defs.ma index e08209626..e0b165e4f 100644 --- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Term/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Term/defs.ma @@ -43,12 +43,16 @@ inductive Flat: Set \def | cast: Flat . -inductive Head: Set \def - | bind: Bind \to Head - | flat: Flat \to Head +inductive IntB: Set \def + | bind: Bool \to Bind \to IntB +. + +inductive IntF: Set \def + | flat: Bool \to Flat \to IntF . inductive Term: Set \def | leaf: Leaf \to Term - | head: Bool \to Head \to Term \to Term \to Term + | intb: IntB \to Term \to Term \to Term + | intf: IntF \to Term \to Term \to Term . diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma index 45f2fb182..9470cf008 100644 --- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma +++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma @@ -24,3 +24,14 @@ include "../../RELATIONAL/NPlus/defs.ma". include "../../RELATIONAL/NLE/defs.ma". include "../../RELATIONAL/Nat/defs.ma". include "../../RELATIONAL/Bool/defs.ma". + +alias id "nplus_conf" = "cic:/matita/RELATIONAL/NPlus/props/nplus_conf.con". +alias id "nle_false" = "cic:/matita/RELATIONAL/NLE/props/nle_false.con". + +axiom f_equal_3: \forall (A,B,C,D:Set). + \forall (f:A \to B \to C \to D). + \forall (x1,x2:A). + \forall (y1,y2:B). + \forall (z1,z2:C). + x1 = x2 \to y1 = y2 \to z1 = z2 \to + f x1 y1 z1 = f x2 y2 z2. diff --git a/matita/contribs/RELATIONAL/NLE/dec.ma b/matita/contribs/RELATIONAL/NLE/dec.ma index 7c45ab488..918acfe53 100644 --- a/matita/contribs/RELATIONAL/NLE/dec.ma +++ b/matita/contribs/RELATIONAL/NLE/dec.ma @@ -18,12 +18,12 @@ include "NLE/props.ma". theorem nat_dec_lt_ge: \forall x,y. x < y \lor y <= x. intros 2; elim y; clear y; - [ auto new timeout=100 + [ auto | decompose; - [ lapply linear nle_gen_succ_1 to H1. decompose. - subst. auto new timeout=100 depth=4 + [ lapply linear nle_inv_succ_1 to H1. decompose. + subst. auto depth=4 | lapply linear nle_lt_or_eq to H1; decompose; - subst; auto new timeout=100 + subst; auto ] ]. qed. diff --git a/matita/contribs/RELATIONAL/NLE/defs.ma b/matita/contribs/RELATIONAL/NLE/defs.ma index a9b33561d..2cea043d5 100644 --- a/matita/contribs/RELATIONAL/NLE/defs.ma +++ b/matita/contribs/RELATIONAL/NLE/defs.ma @@ -16,14 +16,23 @@ set "baseuri" "cic:/matita/RELATIONAL/NLE/defs". include "NPlus/defs.ma". -definition NLE: Nat \to Nat \to Prop \def - \lambda q,r. \exists p. (p + q == r). +inductive NLE (q:Nat) (r:Nat): Prop \def + | nle_nplus: \forall p. (p + q == r) \to NLE q r. (*CSC: the URI must disappear: there is a bug now *) interpretation "natural 'less or equal to'" 'leq x y = - (cic:/matita/RELATIONAL/NLE/defs/NLE.con x y). + (cic:/matita/RELATIONAL/NLE/defs/NLE.ind#xpointer(1/1) x y). (*CSC: the URI must disappear: there is a bug now *) interpretation "natural 'less than'" 'lt x y = - (cic:/matita/RELATIONAL/NLE/defs/NLE.con + (cic:/matita/RELATIONAL/NLE/defs/NLE.ind#xpointer(1/1) + (cic:/matita/RELATIONAL/Nat/defs/Nat.ind#xpointer(1/1/2) x) y). + +(*CSC: the URI must disappear: there is a bug now *) +interpretation "natural 'greater or equal to'" 'geq y x= + (cic:/matita/RELATIONAL/NLE/defs/NLE.ind#xpointer(1/1) x y). + +(*CSC: the URI must disappear: there is a bug now *) +interpretation "natural 'greater than'" 'gt y x = + (cic:/matita/RELATIONAL/NLE/defs/NLE.ind#xpointer(1/1) (cic:/matita/RELATIONAL/Nat/defs/Nat.ind#xpointer(1/1/2) x) y). diff --git a/matita/contribs/RELATIONAL/NLE/fwd.ma b/matita/contribs/RELATIONAL/NLE/fwd.ma index afefbfd4d..06b7c6fef 100644 --- a/matita/contribs/RELATIONAL/NLE/fwd.ma +++ b/matita/contribs/RELATIONAL/NLE/fwd.ma @@ -16,44 +16,41 @@ set "baseuri" "cic:/matita/RELATIONAL/NLE/fwd". include "logic/connectives.ma". -include "NPlus/fwd.ma". +include "NPlus/fwd.ma". include "NLE/defs.ma". -theorem nle_gen_succ_1: \forall x,y. x < y \to - \exists z. y = succ z \land x <= z. - unfold NLE. - intros. decompose. - lapply linear nplus_gen_succ_2 to H1 as H. - decompose. subst. - apply ex_intro;[| auto] (**) +theorem nle_inv_succ_1: \forall x,y. x < y \to + \exists z. y = succ z \land x <= z. + intros. elim H. + lapply linear nplus_gen_succ_2 to H1. + decompose. subst. auto depth = 4. qed. - -theorem nle_gen_succ_succ: \forall x,y. x < succ y \to x <= y. +theorem nle_inv_succ_succ: \forall x,y. x < succ y \to x <= y. intros. - lapply linear nle_gen_succ_1 to H as H0. decompose H0. - lapply linear eq_gen_succ_succ to H1 as H. subst. + lapply linear nle_inv_succ_1 to H. decompose. + lapply linear eq_gen_succ_succ to H1. subst. auto. qed. -theorem nle_gen_succ_zero: \forall x. x < zero \to False. +theorem nle_inv_succ_zero: \forall x. x < zero \to False. intros. - lapply linear nle_gen_succ_1 to H. decompose. + lapply linear nle_inv_succ_1 to H. decompose. lapply linear eq_gen_zero_succ to H1. decompose. qed. -theorem nle_gen_zero_2: \forall x. x <= zero \to x = zero. +theorem nle_inv_zero_2: \forall x. x <= zero \to x = zero. intros 1. elim x; clear x; intros; - [ auto new timeout=30 - | lapply linear nle_gen_succ_zero to H1. decompose. + [ auto + | lapply linear nle_inv_succ_zero to H1. decompose. ]. qed. -theorem nle_gen_succ_2: \forall y,x. x <= succ y \to +theorem nle_inv_succ_2: \forall y,x. x <= succ y \to x = zero \lor \exists z. x = succ z \land z <= y. intros 2; elim x; clear x; intros; - [ auto new timeout=30 - | lapply linear nle_gen_succ_succ to H1. - right. apply ex_intro; [|auto new timeout=30] (**) + [ auto + | lapply linear nle_inv_succ_succ to H1. + auto depth = 4. ]. qed. diff --git a/matita/contribs/RELATIONAL/NLE/nplus.ma b/matita/contribs/RELATIONAL/NLE/nplus.ma new file mode 100644 index 000000000..7bcdd6010 --- /dev/null +++ b/matita/contribs/RELATIONAL/NLE/nplus.ma @@ -0,0 +1,21 @@ +(**************************************************************************) +(* ___ *) +(* ||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/NLE/nplus". + +include "NLE/defs.ma". + +axiom pippo: \forall x1, x2, x3. (x1 + x2 == x3) \to + \forall y1, y2, y3. (y1 + y2 == y3) \to + x1 <= y1 \to x2 < y2 \to x3 < y3. diff --git a/matita/contribs/RELATIONAL/NLE/props.ma b/matita/contribs/RELATIONAL/NLE/props.ma index 549eae418..34e5d0a24 100644 --- a/matita/contribs/RELATIONAL/NLE/props.ma +++ b/matita/contribs/RELATIONAL/NLE/props.ma @@ -16,36 +16,51 @@ set "baseuri" "cic:/matita/RELATIONAL/NLE/props". include "NLE/fwd.ma". -theorem nle_zero: \forall q. zero <= q. - unfold NLE. - intros. apply ex_intro; auto. (**) +theorem nle_zero_1: \forall q. zero <= q. + intros. auto. qed. -theorem nle_succ: \forall p,q. p <= q \to succ p <= succ q. - unfold NLE. - intros. decompose. - apply ex_intro; [|auto] (**) +theorem nle_succ_succ: \forall p,q. p <= q \to succ p <= succ q. + intros. elim H. clear H. auto. +qed. + +theorem nle_ind: \forall P:(Nat \to Nat \to Prop). + (\forall n:Nat.P zero n) \to + (\forall n,n1:Nat. + n <= n1 \to P n n1 \to P (succ n) (succ n1) + ) \to + \forall n,n1:Nat. n <= n1 \to P n n1. + intros 4. elim n; clear n; + [ auto + | lapply linear nle_inv_succ_1 to H3. decompose; subst. + auto + ]. qed. theorem nle_refl: \forall x. x <= x. - intros 1; elim x; clear x; intros; auto new timeout=100. + intros 1; elim x; clear x; intros; auto. qed. theorem nle_trans_succ: \forall x,y. x <= y \to x <= succ y. - intros 1. elim x; clear x; intros; - [ auto new timeout=100. - | lapply linear nle_gen_succ_1 to H1 as H0. decompose H0. subst. - auto new timeout=100. + intros. elim H using nle_ind; clear H x y; auto. +qed. + +theorem nle_false: \forall x,y. x <= y \to y < x \to False. + intros 3; elim H using nle_ind; clear H x y; auto. +qed. + +theorem nle_trans: \forall x,y. x <= y \to + \forall z. y <= z \to x <= z. + intros 3. elim H using nle_ind; clear H x y; + [ auto + | lapply linear nle_inv_succ_1 to H3. decompose. subst. + auto ]. qed. theorem nle_lt_or_eq: \forall y,x. x <= y \to x < y \lor x = y. - intros 1. elim y; clear y; intros; - [ lapply linear nle_gen_zero_2 to H. auto new timeout=100 - | lapply linear nle_gen_succ_2 to H1. decompose; - [ subst. auto new timeout=100 - | lapply linear H to H3 as H0. decompose; - subst; auto new timeout=100 - ] + intros. elim H using nle_ind; clear H x y; + [ elim n; clear n; auto + | decompose; subst; auto ]. qed. -- 2.39.2