From e6d7bb2e5237c8f9c85179715edeab61263ab62d Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 15 Feb 2007 23:02:13 +0000 Subject: [PATCH] contribs: some improvements Sequent2pres: added some spaces --- .../components/content_pres/sequent2pres.ml | 8 +-- .../Unified-Sub/Lift/{fwd.ma => inv.ma} | 2 +- .../LAMBDA-TYPES/Unified-Sub/Lift/props.ma | 39 ++++++++----- .../LAMBDA-TYPES/Unified-Sub/preamble.ma | 11 ++-- .../matita/contribs/RELATIONAL/NPlus/defs.ma | 2 +- .../matita/contribs/RELATIONAL/NPlus/props.ma | 55 ++++++++++--------- .../RELATIONAL/datatypes/{defs.ma => Nat.ma} | 0 7 files changed, 63 insertions(+), 54 deletions(-) rename helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/{fwd.ma => inv.ma} (97%) rename helm/software/matita/contribs/RELATIONAL/datatypes/{defs.ma => Nat.ma} (100%) diff --git a/helm/software/components/content_pres/sequent2pres.ml b/helm/software/components/content_pres/sequent2pres.ml index 391b178a2..2ae090bb0 100644 --- a/helm/software/components/content_pres/sequent2pres.ml +++ b/helm/software/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/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma similarity index 97% rename from helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fwd.ma rename to helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma index 59e33fb6e..8c3d27d7c 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fwd.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/fwd". +set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/inv". include "Lift/defs.ma". 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 9d8749aa5..8c3df062e 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 @@ -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/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma index 9470cf008..3b532dd55 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma +++ b/helm/software/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/helm/software/matita/contribs/RELATIONAL/NPlus/defs.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/defs.ma index 93c7a2e45..8d8b304c3 100644 --- a/helm/software/matita/contribs/RELATIONAL/NPlus/defs.ma +++ b/helm/software/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/helm/software/matita/contribs/RELATIONAL/NPlus/props.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/props.ma index d566e8a32..43966337b 100644 --- a/helm/software/matita/contribs/RELATIONAL/NPlus/props.ma +++ b/helm/software/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/helm/software/matita/contribs/RELATIONAL/datatypes/defs.ma b/helm/software/matita/contribs/RELATIONAL/datatypes/Nat.ma similarity index 100% rename from helm/software/matita/contribs/RELATIONAL/datatypes/defs.ma rename to helm/software/matita/contribs/RELATIONAL/datatypes/Nat.ma -- 2.39.2