include "basic_2/rt_computation/cpms_aaa.ma".
include "basic_2/dynamic/cnv.ma".
-(* CONTEXT_SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
(* Forward lemmas on atomic arity assignment for terms **********************)
--- /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 "basic_2/rt_computation/cpms_cpms.ma".
+include "basic_2/rt_equivalence/cpes.ma".
+include "basic_2/dynamic/cnv.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+(* Properties with t-bound rt-equivalence for terms *************************)
+
+lemma cnv_appl_cpes (a) (h) (G) (L):
+ ∀n. (a = Ⓣ → n ≤ 1) →
+ ∀V. ⦃G, L⦄ ⊢ V ![a, h] → ∀T. ⦃G, L⦄ ⊢ T ![a, h] →
+ ∀W. ⦃G, L⦄ ⊢ V ⬌*[h,1,0] W →
+ ∀p,U. ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W.U → ⦃G, L⦄ ⊢ ⓐV.T ![a, h].
+#a #h #G #L #n #Hn #V #HV #T #HT #W *
+/4 width=11 by cnv_appl, cpms_cprs_trans, cpms_bind/
+qed.
+
+lemma cnv_cast_cpes (a) (h) (G) (L):
+ ∀U. ⦃G, L⦄ ⊢ U ![a, h] →
+ ∀T. ⦃G, L⦄ ⊢ T ![a, h] → ⦃G, L⦄ ⊢ U ⬌*[h,0,1] T → ⦃G, L⦄ ⊢ ⓝU.T ![a, h].
+#a #h #G #L #U #HU #T #HT * /2 width=3 by cnv_cast/
+qed.
+
+(* Inversion lemmas with t-bound rt-equivalence for terms *******************)
+
+lemma cnv_inv_appl_cpes (a) (h) (G) (L):
+ ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] →
+ ∃∃n,p,W,U. a = Ⓣ → n ≤ 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
+ ⦃G, L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W.U.
+#a #h #G #L #V #T #H
+elim (cnv_inv_appl … H) -H #n #p #W #U #Hn #HV #HT #HVW #HTU
+/3 width=7 by cpms_div, ex5_4_intro/
+qed-.
+
+lemma cnv_inv_cast_cpes (a) (h) (G) (L):
+ ∀U,T. ⦃G, L⦄ ⊢ ⓝU.T ![a, h] →
+ ∧∧ ⦃G, L⦄ ⊢ U ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] & ⦃G, L⦄ ⊢ U ⬌*[h,0,1] T.
+#a #h #G #L #U #T #H
+elim (cnv_inv_cast … H) -H
+/3 width=3 by cpms_div, and3_intro/
+qed-.
+
+(* Eliminators with t-bound rt-equivalence for terms ************************)
+
+lemma cnv_ind_cpes (a) (h) (Q:relation3 genv lenv term):
+ (∀G,L,s. Q G L (⋆s)) →
+ (∀I,G,K,V. ⦃G,K⦄ ⊢ V![a,h] → Q G K V → Q G (K.ⓑ{I}V) (#O)) →
+ (∀I,G,K,i. ⦃G,K⦄ ⊢ #i![a,h] → Q G K (#i) → Q G (K.ⓘ{I}) (#(↑i))) →
+ (∀p,I,G,L,V,T. ⦃G,L⦄ ⊢ V![a,h] → ⦃G,L.ⓑ{I}V⦄⊢T![a,h] →
+ Q G L V →Q G (L.ⓑ{I}V) T →Q G L (ⓑ{p,I}V.T)
+ ) →
+ (∀n,p,G,L,V,W,T,U. (a = Ⓣ → n ≤ 1) → ⦃G,L⦄ ⊢ V![a,h] → ⦃G,L⦄ ⊢ T![a,h] →
+ ⦃G,L⦄ ⊢ V ⬌*[h,1,0]W → ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W.U →
+ Q G L V → Q G L T → Q G L (ⓐV.T)
+ ) →
+ (∀G,L,U,T. ⦃G,L⦄⊢ U![a,h] → ⦃G,L⦄ ⊢ T![a,h] → ⦃G,L⦄ ⊢ U ⬌*[h,0,1] T →
+ Q G L U → Q G L T → Q G L (ⓝU.T)
+ ) →
+ ∀G,L,T. ⦃G,L⦄⊢ T![a,h] → Q G L T.
+#a #h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #G #L #T #H
+elim H -G -L -T [5,6: /3 width=7 by cpms_div/ |*: /2 width=1 by/ ]
+qed-.
include "basic_2/rt_computation/cpms_drops.ma".
include "basic_2/dynamic/cnv.ma".
-(* CONTEXT_SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
(* Advanced dproperties *****************************************************)
include "static_2/s_computation/fqus_fqup.ma".
include "basic_2/dynamic/cnv_drops.ma".
-(* CONTEXT_SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
(* Properties with supclosure ***********************************************)
-(**************************************************************************)
-(* ___ *)
-(* ||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/prednormal_3.ma".
-include "basic_2/reduction/cpr.ma".
-
-(* NORMAL TERMS FOR CONTEXT-SENSITIVE REDUCTION *****************************)
-
-definition cnr: relation3 genv lenv term ≝ λG,L. NF … (cpr G L) (eq …).
-
-interpretation
- "normality for context-sensitive reduction (term)"
- 'PRedNormal G L T = (cnr G L T).
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma cnr_inv_delta: ∀G,L,K,V,i. ⬇[i] L ≡ K.ⓓV → ⦃G, L⦄ ⊢ ➡ 𝐍⦃#i⦄ → ⊥.
-#G #L #K #V #i #HLK #H
-elim (lift_total V 0 (i+1)) #W #HVW
-lapply (H W ?) -H [ /3 width=6 by cpr_delta/ ] -HLK #H destruct
-elim (lift_inv_lref2_be … HVW) -HVW /2 width=1 by ylt_inj/
-qed-.
-
-lemma cnr_inv_abst: ∀a,G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃ⓛ{a}V.T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃V⦄ ∧ ⦃G, L.ⓛV⦄ ⊢ ➡ 𝐍⦃T⦄.
-#a #G #L #V1 #T1 #HVT1 @conj
-[ #V2 #HV2 lapply (HVT1 (ⓛ{a}V2.T1) ?) -HVT1 /2 width=2 by cpr_pair_sn/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (ⓛ{a}V1.T2) ?) -HVT1 /2 width=2 by cpr_bind/ -HT2 #H destruct //
-]
-qed-.
-
-lemma cnr_inv_abbr: ∀G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃-ⓓV.T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃V⦄ ∧ ⦃G, L.ⓓV⦄ ⊢ ➡ 𝐍⦃T⦄.
-#G #L #V1 #T1 #HVT1 @conj
-[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2 by cpr_pair_sn/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2 by cpr_bind/ -HT2 #H destruct //
-]
-qed-.
-
lemma cnr_inv_zeta: ∀G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃+ⓓV.T⦄ → ⊥.
#G #L #V #T #H elim (is_lift_dec T 0 1)
[ * #U #HTU
]
qed-.
-lemma cnr_inv_appl: ∀G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃ⓐV.T⦄ → ∧∧ ⦃G, L⦄ ⊢ ➡ 𝐍⦃V⦄ & ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄ & 𝐒⦃T⦄.
-#G #L #V1 #T1 #HVT1 @and3_intro
-[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1 by cpr_pair_sn/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1 by cpr_flat/ -HT2 #H destruct //
-| generalize in match HVT1; -HVT1 elim T1 -T1 * // #a * #W1 #U1 #_ #_ #H
- [ elim (lift_total V1 0 1) #V2 #HV12
- lapply (H (ⓓ{a}W1.ⓐV2.U1) ?) -H /3 width=3 by tpr_cpr, cpr_theta/ -HV12 #H destruct
- | lapply (H (ⓓ{a}ⓝW1.V1.U1) ?) -H /3 width=1 by tpr_cpr, cpr_beta/ #H destruct
-]
-qed-.
-
-lemma cnr_inv_eps: ∀G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃ⓝV.T⦄ → ⊥.
-#G #L #V #T #H lapply (H T ?) -H
-/2 width=4 by cpr_eps, discr_tpair_xy_y/
-qed-.
-
-(* Basic properties *********************************************************)
-
-(* Basic_1: was: nf2_sort *)
-lemma cnr_sort: ∀G,L,s. ⦃G, L⦄ ⊢ ➡ 𝐍⦃⋆s⦄.
-#G #L #s #X #H
->(cpr_inv_sort1 … H) //
-qed.
-
lemma cnr_lref_free: ∀G,L,i. |L| ≤ i → ⦃G, L⦄ ⊢ ➡ 𝐍⦃#i⦄.
#G #L #i #Hi #X #H elim (cpr_inv_lref1 … H) -H // *
#K #V1 #V2 #HLK lapply (drop_fwd_length_lt2 … HLK) -HLK
#H elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/
qed.
-
-(* Basic_1: was only: nf2_csort_lref *)
-lemma cnr_lref_atom: ∀G,L,i. ⬇[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃#i⦄.
-#G #L #i #HL @cnr_lref_free >(drop_fwd_length … HL) -HL //
-qed.
-
-(* Basic_1: was: nf2_abst *)
-lemma cnr_abst: ∀a,G,L,W,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃W⦄ → ⦃G, L.ⓛW⦄ ⊢ ➡ 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃ⓛ{a}W.T⦄.
-#a #G #L #W #T #HW #HT #X #H
-elim (cpr_inv_abst1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
->(HW … HW0) -W0 >(HT … HT0) -T0 //
-qed.
-
-(* Basic_1: was only: nf2_appl_lref *)
-lemma cnr_appl_simple: ∀G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃V⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄ → 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃ⓐV.T⦄.
-#G #L #V #T #HV #HT #HS #X #H
-elim (cpr_inv_appl1_simple … H) -H // #V0 #T0 #HV0 #HT0 #H destruct
->(HV … HV0) -V0 >(HT … HT0) -T0 //
-qed.
-
-(* Basic_1: was: nf2_dec *)
-axiom cnr_dec: ∀G,L,T1. ⦃G, L⦄ ⊢ ➡ 𝐍⦃T1⦄ ∨
- ∃∃T2. ⦃G, L⦄ ⊢ T1 ➡ T2 & (T1 = T2 → ⊥).
-
-(* Basic_1: removed theorems 1: nf2_abst_shift *)
+++ /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 "basic_2/reduction/cpr_lift.ma".
-include "basic_2/reduction/cnr.ma".
-
-(* NORMAL TERMS FOR CONTEXT-SENSITIVE REDUCTION *****************************)
-
-(* Advanced properties ******************************************************)
-
-(* Basic_1: was: nf2_lref_abst *)
-lemma cnr_lref_abst: ∀G,L,K,V,i. ⬇[i] L ≡ K. ⓛV → ⦃G, L⦄ ⊢ ➡ 𝐍⦃#i⦄.
-#G #L #K #V #i #HLK #X #H
-elim (cpr_inv_lref1 … H) -H // *
-#K0 #V1 #V2 #HLK0 #_ #_
-lapply (drop_mono … HLK … HLK0) -L #H destruct
-qed.
-
-(* Relocation properties ****************************************************)
-
-(* Basic_1: was: nf2_lift *)
-lemma cnr_lift: ∀G,L0,L,T,T0,c,l,k. ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄ →
- ⬇[c, l, k] L0 ≡ L → ⬆[l, k] T ≡ T0 → ⦃G, L0⦄ ⊢ ➡ 𝐍⦃T0⦄.
-#G #L0 #L #T #T0 #c #l #k #HLT #HL0 #HT0 #X #H
-elim (cpr_inv_lift1 … H … HL0 … HT0) -L0 #T1 #HT10 #HT1
-<(HLT … HT1) in HT0; -L #HT0
->(lift_mono … HT10 … HT0) -T1 -X //
-qed.
-
-(* Note: this was missing in basic_1 *)
-lemma cnr_inv_lift: ∀G,L0,L,T,T0,c,l,k. ⦃G, L0⦄ ⊢ ➡ 𝐍⦃T0⦄ →
- ⬇[c, l, k] L0 ≡ L → ⬆[l, k] T ≡ T0 → ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄.
-#G #L0 #L #T #T0 #c #l #k #HLT0 #HL0 #HT0 #X #H
-elim (lift_total X l k) #X0 #HX0
-lapply (cpr_lift … H … HL0 … HT0 … HX0) -L #HTX0
->(HLT0 … HTX0) in HX0; -L0 -X0 #H
->(lift_inj … H … HT0) -T0 -X -c -l -k //
-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 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ ➡ 𝐍 break ⦃ term 46 T ⦄ )"
- non associative with precedence 45
- for @{ 'PRedNormal $G $L $T }.
+++ /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 "basic_2/notation/relations/predeval_4.ma".
-include "basic_2/computation/cprs.ma".
-include "basic_2/computation/csx.ma".
-
-(* EVALUATION FOR CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS *************)
-
-definition cpre: relation4 genv lenv term term ≝
- λG,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 ∧ ⦃G, L⦄ ⊢ ➡ 𝐍⦃T2⦄.
-
-interpretation "evaluation for context-sensitive parallel reduction (term)"
- 'PRedEval G L T1 T2 = (cpre G L T1 T2).
-
-(* Basic properties *********************************************************)
-
-(* Basic_1: was just: nf2_sn3 *)
-lemma csx_cpre: ∀h,o,G,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, o] T1 → ∃T2. ⦃G, L⦄ ⊢ T1 ➡* 𝐍⦃T2⦄.
-#h #o #G #L #T1 #H @(csx_ind … H) -T1
-#T1 #_ #IHT1 elim (cnr_dec G L T1) /3 width=3 by ex_intro, conj/
-* #T #H1T1 #H2T1 elim (IHT1 … H2T1) -IHT1 -H2T1 /2 width=2 by cpr_cpx/
-#T2 * /4 width=3 by cprs_strap2, ex_intro, 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 "basic_2/computation/cprs_cprs.ma".
-include "basic_2/computation/cpre.ma".
-
-(* EVALUATION FOR CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS *************)
-
-(* Main properties *********************************************************)
-
-(* Basic_1: was: nf2_pr3_confluence *)
-theorem cpre_mono: ∀G,L,T,T1. ⦃G, L⦄ ⊢ T ➡* 𝐍⦃T1⦄ → ∀T2. ⦃G, L⦄ ⊢ T ➡* 𝐍⦃T2⦄ → T1 = T2.
-#G #L #T #T1 * #H1T1 #H2T1 #T2 * #H1T2 #H2T2
-elim (cprs_conf … H1T1 … H1T2) -T #T #HT1
->(cprs_inv_cnr1 … HT1 H2T1) -T1 #HT2
->(cprs_inv_cnr1 … HT2 H2T2) -T2 //
-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 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * 𝐍 ⦃ break term 46 T2 ⦄ )"
- non associative with precedence 45
- for @{ 'PRedEval $G $L $T1 $T2 }.
(* Basic_1: was: pr3_pr1 *)
lemma tprs_cprs: ∀G,L,T1,T2. ⦃G, ⋆⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ T1 ➡* T2.
/2 width=3 by lsubr_cprs_trans/ qed.
-
-(* Basic_1: was: nf2_pr3_unfold *)
-lemma cprs_inv_cnr1: ∀G,L,T,U. ⦃G, L⦄ ⊢ T ➡* U → ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄ → T = U.
-#G #L #T #U #H @(cprs_ind_dx … H) -T //
-#T0 #T #H1T0 #_ #IHT #H2T0
-lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1 by/
-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 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 • * ⬌ * [ break term 46 h, break term 46 o, break term 46 n1, break term 46 n2 ] break term 46 T2 )"
- non associative with precedence 45
- for @{ 'DPConvStar $h $o $n1 $n2 $G $L $T1 $T2 }.
+++ /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 "basic_2/notation/relations/dpconvstar_8.ma".
-include "basic_2/computation/scpds.ma".
-
-(* STRATIFIED DECOMPOSED PARALLEL EQUIVALENCE FOR TERMS *********************)
-
-definition scpes: ∀h. sd h → nat → nat → relation4 genv lenv term term ≝
- λh,o,d1,d2,G,L,T1,T2.
- ∃∃T. ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d1] T & ⦃G, L⦄ ⊢ T2 •*➡*[h, o, d2] T.
-
-interpretation "stratified decomposed parallel equivalence (term)"
- 'DPConvStar h o d1 d2 G L T1 T2 = (scpes h o d1 d2 G L T1 T2).
-
-(* Basic properties *********************************************************)
-
-lemma scpds_div: ∀h,o,G,L,T1,T2,T,d1,d2.
- ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d1] T → ⦃G, L⦄ ⊢ T2 •*➡*[h, o, d2] T →
- ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2.
-/2 width=3 by ex2_intro/ qed.
-
-lemma scpes_sym: ∀h,o,G,L,T1,T2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2 →
- ⦃G, L⦄ ⊢ T2 •*⬌*[h, o, d2, d1] T1.
-#h #o #G #L #T1 #T2 #L1 #d2 * /2 width=3 by scpds_div/
-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 "basic_2/computation/scpds_aaa.ma".
-include "basic_2/equivalence/scpes.ma".
-
-(* DECOMPOSED EXTENDED PARALLEL EQUIVALENCE FOR TERMS ***********************)
-
-(* Main inversion lemmas about atomic arity assignment on terms *************)
-
-theorem scpes_aaa_mono: ∀h,o,G,L,T1,T2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2 →
- ∀A1. ⦃G, L⦄ ⊢ T1 ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T2 ⁝ A2 →
- A1 = A2.
-#h #o #G #L #T1 #T2 #d1 #d2 * #T #HT1 #HT2 #A1 #HA1 #A2 #HA2
-lapply (scpds_aaa_conf … HA1 … HT1) -T1 #HA1
-lapply (scpds_aaa_conf … HA2 … HT2) -T2 #HA2
-lapply (aaa_mono … HA1 … HA2) -L -T //
-qed-.
(* Advanced properties ******************************************************)
-lemma scpes_refl: ∀h,o,G,L,T,d1,d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ T ▪[h, o] d1 →
- ⦃G, L⦄ ⊢ T •*⬌*[h, o, d2, d2] T.
-#h #o #G #L #T #d1 #d2 #Hd21 #Hd1
-elim (da_lstas … Hd1 … d2) #U #HTU #_
-/3 width=3 by scpds_div, lstas_scpds/
-qed.
-
lemma lstas_scpes_trans: ∀h,o,G,L,T1,d0,d1. ⦃G, L⦄ ⊢ T1 ▪[h, o] d0 → d1 ≤ d0 →
∀T. ⦃G, L⦄ ⊢ T1 •*[h, d1] T →
∀T2,d,d2. ⦃G, L⦄ ⊢ T •*⬌*[h,o,d,d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h,o,d1+d,d2] T2.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ⬌* [ break term 46 h, break term 46 n1, break term 46 n2 ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PConvStar $h $n1 $n2 $G $L $T1 $T2 }.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡* [ break term 46 h ] 𝐍 ⦃ break term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'PRedEval $h $G $L $T1 $T2 }.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡* [ break term 46 h, break term 46 n ] 𝐍 ⦃ break term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'PRedEval $h $n $G $L $T1 $T2 }.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ➡ [ break term 46 h ] 𝐍 ⦃ break term 46 T ⦄ )"
+ non associative with precedence 45
+ for @{ 'PRedNormal $h $G $L $T }.
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡* break term 46 L2 )"
- non associative with precedence 45
- for @{ 'PRedSnStar $G $L1 $L2 }.
--- /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 "basic_2/notation/relations/predeval_6.ma".
+include "basic_2/rt_transition/cnr.ma".
+include "basic_2/rt_computation/cpms.ma".
+
+(* EVALUATION FOR T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION ON TERMS *)
+
+(* Basic_2A1: uses: cpre *)
+definition cpme (h) (n) (G) (L): relation2 term term ≝
+ λT1,T2. ∧∧ ⦃G, L⦄ ⊢ T1 ➡*[n,h] T2 & ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃T2⦄.
+
+interpretation "evaluation for t-bound context-sensitive parallel rt-transition (term)"
+ 'PRedEval h n G L T1 T2 = (cpme h n G L T1 T2).
--- /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 "basic_2/notation/relations/predeval_5.ma".
+include "basic_2/rt_computation/cpme.ma".
+include "basic_2/rt_computation/cprs.ma".
+
+(* EVALUATION FOR CONTEXT-SENSITIVE PARALLEL R-TRANSITION ON TERMS ***********)
+
+interpretation "evaluation for context-sensitive parallel r-transition (term)"
+ 'PRedEval h G L T1 T2 = (cpme h O G L T1 T2).
--- /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 "basic_2/rt_computation/cprs_cnr.ma".
+include "basic_2/rt_computation/cprs_cprs.ma".
+include "basic_2/rt_computation/cpre.ma".
+
+(* EVALUATION FOR CONTEXT-SENSITIVE PARALLEL R-TRANSITION ON TERMS *********)
+
+(* Properties with context-sensitive parallel r-computation for terms ******)
+
+lemma cpre_cprs_conf (h) (G) (L) (T):
+ ∀T1. ⦃G,L⦄ ⊢ T ➡*[h] T1 → ∀T2. ⦃G,L⦄ ⊢ T ➡*[h] 𝐍⦃T2⦄ → ⦃G,L⦄ ⊢ T1 ➡*[h] 𝐍⦃T2⦄.
+#h #G #L #T0 #T1 #HT01 #T2 * #HT02 #HT2
+elim (cprs_conf … HT01 … HT02) -T0 #T0 #HT10 #HT20
+lapply (cprs_inv_cnr_sn … HT20 HT2) -HT20 #H destruct
+/2 width=1 by conj/
+qed-.
+
+(* Main properties *********************************************************)
+
+(* Basic_1: was: nf2_pr3_confluence *)
+theorem cpre_mono (h) (G) (L) (T):
+ ∀T1. ⦃G, L⦄ ⊢ T ➡*[h] 𝐍⦃T1⦄ → ∀T2. ⦃G, L⦄ ⊢ T ➡*[h] 𝐍⦃T2⦄ → T1 = T2.
+#h #G #L #T0 #T1 * #HT01 #HT1 #T2 * #HT02 #HT2
+elim (cprs_conf … HT01 … HT02) -T0 #T0 #HT10 #HT20
+>(cprs_inv_cnr_sn … HT10 HT1) -T1
+>(cprs_inv_cnr_sn … HT20 HT2) -T2 //
+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 "basic_2/rt_transition/cpm_cpx.ma".
+include "basic_2/rt_transition/cnr_tdeq.ma".
+include "basic_2/rt_computation/csx.ma".
+include "basic_2/rt_computation/cpre.ma".
+
+(* EVALUATION FOR CONTEXT-SENSITIVE PARALLEL R-TRANSITION ON TERMS **********)
+
+(* Properties with strong normalization for unbound rt-transition for terms *)
+
+(* Basic_1: was just: nf2_sn3 *)
+lemma csx_cpre (h) (G) (L):
+ ∀T1. ⦃G, L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ → ∃T2. ⦃G, L⦄ ⊢ T1 ➡*[h] 𝐍⦃T2⦄.
+#h #G #L #T1 #H
+@(csx_ind … H) -T1 #T1 #_ #IHT1
+elim (cnr_dec_tdeq h G L T1) [ /3 width=3 by ex_intro, conj/ ] *
+#T0 #HT10 #HnT10
+elim (IHT1 … HnT10) -IHT1 -HnT10 [| /2 width=2 by cpm_fwd_cpx/ ]
+#T2 * /4 width=3 by cprs_step_sn, ex_intro, 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 "basic_2/rt_transition/cnr.ma".
+include "basic_2/rt_computation/cprs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL R-COMPUTATION FOR TERMS ***********************)
+
+(* Inversion lemmas with normal terms for r-transition **********************)
+
+(* Basic_1: was: nf2_pr3_unfold *)
+(* Basic_2A1: was: cprs_inv_cnr1 *)
+lemma cprs_inv_cnr_sn (h) (G) (L):
+ ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h] T2 → ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃T1⦄ → T1 = T2.
+#h #G #L #T1 #T2 #H @(cprs_ind_sn … H) -T1 //
+#T1 #T0 #HT10 #_ #IH #HT1
+lapply (HT1 … HT10) -HT10 #H destruct /2 width=1 by/
+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 "basic_2/notation/relations/pconvstar_7.ma".
+include "basic_2/rt_computation/cpms.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-EQUIVALENCE FOR TERMS **************)
+
+(* Basic_2A1: uses: scpes *)
+definition cpes (h) (n1) (n2): relation4 genv lenv term term ≝
+ λG,L,T1,T2.
+ ∃∃T. ⦃G, L⦄ ⊢ T1 ➡*[n1,h] T & ⦃G, L⦄ ⊢ T2 ➡*[n2,h] T.
+
+interpretation "t-bound context-sensitive parallel rt-equivalence (term)"
+ 'PConvStar h n1 n2 G L T1 T2 = (cpes h n1 n2 G L T1 T2).
+
+(* Basic properties *********************************************************)
+
+(* Basic_2A1: uses: scpds_div *)
+lemma cpms_div (h) (n1) (n2):
+ ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡*[n1,h] T →
+ ∀T2. ⦃G, L⦄ ⊢ T2 ➡*[n2,h] T → ⦃G, L⦄ ⊢ T1 ⬌*[h,n1,n2] T2.
+/2 width=3 by ex2_intro/ qed.
+
+lemma cpes_refl (h): ∀G,L. reflexive … (cpes h 0 0 G L).
+/2 width=3 by cpms_div/ qed.
+
+(* Basic_2A1: uses: scpes_sym *)
+lemma cpes_sym (h) (n1) (n2):
+ ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h,n1,n2] T2 → ⦃G, L⦄ ⊢ T2 ⬌*[h,n2,n1] T1.
+#h #n1 #n2 #G #L #T1 #T2 * /2 width=3 by cpms_div/
+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 "basic_2/rt_computation/cpms_aaa.ma".
+include "basic_2/rt_equivalence/cpes.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-EQUIVALENCE FOR TERMS **************)
+
+(* Properties with atomic arity assignment on terms *************************)
+
+(* Basic_2A1: uses: scpes_refl *)
+lemma cpes_refl_aaa (h) (n):
+ ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ T ⬌*[h,n,n] T.
+#h #n #G #L #T #A #HA
+elim (aaa_cpms_total h … n … HA) #U #HTU
+/2 width=3 by cpms_div/
+qed.
+
+(* Main inversion lemmas with atomic arity assignment on terms **************)
+
+(* Basic_2A1: uses: scpes_aaa_mono *)
+theorem cpes_aaa_mono (h) (n1) (n2):
+ ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h,n1,n2] T2 →
+ ∀A1. ⦃G, L⦄ ⊢ T1 ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T2 ⁝ A2 → A1 = A2.
+#h #n1 #n2 #G #L #T1 #T2 * #T #HT1 #HT2 #A1 #HA1 #A2 #HA2
+lapply (cpms_aaa_conf … HA1 … HT1) -T1 #HA1
+lapply (cpms_aaa_conf … HA2 … HT2) -T2 #HA2
+lapply (aaa_mono … HA1 … HA2) -L -T //
+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 "basic_2/notation/relations/prednormal_4.ma".
+include "basic_2/rt_transition/cpr.ma".
+
+(* NORMAL TERMS FOR CONTEXT-SENSITIVE R-TRANSITION **************************)
+
+definition cnr (h) (G) (L): predicate term ≝ NF … (cpm h G L 0) (eq …).
+
+interpretation
+ "normality for context-sensitive r-transition (term)"
+ 'PRedNormal h G L T = (cnr h G L T).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma cnr_inv_abst (h) (p) (G) (L):
+ ∀V,T. ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃ⓛ{p}V.T⦄ → ∧∧ ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃V⦄ & ⦃G, L.ⓛV⦄ ⊢ ➡[h] 𝐍⦃T⦄.
+#h #p #G #L #V1 #T1 #HVT1 @conj
+[ #V2 #HV2 lapply (HVT1 (ⓛ{p}V2.T1) ?) -HVT1 /2 width=2 by cpr_pair_sn/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (ⓛ{p}V1.T2) ?) -HVT1 /2 width=2 by cpm_bind/ -HT2 #H destruct //
+]
+qed-.
+
+(* Basic_2A1: was: cnr_inv_abbr *)
+lemma cnr_inv_abbr_neg (h) (G) (L):
+ ∀V,T. ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃-ⓓV.T⦄ → ∧∧ ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃V⦄ & ⦃G, L.ⓓV⦄ ⊢ ➡[h] 𝐍⦃T⦄.
+#h #G #L #V1 #T1 #HVT1 @conj
+[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2 by cpr_pair_sn/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2 by cpm_bind/ -HT2 #H destruct //
+]
+qed-.
+
+(* Basic_2A1: was: cnr_inv_eps *)
+lemma cnr_inv_cast (h) (G) (L): ∀V,T. ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃ⓝV.T⦄ → ⊥.
+#h #G #L #V #T #H lapply (H T ?) -H
+/2 width=4 by cpm_eps, discr_tpair_xy_y/
+qed-.
+
+(* Basic properties *********************************************************)
+
+(* Basic_1: was: nf2_sort *)
+lemma cnr_sort (h) (G) (L): ∀s. ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃⋆s⦄.
+#h #G #L #s #X #H
+>(cpr_inv_sort1 … H) //
+qed.
+
+lemma cnr_gref (h) (G) (L): ∀l. ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃§l⦄.
+#h #G #L #l #X #H
+>(cpr_inv_gref1 … H) //
+qed.
+
+(* Basic_1: was: nf2_abst *)
+lemma cnr_abst (h) (p) (G) (L):
+ ∀W,T. ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃W⦄ → ⦃G, L.ⓛW⦄ ⊢ ➡[h] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃ⓛ{p}W.T⦄.
+#h #p #G #L #W #T #HW #HT #X #H
+elim (cpm_inv_abst1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
+<(HW … HW0) -W0 <(HT … HT0) -T0 //
+qed.
+
+lemma cnr_abbr_neg (h) (G) (L):
+ ∀V,T. ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃V⦄ → ⦃G, L.ⓓV⦄ ⊢ ➡[h] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃-ⓓV.T⦄.
+#h #G #L #V #T #HV #HT #X #H
+elim (cpm_inv_abbr1 … H) -H *
+[ #V0 #T0 #HV0 #HT0 #H destruct
+ <(HV … HV0) -V0 <(HT … HT0) -T0 //
+| #T0 #_ #_ #H destruct
+]
+qed.
+
+
+(* Basic_1: removed theorems 1: nf2_abst_shift *)
--- /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 "basic_2/rt_transition/cpr_drops.ma".
+include "basic_2/rt_transition/cnr.ma".
+
+(* NORMAL TERMS FOR CONTEXT-SENSITIVE R-TRANSITION **************************)
+
+(* Advanced properties ******************************************************)
+
+(* Basic_1: was only: nf2_csort_lref *)
+lemma cnr_lref_atom (h) (b) (G) (L):
+ ∀i. ⬇*[b,𝐔❴i❵] L ≘ ⋆ → ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃#i⦄.
+#h #b #G #L #i #Hi #X #H
+elim (cpr_inv_lref1_drops … H) -H // * #K #V1 #V2 #HLK
+lapply (drops_gen b … HLK) -HLK #HLK
+lapply (drops_mono … Hi … HLK) -L #H destruct
+qed.
+
+(* Basic_1: was: nf2_lref_abst *)
+lemma cnr_lref_abst (h) (G) (L):
+ ∀K,V,i. ⬇*[i] L ≘ K.ⓛV → ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃#i⦄.
+#h #G #L #K #V #i #HLK #X #H
+elim (cpr_inv_lref1_drops … H) -H // *
+#K0 #V1 #V2 #HLK0 #_ #_
+lapply (drops_mono … HLK … HLK0) -L #H destruct
+qed.
+
+lemma cnr_lref_unit (h) (I) (G) (L):
+ ∀K,i. ⬇*[i] L ≘ K.ⓤ{I} → ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃#i⦄.
+#h #I #G #L #K #i #HLK #X #H
+elim (cpr_inv_lref1_drops … H) -H // *
+#K0 #V1 #V2 #HLK0 #_ #_
+lapply (drops_mono … HLK … HLK0) -L #H destruct
+qed.
+
+(* Properties with generic relocation ***************************************)
+
+(* Basic_1: was: nf2_lift *)
+(* Basic_2A1: uses: cnr_lift *)
+lemma cnr_lifts (h) (G): d_liftable1 … (cnr h G).
+#h #G #K #T #HT #b #f #L #HLK #U #HTU #U0 #H
+elim (cpm_inv_lifts_sn … H … HLK … HTU) -b -L #T0 #HTU0 #HT0
+lapply (HT … HT0) -G -K #H destruct /2 width=4 by lifts_mono/
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+(* Basic_2A1: was: cnr_inv_delta *)
+lemma cnr_inv_lref_abbr (h) (G) (L):
+ ∀K,V,i. ⬇*[i] L ≘ K.ⓓV → ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃#i⦄ → ⊥.
+#h #G #L #K #V #i #HLK #H
+elim (lifts_total V 𝐔❴↑i❵) #W #HVW
+lapply (H W ?) -H [ /3 width=6 by cpm_delta_drops/ ] -HLK #H destruct
+elim (lifts_inv_lref2_uni_lt … HVW) -HVW //
+qed-.
+
+(* Inversion lemmas with generic relocation *********************************)
+
+(* Note: this was missing in Basic_1 *)
+(* Basic_2A1: uses: cnr_inv_lift *)
+lemma cnr_inv_lifts (h) (G): d_deliftable1 … (cnr h G).
+#h #G #L #U #HU #b #f #K #HLK #T #HTU #T0 #H
+elim (cpm_lifts_sn … H … HLK … HTU) -b -K #U0 #HTU0 #HU0
+lapply (HU … HU0) -G -L #H destruct /2 width=4 by lifts_inj/
+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 "basic_2/rt_transition/cpm_simple.ma".
+include "basic_2/rt_transition/cnr.ma".
+
+(* NORMAL TERMS FOR CONTEXT-SENSITIVE R-TRANSITION **************************)
+
+(* Inversion lemmas with simple terms ***************************************)
+
+lemma cnr_inv_appl (h) (G) (L):
+ ∀V,T. ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃ⓐV.T⦄ → ∧∧ ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃V⦄ & ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃T⦄ & 𝐒⦃T⦄.
+#h #G #L #V1 #T1 #HVT1 @and3_intro
+[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1 by cpr_pair_sn/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1 by cpr_flat/ -HT2 #H destruct //
+| generalize in match HVT1; -HVT1 elim T1 -T1 * // #a * #W1 #U1 #_ #_ #H
+ [ elim (lifts_total V1 𝐔❴1❵) #V2 #HV12
+ lapply (H (ⓓ{a}W1.ⓐV2.U1) ?) -H /2 width=3 by cpm_theta/ -HV12 #H destruct
+ | lapply (H (ⓓ{a}ⓝW1.V1.U1) ?) -H /2 width=1 by cpm_beta/ #H destruct
+ ]
+]
+qed-.
+
+(* Properties with simple terms *********************************************)
+
+(* Basic_1: was only: nf2_appl_lref *)
+lemma cnr_appl_simple (h) (G) (L):
+ ∀V,T. ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃V⦄ → ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃T⦄ → 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃ⓐV.T⦄.
+#h #G #L #V #T #HV #HT #HS #X #H
+elim (cpm_inv_appl1_simple … H) -H // #V0 #T0 #HV0 #HT0 #H destruct
+<(HV … HV0) -V0 <(HT … HT0) -T0 //
+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/relocation/lifts_tdeq.ma".
+include "basic_2/rt_transition/cpr_drops_basic.ma".
+include "basic_2/rt_transition/cnr_simple.ma".
+include "basic_2/rt_transition/cnr_drops.ma".
+
+(* NORMAL TERMS FOR CONTEXT-SENSITIVE R-TRANSITION **************************)
+
+(* Properties with context-free sort-irrelevant equivalence for terms *******)
+
+(* Basic_1: was: nf2_dec *)
+(* Basic_2A1: uses: cnr_dec *)
+lemma cnr_dec_tdeq (h) (G) (L):
+ ∀T1. ∨∨ ⦃G, L⦄ ⊢ ➡[h] 𝐍⦃T1⦄
+ | ∃∃T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 & (T1 ≛ T2 → ⊥).
+#h #G #L #T1
+@(fqup_wf_ind_eq (Ⓣ) … G L T1) -G -L -T1 #G0 #L0 #T0 #IH #G #L * *
+[ #s #HG #HL #HT destruct -IH
+ /3 width=4 by cnr_sort, or_introl/
+| #i #HG #HL #HT destruct -IH
+ elim (drops_F_uni L i)
+ [ /3 width=6 by cnr_lref_atom, or_introl/
+ | * * [ #I | * #V ] #K #HLK
+ [ /3 width=7 by cnr_lref_unit, or_introl/
+ | elim (lifts_total V 𝐔❴↑i❵) #W #HVW
+ @or_intror @(ex2_intro … W) [ /2 width=6 by cpm_delta_drops/ ] #H
+ lapply (tdeq_inv_lref1 … H) -H #H destruct
+ /2 width=5 by lifts_inv_lref2_uni_lt/
+ | /3 width=7 by cnr_lref_abst, or_introl/
+ ]
+ ]
+| #l #HG #HL #HT destruct -IH
+ /3 width=4 by cnr_gref, or_introl/
+| #p * [ cases p ] #V1 #T1 #HG #HL #HT destruct
+ [ elim (cpr_subst h G (L.ⓓV1) T1 0 L V1) [| /2 width=1 by drops_refl/ ] #T2 #X2 #HT12 #HXT2 -IH
+ elim (tdeq_dec T1 T2) [ -HT12 #HT12 | #HnT12 ]
+ [ elim (tdeq_inv_lifts_dx … HT12 … HXT2) -T2 #X1 #HXT1 #_ -X2
+ @or_intror @(ex2_intro … X1) [ /2 width=3 by cpm_zeta/ ] #H
+ /2 width=7 by tdeq_lifts_inv_pair_sn/
+ | @or_intror @(ex2_intro … (+ⓓV1.T2)) [ /2 width=1 by cpm_bind/ ] #H
+ elim (tdeq_inv_pair … H) -H /2 width=1 by/
+ ]
+ | elim (IH G L V1) [ elim (IH G (L.ⓓV1) T1) [| * | // ] | * | // ] -IH
+ [ #HT1 #HV1 /3 width=6 by cnr_abbr_neg, or_introl/
+ | #T2 #HT12 #HnT12 #_
+ @or_intror @(ex2_intro … (-ⓓV1.T2)) [ /2 width=1 by cpm_bind/ ] #H
+ elim (tdeq_inv_pair … H) -H /2 width=1 by/
+ | #V2 #HV12 #HnV12
+ @or_intror @(ex2_intro … (-ⓓV2.T1)) [ /2 width=1 by cpr_pair_sn/ ] #H
+ elim (tdeq_inv_pair … H) -H /2 width=1 by/
+ ]
+ | elim (IH G L V1) [ elim (IH G (L.ⓛV1) T1) [| * | // ] | * | // ] -IH
+ [ #HT1 #HV1 /3 width=6 by cnr_abst, or_introl/
+ | #T2 #HT12 #HnT12 #_
+ @or_intror @(ex2_intro … (ⓛ{p}V1.T2)) [ /2 width=1 by cpm_bind/ ] #H
+ elim (tdeq_inv_pair … H) -H /2 width=1 by/
+ | #V2 #HV12 #HnV12
+ @or_intror @(ex2_intro … (ⓛ{p}V2.T1)) [ /2 width=1 by cpr_pair_sn/ ] #H
+ elim (tdeq_inv_pair … H) -H /2 width=1 by/
+ ]
+ ]
+| * #V1 #T1 #HG #HL #HT destruct [| -IH ]
+ [ elim (IH G L V1) [ elim (IH G L T1) [| * | // ] | * | // ] -IH
+ [ #HT1 #HV1
+ elim (simple_dec_ex T1) [| * #p * #W1 #U1 #H destruct ]
+ [ /3 width=6 by cnr_appl_simple, or_introl/
+ | elim (lifts_total V1 𝐔❴1❵) #X1 #HVX1
+ @or_intror @(ex2_intro … (ⓓ{p}W1.ⓐX1.U1)) [ /2 width=3 by cpm_theta/ ] #H
+ elim (tdeq_inv_pair … H) -H #H destruct
+ | @or_intror @(ex2_intro … (ⓓ{p}ⓝW1.V1.U1)) [ /2 width=1 by cpm_beta/ ] #H
+ elim (tdeq_inv_pair … H) -H #H destruct
+ ]
+ | #T2 #HT12 #HnT12 #_
+ @or_intror @(ex2_intro … (ⓐV1.T2)) [ /2 width=1 by cpm_appl/ ] #H
+ elim (tdeq_inv_pair … H) -H /2 width=1 by/
+ | #V2 #HV12 #HnV12
+ @or_intror @(ex2_intro … (ⓐV2.T1)) [ /2 width=1 by cpr_pair_sn/ ] #H
+ elim (tdeq_inv_pair … H) -H /2 width=1 by/
+ ]
+ | @or_intror @(ex2_intro … T1) [ /2 width=1 by cpm_eps/ ] #H
+ /2 width=4 by tdeq_inv_pair_xy_y/
+ ]
+]
+qed-.
]
[ { "context-sensitive native validity" * } {
[ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" + "lsubv_lsubv" * ]
- [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" + "( ⦃?,?⦄ ⊢ ? ![?] )" + "( ⦃?,?⦄ ⊢ ? !*[?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" * ]
+ [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" + "( ⦃?,?⦄ ⊢ ? ![?] )" + "( ⦃?,?⦄ ⊢ ? !*[?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" * ]
}
]
}
[ [ "for terms" ] "cpcs ( ⦃?,?⦄ ⊢ ? ⬌*[?] ? )" "cpcs_drops" + "cpcs_lsubr" + "cpcs_aaa" + "cpcs_cprs" + "cpcs_lprs" + "cpcs_cpc" + "cpcs_cpcs" * ]
}
]
+ [ { "t-bound context-sensitive parallel rt-equivalence" * } {
+ [ [ "for terms" ] "cpes ( ⦃?,?⦄ ⊢ ? ⬌*[?,?,?] ? )" "cpes_aaa" * ]
+ }
+ ]
}
]
class "blue"
class "sky"
[ { "rt-computation" * } {
[ { "context-sensitive parallel r-computation" * } {
+ [ [ "evaluation for terms" ] "cpre ( ⦃?,?⦄ ⊢ ? ➡*[?] 𝐍⦃?⦄ )" "cpre_cpx" + "cpre_cpre" * ]
[ [ "for lenvs on all entries" ] "lprs ( ⦃?,?⦄ ⊢ ➡*[?] ? )" "lprs_tc" + "lprs_ctc" + "lprs_length" + "lprs_drops" + "lprs_aaa" + "lprs_lpr" + "lprs_lpxs" + "lprs_cpms" + "lprs_cprs" + "lprs_lprs" * ]
[ [ "for binders" ] "cprs_ext" + "( ⦃?,?⦄ ⊢ ? ➡*[?] ?)" * ]
- [ [ "for terms" ] "cprs" + "( ⦃?,?⦄ ⊢ ? ➡*[?] ?)" "cprs_ctc" + "cprs_drops" + "cprs_cpr" + "cprs_lpr" + "cprs_cprs" * ]
+ [ [ "for terms" ] "cprs" + "( ⦃?,?⦄ ⊢ ? ➡*[?] ?)" "cprs_ctc" + "cprs_drops" + "cprs_cpr" + "cprs_lpr" + "cprs_cnr" + "cprs_cprs" * ]
}
]
[ { "t-bound context-sensitive parallel rt-computation" * } {
+ [ [ "evaluation for terms" ] "cpme ( ⦃?,?⦄ ⊢ ? ➡*[?,?] 𝐍⦃?⦄ )" * ]
[ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpms_drops" + "cpms_lsubr" + "cpms_rdeq" + "cpms_aaa" + "cpms_cwhx" + "cpms_lpr" + "cpms_cpxs" + "cpms_fpbs" + "cpms_fpbg" + "cpms_cpms" * ]
}
]
}
]
[ { "context-sensitive parallel r-transition" * } {
+ [ [ "normal form for terms" ] "cnr ( ⦃?,?⦄ ⊢ ➡[?] 𝐍⦃?⦄ )" "cnr_simple" + "cnr_tdeq" + "cnr_drops" * ]
[ [ "for lenvs on all entries" ] "lpr" + "( ⦃?,?⦄ ⊢ ➡[?] ? )" "lpr_length" + "lpr_drops" + "lpr_fquq" + "lpr_aaa" + "lpr_lpx" + "lpr_lpr" * ]
[ [ "for binders" ] "cpr_ext" + "( ⦃?,?⦄ ⊢ ? ➡[?] ? )" * ]
[ [ "for terms" ] "cpr" + "( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" + "cpr_drops_basic" + "cpr_tdeq" + "cpr_cpr" * ]
]
[ [ "" ] "shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )" * ]
[ { "decomposed rt-equivalence" * } {
- [ [ "" ] "scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )" "scpes_aaa" + "scpes_cpcs" + "scpes_scpes" * ]
+ "scpes_cpcs" + "scpes_scpes"
}
]
[ [ "for lenvs on referred entries" ] "rpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "rpxs_length" + "rpxs_drops" + "rpxs_fqup" + "rpxs_rdeq" + "rpxs_fdeq" + "rpxs_aaa" + "rpxs_cpxs" + "rpxs_lpxs" + "rpxs_rpxs" * ]
[ [ "" ] "cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )" * ]
}
]
- [ { "evaluation for context-sensitive reduction" * } {
- [ [ "" ] "cpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )" "cpre_cpre" * ]
- }
- ]
[ { "normal forms for context-sensitive rt-reduction" * } {
[ [ "" ] "cnx_crx" + "cnx_cix" * ]
}
}
]
[ { "normal forms for context-sensitive reduction" * } {
- [ [ "" ] "cnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )" "cnr_lift" + "cnr_crr" + "cnr_cir" * ]
+ "cnr_crr" + "cnr_cir"
}
]
[ { "irreducible forms for context-sensitive reduction" * } {
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* This file was generated by xoa.native: do not edit *********************)
+
+(* multiple existental quantifier (1, 4) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0)"
+ non associative with precedence 20
+ for @{ 'Ex4 (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0)"
+ non associative with precedence 20
+ for @{ 'Ex4 (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) }.
+
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* This file was generated by xoa.native: do not edit *********************)
+
+include "basics/pts.ma".
+
+include "ground_2/notation/xoa/ex_1_4.ma".
+
+(* multiple existental quantifier (1, 4) *)
+
+inductive ex1_4 (A0,A1,A2,A3:Type[0]) (P0:A0→A1→A2→A3→Prop) : Prop ≝
+ | ex1_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → ex1_4 ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (1, 4)" 'Ex4 P0 = (ex1_4 ? ? ? ? P0).
+
include "ground_2/xoa/xoa.ma".
-(* Properties with multiple existental quantifier (5, 1) ********************)
+(* Properties with multiple existental quantifier (4, 1) ********************)
lemma ex4_commute (A0) (P0,P1,P2,P3:A0→Prop):
(∃∃x0. P0 x0 & P1 x0 & P2 x0 & P3 x0) → ∃∃x0. P2 x0 & P3 x0 & P0 x0 & P1 x0.
<key name="objects">ground_2/xoa</key>
<key name="notations">ground_2/notation/xoa</key>
<key name="include">basics/pts.ma</key>
+ <key name="ex">1 4</key>
<key name="ex">5 1</key>
<key name="ex">5 7</key>
<key name="ex">9 3</key>
(* *)
(**************************************************************************)
+include "ground_2/xoa/ex_1_4.ma".
include "static_2/notation/relations/simple_1.ma".
include "static_2/syntax/term.ma".
* /2 width=2 by ex_intro/
#p #I #V #T #H elim (simple_inv_bind … H)
qed-.
+
+(* Basic properties *********************************************************)
+
+lemma simple_dec_ex (X): ∨∨ 𝐒⦃X⦄ | ∃∃p,I,T,U. X = ⓑ{p,I}T.U.
+* [ /2 width=1 by simple_atom, or_introl/ ]
+* [| /2 width=1 by simple_flat, or_introl/ ]
+/3 width=5 by ex1_4_intro, or_intror/
+qed-.
projects / helm.git / commitdiff