(* Properties with context-sensitive parallel eta-conversion for terms ******)
-lemma cpce_total_cnv (h) (a) (G) (L):
+axiom cpce_total_cnv (h) (a) (G) (L):
∀T1. ⦃G,L⦄ ⊢ T1 ![h,a] → ∃T2. ⦃G,L⦄ ⊢ T1 ⬌η[h] T2.
+(*
#h #a #G #L #T1 #HT1
lapply (cnv_fwd_csx … HT1) #H
generalize in match HT1; -HT1
/3 width=2 by cpce_flat, ex_intro/
]
qed-.
+*)
(* *)
(**************************************************************************)
-include "basic_2/dynamic/cnv_cpce.ma".
+include "basic_2/rt_transition/lpr_drops.ma".
+include "basic_2/rt_computation/cpms_lpr.ma".
+include "basic_2/rt_computation/fpbg_fqup.ma".
+include "basic_2/rt_conversion/cpce_drops.ma".
+include "basic_2/rt_conversion/lpce_drops.ma".
+include "basic_2/dynamic/cnv_drops.ma".
(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
definition IH (h) (a): relation3 genv lenv term ≝
λG,L0,T0. ⦃G,L0⦄ ⊢ T0 ![h,a] →
∀n,T1. ⦃G,L0⦄ ⊢ T0 ➡[n,h] T1 → ∀T2. ⦃G,L0⦄ ⊢ T0 ⬌η[h] T2 →
- ∀L1. ⦃G,L0⦄ ⊢ ➡[h] L1 →
- ∃∃T. ⦃G,L1⦄ ⊢ T1 ⬌η[h] T & ⦃G,L0⦄ ⊢ T2 ➡[n,h] T.
+ ∀L1. ⦃G,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L0⦄ ⊢ ⬌η[h] L2 →
+ ∃∃T. ⦃G,L1⦄ ⊢ T1 ⬌η[h] T & ⦃G,L2⦄ ⊢ T2 ➡[n,h] T.
+
+(* Properties with eta-conversion for full local environments ***************)
lemma pippo_aux (h) (a) (G0) (L0) (T0):
(∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH h a G L T) →
IH h a G0 L0 T0.
#h #a #G0 #L0 * *
-[ #s #_ #_ #n #X1 #HX1 #X2 #HX2 #L1 #HL01
+[ #s #_ #_ #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
elim (cpm_inv_sort1 … HX1) -HX1 #H #Hn destruct
lapply (cpce_inv_sort_sn … HX2) -HX2 #H destruct
/3 width=3 by cpce_sort, cpm_sort, ex2_intro/
-| #i #IH #Hi #n #X1 #HX1 #X2 #HX2 #L1 #HL01
+| #i #IH #Hi #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
elim (cnv_inv_lref_drops … Hi) -Hi #I #K0 #W0 #HLK0 #HW0
elim (lpr_drops_conf … HLK0 … HL01) [| // ] #Y1 #H1 #HLK1
- elim (lex_inv_pair_sn … H1) -H1 #K1 #W1 #HK01 #HW01 #H destruct
- elim (cpce_inv_lref_sn_drops_bind … HX2 … HLK0) -HX2 *
- [ #HI #H destruct
- elim (cpm_inv_lref1_drops … HX1) -HX1 *
- [ #H1 #H2 destruct -HW0 -HLK0 -IH
+ elim (lpr_inv_pair_sn … H1) -H1 #K1 #W1 #HK01 #HW01 #H destruct
+ elim (lpce_drops_conf … HLK0 … HL02) [| // ] #Y2 #H2 #HLK2
+ elim (lpce_inv_pair_sn … H2) -H2 #K2 #W2 #HK02 #HW02 #H destruct
+ elim (cpm_inv_lref1_drops … HX1) -HX1 *
+ [ #H1 #H2 destruct
+ elim (cpce_inv_lref_sn_drops_pair … HX2 … HLK0) -HX2 *
+ [ #H1 #H2 destruct -L0 -K0 -W0
+ /3 width=3 by cpce_ldef_drops, ex2_intro/
+ | #H1 #HW #H2 destruct -L0 -W2 -HW0 -HK02
@(ex2_intro … (#i)) [| // ]
- @cpce_zero_drops #n #p #Y1 #X1 #V1 #U1 #HLY1 #HWU1
- lapply (drops_mono … HLY1 … HLK1) -L1 #H2 destruct
- /4 width=12 by lpr_cpms_trans, cpms_step_sn/
- | #Y0 #W0 #W1 #HLY0 #HW01 #HWX1 -HI -HW0 -IH
- lapply (drops_mono … HLY0 … HLK0) -HLY0 #H destruct
- @(ex2_intro … X1) [| /2 width=6 by cpm_delta_drops/ ]
+ @(cpce_ldec_drops … HLK1) -HLK1 #n #p #V0 #U0 #HWU0
+ /4 width=10 by lpr_cpms_trans, cpms_step_sn/
+ | #n #p #W01 #W02 #V0 #V01 #V02 #U0 #H1 #HWU0 #HW001 #HW012 #HV001 #HV012 #H2 destruct
+ ]
+ | lapply (drops_isuni_fwd_drop2 … HLK1) [ // ] -W1 #HLK1
+ #Y0 #X0 #W1 #HLY0 #HW01 #HWX1 -HL01 -HL02
+ lapply (drops_mono … HLY0 … HLK0) -HLY0 #H destruct
+ lapply (cpce_inv_lref_sn_drops_ldef … HX2 … HLK0) -HX2 #H destruct
+ elim (IH … HW0 … HW01 … HW02 … HK01 … HK02)
+ [| /3 width=2 by fqup_fpbg, fqup_lref/ ] -L0 -K0 #W #HW1 #HW2
+ elim (lifts_total W (𝐔❴↑i❵)) #V #HWV
+ /3 width=9 by cpce_lifts_bi, cpm_delta_drops, ex2_intro/
+ | lapply (drops_isuni_fwd_drop2 … HLK1) [ // ] -W1 #HLK1
+ #m #Y0 #X0 #W1 #HLY0 #HW01 #HWX1 #H destruct -HL01 -HL02
+ lapply (drops_mono … HLY0 … HLK0) -HLY0 #H destruct
+ elim (cpce_inv_lref_sn_drops_ldec … HX2 … HLK0) -HX2 *
+ [ #_ #H destruct
+ elim (IH … HW0 … HW01 … HW02 … HK01 … HK02)
+ [| /3 width=2 by fqup_fpbg, fqup_lref/ ] -L0 -K0 #W #HW1 #HW2
+ elim (lifts_total W (𝐔❴↑i❵)) #V #HWV
+ /3 width=9 by cpce_lifts_bi, cpm_ell_drops, ex2_intro/
+ | lapply (drops_isuni_fwd_drop2 … HLK2) [ // ] -W2 #HLK2
+ #n #p #W01 #W02 #V0 #V01 #V02 #U0 #_ #HW001 #HW012 #_ #_ #H destruct -V0 -V01 -U0
+ elim (IH … HW0 … HW01 … HW001 … HK01 … HK02)
+ [| /3 width=2 by fqup_fpbg, fqup_lref/ ] -L0 -K0 #W #HW1 #HW2
+ elim (lifts_total W (𝐔❴↑i❵)) #V #HWV
+ /4 width=11 by cpce_lifts_bi, cpm_lifts_bi, cpm_ee, ex2_intro/
+ ]
+ ]
+| #l #_ #_ #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02
+ elim (cpm_inv_gref1 … HX1) -HX1 #H1 #H2 destruct
+ lapply (cpce_inv_gref_sn … HX2) -HX2 #H destruct
+ /3 width=3 by cpce_gref, cpr_refl, ex2_intro/
(*
lemma cpce_inv_eta_drops (h) (n) (G) (L) (i):
(* *)
(**************************************************************************)
-include "ground_2/xoa/ex_5_7.ma".
include "basic_2/notation/relations/pconveta_5.ma".
include "basic_2/rt_computation/cpms.ma".
inductive cpce (h): relation4 genv lenv term term ≝
| cpce_sort: ∀G,L,s. cpce h G L (⋆s) (⋆s)
| cpce_atom: ∀G,i. cpce h G (⋆) (#i) (#i)
-| cpce_zero: ∀G,K,I. (∀n,p,W,V,U. I = BPair Abst W → ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥) →
- cpce h G (K.ⓘ{I}) (#0) (#0)
-| cpce_eta : ∀n,p,G,K,W,V1,V2,W2,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V1.U →
- cpce h G K V1 V2 → ⇧*[1] V2 ≘ W2 → cpce h G (K.ⓛW) (#0) (+ⓛW2.ⓐ#0.#1)
+| cpce_unit: ∀I,G,K. cpce h G (K.ⓤ{I}) (#0) (#0)
+| cpce_ldef: ∀G,K,V. cpce h G (K.ⓓV) (#0) (#0)
+| cpce_ldec: ∀G,K,W. (∀n,p,V,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥) →
+ cpce h G (K.ⓛW) (#0) (#0)
+| cpce_eta : ∀n,p,G,K,W,W1,W2,V,V1,V2,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U →
+ cpce h G K W W1 → ⇧*[1] W1 ≘ W2 →
+ cpce h G K V V1 → ⇧*[1] V1 ≘ V2 →
+ cpce h G (K.ⓛW) (#0) (ⓝW2.+ⓛV2.ⓐ#0.#1)
| cpce_lref: ∀I,G,K,T,U,i. cpce h G K (#i) T →
⇧*[1] T ≘ U → cpce h G (K.ⓘ{I}) (#↑i) U
| cpce_gref: ∀G,L,l. cpce h G L (§l) (§l)
(* Basic inversion lemmas ***************************************************)
-lemma cpce_inv_sort_sn (h) (G) (L) (X2):
- ∀s. ⦃G,L⦄ ⊢ ⋆s ⬌η[h] X2 → ⋆s = X2.
-#h #G #Y #X2 #s0
+lemma cpce_inv_sort_sn (h) (G) (L) (s):
+ ∀X2. ⦃G,L⦄ ⊢ ⋆s ⬌η[h] X2 → ⋆s = X2.
+#h #G #Y #s0 #X2
@(insert_eq_0 … (⋆s0)) #X1 * -G -Y -X1 -X2
[ #G #L #s #_ //
| #G #i #_ //
-| #G #K #I #_ #_ //
-| #n #p #G #K #W #V1 #V2 #W2 #U #_ #_ #_ #H destruct
+| #I #G #K #_ //
+| #G #K #V #_ //
+| #G #K #W #_ #_ //
+| #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #_ #_ #_ #_ #_ #H destruct
| #I #G #K #T #U #i #_ #_ #H destruct
| #G #L #l #_ //
| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H destruct
]
qed-.
-lemma cpce_inv_atom_sn (h) (G) (X2):
- ∀i. ⦃G,⋆⦄ ⊢ #i ⬌η[h] X2 → #i = X2.
-#h #G #X2 #j
+lemma cpce_inv_atom_sn (h) (G) (i):
+ ∀X2. ⦃G,⋆⦄ ⊢ #i ⬌η[h] X2 → #i = X2.
+#h #G #i0 #X2
@(insert_eq_0 … LAtom) #Y
-@(insert_eq_0 … (#j)) #X1
+@(insert_eq_0 … (#i0)) #X1
* -G -Y -X1 -X2
[ #G #L #s #_ #_ //
| #G #i #_ #_ //
-| #G #K #I #_ #_ #_ //
-| #n #p #G #K #W #V1 #V2 #W2 #U #_ #_ #_ #_ #H destruct
+| #I #G #K #_ #_ //
+| #G #K #V #_ #_ //
+| #G #K #W #_ #_ #_ //
+| #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #_ #_ #_ #_ #_ #_ #H destruct
| #I #G #K #T #U #i #_ #_ #_ #H destruct
| #G #L #l #_ #_ //
| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
]
qed-.
-lemma cpce_inv_zero_sn (h) (G) (K) (X2):
- ∀I. ⦃G,K.ⓘ{I}⦄ ⊢ #0 ⬌η[h] X2 →
- ∨∨ ∧∧ ∀n,p,W,V,U. I = BPair Abst W → ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥ & #0 = X2
- | ∃∃n,p,W,V1,V2,W2,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V1.U & ⦃G,K⦄ ⊢ V1 ⬌η[h] V2
- & ⇧*[1] V2 ≘ W2 & I = BPair Abst W & +ⓛW2.ⓐ#0.#1 = X2.
-#h #G #Y0 #X2 #Z
-@(insert_eq_0 … (Y0.ⓘ{Z})) #Y
+lemma cpce_inv_unit_sn (h) (I) (G) (K):
+ ∀X2. ⦃G,K.ⓤ{I}⦄ ⊢ #0 ⬌η[h] X2 → #0 = X2.
+#h #I0 #G #K0 #X2
+@(insert_eq_0 … (K0.ⓤ{I0})) #Y
+@(insert_eq_0 … (#0)) #X1
+* -G -Y -X1 -X2
+[ #G #L #s #_ #_ //
+| #G #i #_ #_ //
+| #I #G #K #_ #_ //
+| #G #K #V #_ #_ //
+| #G #K #W #_ #_ #_ //
+| #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #_ #_ #_ #_ #_ #_ #H destruct
+| #I #G #K #T #U #i #_ #_ #H #_ destruct
+| #G #L #l #_ #_ //
+| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
+| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
+]
+qed-.
+
+lemma cpce_inv_ldef_sn (h) (G) (K) (V):
+ ∀X2. ⦃G,K.ⓓV⦄ ⊢ #0 ⬌η[h] X2 → #0 = X2.
+#h #G #K0 #V0 #X2
+@(insert_eq_0 … (K0.ⓓV0)) #Y
+@(insert_eq_0 … (#0)) #X1
+* -G -Y -X1 -X2
+[ #G #L #s #_ #_ //
+| #G #i #_ #_ //
+| #I #G #K #_ #_ //
+| #G #K #V #_ #_ //
+| #G #K #W #_ #_ #_ //
+| #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #_ #_ #_ #_ #_ #_ #H destruct
+| #I #G #K #T #U #i #_ #_ #H #_ destruct
+| #G #L #l #_ #_ //
+| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
+| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
+]
+qed-.
+
+lemma cpce_inv_ldec_sn (h) (G) (K) (W):
+ ∀X2. ⦃G,K.ⓛW⦄ ⊢ #0 ⬌η[h] X2 →
+ ∨∨ ∧∧ ∀n,p,V,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥ & #0 = X2
+ | ∃∃n,p,W1,W2,V,V1,V2,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U
+ & ⦃G,K⦄ ⊢ W ⬌η[h] W1 & ⇧*[1] W1 ≘ W2
+ & ⦃G,K⦄ ⊢ V ⬌η[h] V1 & ⇧*[1] V1 ≘ V2
+ & ⓝW2.+ⓛV2.ⓐ#0.#1 = X2.
+#h #G #K0 #W0 #X2
+@(insert_eq_0 … (K0.ⓛW0)) #Y
@(insert_eq_0 … (#0)) #X1
* -G -Y -X1 -X2
[ #G #L #s #H #_ destruct
| #G #i #_ #H destruct
-| #G #K #I #HI #_ #H destruct /4 width=7 by or_introl, conj/
-| #n #p #G #K #W #V1 #V2 #W2 #U #HWU #HV12 #HVW2 #_ #H destruct /3 width=12 by or_intror, ex5_7_intro/
+| #I #G #K #_ #H destruct
+| #G #K #V #_ #H destruct
+| #G #K #W #HW #_ #H destruct /4 width=5 by or_introl, conj/
+| #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #HWU #HW1 #HW12 #HV1 #HV12 #_ #H destruct
+ /3 width=14 by or_intror, ex6_8_intro/
| #I #G #K #T #U #i #_ #_ #H #_ destruct
| #G #L #l #H #_ destruct
| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
]
qed-.
-lemma cpce_inv_lref_sn (h) (G) (K) (X2):
- ∀I,i. ⦃G,K.ⓘ{I}⦄ ⊢ #↑i ⬌η[h] X2 →
+lemma cpce_inv_lref_sn (h) (I) (G) (K) (i):
+ ∀X2. ⦃G,K.ⓘ{I}⦄ ⊢ #↑i ⬌η[h] X2 →
∃∃T2. ⦃G,K⦄ ⊢ #i ⬌η[h] T2 & ⇧*[1] T2 ≘ X2.
-#h #G #Y0 #X2 #Z #j
-@(insert_eq_0 … (Y0.ⓘ{Z})) #Y
-@(insert_eq_0 … (#↑j)) #X1
+#h #I0 #G #K0 #i0 #X2
+@(insert_eq_0 … (K0.ⓘ{I0})) #Y
+@(insert_eq_0 … (#↑i0)) #X1
* -G -Y -X1 -X2
[ #G #L #s #H #_ destruct
| #G #i #_ #H destruct
-| #G #K #I #_ #H #_ destruct
-| #n #p #G #K #W #V1 #V2 #W2 #U #_ #_ #_ #H #_ destruct
+| #I #G #K #H #_ destruct
+| #G #K #V #H #_ destruct
+| #G #K #W #_ #H #_ destruct
+| #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #_ #_ #_ #_ #_ #H #_ destruct
| #I #G #K #T #U #i #Hi #HTU #H1 #H2 destruct /2 width=3 by ex2_intro/
| #G #L #l #H #_ destruct
| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
]
qed-.
-lemma cpce_inv_gref_sn (h) (G) (L) (X2):
- ∀l. ⦃G,L⦄ ⊢ §l ⬌η[h] X2 → §l = X2.
-#h #G #Y #X2 #k
-@(insert_eq_0 … (§k)) #X1 * -G -Y -X1 -X2
+lemma cpce_inv_gref_sn (h) (G) (L) (l):
+ ∀X2. ⦃G,L⦄ ⊢ §l ⬌η[h] X2 → §l = X2.
+#h #G #Y #l0 #X2
+@(insert_eq_0 … (§l0)) #X1 * -G -Y -X1 -X2
[ #G #L #s #_ //
| #G #i #_ //
-| #G #K #I #_ #_ //
-| #n #p #G #K #W #V1 #V2 #W2 #U #_ #_ #_ #H destruct
+| #I #G #K #_ //
+| #G #K #V #_ //
+| #G #K #W #_ #_ //
+| #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #_ #_ #_ #_ #_ #H destruct
| #I #G #K #T #U #i #_ #_ #H destruct
| #G #L #l #_ //
| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H destruct
]
qed-.
-lemma cpce_inv_bind_sn (h) (G) (K) (X2):
- ∀p,I,V1,T1. ⦃G,K⦄ ⊢ ⓑ{p,I}V1.T1 ⬌η[h] X2 →
+lemma cpce_inv_bind_sn (h) (p) (I) (G) (K) (V1) (T1):
+ ∀X2. ⦃G,K⦄ ⊢ ⓑ{p,I}V1.T1 ⬌η[h] X2 →
∃∃V2,T2. ⦃G,K⦄ ⊢ V1 ⬌η[h] V2 & ⦃G,K.ⓑ{I}V1⦄ ⊢ T1 ⬌η[h] T2 & ⓑ{p,I}V2.T2 = X2.
-#h #G #Y #X2 #q #Z #U #X
-@(insert_eq_0 … (ⓑ{q,Z}U.X)) #X1 * -G -Y -X1 -X2
+#h #p0 #I0 #G #Y #V0 #T0 #X2
+@(insert_eq_0 … (ⓑ{p0,I0}V0.T0)) #X1 * -G -Y -X1 -X2
[ #G #L #s #H destruct
| #G #i #H destruct
-| #G #K #I #_ #H destruct
-| #n #p #G #K #W #V1 #V2 #W2 #U #_ #_ #_ #H destruct
+| #I #G #K #H destruct
+| #G #K #V #H destruct
+| #G #K #W #_ #H destruct
+| #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #_ #_ #_ #_ #_ #H destruct
| #I #G #K #T #U #i #_ #_ #H destruct
| #G #L #l #H destruct
| #p #I #G #K #V1 #V2 #T1 #T2 #HV #HT #H destruct /2 width=5 by ex3_2_intro/
]
qed-.
-lemma cpce_inv_flat_sn (h) (G) (L) (X2):
- ∀I,V1,T1. ⦃G,L⦄ ⊢ ⓕ{I}V1.T1 ⬌η[h] X2 →
+lemma cpce_inv_flat_sn (h) (I) (G) (L) (V1) (T1):
+ ∀X2. ⦃G,L⦄ ⊢ ⓕ{I}V1.T1 ⬌η[h] X2 →
∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ⬌η[h] V2 & ⦃G,L⦄ ⊢ T1 ⬌η[h] T2 & ⓕ{I}V2.T2 = X2.
-#h #G #Y #X2 #Z #U #X
-@(insert_eq_0 … (ⓕ{Z}U.X)) #X1 * -G -Y -X1 -X2
+#h #I0 #G #Y #V0 #T0 #X2
+@(insert_eq_0 … (ⓕ{I0}V0.T0)) #X1 * -G -Y -X1 -X2
[ #G #L #s #H destruct
| #G #i #H destruct
-| #G #K #I #_ #H destruct
-| #n #p #G #K #W #V1 #V2 #W2 #U #_ #_ #_ #H destruct
+| #I #G #K #H destruct
+| #G #K #V #H destruct
+| #G #K #W #_ #H destruct
+| #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #_ #_ #_ #_ #_ #H destruct
| #I #G #K #T #U #i #_ #_ #H destruct
| #G #L #l #H destruct
| #p #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct
(* *)
(**************************************************************************)
+include "ground_2/xoa/ex_7_8.ma".
include "basic_2/rt_computation/cpms_drops.ma".
include "basic_2/rt_conversion/cpce.ma".
(* Advanced properties ******************************************************)
-lemma cpce_zero_drops (h) (G):
- ∀i,L. (∀n,p,K,W,V,U. ⇩*[i] L ≘ K.ⓛW → ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥) →
- ⦃G,L⦄ ⊢ #i ⬌η[h] #i.
-#h #G #i elim i -i
-[ * [ #_ // ] #L #I #Hi
- /4 width=8 by cpce_zero, drops_refl/
-| #i #IH * [ -IH #_ // ] #L #I #Hi
- /5 width=8 by cpce_lref, drops_drop/
+lemma cpce_ldef_drops (h) (G) (K) (V):
+ ∀i,L. ⇩*[i] L ≘ K.ⓓV → ⦃G,L⦄ ⊢ #i ⬌η[h] #i.
+#h #G #K #V #i elim i -i
+[ #L #HLK
+ lapply (drops_fwd_isid … HLK ?) -HLK [ // ] #H destruct
+ /2 width=1 by cpce_ldef/
+| #i #IH #L #HLK
+ elim (drops_inv_succ … HLK) -HLK #Z #Y #HYK #H destruct
+ /3 width=3 by cpce_lref/
]
qed.
-lemma cpce_eta_drops (h) (n) (G) (K):
- ∀p,W,V1,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V1.U →
- ∀V2. ⦃G,K⦄ ⊢ V1 ⬌η[h] V2 →
- ∀i,L. ⇩*[i] L ≘ K.ⓛW →
- ∀W2. ⇧*[↑i] V2 ≘ W2 → ⦃G,L⦄ ⊢ #i ⬌η[h] +ⓛW2.ⓐ#0.#↑i.
-#h #n #G #K #p #W #V1 #U #HWU #V2 #HV12 #i elim i -i
-[ #L #HLK #W2 #HVW2
- >(drops_fwd_isid … HLK) -L [| // ] /2 width=8 by cpce_eta/
-| #i #IH #L #HLK #W2 #HVW2
+lemma cpce_ldec_drops (h) (G) (K) (W):
+ (∀n,p,V,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥) →
+ ∀i,L. ⇩*[i] L ≘ K.ⓛW → ⦃G,L⦄ ⊢ #i ⬌η[h] #i.
+#h #G #K #W #HW #i elim i -i
+[ #L #HLK
+ lapply (drops_fwd_isid … HLK ?) -HLK [ // ] #H destruct
+ /3 width=5 by cpce_ldec/
+| #i #IH #L #HLK
+ elim (drops_inv_succ … HLK) -HLK #Z #Y #HYK #H destruct
+ /3 width=3 by cpce_lref/
+]
+qed.
+
+lemma cpce_eta_drops (h) (G) (K) (W):
+ ∀n,p,V,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U →
+ ∀W1. ⦃G,K⦄ ⊢ W ⬌η[h] W1 → ∀V1. ⦃G,K⦄ ⊢ V ⬌η[h] V1 →
+ ∀i,L. ⇩*[i] L ≘ K.ⓛW → ∀W2. ⇧*[↑i] W1 ≘ W2 →
+ ∀V2. ⇧*[↑i] V1 ≘ V2 → ⦃G,L⦄ ⊢ #i ⬌η[h] ⓝW2.+ⓛV2.ⓐ#0.#↑i.
+#h #G #K #W #n #p #V #U #HWU #W1 #HW1 #V1 #HV1 #i elim i -i
+[ #L #HLK #W2 #HW12 #V2 #HV12
+ lapply (drops_fwd_isid … HLK ?) -HLK [ // ] #H destruct
+ /2 width=8 by cpce_eta/
+| #i #IH #L #HLK #W2 #HW12 #V2 #HV12
elim (drops_inv_succ … HLK) -HLK #I #Y #HYK #H destruct
- elim (lifts_split_trans … HVW2 (𝐔❴↑i❵) (𝐔❴1❵)) [| // ] #X2 #HVX2 #HXW2
- /5 width=7 by cpce_lref, lifts_push_lref, lifts_bind, lifts_flat/
+ elim (lifts_split_trans … HW12 (𝐔❴↑i❵) (𝐔❴1❵)) [| // ] #XW #HXW1 #HXW2
+ elim (lifts_split_trans … HV12 (𝐔❴↑i❵) (𝐔❴1❵)) [| // ] #XV #HXV1 #HXV2
+ /6 width=9 by cpce_lref, lifts_push_lref, lifts_bind, lifts_flat/
]
qed.
(* Advanced inversion lemmas ************************************************)
-lemma cpce_inv_lref_sn_drops_bind (h) (G) (i) (L):
+axiom cpce_inv_lref_sn_drops_pair (h) (G) (i) (L):
∀X2. ⦃G,L⦄ ⊢ #i ⬌η[h] X2 →
- ∀I,K. ⇩*[i] L ≘ K.ⓘ{I} →
- ∨∨ ∧∧ ∀n,p,W,V,U. I = BPair Abst W → ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥ & #i = X2
- | ∃∃n,p,W,V1,V2,W2,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V1.U & ⦃G,K⦄ ⊢ V1 ⬌η[h] V2
- & ⇧*[↑i] V2 ≘ W2 & I = BPair Abst W & +ⓛW2.ⓐ#0.#(↑i) = X2.
+ ∀I,K,W. ⇩*[i] L ≘ K.ⓑ{I}W →
+ ∨∨ ∧∧ Abbr = I & #i = X2
+ | ∧∧ Abst = I & ∀n,p,V,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥ & #i = X2
+ | ∃∃n,p,W1,W2,V,V1,V2,U. Abst = I & ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U
+ & ⦃G,K⦄ ⊢ W ⬌η[h] W1 & ⇧*[↑i] W1 ≘ W2
+ & ⦃G,K⦄ ⊢ V ⬌η[h] V1 & ⇧*[↑i] V1 ≘ V2
+ & ⓝW2.+ⓛV2.ⓐ#0.#(↑i) = X2.
+
+axiom cpce_inv_lref_sn_drops_ldef (h) (G) (i) (L):
+ ∀X2. ⦃G,L⦄ ⊢ #i ⬌η[h] X2 →
+ ∀K,V. ⇩*[i] L ≘ K.ⓓV → #i = X2.
+
+axiom cpce_inv_lref_sn_drops_ldec (h) (G) (i) (L):
+ ∀X2. ⦃G,L⦄ ⊢ #i ⬌η[h] X2 →
+ ∀K,W. ⇩*[i] L ≘ K.ⓛW →
+ ∨∨ ∧∧ ∀n,p,V,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥ & #i = X2
+ | ∃∃n,p,W1,W2,V,V1,V2,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U
+ & ⦃G,K⦄ ⊢ W ⬌η[h] W1 & ⇧*[↑i] W1 ≘ W2
+ & ⦃G,K⦄ ⊢ V ⬌η[h] V1 & ⇧*[↑i] V1 ≘ V2
+ & ⓝW2.+ⓛV2.ⓐ#0.#(↑i) = X2.
+(*
#h #G #i elim i -i
[ #L #X2 #HX2 #I #K #HLK
lapply (drops_fwd_isid … HLK ?) -HLK [ // ] #H destruct
elim (HI … HWU) -n -p -K -X2 -V1 -V2 -W2 -U -i //
]
qed-.
-
+*)
(* Properties with uniform slicing for local environments *******************)
-lemma cpce_lifts_sn (h) (G):
+axiom cpce_lifts_sn (h) (G):
d_liftable2_sn … lifts (cpce h G).
+(*
#h #G #K #T1 #T2 #H elim H -G -K -T1 -T2
[ #G #K #s #b #f #L #HLK #X #HX
lapply (lifts_inv_sort1 … HX) -HX #H destruct
/3 width=5 by cpce_flat, lifts_flat, ex2_intro/
]
qed-.
-
+*)
lemma cpce_lifts_bi (h) (G):
d_liftable2_bi … lifts (cpce h G).
/3 width=12 by cpce_lifts_sn, d_liftable2_sn_bi, lifts_mono/ qed-.
(* Inversion lemmas with uniform slicing for local environments *************)
-lemma cpce_inv_lifts_sn (h) (G):
+axiom cpce_inv_lifts_sn (h) (G):
d_deliftable2_sn … lifts (cpce h G).
+(*
#h #G #K #T1 #T2 #H elim H -G -K -T1 -T2
[ #G #K #s #b #f #L #HLK #X #HX
lapply (lifts_inv_sort2 … HX) -HX #H destruct
/3 width=5 by cpce_flat, lifts_flat, ex2_intro/
]
qed-.
-
+*)
lemma cpce_inv_lifts_bi (h) (G):
d_deliftable2_bi … lifts (cpce h G).
/3 width=12 by cpce_inv_lifts_sn, d_deliftable2_sn_bi, 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 "static_2/relocation/drops_lex.ma".
+include "basic_2/rt_conversion/lpce.ma".
+
+(* PARALLEL ETA-CONVERSION FOR FULL LOCAL ENVIRONMENTS **********************)
+
+(* Inversion lemmas with generic slicing for local environments *************)
+
+lemma lpce_drops_conf (h) (G): dropable_sn (cpce h G).
+/2 width=3 by lex_dropable_sn/ qed-.
+
+lemma lpce_drops_trans (h) (G): dropable_dx (cpce h G).
+/2 width=3 by lex_dropable_dx/ 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_acle" + "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_cpme" + "cnv_cpmuwe" + "cnv_cpmuwe_cpme" + "cnv_eval" + "cnv_cpce" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" * ]
+ [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_acle" + "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_cpme" + "cnv_cpmuwe" + "cnv_cpmuwe_cpme" + "cnv_eval" + "cnv_cpce" + "cnv_lpce" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" * ]
}
]
}
class "blue"
[ { "rt-conversion" * } {
[ { "context-sensitive parallel eta-conversion" * } {
- [ [ "for lenvs on all entries" ] "lpce ( ⦃?,?⦄ ⊢ ⬌η[?] ? )" * ]
+ [ [ "for lenvs on all entries" ] "lpce ( ⦃?,?⦄ ⊢ ⬌η[?] ? )" "lpce_drops" * ]
[ [ "for binders" ] "cpce_ext" + "( ⦃?,?⦄ ⊢ ? ⬌η[?] ? )" * ]
[ [ "for terms" ] "cpce" + "( ⦃?,?⦄ ⊢ ? ⬌η[?] ? )" "cpce_drops" * ]
}
--- /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 (7, 8) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 , ident x7 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)"
+ non associative with precedence 20
+ for @{ 'Ex8 (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P6) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 , ident x7 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)"
+ non associative with precedence 20
+ for @{ 'Ex8 (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P6) }.
+
--- /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_7_8.ma".
+
+(* multiple existental quantifier (7, 8) *)
+
+inductive ex7_8 (A0,A1,A2,A3,A4,A5,A6,A7:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→A4→A5→A6→A7→Prop) : Prop ≝
+ | ex7_8_intro: ∀x0,x1,x2,x3,x4,x5,x6,x7. P0 x0 x1 x2 x3 x4 x5 x6 x7 → P1 x0 x1 x2 x3 x4 x5 x6 x7 → P2 x0 x1 x2 x3 x4 x5 x6 x7 → P3 x0 x1 x2 x3 x4 x5 x6 x7 → P4 x0 x1 x2 x3 x4 x5 x6 x7 → P5 x0 x1 x2 x3 x4 x5 x6 x7 → P6 x0 x1 x2 x3 x4 x5 x6 x7 → ex7_8 ? ? ? ? ? ? ? ? ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (7, 8)" 'Ex8 P0 P1 P2 P3 P4 P5 P6 = (ex7_8 ? ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6).
+
<key name="ex">1 4</key>
<key name="ex">5 1</key>
<key name="ex">5 7</key>
+ <key name="ex">7 8</key>
<key name="ex">9 3</key>
</section>
</helm_registry>
projects / helm.git / commitdiff