From: Ferruccio Guidi Date: Fri, 9 Mar 2012 17:31:33 +0000 (+0000) Subject: - lambda_delta: morew propertie in context-sensitive computation X-Git-Tag: make_still_working~1866 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3dd0d3a7493b73418a5a08e540f23fe82106cef9;p=helm.git - lambda_delta: morew propertie in context-sensitive computation - formal_topology: compilation of categories.ma continues ... - grafiteEngine.ml: coercions to sorts can now be defined with the short syntax --- diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index c5e291959..ec14f4d3e 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -495,19 +495,26 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = let ty = NCicTypeChecker.typeof status [] [] [] t in let source, target = let clean = function - | NCic.Appl (NCic.Const _ as r :: l) -> - NotationPt.Appl (NotationPt.NCic r :: - List.map (fun _ -> NotationPt.Implicit `JustOne)l) - | NCic.Const _ as r -> NotationPt.NCic r - | _ -> assert false in + | NCic.Appl (NCic.Const _ as r :: l) -> + NotationPt.Appl (NotationPt.NCic r :: + List.map (fun _ -> NotationPt.Implicit `JustOne)l) + | NCic.Const _ as r -> NotationPt.NCic r + | NCic.Sort _ as r -> NotationPt.NCic r (* FG: missing case *) + | _ -> assert false + in let rec aux = function - | NCic.Prod (_,_, (NCic.Prod _ as rest)) -> aux rest - | NCic.Prod (name, src, tgt) -> (name, clean src), clean tgt - | _ -> assert false in aux ty in - status, o_t, NotationPt.NCic ty, source, target in + | NCic.Prod (_,_, (NCic.Prod _ as rest)) -> aux rest + | NCic.Prod (name, src, tgt) -> (name, clean src), clean tgt + | _ -> assert false + in + aux ty + in + status, o_t, NotationPt.NCic ty, source, target + in let status, composites = NCicCoercDeclaration.eval_ncoercion status name compose t ty source - target in + target + in let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *) let aliases = GrafiteDisambiguate.aliases_for_objs status composites in eval_alias status (mode,aliases) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt b/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt index 54f20be57..bc4582ede 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt +++ b/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt @@ -254,7 +254,6 @@ pr2/subst1 pr2_gen_cabbr pr3/fwd pr3_gen_abst pr3/fwd pr3_gen_lref pr3/fwd pr3_gen_void -pr3/fwd pr3_gen_abbr pr3/fwd pr3_gen_appl pr3/fwd pr3_gen_bind pr3/iso pr3_iso_appls_abbr @@ -271,11 +270,9 @@ pr3/props pr3_head_2 pr3/props pr3_head_21 pr3/props pr3_head_12 pr3/props pr3_flat -pr3/props pr3_pr3_pr3_t pr3/props pr3_eta pr3/subst1 pr3_subst1 pr3/subst1 pr3_gen_cabbr -pr3/wcpr0 pr3_wcpr0_t sn3/props sn3_cpr3_trans sn3/props sn3_shift diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_cprs.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_cprs.ma index 54a94b496..16c1a6256 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_cprs.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_cprs.ma @@ -82,7 +82,7 @@ lemma cprs_flat: ∀I,L,T1,T2. L ⊢ T1 ➡* T2 → ∀V1,V2. L ⊢ V1 ➡* V2 @(cprs_trans … IHV1) -IHV1 /2 width=1/ qed. -(* Basic_1: was only: pr3_pr2_pr3_t *) +(* Basic_1: was only: pr3_pr2_pr3_t pr3_wcpr0_t *) lemma lcpr_cprs_trans: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2. #L1 #L2 #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 // diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_lcprs.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_lcprs.ma new file mode 100644 index 000000000..6d4f5ec8c --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_lcprs.ma @@ -0,0 +1,52 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "Basic_2/computation/cprs_cprs.ma". +include "Basic_2/computation/lcprs_lcprs.ma". + +(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) + +(* Properties exploiting context-senstive computation on local environments *) + +(* Basic_1: was just: pr3_pr3_pr3_t *) +lemma lcprs_cprs_trans: ∀L1,L2. L1 ⊢ ➡* L2 → + ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2. +#L1 #L2 #HL12 @(lcprs_ind … HL12) -L2 // /3 width=3/ +qed. + +(* Advanced inversion lemmas ************************************************) + +(* Basic_1: was pr3_gen_abbr *) +lemma cprs_inv_abbr1: ∀L,V1,T1,U2. L ⊢ ⓓV1. T1 ➡* U2 → + (∃∃V2,T2. L ⊢ V1 ➡* V2 & L. ⓓV1 ⊢ T1 ➡* T2 & + U2 = ⓓV2. T2 + ) ∨ + ∃∃U. ⇧[0, 1] U2 ≡ U & L. ⓓV1 ⊢ T1 ➡* U. +#L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/ +#U0 #U2 #_ #HU02 * * +[ #V0 #T0 #HV10 #HT10 #H destruct + elim (cpr_inv_abbr1 … HU02) -HU02 * + [ #V #V2 #T2 #HV0 #HV2 #HT02 #H destruct + lapply (cpr_intro … HV0 … HV2) -HV2 #HV02 + lapply (ltpr_cpr_trans (L.ⓓV0) … HT02) /2 width=1/ -V #HT02 + lapply (lcprs_cprs_trans (L. ⓓV1) … HT02) -HT02 /2 width=1/ /4 width=5/ + | -V0 #T2 #HT20 #HTU2 + elim (lift_total U2 0 1) #U0 #HU20 + lapply (cpr_lift (L.ⓓV1) … HT20 … HU20 HTU2) -T2 /2 width=1/ /4 width=5/ + ] +| #U1 #HU01 #HTU1 + elim (lift_total U2 0 1) #U #HU2 + lapply (cpr_lift (L.ⓓV1) … HU01 … HU2 HU02) -U0 /2 width=1/ /4 width=5/ +] +qed-. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/lcprs.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/lcprs.ma new file mode 100644 index 000000000..627a0f58d --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/lcprs.ma @@ -0,0 +1,44 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "Basic_2/reducibility/lcpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *************) + +definition lcprs: relation lenv ≝ TC … lcpr. + +interpretation + "context-sensitive parallel computation (environment)" + 'CPRedStar L1 L2 = (lcprs L1 L2). + +(* Basic eliminators ********************************************************) + +lemma lcprs_ind: ∀L1. ∀R:predicate lenv. R L1 → + (∀L,L2. L1 ⊢ ➡* L → L ⊢ ➡ L2 → R L → R L2) → + ∀L2. L1 ⊢ ➡* L2 → R L2. +#L1 #R #HL1 #IHL1 #L2 #HL12 @(TC_star_ind … HL1 IHL1 … HL12) // +qed-. + +(* Basic properties *********************************************************) + +lemma lcprs_refl: ∀L. L ⊢ ➡* L. +/2 width=1/ qed. + +lemma lcprs_strap1: ∀L1,L,L2. + L1 ⊢ ➡* L → L ⊢ ➡ L2 → L1 ⊢ ➡* L2. +/2 width=3/ qed. + +lemma lcprs_strap2: ∀L1,L,L2. + L1 ⊢ ➡ L → L ⊢ ➡* L2 → L1 ⊢ ➡* L2. +/2 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/lcprs_cprs.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/lcprs_cprs.ma new file mode 100644 index 000000000..a45e8ee9f --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/lcprs_cprs.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "Basic_2/reducibility/lcpr_cpr.ma". +include "Basic_2/computation/cprs.ma". +include "Basic_2/computation/lcprs.ma". + +(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *************) + +(* Advanced properties ******************************************************) + +lemma lcprs_pair_dx: ∀I,L1,L2. L1 ⊢ ➡ L2 → ∀V1,V2. L2 ⊢ V1 ➡* V2 → + L1. ⓑ{I} V1 ⊢ ➡* L2. ⓑ{I} V2. +#I #L1 #L2 #HL12 #V1 #V2 #H @(cprs_ind … H) -V2 +/3 width=1/ /3 width=5/ +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/lcprs_lcprs.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/lcprs_lcprs.ma new file mode 100644 index 000000000..935b83d24 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/lcprs_lcprs.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "Basic_2/computation/lcprs_cprs.ma". + +(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *************) + +(* Main properties **********************************************************) + +theorem lcprs_trans: ∀L1,L. L1 ⊢ ➡* L → ∀L2. L ⊢ ➡* L2 → L1 ⊢ ➡* L2. +/2 width=3/ qed. + +lemma lcprs_pair: ∀L1,L2. L1 ⊢ ➡* L2 → ∀V1,V2. L2 ⊢ V1 ➡* V2 → + ∀I. L1. ⓑ{I} V1 ⊢ ➡* L2. ⓑ{I} V2. +#L1 #L2 #H @(lcprs_ind … H) -L2 /2 width=1/ +#L #L2 #_ #HL2 #IHL1 #V1 #V2 #HV12 #I +@(lcprs_trans … (L.ⓑ{I}V1)) /2 width=1/ +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma index 89f1a94e4..7e4ee3839 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma @@ -42,9 +42,9 @@ inductive item2: Type[0] ≝ | Flat2: flat2 → item2 (* non-binding item *) . -coercion item2_of_bind2: ∀I:bind2.item2 ≝ Bind2 on _I:bind2 to item2. +coercion Bind2. -coercion item2_of_flat2: ∀I:flat2.item2 ≝ Flat2 on _I:flat2 to item2. +coercion Flat2. (* Basic properties *********************************************************) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma index 0aabfd481..a9fca999c 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma @@ -300,7 +300,7 @@ notation "hvbox( L ⊢ break term 90 T1 ⬌ break T2 )" non associative with precedence 45 for @{ 'PConv $L $T1 $T2 }. -(* Congruence ***************************************************************) +(* Equivalence **************************************************************) notation "hvbox( L ⊢ break term 90 T1 ⬌* break T2 )" non associative with precedence 45 diff --git a/matita/matita/contribs/lambda_delta/Makefile b/matita/matita/contribs/lambda_delta/Makefile index b90b52178..5d86a4dd2 100644 --- a/matita/matita/contribs/lambda_delta/Makefile +++ b/matita/matita/contribs/lambda_delta/Makefile @@ -65,6 +65,7 @@ tbls: $(PACKAGES:%=etc/ld_%_sum.tbl) etc/ld_%_sum.tbl: MAS = $(shell find $* -name "*.ma") +%.tbl: V1 = $(shell ls $(MAS) | wc -l) %.tbl: C1 = $(shell grep "inductive \|record " $(MAS) | wc -l) %.tbl: C2 = $(shell grep "definition \|let rec " $(MAS) | wc -l) %.tbl: C3 = $(shell grep "inductive \|record \|definition \|let rec " $(MAS) | wc -l) @@ -80,6 +81,10 @@ etc/ld_%_sum.tbl: $(MAS) @printf ' class "grey" [ "category"\n' >> $@ @printf ' [ "objects" * ]\n' >> $@ @printf ' ]\n' >> $@ + @printf ' class "cyan" [ "volume"\n' >> $@ + @printf ' [ "files" "$(V1)" * ]\n' >> $@ + @printf ' [ 4 ]\n' >> $@ + @printf ' ]\n' >> $@ @printf ' class "green" [ "propositions"\n' >> $@ @printf ' [ "theorems" "$(P1)" * ]\n' >> $@ @printf ' [ "lemmas" "$(P2)" * ]\n' >> $@ diff --git a/matita/matita/lib/formal_topology/categories.ma b/matita/matita/lib/formal_topology/categories.ma index f5437449a..68a02e964 100644 --- a/matita/matita/lib/formal_topology/categories.ma +++ b/matita/matita/lib/formal_topology/categories.ma @@ -199,7 +199,6 @@ notation > "B ⇒_1. C" right associative with precedence 72 for @{'arrows1_SETl notation > "B ⇒_2 C" right associative with precedence 72 for @{'arrows2_SET1 $B $C}. notation > "B ⇒_2. C" right associative with precedence 72 for @{'arrows2_SET1low $B $C}. -notation "A × term 74 B ⇒ term 19 C" non associative with precedence 72 for @{'binary_morphism0 $A $B $C}. notation "A × term 74 B ⇒\sub 1 term 19 C" non associative with precedence 72 for @{'binary_morphism1 $A $B $C}. notation "A × term 74 B ⇒\sub 2 term 19 C" non associative with precedence 72 for @{'binary_morphism2 $A $B $C}. notation "A × term 74 B ⇒\sub 3 term 19 C" non associative with precedence 72 for @{'binary_morphism3 $A $B $C}. @@ -231,10 +230,10 @@ definition CPROP: setoid1. [ @CProp[0] | @mk_equivalence_relation1 [ @Iff - | #H1 @mk_Iff #H3 #H5 assumption - | #H7 #H8 #i cases i #H14 #H15 @mk_Iff assumption - | #H17 #H18 #H19 #i1 #i cases i cases i1 #f #f1 #f2 #f3 @mk_Iff - [ #x1 @(f2 (f x1)) | #z1 @(f1 (f3 z1))]]] + | #x @mk_Iff #x1 assumption + | #x #y #i cases i #f #f1 @mk_Iff assumption + | #x #y #z #i1 #i cases i cases i1 #f #f1 #f2 #f3 @mk_Iff #x1 + [ @(f2 (f x1)) | @(f1 (f3 x1))]]] qed. definition CProp0_of_CPROP: carr1 CPROP → CProp[0] ≝ λx.x. @@ -242,16 +241,16 @@ coercion CProp0_of_CPROP. alias symbol "eq" = "setoid1 eq". definition fi': ∀A,B:CPROP. A = B → B → A. - intros; @(fi ?? e); assumption. + #A #B #e #b @(fi ?? e) assumption. qed. notation ". r" with precedence 50 for @{'fi $r}. interpretation "fi" 'fi r = (fi' ?? r). definition and_morphism: binary_morphism1 CPROP CPROP CPROP. - constructor 1; + @mk_binary_morphism1 [ @And - | intros; split; intro; cases a1; split; + | #a #a' #b #b' #e #e1 @mk_Iff #a1 cases a1 #a2 #b1 @Conj [ @(if ?? e a2) | @(if ?? e1 b1) | @(fi ?? e a2) @@ -261,38 +260,40 @@ qed. interpretation "and_morphism" 'and a b = (fun21 ??? and_morphism a b). definition or_morphism: binary_morphism1 CPROP CPROP CPROP. - constructor 1; + @mk_binary_morphism1 [ @Or - | intros; split; intro; cases o; [1,3:left |2,4: right] + | #a #a' #b #b' #e #e1 @mk_Iff #o cases o #a1 [1,3: @Left |2,4: @Right] [ @(if ?? e a1) | @(fi ?? e a1) - | @(if ?? e1 b1) - | @(fi ?? e1 b1)]] + | @(if ?? e1 a1) + | @(fi ?? e1 a1)]] qed. interpretation "or_morphism" 'or a b = (fun21 ??? or_morphism a b). definition if_morphism: binary_morphism1 CPROP CPROP CPROP. - constructor 1; + @mk_binary_morphism1 [ @(λA,B. A → B) - | intros; split; intros; - [ @(if ?? e1); @f; @(fi ?? e); assumption - | @(fi ?? e1); @f; @(if ?? e); assumption]] + | #a #a' #b #b' #e #e1 @mk_Iff #f #a1 + [ @(if ?? e1) @f @(fi ?? e) assumption + | @(fi ?? e1) @f @(if ?? e) assumption]] qed. - +(* notation > "hvbox(a break ∘ b)" left associative with precedence 55 for @{ comp ??? $a $b }. +*) record category : Type[1] ≝ { objs:> Type[0]; arrows: objs → objs → setoid; id: ∀o:objs. arrows o o; comp: ∀o1,o2,o3. (arrows o1 o2) × (arrows o2 o3) ⇒ (arrows o1 o3); comp_assoc: ∀o1,o2,o3,o4.∀a12:arrows o1 ?.∀a23:arrows o2 ?.∀a34:arrows o3 o4. - (a12 ∘ a23) ∘ a34 =_0 a12 ∘ (a23 ∘ a34); - id_neutral_left : ∀o1,o2. ∀a: arrows o1 o2. (id o1) ∘ a =_0 a; - id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. a ∘ (id o2) =_0 a + comp o1 o3 o4 (comp o1 o2 o3 a12 a23) a34 =_0 comp o1 o2 o4 a12 (comp o2 o3 o4 a23 a34); + id_neutral_left : ∀o1,o2. ∀a: arrows o1 o2. comp ??? (id o1) a =_0 a; + id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o2) =_0 a }. +(* notation "hvbox(a break ∘ b)" left associative with precedence 55 for @{ 'compose $a $b }. - +*) record category1 : Type[2] ≝ { objs1:> Type[1]; arrows1: objs1 → objs1 → setoid1; @@ -336,19 +337,18 @@ interpretation "category composition" 'compose x y = (fun2 ??? (comp ????) y x). interpretation "category assoc" 'assoc = (comp_assoc ????????). definition category2_of_category1: category1 → category2. - intro; - constructor 1; - [ @(objs1 c); - | intros; @(setoid2_of_setoid1 (arrows1 c o o1)); - | @(id1 c); - | intros; - constructor 1; - [ intros; @(comp1 c o1 o2 o3 c1 c2); - | intros; unfold setoid2_of_setoid1 in e e1 a a' b b'; simplify in e e1 a a' b b'; - change with ((b∘a) =_1 (b'∘a')); @(e‡e1); ] - | intros; simplify; whd in a12 a23 a34; whd; @rule (ASSOC); - | intros; simplify; whd in a; whd; @id_neutral_right1; - | intros; simplify; whd in a; whd; @id_neutral_left1; ] + #c + @mk_category2 + [ @(objs1 c) + | #o #o1 @(setoid2_of_setoid1 (arrows1 c o o1)) + | @(id1 c) + | #o1 #o2 #o3 + @mk_binary_morphism2 + [ #c1 #c2 @(comp1 c o1 o2 o3 c1 c2) + | #a #a' #b #b' #e #e1 @(e‡e1) ] + | #o1 #o2 #o3 #o4 #a12 #a23 #a34 @comp_assoc1 + | #o1 #o2 #a @id_neutral_right1 + | #o1 #o2 #a @id_neutral_left1 ] qed. (*coercion category2_of_category1.*) @@ -365,11 +365,11 @@ notation "F\sub⇒ x" left associative with precedence 60 for @{'map_arrows2 $F interpretation "map_arrows2" 'map_arrows2 F x = (fun12 ?? (map_arrows2 ?? F ??) x). definition functor2_setoid: category2 → category2 → setoid3. - intros (C1 C2); - constructor 1; - [ @(functor2 C1 C2); - | constructor 1; - [ intros (f g); + #C1 #C2 + @mk_setoid3 + [ @(functor2 C1 C2) + | @mk_equivalence_relation3 + [ #f #g @(∀c:C1. cic:/matita/logic/equality/eq.ind#xpointer(1/1) ? (f c) (g c)); | simplify; intros; @cic:/matita/logic/equality/eq.ind#xpointer(1/1/1); | simplify; intros; @cic:/matita/logic/equality/sym_eq.con; @H;