\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
+module R = Helm_registry
module US = NUri.UriSet
let default_objs = US.empty
let default_net = 0
+let default_no_devel = true
+
+let default_no_init = true
+
let objs = ref default_objs
let srcs = ref default_srcs
let net = ref default_net
-let no_devel = ref true
+let no_devel = ref default_no_devel
+
+let no_init = ref default_no_init
let clear () =
+ R.clear ();
objs := default_objs; srcs := default_srcs;
- exclude := default_exclude; net := default_net
+ exclude := default_exclude; net := default_net;
+ no_devel := default_no_devel; no_init := default_no_init
val net: int ref
-val clear: unit -> unit
-
val no_devel: bool ref
+
+val no_init: bool ref
+
+val clear: unit -> unit
let init registry =
R.load_from registry;
- B.init ();
- C.set_trust trusted;
- H.set_log_callback no_log
+ if !O.no_init then begin
+ B.init ();
+ C.set_trust trusted;
+ H.set_log_callback no_log;
+ O.no_init := false;
+ end
let scan_uri devel str =
M.from_string (R.get "matita.basedir") devel str;
let _ =
let help = "Usage: probe [ -X | <configuration file> | -gp | HELM (base)uri | -i | -on | os | -sn | -ss ]*" in
- let help_X = " Reset options and counters" in
+ let help_X = " Clear configuration, options and counters" in
let help_g = " Exclude generated objects" in
let help_i = " Print the total intrinsic size" in
let help_p = " Exclude provided objects" in
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module R = Helm_registry
+module G = Arg
+
+module R = Helm_registry
module L = Lib
module A = Ast
let process conf =
let preamble = L.get_preamble conf in
- let ooch = L.open_out preamble (R.get_string "xoa.objects") in
- let noch = L.open_out preamble (R.get_string "xoa.notations") in
- List.iter (L.out_include ooch) (R.get_list R.string "xoa.include");
- List.iter (E.generate ooch noch) (R.get_list unm_ex "xoa.ex");
- List.iter (E.generate ooch noch) (R.get_list unm_or "xoa.or");
- List.iter (E.generate ooch noch) (R.get_list unm_and "xoa.and");
- close_out noch; close_out ooch
+ if R.has "xoa.objects" && R.has "xoa.notations" then begin
+ let ooch = L.open_out preamble (R.get_string "xoa.objects") in
+ let noch = L.open_out preamble (R.get_string "xoa.notations") in
+ List.iter (L.out_include ooch) (R.get_list R.string "xoa.include");
+ List.iter (E.generate ooch noch) (R.get_list unm_ex "xoa.ex");
+ List.iter (E.generate ooch noch) (R.get_list unm_or "xoa.or");
+ List.iter (E.generate ooch noch) (R.get_list unm_and "xoa.and");
+ close_out noch; close_out ooch
+ end
let _ =
- let help = "Usage: xoa [ <configuration file> ]*\n" in
- Arg.parse [] process help
+ let help = "Usage: xoa [ -X | <configuration file> ]*\n" in
+ let help_X = " Clear configuration" in
+ Arg.parse [
+ "-X" , G.Unit R.clear, help_X;
+ ] process help
TRIM := sed "s/ \\+$$//"
-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
-
+XOA_DIR := ../../../components/binaries/xoa
+XOA := xoa.native
XOA_CONF := ground_2/xoa.conf.xml
XOA_TARGETS := ground_2/xoa_notation.ma ground_2/xoa.ma
-ORIG := . ./orig.sh
+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 $(XOA_CONF) -g
-ORIGS := basic_2/basic_1.orig
+ORIG := . ./orig.sh
+ORIGS := basic_2/basic_1.orig
-TAGS := all xoa orig deps stats tbls trim
+TAGS := all xoa orig deps stats tbls trim
PACKAGES := ground_2 basic_2 apps_2
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/reducibility/ysc.ma".
-include "basic_2/computation/yprs.ma".
-
-(* "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **********************)
-
-inductive ygt (h) (g) (L1) (T1): relation2 lenv term ≝
-| ygt_inj : ∀L,L2,T,T2. h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ ≻[g] ⦃L2, T2⦄ →
- ygt h g L1 T1 L2 T2
-| ygt_step: ∀L,L2,T. ygt h g L1 T1 L T → L ➡ L2 → ygt h g L1 T1 L2 T
-.
-
-interpretation "'big tree' proper parallel computation (closure)"
- 'BTPRedStarProper h g L1 T1 L2 T2 = (ygt h g L1 T1 L2 T2).
-
-(* Basic forvard lemmas *****************************************************)
-
-lemma ygt_fwd_yprs: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄ →
- h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄.
-#h #g #L1 #L2 #T1 #T2 #H elim H -L2 -T2
-/3 width=4 by yprs_strap1, ysc_ypr, ypr_ltpr/
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma ysc_ygt: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ ≻[g] ⦃L2, T2⦄ →
- h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄.
-/3 width=4/ qed.
-
-lemma ygt_strap1: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ >[g] ⦃L, T⦄ →
- h ⊢ ⦃L, T⦄ ≽[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄.
-#h #g #L1 #L #L2 #T1 #T #T2 #H1 #H2
-lapply (ygt_fwd_yprs … H1) #H0
-elim (ypr_inv_ysc … H2) -H2 [| * #HL2 #H destruct ] /2 width=4/
-qed-.
-
-lemma ygt_strap2: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ ≽[g] ⦃L, T⦄ →
- h ⊢ ⦃L, T⦄ >[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄.
-#h #g #L1 #L #L2 #T1 #T #T2 #H1 #H2 elim H2 -L2 -T2
-[ /3 width=4 by ygt_inj, yprs_strap2/ | /2 width=3/ ]
-qed-.
-
-lemma ygt_yprs_trans: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ >[g] ⦃L, T⦄ →
- h ⊢ ⦃L, T⦄ ≥[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄.
-#h #g #L1 #L #L2 #T1 #T #T2 #HT1 #HT2 @(yprs_ind … HT2) -L2 -T2 //
-/2 width=4 by ygt_strap1/
-qed-.
-
-lemma yprs_ygt_trans: ∀h,g,L1,L,T1,T. h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L, T⦄ →
- ∀L2,T2. h ⊢ ⦃L, T⦄ >[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄.
-#h #g #L1 #L #T1 #T #HT1 @(yprs_ind … HT1) -L -T //
-/3 width=4 by ygt_strap2/
-qed-.
-
-lemma fw_ygt: ∀h,g,L1,L2,T1,T2. ♯{L2, T2} < ♯{L1, T1} → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄.
-/3 width=1/ qed.
-
-lemma cprs_ygt: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) →
- h ⊢ ⦃L, T1⦄ >[g] ⦃L, T2⦄.
-#h #g #L #T1 #T2 #H @(cprs_ind … H) -T2
-[ #H elim H //
-| #T #T2 #_ #HT2 #IHT1 #HT12
- elim (term_eq_dec T1 T) #H destruct
- [ -IHT1 /4 width=1/
- | lapply (IHT1 … H) -IHT1 -H -HT12 #HT1
- @(ygt_strap1 … HT1) -HT1 /2 width=1/
- ]
-]
-qed.
-
-lemma sstas_ygt: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •*[g] T2 → (T1 = T2 → ⊥) →
- h ⊢ ⦃L, T1⦄ >[g] ⦃L, T2⦄.
-#h #g #L #T1 #T2 #H @(sstas_ind … H) -T2
-[ #H elim H //
-| #T #T2 #l #_ #HT2 #IHT1 #HT12 -HT12
- elim (term_eq_dec T1 T) #H destruct
- [ -IHT1 /3 width=2/
- | lapply (IHT1 … H) -IHT1 -H #HT1
- @(ygt_strap1 … HT1) -HT1 /2 width=2/
- ]
-]
-qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/computation/ygt.ma".
-
-(* "BIG TREE" ORDER FOR CLOSURES ********************************************)
-
-(* Main properties **********************************************************)
-
-theorem ygt_trans: ∀h,g. bi_transitive … (ygt h g).
-/3 width=4 by ygt_fwd_yprs, ygt_yprs_trans/ qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/unwind/sstas.ma".
-include "basic_2/reducibility/ypr.ma".
-include "basic_2/computation/ltprs.ma".
-include "basic_2/computation/cprs.ma".
-
-(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************)
-
-definition yprs: ∀h. sd h → bi_relation lenv term ≝
- λh,g. bi_TC … (ypr h g).
-
-interpretation "'big tree' parallel computation (closure)"
- 'BTPRedStar h g L1 T1 L2 T2 = (yprs h g L1 T1 L2 T2).
-
-(* Basic eliminators ********************************************************)
-
-lemma yprs_ind: ∀h,g,L1,T1. ∀R:relation2 lenv term. R L1 T1 →
- (∀L,L2,T,T2. h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ ≽[g] ⦃L2, T2⦄ → R L T → R L2 T2) →
- ∀L2,T2. h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄ → R L2 T2.
-/3 width=7 by bi_TC_star_ind/ qed-.
-
-lemma yprs_ind_dx: ∀h,g,L2,T2. ∀R:relation2 lenv term. R L2 T2 →
- (∀L1,L,T1,T. h ⊢ ⦃L1, T1⦄ ≽[g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ ≥[g] ⦃L2, T2⦄ → R L T → R L1 T1) →
- ∀L1,T1. h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄ → R L1 T1.
-/3 width=7 by bi_TC_star_ind_dx/ qed-.
-
-(* Basic properties *********************************************************)
-
-lemma yprs_refl: ∀h,g. bi_reflexive … (yprs h g).
-/2 width=1/ qed.
-
-lemma ypr_yprs: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ ≽[g] ⦃L2, T2⦄ →
- h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄.
-/2 width=1/ qed.
-
-lemma yprs_strap1: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L, T⦄ →
- h ⊢ ⦃L, T⦄ ≽[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄.
-/2 width=4/ qed-.
-
-lemma yprs_strap2: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ ≽[g] ⦃L, T⦄ →
- h ⊢ ⦃L, T⦄ ≥[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄.
-/2 width=4/ qed-.
-
-lemma fw_yprs: ∀h,g,L1,L2,T1,T2. ♯{L2, T2} < ♯{L1, T1} →
- h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄.
-/3 width=1/ qed.
-
-lemma cprs_yprs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → h ⊢ ⦃L, T1⦄ ≥[g] ⦃L, T2⦄.
-#h #g #L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=4 by ypr_cpr, yprs_strap1/
-qed.
-
-lemma ltprs_yprs: ∀h,g,L1,L2,T. L1 ➡* L2 → h ⊢ ⦃L1, T⦄ ≥[g] ⦃L2, T⦄.
-#h #g #L1 #L2 #T #H @(ltprs_ind … H) -L2 // /3 width=4 by ypr_ltpr, yprs_strap1/
-qed.
-
-lemma sstas_yprs: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •*[g] T2 →
- h ⊢ ⦃L, T1⦄ ≥[g] ⦃L, T2⦄.
-#h #g #L #T1 #T2 #H @(sstas_ind … H) -T2 // /3 width=4 by ypr_ssta, yprs_strap1/
-qed.
-
-lemma ltpr_cprs_yprs: ∀h,g,L1,L2,T1,T2. L1 ➡ L2 → L2 ⊢ T1 ➡* T2 →
- h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄.
-/3 width=4 by yprs_strap2, ypr_ltpr, cprs_yprs/
-qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/computation/yprs.ma".
-
-(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************)
-
-theorem yprs_trans: ∀h,g. bi_transitive … (yprs h g).
-/2 width=4/ qed-.
(* *)
(**************************************************************************)
+include "basic_2/equivalence/lsubse.ma".
include "basic_2/dynamic/snv.ma".
(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
| lsubsv_atom: lsubsv h g (⋆) (⋆)
| lsubsv_pair: ∀I,L1,L2,V. lsubsv h g L1 L2 →
lsubsv h g (L1. ⓑ{I} V) (L2. ⓑ{I} V)
-| lsubsv_abbr: ∀L1,L2,V1,W1,W2,l. ⦃h, L1⦄ ⊩ V1 :[g] → ⦃h, L1⦄ ⊢ V1 •[g, l+1] W1 →
- L1 ⊢ W2 ⬌* W1 → ⦃h, L2⦄ ⊩ W2 :[g] →
+| lsubsv_abbr: ∀L1,L2,V1,V2,W1,W2,l. ⦃h, L1⦄ ⊩ V1 :[g] → ⦃h, L1⦄ ⊢ V1 •[g, l+1] W1 →
+ L1 ⊢ W1 ⬌* W2 → ⦃h, L2⦄ ⊩ W2 :[g] → ⦃h, L2⦄ ⊢ W2 •[g, l] V2 →
lsubsv h g L1 L2 → lsubsv h g (L1. ⓓV1) (L2. ⓛW2)
.
#h #g #L1 #L2 * -L1 -L2
[ //
| #I #L1 #L2 #V #_ #H destruct
-| #L1 #L2 #V1 #W1 #W2 #l #_ #_ #_ #_ #_ #H destruct
+| #L1 #L2 #V1 #V2 #W1 #W2 #l #_ #_ #_ #_ #_ #_ #H destruct
]
qed-.
fact lsubsv_inv_pair1_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 →
∀I,K1,V1. L1 = K1. ⓑ{I} V1 →
(∃∃K2. h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓑ{I} V1) ∨
- ∃∃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.
+ ∃∃K2,V2,W1,W2,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 &
+ K1 ⊢ W1 ⬌* W2 & ⦃h, K2⦄ ⊩ W2 :[g] & ⦃h, K2⦄ ⊢ W2 •[g,l] V2 &
+ h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓛW2 & I = Abbr.
#h #g #L1 #L2 * -L1 -L2
[ #J #K1 #U1 #H destruct
| #I #L1 #L2 #V #HL12 #J #K1 #U1 #H destruct /3 width=3/
-| #L1 #L2 #V1 #W1 #W2 #l #HV1 #HVW1 #HW21 #HW2 #HL12 #J #K1 #U1 #H destruct /3 width=9/
+| #L1 #L2 #V1 #V2 #W1 #W2 #l #HV1 #HVW1 #HW12 #HW2 #HWV2 #HL12 #J #K1 #U1 #H destruct /3 width=11/
]
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 &
- K1 ⊢ W2 ⬌* W1 & ⦃h, K2⦄ ⊩ W2 :[g] &
- h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓛW2 & I = Abbr.
+ ∃∃K2,V2,W1,W2,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 &
+ K1 ⊢ W1 ⬌* W2 & ⦃h, K2⦄ ⊩ W2 :[g] & ⦃h, K2⦄ ⊢ W2 •[g,l] V2 &
+ h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓛW2 & I = Abbr.
/2 width=3 by lsubsv_inv_pair1_aux/ qed-.
fact lsubsv_inv_atom2_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L2 = ⋆ → L1 = ⋆.
#h #g #L1 #L2 * -L1 -L2
[ //
| #I #L1 #L2 #V #_ #H destruct
-| #L1 #L2 #V1 #W1 #W2 #l #_ #_ #_ #_ #_ #H destruct
+| #L1 #L2 #V1 #V2 #W1 #W2 #l #_ #_ #_ #_ #_ #_ #H destruct
]
qed-.
fact lsubsv_inv_pair2_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 →
∀I,K2,W2. L2 = K2. ⓑ{I} W2 →
(∃∃K1. h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓑ{I} W2) ∨
- ∃∃K1,W1,V1,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 &
- K1 ⊢ W2 ⬌* W1 & ⦃h, K2⦄ ⊩ W2 :[g] &
- h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓓV1 & I = Abst.
+ ∃∃K1,W1,V1,V2,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 &
+ K1 ⊢ W1 ⬌* W2 & ⦃h, K2⦄ ⊩ W2 :[g] & ⦃h, K2⦄ ⊢ W2 •[g,l] V2 &
+ h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓓV1 & I = Abst.
#h #g #L1 #L2 * -L1 -L2
[ #J #K2 #U2 #H destruct
| #I #L1 #L2 #V #HL12 #J #K2 #U2 #H destruct /3 width=3/
-| #L1 #L2 #V1 #W1 #W2 #l #HV #HVW1 #HW21 #HW2 #HL12 #J #K2 #U2 #H destruct /3 width=9/
+| #L1 #L2 #V1 #V2 #W1 #W2 #l #HV #HVW1 #HW12 #HW2 #HWV2 #HL12 #J #K2 #U2 #H destruct /3 width=11/
]
qed-.
lemma lsubsv_inv_pair2: ∀h,g,I,L1,K2,W2. h ⊢ L1 ⊩:⊑[g] K2. ⓑ{I} W2 →
(∃∃K1. h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓑ{I} W2) ∨
- ∃∃K1,W1,V1,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 &
- K1 ⊢ W2 ⬌* W1 & ⦃h, K2⦄ ⊩ W2 :[g] &
- h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓓV1 & I = Abst.
+ ∃∃K1,W1,V1,V2,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 &
+ K1 ⊢ W1 ⬌* W2 & ⦃h, K2⦄ ⊩ W2 :[g] & ⦃h, K2⦄ ⊢ W2 •[g,l] V2 &
+ h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓓV1 & I = Abst.
/2 width=3 by lsubsv_inv_pair2_aux/ qed-.
(* Basic_forward lemmas *****************************************************)
+lemma lsubsv_fwd_lsubse: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → h ⊢ L1 ⊢•⊑[g] L2.
+#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ /2 width=6/
+qed-.
+
lemma lsubsv_fwd_lsubs1: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L1 ≼[0, |L1|] L2.
-#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+/3 width=3 by lsubsv_fwd_lsubse, lsubse_fwd_lsubs1/
qed-.
lemma lsubsv_fwd_lsubs2: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L1 ≼[0, |L2|] L2.
-#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+/3 width=3 by lsubsv_fwd_lsubse, lsubse_fwd_lsubs2/
qed-.
(* Basic properties *********************************************************)
lemma lsubsv_cprs_trans: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 →
∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.
-/3 width=5 by lsubsv_fwd_lsubs2, cprs_lsubs_trans/
+/3 width=5 by lsubsv_fwd_lsubse, lsubse_cprs_trans/
qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/dynamic/snv_cpcs.ma".
+include "basic_2/dynamic/lsubsv_ssta.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
+
+(* Properties for the preservation results **********************************)
+
+fact sstas_lsubsv_aux: ∀h,g,L0,T0.
+ (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
+ (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
+ (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
+ (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) →
+ ∀L2,T. h ⊢ ⦃L0, T0⦄ >[g] ⦃L2, T⦄ → ⦃h, L2⦄ ⊩ T :[g] →
+ ∀L1. h ⊢ L1 ⊩:⊑[g] L2 → ∀U2. ⦃h, L2⦄ ⊢ T •*[g] U2 →
+ ∃∃U1. ⦃h, L1⦄ ⊢ T •*[g] U1 & L1 ⊢ U1 ⬌* U2.
+#h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L2 #T #HLT0 #HT #L1 #HL12 #U2 #H @(sstas_ind … H) -U2 [ /2 width=3/ ]
+#U2 #W #l #HTU2 #HU2W * #U1 #HTU1 #HU12
+lapply (IH1 … HT … HL12) // #H
+lapply (snv_sstas_aux … IH2 … HTU1) // /3 width=4 by ygt_yprs_trans, lsubsv_yprs/ -H #HU1
+lapply (snv_sstas_aux … IH2 … HTU2) // #H
+lapply (IH1 … H … HL12) [ /3 width=4 by ygt_yprs_trans, sstas_yprs/ ] -H #HU2
+elim (snv_fwd_ssta … HU1) #W1 #l1 #HUW1
+elim (lsubsv_ssta_trans … HU2W … HL12) -HU2W #W2 #HUW2 #HW2
+elim (ssta_ltpr_cpcs_aux … IH4 IH3 … HU1 HU2 … HUW1 … HUW2 … HU12) -HU1 -HU2 -HUW2 -HU12 //
+[2,3: /4 width=4 by ygt_yprs_trans, sstas_yprs, lsubsv_yprs/ ] -L2 -L0 -T0 -U2 #H #HW12 destruct
+lapply (cpcs_trans … HW12 … HW2) -W2 /3 width=4/
+qed-.
+
+fact dxprs_lsubsv_aux: ∀h,g,L0,T0.
+ (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
+ (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
+ (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
+ (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) →
+ ∀L2,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L2, T1⦄ → ⦃h, L2⦄ ⊩ T1 :[g] →
+ ∀L1. h ⊢ L1 ⊩:⊑[g] L2 → ∀T2. ⦃h, L2⦄ ⊢ T1 •*➡*[g] T2 →
+ ∃∃T. ⦃h, L1⦄ ⊢ T1 •*➡*[g] T & L1 ⊢ T2 ➡* T.
+#h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L2 #T1 #HLT0 #HT1 #L1 #HL12 #T2 * #T #HT1T #HTT2
+lapply (lsubsv_cprs_trans … HL12 … HTT2) -HTT2 #HTT2
+elim (sstas_lsubsv_aux … IH4 IH3 IH2 IH1 … HLT0 … HL12 … HT1T) // -L2 -L0 -T0 #T0 #HT10 #HT0
+lapply (cpcs_cprs_strap1 … HT0 … HTT2) -T #HT02
+elim (cpcs_inv_cprs … HT02) -HT02 /3 width=3/
+qed-.
<(ldrop_inv_refl … H) in HL12; -H /3 width=3/
| elim (IHL12 … HLK1) -L1 /3 width=3/
]
-| #L1 #L2 #V1 #W1 #W2 #l #HV1 #HVW1 #HW21 #HW2 #_ #IHL12 #K1 #e #H
+| #L1 #L2 #V1 #V2 #W1 #W2 #l #HV1 #HVW1 #HW12 #HW2 #HWV2 #_ #IHL12 #K1 #e #H
elim (ldrop_inv_O1 … H) -H * #He #HLK1
[ destruct
elim (IHL12 L1 0 ?) -IHL12 // #X #HL12 #H
- <(ldrop_inv_refl … H) in HL12; -H /3 width=4/
+ <(ldrop_inv_refl … H) in HL12; -H /3 width=6/
| elim (IHL12 … HLK1) -L1 /3 width=3/
]
]
<(ldrop_inv_refl … H) in HL12; -H /3 width=3/
| elim (IHL12 … HLK2) -L2 /3 width=3/
]
-| #L1 #L2 #V1 #W1 #W2 #l #HV1 #HVW1 #HW21 #HW2 #_ #IHL12 #K2 #e #H
+| #L1 #L2 #V1 #V2 #W1 #W2 #l #HV1 #HVW1 #HW12 #HW2 #HWV2 #_ #IHL12 #K2 #e #H
elim (ldrop_inv_O1 … H) -H * #He #HLK2
[ destruct
elim (IHL12 L2 0 ?) -IHL12 // #X #HL12 #H
- <(ldrop_inv_refl … H) in HL12; -H /3 width=4/
+ <(ldrop_inv_refl … H) in HL12; -H /3 width=6/
| elim (IHL12 … HLK2) -L2 /3 width=3/
]
]
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/dynamic/snv_aaa.ma".
+include "basic_2/dynamic/lsubsv.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
+
+(* Properties on local environment refinement for atomic arity assignment ***)
+
+lemma lsubsv_fwd_lsuba: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L1 ⁝⊑ L2.
+#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+#L1 #L2 #V1 #V2 #W1 #W2 #l #HV1 #HVW1 #HW12 #HW2 #_ #_ #HL12
+elim (snv_fwd_aaa … HV1) -HV1 #A #HV1
+elim (snv_fwd_aaa … HW2) -HW2 #B #HW2
+lapply (ssta_aaa … HV1 … HVW1) -HVW1 #H1
+lapply (lsuba_aaa_trans … HW2 … HL12) #H2
+lapply (aaa_cpcs_mono … HW12 … H1 … H2) -W1 -H2 #H destruct /2 width=3/
+qed-.
(* *)
(**************************************************************************)
+include "basic_2/computation/dxprs_dxprs.ma".
include "basic_2/dynamic/lsubsv_ldrop.ma".
+include "basic_2/dynamic/lsubsv_dxprs.ma".
include "basic_2/dynamic/lsubsv_cpcs.ma".
-(*
-include "basic_2/dynamic/lsubsv_ssta.ma".
-*)
+
(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
(* Properties concerning stratified native validity *************************)
-(*
-axiom lsubsv_xprs_trans: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 →
- ∀T1,T2. ⦃h, L2⦄ ⊢ T1 •➡*[g] T2 → ⦃h, L1⦄ ⊢ T1 •➡*[g] T2.
-/3 width=3 by lsubsv_fwd_lsubss, lsubss_xprs_trans/ qed-.
-*)
-lemma lsubsv_snv_trans: ∀h,g,L2,T. ⦃h, L2⦄ ⊩ T :[g] →
- ∀L1. h ⊢ L1 ⊩:⊑[g] L2 → ⦃h, L1⦄ ⊩ T :[g].
-#h #g #L2 #T #H elim H -L2 -T //
-[ #I2 #L2 #K2 #W2 #i #HLK2 #_ #IHW2 #L1 #HL12
- elim (lsubsv_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
- elim (lsubsv_inv_pair2 … H) -H * #K1 [ | -IHW2 ]
- [ #HK12 #H destruct /3 width=5/
- | #W1 #V1 #l #HV1 #_ #_ #_ #_ #H #_ destruct /2 width=5/
+fact snv_lsubsv_aux: ∀h,g,L0,T0.
+ (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
+ (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
+ (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
+ (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) →
+ ∀L1,T1. L0 = L1 → T0 = T1 → IH_snv_lsubsv h g L1 T1.
+#h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L2 * * [||||*] //
+[ #i #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2
+ elim (snv_inv_lref … H) -H #I2 #K2 #W2 #HLK2 #HW2
+ elim (lsubsv_ldrop_O1_trans … HL12 … HLK2) -HL12 #X #H #HLK1
+ lapply (ldrop_pair2_fwd_fw … HLK2 (#i)) -HLK2 #HLK2
+ elim (lsubsv_inv_pair2 … H) -H * #K1
+ [ #HK12 #H destruct /4 width=8 by snv_lref, fw_ygt/ (**) (* auto too slow without trace *)
+ | #W1 #V1 #V2 #l #HV1 #_ #_ #_ #_ #_ #H #_ destruct /2 width=5/
]
-| #a #I #L2 #V #T #_ #_ #IHV #IHT #L1 #HL12 /4 width=1/
-| #a #L2 #V #W #W0 #T #U #l #_ #_ #HVW #HW0 #HTU #IHV #IHT #L1 #HL12
- lapply (IHV … HL12) -IHV #HV
- lapply (IHT … HL12) -IHT #HT
+| #p #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2 -IH1
+ elim (snv_inv_gref … H)
+| #a #I #V #T #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2
+ elim (snv_inv_bind … H) -H /4 width=4/
+| #V #T #HL0 #HT0 #H #L1 #HL12 destruct
+ elim (snv_inv_appl … H) -H #a #W #W0 #U #l #HV #HT #HVW #HW0 #HTU
lapply (lsubsv_cprs_trans … HL12 … HW0) -HW0 #HW0
-(*
- lapply (lsubsv_ssta_trans … HVW … HL12) -HVW #HVW
- lapply (lsubsv_xprs_trans … HL12 … HTU) -HL12 -HTU /2 width=8/
-*)
-| #L2 #W #T #U #l #_ #_ #HTU #HUW #IHW #IHT #L1 #HL12
- lapply (IHW … HL12) -IHW #HW
- lapply (IHT … HL12) -IHT #HT
+ elim (lsubsv_ssta_trans … HVW … HL12) -HVW #W1 #HVW1 #HW1
+ lapply (cpcs_cprs_strap1 … HW1 … HW0) -W #HW10
+ elim (dxprs_lsubsv_aux … IH4 IH3 IH2 IH1 … HL12 … HTU) -IH4 -IH3 -IH2 -HTU // /2 width=1/ #X #HTU #H
+ elim (cprs_inv_abst1 Abst W0 … H) -H #W #U2 #HW0 #HU2 #H destruct
+ lapply (cpcs_cprs_strap1 … HW10 … HW0) -W0 #H
+ elim (cpcs_inv_cprs … H) -H #W0 #HW10 #HW0
+ lapply (dxprs_cprs_trans … (ⓛ{a}W0.U2) HTU ?) [ /2 width=1/ ] -HTU -HW0
+ /4 width=8 by snv_appl, fw_ygt/ (**) (* auto too slow without trace *)
+| #W #T #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2
+ elim (snv_inv_cast … H) -H #U #l #HW #HT #HTU #HUW
lapply (lsubsv_cpcs_trans … HL12 … HUW) -HUW #HUW
-(*
- lapply (lsubsv_ssta_trans … HTU … HL12) -HTU #HTU
--HL12 -HWU /2 width=4/
+ elim (lsubsv_ssta_trans … HTU … HL12) -HTU #U0 #HTU0 #HU0
+ lapply (cpcs_trans … HU0 … HUW) -U /4 width=4 by snv_cast, fw_ygt/ (**) (* auto too slow without trace *)
]
qed-.
-*)
(* *)
(**************************************************************************)
-include "basic_2/equivalence/cpcs_cpcs.ma".
-include "basic_2/dynamic/lsubsv_ldrop.ma".
+include "basic_2/equivalence/lsubse_ssta.ma".
+include "basic_2/dynamic/lsubsv.ma".
(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
-(* Properties on stratified native type assignment **************************)
+(* Properties on stratified static type assignment **************************)
lemma lsubsv_ssta_trans: ∀h,g,L2,T,U2,l. ⦃h, L2⦄ ⊢ T •[g,l] U2 →
∀L1. h ⊢ L1 ⊩:⊑[g] L2 →
- ∃∃U1. L1 ⊢ U2 ⬌* U1 & ⦃h, L1⦄ ⊢ T •[g,l] U1.
-#h #g #L2 #T #U2 #l #H elim H -L2 -T -U2 -l
-[ #L2 #k #l #Hkl #L1 #_ /3 width=3/
-| #L2 #K2 #V2 #W2 #U2 #i #l #HLK2 #_ #HWU2 #IHVW2 #L1 #HL12
- elim (lsubsv_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
- elim (lsubsv_inv_pair2 … H) -H *
- [ #K1 #HK12 #H destruct
- elim (IHVW2 … HK12) -K2 #W1 #HW21 #H
- elim (lift_total W1 0 (i+1)) #U1 #HWU1
- lapply (ldrop_fwd_ldrop2 … HLK1) /3 width=9/
- | #K1 #V1 #W1 #l0 #_ #_ #_ #_ #_ #_ #H destruct
- ]
-| #L2 #K2 #W2 #V2 #U2 #i #l #HLK2 #_ #HWU2 #IHWV2 #L1 #HL12
- elim (lsubsv_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
- elim (lsubsv_inv_pair2 … H) -H *
- [ #K1 #HK12 #H destruct
- elim (IHWV2 … HK12) -K2 #V1 #_ #H -V2 /3 width=6/
- | #K1 #W1 #V1 #l0 #HV1 #HVW1 #HW21 #HW2 #HK12 #H #_ destruct
- elim (IHWV2 … HK12) -K2 #V #_ #H
- elim (lift_total W1 0 (i+1)) #U1 #HWU1
- lapply (ldrop_fwd_ldrop2 … HLK1) #HLK
- @(ex2_intro … U1)
- [ @(cpcs_lift … HLK … HWU2 … HWU1 HW21)
- | @(ssta_ldef … HLK1 … HWU1)
- (*
- /3 width=9/
- *)
\ No newline at end of file
+ ∃∃U1. ⦃h, L1⦄ ⊢ T •[g,l] U1 & L1 ⊢ U1 ⬌* U2.
+/3 width=3 by lsubsv_fwd_lsubse, lsubse_ssta_trans/
+qed-.
(**************************************************************************)
include "basic_2/unwind/sstas_sstas.ma".
-include "basic_2/computation/ygt.ma".
include "basic_2/equivalence/cpcs_ltpr.ma".
include "basic_2/dynamic/snv_ltpss_dx.ma".
include "basic_2/dynamic/snv_sstas.ma".
+include "basic_2/dynamic/ygt.ma".
(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
λh,g,L1,T1. ⦃h, L1⦄ ⊩ T1 :[g] →
∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l + 1] U1 → ⦃h, L1⦄ ⊩ U1 :[g].
+(* Properties for the preservation results **********************************)
+
+definition IH_snv_lsubsv: ∀h:sh. sd h → relation2 lenv term ≝
+ λh,g,L2,T. ⦃h, L2⦄ ⊩ T :[g] →
+ ∀L1. h ⊢ L1 ⊩:⊑[g] L2 → ⦃h, L1⦄ ⊩ T :[g].
+
fact snv_ltpr_cpr_aux: ∀h,g,L1,T1. IH_snv_ltpr_tpr h g L1 T1 →
⦃h, L1⦄ ⊩ T1 :[g] →
∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡ T2 → ⦃h, L2⦄ ⊩ T2 :[g].
include "basic_2/computation/dxprs_dxprs.ma".
include "basic_2/dynamic/snv_cpcs.ma".
-include "basic_2/dynamic/lsubsv_snv.ma".
(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
(* Properties on context-free parallel reduction for local environments *****)
fact snv_ltpr_tpr_aux: ∀h,g,L0,T0.
+ (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) →
(∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
(∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) →
(∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) →
∀L1,T1. L0 = L1 → T0 = T1 → IH_snv_ltpr_tpr h g L1 T1.
-#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 * * [||||*]
-[ #k #HL0 #HT0 #H1 #L2 #_ #X #H2 destruct -IH3 -IH2 -IH1 -L1
+#h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L1 * * [||||*]
+[ #k #HL0 #HT0 #H1 #L2 #_ #X #H2 destruct -IH4 -IH3 -IH2 -IH1 -L1
>(tpr_inv_atom1 … H2) -X //
-| #i #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH3 -IH2
+| #i #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH4 -IH3 -IH2
elim (snv_inv_lref … H1) -H1 #I #K1 #V1 #HLK1 #HV1
>(tpr_inv_atom1 … H2) -X
elim (ltpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) -HLK1 #HLK1
lapply (IH1 … HK12 … HV12) -IH1 -HV12 -HK12 // -HV1 [ /2 width=1/ ] -HLK1 /2 width=5/
-| #p #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH3 -IH2 -IH1
+| #p #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH4 -IH3 -IH2 -IH1
elim (snv_inv_gref … H1)
-| #a #I #V1 #T1 #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH3 -IH2
+| #a #I #V1 #T1 #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH4 -IH3 -IH2
elim (snv_inv_bind … H1) -H1 #HV1 #HT1
elim (tpr_inv_bind1 … H2) -H2 *
[ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct
| #V1 #T1 #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct
elim (snv_inv_appl … H1) -H1 #a #W10 #W1 #U1 #l #HV1 #HT1 #HVW1 #HW10 #HTU1
elim (tpr_inv_appl1 … H2) -H2 *
- [ #V2 #T2 #HV12 #HT12 #H destruct
+ [ #V2 #T2 #HV12 #HT12 #H destruct -IH4
lapply (IH1 … HV1 … HL12 … HV12) [ /2 width=1/ ] #HV2
lapply (IH1 … HT1 … HL12 … HT12) [ /2 width=1/ ] #HT2
elim (IH3 … HVW1 … HL12 … HV12) -HVW1 -HV12 // -HV1 [2: /2 width=1/ ] #W2 #HVW2 #HW12
lapply (IH1 … HT20 … (L2.ⓛW20) … HT202) [1,2: /2 width=1/ ] -IH1 -HT20 -HT202 #HT2
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
+ lapply (IH4 … HT2 (L2.ⓓV2) ?) -HT2
+ [ (* /2 width=4/ *)
+ |
+ | /2 width=1/
+ ]
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/dynamic/ysc.ma".
+include "basic_2/dynamic/yprs.ma".
+
+(* "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **********************)
+
+inductive ygt (h) (g) (L1) (T1): relation2 lenv term ≝
+| ygt_inj : ∀L,L2,T,T2. h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ ≻[g] ⦃L2, T2⦄ →
+ ygt h g L1 T1 L2 T2
+| ygt_step: ∀L,L2,T. ygt h g L1 T1 L T → L ➡ L2 → ygt h g L1 T1 L2 T
+.
+
+interpretation "'big tree' proper parallel computation (closure)"
+ 'BTPRedStarProper h g L1 T1 L2 T2 = (ygt h g L1 T1 L2 T2).
+
+(* Basic forvard lemmas *****************************************************)
+
+lemma ygt_fwd_yprs: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄ →
+ h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄.
+#h #g #L1 #L2 #T1 #T2 #H elim H -L2 -T2
+/3 width=4 by yprs_strap1, ysc_ypr, ypr_ltpr/
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma ysc_ygt: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ ≻[g] ⦃L2, T2⦄ →
+ h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄.
+/3 width=4/ qed.
+
+lemma ygt_strap1: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ >[g] ⦃L, T⦄ →
+ h ⊢ ⦃L, T⦄ ≽[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄.
+#h #g #L1 #L #L2 #T1 #T #T2 #H1 #H2
+lapply (ygt_fwd_yprs … H1) #H0
+elim (ypr_inv_ysc … H2) -H2 [| * #HL2 #H destruct ] /2 width=4/
+qed-.
+
+lemma ygt_strap2: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ ≽[g] ⦃L, T⦄ →
+ h ⊢ ⦃L, T⦄ >[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄.
+#h #g #L1 #L #L2 #T1 #T #T2 #H1 #H2 elim H2 -L2 -T2
+[ /3 width=4 by ygt_inj, yprs_strap2/ | /2 width=3/ ]
+qed-.
+
+lemma ygt_yprs_trans: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ >[g] ⦃L, T⦄ →
+ h ⊢ ⦃L, T⦄ ≥[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄.
+#h #g #L1 #L #L2 #T1 #T #T2 #HT1 #HT2 @(yprs_ind … HT2) -L2 -T2 //
+/2 width=4 by ygt_strap1/
+qed-.
+
+lemma yprs_ygt_trans: ∀h,g,L1,L,T1,T. h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L, T⦄ →
+ ∀L2,T2. h ⊢ ⦃L, T⦄ >[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄.
+#h #g #L1 #L #T1 #T #HT1 @(yprs_ind … HT1) -L -T //
+/3 width=4 by ygt_strap2/
+qed-.
+
+lemma fw_ygt: ∀h,g,L1,L2,T1,T2. ♯{L2, T2} < ♯{L1, T1} → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄.
+/3 width=1/ qed.
+
+lemma cprs_ygt: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) →
+ h ⊢ ⦃L, T1⦄ >[g] ⦃L, T2⦄.
+#h #g #L #T1 #T2 #H @(cprs_ind … H) -T2
+[ #H elim H //
+| #T #T2 #_ #HT2 #IHT1 #HT12
+ elim (term_eq_dec T1 T) #H destruct
+ [ -IHT1 /4 width=1/
+ | lapply (IHT1 … H) -IHT1 -H -HT12 #HT1
+ @(ygt_strap1 … HT1) -HT1 /2 width=1/
+ ]
+]
+qed.
+
+lemma sstas_ygt: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •*[g] T2 → (T1 = T2 → ⊥) →
+ h ⊢ ⦃L, T1⦄ >[g] ⦃L, T2⦄.
+#h #g #L #T1 #T2 #H @(sstas_ind … H) -T2
+[ #H elim H //
+| #T #T2 #l #_ #HT2 #IHT1 #HT12 -HT12
+ elim (term_eq_dec T1 T) #H destruct
+ [ -IHT1 /3 width=2/
+ | lapply (IHT1 … H) -IHT1 -H #HT1
+ @(ygt_strap1 … HT1) -HT1 /2 width=2/
+ ]
+]
+qed.
+
+lemma lsubsv_ygt: ∀h,g,L1,L2,T. h ⊢ L2 ⊩:⊑[g] L1 → (L1 = L2 → ⊥) →
+ h ⊢ ⦃L1, T⦄ >[g] ⦃L2, T⦄.
+/4 width=1/ qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/dynamic/ygt.ma".
+
+(* "BIG TREE" ORDER FOR CLOSURES ********************************************)
+
+(* Main properties **********************************************************)
+
+theorem ygt_trans: ∀h,g. bi_transitive … (ygt h g).
+/3 width=4 by ygt_fwd_yprs, ygt_yprs_trans/ qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/reducibility/ltpr.ma".
+include "basic_2/dynamic/lsubsv.ma".
+
+(* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************)
+
+inductive ypr (h) (g) (L1) (T1): relation2 lenv term ≝
+| ypr_fw : ∀L2,T2. ♯{L2, T2} < ♯{L1, T1} → ypr h g L1 T1 L2 T2
+| ypr_ltpr : ∀L2. L1 ➡ L2 → ypr h g L1 T1 L2 T1
+| ypr_cpr : ∀T2. L1 ⊢ T1 ➡ T2 → ypr h g L1 T1 L1 T2
+| ypr_ssta : ∀T2,l. ⦃h, L1⦄ ⊢ T1 •[g, l + 1] T2 → ypr h g L1 T1 L1 T2
+| ypr_lsubsv: ∀L2. h ⊢ L2 ⊩:⊑[g] L1 → ypr h g L1 T1 L2 T1
+.
+
+interpretation
+ "'big tree' parallel reduction (closure)"
+ 'BTPRed h g L1 T1 L2 T2 = (ypr h g L1 T1 L2 T2).
+
+(* Basic properties *********************************************************)
+
+lemma ypr_refl: ∀h,g. bi_reflexive … (ypr h g).
+/2 width=1/ qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/computation/ltprs.ma".
+include "basic_2/dynamic/ypr.ma".
+
+(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************)
+
+definition yprs: ∀h. sd h → bi_relation lenv term ≝
+ λh,g. bi_TC … (ypr h g).
+
+interpretation "'big tree' parallel computation (closure)"
+ 'BTPRedStar h g L1 T1 L2 T2 = (yprs h g L1 T1 L2 T2).
+
+(* Basic eliminators ********************************************************)
+
+lemma yprs_ind: ∀h,g,L1,T1. ∀R:relation2 lenv term. R L1 T1 →
+ (∀L,L2,T,T2. h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ ≽[g] ⦃L2, T2⦄ → R L T → R L2 T2) →
+ ∀L2,T2. h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄ → R L2 T2.
+/3 width=7 by bi_TC_star_ind/ qed-.
+
+lemma yprs_ind_dx: ∀h,g,L2,T2. ∀R:relation2 lenv term. R L2 T2 →
+ (∀L1,L,T1,T. h ⊢ ⦃L1, T1⦄ ≽[g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ ≥[g] ⦃L2, T2⦄ → R L T → R L1 T1) →
+ ∀L1,T1. h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄ → R L1 T1.
+/3 width=7 by bi_TC_star_ind_dx/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma yprs_refl: ∀h,g. bi_reflexive … (yprs h g).
+/2 width=1/ qed.
+
+lemma ypr_yprs: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ ≽[g] ⦃L2, T2⦄ →
+ h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄.
+/2 width=1/ qed.
+
+lemma yprs_strap1: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L, T⦄ →
+ h ⊢ ⦃L, T⦄ ≽[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄.
+/2 width=4/ qed-.
+
+lemma yprs_strap2: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ ≽[g] ⦃L, T⦄ →
+ h ⊢ ⦃L, T⦄ ≥[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄.
+/2 width=4/ qed-.
+
+lemma fw_yprs: ∀h,g,L1,L2,T1,T2. ♯{L2, T2} < ♯{L1, T1} →
+ h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄.
+/3 width=1/ qed.
+
+lemma cprs_yprs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → h ⊢ ⦃L, T1⦄ ≥[g] ⦃L, T2⦄.
+#h #g #L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=4 by ypr_cpr, yprs_strap1/
+qed.
+
+lemma ltprs_yprs: ∀h,g,L1,L2,T. L1 ➡* L2 → h ⊢ ⦃L1, T⦄ ≥[g] ⦃L2, T⦄.
+#h #g #L1 #L2 #T #H @(ltprs_ind … H) -L2 // /3 width=4 by ypr_ltpr, yprs_strap1/
+qed.
+
+lemma sstas_yprs: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •*[g] T2 →
+ h ⊢ ⦃L, T1⦄ ≥[g] ⦃L, T2⦄.
+#h #g #L #T1 #T2 #H @(sstas_ind … H) -T2 // /3 width=4 by ypr_ssta, yprs_strap1/
+qed.
+
+lemma lsubsv_yprs: ∀h,g,L1,L2,T. h ⊢ L2 ⊩:⊑[g] L1 → h ⊢ ⦃L1, T⦄ ≥[g] ⦃L2, T⦄.
+/3 width=1/ qed.
+
+lemma ltpr_cprs_yprs: ∀h,g,L1,L2,T1,T2. L1 ➡ L2 → L2 ⊢ T1 ➡* T2 →
+ h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄.
+/3 width=4 by yprs_strap2, ypr_ltpr, cprs_yprs/
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/dynamic/yprs.ma".
+
+(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************)
+
+theorem yprs_trans: ∀h,g. bi_transitive … (yprs h g).
+/2 width=4/ qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/dynamic/ypr.ma".
+
+(* "BIG TREE" PROPER PARALLEL REDUCTION FOR CLOSURES ************************)
+
+inductive ysc (h) (g) (L1) (T1): relation2 lenv term ≝
+| ysc_fw : ∀L2,T2. ♯{L2, T2} < ♯{L1, T1} → ysc h g L1 T1 L2 T2
+| ysc_cpr : ∀T2. L1 ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → ysc h g L1 T1 L1 T2
+| ysc_ssta : ∀T2,l. ⦃h, L1⦄ ⊢ T1 •[g, l + 1] T2 → ysc h g L1 T1 L1 T2
+| ysc_lsubsv: ∀L2. h ⊢ L2 ⊩:⊑[g] L1 → (L1 = L2 → ⊥) → ysc h g L1 T1 L2 T1
+.
+
+interpretation
+ "'big tree' proper parallel reduction (closure)"
+ 'BTPRedProper h g L1 T1 L2 T2 = (ysc h g L1 T1 L2 T2).
+
+(* Basic properties *********************************************************)
+
+lemma ysc_ypr: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ ≻[g] ⦃L2, T2⦄ →
+ h ⊢ ⦃L1, T1⦄ ≽[g] ⦃L2, T2⦄.
+#h #g #L1 #L2 #T1 #T2 * -L2 -T2 /2 width=1/ /2 width=2/
+qed.
+
+(* Inversion lemmas on "big tree" parallel reduction for closures ***********)
+
+lemma ypr_inv_ysc: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ ≽[g] ⦃L2, T2⦄ →
+ h ⊢ ⦃L1, T1⦄ ≻[g] ⦃L2, T2⦄ ∨ (L1 ➡ L2 ∧ T1 = T2).
+#h #g #L1 #L2 #T1 #T2 * -L2 -T2 /3 width=1/ /3 width=2/
+[ #T2 #HT12 elim (term_eq_dec T1 T2) #H destruct /3 width=1/ /4 width=1/
+| #L2 #HL21 elim (lenv_eq_dec L1 L2) #H destruct /3 width=1/ /4 width=1/
+]
+qed-.
interpretation "abstraction (local environment)"
'DxAbst L T = (LPair L Abst T).
+(* Basic properties *********************************************************)
+
+axiom lenv_eq_dec: ∀L1,L2:lenv. Decidable (L1 = L2).
+
(* Basic inversion lemmas ***************************************************)
lemma destruct_lpair_lpair: ∀I1,I2,L1,L2,V1,V2. L1.ⓑ{I1}V1 = L2.ⓑ{I2}V2 →
non associative with precedence 45
for @{ 'FocalizedPRedAlt $L1 $L2 }.
-notation "hvbox( h ⊢ break ⦃ term 46 L1, break term 46 T1 ⦄ ≽ break [ term 46 g ] break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
- non associative with precedence 45
- for @{ 'BTPRed $h $g $L1 $T1 $L2 $T2 }.
-
-notation "hvbox( h ⊢ break ⦃ term 46 L1, break term 46 T1 ⦄ ≻ break [ term 46 g ] break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
- non associative with precedence 45
- for @{ 'BTPRedProper $h $g $L1 $T1 $L2 $T2 }.
-
(* Computation **************************************************************)
notation "hvbox( T1 ➡ * break term 46 T2 )"
non associative with precedence 45
for @{ 'DecomposedXSN $h $g $L $T }.
-notation "hvbox( h ⊢ break ⦃ term 46 L1, break term 46 T1 ⦄ ≥ break [ term 46 g ] break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
- non associative with precedence 45
- for @{ 'BTPRedStar $h $g $L1 $T1 $L2 $T2 }.
-
-notation "hvbox( h ⊢ break ⦃ term 46 L1, break term 46 T1 ⦄ > break [ term 46 g ] break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
- non associative with precedence 45
- for @{ 'BTPRedStarProper $h $g $L1 $T1 $L2 $T2 }.
-
(* Conversion ***************************************************************)
notation "hvbox( L ⊢ break term 46 T1 ⬌ break term 46 T2 )"
non associative with precedence 45
for @{ 'CrSubEqV $h $g $L1 $L2 }.
+notation "hvbox( h ⊢ break ⦃ term 46 L1, break term 46 T1 ⦄ ≽ break [ term 46 g ] break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'BTPRed $h $g $L1 $T1 $L2 $T2 }.
+
+notation "hvbox( h ⊢ break ⦃ term 46 L1, break term 46 T1 ⦄ ≻ break [ term 46 g ] break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'BTPRedProper $h $g $L1 $T1 $L2 $T2 }.
+
+notation "hvbox( h ⊢ break ⦃ term 46 L1, break term 46 T1 ⦄ ≥ break [ term 46 g ] break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'BTPRedStar $h $g $L1 $T1 $L2 $T2 }.
+
+notation "hvbox( h ⊢ break ⦃ term 46 L1, break term 46 T1 ⦄ > break [ term 46 g ] break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'BTPRedStarProper $h $g $L1 $T1 $L2 $T2 }.
+
notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 : break term 46 T2 )"
non associative with precedence 45
for @{ 'NativeType $h $L $T1 $T2 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/static/ssta.ma".
-include "basic_2/reducibility/ltpr.ma".
-include "basic_2/reducibility/cpr.ma".
-
-(* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************)
-
-inductive ypr (h) (g) (L1) (T1): relation2 lenv term ≝
-| ypr_fw : ∀L2,T2. ♯{L2, T2} < ♯{L1, T1} → ypr h g L1 T1 L2 T2
-| ypr_ltpr: ∀L2. L1 ➡ L2 → ypr h g L1 T1 L2 T1
-| ypr_cpr : ∀T2. L1 ⊢ T1 ➡ T2 → ypr h g L1 T1 L1 T2
-| ypr_ssta: ∀T2,l. ⦃h, L1⦄ ⊢ T1 •[g, l + 1] T2 → ypr h g L1 T1 L1 T2
-.
-
-interpretation
- "'big tree' parallel reduction (closure)"
- 'BTPRed h g L1 T1 L2 T2 = (ypr h g L1 T1 L2 T2).
-
-(* Basic properties *********************************************************)
-
-lemma ypr_refl: ∀h,g. bi_reflexive … (ypr h g).
-/2 width=1/ qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/reducibility/ypr.ma".
-
-(* "BIG TREE" PROPER PARALLEL REDUCTION FOR CLOSURES ************************)
-
-inductive ysc (h) (g) (L1) (T1): relation2 lenv term ≝
-| ysc_fw : ∀L2,T2. ♯{L2, T2} < ♯{L1, T1} → ysc h g L1 T1 L2 T2
-| ysc_cpr : ∀T2. L1 ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → ysc h g L1 T1 L1 T2
-| ysc_ssta: ∀T2,l. ⦃h, L1⦄ ⊢ T1 •[g, l + 1] T2 → ysc h g L1 T1 L1 T2
-.
-
-interpretation
- "'big tree' proper parallel reduction (closure)"
- 'BTPRedProper h g L1 T1 L2 T2 = (ysc h g L1 T1 L2 T2).
-
-(* Basic properties *********************************************************)
-
-lemma ysc_ypr: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ ≻[g] ⦃L2, T2⦄ →
- h ⊢ ⦃L1, T1⦄ ≽[g] ⦃L2, T2⦄.
-#h #g #L1 #L2 #T1 #T2 * -L2 -T2 /2 width=1/ /2 width=2/
-qed.
-
-(* Inversion lemmas on "big tree" parallel reduction for closures ***********)
-
-lemma ypr_inv_ysc: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ ≽[g] ⦃L2, T2⦄ →
- h ⊢ ⦃L1, T1⦄ ≻[g] ⦃L2, T2⦄ ∨ (L1 ➡ L2 ∧ T1 = T2).
-#h #g #L1 #L2 #T1 #T2 * -L2 -T2 /3 width=1/ /3 width=2/
-#T2 #HT12 elim (term_eq_dec T1 T2) #H destruct /3 width=1/ /4 width=1/
-qed-.
}
]
*)
+ [ { "\"big tree\" parallel computation" * } {
+ [ "yprs ( ? ⊢ ⦃?,?⦄ ≥[g] ⦃?,?⦄ )" "yprs_yprs" "ygt ( ? ⊢ ⦃?,?⦄ >[g] ⦃?,?⦄ )" "ygt_ygt" * ]
+ }
+ ]
+ [ { "\"big tree\" parallel reduction" * } {
+ [ "ypr ( ? ⊢ ⦃?,?⦄ ≽[g] ⦃?,?⦄ )" "ysc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ )" * ]
+ }
+ ]
[ { "local env. ref. for stratified native validity" * } {
- [ "lsubsv ( ? ⊢ ? ⊩:⊑[?] ? )" "lsubsv_ldrop" + "lsubsv_ssta" + "lsubsv_cpcs" + "lsubsv_snv" * ]
+ [ "lsubsv ( ? ⊢ ? ⊩:⊑[?] ? )" "lsubsv_ldrop" + "lsubsv_lsuba" + "lsubsv_ssta" + "lsubsv_dxprs" + "lsubsv_cpcs" + "lsubsv_snv" * ]
}
]
[ { "stratified native validity" * } {
[ "fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ )" "fprs_aaa" + "fprs_fprs" * ]
}
]
- [ { "\"big tree\" parallel computation" * } {
- [ "yprs ( ? ⊢ ⦃?,?⦄ ≥[g] ⦃?,?⦄ )" "yprs_yprs" "ygt ( ? ⊢ ⦃?,?⦄ >[g] ⦃?,?⦄ )" "ygt_ygt" * ]
- }
- ]
[ { "decomposed extended computation" * } {
[ "dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )" "dxprs_lift" + "dxprs_ltpss_dx" + "dxprs_ltpss_sn" + "dxprs_aaa" + "dxpr_lsubss" + "dxprs_dxprs" * ]
}
[ "fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )" "fpr_cpr" + "fpr_fpr" * ]
}
]
- [ { "\"big tree\" parallel reduction" * } {
- [ "ypr ( ? ⊢ ⦃?,?⦄ ≽[g] ⦃?,?⦄ )" "ysc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ )" * ]
- }
- ]
[ { "context-sensitive normal forms" * } {
[ "cnf ( ? ⊢ 𝐍⦃?⦄ )" "cnf_lift" + "cnf_cif" * ]
}
<helm_registry>
<section name="matita">
<key name="rt_base_dir">$(MATITA_RT_BASE_DIR)</key>
-<!--
- <key name="system">false</key>
- <key name="map_unicode_to_tex">false</key>
- <key name="do_heavy_checks">true</key>
- <key name="include_path">lib</key>
--->
</section>
<section name="xoa">
<key name="output_dir">contribs/lambdadelta/ground_2/</key>
<key name="ex">6 5</key>
<key name="ex">6 6</key>
<key name="ex">6 7</key>
- <key name="ex">7 4</key>
<key name="ex">7 7</key>
+ <key name="ex">8 5</key>
<key name="or">3</key>
<key name="or">4</key>
<key name="and">3</key>
interpretation "multiple existental quantifier (6, 7)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5).
-(* multiple existental quantifier (7, 4) *)
-
-inductive ex7_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→Prop) : Prop ≝
- | ex7_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → P5 x0 x1 x2 x3 → P6 x0 x1 x2 x3 → ex7_4 ? ? ? ? ? ? ? ? ? ? ?
-.
-
-interpretation "multiple existental quantifier (7, 4)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_4 ? ? ? ? P0 P1 P2 P3 P4 P5 P6).
-
(* multiple existental quantifier (7, 7) *)
inductive ex7_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→A4→A5→A6→Prop) : Prop ≝
interpretation "multiple existental quantifier (7, 7)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6).
+(* multiple existental quantifier (8, 5) *)
+
+inductive ex8_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3,P4,P5,P6,P7:A0→A1→A2→A3→A4→Prop) : Prop ≝
+ | ex8_5_intro: ∀x0,x1,x2,x3,x4. P0 x0 x1 x2 x3 x4 → P1 x0 x1 x2 x3 x4 → P2 x0 x1 x2 x3 x4 → P3 x0 x1 x2 x3 x4 → P4 x0 x1 x2 x3 x4 → P5 x0 x1 x2 x3 x4 → P6 x0 x1 x2 x3 x4 → P7 x0 x1 x2 x3 x4 → ex8_5 ? ? ? ? ? ? ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (8, 5)" 'Ex P0 P1 P2 P3 P4 P5 P6 P7 = (ex8_5 ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6 P7).
+
(* multiple disjunction connective (3) *)
inductive or3 (P0,P1,P2:Prop) : Prop ≝
non associative with precedence 20
for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P5) }.
-(* multiple existental quantifier (7, 4) *)
-
-notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)"
- non associative with precedence 20
- for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P6) }.
-
-notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)"
- non associative with precedence 20
- for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P6) }.
-
(* multiple existental quantifier (7, 7) *)
notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)"
non associative with precedence 20
for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P6) }.
+(* multiple existental quantifier (8, 5) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P6) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P7) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P6) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P7) }.
+
(* multiple disjunction connective (3) *)
notation "hvbox(∨∨ term 29 P0 break | term 29 P1 break | term 29 P2)"
projects / helm.git / commitdiff