--- /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/grammar/lenv_length.ma".
+
+(* LOCAL ENVIRONMENT EQUALITY ***********************************************)
+
+notation "hvbox( T1 break [ d , break e ] ≈ break T2 )"
+ non associative with precedence 45
+ for @{ 'Eq $T1 $d $e $T2 }.
+
+inductive leq: nat → nat → relation lenv ≝
+| leq_sort: ∀d,e. leq d e (⋆) (⋆)
+| leq_OO: ∀L1,L2. leq 0 0 L1 L2
+| leq_eq: ∀L1,L2,I,V,e. leq 0 e L1 L2 →
+ leq 0 (e + 1) (L1. 𝕓{I} V) (L2.𝕓{I} V)
+| leq_skip: ∀L1,L2,I1,I2,V1,V2,d,e.
+ leq d e L1 L2 → leq (d + 1) e (L1. 𝕓{I1} V1) (L2. 𝕓{I2} V2)
+.
+
+interpretation "local environment equality" 'Eq L1 d e L2 = (leq d e L1 L2).
+
+definition leq_repl_dx: ∀S. (lenv → relation S) → Prop ≝ λS,R.
+ ∀L1,s1,s2. R L1 s1 s2 →
+ ∀L2,d,e. L1 [d, e]≈ L2 → R L2 s1 s2.
+
+(* Basic properties *********************************************************)
+
+lemma TC_leq_repl_dx: ∀S,R. leq_repl_dx S R → leq_repl_dx S (λL. (TC … (R L))).
+#S #R #HR #L1 #s1 #s2 #H elim H -H s2
+[ /3 width=5/
+| #s #s2 #_ #Hs2 #IHs1 #L2 #d #e #HL12
+ lapply (HR … Hs2 … HL12) -HR Hs2 HL12 /3/
+]
+qed.
+
+lemma leq_refl: ∀d,e,L. L [d, e] ≈ L.
+#d elim d -d
+[ #e elim e -e // #e #IHe #L elim L -L /2/
+| #d #IHd #e #L elim L -L /2/
+]
+qed.
+
+lemma leq_sym: ∀L1,L2,d,e. L1 [d, e] ≈ L2 → L2 [d, e] ≈ L1.
+#L1 #L2 #d #e #H elim H -H L1 L2 d e /2/
+qed.
+
+lemma leq_skip_lt: ∀L1,L2,d,e. L1 [d - 1, e] ≈ L2 → 0 < d →
+ ∀I1,I2,V1,V2. L1. 𝕓{I1} V1 [d, e] ≈ L2. 𝕓{I2} V2.
+
+#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) /2/
+qed.
+
+(* Basic inversion lemmas ***************************************************)
--- /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/grammar/lenv_length.ma".
+
+(* LOCAL ENVIRONMENT EQUALITY ***********************************************)
+
+interpretation "local environment equality" 'Eq L1 d e L2 = (leq L1 d e L2).
+
+(* Basic properties *********************************************************)
+
+| leq_comp: ∀L1,L2,I1,I2,V1,V2.
+ leq L1 0 0 L2 → leq (L1. 𝕓{I1} V1) 0 0 (L2. 𝕓{I2} V2)
+
+lemma leq_fwd_length: ∀L1,L2,d,e. L1 [d, e] ≈ L2 → |L1| = |L2|.
+#L1 #L2 #d #e #H elim H -H L1 L2 d e; normalize //
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma leq_inv_sort1_aux: ∀L1,L2,d,e. L1 [d, e] ≈ L2 → L1 = ⋆ → L2 = ⋆.
+#L1 #L2 #d #e #H elim H -H L1 L2 d e
+[ //
+| #L1 #L2 #I1 #I2 #V1 #V2 #_ #_ #H destruct
+| #L1 #L2 #I #V #e #_ #_ #H destruct
+| #L1 #L2 #I1 #I2 #V1 #V2 #d #e #_ #_ #H destruct
+qed.
+
+lemma leq_inv_sort1: ∀L2,d,e. ⋆ [d, e] ≈ L2 → L2 = ⋆.
+/2 width=5/ qed.
+
+lemma leq_inv_sort2: ∀L1,d,e. L1 [d, e] ≈ ⋆ → L1 = ⋆.
+/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/notation/relations/leqdx_3.ma".
+include "basic_2/grammar/lenv_length.ma".
+
+(* DX GUARDED EQUIVALENCE FOR LOCAL ENVIRONMENTS ****************************)
+
+inductive leqdx: nat → relation lenv ≝
+| leqdx_atom: ∀d. leqdx d (⋆) (⋆)
+| leqdx_zero: ∀I1,I2,L1,L2,V1,V2.
+ leqdx 0 L1 L2 → leqdx 0 (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2)
+| leqdx_succ: ∀I,L1,L2,V,d.
+ leqdx d L1 L2 → leqdx (d+1) (L1.ⓑ{I}V) (L2.ⓑ{I}V)
+.
+
+interpretation
+ "guarded equivalence (local environment, dx variant)"
+ 'LEqDx d L1 L2 = (leqdx d L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma leqdx_O: ∀L1,L2. |L1| = |L2| → L1 ≚[0] L2.
+#L1 elim L1 -L1
+[ #L2 #H >(length_inv_zero_sn … H) -L2 //
+| #L1 #I1 #V1 #IHL1 #X #H elim (length_inv_pos_sn … H) -H
+ #I2 #L2 #V2 #HL12 #H destruct /3 width=1 by leqdx_zero/
+]
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact leqdx_inv_succ2_aux: ∀L1,L2,d. L1 ≚[d] L2 →
+ ∀I,K2,V,e. L2 = K2.ⓑ{I}V → d = e + 1 →
+ ∃∃K1. K1 ≚[e] K2 & L1 = K1.ⓑ{I}V.
+#L1 #L2 #d * -L1 -L2 -d
+[ #d #J #K2 #W #e #H destruct
+| #I1 #I2 #L1 #L2 #V1 #V2 #_ #J #K2 #W #e #_
+ >commutative_plus normalize #H destruct
+| #I #L1 #L2 #V #d #HL12 #J #K2 #W #e #H1 #H2 destruct
+ /2 width=3 by ex2_intro/
+]
+qed-.
+
+lemma leqdx_inv_succ2: ∀I,L1,K2,V,d. L1 ≚[d+1] K2.ⓑ{I}V →
+ ∃∃K1. K1 ≚[d] K2 & L1 = K1.ⓑ{I}V.
+/2 width=5 by leqdx_inv_succ2_aux/ 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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( L1 ≚ break [ term 46 d ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'LEqDx $d $L1 $L2 }.
(* PLUS-ITERATED SUPCLOSURE *************************************************)
-(* Main propertis ***********************************************************)
+(* Main properties **********************************************************)
theorem fqup_trans: tri_transitive … fqup.
/2 width=5 by tri_TC_transitive/ 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/relocation/fqu_lleq.ma".
+include "basic_2/substitution/fqup.ma".
+
+(* PLUS-ITERATED SUPCLOSURE *************************************************)
+
+(* Properties on lazy equivalence for local environments ********************)
+
+lemma lleq_fqup_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃+ ⦃G2, K2, U⦄ →
+ ∀L1. L1 ⋕[0, T] L2 →
+ ∃∃K1. ⦃G1, L1, T⦄ ⊃+ ⦃G2, K1, U⦄ & K1 ⋕[0, U] K2.
+#G1 #G2 #L2 #K2 #T #U #H @(fqup_ind … H) -G2 -K2 -U
+[ #G2 #K2 #U #HTU #L1 #HL12 elim (lleq_fqu_trans … HTU … HL12) -L2
+ /3 width=3 by fqu_fqup, ex2_intro/
+| #G #G2 #K #K2 #U #U2 #_ #HU2 #IHTU #L1 #HL12 elim (IHTU … HL12) -L2
+ #K1 #HTU #HK1 elim (lleq_fqu_trans … HU2 … HK1) -K
+ /3 width=5 by fqup_strap1, ex2_intro/
+]
+qed-.
(* STAR-ITERATED SUPCLOSURE *************************************************)
-(* Advaveded properties *****************************************************)
+(* Main properties **********************************************************)
theorem fqus_trans: tri_transitive … fqus.
/2 width=5 by tri_TC_transitive/ 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/substitution/fqup_lleq.ma".
+include "basic_2/substitution/fqus_alt.ma".
+
+(* STAR-ITERATED SUPCLOSURE *************************************************)
+
+(* Properties on lazy equivalence for local environments ********************)
+
+lemma lleq_fqus_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃* ⦃G2, K2, U⦄ →
+ ∀L1. L1 ⋕[0, T] L2 →
+ ∃∃K1. ⦃G1, L1, T⦄ ⊃* ⦃G2, K1, U⦄ & K1 ⋕[0, U] K2.
+#G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fqus_inv_gen … H) -H
+[ #H elim (lleq_fqup_trans … H … HL12) -L2 /3 width=3 by fqup_fqus, ex2_intro/
+| * #HG #HL #HT destruct /2 width=3 by ex2_intro/
+]
+qed-.
<section>Logical Structure of the Specification</section>
<body>The source files are grouped in planes and components
according to the following table.
- A notation file covering the whole specification is provided.
+ Notation files covering the whole specification are provided.
The notation for the relations or functions introduced in each file
is shown in parentheses (? are placeholders).
</body>
]
[ { "context-sensitive extended computation" * } {
[ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? )" "lpxs_ldrop" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ]
- [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_lift" + "cpxs_aaa" + "cpxs_cpxs" * ]
+ [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ]
}
]
[ { "context-sensitive computation" * } {
}
]
[ { "context-sensitive extended reduction" * } {
- [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_aaa" + "lpx_lpx" * ]
- [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_lift" + "cpx_cix" + "cpx_cpx" * ]
+ [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_lleq" + "lpx_aaa" * ]
+ [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_lift" + "cpx_lleq" + "cpx_cix" * ]
}
]
[ { "context-sensitive extended irreducible forms" * } {
}
]
[ { "iterated structural successor for closures" * } {
- [ "fqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )" "fqus_alt" + "fqus_fqus" * ]
- [ "fqup ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ )" "fqup_fqup" * ]
+ [ "fqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )" "fqus_alt" + "fqus_lleq" + "fqus_fqus" * ]
+ [ "fqup ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ )" "fqup_lleq" + "fqup_fqup" * ]
}
]
[ { "generic local env. slicing" * } {
class "orange"
[ { "relocation" * } {
[ { "structural successor for closures" * } {
- [ "fquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )" "fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )" "fquq_fquq" * ]
- [ "fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )" "fqu_fqu" * ]
+ [ "fquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )" "fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )" "fquq_lleq" * ]
+ [ "fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )" "fqu_lleq" * ]
}
]
[ { "lazy equivalence for local environments" * } {
- [ "lleq ( ? ⋕[?] ? )" "lleq_fleq" * ]
+ [ "lleq ( ? ⋕[?,?] ? )" "lleq_lleq" * ]
}
]
[ { "global env. slicing" * } {
}
]
[ { "basic local env. slicing" * } {
- [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_append" + "ldrop_lpx_sn" + "ldrop_ldrop" * ]
+ [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_append" + "ldrop_lpx_sn" + "ldrop_leq" + "ldrop_ldrop" * ]
}
]
[ { "basic term relocation" * } {
]
class "red"
[ { "grammar" * } {
+ [ { "equivalence for local environments" * } {
+ [ "leq ( ? ≃[?,?] ? ) " * ]
+ }
+ ]
[ { "pointwise extension of a relation" * } {
[ "lpx_sn" "lpx_sn_tc" + "lpx_sn_lpx_sn" * ]
}
]
class "yellow"
[ { "natural numbers with infinity" * } {
- [ "ynat ( ∞ )" "ynat_pred ( ⫰? )" "ynat_succ ( ⫯? )" "ynat_le ( ?≤? )" "ynat_lt ( ?<? )" "ynat_plus ( ? + ? )" * ]
+ [ "ynat ( ∞ )" "ynat_pred ( ⫰? )" "ynat_succ ( ⫯? )" "ynat_le ( ?≤? )" "ynat_lt ( ?<? )" "ynat_minus ( ? - ? )" "ynat_plus ( ? + ? )" * ]
}
]
class "orange"
projects / helm.git / commitdiff