lambda_delta: global environments handling: redefined and first results

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / substitution / gdrop.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop.ma
index 5cef649377b112aa4b87ba9d01415ef9587ee148..2f677cb2ff3f6bcecf00df2ea4ea417f2ef1471c 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop.ma
@@ -12,33 +12,69 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Basic_2/substitution/ldrop.ma".
+include "Basic_2/grammar/genv.ma".
 
 (* GLOBAL ENVIRONMENT SLICING ***********************************************)
 
-inductive gdrop (e:nat) (G1:lenv) : predicate lenv ≝
-| gdrop_lt: ∀G2. e < |G1| → ⇓[0, |G1| - (e + 1)] G1 ≡ G2 → gdrop e G1 G2
-| gdrop_ge: |G1| ≤ e → gdrop e G1 (⋆)
+inductive gdrop (e:nat): relation genv ≝
+| gdrop_gt: ∀G. |G| ≤ e → gdrop e G (⋆)
+| gdrop_eq: ∀G. |G| = e + 1 → gdrop e G G
+| gdrop_lt: ∀I,G1,G2,V. e < |G1| → gdrop e G1 G2 → gdrop e (G1. 𝕓{I} V) G2
 .
 
-interpretation "global slicing" 'RGDrop e G1 G2 = (gdrop e G1 G2).
+interpretation "global slicing" 
+   'RLDrop e G1 G2 = (gdrop e G1 G2).
 
 (* basic inversion lemmas ***************************************************)
-(*
-fact gdrop_inv_atom2_aux: ∀G1,G2,e. ⇓[e] G1 ≡ G2 → G2 = ⋆ → |G1| ≤ e.
-#G1 #G2 #e * -G2 //
-#G2 #He #HG12 #H destruct
-lapply (ldrop_fwd_O1_length … HG12) -HG12
->minus_le_minus_minus_comm // -He >le_plus_minus_comm // <minus_n_n
->(commutative_plus e) normalize #H destruct
-qed.
 
-lemma gdrop_inv_atom2: ∀G1,e. ⇓[e] G1 ≡ ⋆ → |G1| ≤ e.
-/2 width=3/ qed-.
+lemma gdrop_inv_gt: ∀G1,G2,e. ⇓[e] G1 ≡ G2 → |G1| ≤ e → G2 = ⋆.
+#G1 #G2 #e * -G1 -G2 //
+[ #G #H >H -H >commutative_plus #H
+  lapply (le_plus_to_le_r … 0 H) -H #H
+  lapply (le_n_O_to_eq … H) -H #H destruct
+| #I #G1 #G2 #V #H1 #_ #H2
+  lapply (le_to_lt_to_lt … H2 H1) -H2 -H1 normalize in ⊢ (? % ? → ?); >commutative_plus #H
+  lapply (lt_plus_to_lt_l … 0 H) -H #H
+  elim (lt_zero_false … H)
+]
+qed-.
 
-lemma gdrop_inv_ge: ∀G1,G2,e. ⇓[e] G1 ≡ G2 → |G1| ≤ e → G2 = ⋆.
-#G1 #G2 #e * // #G2 #H1 #_ #H2
-lapply (lt_to_le_to_lt … H1 H2) -H1 -H2 #He
-elim (lt_refl_false … He)
+lemma gdrop_inv_eq: ∀G1,G2,e. ⇓[e] G1 ≡ G2 → |G1| = e + 1 → G1 = G2.
+#G1 #G2 #e * -G1 -G2 //
+[ #G #H1 #H2 >H2 in H1; -H2 >commutative_plus #H
+  lapply (le_plus_to_le_r … 0 H) -H #H
+  lapply (le_n_O_to_eq … H) -H #H destruct
+| #I #G1 #G2 #V #H1 #_ normalize #H2
+  <(injective_plus_l … H2) in H1; -H2 #H
+  elim (lt_refl_false … H)
+]
 qed-.
-*)
+
+fact gdrop_inv_lt_aux: ∀I,G,G1,G2,V,e. ⇓[e] G ≡ G2 → G = G1. 𝕓{I} V →
+                       e < |G1| → ⇓[e] G1 ≡ G2.
+#I #G #G1 #G2 #V #e * -G -G2
+[ #G #H1 #H destruct #H2
+  lapply (le_to_lt_to_lt … H1 H2) -H1 -H2 normalize in ⊢ (? % ? → ?); >commutative_plus #H
+  lapply (lt_plus_to_lt_l … 0 H) -H #H
+  elim (lt_zero_false … H)
+| #G #H1 #H2 destruct >(injective_plus_l … H1) -H1 #H
+  elim (lt_refl_false … H)
+| #J #G #G2 #W #_ #HG2 #H destruct //
+]
+qed.
+
+lemma gdrop_inv_lt: ∀I,G1,G2,V,e.
+                    ⇓[e] G1. 𝕓{I} V ≡ G2 → e < |G1| → ⇓[e] G1 ≡ G2.
+/2 width=5/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma gdrop_total: ∀e,G1. ∃G2. ⇓[e] G1 ≡ G2.
+#e #G1 elim G1 -G1 /3 width=2/
+#I #V #G1 * #G2 #HG12
+elim (lt_or_eq_or_gt e (|G1|)) #He
+[ /3 width=2/
+| destruct /3 width=2/
+| @ex_intro [2: @gdrop_gt normalize /2 width=1/ | skip ] (**) (* explicit constructor *)
+]
+qed.