(* 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-.
(* 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.
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/
]
(* 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.
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-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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-.
]
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 *)
(* 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 *)
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
(* 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).
{ 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
(* 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/
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
]
]
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-.
]
[ { "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" * } {
projects / helm.git / commitdiff