-(* Inversion lrmmas on static type assignment for terms *********************)
-
-lemma da_inv_sta: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l →
- ∃U. ⦃G, L⦄ ⊢ T •[h] U.
-#h #g #G #L #T #l #H elim H -G -L -T -l
-[ /2 width=2/
-| #G #L #K #V #i #l #HLK #_ * #W #HVW
- elim (lift_total W 0 (i+1)) /3 width=7/
-| #G #L #K #W #i #l #HLK #_ * #V #HWV
- elim (lift_total W 0 (i+1)) /3 width=7/
-| #a #I #G #L #V #T #l #_ * /3 width=2/
-| * #G #L #V #T #l #_ * /3 width=2/
+(**************************************************************************)
+(* ___ *)
+(* ||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/degree_6.ma".
+include "basic_2/grammar/genv.ma".
+include "basic_2/substitution/drop.ma".
+include "basic_2/static/sd.ma".
+
+(* DEGREE ASSIGNMENT FOR TERMS **********************************************)
+
+(* activate genv *)
+inductive da (h:sh) (o:sd h): relation4 genv lenv term nat ≝
+| da_sort: ∀G,L,s,d. deg h o s d → da h o G L (⋆s) d
+| da_ldef: ∀G,L,K,V,i,d. ⬇[i] L ≡ K.ⓓV → da h o G K V d → da h o G L (#i) d
+| da_ldec: ∀G,L,K,W,i,d. ⬇[i] L ≡ K.ⓛW → da h o G K W d → da h o G L (#i) (d+1)
+| da_bind: ∀a,I,G,L,V,T,d. da h o G (L.ⓑ{I}V) T d → da h o G L (ⓑ{a,I}V.T) d
+| da_flat: ∀I,G,L,V,T,d. da h o G L T d → da h o G L (ⓕ{I}V.T) d
+.
+
+interpretation "degree assignment (term)"
+ 'Degree h o G L T d = (da h o G L T d).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact da_inv_sort_aux: ∀h,o,G,L,T,d. ⦃G, L⦄ ⊢ T ▪[h, o] d →
+ ∀s0. T = ⋆s0 → deg h o s0 d.
+#h #o #G #L #T #d * -G -L -T -d
+[ #G #L #s #d #Hkd #s0 #H destruct //
+| #G #L #K #V #i #d #_ #_ #s0 #H destruct
+| #G #L #K #W #i #d #_ #_ #s0 #H destruct
+| #a #I #G #L #V #T #d #_ #s0 #H destruct
+| #I #G #L #V #T #d #_ #s0 #H destruct
+]
+qed-.
+
+lemma da_inv_sort: ∀h,o,G,L,s,d. ⦃G, L⦄ ⊢ ⋆s ▪[h, o] d → deg h o s d.
+/2 width=5 by da_inv_sort_aux/ qed-.
+
+fact da_inv_lref_aux: ∀h,o,G,L,T,d. ⦃G, L⦄ ⊢ T ▪[h, o] d → ∀j. T = #j →
+ (∃∃K,V. ⬇[j] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ▪[h, o] d) ∨
+ (∃∃K,W,d0. ⬇[j] L ≡ K.ⓛW & ⦃G, K⦄ ⊢ W ▪[h, o] d0 &
+ d = d0 + 1
+ ).
+#h #o #G #L #T #d * -G -L -T -d
+[ #G #L #s #d #_ #j #H destruct
+| #G #L #K #V #i #d #HLK #HV #j #H destruct /3 width=4 by ex2_2_intro, or_introl/
+| #G #L #K #W #i #d #HLK #HW #j #H destruct /3 width=6 by ex3_3_intro, or_intror/
+| #a #I #G #L #V #T #d #_ #j #H destruct
+| #I #G #L #V #T #d #_ #j #H destruct
]
qed-.
-(* Properties on static type assignment for terms ***************************)
-
-lemma sta_da: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T •[h] U →
- ∃l. ⦃G, L⦄ ⊢ T ▪[h, g] l.
-#h #g #G #L #T #U #H elim H -G -L -T -U
-[ #G #L #k elim (deg_total h g k) /3 width=2/
-| #G #L #K #V #W #W0 #i #HLK #_ #_ * /3 width=5/
-| #G #L #K #W #V #W0 #i #HLK #_ #_ * /3 width=5/
-| #a #I #G #L #V #T #U #_ * /3 width=2/
-| #G #L #V #T #U #_ * /3 width=2/
-| #G #L #W #T #U #_ * /3 width=2/
+lemma da_inv_lref: ∀h,o,G,L,j,d. ⦃G, L⦄ ⊢ #j ▪[h, o] d →
+ (∃∃K,V. ⬇[j] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ▪[h, o] d) ∨
+ (∃∃K,W,d0. ⬇[j] L ≡ K.ⓛW & ⦃G, K⦄ ⊢ W ▪[h, o] d0 & d = d0+1).
+/2 width=3 by da_inv_lref_aux/ qed-.
+
+fact da_inv_gref_aux: ∀h,o,G,L,T,d. ⦃G, L⦄ ⊢ T ▪[h, o] d → ∀p0. T = §p0 → ⊥.
+#h #o #G #L #T #d * -G -L -T -d
+[ #G #L #s #d #_ #p0 #H destruct
+| #G #L #K #V #i #d #_ #_ #p0 #H destruct
+| #G #L #K #W #i #d #_ #_ #p0 #H destruct
+| #a #I #G #L #V #T #d #_ #p0 #H destruct
+| #I #G #L #V #T #d #_ #p0 #H destruct
+]
+qed-.
+
+lemma da_inv_gref: ∀h,o,G,L,p,d. ⦃G, L⦄ ⊢ §p ▪[h, o] d → ⊥.
+/2 width=9 by da_inv_gref_aux/ qed-.
+
+fact da_inv_bind_aux: ∀h,o,G,L,T,d. ⦃G, L⦄ ⊢ T ▪[h, o] d →
+ ∀b,J,X,Y. T = ⓑ{b,J}Y.X → ⦃G, L.ⓑ{J}Y⦄ ⊢ X ▪[h, o] d.
+#h #o #G #L #T #d * -G -L -T -d
+[ #G #L #s #d #_ #b #J #X #Y #H destruct
+| #G #L #K #V #i #d #_ #_ #b #J #X #Y #H destruct
+| #G #L #K #W #i #d #_ #_ #b #J #X #Y #H destruct
+| #a #I #G #L #V #T #d #HT #b #J #X #Y #H destruct //
+| #I #G #L #V #T #d #_ #b #J #X #Y #H destruct
]
qed-.
+
+lemma da_inv_bind: ∀h,o,b,J,G,L,Y,X,d. ⦃G, L⦄ ⊢ ⓑ{b,J}Y.X ▪[h, o] d → ⦃G, L.ⓑ{J}Y⦄ ⊢ X ▪[h, o] d.
+/2 width=4 by da_inv_bind_aux/ qed-.
+
+fact da_inv_flat_aux: ∀h,o,G,L,T,d. ⦃G, L⦄ ⊢ T ▪[h, o] d →
+ ∀J,X,Y. T = ⓕ{J}Y.X → ⦃G, L⦄ ⊢ X ▪[h, o] d.
+#h #o #G #L #T #d * -G -L -T -d
+[ #G #L #s #d #_ #J #X #Y #H destruct
+| #G #L #K #V #i #d #_ #_ #J #X #Y #H destruct
+| #G #L #K #W #i #d #_ #_ #J #X #Y #H destruct
+| #a #I #G #L #V #T #d #_ #J #X #Y #H destruct
+| #I #G #L #V #T #d #HT #J #X #Y #H destruct //
+]
+qed-.
+
+lemma da_inv_flat: ∀h,o,J,G,L,Y,X,d. ⦃G, L⦄ ⊢ ⓕ{J}Y.X ▪[h, o] d → ⦃G, L⦄ ⊢ X ▪[h, o] d.
+/2 width=5 by da_inv_flat_aux/ qed-.
projects / helm.git / blobdiff