From: Ferruccio Guidi Date: Sun, 10 Mar 2013 17:05:30 +0000 (+0000) Subject: - improved Makefile esp. with the "trim" function X-Git-Tag: make_still_working~1224 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=08cb57944c0df08611d4f35d286e46c0d13e4813 - improved Makefile esp. with the "trim" function - some files trimmed --- diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index 8b6f8e6ed..f8115150d 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -1,24 +1,31 @@ -OPEN = ( +OPEN := ( +H := @ -H = @ -XOA_DIR = ../../../components/binaries/xoa -XOA = xoa.native -DEP_DIR = ../../../components/binaries/matitadep -DEP = matitadep.native -MAC_DIR = ../../../components/binaries/mac -MAC = mac.native -PRB_DIR = ../../../components/binaries/probe -PRB = probe.native -PRB_OPTS = ../../matita.conf.xml -g +TRIM := sed "s/ \\+$$//" -XOA_CONF = ground_2/xoa.conf.xml -XOA_TARGETS = ground_2/xoa_notation.ma ground_2/xoa.ma +XOA_DIR := ../../../components/binaries/xoa +XOA := xoa.native +DEP_DIR := ../../../components/binaries/matitadep +DEP := matitadep.native +MAC_DIR := ../../../components/binaries/mac +MAC := mac.native +PRB_DIR := ../../../components/binaries/probe +PRB := probe.native +PRB_OPTS := ../../matita.conf.xml -g -ORIG = . ./orig.sh +XOA_CONF := ground_2/xoa.conf.xml +XOA_TARGETS := ground_2/xoa_notation.ma ground_2/xoa.ma -ORIGS = basic_2/basic_1.orig +ORIG := . ./orig.sh -PACKAGES = ground_2 basic_2 apps_2 +ORIGS := basic_2/basic_1.orig + +TAGS := all xoa orig deps stats tbls trim + +PACKAGES := ground_2 basic_2 apps_2 + +LDWS := $(shell find -name "*.ldw.xml") +TBLS := $(shell find -name "*.tbl") all: ../../matitac.opt @@ -28,6 +35,10 @@ all: define MAS_TEMPLATE MAS_$(1) := $$(shell find $(1) -name "*.ma") MAS += $$(MAS_$(1)) + +$(1)/$(1)_probe.txt: $$(MAS_$(1)) + @echo " PROBE $(1)" + $$(H)$$(PRB_DIR)/$$(PRB) $$(PRB_OPTS) $(1) -sn -on -i > $$@ endef $(foreach PKG, $(PACKAGES), $(eval $(call MAS_TEMPLATE,$(PKG)))) @@ -44,7 +55,7 @@ $(XOA_TARGETS): $(XOA_CONF) orig: $(ORIGS) @echo " ORIG basic_2" - $(H)$(ORIG) basic_2 < $(ORIGS) + $(H)$(ORIG) basic_2 < $< # dep ######################################################################## @@ -58,52 +69,55 @@ define STATS_TEMPLATE STT_$(1) := $(1).stats STTS += $$(STT_$(1)) - $$(STT_$(1)): S1 = $$(shell $$(MAC_DIR)/$$(MAC) $$(MAS_$(1))) - $$(STT_$(1)): S2 := $$(shell echo $$$$(($$(S1) / 5120))) - $$(STT_$(1)): S4 := $$(shell ls $$(MAS_$(1)) | wc -l) - $$(STT_$(1)): S5 := $$(shell $$(PRB_DIR)/$$(PRB) $$(PRB_OPTS) $(1) -sn -on) - $$(STT_$(1)): P1 := $$(shell grep "theorem " $$(MAS_$(1)) | wc -l) - $$(STT_$(1)): P2 := $$(shell grep "lemma " $$(MAS_$(1)) | wc -l) - $$(STT_$(1)): P3 := $$(shell grep "fact " $$(MAS_$(1)) | wc -l) - $$(STT_$(1)): P4 := $$(shell grep qed $$(MAS_$(1)) | wc -l) - $$(STT_$(1)): C1 := $$(shell grep "inductive \|record " $$(MAS_$(1)) | wc -l) - $$(STT_$(1)): C2 := $$(shell grep "definition \|let rec " $$(MAS_$(1)) | wc -l) - $$(STT_$(1)): M1 := $$(shell grep "axiom " $$(MAS_$(1)) | wc -l) - $$(STT_$(1)): M2 := $$(shell grep "$$(OPEN)\*[^*:]*$$$$" $$(MAS_$(1)) | wc -l) - $$(STT_$(1)): M3 := $$(shell grep "(\*\*)" $$(MAS_$(1)) | wc -l) - -$$(STT_$(1)): + $$(STT_$(1)): S1 := $$(shell $$(MAC_DIR)/$$(MAC) $$(MAS_$(1))) + $$(STT_$(1)): S2 = $$(shell echo $$$$(($$(S1) / 5120))) + $$(STT_$(1)): S4 = $$(shell ls $$(MAS_$(1)) | wc -l) + $$(STT_$(1)): S5 = $$(shell cat $(1)/$(1)_probe.txt) + $$(STT_$(1)): P1 = $$(shell grep "theorem " $$(MAS_$(1)) | wc -l) + $$(STT_$(1)): P2 = $$(shell grep "lemma " $$(MAS_$(1)) | wc -l) + $$(STT_$(1)): P3 = $$(shell grep "fact " $$(MAS_$(1)) | wc -l) + $$(STT_$(1)): P4 = $$(shell grep qed $$(MAS_$(1)) | wc -l) + $$(STT_$(1)): C1 = $$(shell grep "inductive \|record " $$(MAS_$(1)) | wc -l) + $$(STT_$(1)): C2 = $$(shell grep "definition \|let rec " $$(MAS_$(1)) | wc -l) + $$(STT_$(1)): M1 = $$(shell grep "axiom " $$(MAS_$(1)) | wc -l) + $$(STT_$(1)): M2 = $$(shell grep "$$(OPEN)\*[^*:]*$$$$" $$(MAS_$(1)) | wc -l) + $$(STT_$(1)): M3 = $$(shell grep "(\*\*)" $$(MAS_$(1)) | wc -l) + +$$(STT_$(1)): $$(MAS_$(1)) $(1)/$(1)_probe.txt @printf '\x1B[1;40;37m' - @printf '%-15s %-44s' 'Statistics for:' $(1) + @printf '%-15s %-47s' 'Statistics for:' $(1) @printf '\x1B[0m\n' @printf '\x1B[1;40;35m' @printf '%-8s %6i' Chars $$(S1) @printf ' %-8s %4i' Pages $$(S2) - @printf ' %-26s' '' + @printf ' %-7s %7i' Nodes $$(word 3, $$(S5)) + @printf ' %-11s' '' @printf '\x1B[0m\n' @printf '\x1B[1;40;36m' @printf '%-8s %6i' Files $$(S4) - @printf ' %-8s %4i' Sources $$(word 1, $$(S5)) - @printf ' %-7s %4i' Objects $$(word 2, $$(S5)) + @printf ' %-8s %4i' Sources $$(word 1, $$(S5)) + @printf ' %-7s %7i' Objects $$(word 2, $$(S5)) @printf ' %-11s' '' @printf '\x1B[0m\n' @printf '\x1B[1;40;32m' @printf '%-8s %6i' Theorems $$(P1) @printf ' %-8s %4i' Lemmas $$(P2) - @printf ' %-7s %4i' Facts $$(P3) + @printf ' %-7s %7i' Facts $$(P3) @printf ' %-6s %4i' Proofs $$(P4) @printf '\x1B[0m\n' @printf '\x1B[1;40;33m' @printf '%-8s %6i' Declared $$(C1) @printf ' %-8s %4i' Defined $$(C2) - @printf ' %-26s' '' + @printf ' %-29s' '' @printf '\x1B[0m\n' @printf '\x1B[1;40;31m' @printf '%-8s %6i' Axioms $$(M1) @printf ' %-8s %4i' Comments $$(M2) - @printf ' %-7s %4i' Marks $$(M3) + @printf ' %-7s %7i' Marks $$(M3) @printf ' %-11s' '' @printf '\x1B[0m\n' + +.PHONY: $$(STT_$(1)) endef ifeq ($(MAKECMDGOALS), stats) @@ -115,49 +129,65 @@ stats: $(STTS) # summary #################################################################### define SUMMARY_TEMPLATE - TBL_$(1) := $(1)/web/$(1)_sum.tbl - TBLS += $$(TBL_$(1)) - - $$(TBL_$(1)): S1 := $$(shell ls $$(MAS_$(1)) | wc -l) - $$(TBL_$(1)): S2 := $$(shell $$(MAC_DIR)/$$(MAC) $$(MAS_$(1))) - $$(TBL_$(1)): S3 := $$(shell $$(PRB_DIR)/$$(PRB) $$(PRB_OPTS) $(1) -i) - $$(TBL_$(1)): C1 := $$(shell grep "inductive \|record " $$(MAS_$(1)) | wc -l) - $$(TBL_$(1)): C2 := $$(shell grep "definition \|let rec " $$(MAS_$(1)) | wc -l) - $$(TBL_$(1)): C3 := $$(shell grep "inductive \|record \|definition \|let rec " $$(MAS_$(1)) | wc -l) - $$(TBL_$(1)): P1 := $$(shell grep "theorem " $$(MAS_$(1)) | wc -l) - $$(TBL_$(1)): P2 := $$(shell grep "lemma " $$(MAS_$(1)) | wc -l) - $$(TBL_$(1)): P3 := $$(shell grep "lemma \|theorem " $$(MAS_$(1)) | wc -l) - - $$(TBL_$(1)): $$(MAS_$(1)) + SUM_$(1) := $(1)/web/$(1)_sum.tbl + SUMS += $$(SUM_$(1)) + + $$(SUM_$(1)): S1 = $$(shell ls $$(MAS_$(1)) | wc -l) + $$(SUM_$(1)): S2 = $$(shell $$(MAC_DIR)/$$(MAC) $$(MAS_$(1))) + $$(SUM_$(1)): S3 = $$(shell cat $(1)/$(1)_probe.txt) + $$(SUM_$(1)): C1 = $$(shell grep "inductive \|record " $$(MAS_$(1)) | wc -l) + $$(SUM_$(1)): C2 = $$(shell grep "definition \|let rec " $$(MAS_$(1)) | wc -l) + $$(SUM_$(1)): C3 = $$(shell grep "inductive \|record \|definition \|let rec " $$(MAS_$(1)) | wc -l) + $$(SUM_$(1)): P1 = $$(shell grep "theorem " $$(MAS_$(1)) | wc -l) + $$(SUM_$(1)): P2 = $$(shell grep "lemma " $$(MAS_$(1)) | wc -l) + $$(SUM_$(1)): P3 = $$(shell grep "lemma \|theorem " $$(MAS_$(1)) | wc -l) + + $$(SUM_$(1)): $$(MAS_$(1)) $(1)/$(1)_probe.txt @printf ' SUMMARY $(1)\n' - @printf 'name "$$(basename $$(@F))"\n\n' > $$@ - @printf 'table {\n' >> $$@ - @printf ' class "grey" [ "category"\n' >> $$@ - @printf ' [ "objects" * ]\n' >> $$@ - @printf ' ]\n' >> $$@ - @printf ' class "cyan" [ "sizes"\n' >> $$@ - @printf ' [ "files" "$$(S1)" ]\n' >> $$@ - @printf ' [ "characters" "$$(S2)" ]\n' >> $$@ - @printf ' [ "nodes" "$$(S3)" ]\n' >> $$@ - @printf ' ]\n' >> $$@ - @printf ' class "green" [ "propositions"\n' >> $$@ - @printf ' [ "theorems" "$$(P1)" ]\n' >> $$@ - @printf ' [ "lemmas" "$$(P2)" ]\n' >> $$@ - @printf ' [ "total" "$$(P3)" ]\n' >> $$@ - @printf ' ]\n' >> $$@ - @printf ' class "yellow" [ "concepts"\n' >> $$@ - @printf ' [ "declared" "$$(C1)" ]\n' >> $$@ - @printf ' [ "defined" "$$(C2)" ]\n' >> $$@ - @printf ' [ "total" "$$(C3)" ]\n' >> $$@ - @printf ' ]\n' >> $$@ - @printf '}\n\n' >> $$@ - @printf 'class "component" { 0 }\n\n' >> $$@ - @printf 'class "plane" { 1 } { 3 } { 5 }\n\n' >> $$@ - @printf 'class "number" { 2 } { 4 } { 6 }\n\n' >> $$@ + @printf 'name "$$(basename $$(@F))"\n\n' > $$@ + @printf 'table {\n' >> $$@ + @printf ' class "grey" [ "category"\n' >> $$@ + @printf ' [ "objects" * ]\n' >> $$@ + @printf ' ]\n' >> $$@ + @printf ' class "cyan" [ "sizes"\n' >> $$@ + @printf ' [ "files" "$$(S1)" ]\n' >> $$@ + @printf ' [ "characters" "$$(S2)" ]\n' >> $$@ + @printf ' [ "nodes" "$$(word 3, $$(S5))" ]\n' >> $$@ + @printf ' ]\n' >> $$@ + @printf ' class "green" [ "propositions"\n' >> $$@ + @printf ' [ "theorems" "$$(P1)" ]\n' >> $$@ + @printf ' [ "lemmas" "$$(P2)" ]\n' >> $$@ + @printf ' [ "total" "$$(P3)" ]\n' >> $$@ + @printf ' ]\n' >> $$@ + @printf ' class "yellow" [ "concepts"\n' >> $$@ + @printf ' [ "declared" "$$(C1)" ]\n' >> $$@ + @printf ' [ "defined" "$$(C2)" ]\n' >> $$@ + @printf ' [ "total" "$$(C3)" ]\n' >> $$@ + @printf ' ]\n' >> $$@ + @printf '}\n\n' >> $$@ + @printf 'class "component" { 0 }\n\n' >> $$@ + @printf 'class "plane" { 1 } { 3 } { 5 }\n\n' >> $$@ + @printf 'class "number" { 2 } { 4 } { 6 }\n\n' >> $$@ endef ifeq ($(MAKECMDGOALS), tbls) $(foreach PKG, $(PACKAGES), $(eval $(call SUMMARY_TEMPLATE,$(PKG)))) endif -tbls: $(TBLS) +tbls: $(SUMS) + +# trim ####################################################################### + +TRIMS := $(MAS) $(TBLS) $(LDWS) + +%.trimmed: % + $(H)expand $< | $(TRIM) > $@ + $(H)if diff $< $@ > /dev/null; then $(RM) $@; else echo " TRIM $<" & mv $@ $<; fi + +trim: $(TRIMS:%=%.trimmed) + +############################################################################## + +.PHONY: $(TAGS) + +.SUFFIXES: diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/dsubst.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/dsubst.ma index 20e372bb6..c43cd1d74 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/functional/dsubst.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/functional/dsubst.ma @@ -41,7 +41,7 @@ theorem fdsubst_delift: ∀K,V,T,L,d. [ * #i #L #d #HLK normalize in ⊢ (? ? ? ? ? %); /2 width=3/ elim (lt_or_eq_or_gt i d) #Hid [ -HLK >(tri_lt ?????? Hid) /3 width=3/ - | destruct >tri_eq /4 width=4 by tpss_strap2, tps_subst, le_n, ex2_intro/ (**) (* too slow without trace *) + | destruct >tri_eq /4 width=4 by tpss_strap2, tps_subst, le_n, ex2_intro/ (**) (* too slow without trace *) | -HLK >(tri_gt ?????? Hid) /3 width=3/ ] | * /3 width=1/ /4 width=1/ diff --git a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml index 394568e00..1f61d9305 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml @@ -8,17 +8,17 @@
Contents of the Specification
This specification comprises a collection of checked applications of λδ version 2. - In particular it contains the components below. + In particular it contains the components below. Martin-Löf's Type Theory with one universe - using λδ as theory of expressions. + using λδ as theory of expressions. The validation algorithm for λδ as implemented in - Helena 0.8. + Helena 0.8. - +
Summary of the Specification
Here is a numerical acount of the specification's contents and its timeline. @@ -29,7 +29,7 @@ The Functional component is started - inside the specification of λδ version 2. + inside the specification of λδ version 2. The MLTT1 component is started. @@ -39,8 +39,8 @@ The source files are grouped in planes and components according to the following table. Each component contains its own notation file. - The notation for the relations or functions introduced in each file - is shown in parentheses (? are placeholders). + The notation for the relations or functions introduced in each file + is shown in parentheses (? are placeholders). diff --git a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl index d5508e3d6..556df99a7 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl @@ -3,29 +3,29 @@ name "apps_2_src" table { class "grey" [ { "component" * } { - [ { "plane" * } { + [ { "plane" * } { [ "files" * ] - } + } ] } ] class "orange" [ { "MLTT1" * } { - [ { "" * } { + [ { "" * } { [ "genv_primitive" "judgement" * ] - } + } ] } ] class "red" [ { "functional" * } { - [ { "reduction and type machine" * } { + [ { "reduction and type machine" * } { [ "rtm" "rtm_step ( ? ⇨ ? )" * ] - } + } ] - [ { "unfold" * } { + [ { "unfold" * } { [ "lift ( ↑[?,?] ? )" "subst ( [?←?] ? )" * ] - } + } ] } ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma index dc046b094..b7b967e1a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma @@ -26,7 +26,7 @@ definition CP3 ≝ λRR:lenv→relation term. λRP:lenv→predicate term. ∀L,V,k. RP L (ⓐ⋆k.V) → RP L V. definition CP4 ≝ λRR:lenv→relation term. λRS:relation term. - ∀L0,L,T,T0,d,e. NF … (RR L) RS T → + ∀L0,L,T,T0,d,e. NF … (RR L) RS T → ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → NF … (RR L0) RS T0. definition CP4s ≝ λRR:lenv→relation term. λRS:relation term. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma index b0b15e665..e8dfcbfde 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma @@ -89,7 +89,7 @@ qed. lemma rp_lifts: ∀RR,RS,RP. acr RR RS RP (λL,T. RP L T) → ∀des,L0,L,V,V0. ⇩*[des] L0 ≡ L → ⇧*[des] V ≡ V0 → RP L V → RP L0 V0. -#RR #RS #RP #HRP #des #L0 #L #V #V0 #HL0 #HV0 #HV +#RR #RS #RP #HRP #des #L0 #L #V #V0 #HL0 #HV0 #HV @acr_lifts /width=6/ @(s7 … HRP) qed. @@ -103,9 +103,9 @@ lemma rp_liftsv_all: ∀RR,RS,RP. acr RR RS RP (λL,T. RP L T) → @conj /2 width=1/ /2 width=6 by rp_lifts/ qed. -(* Basic_1: was: +(* Basic_1: was: sc3_sn3 sc3_abst sc3_appl sc3_abbr sc3_bind sc3_cast sc3_lift -*) +*) lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → ∀A. acr RR RS RP (aacr RP A). #RR #RS #RP #H1RP #H2RP #A elim A -A normalize // diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma index 3326b8b46..c89fab769 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma @@ -70,7 +70,7 @@ lemma cprs_inv_appl1: ∀L,V1,T1,U2. L ⊢ ⓐV1. T1 ➡* U2 → [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/ | #a #V2 #W2 #T #T2 #HV02 #HT2 #H1 #H2 destruct /4 width=7/ | #a #V #V2 #W0 #W2 #T #T2 #HV0 #HW02 #HT2 #HV2 #H1 #H2 destruct - @or3_intro2 @(ex4_5_intro … HV2 HT10) /2 width=3/ /3 width=1/ (**) (* explicit constructor. /5 width=8/ is too slow because TC_transitive gets in the way *) + @or3_intro2 @(ex4_5_intro … HV2 HT10) /2 width=3/ /3 width=1/ (**) (* explicit constructor. /5 width=8/ is too slow because TC_transitive gets in the way *) ] | /4 width=9/ | /4 width=11/ @@ -115,7 +115,7 @@ qed. lemma cprs_bind1: ∀I,L,V1,T1,T2. L. ⓑ{I}V1 ⊢ T1 ➡* T2 → ∀V2. L ⊢ V1 ➡* V2 → ∀a. L ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2. * /2 width=1/ /2 width=2/ -qed. +qed. lemma cprs_abbr2_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV2 ⊢ T1 ➡* T2 → ∀a. L ⊢ ⓓ{a}V1. T1 ➡* ⓓ{a}V2. T2. @@ -135,10 +135,10 @@ lapply (IHV1 T1 T1 ? a) -IHV1 // #HV1 @(cprs_trans … HV1) -HV1 /2 width=1/ qed. -lemma cprs_bind2: ∀L,V1,V2. L ⊢ V1 ➡* V2 → ∀I,T1,T2. L. ⓑ{I}V2 ⊢ T1 ➡* T2 → +lemma cprs_bind2: ∀L,V1,V2. L ⊢ V1 ➡* V2 → ∀I,T1,T2. L. ⓑ{I}V2 ⊢ T1 ➡* T2 → ∀a. L ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2. #L #V1 #V2 #HV12 * /2 width=1/ /2 width=2/ -qed. +qed. lemma cprs_beta_dx: ∀L,V1,V2,W,T1,T2. L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T1 ➡* T2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tstc_vector.ma index fd3eb585e..8babd61ba 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tstc_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tstc_vector.ma @@ -130,7 +130,7 @@ elim (cprs_inv_appl1 … H) -H * @(cprs_strap2 … (ⓓ{b}V0.ⓐV2a.T0)) [ /3 width=3/ ] -V1a /3 width=1/ ] ] -] +] qed-. (* Basic_1: was: pr3_iso_appls_cast *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma index 3ed310164..2a7f4b7b2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn.ma @@ -61,7 +61,7 @@ elim (cpr_inv_cast1 … H1) -H1 [ * #W0 #T0 #HLW0 #HLT0 #H destruct elim (eq_false_inv_tpair_sn … H2) -H2 [ /3 width=3/ - | -HLW0 * #H destruct /3 width=1/ + | -HLW0 * #H destruct /3 width=1/ ] | /3 width=3/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_aaa.ma index 67744a098..109d93018 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_aaa.ma @@ -22,4 +22,4 @@ include "basic_2/computation/csn_tstc_vector.ma". lemma csn_aaa: ∀L,T,A. L ⊢ T ⁝ A → L ⊢ ⬊* T. #L #T #A #H @(acp_aaa … csn_acp csn_acr … H) -qed. +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_alt.ma index eeba707dc..c880b2dd2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_alt.ma @@ -68,7 +68,7 @@ lemma csna_intro_cpr: ∀L,T1. [ -HLT1 -HLT2 -H /3 width=1/ | -IHT -HT12 /4 width=3/ ] -] +] qed. (* Main properties **********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_tstc_vector.ma index cfee668b9..81b8696b4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_tstc_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_tstc_vector.ma @@ -22,7 +22,7 @@ include "basic_2/computation/csn_vector.ma". (* Advanced properties ******************************************************) (* Basic_1: was only: sn3_appls_lref *) -lemma csn_applv_cnf: ∀L,T. 𝐒⦃T⦄ → L ⊢ 𝐍⦃T⦄ → +lemma csn_applv_cnf: ∀L,T. 𝐒⦃T⦄ → L ⊢ 𝐍⦃T⦄ → ∀Vs. L ⊢ ⬊* Vs → L ⊢ ⬊* ⒶVs.T. #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(csn_cnf … H2T) ] (**) (* /2 width=1/ does not work *) #V #Vs #IHV #H @@ -68,12 +68,12 @@ lemma csn_applv_delta: ∀L,K,V1,i. ⇩[0, i] L ≡ K. ⓓV1 → ] qed. -(* Basic_1: was: sn3_appls_abbr *) +(* Basic_1: was: sn3_appls_abbr *) lemma csn_applv_theta: ∀a,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → ∀V,T. L ⊢ ⬊* ⓓ{a}V. ⒶV2s. T → L ⊢ ⬊* V → L ⊢ ⬊* ⒶV1s. ⓓ{a}V. T. #a #L #V1s #V2s * -V1s -V2s /2 width=1/ -#V1s #V2s #V1 #V2 #HV12 #H +#V1s #V2s #V1 #V2 #HV12 #H generalize in match HV12; -HV12 generalize in match V2; -V2 generalize in match V1; -V1 elim H -V1s -V2s /2 width=3/ #V1s #V2s #V1 #V2 #HV12 #HV12s #IHV12s #W1 #W2 #HW12 #V #T #H #HV diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lift.ma index 431a9f511..628563cf4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lift.ma @@ -30,7 +30,7 @@ qed-. (* Advanced properties ******************************************************) -lemma ssta_cprs_dxprs: ∀h,g,L,T1,T,T2,l. ⦃h, L⦄ ⊢ T1 •[g, l+1] T → +lemma ssta_cprs_dxprs: ∀h,g,L,T1,T,T2,l. ⦃h, L⦄ ⊢ T1 •[g, l+1] T → L ⊢ T ➡* T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2. /3 width=3/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fprs_cprs.ma index b65cd73f5..9d4d954b8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fprs_cprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fprs_cprs.ma @@ -48,7 +48,7 @@ lemma fprs_lift: ∀K1,K2,T1,T2. ⦃K1, T1⦄ ➡* ⦃K2, T2⦄ → elim (IHT1 … HLK1 … HTU1 HTU) -K1 -T1 #L #HU1 #HKL elim (fpr_lift … HT2 … HKL … HTU HTU2) -K -T -T2 /3 width=4/ ] -qed-. +qed-. (* Advanced inversion lemmas ************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma index 92ed705fe..9979efb4e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma @@ -58,7 +58,7 @@ qed-. lemma lsubsv_inv_pair1: ∀h,g,I,K1,L2,V1. h ⊢ K1. ⓑ{I} V1 ⊩:⊑[g] L2 → (∃∃K2. h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓑ{I} V1) ∨ - ∃∃K2,W1,W2,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 & + ∃∃K2,W1,W2,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 & K1 ⊢ W2 ⬌* W1 & ⦃h, K2⦄ ⊩ W2 :[g] & h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓛW2 & I = Abbr. /2 width=3 by lsubsv_inv_pair1_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma index 982d7edaf..538de0334 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma @@ -96,7 +96,7 @@ lemma snv_inv_appl: ∀h,g,L,V,T. ⦃h, L⦄ ⊩ ⓐV.T :[g] → /2 width=3/ qed-. fact snv_inv_cast_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀W,T. X = ⓝW.T → - ∃∃U,l. ⦃h, L⦄ ⊩ W :[g] & ⦃h, L⦄ ⊩ T :[g] & + ∃∃U,l. ⦃h, L⦄ ⊩ W :[g] & ⦃h, L⦄ ⊩ T :[g] & ⦃h, L⦄ ⊢ T •[g, l + 1] U & L ⊢ U ⬌* W. #h #g #L #X * -L -X [ #L #k #W #T #H destruct @@ -123,6 +123,6 @@ lemma snv_fwd_ssta: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → ∃∃U,l. ⦃h, L⦄ ] | #a #I #L #V #T #_ #_ #_ * /3 width=3/ | #a #L #V #W #W1 #T0 #T1 #l #_ #_ #_ #_ #_ #_ * /3 width=3/ -| #L #W #T #U #l #_ #_ #HTU #_ #_ #_ /3 width=3/ (**) (* auto fails without the last #_ *) +| #L #W #T #U #l #_ #_ #HTU #_ #_ #_ /3 width=3/ (**) (* auto fails without the last #_ *) ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma index c17f7e071..ba47b1e47 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma @@ -74,4 +74,4 @@ fact snv_ltpr_tpr_aux: ∀h,g,L0,T0. elim (IH3 … HVW1 … HL12 … HV12) // [2: /2 width=1/ ] -HV1 -HVW1 -HV12 #W200 #HVW200 #H lapply (cpcs_trans … HW210 … H) -W10 #HW200 lapply (lsubsv_snv_trans … HT2 (L2.ⓓV2) ?) -L1 -HT2 /2 width=1/ /2 width=4/ - | \ No newline at end of file + | \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta.ma index f32e1ba01..f6d753d22 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta.ma @@ -47,7 +47,7 @@ fact snv_ssta_aux: ∀h,g,L0,T0. elim (cprs_inv_abst … HU02 Abst W0) -HU02 #HW02 #_ lapply (cprs_trans … HW10 … HW02) -W0 /3 width=10 by snv_appl, ex2_intro/ (**) (* auto is too slow without trace *) | #W1 #T1 #HL0 #HT0 #H1 #X #l #H2 destruct -IH3 -IH2 - elim (snv_inv_cast … H1) -H1 #U1 #l0 #HW1 #HT1 #HTU1 #HUW1 + elim (snv_inv_cast … H1) -H1 #U1 #l0 #HW1 #HT1 #HTU1 #HUW1 lapply (ssta_inv_cast1 … H2) -H2 /3 width=5/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_ltpr.ma index a82640426..131aa1c49 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_ltpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_ltpr.ma @@ -102,7 +102,7 @@ fact ssta_ltpr_tpr_aux: ∀h,g,L0,T0. elim (IH1 … HTU0 (L2.ⓓW2) … HT02) -IH1 -HTU0 // [2,3: /2 width=1/ ] -T0 -HL12 #U2 #HTU2 #HU02 lapply (cpcs_bind2 … W0 … HU02 b) -HU02 [ /2 width=1/ ] #HU02 lapply (cpcs_flat … V1 V0 … HU02 Appl) [ /2 width=1/ ] -HV10 -HU02 #HU02 - lapply (cpcs_cpr_strap1 … HU02 (ⓓ{b}W2.ⓐV2.U2) ?) -HU02 [ /3 width=3/ ] -V0 -HW02 /4 width=3/ + lapply (cpcs_cpr_strap1 … HU02 (ⓓ{b}W2.ⓐV2.U2) ?) -HU02 [ /3 width=3/ ] -V0 -HW02 /4 width=3/ ] | #U0 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #L2 #HL12 #X3 #H3 destruct -IH3 -IH2 elim (snv_inv_cast … H1) -H1 #T0 #l0 #_ #HT1 #HT10 #_ diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma index 8b2259dac..44d59982c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma @@ -87,7 +87,7 @@ lemma cpr_div: ∀L,T1,T. L ⊢ T1 ➡ T → ∀T2. L ⊢ T2 ➡ T → L ⊢ T1 lemma cpcs_cpr_conf: ∀L,T1,T. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2. /3 width=3/ qed. -lemma cpcs_tpss_strap1: ∀L,T1,T. L ⊢ T1 ⬌* T → +lemma cpcs_tpss_strap1: ∀L,T1,T. L ⊢ T1 ⬌* T → ∀T2,d,e. L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ⬌* T2. #L #T1 #T #HT1 #T2 #d #e #HT2 @(cpcs_cpr_strap1 … HT1) -T1 /2 width=3/ @@ -103,7 +103,7 @@ qed-. clear_pc3_trans pc3_ind_left pc3_head_1 pc3_head_2 pc3_head_12 pc3_head_21 pc3_pr2_fsubst0 pc3_pr2_fsubst0_back pc3_fsubst0 -*) +*) (* Basic_1: removed local theorems 6: pc3_left_pr3 pc3_left_trans pc3_left_sym pc3_left_pc3 pc3_pc3_left pc3_wcpr0_t_aux diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma index 35dcf5fc3..a31853a7f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma @@ -215,7 +215,7 @@ lemma cpcs_bind1: ∀I,L,V1,T1,T2. L.ⓑ{I}V1 ⊢ T1 ⬌* T2 → ∀V2. L ⊢ V1 * /2 width=1/ /2 width=2/ qed. -lemma cpcs_bind2: ∀L,V1,V2. L ⊢ V1 ⬌* V2 → ∀I,T1,T2. L.ⓑ{I}V2 ⊢ T1 ⬌* T2 → +lemma cpcs_bind2: ∀L,V1,V2. L ⊢ V1 ⬌* V2 → ∀I,T1,T2. L.ⓑ{I}V2 ⊢ T1 ⬌* T2 → ∀a. L ⊢ ⓑ{a,I}V1. T1 ⬌* ⓑ{a,I}V2. T2. #L #V1 #V2 #HV12 * /2 width=1/ /2 width=2/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_shift.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_shift.ma index bbdc8e7d0..66e54a909 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_shift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_shift.ma @@ -43,4 +43,3 @@ lemma shift_inj: ∀L1,L2. ∀T1,T2:term. L1 @@ T1 = L2 @@ T2 → |L1| = |L2| ] ] qed-. - \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma index 0916ac9e3..c7d7ac9ca 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma @@ -85,7 +85,7 @@ qed-. lemma length_inv_pos_dx_append: ∀d,L. |L| = d + 1 → ∃∃I,K,V. |K| = d & L = ⋆.ⓑ{I}V @@ K. #d @(nat_ind_plus … d) -d -[ #L #H +[ #L #H elim (length_inv_pos_dx … H) -H #I #K #V #H >(length_inv_zero_dx … H) -H #H destruct @ex2_3_intro [4: /2 width=2/ |5: // |1,2,3: skip ] (**) (* /3/ does not work *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px.ma index 11bd6822e..ea916e10a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_px.ma @@ -80,7 +80,7 @@ lemma lpx_inv_append1: ∀R,L1,K1,L. lpx R (K1 @@ L1) L → ∃∃K2,L2. lpx R K1 K2 & lpx R L1 L2 & L = K2 @@ L2. #R #L1 elim L1 -L1 normalize [ #K1 #K2 #HK12 - @(ex3_2_intro … K2 (⋆)) // (**) (* explicit constructor, /2 width=5/ does not work *) + @(ex3_2_intro … K2 (⋆)) // (**) (* explicit constructor, /2 width=5/ does not work *) | #L1 #I #V1 #IH #K1 #X #H elim (lpx_inv_pair1 … H) -H #L #V2 #H1 #HV12 #H destruct elim (IH … H1) -IH -H1 #K2 #L2 #HK12 #HL12 #H destruct @@ -92,13 +92,13 @@ lemma lpx_inv_append2: ∀R,L2,K2,L. lpx R L (K2 @@ L2) → ∃∃K1,L1. lpx R K1 K2 & lpx R L1 L2 & L = K1 @@ L1. #R #L2 elim L2 -L2 normalize [ #K2 #K1 #HK12 - @(ex3_2_intro … K1 (⋆)) // (**) (* explicit constructor, /2 width=5/ does not work *) + @(ex3_2_intro … K1 (⋆)) // (**) (* explicit constructor, /2 width=5/ does not work *) | #L2 #I #V2 #IH #K2 #X #H elim (lpx_inv_pair2 … H) -H #L #V1 #H1 #HV12 #H destruct elim (IH … H1) -IH -H1 #K1 #L1 #HK12 #HL12 #H destruct @(ex3_2_intro … HK12) [2: /2 width=2/ | skip | // ] (* explicit constructor, /3 width=5/ does not work *) ] -qed-. +qed-. (* Basic properties *********************************************************) @@ -126,7 +126,7 @@ lemma lpx_conf: ∀R. confluent ? R → confluent … (lpx R). ] qed. -lemma lpx_TC_inj: ∀R,L1,L2. lpx R L1 L2 → lpx (TC … R) L1 L2. +lemma lpx_TC_inj: ∀R,L1,L2. lpx R L1 L2 → lpx (TC … R) L1 L2. #R #L1 #L2 #H elim H -L1 -L2 // /3 width=1/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma index 5ccb5e4ac..9e6e55ed0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma @@ -104,7 +104,7 @@ lemma eq_false_inv_tpair_sn: ∀I,V1,T1,V2,T2. (V1 = V2 → ⊥) ∨ (V1 = V2 ∧ (T1 = T2 → ⊥)). #I #V1 #T1 #V2 #T2 #H elim (term_eq_dec V1 V2) /3 width=1/ #HV12 destruct -@or_intror @conj // #HT12 destruct /2 width=1/ +@or_intror @conj // #HT12 destruct /2 width=1/ qed-. lemma eq_false_inv_tpair_dx: ∀I,V1,T1,V2,T2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr.ma index 95c01d19f..e1e3c4386 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr.ma @@ -30,7 +30,7 @@ lemma cfpr_refl: ∀L. bi_reflexive … (cfpr L). /2 width=1/ qed. lemma fpr_cfpr: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⋆ ⊢ ⦃L1, T1⦄ ➡ ⦃L2, T2⦄. -#L1 #L2 #T1 #T2 * /3 width=1/ +#L1 #L2 #T1 #T2 * /3 width=1/ qed. (* Basic inversion lemmas ***************************************************) @@ -47,7 +47,7 @@ lemma fpr_inv_pair1_sn: ∀I,K1,L2,V1,T1,T2. ⦃⋆.ⓑ{I}V1@@K1, T1⦄ ➡ ⦃L L2 = ⋆.ⓑ{I}V2@@K2. #I1 #K1 #L2 #V1 #T1 #T2 * >append_length #H elim (length_inv_pos_sn_append … H) -H #I2 #K2 #V2 #HK12 #H destruct ->shift_append_assoc >shift_append_assoc normalize in ⊢ (%→?); #H +>shift_append_assoc >shift_append_assoc normalize in ⊢ (%→?); #H elim (tpr_inv_bind1 … H) -H * [ #V0 #T #T0 #HV10 #HT1 #HT0 #H destruct /5 width=5/ | #T0 #_ #_ #H destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_aaa.ma index 4c9b8ac97..72802e499 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_aaa.ma @@ -22,6 +22,6 @@ include "basic_2/reducibility/cfpr_cpr.ma". lemma aaa_fpr_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → L2 ⊢ T2 ⁝ A. #L1 #T1 #A #HT1 #L2 #T2 #H -elim (fpr_inv_all … H) -H +elim (fpr_inv_all … H) -H /4 width=5 by aaa_cpr_conf, aaa_ltpr_conf, aaa_ltpss_sn_conf/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_ltpss.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_ltpss.ma index 785aefd51..66e102e63 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_ltpss.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_ltpss.ma @@ -26,7 +26,7 @@ lemma cfpr_inv_pair1: ∀I,L,K1,L2,V1,T1,T2. L ⊢ ⦃⋆.ⓑ{I}V1@@K1, T1⦄ L2 = ⋆.ⓑ{I}V2@@K2. * #L #K1 #L2 #V1 #T1 #T2 * >append_length #H elim (length_inv_pos_sn_append … H) -H #I2 #K2 #V2 #HK12 #H destruct ->shift_append_assoc >shift_append_assoc normalize in ⊢ (??%%→?); #H +>shift_append_assoc >shift_append_assoc normalize in ⊢ (??%%→?); #H [ elim (cpr_inv_abbr1 … H) -H * [ #V #V0 #T0 #HV1 #HV0 #HT10 #H destruct /3 width=7/ | #T0 #_ #_ #H destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cif.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cif.ma index 0ea9d519b..0a536a914 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cif.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cif.ma @@ -38,7 +38,7 @@ lemma cif_inv_bind: ∀a,I,L,V,T. L ⊢ 𝐈⦃ⓑ{a,I}V.T⦄ → #a * [ elim a -a ] [ #L #V #T #H elim (H ?) -H /3 width=1/ |*: #L #V #T #H elim (cif_inv_ib2 … H) -H /2 width=1/ /3 width=1/ -] +] qed-. lemma cif_inv_appl: ∀L,V,T. L ⊢ 𝐈⦃ⓐV.T⦄ → ∧∧ L ⊢ 𝐈⦃V⦄ & L ⊢ 𝐈⦃T⦄ & 𝐒⦃T⦄. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_cif.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_cif.ma index 51ce95aa0..8ee507cc1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_cif.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cnf_cif.ma @@ -96,7 +96,7 @@ lemma cnf_crf_false: ∀L,T. L ⊢ 𝐑⦃T⦄ → L ⊢ 𝐍⦃T⦄ → ⊥. | #a #L #V #W #T #H elim (cnf_inv_appl … H) -H #_ #_ #H elim (simple_inv_bind … H) -| #a #L #V #W #T #H +| #a #L #V #W #T #H elim (cnf_inv_appl … H) -H #_ #_ #H elim (simple_inv_bind … H) ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma index ae8e01bbc..56e10d392 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma @@ -41,7 +41,7 @@ lemma cpr_refl: ∀L,T. L ⊢ T ➡ T. /2 width=1/ qed. (* Note: new property *) -(* Basic_1: was only: pr2_thin_dx *) +(* Basic_1: was only: pr2_thin_dx *) lemma cpr_flat: ∀I,L,V1,V2,T1,T2. L ⊢ V1 ➡ V2 → L ⊢ T1 ➡ T2 → L ⊢ ⓕ{I} V1. T1 ➡ ⓕ{I} V2. T2. #I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 * /3 width=5/ @@ -56,7 +56,7 @@ qed. (* Basic_1: was only: pr2_change *) lemma cpr_lsubs_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡ T2 → ∀L2. L2 ≼ [0, |L1|] L1 → L2 ⊢ T1 ➡ T2. -#L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12 +#L1 #T1 #T2 * #T #HT1 #HT2 #L2 #HL12 lapply (tpss_lsubs_trans … HT2 … HL12) -HT2 -HL12 /3 width=4/ qed. @@ -103,7 +103,7 @@ elim (tpr_fwd_shift1 … H1) -H1 #L0 #T0 #HL10 #H destruct elim (tpss_fwd_shift1 … H2) -H2 #L2 #T2 #HL02 #H destruct /2 width=4/ qed-. -(* Basic_1: removed theorems 6: +(* Basic_1: removed theorems 6: pr2_head_2 pr2_cflat pr2_gen_cflat clear_pr2_trans pr2_gen_ctail pr2_ctail Basic_1: removed local theorems 3: diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_cpr.ma index f7738a247..d0738e4c4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_cpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_cpr.ma @@ -35,7 +35,7 @@ lapply (tpss_inv_SO2 … HT0) -HT0 #HT0 @ex2_intro [2: @(tpr_delta … HV12 HT1 HT0) | skip | /2 width=1/ ] (**) (* /3 width=5/ is too slow *) qed. -(* Basic_1: was only: pr2_head_1 *) +(* Basic_1: was only: pr2_head_1 *) lemma cpr_pair_sn: ∀I,L,V1,V2,T1,T2. L ⊢ V1 ➡ V2 → T1 ➡ T2 → L ⊢ ②{I} V1. T1 ➡ ②{I} V2. T2. * /2 width=1/ /3 width=1/ @@ -56,7 +56,7 @@ qed-. theorem cpr_conf: ∀L,U0,T1,T2. L ⊢ U0 ➡ T1 → L ⊢ U0 ➡ T2 → ∃∃T. L ⊢ T1 ➡ T & L ⊢ T2 ➡ T. #L #U0 #T1 #T2 * #U1 #HU01 #HUT1 * #U2 #HU02 #HUT2 -elim (tpr_conf … HU01 HU02) -U0 #U #HU1 #HU2 +elim (tpr_conf … HU01 HU02) -U0 #U #HU1 #HU2 elim (tpr_tpss_ltpr ? L … HU1 … HUT1) -U1 // #U1 #HTU1 #HU1 elim (tpr_tpss_ltpr ? L … HU2 … HUT2) -U2 // #U2 #HTU2 #HU2 elim (tpss_conf_eq … HU1 … HU2) -U /3 width=5/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_fpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_fpr.ma index 9dc995fc7..f798d566b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_fpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr_fpr.ma @@ -22,7 +22,7 @@ include "basic_2/reducibility/cfpr_cpr.ma". lemma fpr_lfpr: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⦃L1⦄ ➡ ⦃L2⦄. #L1 #L2 #T1 #T2 #H elim (fpr_inv_all … H) -H /2 width=3/ -qed. +qed. (* Inversion lemmas on context-free parallel reduction for closures *********) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpss_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpss_sn.ma index 823762356..79ffb7c9e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpss_sn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_ltpss_sn.ma @@ -19,7 +19,7 @@ include "basic_2/reducibility/ltpr_ltpss_dx.ma". (* Properties on sn parallel unfold on local environments *******************) -(* Note: this can also be proved like ltpr_ltpss_dx_conf *) +(* Note: this can also be proved like ltpr_ltpss_dx_conf *) lemma ltpr_ltpss_sn_conf: ∀L1,K1,d,e. L1 ⊢ ▶* [d, e] K1 → ∀L2. L1 ➡ L2 → ∃∃K2. L2 ⊢ ▶* [d, e] K2 & K1 ➡ K2. #L1 #K1 #d #e #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr.ma index 735836d0e..f04b1d972 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr.ma @@ -234,5 +234,5 @@ qed-. (* Basic_1: removed theorems 3: pr0_subst0_back pr0_subst0_fwd pr0_subst0 -*) +*) (* Basic_1: removed local theorems: 1: pr0_delta_tau *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_delift.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_delift.ma index 99e621d15..8e91abc6a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_delift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_delift.ma @@ -24,4 +24,4 @@ lemma tpr_delift_conf: ∀U1,U2. U1 ➡ U2 → ∀L,T1,d,e. L ⊢ ▼*[d, e] U1 #U1 #U2 #HU12 #L #T1 #d #e * #W1 #HUW1 #HTW1 elim (tpr_tpss_conf … HU12 … HUW1) -U1 #U1 #HWU1 #HU21 elim (tpr_inv_lift1 … HWU1 … HTW1) -W1 /3 width=5/ -qed. +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma index efe122261..c12f38cf4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma @@ -199,7 +199,7 @@ qed. (* Basic_1: was: pr0_confluence *) theorem tpr_conf: ∀T0:term. ∀T1,T2. T0 ➡ T1 → T0 ➡ T2 → ∃∃T. T1 ➡ T & T2 ➡ T. -#T0 @(f_ind … tw … T0) -T0 #n #IH * +#T0 @(f_ind … tw … T0) -T0 #n #IH * [ #I #_ #X1 #X2 #H1 #H2 -n >(tpr_inv_atom1 … H1) -X1 >(tpr_inv_atom1 … H2) -X2 @@ -215,13 +215,13 @@ theorem tpr_conf: ∀T0:term. ∀T1,T2. T0 ➡ T1 → T0 ➡ T2 → |2,4: #T2 #HT02 #HXT2 #H21 #H22 ] destruct (* case 2: delta, delta *) - [ /3 width=11 by tpr_conf_delta_delta/ (**) (* /3 width=11/ is too slow *) + [ /3 width=11 by tpr_conf_delta_delta/ (**) (* /3 width=11/ is too slow *) (* case 3: zeta, delta (repeated) *) | @ex2_commute /3 width=10 by tpr_conf_delta_zeta/ (* case 4: delta, zeta *) | /3 width=10 by tpr_conf_delta_zeta/ (**) (* /3 width=10/ is too slow *) (* case 5: zeta, zeta *) - | /3 width=9 by tpr_conf_zeta_zeta/ (**) (* /3 width=9/ is too slow *) + | /3 width=9 by tpr_conf_zeta_zeta/ (**) (* /3 width=9/ is too slow *) ] | elim (tpr_inv_flat1 … H1) -H1 * [ #V1 #T1 #HV01 #HT01 #H1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpss.ma index aadc0c80e..ff5cfb6a1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpss.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpss.ma @@ -88,4 +88,4 @@ qed. lemma tpr_tpss_conf: ∀T1,T2. T1 ➡ T2 → ∀L,U1,d,e. L ⊢ T1 ▶* [d, e] U1 → ∃∃U2. U1 ➡ U2 & L ⊢ T2 ▶* [d, e] U2. -/2 width=5/ qed. +/2 width=5/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma b/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma index 63143b19b..d6737a8ba 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma @@ -82,7 +82,7 @@ definition sd_SO: ∀h. nat → sd h ≝ λh,k. mk_sd h (deg_SO h k) …. qed. let rec sd_l (h:sh) (k:nat) (l:nat) on l : sd h ≝ - match l with + match l with [ O ⇒ sd_O h | S l ⇒ match l with [ O ⇒ sd_SO h k diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ltpss_dx.ma index ccc9ecc9d..48ac6a400 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ltpss_dx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ltpss_dx.ma @@ -106,7 +106,7 @@ lemma ssta_ltpss_dx_tps_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 ∀L2,d,e. L1 ▶* [d, e] L2 → ∀T2. L2 ⊢ T1 ▶ [d, e] T2 → ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & - L2 ⊢ U1 ▶* [d, e] U2. + L2 ⊢ U1 ▶* [d, e] U2. /3 width=5/ qed. lemma ssta_ltpss_dx_conf: ∀h,g,L1,T,U1,l. ⦃h, L1⦄ ⊢ T •[g, l] U1 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/gdrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/gdrop.ma index 218389e1c..ba2be29cc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/gdrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/gdrop.ma @@ -22,7 +22,7 @@ inductive gdrop (e:nat): relation genv ≝ | gdrop_lt: ∀I,G1,G2,V. e < |G1| → gdrop e G1 G2 → gdrop e (G1. ⓑ{I} V) G2 . -interpretation "global slicing" +interpretation "global slicing" 'RDrop e G1 G2 = (gdrop e G1 G2). (* basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma index 12b30e693..87d83b347 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop.ma @@ -81,7 +81,7 @@ lemma ldrop_inv_atom1: ∀d,e,L2. ⇩[d, e] ⋆ ≡ L2 → L2 = ⋆. /2 width=5/ qed-. fact ldrop_inv_O1_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → d = 0 → - ∀K,I,V. L1 = K. ⓑ{I} V → + ∀K,I,V. L1 = K. ⓑ{I} V → (e = 0 ∧ L2 = K. ⓑ{I} V) ∨ (0 < e ∧ ⇩[d, e - 1] K ≡ L2). #d #e #L1 #L2 * -d -e -L1 -L2 @@ -114,7 +114,7 @@ qed-. fact ldrop_inv_skip1_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → 0 < d → ∀I,K1,V1. L1 = K1. ⓑ{I} V1 → ∃∃K2,V2. ⇩[d - 1, e] K1 ≡ K2 & - ⇧[d - 1, e] V2 ≡ V1 & + ⇧[d - 1, e] V2 ≡ V1 & L2 = K2. ⓑ{I} V2. #d #e #L1 #L2 * -d -e -L1 -L2 [ #d #e #_ #I #K #V #H destruct @@ -127,14 +127,14 @@ qed. (* Basic_1: was: drop_gen_skip_l *) lemma ldrop_inv_skip1: ∀d,e,I,K1,V1,L2. ⇩[d, e] K1. ⓑ{I} V1 ≡ L2 → 0 < d → ∃∃K2,V2. ⇩[d - 1, e] K1 ≡ K2 & - ⇧[d - 1, e] V2 ≡ V1 & + ⇧[d - 1, e] V2 ≡ V1 & L2 = K2. ⓑ{I} V2. /2 width=3/ qed-. fact ldrop_inv_skip2_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → 0 < d → ∀I,K2,V2. L2 = K2. ⓑ{I} V2 → ∃∃K1,V1. ⇩[d - 1, e] K1 ≡ K2 & - ⇧[d - 1, e] V2 ≡ V1 & + ⇧[d - 1, e] V2 ≡ V1 & L1 = K1. ⓑ{I} V1. #d #e #L1 #L2 * -d -e -L1 -L2 [ #d #e #_ #I #K #V #H destruct @@ -171,7 +171,7 @@ qed. lemma ldrop_O1_le: ∀i,L. i ≤ |L| → ∃K. ⇩[0, i] L ≡ K. #i @(nat_ind_plus … i) -i /2 width=2/ #i #IHi * -[ #H lapply (le_n_O_to_eq … H) -H >commutative_plus normalize #H destruct +[ #H lapply (le_n_O_to_eq … H) -H >commutative_plus normalize #H destruct | #L #I #V normalize #H elim (IHi L ?) -IHi /2 width=1/ -H /3 width=2/ ] @@ -264,7 +264,7 @@ lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → ♯{L2} ≤ ♯{L1}. | #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12 >(tw_lift … HV21) -HV21 /2 width=1/ ] -qed-. +qed-. lemma ldrop_pair2_fwd_fw: ∀I,L,K,V,d,e. ⇩[d, e] L ≡ K. ⓑ{I} V → ∀T. ♯{K, V} < ♯{L, T}. @@ -298,7 +298,7 @@ lemma ldrop_fwd_O1_length: ∀L1,L2,e. ⇩[0, e] L1 ≡ L2 → |L2| = |L1| - e. qed-. (* Basic_1: removed theorems 50: - drop_ctail drop_skip_flat + drop_ctail drop_skip_flat cimp_flat_sx cimp_flat_dx cimp_bind cimp_getl_conf drop_clear drop_clear_O drop_clear_S clear_gen_sort clear_gen_bind clear_gen_flat clear_gen_flat_r diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_append.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_append.ma index 38244e6be..a122f9d45 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_append.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_append.ma @@ -18,7 +18,7 @@ include "basic_2/substitution/ldrop.ma". (* Properties on append for local environments ******************************) -fact ldrop_O1_append_sn_le_aux: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → +fact ldrop_O1_append_sn_le_aux: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → d = 0 → e ≤ |L1| → ∀L. ⇩[0, e] L @@ L1 ≡ L @@ L2. #L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize // /4 width=1/ @@ -61,4 +61,4 @@ lemma ldrop_O1_inv_append1_le: ∀K,L1,L2,e. ⇩[0, e] L1 @@ L2 ≡ K → e ≤ (H0 I L V 0 ? ? ?) // /5 width=6 by sfr_abbr, ldrop_ldrop, lt_minus_to_plus_r/ (**) (* auto now too slow without trace *) -| #d #_ #e #H0 +| #d #_ #e #H0 /5 width=6 by sfr_skip, ldrop_ldrop, le_S_S, lt_minus_to_plus_r/ (**) (* auto now too slow without trace *) ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma index ec2cc2df5..84babbdc8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma @@ -290,7 +290,7 @@ lemma lift_simple_sn: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → 𝐒⦃T2⦄ → #d #e #T1 #T2 #H elim H -d -e -T1 -T2 // #a #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #H elim (simple_inv_bind … H) -qed-. +qed-. (* Basic properties *********************************************************) @@ -394,7 +394,7 @@ lemma t_deliftable_sn_TC: ∀R. t_deliftable_sn R → t_deliftable_sn (TC … R) elim (IHU1 … HTU1) -U1 #T #HTU #HT1 elim (HR … HU2 … HTU) -U /3 width=5/ ] -qed-. +qed-. (* Basic_1: removed theorems 7: lift_head lift_gen_head diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma index 81f2b49a9..804c903d1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma @@ -103,9 +103,9 @@ theorem lift_mono: ∀d,e,T,U1. ⇧[d,e] T ≡ U1 → ∀U2. ⇧[d,e] T ≡ U2 #d #e #T #U1 #H elim H -d -e -T -U1 [ #k #d #e #X #HX lapply (lift_inv_sort1 … HX) -HX // -| #i #d #e #Hid #X #HX +| #i #d #e #Hid #X #HX lapply (lift_inv_lref1_lt … HX ?) -HX // -| #i #d #e #Hdi #X #HX +| #i #d #e #Hdi #X #HX lapply (lift_inv_lref1_ge … HX ?) -HX // | #p #d #e #X #HX lapply (lift_inv_gref1 … HX) -HX // diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubs.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubs.ma index f27883b02..1c0756c37 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubs.ma @@ -42,7 +42,7 @@ lemma lsubs_bind_eq: ∀L1,L2,e. L1 ≼ [0, e] L2 → ∀I,V. #L1 #L2 #e #HL12 #I #V elim I -I /2 width=1/ qed. -lemma lsubs_abbr_lt: ∀L1,L2,V,e. L1 ≼ [0, e - 1] L2 → 0 < e → +lemma lsubs_abbr_lt: ∀L1,L2,V,e. L1 ≼ [0, e - 1] L2 → 0 < e → L1. ⓓV ≼ [0, e] L2.ⓓV. #L1 #L2 #V #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/ qed. @@ -57,7 +57,7 @@ lemma lsubs_skip_lt: ∀L1,L2,d,e. L1 ≼ [d - 1, e] L2 → 0 < d → #L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) // /2 width=1/ qed. -lemma lsubs_bind_lt: ∀I,L1,L2,V,e. L1 ≼ [0, e - 1] L2 → 0 < e → +lemma lsubs_bind_lt: ∀I,L1,L2,V,e. L1 ≼ [0, e - 1] L2 → 0 < e → L1. ⓓV ≼ [0, e] L2. ⓑ{I}V. * /2 width=1/ qed. @@ -76,7 +76,7 @@ lemma TC_lsubs_trans: ∀S,R. lsubs_trans S R → lsubs_trans S (λL. (TC … (R ] qed. -(* Basic inversion lemmas ***************************************************) +(* Basic inversion lemmas ***************************************************) fact lsubs_inv_atom1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → L1 = ⋆ → L2 = ⋆ ∨ (d = 0 ∧ e = 0). diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma index 38b1dfe7c..2efd00298 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps.ma @@ -203,7 +203,7 @@ qed-. fact tps_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ U1 ▶ [d, e] U2 → ∀a,I,V1,T1. U1 = ⓑ{a,I} V1. T1 → - ∃∃V2,T2. L ⊢ V1 ▶ [d, e] V2 & + ∃∃V2,T2. L ⊢ V1 ▶ [d, e] V2 & L. ⓑ{I} V2 ⊢ T1 ▶ [d + 1, e] T2 & U2 = ⓑ{a,I} V2. T2. #d #e #L #U1 #U2 * -d -e -L -U1 -U2 @@ -215,7 +215,7 @@ fact tps_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ U1 ▶ [d, e] U2 → qed. lemma tps_inv_bind1: ∀d,e,L,a,I,V1,T1,U2. L ⊢ ⓑ{a,I} V1. T1 ▶ [d, e] U2 → - ∃∃V2,T2. L ⊢ V1 ▶ [d, e] V2 & + ∃∃V2,T2. L ⊢ V1 ▶ [d, e] V2 & L. ⓑ{I} V2 ⊢ T1 ▶ [d + 1, e] T2 & U2 = ⓑ{a,I} V2. T2. /2 width=3/ qed-. @@ -280,5 +280,5 @@ qed-. subst0_subst0 subst0_subst0_back subst0_weight_le subst0_weight_lt subst0_confluence_neq subst0_confluence_eq subst0_tlt_head subst0_confluence_lift subst0_tlt - subst1_head subst1_gen_head subst1_lift_S subst1_confluence_lift + subst1_head subst1_gen_head subst1_lift_S subst1_confluence_lift *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps_lift.ma index 808f6e3ba..1d65d8d63 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/tps_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/tps_lift.ma @@ -19,7 +19,7 @@ include "basic_2/substitution/tps.ma". (* Advanced inversion lemmas ************************************************) -fact tps_inv_S2_aux: ∀L,T1,T2,d,e1. L ⊢ T1 ▶ [d, e1] T2 → ∀e2. e1 = e2 + 1 → +fact tps_inv_S2_aux: ∀L,T1,T2,d,e1. L ⊢ T1 ▶ [d, e1] T2 → ∀e2. e1 = e2 + 1 → ∀K,V. ⇩[0, d] L ≡ K. ⓛV → L ⊢ T1 ▶ [d + 1, e2] T2. #L #T1 #T2 #d #e1 #H elim H -L -T1 -T2 -d -e1 [ // @@ -98,7 +98,7 @@ lemma tps_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 ▶ [dt, et] T2 → | #K #a #I #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdtd #Hddet elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct - @tps_bind [ /2 width=6/ | @IHT12 [3,4: // | skip |5,6: /2 width=1/ | /2 width=1/ ] + @tps_bind [ /2 width=6/ | @IHT12 [3,4: // | skip |5,6: /2 width=1/ | /2 width=1/ ] ] (**) (* /3 width=6/ is too slow, simplification like tps_lift_le is too slow *) | #K #I #V1 #V2 #T1 #T2 #dt #et #_ #_ #IHV12 #IHT12 #L #U1 #U2 #d #e #HLK #H1 #H2 #Hdetd elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 @@ -212,7 +212,7 @@ lemma tps_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 ▶ [dt, et] U2 → elim (le_inv_plus_l … Hdei) #Hdie #Hei lapply (lift_inv_lref2_ge … H … Hdei) -H #H destruct lapply (ldrop_conf_ge … HLK … HLKV ?) -L // #HKV - elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW [4: // |3: /2 width=1/ |2: /3 width=1/ ] -Hdei -Hdie + elim (lift_split … HVW d (i - e + 1) ? ? ?) -HVW [4: // |3: /2 width=1/ |2: /3 width=1/ ] -Hdei -Hdie #V0 #HV10 >plus_minus // plus_minus // /2 width=1/ ] ] (**) (* explicit constructor, uses monotonic_lt_minus_l *) | #L #a #I #V1 #V2 #U1 #U2 #dt #et #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H #Hdetd @@ -249,18 +249,18 @@ lemma tps_inv_lift1_eq: ∀L,U1,U2,d,e. ] qed. (* - Theorem subst0_gen_lift_rev_ge: (t1,v,u2,i,h,d:?) + Theorem subst0_gen_lift_rev_ge: (t1,v,u2,i,h,d:?) (subst0 i v t1 (lift h d u2)) -> (le (plus d h) i) -> (EX u1 | (subst0 (minus i h) v u1 u2) & - t1 = (lift h d u1) - ). + t1 = (lift h d u1) + ). Theorem subst0_gen_lift_rev_lelt: (t1,v,u2,i,h,d:?) (subst0 i v t1 (lift h d u2)) -> (le d i) -> (lt i (plus d h)) -> - (EX u1 | t1 = (lift (minus (plus d h) (S i)) (S i) u1)). + (EX u1 | t1 = (lift (minus (plus d h) (S i)) (S i) u1)). *) lemma tps_inv_lift1_ge_up: ∀L,U1,U2,dt,et. L ⊢ U1 ▶ [dt, et] U2 → ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma index 75ce09957..1b82f79e3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_alt.ma @@ -75,7 +75,7 @@ qed. lemma delifta_delift: ∀L,T1,T2,d,e. L ⊢ ▼▼*[d, e] T1 ≡ T2 → L ⊢ ▼*[d, e] T1 ≡ T2. #L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e // /2 width=1/ /2 width=6/ -qed-. +qed-. lemma delift_ind_alt: ∀R:ℕ→ℕ→lenv→relation term. (∀L,d,e,k. R d e L (⋆k) (⋆k)) → diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_lift.ma index 259150909..7a654023a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_lift.ma @@ -25,7 +25,7 @@ lemma delift_lref_be: ∀L,K,V1,V2,U2,i,d,e. d ≤ i → i < d + e → ⇧[0, d] V2 ≡ U2 → L ⊢ ▼*[d, e] #i ≡ U2. #L #K #V1 #V2 #U2 #i #d #e #Hdi #Hide #HLK * #V #HV1 #HV2 #HVU2 elim (lift_total V 0 (i+1)) #U #HVU -lapply (lift_trans_be … HV2 … HVU ? ?) -HV2 // >minus_plus minus_plus commutative_plus in ⊢ (??%??→?); (liftv_inv_nil1 … H) -T1s /2 width=3/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx.ma index 6ba09b962..1beef1bb7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/ltpss_dx.ma @@ -244,7 +244,7 @@ lemma ltpss_dx_append_ge: ∀K1,K2,d,e. K1 ▶* [d, e] K2 → L1 @@ K1 ▶* [d, e] L2 @@ K2. #K1 #K2 #d #e #H elim H -K1 -K2 -d -e [ #d #e #L1 #L2
* In terms only. - ** In terms and local environments only. + ** In terms and local environments only. *** In global environments only. - **** Sort level k in terms only. + **** Sort level k in terms only. - +
Summary of the Specification
Here is a numerical acount of the specification's contents and its timeline. @@ -23,30 +23,30 @@
Context-sensitive subject equivalence - for native type assignment. + for native type assignment. Closure of extended context-sensitive computation - for native validity. + for native validity. Extended context-sensitive strong normalization - for simply typed terms. + for simply typed terms. Confluence for context-free parallel reduction on closures. Term binders polarized to control ζ reduction. - + Context-sensitive subject equivalence - for atomic arity assignment - (anniversary milestone). + for atomic arity assignment + (anniversary milestone). Context-sensitive strong normalization - for simply typed terms. + for simply typed terms. Support for abstract candidates of reducibility. @@ -65,8 +65,8 @@ The source files are grouped in planes and components according to the following table. A notation file covering the whole specification is provided. - The notation for the relations or functions introduced in each file - is shown in parentheses (? are placeholders). + The notation for the relations or functions introduced in each file + is shown in parentheses (? are placeholders).
diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_blk.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_blk.tbl index ed50adf79..0de7f19e6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_blk.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_blk.tbl @@ -4,7 +4,7 @@ table { class "grey" [ { "domain" * } { [ [ "block" ] [ "leader" ] - [ "applicator (with →θ)*" ] [ "reduction" ] [ "→ζ *" ] [ "reference *" ] + [ "applicator (with →θ)*" ] [ "reduction" ] [ "→ζ *" ] [ "reference *" ] ] } ] [ { "{X | Γ ⊢ X : W}" * } { @@ -17,23 +17,23 @@ table { [ "ⓐV" ] [ "→β" ] [ "no" ] [ "#i" ] ] class "prune" [ - [ "global typed declaration ***" ] [ "Γ ⊢ pλW" ] - [ "no" ] [ "no" ] [ "no" ] [ "$p" ] + [ "global typed declaration ***" ] [ "Γ ⊢ pλW" ] + [ "no" ] [ "no" ] [ "no" ] [ "$p" ] ] class "blue" [ [ "native type annotation *" ] [ "Γ ⊢ ⓝW" ] - [ "no" ] [ "no" ] [ "yes" ] [ "no" ] + [ "no" ] [ "no" ] [ "yes" ] [ "no" ] ] } ] [ { "{X | Γ ⊢ X = V}" * } { class "sky" [ - [ "local abbreviation *" ] [ "Γ ⊢ +δV" ] + [ "local abbreviation *" ] [ "Γ ⊢ +δV" ] [ "no" ] [ "local →δ" ] [ "yes" ] [ "#i" ] ] class "cyan" [ - [ "local definition **" ] [ "Γ ⊢ -δV" ] + [ "local definition **" ] [ "Γ ⊢ -δV" ] [ "no" ] [ "local →δ" ] [ "no" ] [ "#i" ] - ] + ] class "water" [ [ "global definition ***" ] [ "Γ ⊢ pδV" ] [ "no" ] [ "global →δ" ] [ "no" ] [ "$p" ] @@ -42,7 +42,7 @@ table { [ { "no" * } { class "green" [ [ "sort ****" ] [ "Γ ⊢ ⋆k" ] - [ "no" ] [ "no" ] [ "no" ] [ "no" ] + [ "no" ] [ "no" ] [ "no" ] [ "no" ] ] } ] } diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index ee1b110eb..9ba552400 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -3,7 +3,7 @@ name "basic_2_src" table { class "grey" [ { "component" * } { - [ { "plane" * } { + [ { "plane" * } { [ "files" * ] } ] @@ -29,7 +29,7 @@ table { *) class "prune" [ { "dynamic typing" * } { -(* +(* [ { "local env. ref. for native type assignment" * } { [ "lsubn ( ? ⊢ ? :⊑ ? )" "lsubn_ldrop" "lsubn_cpcs" "lsubn_nta" * ] } @@ -123,7 +123,7 @@ table { } ] class "water" - [ { "reducibility" * } { + [ { "reducibility" * } { [ { "context-sensitive focalized reduction" * } { [ "cfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )" "cnfpr_ltpss" + "cfpr_aaa" + "cfpr_cpr" + "cfpr_cfpr" * ] } @@ -140,7 +140,7 @@ table { [ { "context-sensitive normal forms" * } { [ "cnf ( ? ⊢ 𝐍⦃?⦄ )" "cnf_lift" + "cnf_cif" * ] } - ] + ] [ { "context-sensitive reduction" * } { [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" + "cpr_tpss" + "cpr_ltpss_dx" + "cpr_ltpss_sn" + "cpr_delift" + "cpr_aaa" + "cpr_ltpr" + "cpr_cpr" * ] } @@ -197,7 +197,7 @@ table { [ { "basic local env. thinning" * } { [ "thin ( ? ▼*[?,?] ≡ ? )" "thin_ldrop" + "thin_delift" * ] } - ] + ] [ { "inverse basic term relocation" * } { [ "delift ( ? ⊢ ? ▼*[?,?] ≡ ? )" "delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )" "delift_lift" + "delift_tpss" + "delift_ltpss" + "delift_delift" * ] } @@ -208,7 +208,7 @@ table { [ "tpss ( ? ⊢ ? ▶*[?,?] ? )" "tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )" "tpss_lift" "tpss_tpss" * ] } ] - [ { "generic local env. slicing" * } { + [ { "generic local env. slicing" * } { [ "ldrops ( ⇩*[?] ? ≡ ? )" "ldrops_ldrop" + "ldrops_ldrops" * ] } ] @@ -219,17 +219,17 @@ table { ] [ { "generic term relocation" * } { [ "lifts_vector ( ⇧*[?] ? ≡ ? )" "lifts_lift_vector" * ] - [ "lifts ( ⇧*[?] ? ≡ ? )" "lifts_lift" + "lifts_lifts" * ] + [ "lifts ( ⇧*[?] ? ≡ ? )" "lifts_lift" + "lifts_lifts" * ] } ] - [ { "support for generic relocation" * } { + [ { "support for generic relocation" * } { [ "gr2 ( @⦃?,?⦄ ≡ ? )" "gr2_plus ( ? + ? )" "gr2_minus ( ? ▭ ? ≡ ? )" "gr2_gr2" * ] } ] } ] - class "orange" - [ { "substitution" * } { + class "orange" + [ { "substitution" * } { [ { "parallel substitution" * } { [ "tps ( ? ⊢ ? ▶[?,?] ? )" "tps_lift" + "tps_tps" * ] } @@ -257,7 +257,7 @@ table { ] } ] - class "red" + class "red" [ { "grammar" * } { [ { "same head term form" * } { [ "tshf ( ? ≈ ? )" "(tshf_tshf)" * ] @@ -277,11 +277,11 @@ table { [ "term" "term_weight ( ♯{?} )" "term_simple ( 𝐒⦃?⦄ )" "term_vector" * ] [ "item" * ] } - ] + ] [ { "external syntax" * } { [ "aarity" * ] } - ] + ] } ] } diff --git a/matita/matita/contribs/lambdadelta/ground_2/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/arith.ma index 8afc445b8..b854c3569 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/arith.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/arith.ma @@ -103,7 +103,7 @@ qed. (* Note: this is "if eqb n1 n2 then a2 else if leb n1 n2 then a1 else a3" *) let rec tri (A:Type[0]) n1 n2 a1 a2 a3 on n1 : A ≝ - match n1 with + match n1 with [ O ⇒ match n2 with [ O ⇒ a2 | S n2 ⇒ a1 ] | S n1 ⇒ match n2 with [ O ⇒ a3 | S n2 ⇒ tri A n1 n2 a1 a2 a3 ] ].