bug fix in cpg allows to prove lsubr_cpg_trans

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma
index 22c671d90e4aeb3afeb82a2ff73b5bcd34905a8a..d270bd2be039c3779158008d00254e6659f0da94 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma
@@ -27,7 +27,7 @@ inductive cpg (h): rtc → relation4 genv lenv term term ≝
 | cpg_atom : ∀I,G,L. cpg h (𝟘𝟘) G L (⓪{I}) (⓪{I})
 | cpg_ess  : ∀G,L,s. cpg h (𝟘𝟙) G L (⋆s) (⋆(next h s))
 | cpg_delta: ∀c,G,L,V1,V2,W2. cpg h c G L V1 V2 →
-             ⬆*[1] V2 ≡ W2 → cpg h (↓c) G (L.ⓓV1) (#0) W2
+             ⬆*[1] V2 ≡ W2 → cpg h c G (L.ⓓV1) (#0) W2
 | cpg_ell  : ∀c,G,L,V1,V2,W2. cpg h c G L V1 V2 →
              ⬆*[1] V2 ≡ W2 → cpg h ((↓c)+𝟘𝟙) G (L.ⓛV1) (#0) W2
 | cpg_lref : ∀c,I,G,L,V,T,U,i. cpg h c G L (#i) T → 
@@ -73,7 +73,7 @@ fact cpg_inv_atom1_aux: ∀c,h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[c, h] T2 → ∀
                         ∨∨ T2 = ⓪{J} ∧ c = 𝟘𝟘 
                          | ∃∃s. J = Sort s & T2 = ⋆(next h s) & c = 𝟘𝟙
                          | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
-                                         L = K.ⓓV1 & J = LRef 0 & c = ↓cV
+                                         L = K.ⓓV1 & J = LRef 0 & c = cV
                          | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
                                          L = K.ⓛV1 & J = LRef 0 & c = (↓cV)+𝟘𝟙
                          | ∃∃I,K,V,T,i. ⦃G, K⦄ ⊢ #i ➡[c, h] T & ⬆*[1] T ≡ T2 &
@@ -98,7 +98,7 @@ lemma cpg_inv_atom1: ∀c,h,J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ➡[c, h] T2 →
                      ∨∨ T2 = ⓪{J} ∧ c = 𝟘𝟘 
                       | ∃∃s. J = Sort s & T2 = ⋆(next h s) & c = 𝟘𝟙
                       | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
-                                      L = K.ⓓV1 & J = LRef 0 & c = ↓cV
+                                      L = K.ⓓV1 & J = LRef 0 & c = cV
                       | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
                                       L = K.ⓛV1 & J = LRef 0 & c = (↓cV)+𝟘𝟙
                       | ∃∃I,K,V,T,i. ⦃G, K⦄ ⊢ #i ➡[c, h] T & ⬆*[1] T ≡ T2 &
@@ -118,7 +118,7 @@ qed-.
 lemma cpg_inv_zero1: ∀c,h,G,L,T2. ⦃G, L⦄ ⊢ #0 ➡[c, h] T2 →
                      ∨∨ (T2 = #0 ∧ c = 𝟘𝟘)
                       | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
-                                      L = K.ⓓV1 & c = ↓cV
+                                      L = K.ⓓV1 & c = cV
                       | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
                                       L = K.ⓛV1 & c = (↓cV)+𝟘𝟙.
 #c #h #G #L #T2 #H

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma
index 4ccf66fdfa32ea49c65e90627b36a7a72d5b6578..950b046a4740a1e6eb6e66f8bcb75163d16ca008 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma
@@ -22,7 +22,7 @@ include "basic_2/rt_transition/cpg.ma".
 (* Advanced properties ******************************************************)
 
 lemma cpg_delta_drops: ∀c,h,G,K,V,V2,i,L,T2. ⬇*[i] L ≡ K.ⓓV → ⦃G, K⦄ ⊢ V ➡[c, h] V2 →
-                       ⬆*[⫯i] V2 ≡ T2 →  ⦃G, L⦄ ⊢ #i ➡[↓c, h] T2.
+                       ⬆*[⫯i] V2 ≡ T2 →  ⦃G, L⦄ ⊢ #i ➡[c, h] T2.
 #c #h #G #K #V #V2 #i elim i -i
 [ #L #T2 #HLK lapply (drops_fwd_isid … HLK ?) // #H destruct /3 width=3 by cpg_delta/
 | #i #IH #L0 #T0 #H0 #HV2 #HVT2
@@ -46,7 +46,7 @@ qed.
 lemma cpg_inv_lref1_drops: ∀c,h,G,i,L,T2. ⦃G, L⦄ ⊢ #i ➡[c, h] T2 →
                            ∨∨ T2 = #i ∧ c = 𝟘𝟘
                             | ∃∃cV,K,V,V2. ⬇*[i] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ➡[cV, h] V2 &
-                                           ⬆*[⫯i] V2 ≡ T2 & c = ↓cV
+                                           ⬆*[⫯i] V2 ≡ T2 & c = cV
                             | ∃∃cV,K,V,V2. ⬇*[i] L ≡ K.ⓛV & ⦃G, K⦄ ⊢ V ➡[cV, h] V2 &
                                            ⬆*[⫯i] V2 ≡ T2 & c = (↓cV) + 𝟘𝟙.
 #c #h #G #i elim i -i

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_lsubr.ma
index f5b94d9050da15f5b2b8e722d9537335900f06a5..93d12c2ed3dbfe9ec9d4eaab5a92f6c3da83eb0a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_lsubr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_lsubr.ma
@@ -22,18 +22,18 @@ include "basic_2/rt_transition/cpg.ma".
 lemma lsubr_cpg_trans: ∀c,h,G. lsub_trans … (cpg h c G) lsubr.
 #c #h #G #L1 #T1 #T2 #H elim H -c -G -L1 -T1 -T2
 [ //
-| /2 width=2 by cpg_st/
+| /2 width=2 by cpg_ess/
 | #c #G #L1 #V1 #V2 #W2 #_ #HVW2 #IH #X #H
   elim (lsubr_inv_abbr2 … H) -H #L2 #HL21 #H destruct
   /3 width=3 by cpg_delta/
 | #c #G #L1 #V1 #V2 #W2 #_ #HVW2 #IH #X #H
   elim (lsubr_inv_abst2 … H) -H * #L2 [2: #V ] #HL21 #H destruct
-  /4 width=3 by cpg_delta, cpg_lt, cpg_ct/
+  /4 width=3 by cpg_delta, cpg_ell, cpg_ee/
 | #c #I1 #G #L1 #V1 #T1 #U1 #i #_ #HTU1 #IH #X #H
   elim (lsubr_fwd_pair2 … H) -H #I2 #L2 #V2 #HL21 #H destruct
-  /3 width=3 by cpt_lref/
+  /3 width=3 by cpg_lref/
 |6,11: /4 width=1 by cpg_bind, cpg_beta, lsubr_pair/
-|7,9,10: /3 width=1 by cpg_flat, cpg_eps, cpg_ct/
+|7,9,10: /3 width=1 by cpg_flat, cpg_eps, cpg_ee/
 |8,12: /4 width=3 by cpg_zeta, cpg_theta, lsubr_pair/
 ]
 qed-.

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 9d6e316b05562adcf7db4792a6e699fba68a7e34..a871f92bc6a11d240f2f6404043780b9773c36a8 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
@@ -128,62 +128,32 @@ table {
         ]
      }
    ]
+*)
    class "water"
-   [ { "reduction" * } {
+   [ { "rt-transition" * } {
+(*
         [ { "parallel qrst-reduction" * } {
              [ "fpbq ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "fpbq_alt ( ⦃?,?,?⦄ ≽≽[?,?] ⦃?,?,?⦄ )" "fpbq_lift" + "fpbq_aaa" * ]
              [ "fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpb_lift" + "fpb_lleq" + "fpb_fleq" * ]
           }
         ]
-        [ { "normal forms for context-sensitive rt-reduction" * } {
-             [ "cnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ )" "cnx_lift" + "cnx_crx" + "cnx_cix" * ]
-          }
-        ]
         [ { "context-sensitive rt-reduction" * } {
              [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_drop" + "lpx_frees" + "lpx_lleq" + "lpx_aaa" * ]
              [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_lreq" + "cpx_lift" + "cpx_llpx_sn" + "cpx_lleq" + "cpx_cix" * ]
           }
         ]
-        [ { "irreducible forms for context-sensitive rt-reduction" * } {
-             [ "cix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )" "cix_lift" * ]
-          }
-        ]
-        [ { "reducible forms for context-sensitive rt-reduction" * } {
-             [ "crx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )" "crx_lift" * ]
-          }
-        ]
-        [ { "normal forms for context-sensitive reduction" * } {
-             [ "cnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )" "cnr_lift" + "cnr_crr" + "cnr_cir" * ]
-          }
-        ]
         [ { "context-sensitive reduction" * } {
              [ "lpr ( ⦃?,?⦄ ⊢ ➡ ? )" "lpr_drop" + "lpr_lpr" * ]
              [ "cpr ( ⦃?,?⦄ ⊢ ? ➡ ? )" "cpr_lift" + "cpr_llpx_sn" + "cpr_cir" * ]
           }
         ]
-        [ { "irreducible forms for context-sensitive reduction" * } {
-             [ "cir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )" "cir_lift" * ]
-          }
-        ]
-        [ { "reducible forms for context-sensitive reduction" * } {
-             [ "crr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )" "crr_lift" * ]
-          }
-        ]
-     }
-   ]
-   class "green"
-   [ { "unfold" * } {
-        [ { "unfold" * } {
-             [ "unfold ( ⦃?,?⦄ ⊢ ? ⧫* ? )" * ]
-          }
-        ]
-        [ { "iterated static type assignment" * } {
-             [ "lstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? )" "lstas_lift" + "lstas_llpx_sn.ma" + "lstas_aaa" + "lstas_da" + "lstas_lstas" * ]
+*)
+        [ { "counted context-sensitive rt-transition" * } {
+             [ "cpg ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpg_simple" + "cpg_drops" + "cpg_lsubr" * ]
           }
         ]
      }
    ]
-*)
    class "green"
    [ { "static typing" * } {
         [ { "parameters" * } {
@@ -299,6 +269,38 @@ class "capitalize italic" { 0 }
 
 class "italic"            { 1 }
 (*
+        [ { "normal forms for context-sensitive rt-reduction" * } {
+             [ "cnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ )" "cnx_lift" + "cnx_crx" + "cnx_cix" * ]
+          }
+        ]
+        [ { "irreducible forms for context-sensitive rt-reduction" * } {
+             [ "cix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )" "cix_lift" * ]
+          }
+        ]
+        [ { "reducible forms for context-sensitive rt-reduction" * } {
+             [ "crx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )" "crx_lift" * ]
+          }
+        ]
+        [ { "normal forms for context-sensitive reduction" * } {
+             [ "cnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )" "cnr_lift" + "cnr_crr" + "cnr_cir" * ]
+          }
+        ]
+        [ { "irreducible forms for context-sensitive reduction" * } {
+             [ "cir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )" "cir_lift" * ]
+          }
+        ]
+        [ { "reducible forms for context-sensitive reduction" * } {
+             [ "crr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )" "crr_lift" * ]
+          }
+        ]
+        [ { "unfold" * } {
+             [ "unfold ( ⦃?,?⦄ ⊢ ? ⧫* ? )" * ]
+          }
+        ]
+        [ { "iterated static type assignment" * } {
+             [ "lstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? )" "lstas_lift" + "lstas_llpx_sn.ma" + "lstas_aaa" + "lstas_da" + "lstas_lstas" * ]
+          }
+        ]
         [ { "local env. ref. for degree assignment" * } {
              [ "lsubd ( ? ⊢ ? ⫃▪[?,?] ? )" "lsubd_da" + "lsubd_lsubd" * ]
           }