matita/matita/lib/pts_dummy_new/rc_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 "pts_dummy/rc_hsat.ma".
  16 include "basics/core_notation/napart_2.ma".
  17 (*
  18 (* THE EVALUATION *************************************************************)
  19
  20 (* The arity of a term t in an environment E *)
  21 let rec aa E t on t ≝ match t with
  22    [ Sort _     ⇒ SORT
  23    | Rel i      ⇒ nth i … E SORT
  24    | App M N    ⇒ pred (aa E M)
  25    | Lambda N M ⇒ let Q ≝ aa E N in ABST Q (aa (Q::E) M)
  26    | Prod N M   ⇒ aa ((aa E N)::E) M
  27    | D M        ⇒ aa E M
  28    ].
  29
  30 interpretation "arity assignment (term)" 'Eval1 t E = (aa E t).
  31
  32 (* The arity of a type context *)
  33 let rec caa E G on G ≝ match G with
  34    [ nil      ⇒ E
  35    | cons t F ⇒ let D ≝ caa E F in 〚t〛_[D] :: D
  36    ].
  37
  38 interpretation "arity assignment (type context)" 'Eval1 G E = (caa E G).
  39
  40 lemma aa_app: ∀M,N,E. 〚App M N〛_[E] = pred (〚M〛_[E]).
  41 // qed.
  42
  43 lemma aa_lambda: ∀M,N,E. 〚Lambda N M〛_[E] = ABST (〚N〛_[E]) (〚M〛_[〚N〛_[E]::E]).
  44 // qed.
  45
  46 lemma aa_prod: ∀M,N,E. 〚Prod N M〛_[E] = 〚M〛_[〚N〛_[E]::E].
  47 // qed.
  48
  49 lemma aa_rel_lt: ∀D,E,i. (S i) ≤ |E| → 〚Rel i〛_[E @ D] = 〚Rel i〛_[E].
  50 #D #E (elim E) -E [1: #i #Hie (elim (not_le_Sn_O i)) #Hi (elim (Hi Hie)) ]
  51 #C #F #IHE #i (elim i) -i // #i #_ #Hie @IHE @le_S_S_to_le @Hie
  52 qed.
  53
  54 lemma aa_rel_ge: ∀D,E,i. (S i) ≰ |E| →
  55                    〚Rel i〛_[E @ D] = 〚Rel (i-|E|)〛_[D].
  56 #D #E (elim E) -E [ normalize // ]
  57 #C #F #IHE #i (elim i) -i [1: -IHE #Hie (elim Hie) -Hie #Hie (elim (Hie ?)) /2/ ]
  58 normalize #i #_ #Hie @IHE /2/
  59 qed.
  60
  61 (* weakeing and thinning lemma arity assignment *)
  62 (* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
  63 lemma aa_lift: ∀E,Ep,t,Ek.
  64                  〚lift t (|Ek|) (|Ep|)〛_[Ek @ Ep @ E] = 〚t〛_[Ek @ E].
  65 #E #Ep #t (elim t) -t
  66    [ #n //
  67    | #i #Ek @(leb_elim (S i) (|Ek|)) #Hik
  68      [ >(lift_rel_lt … Hik) >(aa_rel_lt … Hik) >(aa_rel_lt … Hik) //
  69      | >(lift_rel_ge … Hik) >(aa_rel_ge … Hik) <associative_append
  70        >(aa_rel_ge …) (>length_append)
  71        [ >arith2 // @not_lt_to_le /2/ | @(arith3 … Hik) ]
  72      ]
  73    | /4/
  74    | #N #M #IHN #IHM #Ek >lift_lambda >aa_lambda
  75      >commutative_plus >(IHM (? :: ?)) /3/
  76    | #N #M #IHN #IHM #Ek >lift_prod >aa_prod
  77      >commutative_plus >(IHM (? :: ?)) /3/
  78    | #M #IHM #Ek @IHM
  79    ]
  80 qed.
  81
  82 (* substitution lemma arity assignment *)
  83 (* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
  84 lemma aa_subst: ∀v,E,t,Ek. 〚t[|Ek|≝v]〛_[Ek @ E] = 〚t〛_[Ek @ 〚v〛_[E]::E].
  85 #v #E #t (elim t) -t
  86    [ //
  87    | #i #Ek @(leb_elim (S i) (|Ek|)) #H1ik
  88      [ >(aa_rel_lt … H1ik) >(subst_rel1 … H1ik) >(aa_rel_lt … H1ik) //
  89      | @(eqb_elim i (|Ek|)) #H2ik
  90        [ >(aa_rel_ge … H1ik) >H2ik -H2ik H1ik >subst_rel2
  91          >(aa_lift ? ? ? ([])) <minus_n_n /2/
  92        | (lapply (arith4 … H1ik H2ik)) -H1ik H2ik #Hik
  93          (>(subst_rel3 … Hik)) (>aa_rel_ge) [2: /2/ ]
  94           <(associative_append ? ? ([?]) ?)
  95            >aa_rel_ge >length_append (>commutative_plus)
  96            [ <minus_plus // | @not_le_to_not_le_S_S /2/ ]
  97        ]
  98      ]
  99    | //
 100    | #N #M #IHN #IHM #Ek >subst_lambda > aa_lambda
 101      >commutative_plus >(IHM (? :: ?)) /3/
 102    | #N #M #IHN #IHM #Ek >subst_prod > aa_prod
 103      >commutative_plus >(IHM (? :: ?)) /4/
 104    | #M #IHM #Ek @IHM
 105 qed.
 106
 107
 108
 109
 110
 111
 112
 113
 114
 115
 116
 117
 118
 119
 120
 121
 122
 123
 124
 125
 126 (*
 127 (* extensional equality of the interpretations *)
 128 definition eveq: T → T → Prop ≝ λt1,t2. ∀E,K. 〚t1〛_[E, K] ≅ 〚t2〛_[E, K].
 129
 130 interpretation
 131    "extensional equality of the type interpretations"
 132    'napart t1 t2 = (eveq t1 t2).
 133 *)
 134
 135 axiom ev_lift_0_S: ∀t,p,C,E,K. 〚lift t 0 (S p)〛_[C::E, K] ≅ 〚lift t 0 p〛_[E, K].
 136
 137 theorem tj_ev: ∀G,t,u. G ⊢t:u → ∀E,l. l ∈ 〚G〛_[E] → t[l] ∈ 〚u[l]〛_[[], []].
 138 #G #t #u #tjtu (elim tjtu) -G t u tjtu
 139    [ #i #j #_ #E #l #_ >tsubst_sort >tsubst_sort /2 by SAT0_sort/
 140    | #G #u #n #tju #IHu #E #l (elim l) -l (normalize)
 141      [ #_ /2 by SAT1_rel/
 142      | #hd #tl #_ #H (elim H) -H #Hhd #Htl
 143        >lift_0 >delift // >lift_0
 144
 145
 146
 147        (@mem_rceq_trans) [3: @symmetric_rceq @ev_lift_0_S | skip ]
 148
 149 *)
 150 (*
 151 theorem tj_sn: ∀G,A,B. G ⊢A:B → SN A.
 152 #G #A #B #tjAB lapply (tj_trc … tjAB (nil ?) (nil ?)) -tjAB (normalize) /3/
 153 qed.
 154 *)
 155
 156 (*
 157 theorem tev_rel_S: ∀i,R,H. 〚Rel (S i)〛_(R::H) = 〚Rel i〛_(H).
 158 // qed.
 159 *)
 160 (*
 161 theorem append_cons: ∀(A:Type[0]). ∀(l1,l2:list A). ∀a.
 162                      (a :: l1) @ l2 = a :: (l1 @ l2).
 163 // qed.
 164 *)