From: Ferruccio Guidi Date: Thu, 15 Feb 2007 23:02:13 +0000 (+0000) Subject: contribs: some improvements X-Git-Tag: 0.4.95@7852~593 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1c66d874087fd178b21864cd53fc851dd01c2aff;p=helm.git contribs: some improvements Sequent2pres: added some spaces --- diff --git a/components/content_pres/sequent2pres.ml b/components/content_pres/sequent2pres.ml index 391b178a2..2ae090bb0 100644 --- a/components/content_pres/sequent2pres.ml +++ b/components/content_pres/sequent2pres.ml @@ -64,7 +64,7 @@ let sequent2pres term2pres (_,_,context,ty) = (match dec_name with None -> "_" | Some n -> n)) ; - Box.b_text [] ":" ; + Box.b_space; Box.b_text [] ":"; Box.b_space; term2pres ty] in aux (r::accum) tl | (Some (`Definition d))::tl -> @@ -77,9 +77,9 @@ let sequent2pres term2pres (_,_,context,ty) = [ Box.b_object (p_mi [] (match def_name with None -> "_" - | Some n -> n)) ; - Box.b_text [] (Utf8Macro.unicode_of_tex "\\def") ; - term2pres bo] in + | Some n -> n)) ; Box.b_space ; + Box.b_text [] (Utf8Macro.unicode_of_tex "\\def") ; + Box.b_space; term2pres bo] in aux (r::accum) tl | _::_ -> assert false in aux [] context in diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fwd.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fwd.ma deleted file mode 100644 index 59e33fb6e..000000000 --- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fwd.ma +++ /dev/null @@ -1,74 +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/LAMBDA-TYPES/Unified-Sub/Lift/fwd". - -include "Lift/defs.ma". - -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 H5 - | destruct H5 - ]. -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 - (i <= j1 \land - \exists j2. (l + j1 == j2) \land x = leaf (lref j2) - ). - intros. inversion H; clear H; intros; - [ destruct H1 - | destruct H2. clear H2. subst. auto - | destruct H3. clear H3. subst. auto depth = 5 - | destruct H5 - | destruct H5 - ]. -qed. - -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 H1 - | destruct H2 - | destruct H3 - | destruct H5. clear H5 H1 H3. subst. auto depth = 5 - | destruct H5 - ]. -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/inv.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma new file mode 100644 index 000000000..8c3d27d7c --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma @@ -0,0 +1,74 @@ +(**************************************************************************) +(* ___ *) +(* ||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/LAMBDA-TYPES/Unified-Sub/Lift/inv". + +include "Lift/defs.ma". + +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 H5 + | destruct H5 + ]. +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 + (i <= j1 \land + \exists j2. (l + j1 == j2) \land x = leaf (lref j2) + ). + intros. inversion H; clear H; intros; + [ destruct H1 + | destruct H2. clear H2. subst. auto + | destruct H3. clear H3. subst. auto depth = 5 + | destruct H5 + | destruct H5 + ]. +qed. + +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 H1 + | destruct H2 + | destruct H3 + | destruct H5. clear H5 H1 H3. subst. auto depth = 5 + | destruct H5 + ]. +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 9d8749aa5..8c3df062e 100644 --- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma +++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/props". -include "Lift/fwd.ma". +include "Lift/inv.ma". theorem lift_conf: \forall l,i,t,x. Lift l i t x \to \forall y. Lift l i t y \to @@ -37,15 +37,11 @@ theorem lift_conf: \forall l,i,t,x. Lift l i t x \to ]. 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 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). +theorem lift_comp_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. @@ -53,9 +49,24 @@ theorem lift_ct_le: \forall l1,i1,t,y. (Lift l1 i1 t y) \to | 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. + [ lapply linear nle_nplus to H5 as H0. clear l2. (**) + lapply linear nle_trans to H1, H0. auto - | lapply pippo to H3, H5; [ auto | apply nle_refl | 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. + ] ] - | \ No newline at end of file + | \ No newline at end of file diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma index 9470cf008..3b532dd55 100644 --- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma +++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma @@ -20,13 +20,10 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/preamble". *) include "logic/equality.ma". -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". +include "../../RELATIONAL/datatypes/Bool.ma". +include "../../RELATIONAL/NPlus/props.ma". +include "../../RELATIONAL/NLE/props.ma". +include "../../RELATIONAL/NLE/nplus.ma". axiom f_equal_3: \forall (A,B,C,D:Set). \forall (f:A \to B \to C \to D). diff --git a/matita/contribs/RELATIONAL/NPlus/defs.ma b/matita/contribs/RELATIONAL/NPlus/defs.ma index 93c7a2e45..8d8b304c3 100644 --- a/matita/contribs/RELATIONAL/NPlus/defs.ma +++ b/matita/contribs/RELATIONAL/NPlus/defs.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/RELATIONAL/NPlus/defs". -include "datatypes/defs.ma". +include "datatypes/Nat.ma". inductive NPlus (p:Nat): Nat \to Nat \to Prop \def | nplus_zero_2: NPlus p zero p diff --git a/matita/contribs/RELATIONAL/NPlus/props.ma b/matita/contribs/RELATIONAL/NPlus/props.ma index d566e8a32..43966337b 100644 --- a/matita/contribs/RELATIONAL/NPlus/props.ma +++ b/matita/contribs/RELATIONAL/NPlus/props.ma @@ -16,31 +16,42 @@ set "baseuri" "cic:/matita/RELATIONAL/NPlus/props". include "NPlus/inv.ma". +(* Monoidal properties *) + +theorem nplus_conf: \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 + ]; subst; auto. +qed. + theorem nplus_zero_1: \forall q. zero + q == q. - intros. elim q; clear q; auto new timeout=100. + intros. elim q; clear q; auto. qed. theorem nplus_succ_1: \forall p,q,r. NPlus p q r \to (succ p) + q == (succ r). - intros 2. elim q; clear q; - [ lapply linear nplus_gen_zero_2 to H as H0. - subst - | lapply linear nplus_gen_succ_2 to H1 as H0. - decompose. - subst - ]; auto new timeout=100. + intros. elim H; clear H q r; auto. qed. -theorem nplus_sym: \forall p,q,r. (p + q == r) \to q + p == r. - intros 2. elim q; clear q; - [ lapply linear nplus_gen_zero_2 to H as H0. - subst - | lapply linear nplus_gen_succ_2 to H1 as H0. - decompose. - subst - ]; auto new timeout=100. +theorem nplus_comm: \forall p,q,r. (p + q == r) \to q + p == r. + intros. elim H; clear H q r; auto. +qed. + +(* Corollaries *) + +theorem nplus_comm_1: \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 + ]; auto. qed. +(* theorem nplus_shift_succ_sx: \forall p,q,r. (p + (succ q) == r) \to (succ p) + q == r. intros. @@ -84,15 +95,5 @@ theorem nplus_trans_2: \forall p1,q,r1. (p1 + q == r1) \to decompose. ]; apply ex_intro; [| auto new timeout=100 || auto new timeout=100 ]. (**) qed. +*) -theorem nplus_conf: \forall p,q,r1. (p + q == r1) \to - \forall r2. (p + q == r2) \to r1 = r2. - 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. subst. - lapply linear nplus_gen_succ_2 to H2 as H0. - decompose. subst. - ]; auto new timeout=100. -qed. diff --git a/matita/contribs/RELATIONAL/datatypes/Nat.ma b/matita/contribs/RELATIONAL/datatypes/Nat.ma new file mode 100644 index 000000000..3a3a4f5ed --- /dev/null +++ b/matita/contribs/RELATIONAL/datatypes/Nat.ma @@ -0,0 +1,22 @@ +(**************************************************************************) +(* ___ *) +(* ||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/datatypes/Nat". + +include "preamble.ma". + +inductive Nat: Set \def + | zero: Nat + | succ: Nat \to Nat +. diff --git a/matita/contribs/RELATIONAL/datatypes/defs.ma b/matita/contribs/RELATIONAL/datatypes/defs.ma deleted file mode 100644 index 3a3a4f5ed..000000000 --- a/matita/contribs/RELATIONAL/datatypes/defs.ma +++ /dev/null @@ -1,22 +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/datatypes/Nat". - -include "preamble.ma". - -inductive Nat: Set \def - | zero: Nat - | succ: Nat \to Nat -.