update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / substitution / prelift_label.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_label.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_label.ma
index e4a9c0596c7ba79d887f94a20ce4c1731003b100..8dc8af8f8448c1bd4ca693fc2ee4304eb34075fd 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_label.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_label.ma
@@ -12,15 +12,15 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/notation/functions/uparrow_2.ma".
+include "delayed_updating/notation/functions/uptrianglearrow_2.ma".
 include "delayed_updating/syntax/label.ma".
-include "ground/relocation/tr_pap.ma".
+include "ground/relocation/tr_pap_pap.ma".
 
 (* PRELIFT FOR LABEL ********************************************************)
 
 definition prelift_label (f) (l): label ≝
 match l with
-[ label_d n ⇒ 𝗱(f＠⧣❨n❩)
+[ label_d k ⇒ 𝗱(f＠⧣❨k❩)
 | label_m   ⇒ 𝗺
 | label_L   ⇒ 𝗟
 | label_A   ⇒ 𝗔
@@ -29,26 +29,99 @@ match l with
 
 interpretation
   "prelift (label)"
-  'UpArrow f l = (prelift_label f l).
+  'UpTriangleArrow f l = (prelift_label f l).
 
 (* Basic constructions ******************************************************)
 
-lemma prelift_label_d (f) (n):
-      (𝗱(f＠⧣❨n❩)) = ↑[f]𝗱n.
+lemma prelift_label_d (f) (k):
+      (𝗱(f＠⧣❨k❩)) = 🠡[f]𝗱k.
 // qed.
 
 lemma prelift_label_m (f):
-      (𝗺) = ↑[f]𝗺.
+      (𝗺) = 🠡[f]𝗺.
 // qed.
 
 lemma prelift_label_L (f):
-      (𝗟) = ↑[f]𝗟.
+      (𝗟) = 🠡[f]𝗟.
 // qed.
 
 lemma prelift_label_A (f):
-      (𝗔) = ↑[f]𝗔.
+      (𝗔) = 🠡[f]𝗔.
 // qed.
 
 lemma prelift_label_S (f):
-      (𝗦) = ↑[f]𝗦.
+      (𝗦) = 🠡[f]𝗦.
 // qed.
+
+(* Basic inversions *********************************************************)
+
+lemma prelift_label_inv_d_sn (f) (l) (k1):
+      (𝗱k1) = 🠡[f]l →
+      ∃∃k2. k1 = f＠⧣❨k2❩ & 𝗱k2 = l.
+#f * [ #k ] #k1
+[ <prelift_label_d
+| <prelift_label_m
+| <prelift_label_L
+| <prelift_label_A
+| <prelift_label_S
+] #H0 destruct
+/2 width=3 by ex2_intro/
+qed-.
+
+lemma prelift_label_inv_m_sn (f) (l):
+      (𝗺) = 🠡[f]l → 𝗺 = l.
+#f * [ #k ]
+[ <prelift_label_d
+| <prelift_label_m
+| <prelift_label_L
+| <prelift_label_A
+| <prelift_label_S
+] #H0 destruct //
+qed-.
+
+lemma prelift_label_inv_L_sn (f) (l):
+      (𝗟) = 🠡[f]l → 𝗟 = l.
+#f * [ #k ]
+[ <prelift_label_d
+| <prelift_label_m
+| <prelift_label_L
+| <prelift_label_A
+| <prelift_label_S
+] #H0 destruct //
+qed-.
+
+lemma prelift_label_inv_A_sn (f) (l):
+      (𝗔) = 🠡[f]l → 𝗔 = l.
+#f * [ #k ]
+[ <prelift_label_d
+| <prelift_label_m
+| <prelift_label_L
+| <prelift_label_A
+| <prelift_label_S
+] #H0 destruct //
+qed-.
+
+lemma prelift_label_inv_S_sn (f) (l):
+      (𝗦) = 🠡[f]l → 𝗦 = l.
+#f * [ #k ]
+[ <prelift_label_d
+| <prelift_label_m
+| <prelift_label_L
+| <prelift_label_A
+| <prelift_label_S
+] #H0 destruct //
+qed-.
+
+(* Main inversions **********************************************************)
+
+theorem prelift_label_inj (f) (l1) (l2):
+        🠡[f]l1 = 🠡[f]l2 → l1 = l2.
+#f * [ #k1 ] #l2 #Hl
+[ elim (prelift_label_inv_d_sn … Hl) -Hl #k2 #Hk #H0 destruct
+  >(tr_pap_inj ???? Hk) -Hk //
+| <(prelift_label_inv_m_sn … Hl) -l2 //
+| <(prelift_label_inv_L_sn … Hl) -l2 //
+| <(prelift_label_inv_A_sn … Hl) -l2 //
+| <(prelift_label_inv_S_sn … Hl) -l2 //
+]
+qed-.