--- /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 "lambda/arity.ma".
+
+(* ARITY ASSIGNMENT ***********************************************************)
+
+(* the arity type *************************************************************)
+
+(* arity type assigned to the term t in the environment E *)
+let rec ata K t on t ≝ match t with
+ [ Sort _ ⇒ TOP
+ | Rel i ⇒ nth i … K TOP
+ | App M N ⇒ pred (ata K M)
+ | Lambda N M ⇒ let C ≝ ata K N in FUN C (ata (C::K) M)
+ | Prod _ _ ⇒ TOP
+ | D M ⇒ TOP (* ??? not so sure yet *)
+ ].
+
+interpretation "arity type assignment" 'IInt1 t K = (ata K t).
+
+lemma ata_app: ∀M,N,K. 〚App M N〛_[K] = pred (〚M〛_[K]).
+// qed.
+
+lemma ata_lambda: ∀M,N,K. 〚Lambda N M〛_[K] = FUN (〚N〛_[K]) (〚M〛_[〚N〛_[K]::K]).
+// qed.
+
+lemma ata_rel_lt: ∀H,K,i. (S i) ≤ |K| → 〚Rel i〛_[K @ H] = 〚Rel i〛_[K].
+#H #K elim K -K [1: #i #Hie elim (not_le_Sn_O i) #Hi elim (Hi Hie) ]
+#A #K #IHK #i elim i -i // #i #_ #Hie @IHK @le_S_S_to_le @Hie
+qed.
+
+lemma ata_rel_ge: ∀H,K,i. (S i) ≰ |K| →
+ 〚Rel i〛_[K @ H] = 〚Rel (i-|K|)〛_[H].
+#H #K elim K -K [ normalize // ]
+#A #K #IHK #i elim i -i [1: -IHK #Hie elim Hie -Hie #Hie; elim (Hie ?) /2/ ]
+normalize #i #_ #Hie @IHK /2/
+qed.
+
+(* weakeing and thinning lemma for the arity type assignment *)
+(* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
+lemma ata_lift: ∀p,K,Kp. p = |Kp| → ∀t,k,Kk. k = |Kk| →
+ 〚lift t k p〛_[Kk @ Kp @ K] = 〚t〛_[Kk @ K].
+#p #K #Kp #HKp #t elim t -t //
+ [ #i #k #Kk #HKk @(leb_elim (S i) k) #Hik
+ [ >(lift_rel_lt … Hik) >HKk in Hik #Hik
+ >(ata_rel_lt … Hik) >(ata_rel_lt … Hik) //
+ | >(lift_rel_ge … Hik) >HKk in Hik #Hik
+ >(ata_rel_ge … Hik) <associative_append
+ >(ata_rel_ge …) >length_append >HKp;
+ [ >arith2 // @not_lt_to_le /2/ | @(arith3 … Hik) ]
+ ]
+ | #M #N #IHM #_ #k #Kk #HKk >lift_app >ata_app /3/
+ | #N #M #IHN #IHM #k #Kk #HKk >lift_lambda >ata_lambda
+ >IHN // >(IHM … (? :: ?)) // >commutative_plus /2/
+ ]
+qed.
+
+(* substitution lemma for the arity type assignment *)
+(* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
+lemma ata_subst: ∀v,K,t,k,Kk. k = |Kk| →
+ 〚t[k≝v]〛_[Kk @ K] = 〚t〛_[Kk @ 〚v〛_[K]::K].
+#v #K #t elim t -t //
+ [ #i #k #Kk #HKk @(leb_elim (S i) k) #H1ik
+ [ >(subst_rel1 … H1ik) >HKk in H1ik #H1ik
+ >(ata_rel_lt … H1ik) >(ata_rel_lt … H1ik) //
+ | @(eqb_elim i k) #H2ik
+ [ >H2ik in H1ik -H2ik i #H1ik >subst_rel2 >HKk in H1ik #H1ik
+ >(ata_rel_ge … H1ik) <minus_n_n >(ata_lift ? ? ? ? ? ? ([])) //
+ | lapply (arith4 … H1ik H2ik) -H1ik H2ik #Hik >(subst_rel3 … Hik)
+ >ata_rel_ge; [2: /2/ ] <(associative_append ? ? ([?]) ?)
+ >ata_rel_ge >length_append >commutative_plus;
+ [ <minus_plus // | <HKk -HKk Kk @not_le_to_not_le_S_S /3/ ]
+ ]
+ ]
+ | #M #N #IHM #_ #k #Kk #HKk >subst_app >ata_app /3/
+ | #N #M #IHN #IHM #k #Kk #HKk >subst_lambda > ata_lambda
+ >IHN // >commutative_plus >(IHM … (? :: ?)) /2/
+ ]
+qed.
+
+(* the arity ******************************************************************)
+
+(* arity assigned to the term t in the environments E and K *)
+let rec aa K E t on t ≝ match t with
+ [ Sort _ ⇒ sort
+ | Rel i ⇒ nth i … E sort
+ | App M N ⇒ aapp (〚N〛_[K]) (aa K E M) (aa K E N)
+ | Lambda N M ⇒ aabst (λc. aa (〚N〛_[K]::K) (c :: E) M)
+ | Prod N M ⇒ aabst (λc. aa (〚N〛_[K]::K) (c :: E) M)
+ | D M ⇒ sort (* ??? not so sure yet *)
+ ].
+
+interpretation "arity assignment" 'IInt2 t E K = (aa K E t).
+
+lemma aa_app: ∀M,N,E,K. 〚App M N〛_[E,K] = aapp (〚N〛_[K]) (〚M〛_[E,K]) (〚N〛_[E,K]).
+// qed.
+
+lemma aa_lambda: ∀N,M,E,K. 〚Lambda N M〛_[E,K] = aabst (λc. 〚M〛_[c :: E, 〚N〛_[K]::K]).
+// qed.
+
+lemma aa_prod: ∀N,M,E,K. 〚Prod N M〛_[E,K] = aabst (λc. 〚M〛_[c :: E, 〚N〛_[K]::K]).
+// qed.
+
+lemma aa_rel_lt: ∀K2,K1,D,E,i. (S i) ≤ |E| →
+ 〚Rel i〛_[E @ D, K1] = 〚Rel i〛_[E, K2].
+#K1 #K1 #D #E elim E -E [1: #i #Hie elim (not_le_Sn_O i) #Hi elim (Hi Hie) ]
+#C #E #IHE #i elim i -i // #i #_ #Hie @IHE @le_S_S_to_le @Hie
+qed.
+
+lemma aa_rel_lt_id: ∀K,D,E,i. (S i) ≤ |E| →
+ 〚Rel i〛_[E @ D, K] = 〚Rel i〛_[E, K].
+#K @(aa_rel_lt K) qed.
+
+lemma aa_rel_ge: ∀K2,K1,D,E,i. (S i) ≰ |E| →
+ 〚Rel i〛_[E @ D, K1] = 〚Rel (i-|E|)〛_[D, K2].
+#K2 #K1 #D #E elim E -E [ normalize // ]
+#C #E #IHE #i elim i -i [1: -IHE #Hie elim Hie -Hie #Hie elim (Hie ?) /2/ ]
+normalize #i #_ #Hie @IHE /2/
+qed.
+
+lemma aa_rel_ge_id: ∀K,D,E,i. (S i) ≰ |E| →
+ 〚Rel i〛_[E @ D, K] = 〚Rel (i-|E|)〛_[D, K].
+#K @(aa_rel_ge K) qed.
+
+(* weakeing and thinning lemma for the arity assignment *)
+(* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
+lemma aa_lift: ∀K,E1,E2. E1 ≅ E2 → ∀p,Kp,Ep. p=|Kp| → p = |Ep| →
+ ∀t,k,Kk,E1k,E2k. k = |Kk| → k = |E1k| → E1k ≅ E2k →
+ 〚lift t k p〛_[E1k @ Ep @ E1, Kk @ Kp @ K] ≅ 〚t〛_[E2k @ E2, Kk @ K].
+#K #E1 #E2 #HE #p #Kp #Ep #HKp #HEp #t elim t -t /2 by invariant_sort/
+ [ #i #k #Kk #E1k #E2k #HKk #HE1k #HEk @(leb_elim (S i) k) #Hik
+ [ >(lift_rel_lt … Hik) >HE1k in Hik #Hik >(aa_rel_lt_id … Hik)
+ >(all2_length … HEk) in Hik #Hik >(aa_rel_lt_id … Hik) /2 by nth_sort_comp/
+ | >(lift_rel_ge … Hik) >HE1k in Hik #Hik <(associative_append … E1k)
+ >(aa_rel_ge_id …) >length_append >HEp; [2: @(arith3 … Hik) ]
+ >(all2_length … HEk) in Hik #Hik >(aa_rel_ge_id … Hik) >arith2;
+ [ /2 by nth_sort_comp/ | @not_lt_to_le /2/ ]
+ ]
+ | #M #N #IHM #IHN #k #Kk #E1k #E2k #HKk #HE1k #HEk >lift_app >aa_app
+ >ata_lift /3/
+ | #N #M #_ #IHM #k #Kk #E1k #E2k #HKk #HE1k #HEk >lift_lambda >aa_lambda
+ @aabst_comp #a1 #a2 #Ha >ata_lift // >commutative_plus
+ @(IHM ? (?::?) (?::?) (?::?)); [ >HKk | >HE1k ] /2/
+ | #N #M #_ #IHM #k #Kk #E1k #E2k #HKk #HE1k #HEk >lift_prod >aa_prod
+ @aabst_comp #a1 #a2 #Ha >ata_lift // >commutative_plus
+ @(IHM ? (?::?) (?::?) (?::?)); [ >HKk | >HE1k ] /2/
+ ]
+qed.
+
+lemma aa_comp: ∀E1,E2. E1 ≅ E2 → ∀t,K. 〚t〛_[E1, K] ≅ 〚t〛_[E2, K].
+#E1 #E2 #HE #t #K <(lift_0 t 0) in ⊢ (? % ?)
+@(aa_lift … ([]) ([]) … ([]) ([]) ([])) //
+qed.
+
+(* the assigned arity is invariant *)
+lemma aa_invariant: ∀t,E,K. !E → !〚t〛_[E, K].
+/2/ qed.
+
+(* substitution lemma for the arity assignment *)
+(* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
+lemma aa_subst: ∀K,E1,E2. E1 ≅ E2 →
+ ∀v,t,k,Kk,E1k,E2k. k = |Kk| → k = |E1k| → E1k ≅ E2k →
+ 〚t[k≝v]〛_[E1k@E1, Kk@K] ≅ 〚t〛_[E2k@〚v〛_[E2,K]::E2, Kk@〚v〛_[K]::K].
+#K #E1 #E2 #HE #v #t elim t -t /2 by invariant_sort/
+ [ #i #k #Kk #E1k #E2k #HKk #HE1k #HEk @(leb_elim (S i) k) #H1ik
+ [ >(subst_rel1 … H1ik) >HE1k in H1ik #H1ik >(aa_rel_lt_id … H1ik)
+ >(all2_length … HEk) in H1ik #H1ik >(aa_rel_lt_id … H1ik) /2/
+ | @(eqb_elim i k) #H2ik
+ [ >H2ik in H1ik -H2ik i #H1ik >subst_rel2 >HE1k in H1ik #H1ik
+ >(all2_length … HEk) in H1ik #H1ik >(aa_rel_ge_id … H1ik) <minus_n_n
+ >HE1k in HKk #HKk -HE1k k >(all2_length … HEk) in HKk #HKk
+ @(aa_lift … ([]) ([]) ([])) /3/
+ | lapply (arith4 … H1ik H2ik) -H1ik H2ik #Hik
+ >(subst_rel3 … Hik) >aa_rel_ge_id; [2: /2/ ]
+ <(associative_append ? ? ([?]) ?) in ⊢ (? ? (? ? % ?))
+ >HE1k in Hik #Hik >(aa_rel_ge (Kk@K))
+ >length_append >commutative_plus <(all2_length … HEk);
+ [ <minus_plus /2/ | @not_le_to_not_le_S_S /3/ ]
+ ]
+ ]
+ | #M #N #IHM #IHN #k #Kk #E1k #E2k #HKk #HE1k #HEk >subst_app >aa_app
+ >ata_subst /3/
+ | #N #M #_ #IHM #k #Kk #E1k #E2k #HKk #HE1k #HEk >subst_lambda >aa_lambda
+ @aabst_comp #a1 #a2 #Ha >ata_subst // >commutative_plus
+ @(IHM ? (?::?) (?::?) (?::?)); [ >HKk | >HE1k ] /2/
+ | #N #M #_ #IHM #k #Kk #E1k #E2k #HKk #HE1k #HEk >subst_prod >aa_prod
+ @aabst_comp #a1 #a2 #Ha >ata_subst // >commutative_plus
+ @(IHM ? (?::?) (?::?) (?::?)); [ >HKk | >HE1k ] /2/
+ ]
+qed.
+
+(* the assigned arity is constant *)
+lemma aa_isc: ∀t,E,K. !E → all2 … isc E K → isc (〚t〛_[E,K]) (〚t〛_[K]).
+#t elim t -t /2 by isc_sort/
+ [ #i #E #K #HE #H @(all2_nth … isc) //
+ | /3/
+ | #N #M #IHN #IHM #E #K #HE #H >aa_lambda >ata_lambda
+
+
+
+(*
+const ? (〚v〛_[E1,K] (〚v〛_[K])) ≅ 〚v〛_[E1,K].
+
+theorem aa_beta: ∀K,E1,E2. E1 ≅ E2 → ∀w,t,v. 〚v〛_[K] = 〚w〛_[K] →
+ 〚App (Lambda w t) v〛_[E1,K] ≅ 〚t[0≝v]〛_[E2,K].
+#K #E1 #E2 #HE #w #t #v #H > aa_app >aa_lambda
+@transitive_aeq; [3: @symmetric_aeq @(aa_subst … E1 … ([]) ([]) ([])) /2/ | skip ]
+>H @aa_comp -H v; #C whd in ⊢ (? ? % ?)
+*)
+
+(*
+axiom cons_comp: ∀a1,a2. a1 ≅ a2 → ∀E1,E2. E1 ≅ E2 → a1 :: E1 ≅ a2 :: E2.
+
+axiom pippo: ∀A:Type[0]. ∀a,b,c. (a::b) @ c = a :: b @ c.
+@A qed.
+*)
projects / helm.git / blobdiff