Commits

Paweł Wieczorek committed 0d7de0e

strengthened rule FUN_I works well

Comments (0)

Files changed (5)

 Nbe/Model/Interp.v
 Nbe/Model/Valid.v
 Nbe/Model/Terminating.v
+Nbe/Model/LogRelTm.v
+Nbe/Model/LogRelSb.v
 Nbe/Model/LogRel.v
 Nbe/Model.v
 
   Nbe/Model/Interp.v\
   Nbe/Model/Valid.v\
   Nbe/Model/Terminating.v\
+  Nbe/Model/LogRelTm.v\
+  Nbe/Model/LogRelSb.v\
   Nbe/Model/LogRel.v\
   Nbe/Model.v\
   Nbe/Extraction/Eval.v\

Nbe/Model/LogRelSb.v

 
 Lemma Rel_Fundamental_Abs: forall Gamma Delta A B M SB dt DT DT' (HDT: DT === DT' #in# PerType) denv,
   Gamma,, A |-- M : B ->
+  (forall (Delta : Cxt) (SB : Sb) (denv : DEnv),
+      Delta ||-  [SB]:Gamma #aeq# denv ->
+      forall (DT DT' : D) (HDT : DT === DT' #in# PerType),
+      EvalTm A denv DT -> Delta ||- TmSb A SB #in# HDT
+  ) ->
   ( forall (Delta : Cxt) (SB : Sb) (denv : DEnv),
       Delta ||-  [SB]:Gamma,, A #aeq# denv ->
       forall (DT DT' : D) (HDT : DT === DT' #in# PerType) (dt : D),
 Proof.
 
 intros.
+rename H0 into Hnew.
+rename H1 into H0.
+rename H2 into H1.
+rename H3 into H2.
+rename H4 into H3.
+
 Print EvalTm.
 Print EQ_SBSEQ.
 (* destroying HDT *)
 eapply System.SB.
 eauto.
 eapply FUN_I.
+
+assert (Gamma ,, A |--) as HYY1.
+eauto.
+clear_inversion HYY1.
+auto.
 auto.
 
 (**)
 split.
 auto.
 (**)
- 
-admit.
+
+eauto. 
 
 (**)
 
 
 
 assert (Delta ||- TmSb A SB #in# HDA) as HYY3.
-admit.
+eauto.
 
 assert (Delta0 ||- [Sseq SB (Sups i)] : Gamma #aeq# denv) as HYY4.
 eapply RelSb_ClosedUnderLift.
 eapply Rel_Fundamental_App; eauto.
 
 (* TmAbs *)
-
+ H : forall (Delta : Cxt) (SB : Sb) (denv : DEnv),
+      Delta ||-  [SB]:Gamma #aeq# denv ->
+      forall (DT DT' : D) (HDT : DT === DT' #in# PerType),
+      EvalTm A denv DT -> Delta ||- TmSb A SB #in# HDT
 eapply Rel_Fundamental_Abs; eauto.
 
 (* Tm0 *)

Nbe/Syntax/Inversion.v

 .
 Proof.
 apply System_ind; intros; eauto.
-clear_inversion H; eauto.
+(*clear_inversion H; eauto.*)
 (* clear_inversion H; eauto. *)
 Qed.
 
 Proof.
 apply System_ind; intros; repeat split; program_simpl; eauto.
 (**)
+
+(*
 assert (G,,A0,,A |-- ).
 destruct ContextWellFormedness.
 program_simpl.
 clear_inversion H0.
 clear_inversion H3.
 auto.
+*)
+
 (*
 assert (G,,A0,,A |--).
 destruct ContextWellFormedness.

Nbe/Syntax/System.v

   Gamma |-- TmApp M N : TmSb B (Ssing N)
 
 | FUN_I: forall Gamma M A B,
+  Gamma    |-- A ->
   Gamma,,A |-- M : B ->
   Gamma    |-- TmAbs A M : TmFun A B