-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
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))))
orig: $(ORIGS)
@echo " ORIG basic_2"
- $(H)$(ORIG) basic_2 < $(ORIGS)
+ $(H)$(ORIG) basic_2 < $<
# dep ########################################################################
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)
# 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:
[ * #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/
<section>Contents of the Specification</section>
<body>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.
</body>
<news date="MLTT1.">
Martin-Löf's Type Theory with one universe
- using λδ as theory of expressions.
+ using λδ as theory of expressions.
</news>
<news date="Functional.">
The validation algorithm for λδ as implemented in
- <rlink to="implementation.html#helena">Helena 0.8</rlink>.
+ <rlink to="implementation.html#helena">Helena 0.8</rlink>.
</news>
-
+
<section>Summary of the Specification</section>
<body>Here is a numerical acount of the specification's contents
and its timeline.
</news>
<news date="2011 December 20.">
The Functional component is started
- inside the specification of λδ version 2.
+ inside the specification of λδ version 2.
</news>
<news date="2011 December 12.">
The MLTT1 component is started.
<body>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).
</body>
<table 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 ( [?←?] ? )" * ]
- }
+ }
]
}
]
∀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.
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.
@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 //
[ #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/
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.
@(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 →
@(cprs_strap2 … (ⓓ{b}V0.ⓐV2a.T0)) [ /3 width=3/ ] -V1a /3 width=1/
]
]
-]
+]
qed-.
(* Basic_1: was: pr3_iso_appls_cast *)
[ * #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/
]
lemma csn_aaa: ∀L,T,A. L ⊢ T ⁝ A → L ⊢ ⬊* T.
#L #T #A #H
@(acp_aaa … csn_acp csn_acr … H)
-qed.
+qed.
[ -HLT1 -HLT2 -H /3 width=1/
| -IHT -HT12 /4 width=3/
]
-]
+]
qed.
(* Main properties **********************************************************)
(* 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
]
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
(* 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.
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 ************************************************)
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-.
/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
]
| #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-.
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
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-.
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 #_
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/
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
* /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.
]
]
qed-.
-
\ No newline at end of file
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 *)
∃∃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
∃∃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 *********************************************************)
]
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.
(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.
/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 ***************************************************)
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
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.
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
#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⦄.
| #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)
]
/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/
(* 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.
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:
@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/
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/
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 *********)
(* 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
(* Basic_1: removed theorems 3:
pr0_subst0_back pr0_subst0_fwd pr0_subst0
-*)
+*)
(* Basic_1: removed local theorems: 1: pr0_delta_tau *)
#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.
(* 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
|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
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.
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
∀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 →
| 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 ***************************************************)
/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
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
(* 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
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/
]
| #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}.
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
(* 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/
<minus_plus_m_m /2 width=4/
]
]
-qed-.
+qed-.
(* Note: apparently this was missing in basic_1 *)
theorem ldrop_conf_le: ∀L0,L1,d1,e1. ⇩[d1, e1] L0 ≡ L1 →
- ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
+ ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
∃∃L. ⇩[0, e2] L1 ≡ L & ⇩[d1 - e2, e1] L2 ≡ L.
#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
[ #d1 #e1 #L2 #e2 #H
#e #_ #H0
>(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.
#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 *********************************************************)
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
#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 //
#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.
#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.
]
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).
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
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-.
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
*)
(* 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
[ //
| #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
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 // <minus_minus // /2 width=1/ <minus_n_n <plus_n_O #H
@ex2_intro [3: @H | skip | @tps_subst [5,6: // |1,2: skip | /2 width=1/ | >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
]
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 →
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)) →
⇧[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 <plus_minus_m_m /2 width=1/ #HV2U
+lapply (lift_trans_be … HV2 … HVU ? ?) -HV2 // >minus_plus <plus_minus_m_m /2 width=1/ #HV2U
lapply (lift_conf_be … HVU2 … HV2U ?) //
>commutative_plus in ⊢ (??%??→?); <minus_plus_m_m /3 width=6/
qed.
qed-.
lemma delift_inv_lref1: ∀L,U2,i,d,e. L ⊢ ▼*[d, e] #i ≡ U2 →
- ∨∨ (i < d ∧ U2 = #i)
+ ∨∨ (i < d ∧ U2 = #i)
| (∃∃K,V1,V2. d ≤ i & i < d + e &
⇩[0, i] L ≡ K. ⓓV1 &
K ⊢ ▼*[0, d + e - i - 1] V1 ≡ V2 &
lemma ltpss_sn_delift_trans_eq: ∀L,K,d,e. L ⊢ ▶* [d, e] K →
∀T1,T2. K ⊢ ▼*[d, e] T1 ≡ T2 → L ⊢ ▼*[d, e] T1 ≡ T2.
-#L #K #d #e #HLK #T1 #T2 * #T #HT1 #HT2
+#L #K #d #e #HLK #T1 #T2 * #T #HT1 #HT2
lapply (ltpss_sn_tpss_trans_eq … HT1 … HLK) -K /2 width=3/
qed.
lemma tps_delift_trans_eq: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 →
∀T. L ⊢ ▼*[d, e] U2 ≡ T → L ⊢ ▼*[d, e] U1 ≡ T.
-/3 width=3/ qed.
+/3 width=3/ qed.
(* GENERIC RELOCATION WITH PAIRS ********************************************)
inductive minuss: nat → relation (list2 nat nat) ≝
-| minuss_nil: ∀i. minuss i ⟠ ⟠
+| minuss_nil: ∀i. minuss i ⟠ ⟠
| minuss_lt : ∀des1,des2,d,e,i. i < d → minuss i des1 des2 →
minuss i ({d, e} @ des1) ({d - i, e} @ des2)
| minuss_ge : ∀des1,des2,d,e,i. d ≤ i → minuss (e + i) des1 des2 →
∃∃des0. i < d & des ▭ i ≡ des0 &
des2 = {d - i, e} @ des0.
#des1 #des2 #i * -des1 -des2 -i
-[ #i #d #e #des #H destruct
+[ #i #d #e #des #H destruct
| #des1 #des #d1 #e1 #i1 #Hid1 #Hdes #d2 #e2 #des2 #H destruct /3 width=3/
| #des1 #des #d1 #e1 #i1 #Hdi1 #Hdes #d2 #e2 #des2 #H destruct /3 width=1/
]
qed-.
lemma minuss_inv_cons1_lt: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 →
- i < d →
+ i < d →
∃∃des. des1 ▭ i ≡ des & des2 = {d - i, e} @ des.
#des1 #des2 #d #e #i #H
elim (minuss_inv_cons1 … H) -H * /2 width=3/ #Hdi #_ #Hid
∃∃des1. des1 + i = des2 & des = {d - i, e} @ des1.
#i #d #e #des2 * normalize
[ #H destruct
-| #d1 #e1 #des1 #H destruct /2 width=3/
+| #d1 #e1 #des1 #H destruct /2 width=3/
]
qed-.
qed-.
(* Basic_1: was: lift1_free (right to left) *)
-lemma lifts_lift_trans: ∀des,i,i0. @⦃i, des⦄ ≡ i0 →
+lemma lifts_lift_trans: ∀des,i,i0. @⦃i, des⦄ ≡ i0 →
∀des0. des + 1 ▭ i + 1 ≡ des0 + 1 →
∀T1,T0. ⇧*[des0] T1 ≡ T0 →
∀T2. ⇧[O, i0 + 1] T0 ≡ T2 →
(* Basic_1: was: lifts1_xhg (right to left) *)
lemma liftsv_liftv_trans_le: ∀T1s,Ts,des. ⇧*[des] T1s ≡ Ts →
∀T2s:list term. ⇧[0, 1] Ts ≡ T2s →
- ∃∃T0s. ⇧[0, 1] T1s ≡ T0s & ⇧*[des + 1] T0s ≡ T2s.
+ ∃∃T0s. ⇧[0, 1] T1s ≡ T0s & ⇧*[des + 1] T0s ≡ T2s.
#T1s #Ts #des #H elim H -T1s -Ts
[ #T1s #H
>(liftv_inv_nil1 … H) -T1s /2 width=3/
L1 @@ K1 ▶* [d, e] L2 @@ K2.
#K1 #K2 #d #e #H elim H -K1 -K2 -d -e
[ #d #e #L1 #L2 <minus_n_O //
-| #K #I #V #L1 #L2 #_ #H
+| #K #I #V #L1 #L2 #_ #H
lapply (le_n_O_to_eq … H) -H normalize <plus_n_Sm #H destruct
| #K1 #K2 #I #V1 #V2 #e #_ #_ #_ #L1 #L2 #_ #H
lapply (le_n_O_to_eq … H) -H normalize <plus_n_Sm #H destruct
elim (IHTU2 … HL01) -IHTU2 -HL01 /3 width=5/
]
qed.
-
+
lemma ltpss_dx_tpss_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶* [d2, e2] U2 →
∀L1,d1,e1. L1 ▶* [d1, e1] L0 → d1 + e1 ≤ d2 →
L1 ⊢ T2 ▶* [d2, e2] U2.
L1 @@ K1 ⊢ ▶* [d, e] L2 @@ K2.
#K1 #K2 #d #e #H elim H -K1 -K2 -d -e
[ #d #e #L1 #L2 <minus_n_O //
-| #K #I #V #L1 #L2 #_ #H
+| #K #I #V #L1 #L2 #_ #H
lapply (le_n_O_to_eq … H) -H normalize <plus_n_Sm #H destruct
| #K1 #K2 #I #V1 #V2 #e #_ #_ #_ #L1 #L2 #_ #H
lapply (le_n_O_to_eq … H) -H normalize <plus_n_Sm #H destruct
lemma ldrop_ltpss_sn_trans_be: ∀L1,K1,d1,e1. ⇩[d1, e1] L1 ≡ K1 →
∀K2,d2,e2. K1 ⊢ ▶* [d2, e2] K2 →
- d2 ≤ d1 → d1 ≤ d2 + e2 →
+ d2 ≤ d1 → d1 ≤ d2 + e2 →
∃∃L2. L1 ⊢ ▶* [d2, e1 + e2] L2 &
⇩[d1, e1] L2 ≡ K2.
#L1 #K1 #d1 #e1 #H elim H -L1 -K1 -d1 -e1
/2 width=1/ qed.
lemma tpss_strap1: ∀L,T1,T,T2,d,e.
- L ⊢ T1 ▶* [d, e] T → L ⊢ T ▶ [d, e] T2 → L ⊢ T1 ▶* [d, e] T2.
+ L ⊢ T1 ▶* [d, e] T → L ⊢ T ▶ [d, e] T2 → L ⊢ T1 ▶* [d, e] T2.
/2 width=3/ qed.
lemma tpss_strap2: ∀L,T1,T,T2,d,e.
- L ⊢ T1 ▶ [d, e] T → L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ▶* [d, e] T2.
+ L ⊢ T1 ▶ [d, e] T → L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ▶* [d, e] T2.
/2 width=3/ qed.
lemma tpss_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶* [d, e] T2 →
qed-.
lemma tpss_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.
#d #e #L #a #I #V1 #T1 #U2 #H @(tpss_ind … H) -U2
elim (tps_fwd_shift1 … H0) -H0 #L2 #T2 #HL02 #H destruct /2 width=4/
]
qed-.
-
\ No newline at end of file
lemma tpssa_tpss: ∀L,T1,T2,d,e. L ⊢ T1 ▶▶* [d, e] T2 → L ⊢ T1 ▶* [d, e] T2.
#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e // /2 width=6/
-qed-.
+qed-.
lemma tpss_ind_alt: ∀R:nat→nat→lenv→relation term.
(∀L,I,d,e. R d e L (⓪{I}) (⓪{I})) →
lapply (ltpssa_ltpss_sn … HL1) -HL1 #HL1
lapply (ltpss_sn_dx_trans_eq … HL1 … HL2) -HL1 #HL12
elim (IHL1 … H1) -IHL1 -H1 #U #HU1 #HTU
-elim (sstas_ltpss_dx_conf … HTU … HL2) -HTU -HL2 #U2 #H2 #HU2
+elim (sstas_ltpss_dx_conf … HTU … HL2) -HTU -HL2 #U2 #H2 #HU2
lapply (ltpss_sn_tpss_trans_eq … HU2 … HL12) -HU2 -HL12 #HU2
lapply (tpss_trans_eq … HU1 HU2) -U /2 width=3/
qed.
</body>
<table name="basic_2_blk"/>
<body>* 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.
</body>
-
+
<section>Summary of the Specification</section>
<body>Here is a numerical acount of the specification's contents
and its timeline.
<table name="basic_2_sum"/>
<news date="In progress.">
Context-sensitive subject equivalence
- for native type assignment.
+ for native type assignment.
</news>
<news date="In progress.">
Closure of extended context-sensitive computation
- for native validity.
+ for native validity.
</news>
<news date="In progress.">
Extended context-sensitive strong normalization
- for simply typed terms.
+ for simply typed terms.
</news>
<news date="2012 October 16.">
Confluence for context-free parallel reduction on closures.
</news>
<news date="2012 July 26.">
Term binders polarized to control ζ reduction.
- </news>
+ </news>
<news date="2012 April 16.">
Context-sensitive subject equivalence
- for atomic arity assignment
- (anniversary milestone).
+ for atomic arity assignment
+ (anniversary milestone).
</news>
<news date="2012 March 15.">
Context-sensitive strong normalization
- for simply typed terms.
+ for simply typed terms.
</news>
<news date="2012 January 27.">
Support for abstract candidates of reducibility.
<body>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).
</body>
<table name="basic_2_src"/>
class "grey" [ { "domain" * } {
[
[ "block" ] [ "leader" ]
- [ "applicator (with →θ)*" ] [ "reduction" ] [ "→ζ *" ] [ "reference *" ]
+ [ "applicator (with →θ)*" ] [ "reduction" ] [ "→ζ *" ] [ "reference *" ]
]
} ]
[ { "{X | Γ ⊢ X : W}" * } {
[ "ⓐ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" ]
[ { "no" * } {
class "green" [
[ "sort ****" ] [ "Γ ⊢ ⋆k" ]
- [ "no" ] [ "no" ] [ "no" ] [ "no" ]
+ [ "no" ] [ "no" ] [ "no" ] [ "no" ]
]
} ]
}
table {
class "grey"
[ { "component" * } {
- [ { "plane" * } {
+ [ { "plane" * } {
[ "files" * ]
}
]
*)
class "prune"
[ { "dynamic typing" * } {
-(*
+(*
[ { "local env. ref. for native type assignment" * } {
[ "lsubn ( ? ⊢ ? :⊑ ? )" "lsubn_ldrop" "lsubn_cpcs" "lsubn_nta" * ]
}
}
]
class "water"
- [ { "reducibility" * } {
+ [ { "reducibility" * } {
[ { "context-sensitive focalized reduction" * } {
[ "cfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )" "cnfpr_ltpss" + "cfpr_aaa" + "cfpr_cpr" + "cfpr_cfpr" * ]
}
[ { "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" * ]
}
[ { "basic local env. thinning" * } {
[ "thin ( ? ▼*[?,?] ≡ ? )" "thin_ldrop" + "thin_delift" * ]
}
- ]
+ ]
[ { "inverse basic term relocation" * } {
[ "delift ( ? ⊢ ? ▼*[?,?] ≡ ? )" "delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )" "delift_lift" + "delift_tpss" + "delift_ltpss" + "delift_delift" * ]
}
[ "tpss ( ? ⊢ ? ▶*[?,?] ? )" "tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )" "tpss_lift" "tpss_tpss" * ]
}
]
- [ { "generic local env. slicing" * } {
+ [ { "generic local env. slicing" * } {
[ "ldrops ( ⇩*[?] ? ≡ ? )" "ldrops_ldrop" + "ldrops_ldrops" * ]
}
]
]
[ { "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" * ]
}
]
}
]
- class "red"
+ class "red"
[ { "grammar" * } {
[ { "same head term form" * } {
[ "tshf ( ? ≈ ? )" "(tshf_tshf)" * ]
[ "term" "term_weight ( ♯{?} )" "term_simple ( 𝐒⦃?⦄ )" "term_vector" * ]
[ "item" * ]
}
- ]
+ ]
[ { "external syntax" * } {
[ "aarity" * ]
}
- ]
+ ]
}
]
}
(* 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 ]
].
projects / helm.git / commitdiff