matita/matita/lib/pts_dummy/degree.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 "pts_dummy/ext_lambda.ma".
  16 (*
  17 (* DEGREE ASSIGNMENT **********************************************************)
  18
  19 (* The degree of a term *******************************************************)
  20
  21 (* degree assigned to the term t in the environment L *)
  22 let rec deg L t on t ≝ match t with
  23    [ Sort i     ⇒ i + 3
  24    | Rel i      ⇒ (nth i … L 0)
  25    | App m _    ⇒ deg L m
  26    | Lambda n m ⇒ let l ≝ deg L n in deg (l::L) m
  27    | Prod n m   ⇒ let l ≝ deg L n in deg (l::L) m
  28    | D m        ⇒ deg L m
  29    ].
  30
  31 interpretation "degree assignment (term)" 'IInt1 t L = (deg L t).
  32
  33 lemma deg_app: ∀m,n,L. ║App m n║_[L] = ║m║_[L].
  34 // qed.
  35
  36 lemma deg_lambda: ∀n,m,L. ║Lambda n m║_[L] = ║m║_[║n║_[L]::L].
  37 // qed.
  38
  39 lemma deg_prod: ∀n,m,L. ║Prod n m║_[L] = ║m║_[║n║_[L]::L].
  40 // qed.
  41
  42 lemma deg_rel_lt: ∀L,K,i. (S i) ≤ |K| → ║Rel i║_[K @ L] = ║Rel i║_[K].
  43 #L #K elim K -K [1: #i #Hie elim (not_le_Sn_O i) #Hi elim (Hi Hie) ]
  44 #k #K #IHK #i elim i -i // #i #_ #Hie @IHK @le_S_S_to_le @Hie
  45 qed.
  46
  47 lemma deg_rel_not_le: ∀L,K,i. (S i) ≰ |K| →
  48                       ║Rel i║_[K @ L] = ║Rel (i-|K|)║_[L].
  49 #L #K elim K -K [ normalize // ]
  50 #k #K #IHK #i elim i -i [1: -IHK #Hie elim Hie -Hie #Hie; elim (Hie ?) /2/ ]
  51 normalize #i #_ #Hie @IHK /2/
  52 qed.
  53
  54 (* weakeing and thinning lemma for the degree assignment *)
  55 (* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
  56 lemma deg_lift: ∀p,L,Lp. p = |Lp| → ∀t,k,Lk. k = |Lk| →
  57                 ║lift t k p║_[Lk @ Lp @ L] = ║t║_[Lk @ L].
  58 #p #L #Lp #HLp #t elim t -t //
  59    [ #i #k #Lk #HLk @(leb_elim (S i) k) #Hik
  60      [ >(lift_rel_lt … Hik) >HLk in Hik -HLk #Hik
  61        >(deg_rel_lt … Hik) >(deg_rel_lt … Hik) //
  62      | >(lift_rel_not_le … Hik) >HLk in Hik -HLk #Hik
  63        >(deg_rel_not_le … Hik) <associative_append
  64        >(deg_rel_not_le …) >length_append >HLp -HLp
  65        [ >arith2 // @not_lt_to_le /2/ | @(arith3 … Hik) ]
  66      ]
  67    | #m #n #IHm #_ #k #Lk #HLk >lift_app >deg_app /3/
  68    | #n #m #IHn #IHm #k #Lk #HLk >lift_lambda >deg_lambda
  69      >IHn // >(IHm … (? :: ?)) // >commutative_plus /2/
  70    | #n #m #IHn #IHm #k #Lk #HLk >lift_prod >deg_prod
  71      >IHn // >(IHm … (? :: ?)) // >commutative_plus /2/
  72    | #m #IHm #k #Lk #HLk >IHm //
  73    ]
  74 qed.
  75
  76 lemma deg_lift_1: ∀t,N,L. ║lift t 0 1║_[N :: L] = ║t║_[L].
  77 #t #N #L >(deg_lift ?? ([?]) … ([]) …) //
  78 qed.
  79
  80 (* substitution lemma for the degree assignment *)
  81 (* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
  82 lemma deg_subst: ∀v,L,t,k,Lk. k = |Lk| →
  83                  ║t[k≝v]║_[Lk @ L] = ║t║_[Lk @ ║v║_[L]::L].
  84 #v #L #t elim t -t //
  85    [ #i #k #Lk #HLk @(leb_elim (S i) k) #H1ik
  86      [ >(subst_rel1 … H1ik) >HLk in H1ik #H1ik
  87        >(deg_rel_lt … H1ik) >(deg_rel_lt … H1ik) //
  88      | @(eqb_elim i k) #H2ik
  89        [ >H2ik in H1ik -H2ik i #H1ik >subst_rel2 >HLk in H1ik -HLk #H1ik
  90          >(deg_rel_not_le … H1ik) <minus_n_n >(deg_lift ? ? ? ? ? ? ([])) normalize //
  91        | lapply (arith4 … H1ik H2ik) -H1ik H2ik #Hik >(subst_rel3 … Hik)
  92          >deg_rel_not_le; [2: /2/ ] <(associative_append ? ? ([?]) ?)
  93          >deg_rel_not_le >length_append >commutative_plus;
  94          [ <minus_plus // | <HLk -HLk Lk @not_le_to_not_le_S_S /3/ ]
  95        ]
  96      ]
  97    | #m #n #IHm #_ #k #Lk #HLk >subst_app >deg_app /3/
  98    | #n #m #IHn #IHm #k #Lk #HLk >subst_lambda > deg_lambda
  99      >IHn // >commutative_plus >(IHm … (? :: ?)) /2/
 100    | #n #m #IHn #IHm #k #Lk #HLk >subst_prod > deg_prod
 101      >IHn // >commutative_plus >(IHm … (? :: ?)) /2/
 102    | #m #IHm #k #Lk #HLk >IHm //
 103    ]
 104 qed.
 105
 106 lemma deg_subst_0: ∀t,v,L. ║t[0≝v]║_[L] = ║t║_[║v║_[L]::L].
 107 #t #v #L >(deg_subst ???? ([])) //
 108 qed.
 109
 110 (* The degree context  ********************************************************)
 111
 112 (* degree context assigned to the type context G *)
 113 let rec Deg L G on G ≝ match G with
 114    [ nil      ⇒ L
 115    | cons t F ⇒ let H ≝ Deg L F in ║t║_[H] - 1 :: H
 116    ].
 117
 118 interpretation "degree assignment (type context)" 'IInt1 G L = (Deg L G).
 119
 120 interpretation "degree assignment (type context)" 'IInt G = (Deg (nil ?) G).
 121
 122 lemma Deg_cons: ∀L,F,t. let H ≝ Deg L F in
 123                 ║t :: F║_[L] = ║t║_[H] - 1 :: H.
 124 // qed.
 125
 126 lemma ltl_Deg: ∀L,G. ltl … (║G║_[L]) (|G|) = L.
 127 #L #G elim G normalize //
 128 qed.
 129
 130 lemma Deg_Deg: ∀L,G,H. ║H @ G║_[L] = ║H║_[║G║_[L]].
 131 #L #G #H elim H normalize //
 132 qed.
 133
 134 interpretation "degree assignment (type context)" 'IIntS1 G L = (lhd ? (Deg L G) (length ? G)).
 135
 136 lemma length_DegHd: ∀L,G. |║G║*_[L]| = |G|.
 137 #L #G elim G normalize //
 138 qed.
 139
 140 lemma Deg_decomp: ∀L,G. ║G║*_[L] @ L = ║G║_[L].
 141 // qed.
 142
 143 lemma append_Deg: ∀L,G,H. ║H @ G║_[L] = ║H║*_[║G║_[L]] @ ║G║_[L].
 144 // qed.
 145
 146 lemma DegHd_Lift: ∀L,Lp,p. p = |Lp| →
 147                   ∀G. ║Lift G p║*_[Lp @ L] = ║G║*_[L].
 148 #L #Lp #p #HLp #G elim G //
 149 #t #G #IH normalize >IH <Deg_decomp /4/
 150 qed.
 151
 152 lemma Deg_lift_subst: ∀v,w,G. [║v║_[║G║]] = ║[w]║*_[║G║] →
 153                       ∀t,k,Gk. k = |Gk| →
 154                       ║lift t[k≝v] k 1 :: Lift Gk 1 @ [w] @ G║ =
 155                       ║t :: Lift Gk 1 @ [w] @ G║.
 156 #v #w #G #Hvw #t #k #Gk #HGk
 157 >Deg_cons >Deg_cons in ⊢ (???%)
 158 >append_Deg >append_Deg <Hvw -Hvw >DegHd_Lift; [2: //]
 159 >deg_lift; [2,3: >HGk /2/] <(deg_subst … k) // >HGk /2/
 160 qed.
 161 *)