From c27d792e734c91a9b80cf8456e2c755aae24e994 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 15 Oct 2018 23:09:15 +0200
Subject: [PATCH] auxiliary update in basic_2

- work in progress to justify the type rules for application
---
 .../lambdadelta/basic_2/dynamic/notes.txt     | 14 +++++
 .../basic_2/dynamic/nta_preserve.ma           | 25 ++++++++
 .../lambdadelta/basic_2/etc/cpr_cpm.etc       | 57 +++++++++++++++++++
 .../basic_2/rt_computation/cpms_cpms.ma       | 24 ++++++++
 .../basic_2/rt_computation/cpms_cpr.ma        | 42 ++++++++++++++
 .../lambdadelta/basic_2/rt_transition/cpm.ma  | 16 ++++++
 6 files changed, 178 insertions(+)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/notes.txt
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpr_cpm.etc
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpr.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/notes.txt b/matita/matita/contribs/lambdadelta/basic_2/dynamic/notes.txt
new file mode 100644
index 000000000..f4fa2049e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/notes.txt
@@ -0,0 +1,14 @@
+                D I 
+sort            * *
+lref ldef       *
+lref ldec       *
+lref lref       *
+lref ldef drops *
+lref ldec drops *
+bind            * *
+appl appl       * *
+appl beta       *
+appl pure       *
+cast new        * *
+cast old        * *
+conv            *
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma
index 4e37eb806..464e8603a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma
@@ -94,6 +94,31 @@ elim (cnv_cpms_conf … H1 … H2 … HVTU) -H1 -H2 -HVTU <minus_n_n #X0 #HX0 #H
 /3 width=5 by cprs_div, cprs_trans/
 qed-.
 
