matita/matita/lib/pts_dummy/arity_eval.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "lambda/arity.ma".
  16
  17 (* ARITY ASSIGNMENT ***********************************************************)
  18
  19 (* the arity type *************************************************************)
  20
  21 (* arity type assigned to the term t in the environment E *)
  22 let rec ata K t on t ≝  match t with
  23    [ Sort _     ⇒ TOP
  24    | Rel i      ⇒ nth i … K TOP
  25    | App M N    ⇒ pred (ata K M)
  26    | Lambda N M ⇒ let C ≝ ata K N in FUN C (ata (C::K) M)
  27    | Prod _ _   ⇒ TOP
  28    | D M        ⇒ TOP (* ??? not so sure yet *)
  29    ].
  30
  31 interpretation "arity type assignment" 'IInt1 t K = (ata K t).
  32
  33 lemma ata_app: ∀M,N,K. 〚App M N〛_[K] = pred (〚M〛_[K]).
  34 // qed.
  35
  36 lemma ata_lambda: ∀M,N,K. 〚Lambda N M〛_[K] = FUN (〚N〛_[K]) (〚M〛_[〚N〛_[K]::K]).
  37 // qed.
  38
  39 lemma ata_rel_lt: ∀H,K,i. (S i) ≤ |K| → 〚Rel i〛_[K @ H] = 〚Rel i〛_[K].
  40 #H #K elim K -K [1: #i #Hie elim (not_le_Sn_O i) #Hi elim (Hi Hie) ]
  41 #A #K #IHK #i elim i -i // #i #_ #Hie @IHK @le_S_S_to_le @Hie
  42 qed.
  43
  44 lemma ata_rel_ge: ∀H,K,i. (S i) ≰ |K| →
  45                   〚Rel i〛_[K @ H] = 〚Rel (i-|K|)〛_[H].
  46 #H #K elim K -K [ normalize // ]
  47 #A #K #IHK #i elim i -i [1: -IHK #Hie elim Hie -Hie #Hie; elim (Hie ?) /2/ ]
  48 normalize #i #_ #Hie @IHK /2/
  49 qed.
  50
  51 (* weakeing and thinning lemma for the arity type assignment *)
  52 (* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
  53 lemma ata_lift: ∀p,K,Kp. p = |Kp| → ∀t,k,Kk. k = |Kk| →
  54                 〚lift t k p〛_[Kk @ Kp @ K] = 〚t〛_[Kk @ K].
  55 #p #K #Kp #HKp #t elim t -t //
  56    [ #i #k #Kk #HKk @(leb_elim (S i) k) #Hik
  57      [ >(lift_rel_lt … Hik) >HKk in Hik #Hik
  58        >(ata_rel_lt … Hik) >(ata_rel_lt … Hik) //
  59      | >(lift_rel_ge … Hik) >HKk in Hik #Hik
  60        >(ata_rel_ge … Hik) <associative_append
  61        >(ata_rel_ge …) >length_append >HKp;
  62        [ >arith2 // @not_lt_to_le /2/ | @(arith3 … Hik) ]
  63      ]
  64    | #M #N #IHM #_ #k #Kk #HKk >lift_app >ata_app /3/
  65    | #N #M #IHN #IHM #k #Kk #HKk >lift_lambda >ata_lambda
  66      >IHN // >(IHM … (? :: ?)) // >commutative_plus /2/
  67    ]
  68 qed.
  69
  70 (* substitution lemma for the arity type assignment *)
  71 (* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
  72 lemma ata_subst: ∀v,K,t,k,Kk. k = |Kk| →
  73                  〚t[k≝v]〛_[Kk @ K] = 〚t〛_[Kk @ 〚v〛_[K]::K].
  74 #v #K #t elim t -t //
  75    [ #i #k #Kk #HKk @(leb_elim (S i) k) #H1ik
  76      [ >(subst_rel1 … H1ik) >HKk in H1ik #H1ik
  77        >(ata_rel_lt … H1ik) >(ata_rel_lt … H1ik) //
  78      | @(eqb_elim i k) #H2ik
  79        [ >H2ik in H1ik -H2ik i #H1ik >subst_rel2 >HKk in H1ik #H1ik
  80          >(ata_rel_ge … H1ik) <minus_n_n >(ata_lift ? ? ? ? ? ? ([])) //
  81        | lapply (arith4 … H1ik H2ik) -H1ik H2ik #Hik >(subst_rel3 … Hik)
  82           >ata_rel_ge; [2: /2/ ] <(associative_append ? ? ([?]) ?)
  83            >ata_rel_ge >length_append >commutative_plus;
  84            [ <minus_plus // | <HKk -HKk Kk @not_le_to_not_le_S_S /3/ ]
  85        ]
  86      ]
  87    | #M #N #IHM #_ #k #Kk #HKk >subst_app >ata_app /3/
  88    | #N #M #IHN #IHM #k #Kk #HKk >subst_lambda > ata_lambda
  89      >IHN // >commutative_plus >(IHM … (? :: ?)) /2/
  90    ]
  91 qed.
  92
  93 (* the arity ******************************************************************)
  94
  95 (* arity assigned to the term t in the environments E and K *)
  96 let rec aa K E t on t ≝ match t with
  97    [ Sort _     ⇒ sort
  98    | Rel i      ⇒ nth i … E sort
  99    | App M N    ⇒ aapp (〚N〛_[K]) (aa K E M) (aa K E N)
 100    | Lambda N M ⇒ aabst (λc. aa (〚N〛_[K]::K) (c :: E) M)
 101    | Prod N M   ⇒ aabst (λc. aa (〚N〛_[K]::K) (c :: E) M)
 102    | D M        ⇒ sort (* ??? not so sure yet *)
 103    ].
 104
 105 interpretation "arity assignment" 'IInt2 t E K = (aa K E t).
 106
 107 lemma aa_app: ∀M,N,E,K. 〚App M N〛_[E,K] = aapp (〚N〛_[K]) (〚M〛_[E,K]) (〚N〛_[E,K]).
 108 // qed.
 109
 110 lemma aa_lambda: ∀N,M,E,K. 〚Lambda N M〛_[E,K] = aabst (λc. 〚M〛_[c :: E, 〚N〛_[K]::K]).
 111 // qed.
 112
 113 lemma aa_prod: ∀N,M,E,K. 〚Prod N M〛_[E,K] = aabst (λc. 〚M〛_[c :: E, 〚N〛_[K]::K]).
 114 // qed.
 115
 116 lemma aa_rel_lt: ∀K2,K1,D,E,i. (S i) ≤ |E| →
 117                  〚Rel i〛_[E @ D, K1] = 〚Rel i〛_[E, K2].
 118 #K1 #K1 #D #E elim E -E [1: #i #Hie elim (not_le_Sn_O i) #Hi elim (Hi Hie) ]
 119 #C #E #IHE #i elim i -i // #i #_ #Hie @IHE @le_S_S_to_le @Hie
 120 qed.
 121
 122 lemma aa_rel_lt_id: ∀K,D,E,i. (S i) ≤ |E| →
 123                     〚Rel i〛_[E @ D, K] = 〚Rel i〛_[E, K].
 124 #K @(aa_rel_lt K) qed.
 125
 126 lemma aa_rel_ge: ∀K2,K1,D,E,i. (S i) ≰ |E| →
 127                  〚Rel i〛_[E @ D, K1] = 〚Rel (i-|E|)〛_[D, K2].
 128 #K2 #K1 #D #E elim E -E [ normalize // ]
 129 #C #E #IHE #i elim i -i [1: -IHE #Hie elim Hie -Hie #Hie elim (Hie ?) /2/ ]
 130 normalize #i #_ #Hie @IHE /2/
 131 qed.
 132
 133 lemma aa_rel_ge_id: ∀K,D,E,i. (S i) ≰ |E| →
 134                     〚Rel i〛_[E @ D, K] = 〚Rel (i-|E|)〛_[D, K].
 135 #K @(aa_rel_ge K) qed.
 136
 137 (* weakeing and thinning lemma for the arity assignment *)
 138 (* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
 139 lemma aa_lift: ∀K,E1,E2. E1 ≅ E2 → ∀p,Kp,Ep. p=|Kp| → p = |Ep| →
 140                ∀t,k,Kk,E1k,E2k. k = |Kk| → k = |E1k| → E1k ≅ E2k →
 141                〚lift t k p〛_[E1k @ Ep @ E1, Kk @ Kp @ K] ≅ 〚t〛_[E2k @ E2, Kk @ K].
 142 #K #E1 #E2 #HE #p #Kp #Ep #HKp #HEp #t elim t -t /2 by invariant_sort/
 143    [ #i #k #Kk #E1k #E2k #HKk #HE1k #HEk @(leb_elim (S i) k) #Hik
 144      [ >(lift_rel_lt … Hik) >HE1k in Hik #Hik >(aa_rel_lt_id … Hik)
 145        >(all2_length … HEk) in Hik #Hik >(aa_rel_lt_id … Hik) /2 by nth_sort_comp/
 146      | >(lift_rel_ge … Hik) >HE1k in Hik #Hik <(associative_append … E1k)
 147        >(aa_rel_ge_id …) >length_append >HEp; [2: @(arith3 … Hik) ]
 148        >(all2_length … HEk) in Hik #Hik >(aa_rel_ge_id … Hik) >arith2;
 149        [ /2 by nth_sort_comp/ | @not_lt_to_le /2/ ]
 150      ]
 151    | #M #N #IHM #IHN #k #Kk #E1k #E2k #HKk #HE1k #HEk >lift_app >aa_app
 152      >ata_lift /3/
 153    | #N #M #_ #IHM #k #Kk #E1k #E2k #HKk #HE1k #HEk >lift_lambda >aa_lambda
 154      @aabst_comp #a1 #a2 #Ha >ata_lift // >commutative_plus
 155      @(IHM ? (?::?) (?::?) (?::?)); [ >HKk | >HE1k ] /2/
 156    | #N #M #_ #IHM #k #Kk #E1k #E2k #HKk #HE1k #HEk >lift_prod >aa_prod
 157      @aabst_comp #a1 #a2 #Ha >ata_lift // >commutative_plus
 158      @(IHM ? (?::?) (?::?) (?::?)); [ >HKk | >HE1k ] /2/
 159    ]
 160 qed.
 161
 162 lemma aa_comp: ∀E1,E2. E1 ≅ E2 → ∀t,K. 〚t〛_[E1, K] ≅ 〚t〛_[E2, K].
 163 #E1 #E2 #HE #t #K <(lift_0 t 0) in ⊢ (? % ?)
 164 @(aa_lift … ([]) ([]) … ([]) ([]) ([])) //
 165 qed.
 166
 167 (* the assigned arity is invariant *)
 168 lemma aa_invariant: ∀t,E,K. !E → !〚t〛_[E, K].
 169 /2/ qed.
 170
 171 (* substitution lemma for the arity assignment *)
 172 (* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
 173 lemma aa_subst: ∀K,E1,E2. E1 ≅ E2 →
 174                 ∀v,t,k,Kk,E1k,E2k. k = |Kk| → k = |E1k| → E1k ≅ E2k →
 175                 〚t[k≝v]〛_[E1k@E1, Kk@K] ≅ 〚t〛_[E2k@〚v〛_[E2,K]::E2, Kk@〚v〛_[K]::K].
 176 #K #E1 #E2 #HE #v #t elim t -t /2 by invariant_sort/
 177    [ #i #k #Kk #E1k #E2k #HKk #HE1k #HEk @(leb_elim (S i) k) #H1ik
 178      [ >(subst_rel1 … H1ik) >HE1k in H1ik #H1ik >(aa_rel_lt_id … H1ik)
 179        >(all2_length … HEk) in H1ik #H1ik >(aa_rel_lt_id … H1ik) /2/
 180      | @(eqb_elim i k) #H2ik
 181        [ >H2ik in H1ik -H2ik i #H1ik >subst_rel2 >HE1k in H1ik #H1ik
 182          >(all2_length … HEk) in H1ik #H1ik >(aa_rel_ge_id … H1ik) <minus_n_n
 183          >HE1k in HKk #HKk -HE1k k  >(all2_length … HEk) in HKk #HKk
 184          @(aa_lift … ([]) ([]) ([])) /3/
 185        | lapply (arith4 … H1ik H2ik) -H1ik H2ik #Hik
 186          >(subst_rel3 … Hik) >aa_rel_ge_id; [2: /2/ ]
 187          <(associative_append ? ? ([?]) ?) in ⊢ (? ? (? ? % ?))
 188          >HE1k in Hik #Hik >(aa_rel_ge (Kk@K))
 189          >length_append >commutative_plus <(all2_length … HEk);
 190          [ <minus_plus /2/ | @not_le_to_not_le_S_S /3/ ]
 191        ]
 192      ]
 193    | #M #N #IHM #IHN #k #Kk #E1k #E2k #HKk #HE1k #HEk >subst_app >aa_app
 194      >ata_subst /3/
 195    | #N #M #_ #IHM #k #Kk #E1k #E2k #HKk #HE1k #HEk >subst_lambda >aa_lambda
 196      @aabst_comp #a1 #a2 #Ha >ata_subst // >commutative_plus
 197      @(IHM ? (?::?) (?::?) (?::?)); [ >HKk | >HE1k ] /2/
 198    | #N #M #_ #IHM #k #Kk #E1k #E2k #HKk #HE1k #HEk >subst_prod >aa_prod
 199      @aabst_comp #a1 #a2 #Ha >ata_subst // >commutative_plus
 200      @(IHM ? (?::?) (?::?) (?::?)); [ >HKk | >HE1k ] /2/
 201    ]
 202 qed.
 203
 204 (* the assigned arity is constant *)
 205 lemma aa_isc: ∀t,E,K. !E → all2 … isc E K → isc (〚t〛_[E,K]) (〚t〛_[K]).
 206 #t elim t -t /2 by isc_sort/
 207    [ #i #E #K #HE #H @(all2_nth … isc) //
 208    | /3/
 209    | #N #M #IHN #IHM #E #K #HE #H >aa_lambda >ata_lambda
 210
 211
 212
 213 (*
 214 const ? (〚v〛_[E1,K] (〚v〛_[K])) ≅ 〚v〛_[E1,K].
 215
 216 theorem aa_beta: ∀K,E1,E2. E1 ≅ E2 → ∀w,t,v. 〚v〛_[K] = 〚w〛_[K] →
 217                  〚App (Lambda w t) v〛_[E1,K] ≅ 〚t[0≝v]〛_[E2,K].
 218 #K #E1 #E2 #HE #w #t #v #H > aa_app >aa_lambda
 219 @transitive_aeq; [3: @symmetric_aeq @(aa_subst … E1 … ([]) ([]) ([])) /2/ | skip ]
 220 >H @aa_comp -H v; #C whd in ⊢ (? ? % ?)
 221 *)
 222
 223 (*
 224 axiom cons_comp: ∀a1,a2. a1 ≅ a2 → ∀E1,E2. E1 ≅ E2 → a1 :: E1 ≅ a2 :: E2.
 225
 226 axiom pippo: ∀A:Type[0]. ∀a,b,c. (a::b) @ c = a :: b @ c.
 227 @A qed.
 228 *)