]> matita.cs.unibo.it Git - helm.git/commitdiff
- advances on cnx
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sun, 19 Feb 2017 18:56:35 +0000 (18:56 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sun, 19 Feb 2017 18:56:35 +0000 (18:56 +0000)
- generic reducibility moved to the "static" component

19 files changed:
matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_aaa.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_cr.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_drops.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_lsuba.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_lsubr.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt
matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma
matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt
matita/matita/contribs/lambdadelta/basic_2/static/gcp.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/gcp_aaa.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/gcp_cr.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/lsubc.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/lsubc_drops.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/lsubc_lsuba.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/lsubc_lsubr.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl

index d35fb52a2b748ca31c6c7d8542c5bd241e5b0f0d..7a4ad7662881ea68e23f3f77f8e7062914e763fa 100644 (file)
@@ -42,6 +42,10 @@ definition d_liftable1: predicate (relation2 lenv term) ≝
                         λR. ∀K,T. R K T → ∀b,f,L. ⬇*[b, f] L ≡ K →
                         ∀U. ⬆*[f] T ≡ U → R L U.
 
+definition d_deliftable1: predicate (relation2 lenv term) ≝
+                          λR. ∀L,U. R L U → ∀b,f,K. ⬇*[b, f] L ≡ K →
+                          ∀T. ⬆*[f] T ≡ U → R K T.
+
 definition d_liftable2: predicate (lenv → relation term) ≝
                         λR. ∀K,T1,T2. R K T1 T2 → ∀b,f,L. ⬇*[b, f] L ≡ K →
                         ∀U1. ⬆*[f] T1 ≡ U1 → 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp.ma
deleted file mode 100644 (file)
index e0e3c54..0000000
+++ /dev/null
@@ -1,52 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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/syntax/genv.ma".
-include "basic_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 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 CP1 ≝ λRR:relation4 genv lenv term term. λRS:relation term.
-                 ∀G,L. ∃s. NF … (RR G L) RS (⋆s).
-
-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.
-
-(* requirements for generic computation properties *)
-(* Basic_1: includes: nf2_lift1 *)
-(* Basic_2A1: includes: gcp0_lifts *)
-(* Basic_2A1: includes: gcp2_lifts *)
-record gcp (RR:relation4 genv lenv term term) (RS:relation term) (RP:candidate) : Prop ≝
-{ cp0: CP0 RR RS;
-  cp1: CP1 RR RS;
-  cp2: CP2 RP;
-  cp3: CP3 RP
-}.
-
-(* Basic properties *********************************************************)
-
-(* Basic_1: was only: sns3_lifts1 *)
-(* Basic_2A1: was: gcp2_lifts_all *)
-lemma gcp2_all: ∀RR,RS,RP. gcp RR RS RP → ∀G. d_liftable1_all (RP G).
-/3 width=7 by cp2, d1_liftable_liftable_all/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_aaa.ma
deleted file mode 100644 (file)
index 111d967..0000000
+++ /dev/null
@@ -1,101 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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_aaa.ma".
-include "basic_2/rt_computation/lsubc_drops.ma".
-
-(* GENERIC COMPUTATION PROPERTIES *******************************************)
-
-(* Main properties **********************************************************)
-
-(* Basic_1: was: sc3_arity_csubc *)
-theorem acr_aaa_csubc_lifts: ∀RR,RS,RP.
-                             gcp RR RS RP → gcr RR RS RP RP →
-                             ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀b,f,L0. ⬇*[b, f] L0 ≡ L1 →
-                             ∀T0. ⬆*[f] T ≡ T0 → ∀L2. G ⊢ L2 ⫃[RP] L0 →
-                             ⦃G, L2, T0⦄ ϵ[RP] 〚A〛.
-#RR #RS #RP #H1RP #H2RP #G #L1 #T @(fqup_wf_ind_eq … G L1 T) -G -L1 -T
-#Z #Y #X #IH #G #L1 * [ * | * [ #p ] * ]
-[ #s #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct -IH
-  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/
-| #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
-  lapply (acr_gcr … H1RP H2RP A) #HA
-  lapply (drops_trans … HL01 … HLK1 ??) -HL01 [3: |*: // ] #H
-  elim (drops_split_trans … H) -H [ |*: /2 width=6 by after_uni_dx/ ] #Y #HLK0 #HY
-  lapply (drops_tls_at … Hf … HY) -Hf -HY #HY
-  elim (drops_inv_skip2 … HY) -HY #K0 #V0 #HK01 #HV10 #H destruct
-  elim (lifts_total V0 (𝐔❴⫯j❵)) #V #HV0
-  elim (lsubc_drops_trans_isuni … HL20 … HLK0) -HL20 -HLK0 // #Y #HLK2 #H
-  elim (lsubc_inv_pair2 … H) -H *
-  [ #K2 #HK20 #H destruct
-    lapply (drops_isuni_fwd_drop2 … HLK2) // #HLK2b
-    lapply (s5 … HA ? G ? ? (◊) … HV0 ?) -HA
-    /4 width=11 by acr_lifts, fqup_lref, drops_inv_gen/
-  | #K2 #V2 #B #HKV2 #HK2V0 #HKV0B #_ #H1 #H2 destruct -IH -HLK1
-    lapply (drops_isuni_fwd_drop2 … HLK2) // #HLK2b
-    lapply (aaa_lifts … HKV1 … HK01 … HV10) -HKV1 -HK01 -HV10 #HKV0A
-    lapply (aaa_mono … HKV0B … HKV0A) #H destruct -HKV0B -HKV0A
-    elim (lifts_total V2 (𝐔❴⫯j❵)) #V3 #HV23
-    lapply (s5 … HA … G … (◊) … (ⓝV0.V2) (ⓝV.V3) ????)
-    [3: |*: /2 width=9 by drops_inv_gen, lifts_flat/ ] -HLK2
-    lapply (s7 … HA G L2 (◊)) -HA /3 width=7 by acr_lifts/
-  ]
-| #l #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct -IH
-  elim (aaa_inv_gref … HA)
-| #V #T #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
-  elim (aaa_inv_abbr … HA) -HA #B #HV #HT
-  elim (lifts_inv_bind1 … H0) -H0 #V0 #T0 #HV0 #HT0 #H destruct
-  lapply (acr_gcr … H1RP H2RP A) #HA
-  lapply (acr_gcr … H1RP H2RP B) #HB
-  lapply (s1 … HB) -HB #HB
-  lapply (s6 … HA G L2 (◊) (◊)) /4 width=10 by lsubc_pair, liftsv_nil, drops_skip/
-| #W #T #HG #HL #HT #Z0 #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
-  elim (aaa_inv_abst … HA) -HA #B #A #HW #HT #H destruct
-  elim (lifts_inv_bind1 … H0) -H0 #W0 #T0 #HW0 #HT0 #H destruct
-  @(acr_abst  … H1RP H2RP) /2 width=10 by/
-  #b3 #f3 #L3 #V3 #W3 #T3 #HL32 #HW03 #HT03 #H1B #H2B
-  elim (drops_lsubc_trans … H1RP … HL32 … HL20) -L2 #L2 #HL32 #HL20
-  lapply (aaa_lifts … HW … (f3∘f) L2 … W3 ?) -HW
-  [4: |*: /2 width=8 by drops_trans, lifts_trans/ ] #HW3
-  @(IH … ((↑f3)∘↑f) … (L2. ⓛW3)) -IH
-  /3 width=12 by lsubc_beta, drops_trans, drops_skip, lifts_trans/
-| #V #T #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
-  elim (aaa_inv_appl … HA) -HA #B #HV #HT
-  elim (lifts_inv_flat1 … H0) -H0 #V0 #T0 #HV0 #HT0 #H destruct
-  lapply (IH … HT … HL01 … HT0 … HL20) -HT -HT0
-  /3 width=10 by drops_refl, lifts_refl/
-| #W #T #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
-  elim (aaa_inv_cast … HA) -HA #HW #HT
-  elim (lifts_inv_flat1 … H0) -H0 #W0 #T0 #HW0 #HT0 #H destruct
-  lapply (acr_gcr … H1RP H2RP A) #HA
-  lapply (s7 … HA G L2 (◊)) /3 width=10 by/
-]
-qed.
-
-(* Basic_1: was: sc3_arity *)
-lemma acr_aaa: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
-               ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L, T⦄ ϵ[RP] 〚A〛.
-/3 width=9 by drops_refl, lifts_refl, acr_aaa_csubc_lifts/ qed.
-
-lemma gcr_aaa: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
-               ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → RP G L T.
-#RR #RS #RP #H1RP #H2RP #G #L #T #A #HT
-lapply (acr_gcr … H1RP H2RP A) #HA
-@(s1 … HA) /2 width=4 by acr_aaa/
-qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_cr.ma
deleted file mode 100644 (file)
index 4493ae7..0000000
+++ /dev/null
@@ -1,176 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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/notation/relations/ineint_5.ma".
-include "basic_2/syntax/aarity.ma".
-include "basic_2/relocation/lifts_simple.ma".
-include "basic_2/relocation/lifts_lifts_vector.ma".
-include "basic_2/relocation/drops_drops.ma".
-include "basic_2/rt_computation/gcp.ma".
-
-(* GENERIC COMPUTATION PROPERTIES *******************************************)
-
-(* Note: this is Girard's CR1 *)
-definition S1 ≝ λRP,C:candidate.
-                ∀G,L,T. C G L T → RP G L T.
-
-(* 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).
-
-(* 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).
-
-definition S6 ≝ λRP,C:candidate.
-                ∀G,L,V1b,V2b. ⬆*[1] V1b ≡ V2b →
-                ∀a,V,T. C G (L.ⓓV) (ⒶV2b.T) → RP G L V → C G L (ⒶV1b.ⓓ{a}V.T).
-
-definition S7 ≝ λC:candidate.
-                ∀G,L,Vs,T,W. C G L (ⒶVs.T) → C G L (ⒶVs.W) → C G L (ⒶVs.ⓝW.T).
-
-(* requirements for the generic reducibility candidate *)
-record gcr (RR:relation4 genv lenv term term) (RS:relation term) (RP,C:candidate) : Prop ≝
-{ 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
-}.
-
-(* the functional construction for candidates *)
-definition cfun: candidate → candidate → candidate ≝
-                 λC1,C2,G,K,T. ∀f,L,W,U.
-                 ⬇*[Ⓕ, f] L ≡ K → ⬆*[f] T ≡ U → C1 G L W → C2 G L (ⓐW.U).
-
-(* the reducibility candidate associated to an atomic arity *)
-rec definition acr (RP:candidate) (A:aarity) on A: candidate ≝
-match A with
-[ AAtom     ⇒ RP
-| APair B A ⇒ cfun (acr RP B) (acr RP A)
-].
-
-interpretation
-   "reducibility candidate of an atomic arity (abstract)"
-   'InEInt RP G L T A = (acr RP A G L T).
-
-(* Basic properties *********************************************************)
-
-(* Note: this requires Ⓕ-slicing in cfun since b is unknown in d_liftable_1 *) 
-(* Note: this requires multiple relocation *)
-(* Basic 1: includes: sc3_lift *)
-(* Basic 2A1: includes: gcr_lift *)
-(* Basic 2A1: note: gcr_lift should be acr_lift *)
-(* Basic_1: was: sc3_lift1 *)
-(* Basic 2A1: was: gcr_lifts *)
-(* Basic 2A1: note: gcr_lifts should be acr_lifts *)
-lemma acr_lifts: ∀RR,RS,RP. gcp RR RS RP → ∀A,G. d_liftable1 (acr RP A G).
-#RR #RS #RP #H #A #G elim A -A
-[ /2 width=7 by cp2/
-| #B #A #HB #HA #K #T #HKT #b #f #L #HLK #U #HTU #f0 #L0 #W #U0 #HL0 #HU0 #HW
-  lapply (drops_trans … HL0 … HLK ??) [3:|*: // ] -L #HL0K
-  lapply (lifts_trans … HTU … HU0 ??) [3:|*: // ] -U #HTU0
-  /2 width=3 by/ (**) (* full auto fails *)
-]
-qed-.
-
-(* Basic_1: was:
-   sc3_sn3 sc3_abst sc3_appl sc3_abbr sc3_bind sc3_cast
-*)
-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
-  lapply (s2 … IHB G L (◊) … HK) // #HB
-  lapply (H (𝐈𝐝) L (⋆s) T ? ? ?) -H
-  /3 width=6 by s1, cp3, drops_refl, lifts_refl/
-| #G #L #Vs #HVs #T #H1T #H2T #f #L0 #V0 #X #HL0 #H #HB
-  elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct
-  lapply (s1 … IHB … HB) #HV0
-  @(s2 … IHA  … (V0@V0s)) /3 width=13 by cp0, gcp2_all, lifts_simple_dx, conj/
-| #p #G #L #Vs #U #T #W #HA #f #L0 #V0 #X #HL0 #H #HB
-  elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
-  elim (lifts_inv_flat1 … HY) -HY #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 #Y #HV0s #HY #H destruct
-  >(lifts_inv_sort1 … HY) -Y
-  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 #Y #HV0s #HY #H destruct
-  elim (lifts_inv_lref1 … HY) -HY #j #Hf #H destruct
-  lapply (drops_trans … HL0 … HLK ??) [3: |*: // ] -HLK #H
-  elim (drops_split_trans … H) -H [ |*: /2 width=6 by after_uni_dx/ ] #Y #HLK0 #HY
-  lapply (drops_tls_at … Hf … HY) -HY #HY
-  elim (drops_inv_skip2 … HY) -HY #K0 #W1 #_ #HVW1 #H destruct
-  elim (lifts_total W1 (𝐔❴⫯j❵)) #W2 #HW12
-  lapply (lifts_trans … HVW1 … HW12 ??) -HVW1 [3: |*: // ] #H
-  lapply (lifts_conf … HV12 … H f ?) -V1 [ /2 width=3 by after_uni_succ_sn/ ] #HVW2
-  @(s5 … IHA … (V0@V0s) … HW12) /3 width=4 by drops_inv_gen, lifts_applv/
-| #G #L #V1s #V2s #HV12s #p #V #T #HA #HV #f #L0 #V10 #X #HL0 #H #HB
-  elim (lifts_inv_applv1 … H) -H #V10s #Y #HV10s #HY #H destruct
-  elim (lifts_inv_bind1 … HY) -HY #V0 #T0 #HV0 #HT0 #H destruct
-  elim (lifts_total V10 (𝐔❴1❵)) #V20 #HV120
-  elim (liftsv_total (𝐔❴1❵) V10s) #V20s #HV120s
-  @(s6 … IHA … (V10@V10s) (V20@V20s)) /3 width=7 by cp2, liftsv_cons/
-  @(HA … (↑f)) /2 width=2 by drops_skip/
-  [ @lifts_applv //
-    lapply (liftsv_trans … HV10s … HV120s ??) -V10s [3: |*: // ] #H
-    elim (liftsv_split_trans … H (𝐔❴1❵) (↑f)) /2 width=1 by after_uni_one_sn/ #V10s #HV10s #HV120s
-    >(liftsv_mono … HV12s … HV10s) -V1s //
-  | @(acr_lifts … H1RP … HB … HV120) /3 width=2 by drops_refl, drops_drop/
-  ]
-| #G #L #Vs #T #W #HA #HW #f #L0 #V0 #X #HL0 #H #HB
-  elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
-  elim (lifts_inv_flat1 … HY) -HY #W0 #T0 #HW0 #HT0 #H destruct
-  @(s7 … IHA … (V0@V0s)) /3 width=5 by lifts_applv/
-]
-qed.
-
-lemma acr_abst: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
-                ∀p,G,L,W,T,A,B. ⦃G, L, W⦄ ϵ[RP] 〚B〛 → (
-                   ∀b,f,L0,V0,W0,T0. ⬇*[b, f] L0 ≡ L → ⬆*[f] W ≡ W0 → ⬆*[↑f] T ≡ T0 →
-                                   ⦃G, L0, V0⦄ ϵ[RP] 〚B〛 → ⦃G, L0, W0⦄ ϵ[RP] 〚B〛 → ⦃G, L0.ⓓⓝW0.V0, T0⦄ ϵ[RP] 〚A〛
-                ) →
-                ⦃G, L, ⓛ{p}W.T⦄ ϵ[RP] 〚②B.A〛.
-#RR #RS #RP #H1RP #H2RP #p #G #L #W #T #A #B #HW #HA #f #L0 #V0 #X #HL0 #H #HB
-lapply (acr_gcr … H1RP H2RP A) #HCA
-lapply (acr_gcr … H1RP H2RP B) #HCB
-elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
-lapply (acr_lifts … H1RP … HW … HL0 … HW0) -HW #HW0
-lapply (s3 … HCA … p G L0 (◊)) #H @H -H
-lapply (s6 … HCA G L0 (◊) (◊) ?) // #H @H -H
-[ @(HA … HL0) //
-| lapply (s1 … HCB) -HCB #HCB
-  lapply (s7 … H2RP G L0 (◊)) /3 width=1 by/
-]
-qed.
-
-(* Basic_1: removed theorems 2: sc3_arity_gen sc3_repl *)
-(* Basic_1: removed local theorems 1: sc3_sn3_abst *)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc.ma
deleted file mode 100644 (file)
index 5b994b7..0000000
+++ /dev/null
@@ -1,107 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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/notation/relations/lrsubeqc_4.ma".
-include "basic_2/static/aaa.ma".
-include "basic_2/rt_computation/gcp_cr.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************)
-
-inductive lsubc (RP) (G): relation lenv ≝
-| lsubc_atom: lsubc RP G (⋆) (⋆)
-| lsubc_pair: ∀I,L1,L2,V. lsubc RP G L1 L2 → lsubc RP G (L1.ⓑ{I}V) (L2.ⓑ{I}V)
-| lsubc_beta: ∀L1,L2,V,W,A. ⦃G, L1, V⦄ ϵ[RP] 〚A〛 → ⦃G, L1, W⦄ ϵ[RP] 〚A〛 → ⦃G, L2⦄ ⊢ W ⁝ A →
-              lsubc RP G L1 L2 → lsubc RP G (L1. ⓓⓝW.V) (L2.ⓛW)
-.
-
-interpretation
-  "local environment refinement (generic reducibility)"
-  'LRSubEqC RP G L1 L2 = (lsubc RP G L1 L2).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact lsubc_inv_atom1_aux: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → L1 = ⋆ → L2 = ⋆.
-#RP #G #L1 #L2 * -L1 -L2
-[ //
-| #I #L1 #L2 #V #_ #H destruct
-| #L1 #L2 #V #W #A #_ #_ #_ #_ #H destruct
-]
-qed-.
-
-(* Basic_1: was just: csubc_gen_sort_r *)
-lemma lsubc_inv_atom1: ∀RP,G,L2. G ⊢ ⋆ ⫃[RP] L2 → L2 = ⋆.
-/2 width=5 by lsubc_inv_atom1_aux/ qed-.
-
-fact lsubc_inv_pair1_aux: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X →
-                          (∃∃K2. G ⊢ K1 ⫃[RP] K2 & L2 = K2.ⓑ{I}X) ∨
-                          ∃∃K2,V,W,A. ⦃G, K1, V⦄ ϵ[RP] 〚A〛 & ⦃G, K1, W⦄ ϵ[RP] 〚A〛 & ⦃G, K2⦄ ⊢ W ⁝ A &
-                                      G ⊢ K1 ⫃[RP] K2 &
-                                      L2 = K2. ⓛW & X = ⓝW.V & I = Abbr.
-#RP #G #L1 #L2 * -L1 -L2
-[ #I #K1 #V #H destruct
-| #J #L1 #L2 #V #HL12 #I #K1 #W #H destruct /3 width=3 by ex2_intro, or_introl/
-| #L1 #L2 #V1 #W2 #A #HV1 #H1W2 #H2W2 #HL12 #I #K1 #V #H destruct /3 width=10 by ex7_4_intro, or_intror/
-]
-qed-.
-
-(* Basic_1: was: csubc_gen_head_r *)
-lemma lsubc_inv_pair1: ∀RP,I,G,K1,L2,X. G ⊢ K1.ⓑ{I}X ⫃[RP] L2 →
-                       (∃∃K2. G ⊢ K1 ⫃[RP] K2 & L2 = K2.ⓑ{I}X) ∨
-                       ∃∃K2,V,W,A. ⦃G, K1, V⦄ ϵ[RP] 〚A〛 & ⦃G, K1, W⦄ ϵ[RP] 〚A〛 & ⦃G, K2⦄ ⊢ W ⁝ A &
-                                   G ⊢ K1 ⫃[RP] K2 &
-                                   L2 = K2.ⓛW & X = ⓝW.V & I = Abbr.
-/2 width=3 by lsubc_inv_pair1_aux/ qed-.
-
-fact lsubc_inv_atom2_aux: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → L2 = ⋆ → L1 = ⋆.
-#RP #G #L1 #L2 * -L1 -L2
-[ //
-| #I #L1 #L2 #V #_ #H destruct
-| #L1 #L2 #V #W #A #_ #_ #_ #_ #H destruct
-]
-qed-.
-
-(* Basic_1: was just: csubc_gen_sort_l *)
-lemma lsubc_inv_atom2: ∀RP,G,L1. G ⊢ L1 ⫃[RP] ⋆ → L1 = ⋆.
-/2 width=5 by lsubc_inv_atom2_aux/ qed-.
-
-fact lsubc_inv_pair2_aux: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → ∀I,K2,W. L2 = K2.ⓑ{I} W →
-                          (∃∃K1. G ⊢ K1 ⫃[RP] K2 & L1 = K1. ⓑ{I} W) ∨
-                          ∃∃K1,V,A. ⦃G, K1, V⦄ ϵ[RP] 〚A〛 & ⦃G, K1, W⦄ ϵ[RP] 〚A〛 & ⦃G, K2⦄ ⊢ W ⁝ A &
-                                    G ⊢ K1 ⫃[RP] K2 &
-                                    L1 = K1.ⓓⓝW.V & I = Abst.
-#RP #G #L1 #L2 * -L1 -L2
-[ #I #K2 #W #H destruct
-| #J #L1 #L2 #V #HL12 #I #K2 #W #H destruct /3 width=3 by ex2_intro, or_introl/
-| #L1 #L2 #V1 #W2 #A #HV1 #H1W2 #H2W2 #HL12 #I #K2 #W #H destruct /3 width=8 by ex6_3_intro, or_intror/
-]
-qed-.
-
-(* Basic_1: was just: csubc_gen_head_l *)
-lemma lsubc_inv_pair2: ∀RP,I,G,L1,K2,W. G ⊢ L1 ⫃[RP] K2.ⓑ{I} W →
-                       (∃∃K1. G ⊢ K1 ⫃[RP] K2 & L1 = K1.ⓑ{I} W) ∨
-                       ∃∃K1,V,A. ⦃G, K1, V⦄ ϵ[RP] 〚A〛 & ⦃G, K1, W⦄ ϵ[RP] 〚A〛 & ⦃G, K2⦄ ⊢ W ⁝ A &
-                                 G ⊢ K1 ⫃[RP] K2 &
-                                 L1 = K1.ⓓⓝW.V & I = Abst.
-/2 width=3 by lsubc_inv_pair2_aux/ qed-.
-
-(* Basic properties *********************************************************)
-
-(* Basic_1: was just: csubc_refl *)
-lemma lsubc_refl: ∀RP,G,L. G ⊢ L ⫃[RP] L.
-#RP #G #L elim L -L /2 width=1 by lsubc_pair/
-qed.
-
-(* Basic_1: removed theorems 3:
-            csubc_clear_conf csubc_getl_conf csubc_csuba
-*)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_drops.ma
deleted file mode 100644 (file)
index 59ba61a..0000000
+++ /dev/null
@@ -1,69 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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_drops.ma".
-include "basic_2/rt_computation/lsubc.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************)
-
-(* Properties with generic slicing ******************************************)
-
-(* Note: the premise 𝐔⦃f⦄ cannot be removed *)
-(* Basic_1: includes: csubc_drop_conf_O *)
-(* Basic_2A1: includes: lsubc_drop_O1_trans *)
-lemma lsubc_drops_trans_isuni: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 →
-                               ∀b,f,K2. 𝐔⦃f⦄ → ⬇*[b, f] L2 ≡ K2 →
-                               ∃∃K1. ⬇*[b, f] L1 ≡ K1 & G ⊢ K1 ⫃[RP] K2.
-#RP #G #L1 #L2 #H elim H -L1 -L2
-[ /2 width=3 by ex2_intro/
-| #I #L1 #L2 #V #HL12 #IH #b #f #K2 #Hf #H
-  elim (drops_inv_pair1_isuni … Hf H) -Hf -H *
-  [ #Hf #H destruct -IH
-    /3 width=3 by lsubc_pair, drops_refl, ex2_intro/
-  | #g #Hg #HLK2 #H destruct -HL12
-    elim (IH … Hg HLK2) -L2 -Hg /3 width=3 by drops_drop, ex2_intro/
-  ]
-| #L1 #L2 #V #W #A #HV #H1W #H2W #HL12 #IH #b #f #K2 #Hf #H
-  elim (drops_inv_pair1_isuni … Hf H) -Hf -H *
-  [ #Hf #H destruct -IH
-    /3 width=8 by drops_refl, lsubc_beta, ex2_intro/
-  | #g #Hg #HLK2 #H destruct -HL12
-    elim (IH … Hg HLK2) -L2 -Hg /3 width=3 by drops_drop, ex2_intro/
-  ]
-]
-qed-.
-
-(* Basic_1: was: csubc_drop1_conf_rev *)
-(* Basic_1: includes: csubc_drop_conf_rev *)
-(* Basic_2A1: includes: drop_lsubc_trans *)
-lemma drops_lsubc_trans: ∀RR,RS,RP. gcp RR RS RP →
-                         ∀b,f,G,L1,K1. ⬇*[b, f] L1 ≡ K1 → ∀K2. G ⊢ K1 ⫃[RP] K2 →
-                         ∃∃L2. G ⊢ L1 ⫃[RP] L2 & ⬇*[b, f] L2 ≡ K2.
-#RR #RS #RP #HR #b #f #G #L1 #K1 #H elim H -f -L1 -K1
-[ #f #Hf #Y #H lapply (lsubc_inv_atom1 … H) -H
-  #H destruct /4 width=3 by lsubc_atom, drops_atom, ex2_intro/
-| #f #I #L1 #K1 #V1 #_ #IH #K2 #HK12 elim (IH … HK12) -K1
-  /3 width=5 by lsubc_pair, drops_drop, ex2_intro/
-| #f #I #L1 #K1 #V1 #V2 #HLK1 #HV21 #IH #X #H elim (lsubc_inv_pair1 … H) -H *
-  [ #K2 #HK12 #H destruct -HLK1
-    elim (IH … HK12) -K1 /3 width=5 by lsubc_pair, drops_skip, ex2_intro/
-  | #K2 #V #W2 #A #HV #H1W2 #H2W2 #HK12 #H1 #H2 #H3 destruct
-    elim (lifts_inv_flat1 … HV21) -HV21 #W3 #V3 #HW23 #HV3 #H destruct
-    elim (IH … HK12) -IH -HK12 #K #HL1K #HK2
-    lapply (acr_lifts … HR … HV … HLK1 … HV3) -HV
-    lapply (acr_lifts … HR … H1W2 … HLK1 … HW23) -H1W2
-    /4 width=10 by lsubc_beta, aaa_lifts, drops_skip, ex2_intro/
-  ]
-]
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_lsuba.ma
deleted file mode 100644 (file)
index 2969b9a..0000000
+++ /dev/null
@@ -1,26 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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/lsuba.ma".
-include "basic_2/rt_computation/gcp_aaa.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************)
-
-(* Properties with lenv refinement for atomic arity assignment **************)
-
-lemma lsuba_lsubc: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
-                   ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → G ⊢ L1 ⫃[RP] L2.
-#RR #RS #RP #H1RP #H2RP #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubc_pair/
-#L1 #L2 #W #V #A #H elim (aaa_inv_cast … H) -H /3 width=4 by acr_aaa, lsubc_beta/
-qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_lsubr.ma
deleted file mode 100644 (file)
index 045ad95..0000000
+++ /dev/null
@@ -1,24 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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/lsubr.ma".
-include "basic_2/rt_computation/lsubc.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************)
-
-(* Forward lemmas with restricted refinement for local environments *********)
-
-lemma lsubc_fwd_lsubr: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → L1 ⫃ L2.
-#RP #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_pair, lsubr_beta/
-qed-.
index b47d0e449fcf8ff0cfc2b3824382822c9e373470..41a6c9556739856f726f04b5c2c20f3e201a9188 100644 (file)
@@ -1,3 +1 @@
-lsubc.ma lsubc_drops.ma lsubc_lsubr.ma lsubc_lsuba.ma
-gcp.ma gcp_cr.ma gcp_aaa.ma
 cpxs.ma
index b4f5e8c3d0507b526b897b80d39def1f1bf3cde8..1dcbdf2a41183b5f31f6e1846431d15636d5688f 100644 (file)
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/relocation/lifts_tdeq.ma".
 include "basic_2/rt_transition/cpx_drops.ma".
 include "basic_2/rt_transition/cnx.ma".
 
@@ -24,6 +25,15 @@ lemma cnx_lref_atom: ∀h,o,G,L,i. ⬇*[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ⬈[h, o
 #I #K #V1 #V2 #HLK lapply (drops_mono … Hi … HLK) -L #H destruct
 qed.
 
+(* Basic_2A1: includes: cnx_lift *)
+lemma cnx_lifts: ∀h,o,G. d_liftable1 … (cnx h o G).
+#h #o #G #K #T #HT #b #f #L #HLK #U #HTU #U0 #H
+elim (cpx_inv_lifts … H … HLK … HTU) -b -L #T0 #HTU0 #HT0
+lapply (HT … HT0) -G -K #HT0
+elim (tdeq_lifts … HT0 … HTU) -T #X #HX #HU
+<(lifts_mono … HX … HTU0) -T0 //
+qed-.
+
 (* Inversion lemmas with generic slicing ************************************)
 
 (* Basic_2A1: was: cnx_inv_delta *)
@@ -35,23 +45,11 @@ lapply (H W ?) -H /2 width=7 by cpx_delta_drops/ -HLK
 /2 width=5 by lifts_inv_lref2_uni_lt/
 qed-.
 
-(*
-(* Relocation properties ****************************************************)
-
-lemma cnx_lift: ∀h,o,G,L0,L,T,T0,c,l,k. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃T⦄ → ⬇[c, l, k] L0 ≡ L →
-                ⬆[l, k] T ≡ T0 → ⦃G, L0⦄ ⊢ ➡[h, o] 𝐍⦃T0⦄.
-#h #o #G #L0 #L #T #T0 #c #l #k #HLT #HL0 #HT0 #X #H
-elim (cpx_inv_lift1 … H … HL0 … HT0) -L0 #T1 #HT10 #HT1
-<(HLT … HT1) in HT0; -L #HT0
->(lift_mono … HT10 … HT0) -T1 -X //
-qed.
-
-lemma cnx_inv_lift: ∀h,o,G,L0,L,T,T0,c,l,k. ⦃G, L0⦄ ⊢ ➡[h, o] 𝐍⦃T0⦄ → ⬇[c, l, k] L0 ≡ L →
-                    ⬆[l, k] T ≡ T0 → ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃T⦄.
-#h #o #G #L0 #L #T #T0 #c #l #k #HLT0 #HL0 #HT0 #X #H
-elim (lift_total X l k) #X0 #HX0
-lapply (cpx_lift … H … HL0 … HT0 … HX0) -L #HTX0
->(HLT0 … HTX0) in HX0; -L0 -X0 #H
->(lift_inj … H … HT0) -T0 -X -l -k //
+(* Basic_2A1: includes: cnx_inv_lift *)
+lemma cnx_inv_lifts: ∀h,o,G. d_deliftable1 … (cnx h o G).
+#h #o #G #L #U #HU #b #f #K #HLK #T #HTU #T0 #H
+elim (cpx_lifts … H … HLK … HTU) -b -K #U0 #HTU0 #HU0
+lapply (HU … HU0) -G -L #HU0
+elim (tdeq_inv_lifts … HU0 … HTU) -U #X #HX #HT
+<(lifts_inj … HX … HTU0) -U0 //
 qed-.
-*)
index 9760148c18d787a8d400c64cc0344f387a556cc5..9ed6e41045337ef0e0d5001038ab737b27b8595a 100644 (file)
@@ -1,7 +1,7 @@
 cpg.ma cpg_simple.ma cpg_drops.ma cpg_lsubr.ma
 cpx.ma cpx_simple.ma cpx_drops.ma cpx_fqus.ma cpx_lsubr.ma cpx_lfxs.ma cpx_lfdeq.ma
 lfpx.ma lfpx_length.ma lfpx_drops.ma lfpx_fqup.ma lfpx_frees.ma lfpx_aaa.ma
-cnx.ma cnx_simple.ma
+cnx.ma cnx_simple.ma cnx_drops.ma
 cpm.ma cpm_simple.ma cpm_drops.ma cpm_lsubr.ma cpm_lfxs.ma cpm_cpx.ma
 cpr.ma cpr_drops.ma
 lfpr.ma lfpr_length.ma lfpr_drops.ma lfpr_fqup.ma lfpr_frees.ma lfpr_aaa.ma lfpr_lfpx.ma lfpr_lfpr.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/gcp.ma b/matita/matita/contribs/lambdadelta/basic_2/static/gcp.ma
new file mode 100644 (file)
index 0000000..e0e3c54
--- /dev/null
@@ -0,0 +1,52 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/syntax/genv.ma".
+include "basic_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 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 CP1 ≝ λRR:relation4 genv lenv term term. λRS:relation term.
+                 ∀G,L. ∃s. NF … (RR G L) RS (⋆s).
+
+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.
+
+(* requirements for generic computation properties *)
+(* Basic_1: includes: nf2_lift1 *)
+(* Basic_2A1: includes: gcp0_lifts *)
+(* Basic_2A1: includes: gcp2_lifts *)
+record gcp (RR:relation4 genv lenv term term) (RS:relation term) (RP:candidate) : Prop ≝
+{ cp0: CP0 RR RS;
+  cp1: CP1 RR RS;
+  cp2: CP2 RP;
+  cp3: CP3 RP
+}.
+
+(* Basic properties *********************************************************)
+
+(* Basic_1: was only: sns3_lifts1 *)
+(* Basic_2A1: was: gcp2_lifts_all *)
+lemma gcp2_all: ∀RR,RS,RP. gcp RR RS RP → ∀G. d_liftable1_all (RP G).
+/3 width=7 by cp2, d1_liftable_liftable_all/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/gcp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/gcp_aaa.ma
new file mode 100644 (file)
index 0000000..53b415b
--- /dev/null
@@ -0,0 +1,101 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_aaa.ma".
+include "basic_2/static/lsubc_drops.ma".
+
+(* GENERIC COMPUTATION PROPERTIES *******************************************)
+
+(* Main properties **********************************************************)
+
+(* Basic_1: was: sc3_arity_csubc *)
+theorem acr_aaa_csubc_lifts: ∀RR,RS,RP.
+                             gcp RR RS RP → gcr RR RS RP RP →
+                             ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀b,f,L0. ⬇*[b, f] L0 ≡ L1 →
+                             ∀T0. ⬆*[f] T ≡ T0 → ∀L2. G ⊢ L2 ⫃[RP] L0 →
+                             ⦃G, L2, T0⦄ ϵ[RP] 〚A〛.
+#RR #RS #RP #H1RP #H2RP #G #L1 #T @(fqup_wf_ind_eq … G L1 T) -G -L1 -T
+#Z #Y #X #IH #G #L1 * [ * | * [ #p ] * ]
+[ #s #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct -IH
+  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/
+| #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
+  lapply (acr_gcr … H1RP H2RP A) #HA
+  lapply (drops_trans … HL01 … HLK1 ??) -HL01 [3: |*: // ] #H
+  elim (drops_split_trans … H) -H [ |*: /2 width=6 by after_uni_dx/ ] #Y #HLK0 #HY
+  lapply (drops_tls_at … Hf … HY) -Hf -HY #HY
+  elim (drops_inv_skip2 … HY) -HY #K0 #V0 #HK01 #HV10 #H destruct
+  elim (lifts_total V0 (𝐔❴⫯j❵)) #V #HV0
+  elim (lsubc_drops_trans_isuni … HL20 … HLK0) -HL20 -HLK0 // #Y #HLK2 #H
+  elim (lsubc_inv_pair2 … H) -H *
+  [ #K2 #HK20 #H destruct
+    lapply (drops_isuni_fwd_drop2 … HLK2) // #HLK2b
+    lapply (s5 … HA ? G ? ? (◊) … HV0 ?) -HA
+    /4 width=11 by acr_lifts, fqup_lref, drops_inv_gen/
+  | #K2 #V2 #B #HKV2 #HK2V0 #HKV0B #_ #H1 #H2 destruct -IH -HLK1
+    lapply (drops_isuni_fwd_drop2 … HLK2) // #HLK2b
+    lapply (aaa_lifts … HKV1 … HK01 … HV10) -HKV1 -HK01 -HV10 #HKV0A
+    lapply (aaa_mono … HKV0B … HKV0A) #H destruct -HKV0B -HKV0A
+    elim (lifts_total V2 (𝐔❴⫯j❵)) #V3 #HV23
+    lapply (s5 … HA … G … (◊) … (ⓝV0.V2) (ⓝV.V3) ????)
+    [3: |*: /2 width=9 by drops_inv_gen, lifts_flat/ ] -HLK2
+    lapply (s7 … HA G L2 (◊)) -HA /3 width=7 by acr_lifts/
+  ]
+| #l #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct -IH
+  elim (aaa_inv_gref … HA)
+| #V #T #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
+  elim (aaa_inv_abbr … HA) -HA #B #HV #HT
+  elim (lifts_inv_bind1 … H0) -H0 #V0 #T0 #HV0 #HT0 #H destruct
+  lapply (acr_gcr … H1RP H2RP A) #HA
+  lapply (acr_gcr … H1RP H2RP B) #HB
+  lapply (s1 … HB) -HB #HB
+  lapply (s6 … HA G L2 (◊) (◊)) /4 width=10 by lsubc_pair, liftsv_nil, drops_skip/
+| #W #T #HG #HL #HT #Z0 #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
+  elim (aaa_inv_abst … HA) -HA #B #A #HW #HT #H destruct
+  elim (lifts_inv_bind1 … H0) -H0 #W0 #T0 #HW0 #HT0 #H destruct
+  @(acr_abst  … H1RP H2RP) /2 width=10 by/
+  #b3 #f3 #L3 #V3 #W3 #T3 #HL32 #HW03 #HT03 #H1B #H2B
+  elim (drops_lsubc_trans … H1RP … HL32 … HL20) -L2 #L2 #HL32 #HL20
+  lapply (aaa_lifts … HW … (f3∘f) L2 … W3 ?) -HW
+  [4: |*: /2 width=8 by drops_trans, lifts_trans/ ] #HW3
+  @(IH … ((↑f3)∘↑f) … (L2. ⓛW3)) -IH
+  /3 width=12 by lsubc_beta, drops_trans, drops_skip, lifts_trans/
+| #V #T #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
+  elim (aaa_inv_appl … HA) -HA #B #HV #HT
+  elim (lifts_inv_flat1 … H0) -H0 #V0 #T0 #HV0 #HT0 #H destruct
+  lapply (IH … HT … HL01 … HT0 … HL20) -HT -HT0
+  /3 width=10 by drops_refl, lifts_refl/
+| #W #T #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
+  elim (aaa_inv_cast … HA) -HA #HW #HT
+  elim (lifts_inv_flat1 … H0) -H0 #W0 #T0 #HW0 #HT0 #H destruct
+  lapply (acr_gcr … H1RP H2RP A) #HA
+  lapply (s7 … HA G L2 (◊)) /3 width=10 by/
+]
+qed.
+
+(* Basic_1: was: sc3_arity *)
+lemma acr_aaa: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
+               ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L, T⦄ ϵ[RP] 〚A〛.
+/3 width=9 by drops_refl, lifts_refl, acr_aaa_csubc_lifts/ qed.
+
+lemma gcr_aaa: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
+               ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → RP G L T.
+#RR #RS #RP #H1RP #H2RP #G #L #T #A #HT
+lapply (acr_gcr … H1RP H2RP A) #HA
+@(s1 … HA) /2 width=4 by acr_aaa/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/gcp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/static/gcp_cr.ma
new file mode 100644 (file)
index 0000000..09dd1d3
--- /dev/null
@@ -0,0 +1,176 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/notation/relations/ineint_5.ma".
+include "basic_2/syntax/aarity.ma".
+include "basic_2/relocation/lifts_simple.ma".
+include "basic_2/relocation/lifts_lifts_vector.ma".
+include "basic_2/relocation/drops_drops.ma".
+include "basic_2/static/gcp.ma".
+
+(* GENERIC COMPUTATION PROPERTIES *******************************************)
+
+(* Note: this is Girard's CR1 *)
+definition S1 ≝ λRP,C:candidate.
+                ∀G,L,T. C G L T → RP G L T.
+
+(* 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).
+
+(* 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).
+
+definition S6 ≝ λRP,C:candidate.
+                ∀G,L,V1b,V2b. ⬆*[1] V1b ≡ V2b →
+                ∀a,V,T. C G (L.ⓓV) (ⒶV2b.T) → RP G L V → C G L (ⒶV1b.ⓓ{a}V.T).
+
+definition S7 ≝ λC:candidate.
+                ∀G,L,Vs,T,W. C G L (ⒶVs.T) → C G L (ⒶVs.W) → C G L (ⒶVs.ⓝW.T).
+
+(* requirements for the generic reducibility candidate *)
+record gcr (RR:relation4 genv lenv term term) (RS:relation term) (RP,C:candidate) : Prop ≝
+{ 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
+}.
+
+(* the functional construction for candidates *)
+definition cfun: candidate → candidate → candidate ≝
+                 λC1,C2,G,K,T. ∀f,L,W,U.
+                 ⬇*[Ⓕ, f] L ≡ K → ⬆*[f] T ≡ U → C1 G L W → C2 G L (ⓐW.U).
+
+(* the reducibility candidate associated to an atomic arity *)
+rec definition acr (RP:candidate) (A:aarity) on A: candidate ≝
+match A with
+[ AAtom     ⇒ RP
+| APair B A ⇒ cfun (acr RP B) (acr RP A)
+].
+
+interpretation
+   "reducibility candidate of an atomic arity (abstract)"
+   'InEInt RP G L T A = (acr RP A G L T).
+
+(* Basic properties *********************************************************)
+
+(* Note: this requires Ⓕ-slicing in cfun since b is unknown in d_liftable_1 *) 
+(* Note: this requires multiple relocation *)
+(* Basic 1: includes: sc3_lift *)
+(* Basic 2A1: includes: gcr_lift *)
+(* Basic 2A1: note: gcr_lift should be acr_lift *)
+(* Basic_1: was: sc3_lift1 *)
+(* Basic 2A1: was: gcr_lifts *)
+(* Basic 2A1: note: gcr_lifts should be acr_lifts *)
+lemma acr_lifts: ∀RR,RS,RP. gcp RR RS RP → ∀A,G. d_liftable1 (acr RP A G).
+#RR #RS #RP #H #A #G elim A -A
+[ /2 width=7 by cp2/
+| #B #A #HB #HA #K #T #HKT #b #f #L #HLK #U #HTU #f0 #L0 #W #U0 #HL0 #HU0 #HW
+  lapply (drops_trans … HL0 … HLK ??) [3:|*: // ] -L #HL0K
+  lapply (lifts_trans … HTU … HU0 ??) [3:|*: // ] -U #HTU0
+  /2 width=3 by/ (**) (* full auto fails *)
+]
+qed-.
+
+(* Basic_1: was:
+   sc3_sn3 sc3_abst sc3_appl sc3_abbr sc3_bind sc3_cast
+*)
+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
+  lapply (s2 … IHB G L (◊) … HK) // #HB
+  lapply (H (𝐈𝐝) L (⋆s) T ? ? ?) -H
+  /3 width=6 by s1, cp3, drops_refl, lifts_refl/
+| #G #L #Vs #HVs #T #H1T #H2T #f #L0 #V0 #X #HL0 #H #HB
+  elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct
+  lapply (s1 … IHB … HB) #HV0
+  @(s2 … IHA  … (V0@V0s)) /3 width=13 by cp0, gcp2_all, lifts_simple_dx, conj/
+| #p #G #L #Vs #U #T #W #HA #f #L0 #V0 #X #HL0 #H #HB
+  elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
+  elim (lifts_inv_flat1 … HY) -HY #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 #Y #HV0s #HY #H destruct
+  >(lifts_inv_sort1 … HY) -Y
+  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 #Y #HV0s #HY #H destruct
+  elim (lifts_inv_lref1 … HY) -HY #j #Hf #H destruct
+  lapply (drops_trans … HL0 … HLK ??) [3: |*: // ] -HLK #H
+  elim (drops_split_trans … H) -H [ |*: /2 width=6 by after_uni_dx/ ] #Y #HLK0 #HY
+  lapply (drops_tls_at … Hf … HY) -HY #HY
+  elim (drops_inv_skip2 … HY) -HY #K0 #W1 #_ #HVW1 #H destruct
+  elim (lifts_total W1 (𝐔❴⫯j❵)) #W2 #HW12
+  lapply (lifts_trans … HVW1 … HW12 ??) -HVW1 [3: |*: // ] #H
+  lapply (lifts_conf … HV12 … H f ?) -V1 [ /2 width=3 by after_uni_succ_sn/ ] #HVW2
+  @(s5 … IHA … (V0@V0s) … HW12) /3 width=4 by drops_inv_gen, lifts_applv/
+| #G #L #V1s #V2s #HV12s #p #V #T #HA #HV #f #L0 #V10 #X #HL0 #H #HB
+  elim (lifts_inv_applv1 … H) -H #V10s #Y #HV10s #HY #H destruct
+  elim (lifts_inv_bind1 … HY) -HY #V0 #T0 #HV0 #HT0 #H destruct
+  elim (lifts_total V10 (𝐔❴1❵)) #V20 #HV120
+  elim (liftsv_total (𝐔❴1❵) V10s) #V20s #HV120s
+  @(s6 … IHA … (V10@V10s) (V20@V20s)) /3 width=7 by cp2, liftsv_cons/
+  @(HA … (↑f)) /2 width=2 by drops_skip/
+  [ @lifts_applv //
+    lapply (liftsv_trans … HV10s … HV120s ??) -V10s [3: |*: // ] #H
+    elim (liftsv_split_trans … H (𝐔❴1❵) (↑f)) /2 width=1 by after_uni_one_sn/ #V10s #HV10s #HV120s
+    >(liftsv_mono … HV12s … HV10s) -V1s //
+  | @(acr_lifts … H1RP … HB … HV120) /3 width=2 by drops_refl, drops_drop/
+  ]
+| #G #L #Vs #T #W #HA #HW #f #L0 #V0 #X #HL0 #H #HB
+  elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
+  elim (lifts_inv_flat1 … HY) -HY #W0 #T0 #HW0 #HT0 #H destruct
+  @(s7 … IHA … (V0@V0s)) /3 width=5 by lifts_applv/
+]
+qed.
+
+lemma acr_abst: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
+                ∀p,G,L,W,T,A,B. ⦃G, L, W⦄ ϵ[RP] 〚B〛 → (
+                   ∀b,f,L0,V0,W0,T0. ⬇*[b, f] L0 ≡ L → ⬆*[f] W ≡ W0 → ⬆*[↑f] T ≡ T0 →
+                                   ⦃G, L0, V0⦄ ϵ[RP] 〚B〛 → ⦃G, L0, W0⦄ ϵ[RP] 〚B〛 → ⦃G, L0.ⓓⓝW0.V0, T0⦄ ϵ[RP] 〚A〛
+                ) →
+                ⦃G, L, ⓛ{p}W.T⦄ ϵ[RP] 〚②B.A〛.
+#RR #RS #RP #H1RP #H2RP #p #G #L #W #T #A #B #HW #HA #f #L0 #V0 #X #HL0 #H #HB
+lapply (acr_gcr … H1RP H2RP A) #HCA
+lapply (acr_gcr … H1RP H2RP B) #HCB
+elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
+lapply (acr_lifts … H1RP … HW … HL0 … HW0) -HW #HW0
+lapply (s3 … HCA … p G L0 (◊)) #H @H -H
+lapply (s6 … HCA G L0 (◊) (◊) ?) // #H @H -H
+[ @(HA … HL0) //
+| lapply (s1 … HCB) -HCB #HCB
+  lapply (s7 … H2RP G L0 (◊)) /3 width=1 by/
+]
+qed.
+
+(* Basic_1: removed theorems 2: sc3_arity_gen sc3_repl *)
+(* Basic_1: removed local theorems 1: sc3_sn3_abst *)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubc.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubc.ma
new file mode 100644 (file)
index 0000000..7b5315d
--- /dev/null
@@ -0,0 +1,107 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/notation/relations/lrsubeqc_4.ma".
+include "basic_2/static/aaa.ma".
+include "basic_2/static/gcp_cr.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************)
+
+inductive lsubc (RP) (G): relation lenv ≝
+| lsubc_atom: lsubc RP G (⋆) (⋆)
+| lsubc_pair: ∀I,L1,L2,V. lsubc RP G L1 L2 → lsubc RP G (L1.ⓑ{I}V) (L2.ⓑ{I}V)
+| lsubc_beta: ∀L1,L2,V,W,A. ⦃G, L1, V⦄ ϵ[RP] 〚A〛 → ⦃G, L1, W⦄ ϵ[RP] 〚A〛 → ⦃G, L2⦄ ⊢ W ⁝ A →
+              lsubc RP G L1 L2 → lsubc RP G (L1. ⓓⓝW.V) (L2.ⓛW)
+.
+
+interpretation
+  "local environment refinement (generic reducibility)"
+  'LRSubEqC RP G L1 L2 = (lsubc RP G L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lsubc_inv_atom1_aux: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → L1 = ⋆ → L2 = ⋆.
+#RP #G #L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #V #_ #H destruct
+| #L1 #L2 #V #W #A #_ #_ #_ #_ #H destruct
+]
+qed-.
+
+(* Basic_1: was just: csubc_gen_sort_r *)
+lemma lsubc_inv_atom1: ∀RP,G,L2. G ⊢ ⋆ ⫃[RP] L2 → L2 = ⋆.
+/2 width=5 by lsubc_inv_atom1_aux/ qed-.
+
+fact lsubc_inv_pair1_aux: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X →
+                          (∃∃K2. G ⊢ K1 ⫃[RP] K2 & L2 = K2.ⓑ{I}X) ∨
+                          ∃∃K2,V,W,A. ⦃G, K1, V⦄ ϵ[RP] 〚A〛 & ⦃G, K1, W⦄ ϵ[RP] 〚A〛 & ⦃G, K2⦄ ⊢ W ⁝ A &
+                                      G ⊢ K1 ⫃[RP] K2 &
+                                      L2 = K2. ⓛW & X = ⓝW.V & I = Abbr.
+#RP #G #L1 #L2 * -L1 -L2
+[ #I #K1 #V #H destruct
+| #J #L1 #L2 #V #HL12 #I #K1 #W #H destruct /3 width=3 by ex2_intro, or_introl/
+| #L1 #L2 #V1 #W2 #A #HV1 #H1W2 #H2W2 #HL12 #I #K1 #V #H destruct /3 width=10 by ex7_4_intro, or_intror/
+]
+qed-.
+
+(* Basic_1: was: csubc_gen_head_r *)
+lemma lsubc_inv_pair1: ∀RP,I,G,K1,L2,X. G ⊢ K1.ⓑ{I}X ⫃[RP] L2 →
+                       (∃∃K2. G ⊢ K1 ⫃[RP] K2 & L2 = K2.ⓑ{I}X) ∨
+                       ∃∃K2,V,W,A. ⦃G, K1, V⦄ ϵ[RP] 〚A〛 & ⦃G, K1, W⦄ ϵ[RP] 〚A〛 & ⦃G, K2⦄ ⊢ W ⁝ A &
+                                   G ⊢ K1 ⫃[RP] K2 &
+                                   L2 = K2.ⓛW & X = ⓝW.V & I = Abbr.
+/2 width=3 by lsubc_inv_pair1_aux/ qed-.
+
+fact lsubc_inv_atom2_aux: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → L2 = ⋆ → L1 = ⋆.
+#RP #G #L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #V #_ #H destruct
+| #L1 #L2 #V #W #A #_ #_ #_ #_ #H destruct
+]
+qed-.
+
+(* Basic_1: was just: csubc_gen_sort_l *)
+lemma lsubc_inv_atom2: ∀RP,G,L1. G ⊢ L1 ⫃[RP] ⋆ → L1 = ⋆.
+/2 width=5 by lsubc_inv_atom2_aux/ qed-.
+
+fact lsubc_inv_pair2_aux: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → ∀I,K2,W. L2 = K2.ⓑ{I} W →
+                          (∃∃K1. G ⊢ K1 ⫃[RP] K2 & L1 = K1. ⓑ{I} W) ∨
+                          ∃∃K1,V,A. ⦃G, K1, V⦄ ϵ[RP] 〚A〛 & ⦃G, K1, W⦄ ϵ[RP] 〚A〛 & ⦃G, K2⦄ ⊢ W ⁝ A &
+                                    G ⊢ K1 ⫃[RP] K2 &
+                                    L1 = K1.ⓓⓝW.V & I = Abst.
+#RP #G #L1 #L2 * -L1 -L2
+[ #I #K2 #W #H destruct
+| #J #L1 #L2 #V #HL12 #I #K2 #W #H destruct /3 width=3 by ex2_intro, or_introl/
+| #L1 #L2 #V1 #W2 #A #HV1 #H1W2 #H2W2 #HL12 #I #K2 #W #H destruct /3 width=8 by ex6_3_intro, or_intror/
+]
+qed-.
+
+(* Basic_1: was just: csubc_gen_head_l *)
+lemma lsubc_inv_pair2: ∀RP,I,G,L1,K2,W. G ⊢ L1 ⫃[RP] K2.ⓑ{I} W →
+                       (∃∃K1. G ⊢ K1 ⫃[RP] K2 & L1 = K1.ⓑ{I} W) ∨
+                       ∃∃K1,V,A. ⦃G, K1, V⦄ ϵ[RP] 〚A〛 & ⦃G, K1, W⦄ ϵ[RP] 〚A〛 & ⦃G, K2⦄ ⊢ W ⁝ A &
+                                 G ⊢ K1 ⫃[RP] K2 &
+                                 L1 = K1.ⓓⓝW.V & I = Abst.
+/2 width=3 by lsubc_inv_pair2_aux/ qed-.
+
+(* Basic properties *********************************************************)
+
+(* Basic_1: was just: csubc_refl *)
+lemma lsubc_refl: ∀RP,G,L. G ⊢ L ⫃[RP] L.
+#RP #G #L elim L -L /2 width=1 by lsubc_pair/
+qed.
+
+(* Basic_1: removed theorems 3:
+            csubc_clear_conf csubc_getl_conf csubc_csuba
+*)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubc_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubc_drops.ma
new file mode 100644 (file)
index 0000000..d39dd68
--- /dev/null
@@ -0,0 +1,69 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_drops.ma".
+include "basic_2/static/lsubc.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************)
+
+(* Properties with generic slicing ******************************************)
+
+(* Note: the premise 𝐔⦃f⦄ cannot be removed *)
+(* Basic_1: includes: csubc_drop_conf_O *)
+(* Basic_2A1: includes: lsubc_drop_O1_trans *)
+lemma lsubc_drops_trans_isuni: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 →
+                               ∀b,f,K2. 𝐔⦃f⦄ → ⬇*[b, f] L2 ≡ K2 →
+                               ∃∃K1. ⬇*[b, f] L1 ≡ K1 & G ⊢ K1 ⫃[RP] K2.
+#RP #G #L1 #L2 #H elim H -L1 -L2
+[ /2 width=3 by ex2_intro/
+| #I #L1 #L2 #V #HL12 #IH #b #f #K2 #Hf #H
+  elim (drops_inv_pair1_isuni … Hf H) -Hf -H *
+  [ #Hf #H destruct -IH
+    /3 width=3 by lsubc_pair, drops_refl, ex2_intro/
+  | #g #Hg #HLK2 #H destruct -HL12
+    elim (IH … Hg HLK2) -L2 -Hg /3 width=3 by drops_drop, ex2_intro/
+  ]
+| #L1 #L2 #V #W #A #HV #H1W #H2W #HL12 #IH #b #f #K2 #Hf #H
+  elim (drops_inv_pair1_isuni … Hf H) -Hf -H *
+  [ #Hf #H destruct -IH
+    /3 width=8 by drops_refl, lsubc_beta, ex2_intro/
+  | #g #Hg #HLK2 #H destruct -HL12
+    elim (IH … Hg HLK2) -L2 -Hg /3 width=3 by drops_drop, ex2_intro/
+  ]
+]
+qed-.
+
+(* Basic_1: was: csubc_drop1_conf_rev *)
+(* Basic_1: includes: csubc_drop_conf_rev *)
+(* Basic_2A1: includes: drop_lsubc_trans *)
+lemma drops_lsubc_trans: ∀RR,RS,RP. gcp RR RS RP →
+                         ∀b,f,G,L1,K1. ⬇*[b, f] L1 ≡ K1 → ∀K2. G ⊢ K1 ⫃[RP] K2 →
+                         ∃∃L2. G ⊢ L1 ⫃[RP] L2 & ⬇*[b, f] L2 ≡ K2.
+#RR #RS #RP #HR #b #f #G #L1 #K1 #H elim H -f -L1 -K1
+[ #f #Hf #Y #H lapply (lsubc_inv_atom1 … H) -H
+  #H destruct /4 width=3 by lsubc_atom, drops_atom, ex2_intro/
+| #f #I #L1 #K1 #V1 #_ #IH #K2 #HK12 elim (IH … HK12) -K1
+  /3 width=5 by lsubc_pair, drops_drop, ex2_intro/
+| #f #I #L1 #K1 #V1 #V2 #HLK1 #HV21 #IH #X #H elim (lsubc_inv_pair1 … H) -H *
+  [ #K2 #HK12 #H destruct -HLK1
+    elim (IH … HK12) -K1 /3 width=5 by lsubc_pair, drops_skip, ex2_intro/
+  | #K2 #V #W2 #A #HV #H1W2 #H2W2 #HK12 #H1 #H2 #H3 destruct
+    elim (lifts_inv_flat1 … HV21) -HV21 #W3 #V3 #HW23 #HV3 #H destruct
+    elim (IH … HK12) -IH -HK12 #K #HL1K #HK2
+    lapply (acr_lifts … HR … HV … HLK1 … HV3) -HV
+    lapply (acr_lifts … HR … H1W2 … HLK1 … HW23) -H1W2
+    /4 width=10 by lsubc_beta, aaa_lifts, drops_skip, ex2_intro/
+  ]
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubc_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubc_lsuba.ma
new file mode 100644 (file)
index 0000000..625aed5
--- /dev/null
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lsuba.ma".
+include "basic_2/static/gcp_aaa.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************)
+
+(* Properties with lenv refinement for atomic arity assignment **************)
+
+lemma lsuba_lsubc: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
+                   ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → G ⊢ L1 ⫃[RP] L2.
+#RR #RS #RP #H1RP #H2RP #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubc_pair/
+#L1 #L2 #W #V #A #H elim (aaa_inv_cast … H) -H /3 width=4 by acr_aaa, lsubc_beta/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubc_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubc_lsubr.ma
new file mode 100644 (file)
index 0000000..ddf571d
--- /dev/null
@@ -0,0 +1,24 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lsubr.ma".
+include "basic_2/static/lsubc.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************)
+
+(* Forward lemmas with restricted refinement for local environments *********)
+
+lemma lsubc_fwd_lsubr: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → L1 ⫃ L2.
+#RP #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_pair, lsubr_beta/
+qed-.
index a7fc0d856ba32b0fa440ff5f1a17671d104d4113..4a5a696aca5db847df63cdf3e6ca39d468218e0c 100644 (file)
@@ -124,12 +124,6 @@ table {
              [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" * ] 
           }
         ]
-        [ { "generic reducibility" * } {
-             [ "lsubc ( ? ⊢ ? ⫃[?] ? )" "lsubc_drop" + "lsubc_drops" + "lsubc_lsubr" + "lsubc_lsuba" * ]        
-             [ "gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ]
-             [ "gcp" *] 
-          }
-        ]        
      }
    ]
    class "water"
@@ -166,6 +160,12 @@ table {
    ]
    class "green"
    [ { "static typing" * } {
+        [ { "generic reducibility" * } {
+             [ "lsubc ( ? ⊢ ? ⫃[?] ? )" "lsubc_drop" + "lsubc_drops" + "lsubc_lsubr" + "lsubc_lsuba" * ]        
+             [ "gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ]
+             [ "gcp" *] 
+          }
+        ]
         [ { "atomic arity assignment" * } {
              [ "lsuba ( ? ⊢ ? ⫃⁝ ? )" "lsuba_drops" + "lsuba_lsubr" + "lsuba_aaa" + "lsuba_lsuba" * ]
              [ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_lfdeq" + "aaa_aaa" * ]