eliminators of arited terms based on "big tree" proper computation

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_aaa.ma
new file mode 100644 (file)
index 0000000..7cef763
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_aaa.ma
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/reduction/fpb_aaa.ma".
+include "basic_2/computation/fpbs.ma".
+
+(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************)
+
+(* Properties on atomic arity assignment for terms **************************)
+
+lemma aaa_fpbs_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ →
+                     ∀A1. ⦃G1, L1⦄ ⊢ T1 ⁝ A1 → ∃A2. ⦃G2, L2⦄ ⊢ T2 ⁝ A2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2 /2 width=2 by ex_intro/
+#G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #A #HA elim (IH1 … HA) -IH1 -A
+/2 width=8 by aaa_fpb_conf/
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma
index 49b11f97188e2643bb50af4b02b58a7556501c16..1074ef74d3dad0a0254d3dd7391afcc60b91d9d8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/computation/fpbs_aaa.ma".
 include "basic_2/computation/csx_aaa.ma".
 include "basic_2/computation/fsb_csx.ma".
 
@@ -28,14 +29,43 @@ theorem aaa_fsba: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⦥
 /3 width=2 by fsb_fsba, aaa_fsb/ qed.
 
 (* Advanced eliminators on atomica arity assignment for terms ***************)
-(*
-fact aaa_ind_fpbu: ∀h,g. ∀R:relation3 genv lenv term.
-                   (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A →
-                                 (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
-                                 R G1 L1 T1
-                    ) →
-                    ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ∀A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T.
+
+fact aaa_ind_fpbu_aux: ∀h,g. ∀R:relation3 genv lenv term.
+                       (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A →
+                                     (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
+                                     R G1 L1 T1
+                       ) →
+                       ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ∀A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T.
 #h #g #R #IH #G #L #T #H @(csx_ind_fpbu … H) -G -L -T
 #G1 #L1 #T1 #H1 #IH1 #A1 #HTA1 @IH -IH //
-#G2 #L2 #T2 #H12 @IH1 //
-*)
+#G2 #L2 #T2 #H12 elim (aaa_fpbs_conf h g … G2 … L2 … T2 … HTA1) -A1
+/2 width=2 by fpbu_fwd_fpbs/
+qed-.
+
+lemma aaa_ind_fpbu: ∀h,g. ∀R:relation3 genv lenv term.
+                    (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A →
+                                  (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
+                                  R G1 L1 T1
+                    ) →
+                    ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T.
+/4 width=4 by aaa_ind_fpbu_aux, aaa_csx/ qed-.
+
+fact aaa_ind_fpbg_aux: ∀h,g. ∀R:relation3 genv lenv term.
+                       (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A →
+                                     (∀G2,L2,T2. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
+                                     R G1 L1 T1
+                       ) →
+                       ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ∀A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T.
+#h #g #R #IH #G #L #T #H @(csx_ind_fpbg … H) -G -L -T
+#G1 #L1 #T1 #H1 #IH1 #A1 #HTA1 @IH -IH //
+#G2 #L2 #T2 #H12 elim (aaa_fpbs_conf h g … G2 … L2 … T2 … HTA1) -A1
+/2 width=2 by fpbg_fwd_fpbs/
+qed-.
+
+lemma aaa_ind_fpbg: ∀h,g. ∀R:relation3 genv lenv term.
+                    (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A →
+                                  (∀G2,L2,T2. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) →
+                                  R G1 L1 T1
+                    ) →
+                    ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T.
+/4 width=4 by aaa_ind_fpbg_aux, aaa_csx/ qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_aaa.ma
new file mode 100644 (file)
index 0000000..d61a11a
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_aaa.ma
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/static/aaa_fqus.ma".
+include "basic_2/reduction/lpx_aaa.ma".
+include "basic_2/reduction/fpb.ma".
+
+(* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************)
+
+(* Properties on atomic arity assignment for terms **************************)
+
+lemma aaa_fpb_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ →
+                    ∀A1. ⦃G1, L1⦄ ⊢ T1 ⁝ A1 → ∃A2. ⦃G2, L2⦄ ⊢ T2 ⁝ A2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
+/3 width=6 by aaa_lpx_conf, aaa_cpx_conf, aaa_fquq_conf, ex_intro/
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_fqus.ma
new file mode 100644 (file)
index 0000000..cc37772
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_fqus.ma
@@ -0,0 +1,63 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/substitution/fqus_alt.ma".
+include "basic_2/static/aaa_lift.ma".
+
+(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
+
+(* Properties on supclosure *************************************************)
+
+lemma aaa_fqu_conf: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ →
+                    ∀A1. ⦃G1, L1⦄ ⊢ T1 ⁝ A1 → ∃A2. ⦃G2, L2⦄ ⊢ T2 ⁝ A2.
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+[ #I #G #L #T #A #H elim (aaa_inv_lref … H) -H
+  #J #K #V #H #HA lapply (ldrop_inv_O2 … H) -H
+  #H destruct /2 width=2 by ex_intro/
+| * [ #a ] * #G #L #V #T #X #H
+  [ elim (aaa_inv_abbr … H)
+  | elim (aaa_inv_abst … H)
+  | elim (aaa_inv_appl … H)
+  | elim (aaa_inv_cast … H)
+  ] -H /2 width=2 by ex_intro/
+| #a * #G #L #V #T #X #H
+  [ elim (aaa_inv_abbr … H)
+  | elim (aaa_inv_abst … H)
+  ] -H /2 width=2 by ex_intro/
+| * #G #L #V #T #X #H
+  [ elim (aaa_inv_appl … H)
+  | elim (aaa_inv_cast … H)
+  ] -H /2 width=2 by ex_intro/
+| /3 width=8 by aaa_inv_lift, ex_intro/
+]
+qed-.
+
+lemma aaa_fquq_conf: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+                     ∀A1. ⦃G1, L1⦄ ⊢ T1 ⁝ A1 → ∃A2. ⦃G2, L2⦄ ⊢ T2 ⁝ A2.
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim(fquq_inv_gen … H) -H /2 width=6 by aaa_fqu_conf/
+* #H1 #H2 #H3 destruct /2 width=2 by ex_intro/
+qed-.
+
+lemma aaa_fqup_conf: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
+                     ∀A1. ⦃G1, L1⦄ ⊢ T1 ⁝ A1 → ∃A2. ⦃G2, L2⦄ ⊢ T2 ⁝ A2.
+#G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
+[2: #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #A #HA elim (IH1 … HA) -IH1 -A ]
+/2 width=6 by aaa_fqu_conf/
+qed-.
+
+lemma aaa_fqus_conf: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
+                     ∀A1. ⦃G1, L1⦄ ⊢ T1 ⁝ A1 → ∃A2. ⦃G2, L2⦄ ⊢ T2 ⁝ A2.
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim(fqus_inv_gen … H) -H /2 width=6 by aaa_fqup_conf/
+* #H1 #H2 #H3 destruct /2 width=2 by ex_intro/
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lift.ma
index bcbb5c20785f91730ac540b4ccac6fcc713c2f9a..ea039002f6202dd34dc936519da205c2d14fd01a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_lift.ma
@@ -17,7 +17,7 @@ include "basic_2/static/aaa.ma".
 
 (* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
 
-(* Properties concerning basic relocation ***********************************)
+(* Properties on basic relocation *******************************************)
 
 lemma aaa_lift: ∀G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 →
                 ∀T2. ⇧[d, e] T1 ≡ T2 → ⦃G, L2⦄ ⊢ T2 ⁝ A.
@@ -26,23 +26,23 @@ lemma aaa_lift: ∀G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → ∀L2,d,e. ⇩[d, e]
   >(lift_inv_sort1 … H) -H //
 | #I #G #L1 #K1 #V1 #B #i #HLK1 #_ #IHB #L2 #d #e #HL21 #T2 #H
   elim (lift_inv_lref1 … H) -H * #Hid #H destruct
-  [ elim (ldrop_trans_le … HL21 … HLK1) -L1 /2 width=2/ #X #HLK2 #H
-    elim (ldrop_inv_skip2 … H) -H /2 width=1/ -Hid #K2 #V2 #HK21 #HV12 #H destruct
+  [ elim (ldrop_trans_le … HL21 … HLK1) -L1 /2 width=2 by lt_to_le/ #X #HLK2 #H
+    elim (ldrop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ -Hid #K2 #V2 #HK21 #HV12 #H destruct
     /3 width=8/
-  | lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
+  | lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 /3 width=8 by aaa_lref/
   ]
 | #a #G #L1 #V1 #T1 #B #A #_ #_ #IHB #IHA #L2 #d #e #HL21 #X #H
   elim (lift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
-  /4 width=4/
+  /4 width=4 by aaa_abbr, ldrop_skip/
 | #a #G #L1 #V1 #T1 #B #A #_ #_ #IHB #IHA #L2 #d #e #HL21 #X #H
   elim (lift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
-  /4 width=4/
+  /4 width=4 by aaa_abst, ldrop_skip/
 | #G #L1 #V1 #T1 #B #A #_ #_ #IHB #IHA #L2 #d #e #HL21 #X #H
   elim (lift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
-  /3 width=4/
+  /3 width=4 by aaa_appl/
 | #G #L1 #V1 #T1 #A #_ #_ #IH1 #IH2 #L2 #d #e #HL21 #X #H
   elim (lift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
-  /3 width=4/
+  /3 width=4 by aaa_cast/
 ]
 qed.
 
@@ -53,20 +53,20 @@ lemma aaa_inv_lift: ∀G,L2,T2,A. ⦃G, L2⦄ ⊢ T2 ⁝ A → ∀L1,d,e. ⇩[d,
   >(lift_inv_sort2 … H) -H //
 | #I #G #L2 #K2 #V2 #B #i #HLK2 #_ #IHB #L1 #d #e #HL21 #T1 #H
   elim (lift_inv_lref2 … H) -H * #Hid #H destruct
-  [ elim (ldrop_conf_lt … HL21 … HLK2) -L2 // -Hid /3 width=8/
-  | lapply (ldrop_conf_ge … HL21 … HLK2 ?) -L2 // -Hid /3 width=8/
+  [ elim (ldrop_conf_lt … HL21 … HLK2) -L2 /3 width=8 by aaa_lref/
+  | lapply (ldrop_conf_ge … HL21 … HLK2 ?) -L2 /3 width=8 by aaa_lref/
   ]
 | #a #G #L2 #V2 #T2 #B #A #_ #_ #IHB #IHA #L1 #d #e #HL21 #X #H
   elim (lift_inv_bind2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
-  /4 width=4/
+  /4 width=4 by aaa_abbr, ldrop_skip/
 | #a #G #L2 #V2 #T2 #B #A #_ #_ #IHB #IHA #L1 #d #e #HL21 #X #H
   elim (lift_inv_bind2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
-  /4 width=4/
+  /4 width=4 by aaa_abst, ldrop_skip/
 | #G #L2 #V2 #T2 #B #A #_ #_ #IHB #IHA #L1 #d #e #HL21 #X #H
   elim (lift_inv_flat2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
-  /3 width=4/
+  /3 width=4 by aaa_appl/
 | #G #L2 #V2 #T2 #A #_ #_ #IH1 #IH2 #L1 #d #e #HL21 #X #H
   elim (lift_inv_flat2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
-  /3 width=4/
+  /3 width=4 by aaa_cast/
 ]
 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 48a2983e93e8b5154652c29175ee1fc8540a48da..4f3d0f8dd234d8d2b7670d643061ef1066e58a59 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
@@ -93,7 +93,7 @@ table {
              [ "fpbg ( ⦃?,?,?⦄ >⋕[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fpns" + "fpbg_fpbg" * ]
              [ "fpbc ( ⦃?,?,?⦄ ≻⋕[?,?] ⦃?,?,?⦄ )" "fpbc_fpns" + "fpbc_fpbs" * ]
              [ "fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpbu_lift" + "fpbu_fpns" * ]
-             [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fpns" + "fpbs_fpbs" * ]
+             [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_aaa" + "fpbs_fpns" + "fpbs_fpbs" * ]
           }
         ]
         [ { "parallel computation for \"big tree\" normal forms" * } {
@@ -127,7 +127,7 @@ table {
    class "water"
    [ { "reduction" * } {
         [ { "\"big tree\" parallel reduction" * } {
-             [ "fpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "fpb_lift" * ]
+             [ "fpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "fpb_lift" + "fpb_aaa" * ]
           }
         ]
         [ { "context-sensitive extended normal forms" * } {
@@ -185,7 +185,7 @@ table {
           }
         ]
         [ { "atomic arity assignment" * } {
-             [ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_lift" + "aaa_lifts" + "aaa_da" + "aaa_ssta" + "aaa_aaa" * ]
+             [ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_lift" + "aaa_lifts" + "aaa_fqus" + "aaa_da" + "aaa_ssta" + "aaa_aaa" * ]
           }
         ]
         [ { "stratified static type assignment" * } {