Commits

Paweł Wieczorek committed 0287072

Added _S case as seperate lemma, not finished

Comments (0)

Files changed (1)

Nbe/Model/LogRelSb.v

 
 Qed.
 
+Theorem Rel_Fundamental_S: forall Gamma Delta SB denv dt DT DT' (HDT : DT === DT' #in# PerType),
+  Gamma |-- ->
+  Delta ||-  [SB]:Gamma #aeq# denv ->
+  EvalTm (TmArr TmNat TmNat) denv DT ->
+  EvalTm TmS denv dt ->
+   Delta ||- TmSb TmS SB : TmSb (TmArr TmNat TmNat) SB #aeq# dt #in# HDT
+.
+Proof.
+assert (H : True) by auto.
+intros.
+
+assert (Delta |-- [SB] : Gamma) as HYY1 by (eapply RelSb_wellformed; eauto).
+
+destruct HDT; try solve [clear_inversion H2].
+simpl.
+repeat (split; auto).
+eauto.
+
+intros.
+
+clear_inversion H2.
+clear_inversion H3.
+clear_inversion H7.
+clear_inversion i0.
+inversion i; subst.
+
+(* OLD *)
+
+assert (Gamma |= TmArr TmNat TmNat) as HV.
+apply Valid_for_WfTp.
+eauto.
+
+clear_inversion HV.
+destruct H2 with (env0 := denv) (env1 := denv) as [DT [DT' [HV1 [HV2 HV3]]]] .
+eapply RelSb_valenv.
+apply H0.
+clear H2.
+
+exists TmNat TmNat.
+
+assert (exists PT, Interp DT PT) as HPT by eauto.
+destruct HPT as [PT HPT].
+exists PT.
+
+clear_inversion HV1.
+clear_inversion H7.
+clear_inversion HV2.
+clear_inversion H7.
+
+repeat (split; auto).
+
+clear_inversion HPT.
+clear_inversion H5.
+apply RelProd_intro.
+intros.
+
+clear_inversion H6.
+clear_inversion po_ro.
+destruct ro_resp_ex with a0 as [Y HY].
+eauto.
+
+ 
+assert (Interp Dnat Y) as HI.
+eapply H7 with a0.
+eauto.
+eauto.
+eauto.
+
+clear_inversion HI.
+
+clear_inversion H2.
+
+exists (Dnv (S n)).
+exists (Dnv (S n)).
+exists PerNat.
+repeat (split; auto).
+
+exists (Dup Dnat (DneS e1)).
+exists (Dup Dnat (DneS e')).
+exists PerNat.
+
+repeat (split; auto).
+unfold Dup; simpl; auto.
+unfold Dup; simpl; auto.
+
+
+apply Reflect_Characterization.
+eauto.
+eauto.
+apply PerNe_intro.
+intros.
+clear_inversion H4.
+destruct H2 with m as [ne [Hne1 Hne2]].
+exists (TmApp TmS ne).
+split; auto.
+ 
+ 
+assert (Delta |--) as HX1.
+eauto.
+
+assert (Delta,, TmSb TmNat SB |--) as HX2.
+eauto.
+
+assert ( Delta,, TmSb TmNat SB |-- TmVar : TmSb TmNat (Sseq SB Sup) ) as HX3.
+eapply CONV.
+eapply HYP; eauto.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+assert ( Delta,, TmSb TmNat SB |--  [Sext (Sseq SB Sup) TmVar] :  Gamma,, TmNat ) as HX4.
+eapply SEXT.
+eapply SSEQ.
+eauto.
+eauto.
+eauto.
+eauto.
+
+
+(**)
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SB_FUN.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_CONG_FUN.
+eauto.
+ 
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_SB_NAT.
+eapply SSEQ.
+eauto.
+eauto.
+
+(**) 
+
+assert (Delta,,  TmNat  |--) as HX5.
+eauto.
+
+assert ( Delta,, TmNat |-- TmVar : TmSb TmNat (Sseq SB Sup) ) as HX6.
+eapply CONV.
+eapply HYP; eauto.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SB_NAT.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SB_NAT.
+eauto.
+
+assert ( Delta,, TmNat |--  [Sext (Sseq SB Sup) TmVar] :  Gamma,, TmNat ) as HX7.
+eapply SEXT.
+eapply SSEQ.
+eauto.
+eauto.
+eauto.
+eauto.
+
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_SB_NAT.
+eapply SSEQ.
+eauto.
+eauto.
+
+(**)
+ 
+generalize dependent i.
+cut (Dnat = Dnat); auto.
+cut (Dnat = Dnat); auto.
+generalize Dnat at 1 5 7 as d0.
+generalize Dnat at 2 4 5  as d1.
+intros.
+destruct i; clear_inversion H2.
+simpl.
+eauto.
+
+(**)
+
+intros.
+
+rename i into HDT.
+rename i1 into HREC.
+
+inversion HPA; subst.
+inversion Happ; subst.
+clear_inversion H9.
+clear_inversion H11.
+clear_inversion H7.
+
+
+
+set (HDT' := HREC da da Dnat DB' PerNat HPA Hda Happ Happ').
+
+generalize dependent HDT'.
+cut (Dnat = Dnat); auto.
+generalize Dnat at 1 3 4.
+intros d HEQ. intros.
+destruct HDT'; try clear_inversion HEQ.
+
+simpl.
+
+inversion Hda; subst.
+
+(**)
+  
+exists (Dnv (S n)).
+repeat (split; auto).
+ 
+eapply EQ_TP_SB_NAT.
+eapply SEXT.
+eauto.
+eauto.
+eapply RelTerm_implies_WtTm.
+eauto.
+ 
+intros.
+edestruct RelTerm_Reify as [v [Hv1 Hv2]].
+eauto.
+eauto.
+
+clear_inversion Hv1.
+
+exists (fromDnv (S n)).
+split; auto.
+simpl.
+
+assert (Delta0 |-- TmSb (TmSb TmS SB) (Sups i0)
+   : TmFun (TmSb TmNat (Sups i0)) TmNat) as HX1.
+eapply CONV.
+eapply Syntax.System.SB.
+eauto.
+eauto.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SB_ARR.
+eauto.
+eauto.
+eauto.
+unfold TmArr.
+eapply EQ_TP_CONG_FUN.
+eauto.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_SB_NAT.
+eauto.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_SB_NAT.
+eauto.
+
+
+eapply EQ_TRANS.
+eapply EQ_CONV.
+eapply EQ_SBAPP.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_SB_NAT.
+eapply SEXT.
+eauto.
+eapply NAT_F.
+eauto.
+eapply Syntax.System.SB.
+eauto.
+eapply CONV.
+eauto.
+eapply EQ_TP_SB_NAT.
+eauto.
+
+(**)
+
+eapply EQ_CONV.
+eapply EQ_CONG_FUN_E.
+eapply EQ_TRANS.
+eapply EQ_CONV.
+eapply EQ_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_SB_ARR.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TRANS.
+eapply EQ_CONV.
+eapply EQ_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SB_ARR.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_CONG_FUN.
+eapply EQ_TP_TRANS with TmNat.
+eapply EQ_TP_SB_NAT.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SB_NAT.
+eauto.
+
+eapply EQ_TP_TRANS with TmNat.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eapply SUP.
+eapply SB_F.
+eauto.
+eauto.
+
+eauto.
+eauto.
+eapply EQ_TP_SB_NAT.
+eapply SSEQ.
+eapply SUP.
+eapply SB_F.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_SYM.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eapply SUP.
+eapply SB_F.
+eauto.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_SB_NAT.
+eapply SSEQ.
+eapply SUP.
+eapply SB_F.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_REFL.
+eapply SUP.
+eauto.
+
+
+(**)
+
+admit.
+admit.
+admit.
+admit.
+admit.
+
+
 Theorem Rel_Fundamental: 
     (forall Gamma, Gamma |-- -> True) /\
 
 
 (* TmS *)
 
+Theorem Rel_Fundamental_S: forall Gamma Delta SB denv dt DT DT' (HDT : DT === DT' #in# PerType),
+  Gamma |-- ->
+  Delta ||-  [SB]:Gamma #aeq# denv ->
+  EvalTm (TmArr TmNat TmNat) denv DT ->
+  EvalTm TmS denv dt ->
+   Delta ||- TmSb TmS SB : TmSb (TmArr TmNat TmNat) SB #aeq# dt #in# HDT
+.
+
 assert (Delta |-- [SB] : Gamma) by (eapply RelSb_wellformed; eauto).
 destruct HDT; try solve [clear_inversion H1].
 simpl.