milestone uupdate in basic_2

extended and restricted type rules justified

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma
index e5b5d6f7a8696ddaadcb56aeca60ec408f2a4f08..7f71bea7cb0c88557eed5090e04b90d427b9af81 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
 (*                                                                        *)
 (**************************************************************************)
 

-include "basic_2/rt_transition/cpm_aaa.ma".

 include "basic_2/rt_computation/cpms_aaa.ma".
 include "basic_2/dynamic/cnv.ma".
 
 include "basic_2/rt_computation/cpms_aaa.ma".
 include "basic_2/dynamic/cnv.ma".
 


@@ -50,3 +49,12 @@ lemma cnv_fwd_cpm_SO (a) (h) (G) (L):
 elim (cnv_fwd_aaa … H) -H #A #HA
 /2 width=2 by aaa_cpm_SO/
 qed-.
 elim (cnv_fwd_aaa … H) -H #A #HA
 /2 width=2 by aaa_cpm_SO/
 qed-.

+
+(* Forward lemmas with t_bound rt_computation for terms *********************)
+
+lemma cnv_fwd_cpms_total (a) (h) (n) (G) (L):
+      ∀T. ⦃G, L⦄ ⊢ T ![a, h] → ∃U. ⦃G,L⦄ ⊢ T ➡*[n,h] U.
+#a #h #n #G #L #T #H
+elim (cnv_fwd_aaa … H) -H #A #HA
+/2 width=2 by aaa_cpms_total/
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpcs.ma
new file mode 100644 (file)
index 0000000..ba4b824
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpcs.ma
@@ -0,0 +1,38 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/rt_equivalence/cpcs_cprs.ma".
+include "basic_2/dynamic/cnv_preserve.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+(* Forward lemmas with r-equivalence ****************************************)
+
+lemma cnv_cpms_conf_eq (a) (h) (n) (G) (L):
+      ∀T. ⦃G,L⦄ ⊢ T ![a,h] →
+      ∀T1. ⦃G,L⦄ ⊢ T ➡*[n,h] T1 → ∀T2. ⦃G,L⦄ ⊢ T ➡*[n,h] T2 → ⦃G,L⦄ ⊢ T1 ⬌*[h] T2.
+#a #h #n #G #L #T #HT #T1 #HT1 #T2 #HT2
+elim (cnv_cpms_conf … HT … HT1 … HT2) -T <minus_n_n #T #HT1 #HT2
+/2 width=3 by cprs_div/
+qed-.
+
+lemma cnv_cpms_fwd_appl_sn_decompose (a) (h) (G) (L):
+      ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![a,h] → ∀n,X. ⦃G,L⦄ ⊢ ⓐV.T ➡*[n,h] X →
+      ∃∃U. ⦃G,L⦄ ⊢ T ![a,h] & ⦃G,L⦄ ⊢ T ➡*[n,h] U & ⦃G,L⦄ ⊢ ⓐV.U ⬌*[h] X.
+#a #h #G #L #V #T #H0 #n #X #HX
+elim (cnv_inv_appl … H0) #m #p #W #U #_ #_ #HT #_ #_ -m -p -W -U
+elim (cnv_fwd_cpms_total … h n … HT) #U #HTU
+lapply (cpms_appl_dx … V V … HTU) [ // ] #H
+/3 width=8 by cnv_cpms_conf_eq, ex3_intro/
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cpms_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cpms_cpr.ma
deleted file mode 100644 (file)
index cdcb23a..0000000
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cpms_cpr.ma
+++ /dev/null
@@ -1,160 +0,0 @@
-
-include "basic_2/rt_computation/cpms_lpr.ma".
-(*
-lemma cpm_lsubr_trans (h) (n) (G) (L1) (T1):
-      ∀T2. ⦃G,L1⦄ ⊢ T1 ➡[↑n,h] T2 → ∀L2. L1 ⫃ L2 →
-      ∃∃T0. ⦃G,L2⦄ ⊢ T1 ➡[↑n,h] T0 & ⦃G,L2⦄ ⊢ T0 ➡*[h] T2.
-#h #m #G #L1 #T1 #T2
-@(insert_eq_0 … (↑m)) #n #H
-@(cpm_ind … H) -n -G -L1 -T1 -T2
-[ 
-|
-| #n #G #K1 #V1 #V2 #W2 #_ #IH #HVW2 #Hm #L2 #H destruct
-  elim (lsubr_inv_bind1 … H) -H *
-  [ #K2 #HK #H destruct
-    elim (IH … HK) -K1 [| // ] #V0 #HV10 #HV02
-    elim (lifts_total V0 (𝐔❴1❵)) #W0 #HVW0
-    lapply (cpms_lifts_bi … HV02 (Ⓣ) … (K2.ⓓV1) … HVW0 … HVW2) -V2
-    [ /3 width=2 by drops_refl, drops_drop/ ] #HW02
-    /3 width=3 by cpm_delta, ex2_intro/
-  | #K2 #VX #WX #HK #H1 #H2 destruct
-    elim (IH … HK) -K1 [| // ] #X0 #H1 #H2
-    elim (cpm_inv_cast1 … H1) -H1 [ * || * ]
-    [ #W0 #V0 #HW0 #HV0 #H destruct
-        @(ex2_intro … (#0)) [ // | 
-  | #I1 #I2 #K2 #VX #HK #H1 #H2 destruct   
-    
-|
-|
-| #n #p #I #G #L1 #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #L2 #HL
-  elim (IHV … HL) -IHV #V0 #HV01 #HV02
-  elim (IHT (L2.ⓑ{I}V1)) [| /2 width=1 by lsubr_bind/ ] -L1 #T0 #HT10 #HT02
-  @(ex2_intro … (ⓑ{p,I}V1.T0)) /3 width=3 by cprs_step_sn, cpms_bind, cpm_bind/ (**) (* full auto a bit slow *)
-| 
-|
-|  //   
-*)
-(*
-lemma cpr_cpm_trans_swap_lsubr_lpr (h) (G) (L1) (T1):
-      ∀T. ⦃G,L1⦄ ⊢ T1 ➡[h] T → ∀L. L ⫃ L1 →
-      ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → ∀n2,T2. ⦃G,L2⦄ ⊢ T ➡[n2,h] T2 →
-      ∃∃T0. ⦃G,L⦄ ⊢ T1 ➡[n2,h] T0 & ⦃G,L⦄ ⊢ T0 ➡*[h] T2.
-#h #G #L1 #T1 @(fqup_wf_ind_eq (Ⓣ) … G L1 T1) -G -L1 -T1
-#G0 #L0 #T0 #IH #G #L1 * [| * [| * ]]
-[ (*
-  #I #HG #HL #HT #X #H1 #L2 #HL12 #m2 #X2 #H2 destruct
-  elim (cpr_inv_atom1 … H1) -H1 [|*: * ]
-  [ #H destruct
-    elim (cpm_inv_atom1 … H2) -H2 *
-    [ #H1 #H2 destruct /3 width=3 by cpm_cpms, ex2_intro/
-    | #s #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/
-    | #K2 #V #V2 #HV2 #HVT2 #H1 #H2 destruct
-      elim (lpr_inv_pair_dx … HL12) -HL12 #K1 #V1 #HK12 #HV1 #H destruct
-      elim (IH … HV1 … HK12 … HV2) -K2 -V -IH
-      [| /2 width=1 by fqu_fqup, fqu_lref_O/ ] #V0 #HV10 #HV02
-      elim (lifts_total V0 (𝐔❴1❵)) #T0 #HVT0
-      lapply (cpms_lifts_bi … HV02 (Ⓣ) … (K1.ⓓV1) … HVT0 … HVT2) -V2
-      [ /3 width=2 by drops_refl, drops_drop/ ] #HT02
-      /3 width=3 by cpm_delta, ex2_intro/
-    | #n2 #K2 #W #W2 #HW2 #HWT2 #H1 #H2 #H3 destruct
-      elim (lpr_inv_pair_dx … HL12) -HL12 #K1 #W1 #HK12 #HW1 #H destruct
-      elim (IH … HW1 … HK12 … HW2) -K2 -W -IH
-      [| /2 width=1 by fqu_fqup, fqu_lref_O/ ] #W0 #HW10 #HW02
-      elim (lifts_total W0 (𝐔❴1❵)) #T0 #HWT0
-      lapply (cpms_lifts_bi … HW02 (Ⓣ) … (K1.ⓛW1) … HWT0 … HWT2) -W2
-      [ /3 width=2 by drops_refl, drops_drop/ ] #HT02
-      /3 width=3 by cpm_ell, ex2_intro/
-    | #I2 #K2 #T2 #i #HT2 #HTU2 #H1 #H2 destruct
-      elim (lpr_inv_bind_dx … HL12) -HL12 #I1 #K1 #HK12 #_ #H destruct
-      elim (IH … (#i) … HK12 … HT2) -I2 -K2 -IH
-      [|*: /2 width=1 by fqu_fqup/ ] #T0 #HT10 #HT02
-      elim (lifts_total T0 (𝐔❴1❵)) #U0 #HTU0
-      lapply (cpms_lifts_bi … HT02 (Ⓣ) … (K1.ⓘ{I1}) … HTU0 … HTU2) -T2
-      [ /3 width=2 by drops_refl, drops_drop/ ] #HU02
-      /3 width=3 by cpm_lref, ex2_intro/
-    ]
-  | #K1 #V1 #V #HV1 #HVT #H1 #H2 destruct
-    elim (lpr_inv_pair_sn … HL12) -HL12 #K2 #V0 #HK12 #_ #H destruct
-    elim (cpm_inv_lifts_sn … H2 (Ⓣ) … HVT) -X
-    [|*: /3 width=2 by drops_refl, drops_drop/ ] -V0 #V2 #HVT2 #HV2
-    elim (IH … HV1 … HK12 … HV2) -K2 -V -IH
-    [| /2 width=1 by fqu_fqup, fqu_lref_O/ ] #V0 #HV10 #HV02
-    elim (lifts_total V0 (𝐔❴1❵)) #T0 #HVT0
-    lapply (cpms_lifts_bi … HV02 (Ⓣ) … (K1.ⓓV1) … HVT0 … HVT2) -V2
-    [ /3 width=2 by drops_refl, drops_drop/ ] #HT02
-    /3 width=3 by cpm_delta, ex2_intro/
-  | #I1 #K1 #T #i #HT1 #HTU #H1 #H2 destruct
-    elim (lpr_inv_bind_sn … HL12) -HL12 #I2 #K2 #HK12 #_ #H destruct
-    elim (cpm_inv_lifts_sn … H2 (Ⓣ) … HTU) -X
-    [|*: /3 width=2 by drops_refl, drops_drop/ ] -I2 #T2 #HTU2 #HT2
-    elim (IH … HT1 … HK12 … HT2) -K2 -T -IH
-    [| /2 width=1 by fqu_fqup/ ] #T0 #HT10 #HT02
-    elim (lifts_total T0 (𝐔❴1❵)) #U0 #HTU0
-    lapply (cpms_lifts_bi … HT02 (Ⓣ) … (K1.ⓘ{I1}) … HTU0 … HTU2) -T2
-    [ /3 width=2 by drops_refl, drops_drop/ ] #HU02
-    /3 width=3 by cpm_lref, ex2_intro/
-  ]
-*)
-| (*
-  #p #I #V1 #T1 #HG #HL #HT #X #H1 #L2 #HL12 #n2 #X2 #H2
-  elim (cpm_inv_bind1 … H1) -H1 *
-  [ #V #T #HV1 #HT1 #H destruct
-    elim (cpm_inv_bind1 … H2) -H2 *
-    [ #V2 #T2 #HV2 #HT2 #H destruct
-      elim (IH … HT1 … HT2) -T
-      [|*: /2 width=1 by lpr_pair/ ] #T0 #HT10 #HT02
-      elim (IH … HV1 … HL12 … HV2) -L2 -V -IH
-      [| // ] #V0 #HV10 #HV02
-      /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 (IH … HT1 … HT2) -HT2 -IH
-      [|*: /2 width=1 by lpr_pair/ ] -L2 #T0 #HT10 #HT02
-      /3 width=6 by cpms_zeta_dx, cpm_bind, ex2_intro/
-    ]
-  | #X1 #HXT1 #HX1 #H1 #H2 destruct
-    elim (IH … HX1 … HL12 … H2) -L2 -X -IH
-    [| /2 width=1 by fqup_zeta/ ] #X0 #HX10 #HX02
-    /3 width=3 by cpm_zeta, ex2_intro/
-  ]
-*)
-| #V1 #T1 #HG #HL #HT #X #H1 #L #HL1 #L2 #HL2 #m2 #X2 #H2 destruct
-  elim (cpm_inv_appl1 … H1) -H1 *
-  [ (*
-    #V #T #HV1 #HT1 #H destruct
-    elim (cpm_inv_appl1 … H2) -H2 *
-    [ #V2 #T2 #HV2 #HT2 #H destruct
-      elim (IH … HV1 … HL12 … HV2) -V [| // ] #V0 #HV10 #HV02
-      elim (IH … HT1 … HL12 … HT2) -L2 -T -IH [| // ] #T0 #HT10 #HT02
-      /3 width=5 by cpms_appl, cpm_appl, ex2_intro/
-    | #q #V2 #WX #W2 #TX #T2 #HV2 #HW2 #HT2 #H1 #H2 destruct
-      elim (IH … HV1 … HL12 … HV2) -V [| // ] #V0 #HV10 #HV02
-      elim (IH … HT1 … HL12 m2 (ⓛ{q}W2.T2)) -IH -HT1
-      [|*: /2 width=1 by cpm_bind/ ] -L2 -WX -TX #T0 #HT10 #HT02
-      /4 width=9 by cprs_step_dx, cpms_appl, cpm_beta, cpm_appl, ex2_intro/
-    | #q #V2 #U2 #WX #W2 #TX #T2 #HV2 #HVU2 #HW2 #HT2 #H1 #H2 destruct
-      elim (IH … HV1 … HL12 … HV2) -V [| // ] #V0 #HV10 #HV02
-      elim (IH … HT1 … HL12 m2 (ⓓ{q}W2.T2)) -IH -HT1
-      [|*: /2 width=1 by cpm_bind/ ] -L2 -WX -TX #T0 #HT10 #HT02
-      /4 width=11 by cprs_step_dx, cpms_appl, cpm_theta, cpm_appl, ex2_intro/
-    ]
-    *)
-  | #p #V #W1 #W #TX1 #T #HV1 #HW1 #HT1 #H1 #H3 destruct
-    elim (cpm_inv_abbr1 … H2) -H2 *
-    [ #X3 #T2 #H2 #HT2 #H destruct
-      elim (cpr_inv_cast1 … H2) -H2 [ * ]
-      [ #W2 #V2 #HW2 #HV2 #H destruct
-        elim (IH … HT1 (L.ⓓⓝW1.V1) … HT2) -T
-        [|*: /4 width=3 by lsubr_beta, lpr_pair, cpm_cast, lsubr_cpm_trans/ ] #T0 #HT10 #HT02
-        elim (IH … HV1 … HL1 … HL2 … HV2) -V [| // ] #V0 #HV10 #HV02
-        elim (IH … HW1 … HL1 … HL2 … HW2) -L2 -W -IH [| // ] #W0 #HW10 #HW02
-        @(ex2_intro … (ⓓ{p}ⓝW1.V1.T0))
-        [ @cpm_beta //
-          
-           /2 width=1 by cpm_beta/
-      | /3 width=7 by cprs_step_dx, cpms_appl, cpm_beta/
-      
-       @cprs_step_dx [| @(cpms_appl … HT02 … HV02) | /2 width=1 by cpm_beta/
-      @cpms_beta
-*)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/notes.txt b/matita/matita/contribs/lambdadelta/basic_2/dynamic/notes.txt
deleted file mode 100644 (file)
index 8334213..0000000
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/notes.txt
+++ /dev/null
@@ -1,15 +0,0 @@
-                D I 
-sort            * *
-lref ldef       * *
-lref ldec       * *
-lref lref       * *
-lref ldef drops * *
-lref ldec drops * *
-gref              *
-bind            * *
-appl appl       * *
-appl beta       *
-appl pure       *
-cast new        * *
-cast old        * *
-conv            *

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpms.ma
index 71cc3f94e2cabd2a39632a44d190bfb39d765a9f..1cdaf8c46b3b86e3702c267ccbbd4d5453ed4dec 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpms.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpms.ma
@@ -21,21 +21,21 @@ include "basic_2/dynamic/nta.ma".
 (* Properties with rt_computation for terms *********************************)
 
 (* Basic_2A1: was by definition nta_appl ntaa_appl *)
 (* Properties with rt_computation for terms *********************************)
 
 (* Basic_2A1: was by definition nta_appl ntaa_appl *)

-lemma nta_beta (a) (h) (p) (G) (L):
-      ∀V,W. ⦃G,L⦄ ⊢ V :[a,h] W →
-      ∀T,U. ⦃G,L⦄ ⊢ ⓛ{p}W.T :[a,h] ⓛ{p}W.U → ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.T :[a,h] ⓐV.ⓛ{p}W.U.
-#a #h #p #G #L #V #W #H1 #T #U #H2
+lemma nta_beta (a) (h) (p) (G) (K):
+      ∀V,W. ⦃G,K⦄ ⊢ V :[a,h] W →
+      ∀T,U. ⦃G,K.ⓛW⦄ ⊢ T :[a,h] U → ⦃G,K⦄ ⊢ ⓐV.ⓛ{p}W.T :[a,h] ⓐV.ⓛ{p}W.U.
+#a #h #p #G #K #V #W #H1 #T #U #H2

 elim (cnv_inv_cast … H1) -H1 #X1 #HW #HV #HWX1 #HVX1
 elim (cnv_inv_cast … H2) -H2 #X2 #HU #HT #HUX2 #HTX2
 elim (cnv_inv_cast … H1) -H1 #X1 #HW #HV #HWX1 #HVX1
 elim (cnv_inv_cast … H2) -H2 #X2 #HU #HT #HUX2 #HTX2

-/4 width=7 by cnv_cast, cnv_appl, cpms_bind, cpms_appl_dx/
+/4 width=7 by cnv_bind, cnv_appl, cnv_cast, cpms_appl_dx, cpms_bind_dx/

 qed.
 
 (* Basic_1: was by definition: ty3_appl *)
 (* Basic_2A1: was nta_appl_old *)
 qed.
 
 (* Basic_1: was by definition: ty3_appl *)
 (* Basic_2A1: was nta_appl_old *)

-lemma nta_appl (h) (p) (G) (L):
-      ∀V,W. ⦃G,L⦄ ⊢ V :[h] W →
-      ∀T,U. ⦃G,L⦄ ⊢ T :[h] ⓛ{p}W.U → ⦃G,L⦄ ⊢ ⓐV.T :[h] ⓐV.ⓛ{p}W.U.
-#h #p #G #L #V #W #H1 #T #U #H2
+lemma nta_appl (a) (h) (p) (G) (L):
+      ∀V,W. ⦃G,L⦄ ⊢ V :[a,h] W →
+      ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] ⓛ{p}W.U → ⦃G,L⦄ ⊢ ⓐV.T :[a,h] ⓐV.ⓛ{p}W.U.
+#a #h #p #G #L #V #W #H1 #T #U #H2

 elim (cnv_inv_cast … H1) -H1 #X1 #HW #HV #HWX1 #HVX1
 elim (cnv_inv_cast … H2) -H2 #X2 #HU #HT #HUX2 #HTX2
 elim (cpms_inv_abst_sn … HUX2) #W0 #U0 #HW0 #HU0 #H destruct
 elim (cnv_inv_cast … H1) -H1 #X1 #HW #HV #HWX1 #HVX1
 elim (cnv_inv_cast … H2) -H2 #X2 #HU #HT #HUX2 #HTX2
 elim (cpms_inv_abst_sn … HUX2) #W0 #U0 #HW0 #HU0 #H destruct

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_etc.ma
deleted file mode 100644 (file)
index 320ec67..0000000
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_etc.ma
+++ /dev/null
@@ -1,8 +0,0 @@
-(*
-(* Advanced forvard lemmas **************************************************)
-
-lemma nta_fwd_pure1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓐY.X : U →
-                     ∃∃V,W. ⦃h, L⦄ ⊢ Y : W & ⦃h, L⦄ ⊢ X : V & L ⊢ ⓐY.V ⬌* U.
-/2 width=3/ qed-.
-
-*)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma
index 2e655049e9d864e5c6ebb1662b402c5ac8882671..4de1ae8019b368e26b172f24c38685620de5978d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma
@@ -77,3 +77,107 @@ lemma nta_ind_rest_cnv (h) (Q:relation4 …):
   /4 width=4 by nta_cast/
 ]
 qed-.
   /4 width=4 by nta_cast/
 ]
 qed-.

+
+lemma nta_ind_ext_cnv_mixed (h) (Q:relation4 …):
+      (∀G,L,s. Q G L (⋆s) (⋆(next h s))) →
+      (∀G,K,V,W,U.
+        ⦃G,K⦄ ⊢ V :*[h] W → ⬆*[1] W ≘ U →
+        Q G K V W → Q G (K.ⓓV) (#0) U
+      ) →
+      (∀G,K,W,U. ⦃G,K⦄ ⊢ W !*[h] → ⬆*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
+      (∀I,G,K,W,U,i.
+        ⦃G,K⦄ ⊢ #i :*[h] W → ⬆*[1] W ≘ U →
+        Q G K (#i) W → Q G (K.ⓘ{I}) (#↑i) U
+      ) →
+      (∀p,I,G,K,V,T,U.
+        ⦃G,K⦄ ⊢ V !*[h] → ⦃G,K.ⓑ{I}V⦄ ⊢ T :*[h] U →
+        Q G (K.ⓑ{I}V) T U → Q G K (ⓑ{p,I}V.T) (ⓑ{p,I}V.U)
+      ) →
+      (∀p,G,L,V,W,T,U.
+        ⦃G,L⦄ ⊢ V :*[h] W → ⦃G,L⦄ ⊢ T :*[h] ⓛ{p}W.U →
+        Q G L V W → Q G L T (ⓛ{p}W.U) → Q G L (ⓐV.T) (ⓐV.ⓛ{p}W.U)
+      ) →
+      (∀G,L,V,T,U.
+        ⦃G,L⦄ ⊢ T :*[h] U → ⦃G,L⦄ ⊢ ⓐV.U !*[h] →
+        Q G L T U → Q G L (ⓐV.T) (ⓐV.U)
+      ) →
+      (∀G,L,T,U. ⦃G,L⦄ ⊢ T :*[h] U → Q G L T U → Q G L (ⓝU.T) U
+      ) →
+      (∀G,L,T,U1,U2.
+        ⦃G,L⦄ ⊢ T :*[h] U1 → ⦃G,L⦄ ⊢ U1 ⬌*[h] U2 → ⦃G,L⦄ ⊢ U2 !*[h] →
+        Q G L T U1 → Q G L T U2
+      ) →
+      ∀G,L,T,U. ⦃G,L⦄ ⊢ T :*[h] U → Q G L T U.
+#h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #G #L #T
+@(fqup_wf_ind_eq (Ⓣ) … G L T) -G -L -T #G0 #L0 #T0 #IH #G #L * * [|||| * ]
+[ #s #HG #HL #HT #X #H destruct -IH
+  elim (nta_inv_sort_sn … H) -H #HUX #HX
+  /2 width=4 by/
+| * [| #i ] #HG #HL #HT #X #H destruct
+  [ elim (nta_inv_lref_sn_drops_cnv … H) -H *
+    [ #K #V #W #U #H #HVW #HWU #HUX #HX
+      lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
+      /5 width=7 by nta_ldef, fqu_fqup, fqu_lref_O/
+    | #K #W #U #H #HW #HWU #HUX #HX
+      lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
+      /3 width=4 by nta_ldec_cnv/
+    ]
+  | elim (nta_inv_lref_sn … H) -H #I #K #T #U #HT #HTU #HUX #HX #H destruct
+    /5 width=7 by nta_lref, fqu_fqup/
+  ]
+| #l #HG #HL #HT #U #H destruct -IH
+  elim (nta_inv_gref_sn … H)
+| #p #I #V #T #HG #HL #HT #X #H destruct
+  elim (nta_inv_bind_sn_cnv … H) -H #U #HV #HTU #HUX #HX
+  /4 width=5 by nta_bind_cnv/
+| #V #T #HG #HL #HT #X #H destruct
+  elim (nta_inv_pure_sn_cnv … H) -H *
+  [ #p #W #U #HVW #HTU #HUX #HX
+    /4 width=9 by nta_appl/
+  | #U #HTU #HVU #HUX #HX
+    /4 width=6 by nta_pure_cnv/
+  ]
+| #U #T #HG #HL #HT #X #H destruct
+  elim (nta_inv_cast_sn … H) -H #HTU #HUX #HX
+  /4 width=4 by nta_cast/
+]
+qed-.
+
+lemma nta_ind_ext_cnv (h) (Q:relation4 …):
+      (∀G,L,s. Q G L (⋆s) (⋆(next h s))) →
+      (∀G,K,V,W,U.
+        ⦃G,K⦄ ⊢ V :*[h] W → ⬆*[1] W ≘ U →
+        Q G K V W → Q G (K.ⓓV) (#0) U
+      ) →
+      (∀G,K,W,U. ⦃G,K⦄ ⊢ W !*[h] → ⬆*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
+      (∀I,G,K,W,U,i.
+        ⦃G,K⦄ ⊢ #i :*[h] W → ⬆*[1] W ≘ U →
+        Q G K (#i) W → Q G (K.ⓘ{I}) (#↑i) U
+      ) →
+      (∀p,I,G,K,V,T,U.
+        ⦃G,K⦄ ⊢ V !*[h] → ⦃G,K.ⓑ{I}V⦄ ⊢ T :*[h] U →
+        Q G (K.ⓑ{I}V) T U → Q G K (ⓑ{p,I}V.T) (ⓑ{p,I}V.U)
+      ) →
+      (∀p,G,K,V,W,T,U.
+        ⦃G,K⦄ ⊢ V :*[h] W → ⦃G,K.ⓛW⦄ ⊢ T :*[h] U →
+        Q G K V W → Q G (K.ⓛW) T U → Q G K (ⓐV.ⓛ{p}W.T) (ⓐV.ⓛ{p}W.U)
+      ) →
+      (∀G,L,V,T,U.
+        ⦃G,L⦄ ⊢ T :*[h] U → ⦃G,L⦄ ⊢ ⓐV.U !*[h] →
+        Q G L T U → Q G L (ⓐV.T) (ⓐV.U)
+      ) →
+      (∀G,L,T,U. ⦃G,L⦄ ⊢ T :*[h] U → Q G L T U → Q G L (ⓝU.T) U
+      ) →
+      (∀G,L,T,U1,U2.
+        ⦃G,L⦄ ⊢ T :*[h] U1 → ⦃G,L⦄ ⊢ U1 ⬌*[h] U2 → ⦃G,L⦄ ⊢ U2 !*[h] →
+        Q G L T U1 → Q G L T U2
+      ) →
+      ∀G,L,T,U. ⦃G,L⦄ ⊢ T :*[h] U → Q G L T U.
+#h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #G #L #T #U #H
+@(nta_ind_ext_cnv_mixed … IH1 IH2 IH3 IH4 IH5 … IH7 IH8 IH9 … H) -G -L -T -U -IH1 -IH2 -IH3 -IH4 -IH5 -IH6 -IH8 -IH9
+#p #G #L #V #W #T #U #HVW #HTU #_ #IHTU
+lapply (nta_fwd_cnv_dx … HTU) #H
+elim (cnv_inv_bind … H) -H #_ #HU
+elim (cnv_nta_sn … HU) -HU #X #HUX
+/4 width=2 by nta_beta, nta_fwd_cnv_sn/
+qed-.

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 e6dd70e6541dbd076880d9aa46aac0eda03938bc..b308c118d6ca11150f56b49cb0261bf5ab6145fe 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
 (*                                                                        *)
 (**************************************************************************)
 

-include "basic_2/rt_equivalence/cpcs_cprs.ma".
-include "basic_2/dynamic/cnv_preserve.ma".
+include "basic_2/rt_equivalence/cpcs_cpcs.ma".
+include "basic_2/dynamic/cnv_cpcs.ma".

 include "basic_2/dynamic/nta.ma".
 
 (* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************)
 include "basic_2/dynamic/nta.ma".
 
 (* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************)


@@ -135,60 +135,36 @@ elim (cnv_inv_appl … H1) * [ | #n ] #p #W #U #Hn #HV #HT #HVW #HTU
   lapply (cpms_step_dx … HTU 1 (ⓛ{p}W.U0) ?) -HTU [ /2 width=1 by cpm_bind/ ] #HTU
 | lapply (le_n_O_to_eq n ?) [ /3 width=1 by le_S_S_to_le/ ] -Hn #H destruct
 ]
   lapply (cpms_step_dx … HTU 1 (ⓛ{p}W.U0) ?) -HTU [ /2 width=1 by cpm_bind/ ] #HTU
 | lapply (le_n_O_to_eq n ?) [ /3 width=1 by le_S_S_to_le/ ] -Hn #H destruct
 ]

-lapply (cpms_appl_dx … V V … HTU) [1,3: // ] #HVTU
-elim (cnv_cpms_conf … H1 … H2 … HVTU) -H1 -H2 -HVTU <minus_n_n #X0 #HX0 #HUX0
-@ex4_3_intro [6,13: |*: /2 width=5 by cnv_cpms_nta/ ]
-/3 width=5 by cprs_div, cprs_trans/
+/5 width=11 by cnv_cpms_nta, cnv_cpms_conf_eq, cpcs_cprs_div, cpms_appl_dx, ex4_3_intro/

 qed-.
 qed-.

-(*
- (ltc_ind
- :∀A: Type \sub 0 
-  .(A→A→A)
-   →∀B: Type \sub 0 
-    .relation3 A B B
-     →∀Q_:∀x_3:A.∀x_2:B.∀x_1:B.ltc A __6 B __4 x_3 x_2 x_1→Prop
-      .(∀a:A
-        .∀b1:B
-         .∀b2:B.∀x_5:__5 a b1 b2.Q_ a b1 b2 (ltc_rc A __8 B __6 a b1 b2 x_5))
-       →(∀a1:A
-         .∀a2:A
-          .∀b1:B
-           .∀b:B
-            .∀b2:B
-             .∀x_7:ltc A __10 B __8 a1 b1 b
-              .∀x_6:ltc A __11 B __9 a2 b b2
-               .Q_ a1 b1 b x_7
-                →Q_ a2 b b2 x_6
-                 →Q_ (__14 a1 a2) b1 b2
-                  (ltc_trans A __14 B __12 a1 a2 b1 b b2 x_7 x_6))
-        →∀x_3:A
-         .∀x_2:B.∀x_1:B.∀x_4:ltc A __9 B __7 x_3 x_2 x_1.Q_ x_3 x_2 x_1 x_4)

 
 

+(* Basic_2A1: uses: nta_fwd_pure1 *)

 lemma nta_inv_pure_sn_cnv (h) (G) (L) (X2):
                           ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T :*[h] X2 →
 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]
+                          ∨∨ ∃∃p,W,U. ⦃G,L⦄ ⊢ V :*[h] W & ⦃G,L⦄ ⊢ T :*[h] ⓛ{p}W.U & ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.U ⬌*[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
                            | ∃∃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/ 
-    ]
-*)
+elim (cnv_inv_appl … H1) * [| #n ] #p #W0 #T0 #Hn #HV #HT #HW0 #HT0
+[ lapply (cnv_cpms_trans … HT … HT0) #H0
+  elim (cnv_inv_bind … H0) -H0 #_ #HU
+  elim (cnv_fwd_cpm_SO … HU) #U0 #HU0 -HU
+  lapply (cpms_step_dx … HT0 1 (ⓛ{p}W0.U0) ?) -HT0 [ /2 width=1 by cpm_bind/ ] #HT0
+  lapply (cpms_appl_dx … V V … HT0) [ // ] #HTU0
+  lapply (cnv_cpms_conf_eq … H1 … HTU0 … H) -H1 -H -HTU0 #HU0X1
+  /4 width=8 by cnv_cpms_nta, cpcs_cprs_div, ex4_3_intro, or_introl/
+| elim (cnv_cpms_fwd_appl_sn_decompose …  H1 … H) -H1 -H #X0 #_ #H #HX01
+  elim (cpms_inv_plus … 1 n … HT0) #U #HTU #HUT0
+  lapply (cnv_cpms_trans … HT … HTU) #HU
+  lapply (cnv_cpms_conf_eq … HT … HTU … H) -H #HUX0
+  @or_intror @(ex4_intro … U … HX2) -HX2
+  [ /2 width=1 by cnv_cpms_nta/
+  | /4 width=7 by cnv_appl, lt_to_le/
+  | /4 width=3 by cpcs_trans, cpcs_cprs_div, cpcs_flat/
+  ]
+]
+qed-.
+

 (* 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 →
 (* 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 →


@@ -198,18 +174,14 @@ elim (cnv_inv_cast … H) -H #X0 #HX2 #H1 #HX20 #H2
 elim (cnv_inv_cast … H1) #X #HU #HT #HUX #HTX
 elim (cpms_inv_cast1 … H2) -H2 [ * || * ]
 [ #U0 #T0 #HU0 #HT0 #H destruct -HU -HU0
 elim (cnv_inv_cast … H1) #X #HU #HT #HUX #HTX
 elim (cpms_inv_cast1 … H2) -H2 [ * || * ]
 [ #U0 #T0 #HU0 #HT0 #H destruct -HU -HU0

-  elim (cnv_cpms_conf … HT … HTX … HT0) -HT -HTX -HT0
-  <minus_n_n #T1 #HXT1 #HT01
-  @and3_intro // @(cprs_div … T1) /3 width=4 by cprs_trans, cpms_eps/ (**) (* full auto too slow *)
+  lapply (cnv_cpms_conf_eq … HT … HTX … HT0) -HT -HT0 -HTX #HXT0
+  lapply (cprs_step_dx … HX20 T0 ?) -HX20 [ /2 width=1 by cpm_eps/ ] #HX20

 | #HTX0 -HU
 | #HTX0 -HU

-  elim (cnv_cpms_conf … HT … HTX … HTX0) -HT -HTX -HTX0
-  <minus_n_n #T1 #HXT1 #HXT01
-  @and3_intro // @(cprs_div … T1) /2 width=3 by cprs_trans/ (**) (* full auto too slow *)
+  lapply (cnv_cpms_conf_eq … HT … HTX … HTX0) -HT -HTX -HTX0 #HX0

 | #m #HUX0 #H destruct -HT -HTX
 | #m #HUX0 #H destruct -HT -HTX

-  elim (cnv_cpms_conf … HU … HUX … HUX0) -HU -HUX0
-  <minus_n_n #U1 #HXU1 #HXU01
-  @and3_intro // @(cprs_div … U1) /2 width=3 by cprs_trans/ (**) (* full auto too slow *)
+  lapply (cnv_cpms_conf_eq … HU … HUX … HUX0) -HU -HUX0 #HX0

 ]
 ]

+/4 width=3 by cpcs_cprs_div, cpcs_cprs_step_sn, and3_intro/

 qed-.
 
 (* Basic_1: uses: ty3_gen_cast *)
 qed-.
 
 (* Basic_1: uses: ty3_gen_cast *)


@@ -221,17 +193,13 @@ elim (cnv_inv_cast … H) -H #X0 #HX2 #H1 #HX20 #H2
 elim (cnv_inv_cast … H1) #X #HT1 #HT0 #HT1X #HT0X
 elim (cpms_inv_cast1 … H2) -H2 [ * || * ]
 [ #U1 #U0 #HTU1 #HTU0 #H destruct
 elim (cnv_inv_cast … H1) #X #HT1 #HT0 #HT1X #HT0X
 elim (cpms_inv_cast1 … H2) -H2 [ * || * ]
 [ #U1 #U0 #HTU1 #HTU0 #H destruct

-  elim (cnv_cpms_conf … HT0 … HT0X … HTU0) -HT0 -HT0X -HTU0
-  <minus_n_n #X0 #HX0 #HUX0
-  lapply (cprs_trans … HT1X … HX0) -X #HT1X0
-  /5 width=7 by cnv_cpms_nta, cpcs_cprs_div, cprs_div, cpms_cast, ex4_intro/
+  lapply (cnv_cpms_conf_eq … HT0 … HT0X … HTU0) -HT0 -HT0X -HTU0 #HXU0
+  /5 width=5 by cnv_cpms_nta, cpcs_cprs_div, cpcs_cprs_step_sn, cpcs_flat, ex4_intro/

 | #HTX0
 | #HTX0

-  elim (cnv_cpms_conf … HT0 … HT0X … HTX0) -HT0 -HT0X -HTX0
-  <minus_n_n #X1 #HX1 #HX01

   elim (cnv_nta_sn … HT1) -HT1 #U1 #HTU1
   elim (cnv_nta_sn … HT1) -HT1 #U1 #HTU1

-  lapply (cprs_trans … HT1X … HX1) -X #HTX1
-  lapply (cprs_trans … HX20 … HX01) -X0 #HX21
-  /4 width=5 by cprs_div, cpms_eps, ex4_intro/
+  lapply (cnv_cpms_conf_eq … HT0 … HT0X … HTX0) -HT0 -HT0X -HTX0 #HX0
+  lapply (cprs_step_sn … (ⓝU1.T1) … HT1X) -HT1X [ /2 width=1 by cpm_eps/ ] #HT1X
+  /4 width=5 by cpcs_cprs_div, cpcs_cprs_step_sn, ex4_intro/

 | #n #HT1X0 #H destruct -X -HT0
   elim (cnv_nta_sn … HT1) -HT1 #U1 #HTU1
   /4 width=5 by cprs_div, cpms_eps, ex4_intro/
 | #n #HT1X0 #H destruct -X -HT0
   elim (cnv_nta_sn … HT1) -HT1 #U1 #HTU1
   /4 width=5 by cprs_div, cpms_eps, ex4_intro/


@@ -246,6 +214,6 @@ theorem nta_mono (a) (h) (G) (L) (T):
 #a #h #G #L #T #U1 #H1 #U2 #H2
 elim (cnv_inv_cast … H1) -H1 #X1 #_ #_ #HUX1 #HTX1
 elim (cnv_inv_cast … H2) -H2 #X2 #_ #HT #HUX2 #HTX2
 #a #h #G #L #T #U1 #H1 #U2 #H2
 elim (cnv_inv_cast … H1) -H1 #X1 #_ #_ #HUX1 #HTX1
 elim (cnv_inv_cast … H2) -H2 #X2 #_ #HT #HUX2 #HTX2

-elim (cnv_cpms_conf … HT … HTX1 … HTX2) -T <minus_n_n #X #HX1 #HX2
-/3 width=5 by cprs_div, cprs_trans/
+lapply (cnv_cpms_conf_eq … HT … HTX1 … HTX2) -T #HX12
+/3 width=3 by cpcs_cprs_div, cpcs_cprs_step_sn/

 qed-.
 qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/nta_extra.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/nta_extra.etc
new file mode 100644 (file)
index 0000000..ae24853
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/nta_extra.etc
@@ -0,0 +1,31 @@
+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.ⓛW⦄ ⊢ T0 :*[h] 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) * [| #n ] #p #W0 #T0 #Hn #HV #HT #HW0 #HT0
+[ lapply (cpms_appl_dx … V V … HT0) // #H0
+  lapply (cnv_cpms_trans … H1 … H0) #H2
+  elim (cnv_cpms_conf … H1 … H … H0) -H1 -H -H0
+  <minus_O_n <minus_n_O #X #HX #HT0X
+  lapply (cprs_trans … HX21 … HX) -X1 #H1X2
+  elim (cnv_cpms_fwd_appl_sn_decompose …  H2 … HT0X) -H2 -HT0X #X0 #H #HTX0 #HX0
+  elim (cnv_inv_bind … H) -H #_ #H1T0
+  elim (cpms_inv_abst_sn_cprs … HTX0) -HTX0 #U0 #HTU0 #HUX0
+  @or_introl @(ex5_4_intro … U0 … HT0 … HX2)
+  [ /2 width=1 by cnv_cpms_nta/
+  | /3 width=1 by cnv_cpms_nta/
+  | /4 width=3 by cpcs_cprs_div, cpcs_cprs_step_sn, cpms_appl_dx/
+  ]
+| elim (cnv_cpms_fwd_appl_sn_decompose …  H1 … H) -H1 -H #X0 #_ #H #HX01
+  elim (cpms_inv_plus … 1 n … HT0) #U #HTU #HUT0
+  lapply (cnv_cpms_trans … HT … HTU) #HU
+  lapply (cnv_cpms_conf_eq … HT … HTU … H) -H #HUX0
+  @or_intror @(ex4_intro … U … HX2) -HX2
+  [ /2 width=1 by cnv_cpms_nta/
+  | /4 width=7 by cnv_appl, lt_to_le/
+  | /4 width=3 by cpcs_trans, cpcs_cprs_div, cpcs_flat/
+  ]
+]
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_aaa.ma
index f4fdb524fc6aa30ee7571458097c6c8ec30b60b6..08f2039c8bacd5fee9466f3f8eb72c61a83092c2 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_aaa.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
 (*                                                                        *)
 (**************************************************************************)
 

+include "basic_2/rt_transition/cpm_aaa.ma".

 include "basic_2/rt_computation/cpxs_aaa.ma".
 include "basic_2/rt_computation/cpms_cpxs.ma".
 
 include "basic_2/rt_computation/cpxs_aaa.ma".
 include "basic_2/rt_computation/cpms_cpxs.ma".
 


@@ -23,3 +24,15 @@ include "basic_2/rt_computation/cpms_cpxs.ma".
 (* Basic_2A1: includes: cprs_aaa_conf *)
 lemma cpms_aaa_conf (n) (h): ∀G,L. Conf3 … (aaa G L) (cpms h G L n).
 /3 width=5 by cpms_fwd_cpxs, cpxs_aaa_conf/ qed-.
 (* Basic_2A1: includes: cprs_aaa_conf *)
 lemma cpms_aaa_conf (n) (h): ∀G,L. Conf3 … (aaa G L) (cpms h G L n).
 /3 width=5 by cpms_fwd_cpxs, cpxs_aaa_conf/ qed-.

+
+lemma aaa_cpms_total (h) (G) (L) (n) (A):
+      ∀T. ⦃G, L⦄ ⊢ T ⁝ A → ∃U. ⦃G,L⦄ ⊢ T ➡*[n,h] U.
+#h #G #L #n elim n -n
+[ /2 width=3 by ex_intro/
+| #n #IH #A #T1 #HT1 <plus_SO
+  elim (IH … HT1) -IH #T0 #HT10
+  lapply (cpms_aaa_conf … HT1 … HT10) -HT1 #HT0
+  elim (aaa_cpm_SO h … HT0) -HT0 #T2 #HT02
+  /3 width=4 by cpms_step_dx, ex_intro/
+]
+qed-.

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 23d0295ca94e8464aaeb3eb4c2ff029def87f670..fcd97f3b905b5192dc3c7cc908bfebe0ef7bab2a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpms.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpms.ma
@@ -176,19 +176,3 @@ theorem cpms_trans_swap (h) (G) (L) (T1):
 lapply (cpms_trans … HT1 … HT2) -T <commutative_plus #HT12
 /2 width=1 by cpms_inv_plus/
 qed-.
 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/lprs_cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cpms.ma
index ac04fa427baff8081ffca9bd39bcc63eba080983..0c625a2da98c46baf9f391a9d5d3975d52991f0a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cpms.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cpms.ma
@@ -53,6 +53,14 @@ elim (cpm_inv_abst1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H2 destruct
 /5 width=7 by lprs_cpm_trans, lprs_pair, cprs_step_dx, cpms_trans, ex3_2_intro/
 qed-.
 
 /5 width=7 by lprs_cpm_trans, lprs_pair, cprs_step_dx, cpms_trans, ex3_2_intro/
 qed-.
 

+lemma cpms_inv_abst_sn_cprs (h) (n) (p) (G) (L) (W):
+                            ∀T,X. ⦃G,L⦄ ⊢ ⓛ{p}W.T ➡*[n,h] X →
+                            ∃∃U. ⦃G,L.ⓛW⦄⊢ T ➡*[n,h] U & ⦃G,L⦄ ⊢ ⓛ{p}W.U ➡*[h] X.
+#h #n #p #G #L #W #T #X #H
+elim (cpms_inv_abst_sn … H) -H #W0 #U #HW0 #HTU #H destruct
+@(ex2_intro … HTU) /2 width=1 by cpms_bind/
+qed-.
+

 (* Basic_2A1: includes: cprs_inv_abst *)
 lemma cpms_inv_abst_bi (n) (h) (G) (L):
                        ∀p,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{p}W1.T1 ➡*[n, h] ⓛ{p}W2.T2 →
 (* Basic_2A1: includes: cprs_inv_abst *)
 lemma cpms_inv_abst_bi (n) (h) (G) (L):
                        ∀p,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{p}W1.T1 ➡*[n, h] ⓛ{p}W2.T2 →

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 97cfd31a44e5096dc744e2f55fc528193c7bb303..341ecee8cfde5b23e00b615b04c4d3ef40673cc7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma
@@ -290,22 +290,6 @@ lemma cpm_inv_cast1: ∀n,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝV1.U1 ➡[n, h] U2 
 ]
 qed-.
 
 ]
 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 *)
 (* Basic forward lemmas *****************************************************)
 
 (* Basic_2A1: includes: cpr_fwd_bind1_minus *)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
index ffb7cbb90d332fc4cbc01daee40aca9ffcae9c0f..3aff8e423f73848c7ca05cf6e211207152b6032a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
@@ -33,6 +33,9 @@
          for native type assignment.
    </news>
 -->
          for native type assignment.
    </news>
 -->

+   <news class="alpha" date="2018 November 1.">
+         Extended (λδ-2) and restricted (λδ-1) type rules justified.
+   </news>

    <news class="alpha" date="2018 September 21.">
          λδ-2A completed with
          confluence of rt-computation and
    <news class="alpha" date="2018 September 21.">
          λδ-2A completed with
          confluence of rt-computation and

diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index 5de8018a2086598f0d0b4cba5fb99fa21afd275a..f02240094297af8b7e0cad9da7e600412b8f805b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -25,7 +25,7 @@ table {
         ]
         [ { "context-sensitive native validity" * } {
              [ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" + "lsubv_lsubv" * ]
         ]
         [ { "context-sensitive native validity" * } {
              [ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" + "lsubv_lsubv" * ]

-             [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" + "( ⦃?,?⦄ ⊢ ? ![?] )" + "( ⦃?,?⦄ ⊢ ? !*[?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_preserve_sub" + "cnv_preserve" * ]
+             [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" + "( ⦃?,?⦄ ⊢ ? ![?] )" + "( ⦃?,?⦄ ⊢ ? !*[?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" * ]

           }
         ]
      }
           }
         ]
      }