+lemma nta_inv_pure_sn_cnv (h) (G) (L) (X2):
+                          ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T :*[h] X2 →
+                          ∨∨ ∃∃p,W,T0,U0. ⦃G,L⦄ ⊢ V :*[h] W & ⦃G,L⦄ ⊢ ⓛ{p}W.T0 :*[h] ⓛ{p}W.U0 & ⦃G,L⦄ ⊢ T ➡*[h] ⓛ{p}W.T0 & ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.U0 ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 !*[h]
+                           | ∃∃U. ⦃G,L⦄ ⊢ T :*[h] U & ⦃G,L⦄ ⊢ ⓐV.U !*[h] & ⦃G,L⦄ ⊢ ⓐV.U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 !*[h].
+#h #G #L #X2 #V #T #H
+elim (cnv_inv_cast … H) -H #X1 #HX2 #H1 #HX21 #H
+elim (cnv_inv_appl … H1) -H1 * [| #n ] #p #W0 #T0 #_ #HV #HT #HW0 #HT0
+lapply (cnv_cpms_trans … HT … HT0) #H
+elim (cnv_inv_bind … H) -H #_ #H1T0
+[ elim (cpms_inv_appl_sn_decompose … H) -H #U #HTU #HUX1 
+  
+
+  [ #V0 #U0 #HV0 #HU0 #H destruct
+    elim (cnv_cpms_conf … HT … HT0 … HU0)
+    <minus_O_n <minus_n_O #X #H #HU0X
+    elim (cpms_inv_abst_sn … H) -H #W1 #U1 #HW01 #HU01 #H destruct
+    @or_introl
+    @(ex5_4_intro … U1 … HT0 … HX2) -HX2
+    [ /2 width=1 by cnv_cpms_nta/
+    | @nta_bind_cnv /2 width=4 by cnv_cpms_trans/ /2 width=3 by cnv_cpms_nta/
+    | @(cpcs_cprs_div … HX21) -HX21
+      @(cprs_div … (ⓐV0.ⓛ{p}W1.U1))
+      /3 width=1 by cpms_appl, cpms_appl_dx, cpms_bind/ 
+    ]
+  
 (* Basic_2A1: uses: nta_inv_cast1 *)
 lemma nta_inv_cast_sn (a) (h) (G) (L) (X2):
       ∀U,T. ⦃G,L⦄ ⊢ ⓝU.T :[a,h] X2 →
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpr_cpm.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr_cpm.etc
new file mode 100644
index 000000000..dcb1c9302
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpr_cpm.etc
@@ -0,0 +1,57 @@
+include "basic_2/rt_transition/cpm_drops.ma".
+include "basic_2/rt_transition/cpr.ma".
+(*
+theorem cpm_cpm_trans_swap (h) (G) (L) (T1):
+        ∀n1,T. ⦃G,L⦄ ⊢ T1 ➡[n1,h] T → ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 → n1 ≤ n2 →
+        ∃∃T0. ⦃G,L⦄ ⊢ T1 ➡[n2,h] T0 & ⦃G,L⦄ ⊢ T0 ➡[n1,h] T2.
+#h #G #L #T1 #n1 #T #H
+@(cpm_ind … H) -n1 -G -L -T1 -T
+[ #I #G #L #n2 #T2 #HT2 #_ /2 width=3 by ex2_intro/
+| #G #L #s #n2 #X2 #H #_
+  elim (cpm_inv_sort1 … H) -H #H #Hn2 destruct >iter_n_Sm
+  /3 width=3 by cpm_sort, ex2_intro/
+| #n1 #G #K #V1 #V #W #_ #IH #HVW #n2 #T2 #HT2 #Hn
+  elim (cpm_inv_lifts_sn … HT2 (Ⓣ) … HVW) -W
+  [|*: /3 width=2 by drops_refl, drops_drop/ ] #V2 #HVT2 #HV2
+  elim (IH … HV2) -V [| // ] #V0 #HV10 #HV02
+  elim (lifts_total V0 (𝐔❴1❵)) #T0 #HVT0
+  lapply (cpm_lifts_bi … HV02 (Ⓣ) … (K.ⓓV1) … HVT0 … HVT2) -V2
+  [ /3 width=2 by drops_refl, drops_drop/ ] #HT02
+  /3 width=3 by cpm_delta, ex2_intro/
+| #n1 #G #K #V1 #V #W #_ #IH #HVW #m2 #T2 #HT2 #H
+  elim (le_inv_S1 … H) -H #n2 #Hn #H destruct
+  elim (cpm_inv_lifts_sn … HT2 (Ⓣ) … HVW) -W
+  [|*: /3 width=2 by drops_refl, drops_drop/ ] #V2 #HVT2 #HV2
+  elim (IH … HV2) -V [| /2 width=1 by le_S/ ] #V0 #HV10 #HV02
+  elim (lifts_total V0 (𝐔❴1❵)) #T0 #HVT0
+  lapply (cpm_lifts_bi … HV02 (Ⓣ) … (K.ⓛV1) … HVT0 … HVT2) -V2
+  [ /3 width=2 by drops_refl, drops_drop/ ] #HT02
+  /3 width=5 by cpm_ell, ex2_intro/
+*)
+
+(* Note: cpm_cpm_trans_swap does not hold: take L = K.ⓛV1, T1 = #0, n2 = 0 *)
+theorem cpr_cpm_trans_swap (h) (G) (L):
+        ∀T1,T. ⦃G,L⦄ ⊢ T1 ➡[h] T → ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 →
+        ∃∃T0. ⦃G,L⦄ ⊢ T1 ➡[n2,h] T0 & ⦃G,L⦄ ⊢ T0 ➡[h] T2.
+#h #G #L #T1 #T #H
+@(cpr_ind … H) -G -L -T1 -T
+[ #I #G #L #n2 #T2 #HT2 /2 width=3 by ex2_intro/
+| #G #K #V1 #V #W #_ #IH #HVW #n2 #T2 #HT2
+  elim (cpm_inv_lifts_sn … HT2 (Ⓣ) … HVW) -W
+  [|*: /3 width=2 by drops_refl, drops_drop/ ] #V2 #HVT2 #HV2
+  elim (IH … HV2) -V #V0 #HV10 #HV02
+  elim (lifts_total V0 (𝐔❴1❵)) #T0 #HVT0
+  lapply (cpm_lifts_bi … HV02 (Ⓣ) … (K.ⓓV1) … HVT0 … HVT2) -V2
+  [ /3 width=2 by drops_refl, drops_drop/ ] #HT02
+  /3 width=3 by cpm_delta, ex2_intro/
+| #I #G #K #T #U #i #_ #IH #HTU #n2 #U2 #HU2
+  elim (cpm_inv_lifts_sn … HU2 (Ⓣ) … HTU) -U
+  [|*: /3 width=2 by drops_refl, drops_drop/ ] #T2 #HTU2 #HT2
+  elim (IH … HT2) -T #T0 #HT0 #HT02
+  elim (lifts_total T0 (𝐔❴1❵)) #U0 #HTU0
+  lapply (cpm_lifts_bi … HT02 (Ⓣ) … (K.ⓘ{I}) … HTU0 … HTU2) -T2
+  [ /3 width=2 by drops_refl, drops_drop/ ] #HU02
+  /3 width=3 by cpm_lref, ex2_intro/
+| #p #I #G #L #V1 #V #T1 #T #_ #_ #IHV #IHT #n2 #X2 #H
+  elim (cpm_inv_bind1 … H) -H *
+  [ #V2 #T2 #HV2 #HT2 #H destruct 
\ No newline at end of file
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpms.ma
index a9f2d248c..23d0295ca 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpms.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpms.ma
@@ -168,3 +168,27 @@ theorem cpms_cast (n) (h) (G) (L):
   /3 width=3 by cpms_trans, cpms_cast_sn/
 ]
 qed.
+
+theorem cpms_trans_swap (h) (G) (L) (T1):
+        ∀n1,T. ⦃G,L⦄ ⊢ T1 ➡*[n1,h] T → ∀n2,T2. ⦃G,L⦄ ⊢ T ➡*[n2,h] T2 →
+        ∃∃T0. ⦃G,L⦄ ⊢ T1 ➡*[n2,h] T0 & ⦃G,L⦄ ⊢ T0 ➡*[n1,h] T2.
+#h #G #L #T1 #n1 #T #HT1 #n2 #T2 #HT2
+lapply (cpms_trans … HT1 … HT2) -T <commutative_plus #HT12
+/2 width=1 by cpms_inv_plus/
+qed-.
+
+(* More advanced inversion lemmas *******************************************)
+(*
+lemma cpms_inv_appl_sn_decompose (h) (n) (G) (L) (V1) (T1):
+      ∀X2. ⦃G,L⦄ ⊢ ⓐV1.T1 ➡*[n,h] X2 →
+      ∃∃T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 & ⦃G,L⦄ ⊢ ⓐV1.T2 ➡*[h] X2.
+#h #n #G #L #V1 #T1 #X2 #H
+@(cpms_ind_dx … H) -n -X2
+[ /2 width=3 by ex2_intro/
+| #n1 #n2 #X #X2 #_ * #X1 #HTX1 #HX1 #HX2
+  elim (pippo … HX1 … HX2) -X #X #HX1 #HX2
+  elim (cpm_inv_appl_sn_decompose … HX1) -HX1 #U1 #HXU1 #HU1X
+  /3 width=5 by cprs_step_sn, cpms_step_dx, ex2_intro/
+]
+qed-.
+*)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpr.ma
new file mode 100644
index 000000000..92a99ed77
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpr.ma
@@ -0,0 +1,42 @@
+
+include "basic_2/rt_computation/cpms_lpr.ma".
+
+theorem cpr_cpm_trans_swap_lpr (h) (G) (L1) (T1):
+        ∀T. ⦃G,L1⦄ ⊢ T1 ➡[h] T → ∀L2. ⦃G,L1⦄ ⊢ ➡[h] L2 → ∀n2,T2. ⦃G,L2⦄ ⊢ T ➡[n2,h] T2 →
+        ∃∃T0. ⦃G,L1⦄ ⊢ T1 ➡[n2,h] T0 & ⦃G,L1⦄ ⊢ T0 ➡*[h] T2.
+#h #G #L1 #T1 #T #H
+@(cpr_ind … H) -G -L1 -T1 -T
+[ (* #I #G #L1 #L2 #HL12 #n2 #T2 #HT2 /2 width=3 by ex2_intro/ *)
+| (*
+  #G #K #V1 #V #W #_ #IH #HVW #n2 #T2 #HT2
+  elim (cpm_inv_lifts_sn … HT2 (Ⓣ) … HVW) -W
+  [|*: /3 width=2 by drops_refl, drops_drop/ ] #V2 #HVT2 #HV2
+  elim (IH … HV2) -V #V0 #HV10 #HV02
+  elim (lifts_total V0 (𝐔❴1❵)) #T0 #HVT0
+  lapply (cpm_lifts_bi … HV02 (Ⓣ) … (K.ⓓV1) … HVT0 … HVT2) -V2
+  [ /3 width=2 by drops_refl, drops_drop/ ] #HT02
+  /3 width=3 by cpm_delta, ex2_intro/
+*)
+| (*
+  #I #G #K #T #U #i #_ #IH #HTU #n2 #U2 #HU2
+  elim (cpm_inv_lifts_sn … HU2 (Ⓣ) … HTU) -U
+  [|*: /3 width=2 by drops_refl, drops_drop/ ] #T2 #HTU2 #HT2
+  elim (IH … HT2) -T #T0 #HT0 #HT02
+  elim (lifts_total T0 (𝐔❴1❵)) #U0 #HTU0
+  lapply (cpm_lifts_bi … HT02 (Ⓣ) … (K.ⓘ{I}) … HTU0 … HTU2) -T2
+  [ /3 width=2 by drops_refl, drops_drop/ ] #HU02
+  /3 width=3 by cpm_lref, ex2_intro/
+*)
+| #p #I #G #L1 #V1 #V #T1 #T #HV1 #_ #_ #IHT #L2 #HL12 #n2 #X2 #H
+  elim (cpm_inv_bind1 … H) -H *
+  [ #V2 #T2 #HV2 #HT2 #H destruct
+    elim (IHT … HT2) -T [| /2 width=1 by lpr_pair/ ] #T0 #HT10 #HT02
+    lapply (lpr_cpm_trans … HV2 … HL12) -L2 #HV2
+    /4 width=7 by cpms_bind, cpms_step_sn, cpm_bind, ex2_intro/
+  | #X #HXT #HX2 #H1 #H2 destruct
+    elim (cpm_lifts_sn … HX2 (Ⓣ) … (L2.ⓓV) … HXT) -HX2
+    [| /3 width=2 by drops_refl, drops_drop/ ] #T2 #HXT2 #HT2
+    elim (IHT … HT2) -HT2 -IHT [| /2 width=1 by lpr_pair/ ] #T0 #HT10 #HT02
+    /3 width=6 by cpms_zeta_dx, cpm_bind, ex2_intro/
+  ]
+|
\ No newline at end of file
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma
index 341ecee8c..97cfd31a4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma
@@ -290,6 +290,22 @@ lemma cpm_inv_cast1: ∀n,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝV1.U1 ➡[n, h] U2 
 ]
 qed-.
 
+(* Advanced inversion lemmas ************************************************)
+
+lemma cpm_inv_appl_sn_decompose (h) (n) (G) (L) (V1) (T1):
+      ∀X2. ⦃G,L⦄ ⊢ ⓐV1.T1 ➡[n,h] X2 →
+      ∃∃T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 & ⦃G,L⦄ ⊢ ⓐV1.T2 ➡[h] X2.
+#h #n #G #L #V1 #T1 #X2 #H
+elim (cpm_inv_appl1 … H) -H *
+[ #V2 #T2 #HV12 #HT12 #H destruct
+  /3 width=3 by cpm_appl, ex2_intro/
+| #p #V2 #W1 #W2 #U1 #U2 #HV12 #HW12 #HU12 #H1 #H2 destruct
+  /3 width=5 by cpm_beta, cpm_bind, ex2_intro/
+| #p #V2 #V0 #W1 #W2 #U1 #U2 #HV12 #HV20 #HW12 #HU12 #H1 #H2 destruct
+  /3 width=5 by cpm_theta, cpm_bind, ex2_intro/
+]
+qed-.
+
 (* Basic forward lemmas *****************************************************)
 
 (* Basic_2A1: includes: cpr_fwd_bind1_minus *)
-- 
2.39.2