aux (F.dirname bdir) (F.concat (F.basename bdir) file)
in
aux dir file
-(*
-
- let bpath = F.dirname str ^ "/" in
- bpath, buri
-*)
let str = F.concat "cic:" path ^ "/" in
O.srcs := US.add (U.uri_of_string str) !O.srcs
+let add_remove base path =
+ O.remove := F.concat base path :: !O.remove
+
let rec scan_entry base devel path =
if F.check_suffix path ".con.ng" then add_obj path else
if F.check_suffix path ".ind.ng" then add_obj path else
if F.check_suffix path ".var.ng" then add_obj path else
- if F.check_suffix path ".ng" then add_src devel path else
+ if F.check_suffix path ".ng" then
+ if src_exists (F.chop_extension devel ^ ".ma")
+ then add_src devel path else add_remove base path
+ else
if src_exists devel || src_exists (devel ^ ".ma") then
let files = Y.readdir (F.concat base path) in
let map base file = scan_entry base (F.concat devel file) (F.concat path file) in
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+module A = Array
+module F = Filename
+module Y = Sys
+module U = Unix
+
+module O = Options
+
+let remove_dir dir =
+ if Y.file_exists dir then begin
+ let map name = Y.remove (F.concat dir name) in
+ A.iter map (Y.readdir dir);
+ U.rmdir dir (* Sys.remove does not seem to remove empty directories *)
+ end
+
+let objects () =
+ let map name =
+ Y.remove name;
+ remove_dir (F.chop_extension name)
+ in
+ List.iter map !O.remove
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+val objects: unit -> unit
let default_srcs = US.empty
+let default_remove = []
+
let default_exclude = []
let default_net = 0
let srcs = ref default_srcs
+let remove = ref default_remove
+
let exclude = ref default_exclude
let net = ref default_net
let clear () =
R.clear ();
- objs := default_objs; srcs := default_srcs;
+ objs := default_objs; srcs := default_srcs; remove := default_remove;
exclude := default_exclude; net := default_net;
no_devel := default_no_devel; no_init := default_no_init
val srcs: NUri.UriSet.t ref
+val remove: string list ref
+
val exclude: NCic.generated list ref
val net: int ref
module O = Options
module M = MatitaList
+module D = MatitaRemove
module S = NCicScan
module E = Engine
else if E.is_registry s then init s
else scan_from s
+let clear () =
+ D.objects (); O.clear ()
+
let _ =
let help = "Usage: probe [ -X | <configuration file> | -gp | HELM (base)uri | -i | -on | os | -sn | -ss ]*" in
let help_X = " Clear configuration, options and counters" in
let help_sn = " Print the number of sources" in
let help_ss = " Print the list of sources" in
A.parse [
- "-X" , A.Unit O.clear, help_X;
+ "-X" , A.Unit clear, help_X;
"-g" , A.Unit set_g, help_g;
"-i" , A.Unit out_i, help_i;
"-on", A.Unit out_on, help_on;
"-p" , A.Unit set_p, help_p;
"-sn", A.Unit out_sn, help_sn;
"-ss", A.Unit out_ss, help_ss;
- ] process help
+ ] process help;
+ D.objects ()
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<page xmlns="http://lambdadelta.info/"
+ description = "BTM"
+ title = "BTM"
+ head = "cic:/matita/BTM/"
+>
+ <section>Character classes</section>
+ <body>This table shows how the first 45 positive integers
+ are distributed in the four classes.
+ </body>
+ <table name="chc_45"/>
+
+ <footer/>
+</page>
qed.
lemma dxprs_strap2: ∀h,g,L,T1,T,T2,l.
- ⦃h, L⦄ ⊢ T1 •[g, l+1] T → ⦃h, L⦄ ⊢ T •*➡*[g] T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2.
+ ⦃h, L⦄ ⊢ T1 •[g] ⦃l+1, T⦄ → ⦃h, L⦄ ⊢ T •*➡*[g] T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2.
#h #g #L #T1 #T #T2 #l #HT1 * /3 width=4/
qed.
(**************************************************************************)
include "basic_2/unwind/sstas_sstas.ma".
-include "basic_2/computation/cprs_cprs.ma".
+include "basic_2/computation/cprs_lfprs.ma".
include "basic_2/computation/dxprs.ma".
(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************)
#h #g #L #T1 #T #T2 #HT1 * #T0 #HT0 #HT02
lapply (sstas_trans … HT1 … HT0) -T /2 width=3/
qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma dxprs_inv_abbr_abst: ∀h,g,a1,a2,L,V1,W2,T1,T2. ⦃h, L⦄ ⊢ ⓓ{a1}V1.T1 •*➡*[g] ⓛ{a2}W2.T2 →
+ ∃∃T. ⦃h, L.ⓓV1⦄ ⊢ T1 •*➡*[g] T & ⇧[0, 1] ⓛ{a2}W2.T2 ≡ T & a1 = true.
+#h #g #a1 #a2 #L #V1 #W2 #T1 #T2 * #X #H1 #H2
+elim (sstas_inv_bind1 … H1) -H1 #U1 #HTU1 #H destruct
+elim (cprs_inv_abbr1 … H2) -H2 *
+[ #V2 #U2 #HV12 #HU12 #H destruct
+| /3 width=3/
+]
+qed-.
(* Advanced properties ******************************************************)
-lemma ssta_cprs_dxprs: ∀h,g,L,T1,T,T2,l. ⦃h, L⦄ ⊢ T1 •[g, l+1] T →
+lemma ssta_cprs_dxprs: ∀h,g,L,T1,T,T2,l. ⦃h, L⦄ ⊢ T1 •[g] ⦃l+1, T⦄ →
L ⊢ T ➡* T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2.
/3 width=3/ qed.
(* *)
(**************************************************************************)
-include "basic_2/equivalence/lsubse.ma".
+include "basic_2/equivalence/lsubss.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,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_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)
.
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,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 &
+ ∃∃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
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,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 &
+ ∃∃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_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,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 &
+ ∃∃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
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,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 &
+ ∃∃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.
+lemma lsubsv_fwd_lsubss: ∀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.
-/3 width=3 by lsubsv_fwd_lsubse, lsubse_fwd_lsubs1/
+/3 width=3 by lsubsv_fwd_lsubss, lsubss_fwd_lsubs1/
qed-.
lemma lsubsv_fwd_lsubs2: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L1 ≼[0, |L2|] L2.
-/3 width=3 by lsubsv_fwd_lsubse, lsubse_fwd_lsubs2/
+/3 width=3 by lsubsv_fwd_lsubss, lsubss_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_lsubse, lsubse_cprs_trans/
+/3 width=5 by lsubsv_fwd_lsubss, lsubss_cprs_trans/
qed-.
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 (snv_fwd_ssta … HU1) #l1 #W1 #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
(* *)
(**************************************************************************)
-include "basic_2/equivalence/lsubse_ssta.ma".
+include "basic_2/equivalence/lsubss_ssta.ma".
include "basic_2/dynamic/lsubsv.ma".
(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
(* Properties on stratified static type assignment **************************)
-lemma lsubsv_ssta_trans: ∀h,g,L2,T,U2,l. ⦃h, L2⦄ ⊢ T •[g,l] U2 →
+lemma lsubsv_ssta_trans: ∀h,g,L2,T,U2,l. ⦃h, L2⦄ ⊢ T •[g] ⦃l, U2⦄ →
∀L1. h ⊢ L1 ⊩:⊑[g] L2 →
- ∃∃U1. ⦃h, L1⦄ ⊢ T •[g,l] U1 & L1 ⊢ U1 ⬌* U2.
-/3 width=3 by lsubsv_fwd_lsubse, lsubse_ssta_trans/
+ ∃∃U1. ⦃h, L1⦄ ⊢ T •[g] ⦃l, U1⦄ & L1 ⊢ U1 ⬌* U2.
+/3 width=3 by lsubsv_fwd_lsubss, lsubss_ssta_trans/
qed-.
| snv_lref: ∀I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → snv h g K V → snv h g L (#i)
| snv_bind: ∀a,I,L,V,T. snv h g L V → snv h g (L.ⓑ{I}V) T → snv h g L (ⓑ{a,I}V.T)
| snv_appl: ∀a,L,V,W,W0,T,U,l. snv h g L V → snv h g L T →
- ⦃h, L⦄ ⊢ V •[g, l + 1] W → L ⊢ W ➡* W0 →
+ ⦃h, L⦄ ⊢ V •[g] ⦃l+1, W⦄ → L ⊢ W ➡* W0 →
⦃h, L⦄ ⊢ T •*➡*[g] ⓛ{a}W0.U → snv h g L (ⓐV.T)
| snv_cast: ∀L,W,T,U,l. snv h g L W → snv h g L T →
- ⦃h, L⦄ ⊢ T •[g, l + 1] U → L ⊢ U ⬌* W → snv h g L (ⓝW.T)
+ ⦃h, L⦄ ⊢ T •[g] ⦃l+1, U⦄ → L ⊢ U ⬌* W → snv h g L (ⓝW.T)
.
interpretation "stratified native validity (term)"
fact snv_inv_appl_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀V,T. X = ⓐV.T →
∃∃a,W,W0,U,l. ⦃h, L⦄ ⊩ V :[g] & ⦃h, L⦄ ⊩ T :[g] &
- ⦃h, L⦄ ⊢ V •[g, l + 1] W & L ⊢ W ➡* W0 &
+ ⦃h, L⦄ ⊢ V •[g] ⦃l+1, W⦄ & L ⊢ W ➡* W0 &
⦃h, L⦄ ⊢ T •*➡*[g] ⓛ{a}W0.U.
#h #g #L #X * -L -X
[ #L #k #V #T #H destruct
lemma snv_inv_appl: ∀h,g,L,V,T. ⦃h, L⦄ ⊩ ⓐV.T :[g] →
∃∃a,W,W0,U,l. ⦃h, L⦄ ⊩ V :[g] & ⦃h, L⦄ ⊩ T :[g] &
- ⦃h, L⦄ ⊢ V •[g, l + 1] W & L ⊢ W ➡* W0 &
+ ⦃h, L⦄ ⊢ V •[g] ⦃l+1, W⦄ & L ⊢ W ➡* W0 &
⦃h, L⦄ ⊢ T •*➡*[g] ⓛ{a}W0.U.
/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] &
- ⦃h, L⦄ ⊢ T •[g, l + 1] U & L ⊢ U ⬌* W.
+ ⦃h, L⦄ ⊢ T •[g] ⦃l+1, U⦄ & L ⊢ U ⬌* W.
#h #g #L #X * -L -X
[ #L #k #W #T #H destruct
| #I #L #K #V #i #_ #_ #W #T #H destruct
lemma snv_inv_cast: ∀h,g,L,W,T. ⦃h, L⦄ ⊩ ⓝW.T :[g] →
∃∃U,l. ⦃h, L⦄ ⊩ W :[g] & ⦃h, L⦄ ⊩ T :[g] &
- ⦃h, L⦄ ⊢ T •[g, l + 1] U & L ⊢ U ⬌* W.
+ ⦃h, L⦄ ⊢ T •[g] ⦃l+1, U⦄ & L ⊢ U ⬌* W.
/2 width=3/ qed-.
(* Basic forward lemmas *****************************************************)
-lemma snv_fwd_ssta: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → ∃∃U,l. ⦃h, L⦄ ⊢ T •[g, l] U.
+lemma snv_fwd_ssta: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → ∃∃l,U. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄.
#h #g #L #T #H elim H -L -T
[ #L #k elim (deg_total h g k) /3 width=3/
-| * #L #K #V #i #HLK #_ * #W #l0 #HVW
+| * #L #K #V #i #HLK #_ * #l0 #W #HVW
[ elim (lift_total W 0 (i+1)) /3 width=8/
| elim (lift_total V 0 (i+1)) /3 width=8/
]
definition IH_ssta_ltpr_tpr: ∀h:sh. sd h → relation2 lenv term ≝
λh,g,L1,T1. ⦃h, L1⦄ ⊩ T1 :[g] →
- ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 →
+ ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ →
∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 →
- ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & L2 ⊢ U1 ⬌* U2.
+ ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L2 ⊢ U1 ⬌* U2.
definition IH_snv_ssta: ∀h:sh. sd h → relation2 lenv term ≝
λ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 **********************************)
+ ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l+1, U1⦄ → ⦃h, L1⦄ ⊩ U1 :[g].
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].
+(* Properties for the preservation results **********************************)
+
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].
fact ssta_ltpr_cpr_aux: ∀h,g,L1,T1. IH_ssta_ltpr_tpr h g L1 T1 →
⦃h, L1⦄ ⊩ T1 :[g] →
- ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 →
+ ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ →
∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡ T2 →
- ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & L2 ⊢ U1 ⬌* U2.
+ ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L2 ⊢ U1 ⬌* U2.
#h #g #L1 #T1 #IH #HT1 #U1 #l #HTU1 #L2 #HL12 #T2 * #T #HT1T #HTT2
elim (IH … HTU1 … HL12 … HT1T) // -L1 -T1 #U #HTU #HU1
elim (ssta_tpss_conf … HTU … HTT2) -T #U2 #HTU2 #HU2
(∀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⦄ → ⦃h, L1⦄ ⊩ T1 :[g] →
- ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 →
+ ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ →
∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 →
- ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & L2 ⊢ U1 ⬌* U2.
+ ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L2 ⊢ U1 ⬌* U2.
#h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 #l #HTU1 #L2 #HL12 #T2 #H
@(cprs_ind … H) -T2 [ /2 width=7 by ssta_ltpr_cpr_aux/ ]
#T #T2 #HT1T #HTT2 * #U #HTU #HU1
(∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) →
∀L1,L2,T1,T2. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → h ⊢ ⦃L0, T0⦄ >[g] ⦃L2, T2⦄ →
⦃h, L1⦄ ⊩ T1 :[g] → ⦃h, L2⦄ ⊩ T2 :[g] →
- ∀U1,l1. ⦃h, L1⦄ ⊢ T1 •[g, l1] U1 →
- ∀U2,l2. ⦃h, L2⦄ ⊢ T2 •[g, l2] U2 →
+ ∀U1,l1. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l1, U1⦄ →
+ ∀U2,l2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l2, U2⦄ →
L1 ➡ L2 → L2 ⊢ T1 ⬌* T2 →
l1 = l2 ∧ L2 ⊢ U1 ⬌* U2.
#h #g #L0 #T0 #IH2 #IH1 #L1 #L2 #T1 #T2 #HLT01 #HLT02 #HT1 #HT2 #U1 #l1 #HTU1 #U2 #l2 #HTU2 #HL12 #H
(∀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⦄ → ⦃h, L1⦄ ⊩ T1 :[g] →
- ∀l,U1. ⦃h, L1⦄ ⊢ T1 •[g, l+1] U1 → ∀T2. ⦃h, L1⦄ ⊢ T1 •*➡*[g] T2 →
+ ∀l,U1. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l+1, U1⦄ → ∀T2. ⦃h, L1⦄ ⊢ T1 •*➡*[g] T2 →
∃∃U,U2. ⦃h, L1⦄ ⊢ U1 •*[g] U & ⦃h, L1⦄ ⊢ T2 •*[g] U2 & L1 ⊢ U ⬌* U2.
#h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #H01 #HT1 #l #U1 #HTU1 #T2 * #T #HT1T #HTT2
elim (sstas_strip … HT1T … HTU1) #HU1T destruct [ -HT1T | -L0 -T0 -T1 ]
lapply (cpcs_cprs_strap1 … HW10 … HW120) -W1 #HW120
lapply (cpcs_canc_sn … HW12 HW120) -W10 #HW20
elim (cpcs_inv_cprs … HW20) -HW20 #W0 #HW20 #HW200
- lapply (dxprs_cprs_trans … (ⓛ{a}W0.U2) HTU2 ?) [ /2 width=1/ ] -HW200 /2 width=8/
+ lapply (dxprs_cprs_trans … (ⓛ{a}W0.U2) HTU2 ?) [ /2 width=1/ ] -HW200 -HTU2 /2 width=8/
| #b #V2 #W20 #T20 #T2 #HV12 #HT202 #H1 #H2 destruct
elim (snv_inv_bind … HT1) -HT1 #HW20 #HT20
elim (dxprs_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW230 #_ #H destruct -T30
lapply (cprs_div … HW10 … HW230) -W30 #HW120
- elim (snv_fwd_ssta … HW20) #U20 #l0 #HWU20
+ elim (snv_fwd_ssta … HW20) #l0 #U20 #HWU20
elim (ssta_fwd_correct … HVW1) <minus_plus_m_m #U10 #HWU10
elim (ssta_ltpr_cpcs_aux … IH1 IH3 … HW20 … HWU10 … HWU20) // -IH3 -HWU10
[2: /3 width=5/ |3: /2 width=1/
lapply (IH4 … HT20 (L1.ⓓV1) ?) [ /2 width=6/ | /2 width=1/ ] -U20 -W10 -l0 -IH4 -HT20 -HW20 #HT20
lapply (IH1 … HL12 … HV12) // [ /2 width=1/ ] #HV2
lapply (IH1 … HT20 … (L2.ⓓV2) … HT202) [1,2: /2 width=1/ ] -L1 -V1 -W20 -T20 /2 width=1/
- |
\ No newline at end of file
+ | #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HW02 #HT02 #HV02 #H1 #H2 destruct -IH4
+ elim (snv_inv_bind … HT1) -HT1 #HW0 #HT0
+ elim (dxprs_inv_abbr_abst … HTU1) -HTU1 #X #HTU0 #HX #H destruct
+ elim (lift_inv_bind1 … HX) -HX #W3 #U3 #HW13 #_ #H destruct
+ lapply (ltpr_cprs_conf … HL12 … HW10) -HW10 #HW10
+ elim (dxprs_ltpr_cprs_aux … IH2 IH1 IH3 … HTU0 (L2.ⓓW2) … T2 ?) // [2: /3 width=1/ |3,4: /2 width=1/ ] -IH2 -HTU0 #X #HTU2 #H
+ elim (cprs_inv_abst1 Abst W3 … H) -H #W #U2 #HW1 #_ #H destruct -U3
+ elim (IH3 … HVW1 … HL12 … HV10) // /2 width=1/ -IH3 -HVW1 #X #H1 #H2
+ lapply (cpcs_canc_sn … H2 HW10) -W10 #H2
+ elim (lift_total X 0 1) #W20 #H3
+ lapply (ssta_lift … H1 (L2.ⓓW2) … HV02 … H3) /2 width=1/ -H1 #HVW20
+ lapply (cpcs_lift (L2.ⓓW2) … H3 … HW13 H2) /2 width=1/ -HW13 -H3 -H2 #HW320
+ lapply (cpcs_cprs_strap1 … HW320 … HW1) -W3 #HW20
+ elim (cpcs_inv_cprs … HW20) -HW20 #W3 #HW203 #HW3
+ lapply (dxprs_cprs_trans … (ⓛ{a}W3.U2) HTU2 ?) [ /2 width=1/ ] -HW3 -HTU2 #HTU2
+ lapply (IH1 … HL12 … HW02) // [ /2 width=1/ ] -HW0 #HW2
+ lapply (IH1 … HL12 … HV10) // [ /2 width=1/ ] -HV1 -HV10 #HV0
+ lapply (IH1 … HT0 … (L2.ⓓW2) … HT02) [1,2: /2 width=1/ ] -L1 -HT02 -HW02 #HT2
+ lapply (snv_lift … HV0 (L2.ⓓW2) … HV02) /2 width=1/ -HV0 -HV02 /3 width=8/
+ ]
+| #W1 #T1 #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH4 -IH2
+ elim (snv_inv_cast … H1) -H1 #U1 #l #HW1 #HT1 #HTU1 #HUW1
+ elim (tpr_inv_cast1 … H2) -H2
+ [ * #W2 #T2 #HW12 #HT12 #H destruct
+ lapply (cpcs_cprs_strap1 … HUW1 W2 ?) [ /3 width=1/ ] -HUW1 #H1
+ lapply (IH1 … HL12 … HW12) // /2 width=1/ -HW1 -HW12 #HW2
+ lapply (IH1 … HL12 … HT12) // /2 width=1/ -IH1 #HT2
+ elim (IH3 … HTU1 … HL12 … HT12) // /2 width=1/ -IH3 -HT1 -HT12 -HTU1 #U2 #HTU2 #HU12
+ lapply (ltpr_cpcs_conf … HL12 … H1) -L1 #H1
+ lapply (cpcs_canc_sn … HU12 H1) -U1 /2 width=4/
+ | #H -IH3 -HW1 -HTU1 -HUW1
+ lapply (IH1 … HL12 … H) // /2 width=1/
+ ]
+]
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/equivalence/lsubse_ssta.ma".
+include "basic_2/equivalence/lsubss_ssta.ma".
include "basic_2/dynamic/snv_cpcs.ma".
(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
elim (dxprs_inv_abst1 … HTU10) -HTU10 #W0 #U0 #HW0 #_ #H destruct
lapply (cprs_div … HW10 … HW0) -W0 #HW1W
elim (ssta_fwd_correct … HVW1) <minus_plus_m_m #X1 #HWX1
- elim (snv_fwd_ssta … HW) #V #l1 #HWV
+ elim (snv_fwd_ssta … HW) #l1 #V #HWV
lapply (IH3 … HVW1) -IH3 // [ /2 width=1/ ] #HW1
elim (ssta_ltpr_cpcs_aux … IH2 IH1 … HWX1 … HWV …) -IH2 -HWX1 //
[2: /2 width=1/ |3: /3 width=4 by ygt_strap1, fw_ygt, ypr_ssta/ ] #H #_ destruct -X1
elim (IH1 … HTU2 (L2.ⓛW) … HT20) -IH1 -HTU2 -HT20 // [2,3: /2 width=1/ ] -HT2 #U20 #HTU20 #HU20
lapply (ltpr_cpcs_conf … HL12 … HW1W) -L1 #HW1W
lapply (cpcs_canc_sn … HW12 HW1W) -W1 #HW2
- elim (lsubse_ssta_trans … HTU20 (L2.ⓓV2) ?) -HTU20
+ elim (lsubss_ssta_trans … HTU20 (L2.ⓓV2) ?) -HTU20
[ #U #HTU20 #HUU20 -HWV0 -W2
@(ex2_intro … (ⓓ{b}V2.U)) [ /2 width=1/ ] -h -l -l1 -V -V0 -T2 -T20 -U0
@(cpcs_cprs_strap2 … (ⓓ{b}V2.U2)) [ /3 width=1/ ] -V1
(* Forward_lemmas on iterated stratified static type assignment for terms ***)
lemma snv_sstas_fwd_correct: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊩ T1 :[g] → ⦃h, L⦄ ⊢ T1 •* [g] T2 →
- ∃∃U2,l. ⦃h, L⦄ ⊢ T2 •[g, l] U2.
+ ∃∃U2,l. ⦃h, L⦄ ⊢ T2 •[g] ⦃l, U2⦄.
#h #g #L #T1 #T2 #HT1 #HT12
elim (snv_fwd_ssta … HT1) -HT1 /2 width=5 by sstas_fwd_correct/
qed-.
| 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_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
.
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_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
.
+++ /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/computation/cprs.ma".
-include "basic_2/equivalence/cpcs.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR CONTEXT-SENSITIVE PARALLEL EQUIVALENCE **)
-
-(* Note: this is not transitive *)
-inductive lsubse (h:sh) (g:sd h): relation lenv ≝
-| lsubse_atom: lsubse h g (⋆) (⋆)
-| lsubse_pair: ∀I,L1,L2,V. lsubse h g L1 L2 →
- lsubse h g (L1. ⓑ{I} V) (L2. ⓑ{I} V)
-| lsubse_abbr: ∀L1,L2,V1,V2,W1,W2,l. L1 ⊢ W1 ⬌* W2 →
- ⦃h, L1⦄ ⊢ V1 •[g, l + 1] W1 → ⦃h, L2⦄ ⊢ W2 •[g, l] V2 →
- lsubse h g L1 L2 → lsubse h g (L1. ⓓV1) (L2. ⓛW2)
-.
-
-interpretation
- "local environment refinement (context-sensitive parallel equivalence)"
- 'CrSubEqSE h g L1 L2 = (lsubse h g L1 L2).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact lsubse_inv_atom1_aux: ∀h,g,L1,L2. h ⊢ L1 ⊢•⊑[g] L2 → L1 = ⋆ → L2 = ⋆.
-#h #g #L1 #L2 * -L1 -L2
-[ //
-| #I #L1 #L2 #V #_ #H destruct
-| #L1 #L2 #V1 #V2 #W1 #W2 #l #_ #_ #_ #_ #H destruct
-]
-qed-.
-
-lemma lsubse_inv_atom1: ∀h,g,L2. h ⊢ ⋆ ⊢•⊑[g] L2 → L2 = ⋆.
-/2 width=5 by lsubse_inv_atom1_aux/ qed-.
-
-fact lsubse_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,V2,l. ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 & ⦃h, K2⦄ ⊢ W2 •[g,l] V2 &
- K1 ⊢ W1 ⬌* W2 & 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 #V2 #W1 #W2 #l #HW12 #HVW1 #HWV2 #HL12 #J #K1 #U1 #H destruct /3 width=10/
-]
-qed-.
-
-lemma lsubse_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,V2,l. ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 & ⦃h, K2⦄ ⊢ W2 •[g,l] V2 &
- K1 ⊢ W1 ⬌* W2 & h ⊢ K1 ⊢•⊑[g] K2 & L2 = K2. ⓛW2 & I = Abbr.
-/2 width=3 by lsubse_inv_pair1_aux/ qed-.
-
-fact lsubse_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 #V2 #W1 #W2 #l #_ #_ #_ #_ #H destruct
-]
-qed-.
-
-lemma lsubse_inv_atom2: ∀h,g,L1. h ⊢ L1 ⊢•⊑[g] ⋆ → L1 = ⋆.
-/2 width=5 by lsubse_inv_atom2_aux/ qed-.
-
-fact lsubse_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,V2,l. ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 & ⦃h, K2⦄ ⊢ W2 •[g,l] V2 &
- K1 ⊢ W1 ⬌* W2 & 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 #V2 #W1 #W2 #l #HW12 #HVW1 #HWV2 #HL12 #J #K2 #U2 #H destruct /3 width=10/
-]
-qed-.
-
-lemma lsubse_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,V2,l. ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 & ⦃h, K2⦄ ⊢ W2 •[g,l] V2 &
- K1 ⊢ W1 ⬌* W2 & h ⊢ K1 ⊢•⊑[g] K2 & L1 = K1. ⓓV1 & I = Abst.
-/2 width=3 by lsubse_inv_pair2_aux/ qed-.
-
-(* Basic_forward lemmas *****************************************************)
-
-lemma lsubse_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/
-qed-.
-
-lemma lsubse_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/
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma lsubse_refl: ∀h,g,L. h ⊢ L ⊢•⊑[g] L.
-#h #g #L elim L -L // /2 width=1/
-qed.
-
-lemma lsubse_cprs_trans: ∀h,g,L1,L2. h ⊢ L1 ⊢•⊑[g] L2 →
- ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.
-/3 width=5 by lsubse_fwd_lsubs2, cprs_lsubs_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/equivalence/cpcs_cpcs.ma".
-include "basic_2/equivalence/lsubse.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR CONTEXT-SENSITIVE PARALLEL EQUIVALENCE **)
-
-(* Properties on context-sensitive parallel equivalence for terms ***********)
-
-lemma lsubse_cpcs_trans: ∀h,g,L1,L2. h ⊢ L1 ⊢•⊑[g] L2 →
- ∀T1,T2. L2 ⊢ T1 ⬌* T2 → L1 ⊢ T1 ⬌* T2.
-/3 width=5 by lsubse_fwd_lsubs2, cpcs_lsubs_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/equivalence/lsubse.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR CONTEXT-SENSITIVE PARALLEL EQUIVALENCE **)
-
-(* Properties concerning basic local environment slicing ********************)
-
-(* Note: the constant 0 cannot be generalized *)
-lemma lsubse_ldrop_O1_conf: ∀h,g,L1,L2. h ⊢ L1 ⊢•⊑[g] L2 →
- ∀K1,e. ⇩[0, e] L1 ≡ K1 →
- ∃∃K2. h ⊢ K1 ⊢•⊑[g] K2 & ⇩[0, e] L2 ≡ K2.
-#h #g #L1 #L2 #H elim H -L1 -L2
-[ /2 width=3/
-| #I #L1 #L2 #V #_ #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=3/
- | elim (IHL12 … HLK1) -L1 /3 width=3/
- ]
-| #L1 #L2 #V1 #V2 #W1 #W2 #l #HW12 #HVW1 #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=6/
- | elim (IHL12 … HLK1) -L1 /3 width=3/
- ]
-]
-qed-.
-
-(* Note: the constant 0 cannot be generalized *)
-lemma lsubse_ldrop_O1_trans: ∀h,g,L1,L2. h ⊢ L1 ⊢•⊑[g] L2 →
- ∀K2,e. ⇩[0, e] L2 ≡ K2 →
- ∃∃K1. h ⊢ K1 ⊢•⊑[g] K2 & ⇩[0, e] L1 ≡ K1.
-#h #g #L1 #L2 #H elim H -L1 -L2
-[ /2 width=3/
-| #I #L1 #L2 #V #_ #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=3/
- | elim (IHL12 … HLK2) -L2 /3 width=3/
- ]
-| #L1 #L2 #V1 #V2 #W1 #W2 #l #HW12 #HVW1 #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=6/
- | elim (IHL12 … HLK2) -L2 /3 width=3/
- ]
-]
-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/static/ssta_ssta.ma".
-include "basic_2/equivalence/cpcs_cpcs.ma".
-include "basic_2/equivalence/lsubse_ldrop.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR CONTEXT-SENSITIVE PARALLEL EQUIVALENCE **)
-
-(* Properties on stratified native type assignment **************************)
-
-lemma lsubse_ssta_trans: ∀h,g,L2,T,U2,l. ⦃h, L2⦄ ⊢ T •[g,l] U2 →
- ∀L1. h ⊢ L1 ⊢•⊑[g] L2 →
- ∃∃U1. ⦃h, L1⦄ ⊢ T •[g,l] U1 & L1 ⊢ U1 ⬌* U2.
-#h #g #L2 #T #U #l #H elim H -L2 -T -U -l
-[ /3 width=3/
-| #L2 #K2 #V2 #W2 #U2 #i #l #HLK2 #_ #HWU2 #IHVW2 #L1 #HL12
- elim (lsubse_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
- elim (lsubse_inv_pair2 … H) -H * #K1 [ | -HWU2 -IHVW2 -HLK1 ]
- [ #HK12 #H destruct
- elim (IHVW2 … HK12) -K2 #T2 #HVT2 #HTW2
- lapply (ldrop_fwd_ldrop2 … HLK1) #H
- elim (lift_total T2 0 (i+1)) /3 width=11/
- | #W1 #V1 #W2 #l0 #_ #_ #_ #_ #_ #H destruct
- ]
-| #L2 #K2 #W2 #V2 #U2 #i #l #HLK2 #HWV2 #HWU2 #IHWV2 #L1 #HL12
- elim (lsubse_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
- elim (lsubse_inv_pair2 … H) -H * #K1 [ -HWV2 | -IHWV2 ]
- [ #HK12 #H destruct
- elim (IHWV2 … HK12) -K2 /3 width=6/
- | #W1 #V1 #T2 #l0 #HVW1 #HWT2 #HW12 #_ #H #_ destruct
- elim (ssta_mono … HWV2 … HWT2) -HWV2 -HWT2 #H1 #H2 destruct
- lapply (ldrop_fwd_ldrop2 … HLK1) #H
- elim (lift_total W1 0 (i+1)) /3 width=11/
- ]
-| #a #I #L2 #V2 #T2 #U2 #l #_ #IHTU2 #L1 #HL12
- elim (IHTU2 (L1.ⓑ{I}V2) …) [2: /2 width=1/ ] -L2 /3 width=3/
-| #L2 #V2 #T2 #U2 #l #_ #IHTU2 #L1 #HL12
- elim (IHTU2 … HL12) -L2 /3 width=5/
-| #L2 #W2 #T2 #U2 #l #_ #IHTU2 #L1 #HL12
- elim (IHTU2 … HL12) -L2 /3 width=3/
-]
-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/static/ssta.ma".
+include "basic_2/computation/cprs.ma".
+include "basic_2/equivalence/cpcs.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED STATIC TYPE ASSIGNMENT *******)
+
+(* Note: this is not transitive *)
+inductive lsubss (h:sh) (g:sd h): relation lenv ≝
+| lsubss_atom: lsubss h g (⋆) (⋆)
+| lsubss_pair: ∀I,L1,L2,V. lsubss h g L1 L2 →
+ lsubss h g (L1. ⓑ{I} V) (L2. ⓑ{I} V)
+| lsubss_abbr: ∀L1,L2,V1,V2,W1,W2,l. L1 ⊢ W1 ⬌* W2 →
+ ⦃h, L1⦄ ⊢ V1 •[g] ⦃l+1, W1⦄ → ⦃h, L2⦄ ⊢ W2 •[g] ⦃l, V2⦄ →
+ lsubss h g L1 L2 → lsubss h g (L1. ⓓV1) (L2. ⓛW2)
+.
+
+interpretation
+ "local environment refinement (stratified static type assigment)"
+ 'CrSubEqS h g L1 L2 = (lsubss h g L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lsubss_inv_atom1_aux: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 = ⋆ → L2 = ⋆.
+#h #g #L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #V #_ #H destruct
+| #L1 #L2 #V1 #V2 #W1 #W2 #l #_ #_ #_ #_ #H destruct
+]
+qed-.
+
+lemma lsubss_inv_atom1: ∀h,g,L2. h ⊢ ⋆ •⊑[g] L2 → L2 = ⋆.
+/2 width=5 by lsubss_inv_atom1_aux/ qed-.
+
+fact lsubss_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,V2,l. ⦃h, K1⦄ ⊢ V1 •[g] ⦃l+1, W1⦄ & ⦃h, K2⦄ ⊢ W2 •[g] ⦃l, V2⦄ &
+ K1 ⊢ W1 ⬌* W2 & 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 #V2 #W1 #W2 #l #HW12 #HVW1 #HWV2 #HL12 #J #K1 #U1 #H destruct /3 width=10/
+]
+qed-.
+
+lemma lsubss_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,V2,l. ⦃h, K1⦄ ⊢ V1 •[g] ⦃l+1, W1⦄ & ⦃h, K2⦄ ⊢ W2 •[g] ⦃l, V2⦄ &
+ K1 ⊢ W1 ⬌* W2 & h ⊢ K1 •⊑[g] K2 & L2 = K2. ⓛW2 & I = Abbr.
+/2 width=3 by lsubss_inv_pair1_aux/ qed-.
+
+fact lsubss_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 #V2 #W1 #W2 #l #_ #_ #_ #_ #H destruct
+]
+qed-.
+
+lemma lsubss_inv_atom2: ∀h,g,L1. h ⊢ L1 •⊑[g] ⋆ → L1 = ⋆.
+/2 width=5 by lsubss_inv_atom2_aux/ qed-.
+
+fact lsubss_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,V2,l. ⦃h, K1⦄ ⊢ V1 •[g] ⦃l+1, W1⦄ & ⦃h, K2⦄ ⊢ W2 •[g] ⦃l, V2⦄ &
+ K1 ⊢ W1 ⬌* W2 & 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 #V2 #W1 #W2 #l #HW12 #HVW1 #HWV2 #HL12 #J #K2 #U2 #H destruct /3 width=10/
+]
+qed-.
+
+lemma lsubss_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,V2,l. ⦃h, K1⦄ ⊢ V1 •[g] ⦃l+1, W1⦄ & ⦃h, K2⦄ ⊢ W2 •[g] ⦃l, V2⦄ &
+ K1 ⊢ W1 ⬌* W2 & h ⊢ K1 •⊑[g] K2 & L1 = K1. ⓓV1 & I = Abst.
+/2 width=3 by lsubss_inv_pair2_aux/ qed-.
+
+(* Basic_forward lemmas *****************************************************)
+
+lemma lsubss_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/
+qed-.
+
+lemma lsubss_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/
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lsubss_refl: ∀h,g,L. h ⊢ L •⊑[g] L.
+#h #g #L elim L -L // /2 width=1/
+qed.
+
+lemma lsubss_cprs_trans: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
+ ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.
+/3 width=5 by lsubss_fwd_lsubs2, cprs_lsubs_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/equivalence/cpcs_cpcs.ma".
+include "basic_2/equivalence/lsubss.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED STATIC TYPE ASSIGNMENT *******)
+
+(* Properties on context-sensitive parallel equivalence for terms ***********)
+
+lemma lsubss_cpcs_trans: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
+ ∀T1,T2. L2 ⊢ T1 ⬌* T2 → L1 ⊢ T1 ⬌* T2.
+/3 width=5 by lsubss_fwd_lsubs2, cpcs_lsubs_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/equivalence/lsubss.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED STATIC TYPE ASSIGNMENT *******)
+
+(* Properties concerning basic local environment slicing ********************)
+
+(* Note: the constant 0 cannot be generalized *)
+lemma lsubss_ldrop_O1_conf: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
+ ∀K1,e. ⇩[0, e] L1 ≡ K1 →
+ ∃∃K2. h ⊢ K1 •⊑[g] K2 & ⇩[0, e] L2 ≡ K2.
+#h #g #L1 #L2 #H elim H -L1 -L2
+[ /2 width=3/
+| #I #L1 #L2 #V #_ #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=3/
+ | elim (IHL12 … HLK1) -L1 /3 width=3/
+ ]
+| #L1 #L2 #V1 #V2 #W1 #W2 #l #HW12 #HVW1 #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=6/
+ | elim (IHL12 … HLK1) -L1 /3 width=3/
+ ]
+]
+qed-.
+
+(* Note: the constant 0 cannot be generalized *)
+lemma lsubss_ldrop_O1_trans: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
+ ∀K2,e. ⇩[0, e] L2 ≡ K2 →
+ ∃∃K1. h ⊢ K1 •⊑[g] K2 & ⇩[0, e] L1 ≡ K1.
+#h #g #L1 #L2 #H elim H -L1 -L2
+[ /2 width=3/
+| #I #L1 #L2 #V #_ #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=3/
+ | elim (IHL12 … HLK2) -L2 /3 width=3/
+ ]
+| #L1 #L2 #V1 #V2 #W1 #W2 #l #HW12 #HVW1 #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=6/
+ | elim (IHL12 … HLK2) -L2 /3 width=3/
+ ]
+]
+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/static/ssta_ssta.ma".
+include "basic_2/equivalence/cpcs_cpcs.ma".
+include "basic_2/equivalence/lsubss_ldrop.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED STATIC TYPE ASSIGNMENT *******)
+
+(* Properties on stratified native type assignment **************************)
+
+lemma lsubss_ssta_trans: ∀h,g,L2,T,U2,l. ⦃h, L2⦄ ⊢ T •[g] ⦃l, U2⦄ →
+ ∀L1. h ⊢ L1 •⊑[g] L2 →
+ ∃∃U1. ⦃h, L1⦄ ⊢ T •[g] ⦃l, U1⦄ & L1 ⊢ U1 ⬌* U2.
+#h #g #L2 #T #U #l #H elim H -L2 -T -U -l
+[ /3 width=3/
+| #L2 #K2 #V2 #W2 #U2 #i #l #HLK2 #_ #HWU2 #IHVW2 #L1 #HL12
+ elim (lsubss_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
+ elim (lsubss_inv_pair2 … H) -H * #K1 [ | -HWU2 -IHVW2 -HLK1 ]
+ [ #HK12 #H destruct
+ elim (IHVW2 … HK12) -K2 #T2 #HVT2 #HTW2
+ lapply (ldrop_fwd_ldrop2 … HLK1) #H
+ elim (lift_total T2 0 (i+1)) /3 width=11/
+ | #W1 #V1 #W2 #l0 #_ #_ #_ #_ #_ #H destruct
+ ]
+| #L2 #K2 #W2 #V2 #U2 #i #l #HLK2 #HWV2 #HWU2 #IHWV2 #L1 #HL12
+ elim (lsubss_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
+ elim (lsubss_inv_pair2 … H) -H * #K1 [ -HWV2 | -IHWV2 ]
+ [ #HK12 #H destruct
+ elim (IHWV2 … HK12) -K2 /3 width=6/
+ | #W1 #V1 #T2 #l0 #HVW1 #HWT2 #HW12 #_ #H #_ destruct
+ elim (ssta_mono … HWV2 … HWT2) -HWV2 -HWT2 #H1 #H2 destruct
+ lapply (ldrop_fwd_ldrop2 … HLK1) #H
+ elim (lift_total W1 0 (i+1)) /3 width=11/
+ ]
+| #a #I #L2 #V2 #T2 #U2 #l #_ #IHTU2 #L1 #HL12
+ elim (IHTU2 (L1.ⓑ{I}V2) …) [2: /2 width=1/ ] -L2 /3 width=3/
+| #L2 #V2 #T2 #U2 #l #_ #IHTU2 #L1 #HL12
+ elim (IHTU2 … HL12) -L2 /3 width=5/
+| #L2 #W2 #T2 #U2 #l #_ #IHTU2 #L1 #HL12
+ elim (IHTU2 … HL12) -L2 /3 width=3/
+]
+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_lsubss.ma".
-include "basic_2/computation/dxprs.ma".
-
-(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************)
-
-(* Properties on lenv ref for stratified type assignment ********************)
-
-lemma lsubss_dxprs_trans: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
- ∀T1,T2. ⦃h, L2⦄ ⊢ T1 •*➡*[g] T2 → ⦃h, L1⦄ ⊢ T1 •*➡*[g] T2.
-#h #g #L1 #L2 #HL12 #T1 #T2 *
-lapply (lsubss_fwd_lsubs2 … HL12) /3 width=5/
-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/static/ssta.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED STATIC TYPE ASSIGNMENT *******)
-
-inductive lsubss (h:sh) (g:sd h): relation lenv ≝
-| lsubss_atom: lsubss h g (⋆) (⋆)
-| lsubss_pair: ∀I,L1,L2,W. lsubss h g L1 L2 →
- lsubss h g (L1. ⓑ{I} W) (L2. ⓑ{I} W)
-| lsubss_abbr: ∀L1,L2,V,W,l. ⦃h, L1⦄ ⊢ V •[g, l+1] W → ⦃h, L2⦄ ⊢ V •[g, l+1] W →
- lsubss h g L1 L2 → lsubss h g (L1. ⓓV) (L2. ⓛW)
-.
-
-interpretation
- "local environment refinement (stratified static type assigment)"
- 'CrSubEqS h g L1 L2 = (lsubss h g L1 L2).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact lsubss_inv_atom1_aux: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 → L1 = ⋆ → L2 = ⋆.
-#h #g #L1 #L2 * -L1 -L2
-[ //
-| #I #L1 #L2 #V #_ #H destruct
-| #L1 #L2 #V #W #l #_ #_ #_ #H destruct
-]
-qed.
-
-lemma lsubss_inv_atom1: ∀h,g,L2. h ⊢ ⋆ •⊑[g] L2 → L2 = ⋆.
-/2 width=5/ qed-.
-
-fact lsubss_inv_pair1_aux: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
- ∀I,K1,V. L1 = K1. ⓑ{I} V →
- (∃∃K2. h ⊢ K1 •⊑[g] K2 & L2 = K2. ⓑ{I} V) ∨
- ∃∃K2,W,l. ⦃h, K1⦄ ⊢ V •[g,l+1] W & ⦃h, K2⦄ ⊢ V •[g,l+1] W &
- h ⊢ K1 •⊑[g] K2 & L2 = K2. ⓛW & I = Abbr.
-#h #g #L1 #L2 * -L1 -L2
-[ #I #K1 #V #H destruct
-| #J #L1 #L2 #V #HL12 #I #K1 #W #H destruct /3 width=3/
-| #L1 #L2 #V #W #l #H1VW #H2VW #HL12 #I #K1 #V1 #H destruct /3 width=7/
-]
-qed.
-
-lemma lsubss_inv_pair1: ∀h,g,I,K1,L2,V. h ⊢ K1. ⓑ{I} V •⊑[g] L2 →
- (∃∃K2. h ⊢ K1 •⊑[g] K2 & L2 = K2. ⓑ{I} V) ∨
- ∃∃K2,W,l. ⦃h, K1⦄ ⊢ V •[g,l+1] W & ⦃h, K2⦄ ⊢ V •[g,l+1] W &
- h ⊢ K1 •⊑[g] K2 & L2 = K2. ⓛW & I = Abbr.
-/2 width=3/ qed-.
-
-fact lsubss_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 #V #W #l #_ #_ #_ #H destruct
-]
-qed.
-
-lemma lsubss_inv_atom2: ∀h,g,L1. h ⊢ L1 •⊑[g] ⋆ → L1 = ⋆.
-/2 width=5/ qed-.
-
-fact lsubss_inv_pair2_aux: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
- ∀I,K2,W. L2 = K2. ⓑ{I} W →
- (∃∃K1. h ⊢ K1 •⊑[g] K2 & L1 = K1. ⓑ{I} W) ∨
- ∃∃K1,V,l. ⦃h, K1⦄ ⊢ V •[g,l+1] W & ⦃h, K2⦄ ⊢ V •[g,l+1] W &
- h ⊢ K1 •⊑[g] K2 & L1 = K1. ⓓV & I = Abst.
-#h #g #L1 #L2 * -L1 -L2
-[ #I #K2 #W #H destruct
-| #J #L1 #L2 #V #HL12 #I #K2 #W #H destruct /3 width=3/
-| #L1 #L2 #V #W #l #H1VW #H2VW #HL12 #I #K2 #W2 #H destruct /3 width=7/
-]
-qed.
-
-lemma lsubss_inv_pair2: ∀h,g,I,L1,K2,W. h ⊢ L1 •⊑[g] K2. ⓑ{I} W →
- (∃∃K1. h ⊢ K1 •⊑[g] K2 & L1 = K1. ⓑ{I} W) ∨
- ∃∃K1,V,l. ⦃h, K1⦄ ⊢ V •[g,l+1] W & ⦃h, K2⦄ ⊢ V •[g,l+1] W &
- h ⊢ K1 •⊑[g] K2 & L1 = K1. ⓓV & I = Abst.
-/2 width=3/ qed-.
-
-(* Basic_forward lemmas *****************************************************)
-
-lemma lsubss_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/
-qed-.
-
-lemma lsubss_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/
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma lsubss_refl: ∀h,g,L. h ⊢ L •⊑[g] L.
-#h #g #L elim L -L // /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/static/lsubss.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED STATIC TYPE ASSIGNMENT *******)
-
-(* Properties concerning basic local environment slicing ********************)
-
-(* Note: the constant 0 cannot be generalized *)
-lemma lsubss_ldrop_O1_conf: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
- ∀K1,e. ⇩[0, e] L1 ≡ K1 →
- ∃∃K2. h ⊢ K1 •⊑[g] K2 & ⇩[0, e] L2 ≡ K2.
-#h #g #L1 #L2 #H elim H -L1 -L2
-[ /2 width=3/
-| #I #L1 #L2 #V #_ #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=3/
- | elim (IHL12 … HLK1) -L1 /3 width=3/
- ]
-| #L1 #L2 #V #W #l #H1VW #H2VW #_ #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=3/
- | elim (IHL12 … HLK1) -L1 /3 width=3/
- ]
-]
-qed.
-
-(* Note: the constant 0 cannot be generalized *)
-lemma lsubss_ldrop_O1_trans: ∀h,g,L1,L2. h ⊢ L1 •⊑[g] L2 →
- ∀K2,e. ⇩[0, e] L2 ≡ K2 →
- ∃∃K1. h ⊢ K1 •⊑[g] K2 & ⇩[0, e] L1 ≡ K1.
-#h #g #L1 #L2 #H elim H -L1 -L2
-[ /2 width=3/
-| #I #L1 #L2 #V #_ #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=3/
- | elim (IHL12 … HLK2) -L2 /3 width=3/
- ]
-| #L1 #L2 #V #W #l #H1VW #H2VW #_ #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=3/
- | elim (IHL12 … HLK2) -L2 /3 width=3/
- ]
-]
-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/static/lsubss_ssta.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR STATIC TYPE ASSIGNMENT ******************)
-
-(* Main properties **********************************************************)
-
-theorem lsubss_trans: ∀h,g,L1,L. h ⊢ L1 •⊑[g] L → ∀L2. h ⊢ L •⊑[g] L2 →
- h ⊢ L1 •⊑[g] L2.
-#h #g #L1 #L #H elim H -L1 -L
-[ #X #H >(lsubss_inv_atom1 … H) -H //
-| #I #L1 #L #W #HL1 #IHL1 #X #H
- elim (lsubss_inv_pair1 … H) -H * #L2
- [ #HL2 #H destruct /3 width=1/
- | #V #l #H1WV #H2WV #HL2 #H1 #H2 destruct /3 width=3/
- ]
-| #L1 #L #V1 #W1 #l #H1VW1 #H2VW1 #HL1 #IHL1 #X #H
- elim (lsubss_inv_pair1 … H) -H * #L2
- [ #HL2 #H destruct /3 width=5/
- | #V #l0 #_ #_ #_ #_ #H destruct
- ]
-]
-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/static/ssta_lift.ma".
-include "basic_2/static/ssta_ssta.ma".
-include "basic_2/static/lsubss_ldrop.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED STATIC TYPE ASSIGNMENT *******)
-
-(* Properties concerning stratified native type assignment ******************)
-
-lemma lsubss_ssta_trans: ∀h,g,L2,T,U,l. ⦃h, L2⦄ ⊢ T •[g,l] U →
- ∀L1. h ⊢ L1 •⊑[g] L2 → ⦃h, L1⦄ ⊢ T •[g,l] U.
-#h #g #L2 #T #U #l #H elim H -L2 -T -U -l
-[ /2 width=1/
-| #L2 #K2 #V2 #W2 #U2 #i #l #HLK2 #_ #HWU2 #IHVW2 #L1 #HL12
- elim (lsubss_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
- elim (lsubss_inv_pair2 … H) -H * #K1 [ | -HWU2 -IHVW2 -HLK1 ]
- [ #HK12 #H destruct /3 width=6/
- | #V1 #l0 #_ #_ #_ #_ #H destruct
- ]
-| #L2 #K2 #W2 #V2 #U2 #i #l #HLK2 #HWV2 #HWU2 #IHWV2 #L1 #HL12
- elim (lsubss_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
- elim (lsubss_inv_pair2 … H) -H * #K1 [ -HWV2 | -IHWV2 ]
- [ #HK12 #H destruct /3 width=6/
- | #V1 #l0 #H1 #H2 #_ #H #_ destruct
- elim (ssta_fwd_correct … H2) -H2 #V #H
- elim (ssta_mono … HWV2 … H) -HWV2 -H /2 width=6/
- ]
-| /4 width=1/
-| /3 width=1/
-| /3 width=1/
-]
-qed.
-
-lemma lsubss_ssta_conf: ∀h,g,L1,T,U,l. ⦃h, L1⦄ ⊢ T •[g,l] U →
- ∀L2. h ⊢ L1 •⊑[g] L2 → ⦃h, L2⦄ ⊢ T •[g,l] U.
-#h #g #L1 #T #U #l #H elim H -L1 -T -U -l
-[ /2 width=1/
-| #L1 #K1 #V1 #W1 #U1 #i #l #HLK1 #HVW1 #HWU1 #IHVW1 #L2 #HL12
- elim (lsubss_ldrop_O1_conf … HL12 … HLK1) -L1 #X #H #HLK2
- elim (lsubss_inv_pair1 … H) -H * #K2 [ -HVW1 | -IHVW1 ]
- [ #HK12 #H destruct /3 width=6/
- | #V2 #l0 #H1 #H2 #_ #H #_ destruct
- elim (ssta_mono … HVW1 … H1) -HVW1 -H1 #H1 #H2 destruct
- elim (ssta_fwd_correct … H2) -H2 /2 width=6/
- ]
-| #L1 #K1 #W1 #V1 #U1 #i #l #HLK1 #_ #HWU1 #IHWV1 #L2 #HL12
- elim (lsubss_ldrop_O1_conf … HL12 … HLK1) -L1 #X #H #HLK2
- elim (lsubss_inv_pair1 … H) -H * #K2 [ | -HWU1 -IHWV1 -HLK2 ]
- [ #HK12 #H destruct /3 width=6/
- | #V2 #l0 #_ #_ #_ #_ #H destruct
- ]
-| /4 width=1/
-| /3 width=1/
-| /3 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/static/lsubss_ssta.ma".
-include "basic_2/unwind/sstas.ma".
-
-(* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************)
-
-(* Properties on lenv ref for stratified type assignment ********************)
-
-lemma lsubss_sstas_trans: ∀h,g,L2,T,U. ⦃h, L2⦄ ⊢ T •*[g] U →
- ∀L1. h ⊢ L1 •⊑[g] L2 → ⦃h, L1⦄ ⊢ T •*[g] U.
-#h #g #L2 #T #U #H @(sstas_ind_dx … H) -T // /3 width=5/
-qed.
-
-lemma lsubss_sstas_conf: ∀h,g,L1,T,U. ⦃h, L1⦄ ⊢ T •*[g] U →
- ∀L2. h ⊢ L1 •⊑[g] L2 → ⦃h, L2⦄ ⊢ T •*[g] U.
-#h #g #L2 #T #U #H @(sstas_ind_dx … H) -T // /3 width=5/
-qed.
non associative with precedence 45
for @{ 'CrSubEqB $h $L1 $L2 }.
-notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 • break [ term 46 g , break term 46 l ] break term 46 T2 )"
+notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 • break [ term 46 g ] break ⦃ term 46 l , break term 46 T2 ⦄ )"
non associative with precedence 45
- for @{ 'StaticType $h $g $l $L $T1 $T2 }.
-
-notation "hvbox( h ⊢ break term 46 L1 • ⊑ [ term 46 g ] break term 46 L2 )"
- non associative with precedence 45
- for @{ 'CrSubEqS $h $g $L1 $L2 }.
+ for @{ 'StaticType $h $g $L $T1 $T2 $l }.
(* Unwind *******************************************************************)
non associative with precedence 45
for @{ 'PConvStar $L $T1 $T2 }.
-notation "hvbox( h â\8a¢ break term 46 L1 â\8a¢ â\80¢ â\8a\91 [ term 46 g ] break term 46 L2 )"
+notation "hvbox( h â\8a¢ break term 46 L1 â\80¢ â\8a\91 break [ term 46 g ] break term 46 L2 )"
non associative with precedence 45
- for @{ 'CrSubEqSE $h $g $L1 $L2 }.
+ for @{ 'CrSubEqS $h $g $L1 $L2 }.
notation "hvbox( ⦃ term 46 L1 ⦄ ⬌ * break ⦃ term 46 L2 ⦄ )"
non associative with precedence 45
non associative with precedence 45
for @{ 'NativeValid $h $g $L $T }.
-notation "hvbox( h ⊢ break term 46 L1 ⊩ : ⊑ [ term 46 g ] break term 46 L2 )"
+notation "hvbox( h ⊢ break term 46 L1 ⊩ : ⊑ break [ term 46 g ] break term 46 L2 )"
non associative with precedence 45
for @{ 'CrSubEqV $h $g $L1 $L2 }.
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 ⦄ )"
+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 }.
.
interpretation "stratified static type assignment (term)"
- 'StaticType h g l L T U = (ssta h g l L T U).
+ 'StaticType h g L T U l = (ssta h g l L T U).
definition ssta_step: ∀h. sd h → lenv → relation term ≝ λh,g,L,T,U.
- ∃l. ⦃h, L⦄ ⊢ T •[g, l+1] U.
+ ∃l. ⦃h, L⦄ ⊢ T •[g] ⦃l+1, U⦄.
(* Basic inversion lemmas ************************************************)
-fact ssta_inv_sort1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ∀k0. T = ⋆k0 →
+fact ssta_inv_sort1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → ∀k0. T = ⋆k0 →
deg h g k0 l ∧ U = ⋆(next h k0).
#h #g #L #T #U #l * -L -T -U -l
[ #L #k #l #Hkl #k0 #H destruct /2 width=1/
qed.
(* Basic_1: was just: sty0_gen_sort *)
-lemma ssta_inv_sort1: ∀h,g,L,U,k,l. ⦃h, L⦄ ⊢ ⋆k •[g, l] U →
+lemma ssta_inv_sort1: ∀h,g,L,U,k,l. ⦃h, L⦄ ⊢ ⋆k •[g] ⦃l, U⦄ →
deg h g k l ∧ U = ⋆(next h k).
/2 width=4/ qed-.
-fact ssta_inv_lref1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ∀j. T = #j →
- (∃∃K,V,W. ⇩[0, j] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V •[g, l] W &
+fact ssta_inv_lref1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → ∀j. T = #j →
+ (∃∃K,V,W. ⇩[0, j] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V •[g] ⦃l, W⦄ &
⇧[0, j + 1] W ≡ U
) ∨
- (∃∃K,W,V,l0. ⇩[0, j] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W •[g, l0] V &
+ (∃∃K,W,V,l0. ⇩[0, j] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W •[g] ⦃l0, V⦄ &
⇧[0, j + 1] W ≡ U & l = l0 + 1
).
#h #g #L #T #U #l * -L -T -U -l
qed.
(* Basic_1: was just: sty0_gen_lref *)
-lemma ssta_inv_lref1: ∀h,g,L,U,i,l. ⦃h, L⦄ ⊢ #i •[g, l] U →
- (∃∃K,V,W. ⇩[0, i] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V •[g, l] W &
+lemma ssta_inv_lref1: ∀h,g,L,U,i,l. ⦃h, L⦄ ⊢ #i •[g] ⦃l, U⦄ →
+ (∃∃K,V,W. ⇩[0, i] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V •[g] ⦃l, W⦄ &
⇧[0, i + 1] W ≡ U
) ∨
- (∃∃K,W,V,l0. ⇩[0, i] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W •[g, l0] V &
+ (∃∃K,W,V,l0. ⇩[0, i] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W •[g] ⦃l0, V⦄ &
⇧[0, i + 1] W ≡ U & l = l0 + 1
).
/2 width=3/ qed-.
-fact ssta_inv_gref1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ∀p0. T = §p0 → ⊥.
+fact ssta_inv_gref1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → ∀p0. T = §p0 → ⊥.
#h #g #L #T #U #l * -L -T -U -l
[ #L #k #l #_ #p0 #H destruct
| #L #K #V #W #U #i #l #_ #_ #_ #p0 #H destruct
| #L #W #T #U #l #_ #p0 #H destruct
qed.
-lemma ssta_inv_gref1: ∀h,g,L,U,p,l. ⦃h, L⦄ ⊢ §p •[g, l] U → ⊥.
+lemma ssta_inv_gref1: ∀h,g,L,U,p,l. ⦃h, L⦄ ⊢ §p •[g] ⦃l, U⦄ → ⊥.
/2 width=9/ qed-.
-fact ssta_inv_bind1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U →
+fact ssta_inv_bind1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ →
∀a,I,X,Y. T = ⓑ{a,I}Y.X →
- ∃∃Z. ⦃h, L.ⓑ{I}Y⦄ ⊢ X •[g, l] Z & U = ⓑ{a,I}Y.Z.
+ ∃∃Z. ⦃h, L.ⓑ{I}Y⦄ ⊢ X •[g] ⦃l, Z⦄ & U = ⓑ{a,I}Y.Z.
#h #g #L #T #U #l * -L -T -U -l
[ #L #k #l #_ #a #I #X #Y #H destruct
| #L #K #V #W #U #i #l #_ #_ #_ #a #I #X #Y #H destruct
qed.
(* Basic_1: was just: sty0_gen_bind *)
-lemma ssta_inv_bind1: ∀h,g,a,I,L,Y,X,U,l. ⦃h, L⦄ ⊢ ⓑ{a,I}Y.X •[g, l] U →
- ∃∃Z. ⦃h, L.ⓑ{I}Y⦄ ⊢ X •[g, l] Z & U = ⓑ{a,I}Y.Z.
+lemma ssta_inv_bind1: ∀h,g,a,I,L,Y,X,U,l. ⦃h, L⦄ ⊢ ⓑ{a,I}Y.X •[g] ⦃l, U⦄ →
+ ∃∃Z. ⦃h, L.ⓑ{I}Y⦄ ⊢ X •[g] ⦃l, Z⦄ & U = ⓑ{a,I}Y.Z.
/2 width=3/ qed-.
-fact ssta_inv_appl1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ∀X,Y. T = ⓐY.X →
- ∃∃Z. ⦃h, L⦄ ⊢ X •[g, l] Z & U = ⓐY.Z.
+fact ssta_inv_appl1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → ∀X,Y. T = ⓐY.X →
+ ∃∃Z. ⦃h, L⦄ ⊢ X •[g] ⦃l, Z⦄ & U = ⓐY.Z.
#h #g #L #T #U #l * -L -T -U -l
[ #L #k #l #_ #X #Y #H destruct
| #L #K #V #W #U #i #l #_ #_ #_ #X #Y #H destruct
qed.
(* Basic_1: was just: sty0_gen_appl *)
-lemma ssta_inv_appl1: ∀h,g,L,Y,X,U,l. ⦃h, L⦄ ⊢ ⓐY.X •[g, l] U →
- ∃∃Z. ⦃h, L⦄ ⊢ X •[g, l] Z & U = ⓐY.Z.
+lemma ssta_inv_appl1: ∀h,g,L,Y,X,U,l. ⦃h, L⦄ ⊢ ⓐY.X •[g] ⦃l, U⦄ →
+ ∃∃Z. ⦃h, L⦄ ⊢ X •[g] ⦃l, Z⦄ & U = ⓐY.Z.
/2 width=3/ qed-.
-fact ssta_inv_cast1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U →
- ∀X,Y. T = ⓝY.X → ⦃h, L⦄ ⊢ X •[g, l] U.
+fact ssta_inv_cast1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ →
+ ∀X,Y. T = ⓝY.X → ⦃h, L⦄ ⊢ X •[g] ⦃l, U⦄.
#h #g #L #T #U #l * -L -T -U -l
[ #L #k #l #_ #X #Y #H destruct
| #L #K #V #W #U #l #i #_ #_ #_ #X #Y #H destruct
qed.
(* Basic_1: was just: sty0_gen_cast *)
-lemma ssta_inv_cast1: ∀h,g,L,X,Y,U,l. ⦃h, L⦄ ⊢ ⓝY.X •[g, l] U →
- ⦃h, L⦄ ⊢ X •[g, l] U.
+lemma ssta_inv_cast1: ∀h,g,L,X,Y,U,l. ⦃h, L⦄ ⊢ ⓝY.X •[g] ⦃l, U⦄ →
+ ⦃h, L⦄ ⊢ X •[g] ⦃l, U⦄.
/2 width=4/ qed-.
(* Advanced inversion lemmas ************************************************)
-lemma ssta_inv_frsupp: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ⦃L, U⦄ ⧁+ ⦃L, T⦄ → ⊥.
+lemma ssta_inv_frsupp: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → ⦃L, U⦄ ⧁+ ⦃L, T⦄ → ⊥.
#h #g #L #T #U #l #H elim H -L -T -U -l
[ #L #k #l #_ #H
elim (frsupp_inv_atom1_frsups … H)
]
qed-.
-fact ssta_inv_refl_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → T = U → ⊥.
+fact ssta_inv_refl_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → T = U → ⊥.
#h #g #L #T #U #l #H elim H -L -T -U -l
[ #L #k #l #_ #H
lapply (next_lt h k) destruct -H -e0 (**) (* destruct: these premises are not erased *)
]
qed-.
-lemma ssta_inv_refl: ∀h,g,T,L,l. ⦃h, L⦄ ⊢ T •[g, l] T → ⊥.
+lemma ssta_inv_refl: ∀h,g,T,L,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, T⦄ → ⊥.
/2 width=8 by ssta_inv_refl_aux/ qed-.
-lemma ssta_inv_frsups: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ⦃L, U⦄ ⧁* ⦃L, T⦄ → ⊥.
+lemma ssta_inv_frsups: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → ⦃L, U⦄ ⧁* ⦃L, T⦄ → ⊥.
#h #g #L #T #U #L #HTU #H elim (frsups_inv_all … H) -H
[ * #_ #H destruct /2 width=6 by ssta_inv_refl/
| /2 width=8 by ssta_inv_frsupp/
(* Properties on atomic arity assignment for terms **************************)
-lemma ssta_aaa: ∀h,g,L,T,A. L ⊢ T ⁝ A → ∀U,l. ⦃h, L⦄ ⊢ T •[g, l] U → L ⊢ U ⁝ A.
+lemma ssta_aaa: ∀h,g,L,T,A. L ⊢ T ⁝ A → ∀U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → L ⊢ U ⁝ A.
#h #g #L #T #A #H elim H -L -T -A
[ #L #k #U #l #H
elim (ssta_inv_sort1 … H) -H #_ #H destruct //
(* Properties on relocation *************************************************)
(* Basic_1: was just: sty0_lift *)
-lemma ssta_lift: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 →
+lemma ssta_lift: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ →
∀L2,d,e. ⇩[d, e] L2 ≡ L1 → ∀T2. ⇧[d, e] T1 ≡ T2 →
- ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 •[g, l] U2.
+ ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄.
#h #g #L1 #T1 #U1 #l #H elim H -L1 -T1 -U1 -l
[ #L1 #k #l #Hkl #L2 #d #e #HL21 #X1 #H1 #X2 #H2
>(lift_inv_sort1 … H1) -X1
qed.
(* Note: apparently this was missing in basic_1 *)
-lemma ssta_inv_lift1: ∀h,g,L2,T2,U2,l. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 →
+lemma ssta_inv_lift1: ∀h,g,L2,T2,U2,l. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ →
∀L1,d,e. ⇩[d, e] L2 ≡ L1 → ∀T1. ⇧[d, e] T1 ≡ T2 →
- ∃∃U1. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 & ⇧[d, e] U1 ≡ U2.
+ ∃∃U1. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ & ⇧[d, e] U1 ≡ U2.
#h #g #L2 #T2 #U2 #l #H elim H -L2 -T2 -U2 -l
[ #L2 #k #l #Hkl #L1 #d #e #_ #X #H
>(lift_inv_sort2 … H) -X /3 width=3/
(* Advanced forvard lemmas **************************************************)
(* Basic_1: was just: sty0_correct *)
-lemma ssta_fwd_correct: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U →
- ∃T0. ⦃h, L⦄ ⊢ U •[g, l - 1] T0.
+lemma ssta_fwd_correct: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ →
+ ∃T0. ⦃h, L⦄ ⊢ U •[g] ⦃l-1, T0⦄.
#h #g #L #T #U #l #H elim H -L -T -U -l
[ /4 width=2/
| #L #K #V #W #W0 #i #l #HLK #_ #HW0 * #V0 #HWV0
(* Properties about dx parallel unfold **************************************)
(* Note: apparently this was missing in basic_1 *)
-lemma ssta_ltpss_dx_tpss_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 →
+lemma ssta_ltpss_dx_tpss_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ →
∀L2,d,e. L1 ▶* [d, e] L2 →
∀T2. L2 ⊢ T1 ▶* [d, e] T2 →
- ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 &
+ ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ &
L2 ⊢ U1 ▶* [d, e] U2.
#h #g #L1 #T1 #U #l #H elim H -L1 -T1 -U -l
[ #L1 #k1 #l1 #Hkl1 #L2 #d #e #_ #T2 #H
]
qed.
-lemma ssta_ltpss_dx_tps_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 →
+lemma ssta_ltpss_dx_tps_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ →
∀L2,d,e. L1 ▶* [d, e] L2 →
∀T2. L2 ⊢ T1 ▶ [d, e] T2 →
- ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 &
+ ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, 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 →
+lemma ssta_ltpss_dx_conf: ∀h,g,L1,T,U1,l. ⦃h, L1⦄ ⊢ T •[g] ⦃l, U1⦄ →
∀L2,d,e. L1 ▶* [d, e] L2 →
- ∃∃U2. ⦃h, L2⦄ ⊢ T •[g, l] U2 & L2 ⊢ U1 ▶* [d, e] U2.
+ ∃∃U2. ⦃h, L2⦄ ⊢ T •[g] ⦃l, U2⦄ & L2 ⊢ U1 ▶* [d, e] U2.
/2 width=5/ qed.
-lemma ssta_tpss_conf: ∀h,g,L,T1,U1,l. ⦃h, L⦄ ⊢ T1 •[g, l] U1 →
+lemma ssta_tpss_conf: ∀h,g,L,T1,U1,l. ⦃h, L⦄ ⊢ T1 •[g] ⦃l, U1⦄ →
∀T2,d,e. L ⊢ T1 ▶* [d, e] T2 →
- ∃∃U2. ⦃h, L⦄ ⊢ T2 •[g, l] U2 & L ⊢ U1 ▶* [d, e] U2.
+ ∃∃U2. ⦃h, L⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L ⊢ U1 ▶* [d, e] U2.
/2 width=5/ qed.
-lemma ssta_tps_conf: ∀h,g,L,T1,U1,l. ⦃h, L⦄ ⊢ T1 •[g, l] U1 →
+lemma ssta_tps_conf: ∀h,g,L,T1,U1,l. ⦃h, L⦄ ⊢ T1 •[g] ⦃l, U1⦄ →
∀T2,d,e. L ⊢ T1 ▶ [d, e] T2 →
- ∃∃U2. ⦃h, L⦄ ⊢ T2 •[g, l] U2 & L ⊢ U1 ▶* [d, e] U2.
+ ∃∃U2. ⦃h, L⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L ⊢ U1 ▶* [d, e] U2.
/2 width=5/ qed.
(* Properties about sn parallel unfold **************************************)
-lemma ssta_ltpss_sn_conf: ∀h,g,L1,T,U1,l. ⦃h, L1⦄ ⊢ T •[g, l] U1 →
+lemma ssta_ltpss_sn_conf: ∀h,g,L1,T,U1,l. ⦃h, L1⦄ ⊢ T •[g] ⦃l, U1⦄ →
∀L2,d,e. L1 ⊢ ▶* [d, e] L2 →
- ∃∃U2. ⦃h, L2⦄ ⊢ T •[g, l] U2 & L1 ⊢ U1 ▶* [d, e] U2.
+ ∃∃U2. ⦃h, L2⦄ ⊢ T •[g] ⦃l, U2⦄ & L1 ⊢ U1 ▶* [d, e] U2.
#h #g #L1 #T #U1 #l #HTU1 #L2 #d #e #HL12
lapply (ltpss_sn_ltpssa … HL12) -HL12 #HL12
@(ltpssa_ind … HL12) -L2 [ /2 width=3/ ] -HTU1
lapply (tpss_trans_eq … HU1 HU2) -U /2 width=3/
qed.
-lemma ssta_ltpss_sn_tpss_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 →
+lemma ssta_ltpss_sn_tpss_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ →
∀L2,d,e. L1 ⊢ ▶* [d, e] L2 →
∀T2. L2 ⊢ T1 ▶* [d, e] T2 →
- ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 &
+ ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ &
L1 ⊢ U1 ▶* [d, e] U2.
#h #g #L1 #T1 #U1 #l #HTU1 #L2 #d #e #HL12 #T2 #HT12
elim (ssta_ltpss_sn_conf … HTU1 … HL12) -HTU1 #U #HT1U #HU1
lapply (tpss_trans_eq … HU1 HU2) -U /2 width=3/
qed.
-lemma ssta_ltpss_sn_tps_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 →
+lemma ssta_ltpss_sn_tps_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ →
∀L2,d,e. L1 ⊢ ▶* [d, e] L2 →
∀T2. L2 ⊢ T1 ▶ [d, e] T2 →
- ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 &
+ ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ &
L1 ⊢ U1 ▶* [d, e] U2.
/3 width=3/ qed.
(* Main properties **********************************************************)
(* Note: apparently this was missing in basic_1 *)
-theorem ssta_mono: ∀h,g,L,T,U1,l1. ⦃h, L⦄ ⊢ T •[g, l1] U1 →
- ∀U2,l2. ⦃h, L⦄ ⊢ T •[g, l2] U2 → l1 = l2 ∧ U1 = U2.
+theorem ssta_mono: ∀h,g,L,T,U1,l1. ⦃h, L⦄ ⊢ T •[g] ⦃l1, U1⦄ →
+ ∀U2,l2. ⦃h, L⦄ ⊢ T •[g] ⦃l2, U2⦄ → l1 = l2 ∧ U1 = U2.
#h #g #L #T #U1 #l1 #H elim H -L -T -U1 -l1
[ #L #k #l #Hkl #X #l2 #H
elim (ssta_inv_sort1 … H) -H #Hkl2 #H destruct
lemma sstas_ind: ∀h,g,L,T. ∀R:predicate term.
R T → (
- ∀U1,U2,l. ⦃h, L⦄ ⊢ T •* [g] U1 → ⦃h, L⦄ ⊢ U1 •[g, l + 1] U2 →
+ ∀U1,U2,l. ⦃h, L⦄ ⊢ T •* [g] U1 → ⦃h, L⦄ ⊢ U1 •[g] ⦃l+1, U2⦄ →
R U1 → R U2
) →
∀U. ⦃h, L⦄ ⊢ T •*[g] U → R U.
lemma sstas_ind_dx: ∀h,g,L,U2. ∀R:predicate term.
R U2 → (
- ∀T,U1,l. ⦃h, L⦄ ⊢ T •[g, l + 1] U1 → ⦃h, L⦄ ⊢ U1 •* [g] U2 →
+ ∀T,U1,l. ⦃h, L⦄ ⊢ T •[g] ⦃l+1, U1⦄ → ⦃h, L⦄ ⊢ U1 •* [g] U2 →
R U1 → R T
) →
∀T. ⦃h, L⦄ ⊢ T •*[g] U2 → R T.
lemma sstas_refl: ∀h,g,L. reflexive … (sstas h g L).
// qed.
-lemma ssta_sstas: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l+1] U → ⦃h, L⦄ ⊢ T •*[g] U.
+lemma ssta_sstas: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l+1, U⦄ → ⦃h, L⦄ ⊢ T •*[g] U.
/3 width=2 by R_to_star, ex_intro/ qed. (**) (* auto fails without trace *)
-lemma sstas_strap1: ∀h,g,L,T1,T2,U2,l. ⦃h, L⦄ ⊢ T1 •*[g] T2 → ⦃h, L⦄ ⊢ T2 •[g,l+1] U2 →
+lemma sstas_strap1: ∀h,g,L,T1,T2,U2,l. ⦃h, L⦄ ⊢ T1 •*[g] T2 → ⦃h, L⦄ ⊢ T2 •[g] ⦃l+1, U2⦄ →
⦃h, L⦄ ⊢ T1 •*[g] U2.
/3 width=4 by sstep, ex_intro/ (**) (* auto fails without trace *)
qed.
-lemma sstas_strap2: ∀h,g,L,T1,U1,U2,l. ⦃h, L⦄ ⊢ T1 •[g, l+1] U1 → ⦃h, L⦄ ⊢ U1 •*[g] U2 →
+lemma sstas_strap2: ∀h,g,L,T1,U1,U2,l. ⦃h, L⦄ ⊢ T1 •[g] ⦃l+1, U1⦄ → ⦃h, L⦄ ⊢ U1 •*[g] U2 →
⦃h, L⦄ ⊢ T1 •*[g] U2.
/3 width=3 by star_compl, ex_intro/ (**) (* auto fails without trace *)
qed.
(* Advanced forward lemmas **************************************************)
-lemma sstas_fwd_correct: ∀h,g,L,T1,U1,l1. ⦃h, L⦄ ⊢ T1 •[g, l1] U1 →
+lemma sstas_fwd_correct: ∀h,g,L,T1,U1,l1. ⦃h, L⦄ ⊢ T1 •[g] ⦃l1, U1⦄ →
∀T2. ⦃h, L⦄ ⊢ T1 •*[g] T2 →
- ∃∃U2,l2. ⦃h, L⦄ ⊢ T2 •[g, l2] U2.
+ ∃∃U2,l2. ⦃h, L⦄ ⊢ T2 •[g] ⦃l2, U2⦄.
#h #g #L #T1 #U1 #l1 #HTU1 #T2 #H @(sstas_ind … H) -T2 [ /2 width=3/ ] -HTU1
#T #T2 #l #_ #HT2 * #U #l0 #_ -l0
elim (ssta_fwd_correct … HT2) -T /2 width=3/
(* Advanced inversion lemmas ************************************************)
lemma sstas_inv_O: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U →
- ∀T0. ⦃h, L⦄ ⊢ T •[g , 0] T0 → U = T.
+ ∀T0. ⦃h, L⦄ ⊢ T •[g] ⦃0, T0⦄ → U = T.
#h #g #L #T #U #H @(sstas_ind_dx … H) -T //
#T0 #U0 #l0 #HTU0 #_ #_ #T1 #HT01
elim (ssta_mono … HTU0 … HT01) <plus_n_Sm #H destruct
(* Advanced properties ******************************************************)
lemma sstas_strip: ∀h,g,L,T,U1. ⦃h, L⦄ ⊢ T •*[g] U1 →
- ∀U2,l. ⦃h, L⦄ ⊢ T •[g, l] U2 →
+ ∀U2,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U2⦄ →
T = U1 ∨ ⦃h, L⦄ ⊢ U2 •*[g] U1.
#h #g #L #T #U1 #H1 @(sstas_ind_dx … H1) -T /2 width=1/
#T #U #l0 #HTU #HU1 #_ #U2 #l #H2
Extended context-sensitive strong normalization
for simply typed terms.
</news>
+ <news date="2013 March 16.">
+ Mutual recursive preservation of stratified native validity
+ for hyper computation on closures.
+ </news>
<news date="2012 October 16.">
Confluence for context-free parallel reduction on closures.
</news>
[ "fpcs ( ⦃?,?⦄ ⬌* ⦃?,?⦄ )" "fpcs_aaa" + "fpcs_cpcs" + "fpcs_fprs" + "fpcs_fpcs" * ]
}
]
- [ { "local env. ref. for context-sensitive equivalence" * } {
- [ "lsubse ( ? ⊢•⊑[?] ? )" "lsubse_ldrop" + "lsubse_ssta" + "lsubse_cpcs" * ]
+ [ { "local env. ref. for stratified static type assignment" * } {
+ [ "lsubss ( ? •⊑[?] ? )" "lsubss_ldrop" + "lsubss_ssta" + "lsubss_cpcs" * ]
}
]
[ { "context-sensitive equivalence" * } {
]
class "grass"
[ { "static typing" * } {
-(*
- [ { "local env. ref. for stratified static type assignment" * } {
- [ "lsubss ( ? •⊑[?] ? )" "lsubss_ldrop" + "lsubss_ssta" + "lsubss_lsubss" * ]
- }
- ]
-*)
[ { "stratified static type assignment" * } {
[ "ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )" "ssta_lift" + "ssta_ltpss_dx" + "ssta_ltpss_sn" + "ssta_aaa" + "ssta_ssta" * ]
}
<?xml version="1.0" encoding="utf-8"?>
<helm_registry>
- <section name="matita">
- <key name="rt_base_dir">$(MATITA_RT_BASE_DIR)</key>
- </section>
<section name="xoa">
<key name="output_dir">contribs/lambdadelta/ground_2/</key>
<key name="objects">xoa</key>
projects / helm.git / commitdiff