--- /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/multiple/lleq_drop.ma".
+include "basic_2/static/aaa.ma".
+
+(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
+
+(* Properties on lazy equivalence for local environments ********************)
+
+lemma lleq_aaa_trans: ∀G,L2,T,A. ⦃G, L2⦄ ⊢ T ⁝ A →
+ ∀L1. L1 ≡[T, 0] L2 → ⦃G, L1⦄ ⊢ T ⁝ A.
+#G #L2 #T #A #H elim H -G -L2 -T -A /2 width=1 by aaa_sort/
+[ #I #G #L2 #K2 #V2 #A #i #HLK2 #_ #IHV2 #L1 #H elim (lleq_fwd_lref_dx … H … HLK2) -L2
+ [ #H elim (ylt_yle_false … H) //
+ | * /3 width=5 by aaa_lref/
+ ]
+| #a #G #L2 #V #T #B #A #_ #_ #IHV #IHT #L1 #H elim (lleq_inv_bind_O … H) -H
+ /3 width=2 by aaa_abbr/
+| #a #G #L2 #V #T #B #A #_ #_ #IHV #IHT #L1 #H elim (lleq_inv_bind_O … H) -H
+ /3 width=1 by aaa_abst/
+| #G #L2 #V #T #B #A #_ #_ #IHV #IHT #L1 #H elim (lleq_inv_flat … H) -H
+ /3 width=3 by aaa_appl/
+| #G #L2 #V #T #A #_ #_ #IHV #IHT #L1 #H elim (lleq_inv_flat … H) -H
+ /3 width=1 by aaa_cast/
+]
+qed-.
+
+lemma aaa_lleq_conf: ∀G,L2,T,A. ⦃G, L2⦄ ⊢ T ⁝ A →
+ ∀L1. L2 ≡[T, 0] L1 → ⦃G, L1⦄ ⊢ T ⁝ A.
+/3 width=3 by lleq_aaa_trans, lleq_sym/ qed-.
lemma drop_inv_refl: ∀L,l,m. ⬇[Ⓕ, l, m] L ≡ L → m = 0.
/2 width=5 by drop_inv_length_eq/ qed-.
-
-fact drop_inv_FT_aux: ∀L1,L2,s,l,m. ⬇[s, l, m] L1 ≡ L2 →
- ∀I,K,V. L2 = K.ⓑ{I}V → s = Ⓣ → l = 0 →
- ⬇[Ⓕ, l, m] L1 ≡ K.ⓑ{I}V.
-#L1 #L2 #s #l #m #H elim H -L1 -L2 -l -m
-[ #l #m #_ #J #K #W #H destruct
-| #I #L #V #J #K #W #H destruct //
-| #I #L1 #L2 #V #m #_ #IHL12 #J #K #W #H1 #H2 destruct
- /3 width=1 by drop_drop/
-| #I #L1 #L2 #V1 #V2 #l #m #_ #_ #_ #J #K #W #_ #_ #H
- elim (ysucc_inv_O_dx … H)
-]
-qed-.
-
-lemma drop_inv_FT: ∀I,L,K,V,m. ⬇[Ⓣ, 0, m] L ≡ K.ⓑ{I}V → ⬇[m] L ≡
-K.ⓑ{I}V.
-/2 width=5 by drop_inv_FT_aux/ qed.
-
-lemma drop_inv_gen: ∀I,L,K,V,s,m. ⬇[s, 0, m] L ≡ K.ⓑ{I}V → ⬇[m] L ≡
-K.ⓑ{I}V.
-#I #L #K #V * /2 width=1 by drop_inv_FT/
-qed-.
-
-lemma drop_inv_T: ∀I,L,K,V,s,m. ⬇[Ⓣ, 0, m] L ≡ K.ⓑ{I}V → ⬇[s, 0, m] L
-≡ K.ⓑ{I}V.
-#I #L #K #V * /2 width=1 by drop_inv_FT/
-qed-.
(* *)
(**************************************************************************)
-include "ground_2/relocation/rtmap_isfin.ma".
include "basic_2/notation/relations/rdropstar_3.ma".
include "basic_2/notation/relations/rdropstar_4.ma".
include "basic_2/relocation/lreq.ma".
#L1 #L2 #c @eq_repl_sym /2 width=3 by drops_eq_repl_back/ (**) (* full auto fails *)
qed-.
+lemma drops_inv_tls_at: ∀f,i1,i2. @⦃i1,f⦄ ≡ i2 →
+ ∀c, L1,L2. ⬇*[c,⫱*[i2]f] L1 ≡ L2 →
+ ⬇*[c,↑⫱*[⫯i2]f] L1 ≡ L2.
+/3 width=3 by drops_eq_repl_fwd, at_inv_tls/ qed-.
+
+(* Basic_2A1: includes: drop_FT *)
+lemma drops_TF: ∀L1,L2,f. ⬇*[Ⓣ, f] L1 ≡ L2 → ⬇*[Ⓕ, f] L1 ≡ L2.
+#L1 #L2 #f #H elim H -L1 -L2 -f
+/3 width=1 by drops_atom, drops_drop, drops_skip/
+qed.
+
+(* Basic_2A1: includes: drop_gen *)
+lemma drops_gen: ∀L1,L2,c,f. ⬇*[Ⓣ, f] L1 ≡ L2 → ⬇*[c, f] L1 ≡ L2.
+#L1 #L2 * /2 width=1 by drops_TF/
+qed-.
+
+(* Basic_2A1: includes: drop_T *)
+lemma drops_F: ∀L1,L2,c,f. ⬇*[c, f] L1 ≡ L2 → ⬇*[Ⓕ, f] L1 ≡ L2.
+#L1 #L2 * /2 width=1 by drops_TF/
+qed-.
+
(* Basic_2A1: includes: drop_refl *)
lemma drops_refl: ∀c,L,f. 𝐈⦃f⦄ → ⬇*[c, f] L ≡ L.
#c #L elim L -L /2 width=1 by drops_atom/
]
qed-.
-(* Basic_2A1: includes: drop_FT *)
-lemma drops_TF: ∀L1,L2,f. ⬇*[Ⓣ, f] L1 ≡ L2 → ⬇*[Ⓕ, f] L1 ≡ L2.
-#L1 #L2 #f #H elim H -L1 -L2 -f
-/3 width=1 by drops_atom, drops_drop, drops_skip/
-qed.
-
-(* Basic_2A1: includes: drop_gen *)
-lemma drops_gen: ∀L1,L2,c,f. ⬇*[Ⓣ, f] L1 ≡ L2 → ⬇*[c, f] L1 ≡ L2.
-#L1 #L2 * /2 width=1 by drops_TF/
-qed-.
-
-(* Basic_2A1: includes: drop_T *)
-lemma drops_F: ∀L1,L2,c,f. ⬇*[c, f] L1 ≡ L2 → ⬇*[Ⓕ, f] L1 ≡ L2.
-#L1 #L2 * /2 width=1 by drops_TF/
+lemma drops_split_div: ∀L1,L,f1,c. ⬇*[c, f1] L1 ≡ L → ∀f2,f. f1 ⊚ f2 ≡ f → 𝐔⦃f2⦄ →
+ ∃∃L2. ⬇*[Ⓕ, f2] L ≡ L2 & ⬇*[Ⓕ, f] L1 ≡ L2.
+#L1 #L #f1 #c #H elim H -L1 -L -f1
+[ #f1 #Hc #f2 #f #Hf #Hf2 @(ex2_intro … (⋆)) @drops_atom #H destruct
+| #I #L1 #L #V #f1 #HL1 #IH #f2 #f #Hf #Hf2 elim (after_inv_nxx … Hf) -Hf [2,3: // ]
+ #g #Hg #H destruct elim (IH … Hg) -IH -Hg /3 width=5 by drops_drop, ex2_intro/
+| #I #L1 #L #V1 #V #f1 #HL1 #HV1 #IH #f2 #f #Hf #Hf2
+ elim (after_inv_pxx … Hf) -Hf [1,3: * |*: // ]
+ #g2 #g #Hg #H2 #H0 destruct
+ [ lapply (isuni_inv_push … Hf2 ??) -Hf2 [1,2: // ] #Hg2 -IH
+ lapply (after_isid_inv_dx … Hg … Hg2) -Hg #Hg
+ /5 width=7 by drops_eq_repl_back, drops_F, drops_refl, drops_skip, lifts_eq_repl_back, isid_push, ex2_intro/
+ | lapply (isuni_inv_next … Hf2 ??) -Hf2 [1,2: // ] #Hg2 -HL1 -HV1
+ elim (IH … Hg) -f1 /3 width=3 by drops_drop, ex2_intro/
+ ]
+]
qed-.
(* Basic forward lemmas *****************************************************)
∃∃K1,V1. ⬇*[c, f] K1 ≡ K2 & ⬆*[f] V2 ≡ V1 & X = K1.ⓑ{I}V1.
/2 width=5 by drops_inv_skip2_aux/ qed-.
+fact drops_inv_TF_aux: ∀L1,L2,f. ⬇*[Ⓕ, f] L1 ≡ L2 → 𝐔⦃f⦄ →
+ ∀I,K,V. L2 = K.ⓑ{I}V →
+ ⬇*[Ⓣ, f] L1 ≡ K.ⓑ{I}V.
+#L1 #L2 #f #H elim H -L1 -L2 -f
+[ #f #_ #_ #J #K #W #H destruct
+| #I #L1 #L2 #V #f #_ #IH #Hf #J #K #W #H destruct
+ /4 width=3 by drops_drop, isuni_inv_next/
+| #I #L1 #L2 #V1 #V2 #f #HL12 #HV21 #_ #Hf #J #K #W #H destruct
+ lapply (isuni_inv_push … Hf ??) -Hf [1,2: // ] #Hf
+ <(drops_fwd_isid … HL12) -K // <(lifts_fwd_isid … HV21) -V1
+ /3 width=3 by drops_refl, isid_push/
+]
+qed-.
+
+(* Basic_2A1: includes: drop_inv_FT *)
+lemma drops_inv_TF: ∀I,L,K,V,f. ⬇*[Ⓕ, f] L ≡ K.ⓑ{I}V → 𝐔⦃f⦄ →
+ ⬇*[Ⓣ, f] L ≡ K.ⓑ{I}V.
+/2 width=3 by drops_inv_TF_aux/ qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+(* Basic_2A1: includes: drop_inv_gen *)
+lemma drops_inv_gen: ∀I,L,K,V,c,f. ⬇*[c, f] L ≡ K.ⓑ{I}V → 𝐔⦃f⦄ →
+ ⬇*[Ⓣ, f] L ≡ K.ⓑ{I}V.
+#I #L #K #V * /2 width=1 by drops_inv_TF/
+qed-.
+
+(* Basic_2A1: includes: drop_inv_T *)
+lemma drops_inv_F: ∀I,L,K,V,c,f. ⬇*[Ⓕ, f] L ≡ K.ⓑ{I}V → 𝐔⦃f⦄ →
+ ⬇*[c, f] L ≡ K.ⓑ{I}V.
+#I #L #K #V * /2 width=1 by drops_inv_TF/
+qed-.
+
(* Inversion lemmas with test for uniformity ********************************)
lemma drops_inv_isuni: ∀L1,L2,f. ⬇*[Ⓣ, f] L1 ≡ L2 → 𝐔⦃f⦄ →
(* *)
(**************************************************************************)
-include "basic_2/substitution/drop_drop.ma".
include "basic_2/static/aaa.ma".
(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
-(* Main properties **********************************************************)
+(* Main inversion lemmas ****************************************************)
theorem aaa_mono: ∀G,L,T,A1. ⦃G, L⦄ ⊢ T ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T ⁝ A2 → A1 = A2.
#G #L #T #A1 #H elim H -G -L -T -A1
-[ #G #L #s #A2 #H
- >(aaa_inv_sort … H) -H //
-| #I1 #G #L #K1 #V1 #B #i #HLK1 #_ #IHA1 #A2 #H
- elim (aaa_inv_lref … H) -H #I2 #K2 #V2 #HLK2 #HA2
- lapply (drop_mono … HLK1 … HLK2) -L #H destruct /2 width=1 by/
-| #a #G #L #V #T #B1 #A1 #_ #_ #_ #IHA1 #A2 #H
+[ #G #L #s #A2 #H >(aaa_inv_sort … H) -H //
+| #I1 #G #L #V1 #B #_ #IH #A2 #H
+ elim (aaa_inv_zero … H) -H #I2 #K2 #V2 #H #HA2 destruct /2 width=1 by/
+| #I1 #G #L #V1 #B #i #_ #IH #A2 #H
+ elim (aaa_inv_lref … H) -H #I2 #K2 #V2 #H #HA2 destruct /2 width=1 by/
+| #p #G #L #V #T #B1 #A1 #_ #_ #_ #IH #A2 #H
elim (aaa_inv_abbr … H) -H /2 width=1 by/
-| #a #G #L #V1 #T1 #B1 #A1 #_ #_ #IHB1 #IHA1 #X #H
+| #p #G #L #V1 #T1 #B1 #A1 #_ #_ #IHB1 #IHA1 #X #H
elim (aaa_inv_abst … H) -H #B2 #A2 #HB2 #HA2 #H destruct /3 width=1 by eq_f2/
| #G #L #V1 #T1 #B1 #A1 #_ #_ #_ #IHA1 #A2 #H
elim (aaa_inv_appl … H) -H #B2 #_ #HA2
(* *)
(**************************************************************************)
-include "basic_2/relocation/drops.ma".
+include "basic_2/relocation/drops_drops.ma".
+include "basic_2/s_computation/fqup_weight.ma".
+include "basic_2/s_computation/fqup_drops.ma".
include "basic_2/static/aaa.ma".
(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
-(* Properties with generic slicing for local environments *******************)
+(* Advanced properties ******************************************************)
(* Basic_2A1: was: aaa_lref *)
lemma aaa_lref_gen: ∀I,G,K,V,B,i,L. ⬇*[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ⁝ B → ⦃G, L⦄ ⊢ #i ⁝ B.
]
qed.
-(* Basic_2A1: includes: aaa_lift *)
-lemma aaa_lifts: ∀G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → ∀L2,c,f. ⬇*[c, f] L2 ≡ L1 →
- ∀T2. ⬆*[f] T1 ≡ T2 → ⦃G, L2⦄ ⊢ T2 ⁝ A.
-#G #L1 #T1 #A #H elim H -G -L1 -T1 -A
-[ #G #L1 #s #L2 #c #f #_ #T2 #H
- >(lifts_inv_sort1 … H) -H //
-| #I #G #L1 #V1 #B #_ #IHB #L2 #c #f #HL21 #T2 #H
- elim (lifts_inv_lref1 … H) -H #i2 #Hi #H destruct
- @aaa_lref_gen [5: @IHB ]
-| #I #G #L1 #V1 #B #i1 #_ #IHB #L2 #c #f #HL21 #T2 #H
- elim (lifts_inv_lref1 … H) -H #i2 #Hi #H destruct
- lapply (at_inv_nxx … H)
-
-
-
-
-| #I #G #L1 #K1 #V1 #B #i #HLK1 #_ #IHB #L2 #c #l #k #HL21 #T2 #H
- elim (lift_inv_lref1 … H) -H * #Hil #H destruct
- [ elim (drop_trans_le … HL21 … HLK1) -L1 /2 width=2 by ylt_fwd_le/ #X #HLK2 #H
- elim (drop_inv_skip2 … H) -H /2 width=1 by ylt_to_minus/ -Hil #K2 #V2 #HK21 #HV12 #H destruct
- /3 width=9 by aaa_lref/
- | lapply (drop_trans_ge … HL21 … HLK1 ?) -L1
- /3 width=9 by aaa_lref, drop_inv_gen/
- ]
-| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHB #IHA #L2 #c #l #k #HL21 #X #H
- elim (lift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
- /4 width=5 by aaa_abbr, drop_skip/
-| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHB #IHA #L2 #c #l #k #HL21 #X #H
- elim (lift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
- /4 width=5 by aaa_abst, drop_skip/
-| #G #L1 #V1 #T1 #B #A #_ #_ #IHB #IHA #L2 #c #l #k #HL21 #X #H
- elim (lift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
- /3 width=5 by aaa_appl/
-| #G #L1 #V1 #T1 #A #_ #_ #IH1 #IH2 #L2 #c #l #k #HL21 #X #H
- elim (lift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
- /3 width=5 by aaa_cast/
-]
-qed.
-
-(* Inversion lemmas with generic slicing for local environments *************)
+(* Advanced inversion lemmas ************************************************)
(* Basic_2A1: was: aaa_inv_lref *)
lemma aaa_inv_lref_gen: ∀G,A,i,L. ⦃G, L⦄ ⊢ #i ⁝ A →
]
qed-.
-lemma aaa_inv_lift: ∀G,L2,T2,A. ⦃G, L2⦄ ⊢ T2 ⁝ A → ∀L1,c,l,k. ⬇[c, l, k] L2 ≡ L1 →
- ∀T1. ⬆[l, k] T1 ≡ T2 → ⦃G, L1⦄ ⊢ T1 ⁝ A.
-#G #L2 #T2 #A #H elim H -G -L2 -T2 -A
-[ #G #L2 #s #L1 #c #l #k #_ #T1 #H
- >(lift_inv_sort2 … H) -H //
-| #I #G #L2 #K2 #V2 #B #i #HLK2 #_ #IHB #L1 #c #l #k #HL21 #T1 #H
- elim (lift_inv_lref2 … H) -H * #Hil #H destruct
- [ elim (drop_conf_lt … HL21 … HLK2) -L2 /3 width=9 by aaa_lref/
- | lapply (drop_conf_ge … HL21 … HLK2 ?) -L2 /3 width=9 by aaa_lref/
+(* Properties with generic slicing for local environments *******************)
+
+(* Basic_2A1: includes: aaa_lift *)
+lemma aaa_lifts: ∀G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → ∀L2,c,f. ⬇*[c, f] L2 ≡ L1 →
+ ∀T2. ⬆*[f] T1 ≡ T2 → ⦃G, L2⦄ ⊢ T2 ⁝ A.
+@fqup_wf_ind_eq #G0 #L0 #T0 #IH #G #L1 * *
+[ #s #HG #HL #HT #A #H #L2 #c #f #HL21 #X #HX -IH -c
+ lapply (aaa_inv_sort … H) -H #H destruct
+ >(lifts_inv_sort1 … HX) -HX //
+| #i1 #HG #HL #HT #A #H #L2 #c #f #HL21 #X #HX
+ elim (aaa_inv_lref_gen … H) -H #J #K1 #V1 #HLK1 #HA
+ elim (lifts_inv_lref1 … HX) -HX #i2 #Hf #H destruct
+ lapply (drops_trans … HL21 … HLK1 ??) -HL21 [1,2: // ] #H
+ elim (drops_split_trans … H) -H [ |*: /2 width=6 by after_uni_dx/ ] #Y #HLK2 #HY
+ lapply (drops_inv_tls_at … Hf … HY) -HY #HY -Hf
+ elim (drops_inv_skip2 … HY) -HY #K2 #V2 #HK21 #HV12 #H destruct
+ /4 width=12 by aaa_lref_gen, fqup_lref, drops_inv_gen/
+| #l #HG #HL #HT #A #H #L2 #c #f #HL21 #X #HX -IH -c -f
+ elim (aaa_inv_gref … H)
+| #p * #V1 #T1 #HG #HL #HT #A #H #L2 #c #f #HL21 #X #HX
+ [ elim (aaa_inv_abbr … H) -H #B #HB #HA
+ elim (lifts_inv_bind1 … HX) -HX #V2 #T2 #HV12 #HT12 #H destruct
+ /4 width=9 by aaa_abbr, drops_skip/
+ | elim (aaa_inv_abst … H) -H #B #A0 #HB #HA #H0
+ elim (lifts_inv_bind1 … HX) -HX #V2 #T2 #HV12 #HT12 #H destruct
+ /4 width=8 by aaa_abst, drops_skip/
+ ]
+| * #V1 #T1 #HG #HL #HT #A #H #L2 #c #f #HL21 #X #HX
+ [ elim (aaa_inv_appl … H) -H #B #HB #HA
+ elim (lifts_inv_flat1 … HX) -HX #V2 #T2 #HV12 #HT12 #H destruct
+ /3 width=10 by aaa_appl/
+ | elim (aaa_inv_cast … H) -H #H1A #H2A
+ elim (lifts_inv_flat1 … HX) -HX #V2 #T2 #HV12 #HT12 #H destruct
+ /3 width=8 by aaa_cast/
+ ]
+]
+qed-.
+
+(* Inversion lemmas with generic slicing for local environments *************)
+
+(* Basic_2A1: includes: aaa_inv_lift *)
+lemma aaa_inv_lifts: ∀G,L2,T2,A. ⦃G, L2⦄ ⊢ T2 ⁝ A → ∀L1,c,f. ⬇*[c, f] L2 ≡ L1 →
+ ∀T1. ⬆*[f] T1 ≡ T2 → ⦃G, L1⦄ ⊢ T1 ⁝ A.
+@fqup_wf_ind_eq #G0 #L0 #T0 #IH #G #L2 * *
+[ #s #HG #HL #HT #A #H #L1 #c #f #HL21 #X #HX -IH -c
+ lapply (aaa_inv_sort … H) -H #H destruct
+ >(lifts_inv_sort2 … HX) -HX //
+| #i2 #HG #HL #HT #A #H #L1 #c #f #HL21 #X #HX
+ elim (aaa_inv_lref_gen … H) -H #J #K2 #V2 #HLK2 #HA
+ elim (lifts_inv_lref2 … HX) -HX #i1 #Hf #H destruct
+ lapply (drops_split_div … HL21 (𝐔❴i1❵) ???) -HL21 [4: * |*: // ] #Y #HLK1 #HY
+ lapply (drops_conf … HLK2 … HY ??) -HY [1,2: /2 width=6 by after_uni_dx/ ] #HY
+ lapply (drops_inv_tls_at … Hf … HY) -HY #HY -Hf
+ elim (drops_inv_skip1 … HY) -HY #K1 #V1 #HK21 #HV12 #H destruct
+ /4 width=12 by aaa_lref_gen, fqup_lref, drops_inv_F/
+| #l #HG #HL #HT #A #H #L1 #c #f #HL21 #X #HX -IH -c -f
+ elim (aaa_inv_gref … H)
+| #p * #V2 #T2 #HG #HL #HT #A #H #L1 #c #f #HL21 #X #HX
+ [ elim (aaa_inv_abbr … H) -H #B #HB #HA
+ elim (lifts_inv_bind2 … HX) -HX #V1 #T1 #HV12 #HT12 #H destruct
+ /4 width=9 by aaa_abbr, drops_skip/
+ | elim (aaa_inv_abst … H) -H #B #A0 #HB #HA #H0
+ elim (lifts_inv_bind2 … HX) -HX #V1 #T1 #HV12 #HT12 #H destruct
+ /4 width=8 by aaa_abst, drops_skip/
+ ]
+| * #V2 #T2 #HG #HL #HT #A #H #L1 #c #f #HL21 #X #HX
+ [ elim (aaa_inv_appl … H) -H #B #HB #HA
+ elim (lifts_inv_flat2 … HX) -HX #V1 #T1 #HV12 #HT12 #H destruct
+ /3 width=10 by aaa_appl/
+ | elim (aaa_inv_cast … H) -H #H1A #H2A
+ elim (lifts_inv_flat2 … HX) -HX #V1 #T1 #HV12 #HT12 #H destruct
+ /3 width=8 by aaa_cast/
]
-| #a #G #L2 #V2 #T2 #B #A #_ #_ #IHB #IHA #L1 #c #l #k #HL21 #X #H
- elim (lift_inv_bind2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
- /4 width=5 by aaa_abbr, drop_skip/
-| #a #G #L2 #V2 #T2 #B #A #_ #_ #IHB #IHA #L1 #c #l #k #HL21 #X #H
- elim (lift_inv_bind2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
- /4 width=5 by aaa_abst, drop_skip/
-| #G #L2 #V2 #T2 #B #A #_ #_ #IHB #IHA #L1 #c #l #k #HL21 #X #H
- elim (lift_inv_flat2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
- /3 width=5 by aaa_appl/
-| #G #L2 #V2 #T2 #A #_ #_ #IH1 #IH2 #L1 #c #l #k #HL21 #X #H
- elim (lift_inv_flat2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
- /3 width=5 by aaa_cast/
]
qed-.
(* *)
(**************************************************************************)
-include "basic_2/multiple/fqus_alt.ma".
-include "basic_2/static/aaa_lift.ma".
+include "basic_2/s_computation/fqus_fqup.ma".
+include "basic_2/static/aaa_drops.ma".
(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
lemma aaa_fqu_conf: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
∀A1. ⦃G1, L1⦄ ⊢ T1 ⁝ A1 → ∃A2. ⦃G2, L2⦄ ⊢ T2 ⁝ A2.
#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-[ #I #G #L #T #A #H elim (aaa_inv_lref … H) -H
- #J #K #V #H #HA lapply (drop_inv_O2 … H) -H
- #H destruct /2 width=2 by ex_intro/
-| * [ #a ] * #G #L #V #T #X #H
+[ #I #G #L #T #A #H elim (aaa_inv_zero … H) -H
+ #J #K #V #H #HA destruct /2 width=2 by ex_intro/
+| * [ #p ] * #G #L #V #T #X #H
[ elim (aaa_inv_abbr … H)
| elim (aaa_inv_abst … H)
| elim (aaa_inv_appl … H)
| elim (aaa_inv_cast … H)
] -H /2 width=2 by ex_intro/
-| #a * #G #L #V #T #X #H
+| #p * #G #L #V #T #X #H
[ elim (aaa_inv_abbr … H)
| elim (aaa_inv_abst … H)
] -H /2 width=2 by ex_intro/
[ elim (aaa_inv_appl … H)
| elim (aaa_inv_cast … H)
] -H /2 width=2 by ex_intro/
-| /3 width=9 by aaa_inv_lift, ex_intro/
+| /5 width=8 by aaa_inv_lifts, drops_refl, drops_drop, ex_intro/
]
qed-.
lemma aaa_fquq_conf: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
∀A1. ⦃G1, L1⦄ ⊢ T1 ⁝ A1 → ∃A2. ⦃G2, L2⦄ ⊢ T2 ⁝ A2.
-#G1 #G2 #L1 #L2 #T1 #T2 #H elim(fquq_inv_gen … H) -H /2 width=6 by aaa_fqu_conf/
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -H /2 width=6 by aaa_fqu_conf/
* #H1 #H2 #H3 destruct /2 width=2 by ex_intro/
qed-.
lemma aaa_fqus_conf: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ →
∀A1. ⦃G1, L1⦄ ⊢ T1 ⁝ A1 → ∃A2. ⦃G2, L2⦄ ⊢ T2 ⁝ A2.
-#G1 #G2 #L1 #L2 #T1 #T2 #H elim(fqus_inv_gen … H) -H /2 width=6 by aaa_fqup_conf/
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim(fqus_inv_fqup … H) -H /2 width=6 by aaa_fqup_conf/
* #H1 #H2 #H3 destruct /2 width=2 by ex_intro/
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/multiple/lleq_drop.ma".
-include "basic_2/static/aaa.ma".
-
-(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
-
-(* Properties on lazy equivalence for local environments ********************)
-
-lemma lleq_aaa_trans: ∀G,L2,T,A. ⦃G, L2⦄ ⊢ T ⁝ A →
- ∀L1. L1 ≡[T, 0] L2 → ⦃G, L1⦄ ⊢ T ⁝ A.
-#G #L2 #T #A #H elim H -G -L2 -T -A /2 width=1 by aaa_sort/
-[ #I #G #L2 #K2 #V2 #A #i #HLK2 #_ #IHV2 #L1 #H elim (lleq_fwd_lref_dx … H … HLK2) -L2
- [ #H elim (ylt_yle_false … H) //
- | * /3 width=5 by aaa_lref/
- ]
-| #a #G #L2 #V #T #B #A #_ #_ #IHV #IHT #L1 #H elim (lleq_inv_bind_O … H) -H
- /3 width=2 by aaa_abbr/
-| #a #G #L2 #V #T #B #A #_ #_ #IHV #IHT #L1 #H elim (lleq_inv_bind_O … H) -H
- /3 width=1 by aaa_abst/
-| #G #L2 #V #T #B #A #_ #_ #IHV #IHT #L1 #H elim (lleq_inv_flat … H) -H
- /3 width=3 by aaa_appl/
-| #G #L2 #V #T #A #_ #_ #IHV #IHT #L1 #H elim (lleq_inv_flat … H) -H
- /3 width=1 by aaa_cast/
-]
-qed-.
-
-lemma aaa_lleq_conf: ∀G,L2,T,A. ⦃G, L2⦄ ⊢ T ⁝ A →
- ∀L1. L2 ≡[T, 0] L1 → ⦃G, L1⦄ ⊢ T ⁝ A.
-/3 width=3 by lleq_aaa_trans, lleq_sym/ 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 "ground_2/relocation/rtmap_id.ma".
+include "basic_2/s_computation/fqup_weight.ma".
+include "basic_2/static/frees.ma".
+
+(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
+
+(* Advanced properties ******************************************************)
+
+(* Notes: this replaces lemma 1400 concluding the "big tree" theorem *)
+lemma frees_total: ∀L,T. ∃f. L ⊢ 𝐅*⦃T⦄ ≡ f.
+#L #T @(fqup_wf_ind_eq … (⋆) L T) -L -T
+#G0 #L0 #T0 #IH #G #L *
+[ cases L -L /3 width=2 by frees_atom, ex_intro/
+ #L #I #V *
+ [ #s #HG #HL #HT destruct
+ elim (IH G L (⋆s)) -IH /3 width=2 by frees_sort_gen, fqu_fqup, fqu_drop, lifts_sort, ex_intro/
+ | * [2: #i ] #HG #HL #HT destruct
+ [ elim (IH G L (#i)) -IH /3 width=2 by frees_lref, fqu_fqup, ex_intro/
+ | elim (IH G L V) -IH /3 width=2 by frees_zero, fqu_fqup, fqu_lref_O, ex_intro/
+ ]
+ | #l #HG #HL #HT destruct
+ elim (IH G L (§l)) -IH /3 width=2 by frees_gref_gen, fqu_fqup, fqu_drop, lifts_gref, ex_intro/
+ ]
+| * [ #p ] #I #V #T #HG #HL #HT destruct elim (IH G L V) // #f1 #HV
+ [ elim (IH G (L.ⓑ{I}V) T) -IH // #f2 #HT
+ elim (sor_isfin_ex f1 (⫱f2))
+ /3 width=6 by frees_fwd_isfin, frees_bind, isfin_tl, ex_intro/
+ | elim (IH G L T) -IH // #f2 #HT
+ elim (sor_isfin_ex f1 f2)
+ /3 width=6 by frees_fwd_isfin, frees_flat, ex_intro/
+ ]
+]
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/relocation/frees.ma".
+include "basic_2/static/frees.ma".
(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
(**************************************************************************)
include "basic_2/relocation/lreq.ma".
-include "basic_2/relocation/frees.ma".
+include "basic_2/static/frees.ma".
(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
+++ /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 "ground_2/relocation/rtmap_id.ma".
-include "basic_2/grammar/cl_restricted_weight.ma".
-include "basic_2/relocation/frees.ma".
-
-(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
-
-(* Advanced properties ******************************************************)
-
-(* Notes: this replaces lemma 1400 concluding the "big tree" theorem *)
-lemma frees_total: ∀L,T. ∃f. L ⊢ 𝐅*⦃T⦄ ≡ f.
-@(f2_ind … rfw) #n #IH #L *
-[ cases L -L /3 width=2 by frees_atom, ex_intro/
- #L #I #V *
- [ #s #Hn destruct elim (IH L (⋆s)) -IH /3 width=2 by frees_sort, ex_intro/
- | * [2: #i ] #Hn destruct
- [ elim (IH L (#i)) -IH /3 width=2 by frees_lref, ex_intro/
- | elim (IH L V) -IH /3 width=2 by frees_zero, ex_intro/
- ]
- | #l #Hn destruct elim (IH L (§l)) -IH /3 width=2 by frees_gref, ex_intro/
- ]
-| * [ #p ] #I #V #T #Hn destruct elim (IH L V) // #f1 #HV
- [ elim (IH (L.ⓑ{I}V) T) -IH // #f2 #HT
- elim (sor_isfin_ex f1 (⫱f2))
- /3 width=6 by frees_fwd_isfin, frees_bind, isfin_tl, ex_intro/
- | elim (IH L T) -IH // #f2 #HT
- elim (sor_isfin_ex f1 f2)
- /3 width=6 by frees_fwd_isfin, frees_flat, ex_intro/
- ]
-]
-qed-.
include "basic_2/notation/relations/lazyeq_6.ma".
include "basic_2/grammar/genv.ma".
-include "basic_2/relocation/frees_weight.ma".
-include "basic_2/relocation/frees_lreq.ma".
+include "basic_2/static/frees_fqup.ma".
+include "basic_2/static/frees_lreq.ma".
(* RANGED EQUIVALENCE FOR CLOSURES ******************************************)
(**************************************************************************)
include "basic_2/relocation/lreq_lreq.ma".
-include "basic_2/relocation/frees_frees.ma".
-include "basic_2/relocation/freq.ma".
+include "basic_2/static/frees_frees.ma".
+include "basic_2/static/freq.ma".
(* RANGED EQUIVALENCE FOR CLOSURES *****************************************)
(**************************************************************************)
include "basic_2/notation/relations/lrsubeqa_3.ma".
-include "basic_2/static/lsubr.ma".
include "basic_2/static/aaa.ma".
-(* LOCAL ENVIRONMENT REFINEMENT FOR ATOMIC ARITY ASSIGNMENT *****************)
+(* RESTRICTED REFINEMENT FOR ATOMIC ARITY ASSIGNMENT ************************)
inductive lsuba (G:genv): relation lenv ≝
| lsuba_atom: lsuba G (⋆) (⋆)
I = Abst & L1 = K1.ⓓⓝW.V.
/2 width=3 by lsuba_inv_pair2_aux/ qed-.
-(* Basic forward lemmas *****************************************************)
-
-lemma lsuba_fwd_lsubr: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → L1 ⫃ L2.
-#G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_pair, lsubr_beta/
-qed-.
-
(* Basic properties *********************************************************)
lemma lsuba_refl: ∀G,L. G ⊢ L ⫃⁝ L.
#G #L elim L -L /2 width=1 by lsuba_atom, lsuba_pair/
qed.
-
-(* Note: the constant 0 cannot be generalized *)
-lemma lsuba_drop_O1_conf: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → ∀K1,c,k. ⬇[c, 0, k] L1 ≡ K1 →
- ∃∃K2. G ⊢ K1 ⫃⁝ K2 & ⬇[c, 0, k] L2 ≡ K2.
-#G #L1 #L2 #H elim H -L1 -L2
-[ /2 width=3 by ex2_intro/
-| #I #L1 #L2 #V #_ #IHL12 #K1 #c #k #H
- elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK1
- [ destruct
- elim (IHL12 L1 c 0) -IHL12 // #X #HL12 #H
- <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_pair, drop_pair, ex2_intro/
- | elim (IHL12 … HLK1) -L1 /3 width=3 by drop_drop_lt, ex2_intro/
- ]
-| #L1 #L2 #W #V #A #HV #HW #_ #IHL12 #K1 #c #k #H
- elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK1
- [ destruct
- elim (IHL12 L1 c 0) -IHL12 // #X #HL12 #H
- <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_beta, drop_pair, ex2_intro/
- | elim (IHL12 … HLK1) -L1 /3 width=3 by drop_drop_lt, ex2_intro/
- ]
-]
-qed-.
-
-(* Note: the constant 0 cannot be generalized *)
-lemma lsuba_drop_O1_trans: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → ∀K2,c,k. ⬇[c, 0, k] L2 ≡ K2 →
- ∃∃K1. G ⊢ K1 ⫃⁝ K2 & ⬇[c, 0, k] L1 ≡ K1.
-#G #L1 #L2 #H elim H -L1 -L2
-[ /2 width=3 by ex2_intro/
-| #I #L1 #L2 #V #_ #IHL12 #K2 #c #k #H
- elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK2
- [ destruct
- elim (IHL12 L2 c 0) -IHL12 // #X #HL12 #H
- <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_pair, drop_pair, ex2_intro/
- | elim (IHL12 … HLK2) -L2 /3 width=3 by drop_drop_lt, ex2_intro/
- ]
-| #L1 #L2 #W #V #A #HV #HW #_ #IHL12 #K2 #c #k #H
- elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK2
- [ destruct
- elim (IHL12 L2 c 0) -IHL12 // #X #HL12 #H
- <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_beta, drop_pair, ex2_intro/
- | elim (IHL12 … HLK2) -L2 /3 width=3 by drop_drop_lt, ex2_intro/
- ]
-]
-qed-.
include "basic_2/static/aaa_aaa.ma".
include "basic_2/static/lsuba.ma".
-(* LOCAL ENVIRONMENT REFINEMENT FOR ATOMIC ARITY ASSIGNMENT *****************)
+(* RESTRICTED REFINEMENT FOR ATOMIC ARITY ASSIGNMENT ************************)
(* Properties concerning atomic arity assignment ****************************)
--- /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/lrsubeqa_3.ma".
+include "basic_2/static/lsubr.ma".
+include "basic_2/static/aaa.ma".
+
+(* RESTRICTED REFINEMENT FOR ATOMIC ARITY ASSIGNMENT ************************)
+
+(* Basic properties *********************************************************)
+
+(* Note: the constant 0 cannot be generalized *)
+lemma lsuba_drop_O1_conf: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → ∀K1,c,k. ⬇[c, 0, k] L1 ≡ K1 →
+ ∃∃K2. G ⊢ K1 ⫃⁝ K2 & ⬇[c, 0, k] L2 ≡ K2.
+#G #L1 #L2 #H elim H -L1 -L2
+[ /2 width=3 by ex2_intro/
+| #I #L1 #L2 #V #_ #IHL12 #K1 #c #k #H
+ elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK1
+ [ destruct
+ elim (IHL12 L1 c 0) -IHL12 // #X #HL12 #H
+ <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_pair, drop_pair, ex2_intro/
+ | elim (IHL12 … HLK1) -L1 /3 width=3 by drop_drop_lt, ex2_intro/
+ ]
+| #L1 #L2 #W #V #A #HV #HW #_ #IHL12 #K1 #c #k #H
+ elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK1
+ [ destruct
+ elim (IHL12 L1 c 0) -IHL12 // #X #HL12 #H
+ <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_beta, drop_pair, ex2_intro/
+ | elim (IHL12 … HLK1) -L1 /3 width=3 by drop_drop_lt, ex2_intro/
+ ]
+]
+qed-.
+
+(* Note: the constant 0 cannot be generalized *)
+lemma lsuba_drop_O1_trans: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → ∀K2,c,k. ⬇[c, 0, k] L2 ≡ K2 →
+ ∃∃K1. G ⊢ K1 ⫃⁝ K2 & ⬇[c, 0, k] L1 ≡ K1.
+#G #L1 #L2 #H elim H -L1 -L2
+[ /2 width=3 by ex2_intro/
+| #I #L1 #L2 #V #_ #IHL12 #K2 #c #k #H
+ elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK2
+ [ destruct
+ elim (IHL12 L2 c 0) -IHL12 // #X #HL12 #H
+ <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_pair, drop_pair, ex2_intro/
+ | elim (IHL12 … HLK2) -L2 /3 width=3 by drop_drop_lt, ex2_intro/
+ ]
+| #L1 #L2 #W #V #A #HV #HW #_ #IHL12 #K2 #c #k #H
+ elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK2
+ [ destruct
+ elim (IHL12 L2 c 0) -IHL12 // #X #HL12 #H
+ <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_beta, drop_pair, ex2_intro/
+ | elim (IHL12 … HLK2) -L2 /3 width=3 by drop_drop_lt, ex2_intro/
+ ]
+]
+qed-.
include "basic_2/static/lsuba_aaa.ma".
-(* LOCAL ENVIRONMENT REFINEMENT FOR ATOMIC ARITY ASSIGNMENT *****************)
+(* RESTRICTED REFINEMENT FOR ATOMIC ARITY ASSIGNMENT ************************)
(* Main properties **********************************************************)
--- /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/static/lsubr.ma".
+include "basic_2/static/lsuba.ma".
+
+(* RESTRICTED REFINEMENT FOR ATOMIC ARITY ASSIGNMENT ************************)
+
+(* Forward lemmas with restricted refinement for local environments *********)
+
+lemma lsuba_fwd_lsubr: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → L1 ⫃ L2.
+#G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_pair, lsubr_beta/
+qed-.
(* Properties with at *******************************************************)
-lemma after_isuni_dx: ∀i2,i1,f2. @⦃i1, f2⦄ ≡ i2 →
- ∀f. f2 ⊚ 𝐔❴i1❵ ≡ f → 𝐔❴i2❵ ⊚ ⫱*[i2] f2 ≡ f.
+lemma after_uni_dx: ∀i2,i1,f2. @⦃i1, f2⦄ ≡ i2 →
+ ∀f. f2 ⊚ 𝐔❴i1❵ ≡ f → 𝐔❴i2❵ ⊚ ⫱*[i2] f2 ≡ f.
#i2 elim i2 -i2
[ #i1 #f2 #Hf2 #f #Hf
elim (at_inv_xxp … Hf2) -Hf2 // #g2 #H1 #H2 destruct
]
qed.
-lemma after_isuni_sn: ∀i2,i1,f2. @⦃i1, f2⦄ ≡ i2 →
- ∀f. 𝐔❴i2❵ ⊚ ⫱*[i2] f2 ≡ f → f2 ⊚ 𝐔❴i1❵ ≡ f.
+lemma after_uni_sn: ∀i2,i1,f2. @⦃i1, f2⦄ ≡ i2 →
+ ∀f. 𝐔❴i2❵ ⊚ ⫱*[i2] f2 ≡ f → f2 ⊚ 𝐔❴i1❵ ≡ f.
#i2 elim i2 -i2
[ #i1 #f2 #Hf2 #f #Hf
elim (at_inv_xxp … Hf2) -Hf2 // #g2 #H1 #H2 destruct
projects / helm.git / commitdiff