X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda%2Frc_eval.ma;h=3fdeed41025b2fc7783e720bbe2c42b0effd859e;hb=bfafdf7d8313ddd24c06d8ce3bba874f780403a9;hp=515c674213ae139a4c56b10098a7fe2478eeeaa1;hpb=8d0c0ab4df0d236e3b57e3b3feccae5fed2f6ad8;p=helm.git

diff --git a/matita/matita/lib/lambda/rc_eval.ma b/matita/matita/lib/lambda/rc_eval.ma
index 515c67421..3fdeed410 100644
--- a/matita/matita/lib/lambda/rc_eval.ma
+++ b/matita/matita/lib/lambda/rc_eval.ma
@@ -12,115 +12,138 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda/rc_sat.ma".
+include "lambda/rc_hsat.ma".
 
 (* THE EVALUATION *************************************************************)
 
-(* The interpretation of a type t as a r.c. denoted by 〚t〛.
- * For the "conv" rule we need 〚M〛 ≈ 〚N〛 when M and N are convertible, so:
- * 1) 〚(λB.M N)〛 ≈ 〚N[0≝N]〛 implies that 〚(M N)〛 and 〚λB.M〛 are evaluated by
- *    stacking the application arguments like a reduction machine does
- * 2) ∀M,N. 〚D M〛 ≈ 〚D N〛, implies that 〚D M〛 must be a constant.
- *)
-let rec ev E K t on t : RC ≝ match t with (* E: environment, K: stack *)
-   [ Sort _     ⇒ snRC                               (* from λ→ *)
-   | Rel i      ⇒ nth i … E snRC                     (* from F *)
-   | App M N    ⇒ ev E (ev E ([]) N :: K) M          (* machine-like push *)
-   | Lambda _ M ⇒ ev (hd … K snRC :: E) (tail … K) M (* machine-like pop *)
-   | Prod N M   ⇒ let C ≝ (ev E ([]) N) in
-                  depRC C (ev (C :: E) K M)          (* from λ→ and F *)
-   | D _        ⇒ snRC                               (* see note 2 above *)
+(* The arity of a term t in an environment E *)
+let rec aa E t on t ≝ match t with
+   [ Sort _     ⇒ SORT
+   | Rel i      ⇒ nth i … E SORT
+   | App M N    ⇒ pred (aa E M)
+   | Lambda N M ⇒ let Q ≝ aa E N in ABST Q (aa (Q::E) M)
+   | Prod N M   ⇒ aa ((aa E N)::E) M
+   | D M        ⇒ aa E M
    ].
 
-interpretation "interpretation of a type" 'Eval2 t E K = (ev E K t).
+interpretation "arity assignment (term)" 'Eval1 t E = (aa E t).
 
-(* extensional equality of the interpretations *)
-definition eveq: T → T → Prop ≝ λt1,t2. ∀E,K. 〚t1〛_[E, K] ≅ 〚t2〛_[E, K].
-
-interpretation 
-   "extensional equality of the type interpretations"
-   'napart t1 t2 = (eveq t1 t2).
-
-(* The interpretation of a context of types as a context of r.c.'s *)
-let rec cev E G on G : list RC ≝ match G with
+(* The arity of a type context *)
+let rec caa E G on G ≝ match G with
    [ nil      ⇒ E
-   | cons t F ⇒ let D ≝ cev E F in 〚t〛_[D,[]] :: D
+   | cons t F ⇒ let D ≝ caa E F in 〚t〛_[D] :: D
    ].
 
-interpretation "interpretation of a context" 'Eval1 G E = (cev E G).
+interpretation "arity assignment (type context)" 'Eval1 G E = (caa E G).
 
-theorem ev_app: ∀M,N,E,K. 〚App M N〛_[E, K] = 〚M〛_[E, 〚N〛_[E,[]]::K].
+lemma aa_app: ∀M,N,E. 〚App M N〛_[E] = pred (〚M〛_[E]).
 // qed.
 
-theorem ev_lambda: ∀M,N,E,K.
-                   〚Lambda N M〛_[E, K] = 〚M〛_[hd … K snRC :: E, tail … K].
+lemma aa_lambda: ∀M,N,E. 〚Lambda N M〛_[E] = ABST (〚N〛_[E]) (〚M〛_[〚N〛_[E]::E]).
 // qed.
 
-theorem ev_prod: ∀M,N,E,K.
-                 〚Prod N M〛_[E,K] = depRC (〚N〛_[E,[]]) (〚M〛_[〚N〛_[E,[]]::E,K]).
+lemma aa_prod: ∀M,N,E. 〚Prod N M〛_[E] = 〚M〛_[〚N〛_[E]::E].
 // qed.
 
-theorem ev_repl: ∀t,E1,E2,K1,K2. E1 ≅ E2 → K1 ≅ K2 → 〚t〛_[E1,K1] ≅ 〚t〛_[E2,K2].
-#t (elim t) /5/
-qed.
-
-theorem ev_rel_lt: ∀K,D,E,i. (S i) ≤ |E| → 〚Rel i〛_[E @ D, K] = 〚Rel i〛_[E,K].
-#K #D #E (elim E) -E [1: #i #Hie (elim (not_le_Sn_O i)) #Hi (elim (Hi Hie)) ]
+lemma aa_rel_lt: ∀D,E,i. (S i) ≤ |E| → 〚Rel i〛_[E @ D] = 〚Rel i〛_[E].
+#D #E (elim E) -E [1: #i #Hie (elim (not_le_Sn_O i)) #Hi (elim (Hi Hie)) ]
 #C #F #IHE #i (elim i) -i // #i #_ #Hie @IHE @le_S_S_to_le @Hie
 qed.
 
-theorem ev_rel_ge: ∀K,D,E,i. (S i) ≰ |E| →
-                   〚Rel i〛_[E @ D, K] = 〚Rel (i-|E|)〛_[D,K].
-#K #D #E (elim E) -E [ normalize // ]
+lemma aa_rel_ge: ∀D,E,i. (S i) ≰ |E| →
+                   〚Rel i〛_[E @ D] = 〚Rel (i-|E|)〛_[D].
+#D #E (elim E) -E [ normalize // ]
 #C #F #IHE #i (elim i) -i [1: -IHE #Hie (elim Hie) -Hie #Hie (elim (Hie ?)) /2/ ]
 normalize #i #_ #Hie @IHE /2/
 qed.
 
-theorem ev_app_repl: ∀M1,M2,N1,N2. M1 ≈ M2 → N1 ≈ N2 →
-                     App M1 N1 ≈ App M2 N2.
-#M1 #M2 #N1 #N2 #IHM #IHN #E #K >ev_app (@transitive_rceq) /3/
-qed.
-
-theorem ev_lambda_repl: ∀N1,N2,M1,M2. N1 ≈ N2 → M1 ≈ M2 →
-                        Lambda N1 M1 ≈ Lambda N2 M2.
-#N1 #N2 #M1 #M2 #IHN #IHM #E #K >ev_lambda (@transitive_rceq) //
-qed.
-
-theorem ev_prod_repl: ∀N1,N2,M1,M2. N1 ≈ N2 → M1 ≈ M2 →
-                      Prod N1 M1 ≈ Prod N2 M2.
-#N1 #N2 #M1 #M2 #IHN #IHM #E #K >ev_prod @dep_repl //
-(@transitive_rceq) [2: @IHM | skip ] /3/
-qed. 
-
-(* weakeing and thinning lemma for the type interpretation *)
+(* weakeing and thinning lemma arity assignment *)
 (* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
-theorem ev_lift: ∀E,Ep,t,Ek,K.
-                 〚lift t (|Ek|) (|Ep|)〛_[Ek @ Ep @ E, K] ≅ 〚t〛_[Ek @ E, K].
+lemma aa_lift: ∀E,Ep,t,Ek.
+                 〚lift t (|Ek|) (|Ep|)〛_[Ek @ Ep @ E] = 〚t〛_[Ek @ E].
 #E #Ep #t (elim t) -t
-   [ #n >lift_sort /by SAT0_sort/
-   | #i #Ek #K @(leb_elim (S i) (|Ek|)) #Hik
-     [ >(lift_rel_lt … Hik) >(ev_rel_lt … Hik) >(ev_rel_lt … Hik) //
-     | >(lift_rel_ge … Hik) >(ev_rel_ge … Hik) <associative_append
-       >(ev_rel_ge …) (>length_append)
+   [ #n //
+   | #i #Ek @(leb_elim (S i) (|Ek|)) #Hik
+     [ >(lift_rel_lt … Hik) >(aa_rel_lt … Hik) >(aa_rel_lt … Hik) //
+     | >(lift_rel_ge … Hik) >(aa_rel_ge … Hik) <associative_append
+       >(aa_rel_ge …) (>length_append)
        [ >arith2 // @not_lt_to_le /2/ | @(arith3 … Hik) ]
      ]
-   | #M #N #IHM #IHN #Ek #K >lift_app >ev_app (@transitive_rceq) /3/
-   | #N #M #IHN #IHM #Ek #K >lift_lambda >ev_lambda (@transitive_rceq)
-     [2: >commutative_plus @(IHM (? :: ?)) | skip ] //
-   | #N #M #IHN #IHM #Ek #K >lift_prod >ev_prod (@dep_repl) //
-     (@transitive_rceq) [2: >commutative_plus @(IHM (? :: ?)) | skip ] /3/
-   | //
+   | /4/
+   | #N #M #IHN #IHM #Ek >lift_lambda >aa_lambda
+     >commutative_plus >(IHM (? :: ?)) /3/
+   | #N #M #IHN #IHM #Ek >lift_prod >aa_prod
+     >commutative_plus >(IHM (? :: ?)) /3/
+   | #M #IHM #Ek @IHM
    ]
 qed.
 
+(* substitution lemma arity assignment *)
+(* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
+lemma aa_subst: ∀v,E,t,Ek. 〚t[|Ek|≝v]〛_[Ek @ E] = 〚t〛_[Ek @ 〚v〛_[E]::E].
+#v #E #t (elim t) -t
+   [ //
+   | #i #Ek @(leb_elim (S i) (|Ek|)) #H1ik
+     [ >(aa_rel_lt … H1ik) >(subst_rel1 … H1ik) >(aa_rel_lt … H1ik) //
+     | @(eqb_elim i (|Ek|)) #H2ik
+       [ >(aa_rel_ge … H1ik) >H2ik -H2ik H1ik >subst_rel2
+         >(aa_lift ? ? ? ([])) <minus_n_n /2/
+       | (lapply (arith4 … H1ik H2ik)) -H1ik H2ik #Hik
+         (>(subst_rel3 … Hik)) (>aa_rel_ge) [2: /2/ ] 
+          <(associative_append ? ? ([?]) ?) 
+           >aa_rel_ge >length_append (>commutative_plus)
+           [ <minus_plus // | @not_le_to_not_le_S_S /2/ ]
+       ]
+     ]
+   | //
+   | #N #M #IHN #IHM #Ek >subst_lambda > aa_lambda
+     >commutative_plus >(IHM (? :: ?)) /3/
+   | #N #M #IHN #IHM #Ek >subst_prod > aa_prod
+     >commutative_plus >(IHM (? :: ?)) /4/
+   | #M #IHM #Ek @IHM
+qed.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
 (*
-theorem tj_ev: ∀G,A,B. G ⊢A:B → ∀H,l. l ∈ 〚G〛_(H) → A[l] ∈ 〚B[l]〛_〚G〛_(H).
-#G #A #B #tjAB (elim tjAB) -G A B tjAB
-   [ #i #j #_ #H #l #_ >substc_sort >substc_sort /2 by SAT0_sort/
-   | #G #B #n #tjB #IH #H #l (elim l) -l (normalize) 
+(* extensional equality of the interpretations *)
+definition eveq: T → T → Prop ≝ λt1,t2. ∀E,K. 〚t1〛_[E, K] ≅ 〚t2〛_[E, K].
+
+interpretation 
+   "extensional equality of the type interpretations"
+   'napart t1 t2 = (eveq t1 t2).
+*)
+
+axiom ev_lift_0_S: ∀t,p,C,E,K. 〚lift t 0 (S p)〛_[C::E, K] ≅ 〚lift t 0 p〛_[E, K].
+
+theorem tj_ev: ∀G,t,u. G ⊢t:u → ∀E,l. l ∈ 〚G〛_[E] → t[l] ∈ 〚u[l]〛_[[], []].
+#G #t #u #tjtu (elim tjtu) -G t u tjtu
+   [ #i #j #_ #E #l #_ >tsubst_sort >tsubst_sort /2 by SAT0_sort/
+   | #G #u #n #tju #IHu #E #l (elim l) -l (normalize)
      [ #_ /2 by SAT1_rel/
-     | #C #D #IHl #mem (elim mem) -mem #mem #memc
-       >lift_0 >delift // >lift_0 
+     | #hd #tl #_ #H (elim H) -H #Hhd #Htl
+       >lift_0 >delift // >lift_0
+       
+       
+       
+       (@mem_rceq_trans) [3: @symmetric_rceq @ev_lift_0_S | skip ] 
 
 *)
 (* 
@@ -137,4 +160,4 @@ theorem tev_rel_S: ∀i,R,H. 〚Rel (S i)〛_(R::H) = 〚Rel i〛_(H).
 theorem append_cons: ∀(A:Type[0]). ∀(l1,l2:list A). ∀a.
                      (a :: l1) @ l2 = a :: (l1 @ l2).
 // qed.
-*)
\ No newline at end of file
+*)