--- /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/cpue_csx.ma".
+include "basic_2/rt_conversion/cpce_drops.ma".
+include "basic_2/dynamic/cnv_cpue.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+(* Properties with context-sensitive parallel eta-conversion for terms ******)
+
+lemma cpce_total_cnv (a) (h) (G) (L):
+ ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → ∃T2. ⦃G,L⦄ ⊢ T1 ⬌η[h] T2.
+#a #h #G #L #T1 #HT1
+lapply (cnv_fwd_csx … HT1) #H
+generalize in match HT1; -HT1
+@(csx_ind_fpbg … H) -G -L -T1
+#G #L * *
+[ #s #_ #_ /2 width=2 by cpce_sort, ex_intro/
+| #i #H1i #IH #H2i
+ elim (drops_ldec_dec L i) [ * #K #W #HLK | -H1i -IH #HnX ]
+ [ lapply (cnv_inv_lref_pair … H2i … HLK) -H2i #H2W
+ lapply (csx_inv_lref_pair … HLK H1i) -H1i #H1W
+ elim (cpue_total_csx … H1W) -H1W #X
+ elim (abst_dec X) [ * | -IH ]
+ [ #p #V1 #U #H destruct * #n #HWU #_
+ elim (IH G K V1) -IH
+ [ #V2 #HV12
+ elim (lifts_total V2 (𝐔❴↑i❵)) #W2 #HVW2
+ /3 width=12 by cpce_eta_drops, ex_intro/
+ | /3 width=6 by cnv_cpms_trans, cnv_fwd_pair_sn/
+ | /4 width=6 by fqup_cpms_fwd_fpbg, fpbg_fqu_trans, fqup_lref/
+ ]
+ | #HnX #HWX
+ @(ex_intro … (#i))
+ @cpce_zero_drops #n0 #p #K0 #W0 #V0 #U0 #HLK0 #HWU0
+ lapply (drops_mono … HLK0 … HLK) -i -L #H destruct
+ elim (cnv_cpue_cpms_conf … H2W … HWU0 … HWX) -n0 -W #X0 * #n0 #HUX0 #_ #HX0
+ elim (cpms_inv_abst_sn … HUX0) -HUX0 #V1 #U1 #_ #_ #H destruct -n0 -K -V0 -U0
+ elim (tueq_inv_bind2 … HX0) -HX0 #U0 #_ #H destruct -U1
+ /2 width=4 by/
+ ]
+ | /5 width=3 by cpce_zero_drops, ex1_2_intro, ex_intro/
+ ]
+| #l #_ #_ /2 width=2 by cpce_gref, ex_intro/
+| #p #I #V1 #T1 #_ #IH #H
+ elim (cnv_inv_bind … H) -H #HV1 #HT1
+ elim (IH … HV1) [| /3 width=1 by fpb_fpbg, fpb_fqu, fqu_pair_sn/ ] #V2 #HV12
+ elim (IH … HT1) [| /3 width=1 by fpb_fpbg, fpb_fqu, fqu_bind_dx/ ] #T2 #HT12
+ /3 width=2 by cpce_bind, ex_intro/
+| #I #V1 #T1 #_ #IH #H
+ elim (cnv_fwd_flat … H) -H #HV1 #HT1
+ elim (IH … HV1) [| /3 width=1 by fpb_fpbg, fpb_fqu, fqu_pair_sn/ ] #V2 #HV12
+ elim (IH … HT1) [| /3 width=1 by fpb_fpbg, fpb_fqu, fqu_flat_dx/ ] #T2 #HT12
+ /3 width=2 by cpce_flat, ex_intro/
+]
+qed-.
(* *)
(**************************************************************************)
+include "ground_2/xoa/ex_5_7.ma".
include "basic_2/notation/relations/pconveta_5.ma".
include "basic_2/rt_computation/cpms.ma".
(* avtivate genv *)
inductive cpce (h): relation4 genv lenv term term ≝
| cpce_sort: ∀G,L,s. cpce h G L (⋆s) (⋆s)
-| cpce_ldef: ∀G,K,V. cpce h G (K.ⓓV) (#0) (#0)
-| cpce_ldec: ∀n,G,K,V,s. ⦃G,K⦄ ⊢ V ➡*[n,h] ⋆s →
- cpce h G (K.â\93\9bV) (#0) (#0)
-| cpce_eta : ∀n,p,G,K,V,W1,W2,T. ⦃G,K⦄ ⊢ V ➡*[n,h] ⓛ{p}W1.T →
- cpce h G K W1 W2 → cpce h G (K.ⓛV) (#0) (+ⓛW2.ⓐ#0.#1)
+| 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.â\93\98{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_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)
| cpce_bind: ∀p,I,G,K,V1,V2,T1,T2.
cpce h G K V1 V2 → cpce h G (K.ⓑ{I}V1) T1 T2 →
cpce h G K (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
#h #G #Y #X2 #s0
@(insert_eq_0 … (⋆s0)) #X1 * -G -Y -X1 -X2
[ #G #L #s #_ //
-| #G #K #V #_ //
-| #n #G #K #V #s #_ #_ //
-| #n #p #G #K #V #W1 #W2 #T #_ #_ #H destruct
+| #G #i #_ //
+| #G #K #I #_ #_ //
+| #n #p #G #K #W #V1 #V2 #W2 #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) (X2):
- ∀V. ⦃G,K.ⓓV⦄ ⊢ #0 ⬌η[h] X2 → #0 = X2.
-#h #G #Y #X2 #X
-@(insert_eq_0 … (Y.ⓓX)) #Y1
-@(insert_eq_0 … (#0)) #X1
-* -G -Y1 -X1 -X2
+lemma cpce_inv_atom_sn (h) (G) (X2):
+ ∀i. ⦃G,⋆⦄ ⊢ #i ⬌η[h] X2 → #i = X2.
+#h #G #X2 #j
+@(insert_eq_0 … LAtom) #Y
+@(insert_eq_0 … (#j)) #X1
+* -G -Y -X1 -X2
[ #G #L #s #_ #_ //
-| #G #K #V #_ #_ //
-| #n #G #K #V #s #_ #_ #_ //
-| #n #p #G #K #V #W1 #W2 #T #_ #_ #_ #H destruct
-| #I #G #K #T #U #i #_ #_ #H #_ destruct
+| #G #i #_ #_ //
+| #G #K #I #_ #_ #_ //
+| #n #p #G #K #W #V1 #V2 #W2 #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) (X2):
- ∀V. ⦃G,K.ⓛV⦄ ⊢ #0 ⬌η[h] X2 →
- ∨∨ ∃∃n,s. ⦃G,K⦄ ⊢ V ➡*[n,h] ⋆s & #0 = X2
- | ∃∃n,p,W1,W2,T. ⦃G,K⦄ ⊢ V ➡*[n,h] ⓛ{p}W1.T & ⦃G,K⦄ ⊢ W1 ⬌η[h] W2 & +ⓛW2.ⓐ#0.#1 = X2.
-#h #G #Y #X2 #X
-@(insert_eq_0 … (Y.ⓛX)) #Y1
+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
@(insert_eq_0 … (#0)) #X1
-* -G -Y1 -X1 -X2
+* -G -Y -X1 -X2
[ #G #L #s #H #_ destruct
-| #G #K #V #_ #H destruct
-| #n #G #K #V #s #HV #_ #H destruct /3 width=3 by ex2_2_intro, or_introl/
-| #n #p #G #K #V #W1 #W2 #T #HV #HW #_ #H destruct /3 width=8 by ex3_5_intro, or_intror/
+| #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 #T #U #i #_ #_ #H #_ destruct
+| #G #L #l #H #_ destruct
| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
]
lemma cpce_inv_lref_sn (h) (G) (K) (X2):
∀I,i. ⦃G,K.ⓘ{I}⦄ ⊢ #↑i ⬌η[h] X2 →
∃∃T2. ⦃G,K⦄ ⊢ #i ⬌η[h] T2 & ⬆*[1] T2 ≘ X2.
-#h #G #Y #X2 #Z #j
-@(insert_eq_0 … (Y.ⓘ{Z})) #Y1
+#h #G #Y0 #X2 #Z #j
+@(insert_eq_0 … (Y0.ⓘ{Z})) #Y
@(insert_eq_0 … (#↑j)) #X1
-* -G -Y1 -X1 -X2
+* -G -Y -X1 -X2
[ #G #L #s #H #_ destruct
-| #G #K #V #H #_ destruct
-| #n #G #K #V #s #_ #H #_ destruct
-| #n #p #G #K #V #W1 #W2 #T #_ #_ #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 #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
| #I #G #L #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
+[ #G #L #s #_ //
+| #G #i #_ //
+| #G #K #I #_ #_ //
+| #n #p #G #K #W #V1 #V2 #W2 #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_bind_sn (h) (G) (K) (X2):
∀p,I,V1,T1. ⦃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
[ #G #L #s #H destruct
-| #G #K #V #H destruct
-| #n #G #K #V #s #_ #H destruct
-| #n #p #G #K #V #W1 #W2 #T #_ #_ #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 #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/
| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct
]
#h #G #Y #X2 #Z #U #X
@(insert_eq_0 … (ⓕ{Z}U.X)) #X1 * -G -Y -X1 -X2
[ #G #L #s #H destruct
-| #G #K #V #H destruct
-| #n #G #K #V #s #_ #H destruct
-| #n #p #G #K #V #W1 #W2 #T #_ #_ #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 #T #U #i #_ #_ #H destruct
+| #G #L #l #H destruct
| #p #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct
| #I #G #K #V1 #V2 #T1 #T2 #HV #HT #H destruct /2 width=5 by ex3_2_intro/
]
--- /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.ma".
+include "basic_2/rt_conversion/cpce.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL ETA-CONVERSION FOR TERMS **********************)
+
+(* Properties with uniform slicing for local environments *******************)
+
+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
+ 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/
+]
+qed.
+
+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/
+]
+qed.
projects / helm.git / commitdiff