From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 15 Jul 2019 17:40:22 +0000 (+0200)
Subject: additions and corrections for the article on λδ-2B
X-Git-Tag: make_still_working~243
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b4283c079ed7069016b8d924bbc7e08872440829;p=helm.git

additions and corrections for the article on λδ-2B

+ candidates: condition S4 removed
+ arity assignment: decidability proved
+ minor additions
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cnx.ma
index 6dd802001..453c91e45 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cnx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cnx.ma
@@ -17,10 +17,16 @@ include "basic_2/rt_computation/cpxs.ma".
 
 (* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
 
+(* Properties with normal forms *********************************************)
+
+lemma cpxs_cnx (h) (G) (L) (T1):
+      (∀T2. ⦃G,L⦄ ⊢ T1 ⬈*[h] T2 → T1 ≛ T2) → ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃T1⦄.
+/3 width=1 by cpx_cpxs/ qed.
+
 (* Inversion lemmas with normal terms ***************************************)
 
-lemma cpxs_inv_cnx1: ∀h,G,L,T1,T2. ⦃G,L⦄ ⊢ T1 ⬈*[h] T2 → ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃T1⦄ →
-                     T1 ≛ T2.
+lemma cpxs_inv_cnx1 (h) (G) (L):
+      ∀T1,T2. ⦃G,L⦄ ⊢ T1 ⬈*[h] T2 → ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃T1⦄ → T1 ≛ T2.
 #h #G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1
 /5 width=9 by cnx_tdeq_trans, tdeq_trans/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma
index 91a7f2925..fbaee7c73 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma
@@ -38,5 +38,6 @@ qed.
 
 (* Advanced properties ******************************************************)
 
+(* Note: strong normalization does not depend on this any more *)
 lemma csx_applv_sort: ∀h,G,L,s,Vs. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃Vs⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.⋆s⦄.
 /3 width=6 by csx_applv_cnx, cnx_sort, simple_atom/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcp.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcp.ma
index ead714a32..716032c85 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcp.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcp.ma
@@ -23,7 +23,7 @@ include "basic_2/rt_computation/csx_drops.ma".
 theorem csx_gcp: ∀h. gcp (cpx h) tdeq (csx h).
 #h @mk_gcp
 [ normalize /3 width=13 by cnx_lifts/
-| /3 width=5 by O, cnx_sort, ex_intro/
+| /2 width=4 by cnx_sort/
 | /2 width=8 by csx_lifts/
 | /2 width=3 by csx_fwd_flat_dx/
 ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcr.ma
index b95725eec..a757a9374 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcr.ma
@@ -21,12 +21,13 @@ include "basic_2/rt_computation/csx_csx_vector.ma".
 (* Main properties with generic candidates of reducibility ******************)
 
 theorem csx_gcr: ∀h. gcr (cpx h) tdeq (csx h) (csx h).
-#h @mk_gcr //
-[ /3 width=1 by csx_applv_cnx/
-|2,3,6: /2 width=1 by csx_applv_beta, csx_applv_sort, csx_applv_cast/
+#h @mk_gcr
+[ //
+| #G #L #Vs #Hvs #T #HT #H
+  @(csx_applv_cnx … H) -H // (**) (* auto fails *)
+| /2 width=1 by csx_applv_beta/
 | /2 width=7 by csx_applv_delta/
-| #G #L #V1b #V2b #HV12b #a #V #T #H #HV
-  @(csx_applv_theta … HV12b) -HV12b
-  @csx_abbr //
+| /3 width=3 by csx_applv_theta, csx_abbr/
+| /2 width=1 by csx_applv_cast/
 ]
 qed.
diff --git a/matita/matita/contribs/lambdadelta/static_2/static/aaa_aaa.ma b/matita/matita/contribs/lambdadelta/static_2/static/aaa_aaa.ma
index bd1eb91a2..968112846 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/aaa_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/aaa_aaa.ma
@@ -36,3 +36,22 @@ theorem aaa_mono: ∀G,L,T,A1. ⦃G,L⦄ ⊢ T ⁝ A1 → ∀A2. ⦃G,L⦄ ⊢ T
   elim (aaa_inv_cast … H) -H /2 width=1 by/
 ]
 qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma aaa_aaa_inv_appl (G) (L) (V) (T) (B) (X):
+      ∀A. ⦃G,L⦄ ⊢ ⓐV.T ⁝ A → ⦃G,L⦄ ⊢ V ⁝ B → ⦃G,L⦄⊢ T ⁝ X → ②B.A = X.
+#G #L #V #T #B #X #A #H #H1V #H1T
+elim (aaa_inv_appl … H) -H #B0 #H2V #H2T
+lapply (aaa_mono … H2V … H1V) -V #H destruct
+lapply (aaa_mono … H2T … H1T) -G -L -T //
+qed-.
+
+lemma aaa_aaa_inv_cast (G) (L) (U) (T) (B) (A):
+      ∀X. ⦃G,L⦄ ⊢ ⓝU.T ⁝ X → ⦃G,L⦄ ⊢ U ⁝ B → ⦃G,L⦄⊢ T ⁝ A → ∧∧ B = X & A = X.
+#G #L #U #T #B #A #X #H #H1U #H1T
+elim (aaa_inv_cast … H) -H #H2U #H2T
+lapply (aaa_mono … H1U … H2U) -U #HB
+lapply (aaa_mono … H1T … H2T) -G -L -T #HA
+/2 width=1 by conj/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/static_2/static/aaa_dec.ma b/matita/matita/contribs/lambdadelta/static_2/static/aaa_dec.ma
new file mode 100644
index 000000000..045657326
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/static_2/static/aaa_dec.ma
@@ -0,0 +1,80 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "static_2/static/aaa_drops.ma".
+include "static_2/static/aaa_aaa.ma".
+
+(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
+
+(* Main properties **********************************************************)
+
+theorem aaa_dec (G) (L) (T): Decidable (∃A. ⦃G,L⦄ ⊢ T ⁝ A).
+#G #L #T @(fqup_wf_ind_eq (Ⓣ) … G L T) -G -L -T
+#G0 #L0 #T0 #IH #G #L * * [||| #p * | * ]
+[ #s #HG #HL #HT destruct -IH
+  /3 width=2 by aaa_sort, ex_intro, or_introl/
+| #i #HG #HL #HT destruct
+  elim (drops_F_uni L i) [| * * #I [| #V ] #K ] #HLK
+  [1,2: -IH
+    @or_intror * #A #H
+    elim (aaa_inv_lref_drops … H) -H #J #Y #X #HLY #_ -G -A
+    lapply (drops_mono … HLY … HLK) -L -i #H destruct
+  | elim (IH G K V) -IH [3: /2 width=2 by fqup_lref/ ]
+    [ * /4 width=6 by aaa_lref_drops, ex_intro, or_introl/
+    | #H0 @or_intror * #A #H
+      lapply (aaa_pair_inv_lref … H … HLK) -I -L -i
+      /3 width=2 by ex_intro/
+    ]
+  ]
+| #l #HG #HL #HT destruct -IH
+  @or_intror * #A #H
+  @(aaa_inv_gref … H)
+| #V #T #HG #HL #HT destruct
+  elim (IH G L V) [ * #B #HB | #HnB | // ]
+  [ elim (IH G (L.ⓓV) T) [ * #A #HA | #HnA | // ] ] -IH
+  [ /4 width=2 by aaa_abbr, ex_intro, or_introl/ ]
+  @or_intror * #A #H
+  elim (aaa_inv_abbr … H) -H #B0 #HB0 #HA0
+  /3 width=2 by ex_intro/
+| #W #T #HG #HL #HT destruct
+  elim (IH G L W) [ * #B #HB | #HnB | // ]
+  [ elim (IH G (L.ⓛW) T) [ * #A #HA | #HnA | // ] ] -IH
+  [ /4 width=2 by aaa_abst, ex_intro, or_introl/ ]
+  @or_intror * #A #H
+  elim (aaa_inv_abst … H) -H #B0 #A0 #HB0 #HA0 #H destruct
+  /3 width=2 by ex_intro/
+| #V #T #HG #HL #HT destruct
+  elim (IH G L V) [ * #B #HB | #HnB | // ]
+  [ elim (IH G L T) [ * #X #HX | #HnX | // ] ] -IH
+  [ elim (is_apear_dec B X) [ * #A #H destruct | #HnX ]
+    [ /4 width=4 by aaa_appl, ex_intro, or_introl/ ]
+  ]
+  @or_intror * #A #H
+  [ lapply (aaa_aaa_inv_appl … H HB HX) -G -L -V -T
+  |*: elim (aaa_inv_appl … H) -H #B0 #HB0 #HA0
+  ]
+  /3 width=2 by ex_intro/
+| #U #T #HG #HL #HT destruct
+  elim (IH G L U) [ * #B #HB | #HnB | // ]
+  [ elim (IH G L T) [ * #A #HA | #HnA | // ] ] -IH
+  [ elim (eq_aarity_dec B A) [ #H destruct | #HnA ]
+    [ /4 width=3 by aaa_cast, ex_intro, or_introl/ ]
+  ]
+  @or_intror * #X #H
+  [ elim (aaa_aaa_inv_cast … H HB HA) -G -L -U -T
+  |*: elim (aaa_inv_cast … H) -H #HU #HT
+  ]
+  /3 width=2 by ex_intro/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/static_2/static/aaa_drops.ma b/matita/matita/contribs/lambdadelta/static_2/static/aaa_drops.ma
index b006c2d21..b04f0c05f 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/aaa_drops.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/aaa_drops.ma
@@ -43,6 +43,13 @@ lemma aaa_inv_lref_drops: ∀G,A,i,L. ⦃G,L⦄ ⊢ #i ⁝ A →
 ]
 qed-.
 
+lemma aaa_pair_inv_lref (G) (L) (i):
+      ∀A. ⦃G,L⦄ ⊢ #i ⁝ A → ∀I,K,V. ⬇*[i] L ≘ K.ⓑ{I}V → ⦃G,K⦄ ⊢ V ⁝ A.
+#G #L #i #A #H #I #K #V #HLK
+elim (aaa_inv_lref_drops … H) -H #J #Y #X #HLY #HX
+lapply (drops_mono … HLY … HLK) -L -i #H destruct //
+qed-.
+
 (* Properties with generic slicing for local environments *******************)
 
 (* Basic_2A1: includes: aaa_lift *)
diff --git a/matita/matita/contribs/lambdadelta/static_2/static/gcp.ma b/matita/matita/contribs/lambdadelta/static_2/static/gcp.ma
index 569152d1e..73cfc105e 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/gcp.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/gcp.ma
@@ -17,21 +17,18 @@ include "static_2/relocation/drops_vector.ma".
 
 (* GENERIC COMPUTATION PROPERTIES *******************************************)
 
-definition nf ≝ λRR:relation4 genv lenv term term. λRS:relation term.
-                λG,L,T. NF … (RR G L) RS T.
+definition nf (RR:relation4 genv lenv term term) (RS:relation term) ≝
+              λG,L,T. NF … (RR G L) RS T.
 
 definition candidate: Type[0] ≝ relation3 genv lenv term.
 
-definition CP0 ≝ λRR:relation4 genv lenv term term. λRS:relation term.
-                 ∀G. d_liftable1 (nf RR RS G).
+definition CP0 (RR) (RS) ≝ ∀G. d_liftable1 (nf RR RS G).
 
-definition CP1 ≝ λRR:relation4 genv lenv term term. λRS:relation term.
-                 ∀G,L. ∃s. NF … (RR G L) RS (⋆s).
+definition CP1 (RR) (RS) ≝ ∀G,L,s. nf RR RS G L (⋆s).
 
-definition CP2 ≝ λRP:candidate. ∀G. d_liftable1 (RP G).
+definition CP2 (RP:candidate) ≝ ∀G. d_liftable1 (RP G).
 
-definition CP3 ≝ λRP:candidate.
-                 ∀G,L,T,s. RP G L (ⓐ⋆s.T) → RP G L T.
+definition CP3 (RP:candidate) ≝ ∀G,L,T,s. RP G L (ⓐ⋆s.T) → RP G L T.
 
 (* requirements for generic computation properties *)
 (* Basic_1: includes: nf2_lift1 *)
diff --git a/matita/matita/contribs/lambdadelta/static_2/static/gcp_aaa.ma b/matita/matita/contribs/lambdadelta/static_2/static/gcp_aaa.ma
index d1dc57ece..7fa84f9fb 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/gcp_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/gcp_aaa.ma
@@ -31,7 +31,7 @@ theorem acr_aaa_csubc_lifts: ∀RR,RS,RP.
   lapply (aaa_inv_sort … HA) -HA #H destruct
   >(lifts_inv_sort1 … H0) -H0
   lapply (acr_gcr … H1RP H2RP (⓪)) #HAtom
-  lapply (s4 … HAtom G L2 (Ⓔ)) /2 width=1 by/
+  lapply (s2 … HAtom G L2 (Ⓔ)) /3 width=7 by cp1, simple_atom/
 | #i #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
   elim (aaa_inv_lref_drops … HA) -HA #I #K1 #V1 #HLK1 #HKV1
   elim (lifts_inv_lref1 … H0) -H0 #j #Hf #H destruct
diff --git a/matita/matita/contribs/lambdadelta/static_2/static/gcp_cr.ma b/matita/matita/contribs/lambdadelta/static_2/static/gcp_cr.ma
index 10d8fa4b1..d13387c3f 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/gcp_cr.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/gcp_cr.ma
@@ -28,16 +28,13 @@ definition S1 ≝ λRP,C:candidate.
 (* Note: this is Tait's iii, or Girard's CR4 *)
 definition S2 ≝ λRR:relation4 genv lenv term term. λRS:relation term. λRP,C:candidate.
                 ∀G,L,Vs. all … (RP G L) Vs →
-                ∀T. 𝐒⦃T⦄ → NF … (RR G L) RS T → C G L (ⒶVs.T).
+                ∀T. 𝐒⦃T⦄ → nf RR RS G L T → C G L (ⒶVs.T).
 
 (* Note: this generalizes Tait's ii *)
 definition S3 ≝ λC:candidate.
                 ∀a,G,L,Vs,V,T,W.
                 C G L (ⒶVs.ⓓ{a}ⓝW.V.T) → C G L (ⒶVs.ⓐV.ⓛ{a}W.T).
 
-definition S4 ≝ λRP,C:candidate.
-                ∀G,L,Vs. all … (RP G L) Vs → ∀s. C G L (ⒶVs.⋆s).
-
 definition S5 ≝ λC:candidate. ∀I,G,L,K,Vs,V1,V2,i.
                 C G L (ⒶVs.V2) → ⬆*[↑i] V1 ≘ V2 →
                 ⬇*[i] L ≘ K.ⓑ{I}V1 → C G L (ⒶVs.#i).
@@ -54,7 +51,6 @@ record gcr (RR:relation4 genv lenv term term) (RS:relation term) (RP,C:candidate
 { s1: S1 RP C;
   s2: S2 RR RS RP C;
   s3: S3 C;
-  s4: S4 RP C;
   s5: S5 C;
   s6: S6 RP C;
   s7: S7 C
@@ -99,12 +95,14 @@ qed-.
 (* Basic_1: was:
    sc3_sn3 sc3_abst sc3_appl sc3_abbr sc3_bind sc3_cast
 *)
+(* Note: one sort must exist *)
 lemma acr_gcr: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
                ∀A. gcr RR RS RP (acr RP A).
 #RR #RS #RP #H1RP #H2RP #A elim A -A //
 #B #A #IHB #IHA @mk_gcr
 [ #G #L #T #H
-  elim (cp1 … H1RP G L) #s #HK
+  letin s ≝ 0 (* one sort must exist *)
+  lapply (cp1 … H1RP G L s) #HK
   lapply (s2 … IHB G L (Ⓔ) … HK) // #HB
   lapply (H (𝐈𝐝) L (⋆s) T ? ? ?) -H
   /3 width=6 by s1, cp3, drops_refl, lifts_refl/
@@ -117,11 +115,6 @@ lemma acr_gcr: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
   elim (lifts_inv_flat1 … H0) -H0 #U0 #X #HU0 #HX #H destruct
   elim (lifts_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT0 #H destruct
   @(s3 … IHA … (V0⨮V0s)) /5 width=6 by lifts_applv, lifts_flat, lifts_bind/
-| #G #L #Vs #HVs #s #f #L0 #V0 #X #HL0 #H #HB
-  elim (lifts_inv_applv1 … H) -H #V0s #X0 #HV0s #H0 #H destruct
-  >(lifts_inv_sort1 … H0) -X0
-  lapply (s1 … IHB … HB) #HV0
-  @(s4 … IHA … (V0⨮V0s)) /3 width=7 by gcp2_all, conj/
 | #I #G #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #f #L0 #V0 #X #HL0 #H #HB
   elim (lifts_inv_applv1 … H) -H #V0s #X0 #HV0s #H0 #H destruct
   elim (lifts_inv_lref1 … H0) -H0 #j #Hf #H destruct
diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/aarity.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/aarity.ma
index 89199fabb..db3820964 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/aarity.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/aarity.ma
@@ -72,3 +72,11 @@ lemma eq_aarity_dec: ∀A1,A2:aarity. Decidable (A1 = A2).
   ]
 ]
 qed-.
+
+lemma is_apear_dec (B) (X): Decidable (∃A. ②B.A = X).
+#B * [| #X #A ]
+[| elim (eq_aarity_dec X B) #HX ]
+[| /3 width=2 by ex_intro, or_introl/ ]
+@or_intror * #A #H destruct
+/2 width=1 by/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl
index 723104f7b..2df44f0d2 100644
--- a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl
@@ -27,7 +27,7 @@ table {
         ]
         [ { "atomic arity assignment" * } {
              [ [ "restricted refinement for lenvs" ] "lsuba" + "( ? ⊢ ? ⫃⁝ ? )" "lsuba_drops" + "lsuba_lsubr" + "lsuba_aaa" + "lsuba_lsuba" * ]
-             [ [ "for terms" ] "aaa" + "( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_rdeq" + "aaa_fdeq" + "aaa_aaa" * ]
+             [ [ "for terms" ] "aaa" + "( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_rdeq" + "aaa_fdeq" + "aaa_aaa" + "aaa_dec" * ]
           }
         ]
         [ { "degree-based equivalence" * } {