matita/matita/lib/lambda/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 "lambda/rc_sat.ma".
  16
  17 (* THE EVALUATION *************************************************************)
  18
  19 (* The interpretation of a type t as a r.c. denoted by 〚t〛.
  20  * For the "conv" rule we need 〚M〛 ≈ 〚N〛 when M and N are convertible, so:
  21  * 1) 〚(λB.M N)〛 ≈ 〚N[0≝N]〛 implies that 〚(M N)〛 and 〚λB.M〛 are evaluated by
  22  *    stacking the application arguments like a reduction machine does
  23  * 2) ∀M,N. 〚D M〛 ≈ 〚D N〛, implies that 〚D M〛 must be a constant.
  24  *)
  25 let rec ev E K t on t : RC ≝ match t with (* E: environment, K: stack *)
  26    [ Sort _     ⇒ snRC                               (* from λ→ *)
  27    | Rel i      ⇒ nth i … E snRC                     (* from F *)
  28    | App M N    ⇒ ev E (ev E ([]) N :: K) M          (* machine-like push *)
  29    | Lambda _ M ⇒ ev (hd … K snRC :: E) (tail … K) M (* machine-like pop *)
  30    | Prod N M   ⇒ let C ≝ (ev E ([]) N) in
  31                   depRC C (ev (C :: E) K M)          (* from λ→ and F *)
  32    | D _        ⇒ snRC                               (* see note 2 above *)
  33    ].
  34
  35 interpretation "interpretation of a type" 'Eval2 t E K = (ev E K t).
  36
  37 (* extensional equality of the interpretations *)
  38 definition eveq: T → T → Prop ≝ λt1,t2. ∀E,K. 〚t1〛_[E, K] ≅ 〚t2〛_[E, K].
  39
  40 interpretation
  41    "extensional equality of the type interpretations"
  42    'napart t1 t2 = (eveq t1 t2).
  43
  44 (* The interpretation of a context of types as a context of r.c.'s *)
  45 let rec cev E G on G : list RC ≝ match G with
  46    [ nil      ⇒ E
  47    | cons t F ⇒ let D ≝ cev E F in 〚t〛_[D,[]] :: D
  48    ].
  49
  50 interpretation "interpretation of a context" 'Eval1 G E = (cev E G).
  51
  52 theorem ev_app: ∀M,N,E,K. 〚App M N〛_[E, K] = 〚M〛_[E, 〚N〛_[E,[]]::K].
  53 // qed.
  54
  55 theorem ev_lambda: ∀M,N,E,K.
  56                    〚Lambda N M〛_[E, K] = 〚M〛_[hd … K snRC :: E, tail … K].
  57 // qed.
  58
  59 theorem ev_prod: ∀M,N,E,K.
  60                  〚Prod N M〛_[E,K] = depRC (〚N〛_[E,[]]) (〚M〛_[〚N〛_[E,[]]::E,K]).
  61 // qed.
  62
  63 theorem ev_repl: ∀t,E1,E2,K1,K2. E1 ≅ E2 → K1 ≅ K2 → 〚t〛_[E1,K1] ≅ 〚t〛_[E2,K2].
  64 #t (elim t) /5/
  65 qed.
  66
  67 theorem ev_rel_lt: ∀K,D,E,i. (S i) ≤ |E| → 〚Rel i〛_[E @ D, K] = 〚Rel i〛_[E,K].
  68 #K #D #E (elim E) -E [1: #i #Hie (elim (not_le_Sn_O i)) #Hi (elim (Hi Hie)) ]
  69 #C #F #IHE #i (elim i) -i // #i #_ #Hie @IHE @le_S_S_to_le @Hie
  70 qed.
  71
  72 theorem ev_rel_ge: ∀K,D,E,i. (S i) ≰ |E| →
  73                    〚Rel i〛_[E @ D, K] = 〚Rel (i-|E|)〛_[D,K].
  74 #K #D #E (elim E) -E [ normalize // ]
  75 #C #F #IHE #i (elim i) -i [1: -IHE #Hie (elim Hie) -Hie #Hie (elim (Hie ?)) /2/ ]
  76 normalize #i #_ #Hie @IHE /2/
  77 qed.
  78
  79 theorem ev_app_repl: ∀M1,M2,N1,N2. M1 ≈ M2 → N1 ≈ N2 →
  80                      App M1 N1 ≈ App M2 N2.
  81 #M1 #M2 #N1 #N2 #IHM #IHN #E #K >ev_app (@transitive_rceq) /3/
  82 qed.
  83
  84 theorem ev_lambda_repl: ∀N1,N2,M1,M2. N1 ≈ N2 → M1 ≈ M2 →
  85                         Lambda N1 M1 ≈ Lambda N2 M2.
  86 #N1 #N2 #M1 #M2 #IHN #IHM #E #K >ev_lambda (@transitive_rceq) //
  87 qed.
  88
  89 theorem ev_prod_repl: ∀N1,N2,M1,M2. N1 ≈ N2 → M1 ≈ M2 →
  90                       Prod N1 M1 ≈ Prod N2 M2.
  91 #N1 #N2 #M1 #M2 #IHN #IHM #E #K >ev_prod @dep_repl //
  92 (@transitive_rceq) [2: @IHM | skip ] /3/
  93 qed.
  94
  95 (* weakeing and thinning lemma for the type interpretation *)
  96 (* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
  97 theorem ev_lift: ∀E,Ep,t,Ek,K.
  98                  〚lift t (|Ek|) (|Ep|)〛_[Ek @ Ep @ E, K] ≅ 〚t〛_[Ek @ E, K].
  99 #E #Ep #t (elim t) -t
 100    [ #n >lift_sort /by SAT0_sort/
 101    | #i #Ek #K @(leb_elim (S i) (|Ek|)) #Hik
 102      [ >(lift_rel_lt … Hik) >(ev_rel_lt … Hik) >(ev_rel_lt … Hik) //
 103      | >(lift_rel_ge … Hik) >(ev_rel_ge … Hik) <associative_append
 104        >(ev_rel_ge …) (>length_append)
 105        [ >arith2 // @not_lt_to_le /2/ | @(arith3 … Hik) ]
 106      ]
 107    | #M #N #IHM #IHN #Ek #K >lift_app >ev_app (@transitive_rceq) /3/
 108    | #N #M #IHN #IHM #Ek #K >lift_lambda >ev_lambda (@transitive_rceq)
 109      [2: >commutative_plus @(IHM (? :: ?)) | skip ] //
 110    | #N #M #IHN #IHM #Ek #K >lift_prod >ev_prod (@dep_repl) //
 111      (@transitive_rceq) [2: >commutative_plus @(IHM (? :: ?)) | skip ] /3/
 112    | //
 113    ]
 114 qed.
 115
 116 (*
 117 theorem tj_ev: ∀G,A,B. G ⊢A:B → ∀H,l. l ∈ 〚G〛_(H) → A[l] ∈ 〚B[l]〛_〚G〛_(H).
 118 #G #A #B #tjAB (elim tjAB) -G A B tjAB
 119    [ #i #j #_ #H #l #_ >substc_sort >substc_sort /2 by SAT0_sort/
 120    | #G #B #n #tjB #IH #H #l (elim l) -l (normalize)
 121      [ #_ /2 by SAT1_rel/
 122      | #C #D #IHl #mem (elim mem) -mem #mem #memc
 123        >lift_0 >delift // >lift_0
 124
 125 *)
 126 (*
 127 theorem tj_sn: ∀G,A,B. G ⊢A:B → SN A.
 128 #G #A #B #tjAB lapply (tj_trc … tjAB (nil ?) (nil ?)) -tjAB (normalize) /3/
 129 qed.
 130 *)
 131
 132 (*
 133 theorem tev_rel_S: ∀i,R,H. 〚Rel (S i)〛_(R::H) = 〚Rel i〛_(H).
 134 // qed.
 135 *)
 136 (*
 137 theorem append_cons: ∀(A:Type[0]). ∀(l1,l2:list A). ∀a.
 138                      (a :: l1) @ l2 = a :: (l1 @ l2).
 139 // qed.
 140 *)