Paweł Wieczorek avatar Paweł Wieczorek committed e6f2e36

Removed admint in Valid.v

Comments (0)

Files changed (3)

Nbe/Model/LogRelSb.v

 eauto.
 Qed.
 
-
-Lemma NoApp_On_Tp: forall Gamma A B,
-  ~ Gamma |-- TmApp A B.
-Proof.
-intros. intro H.
-remember (TmApp A B).
-induction H.
-inversion  Heqt.
-inversion  Heqt.
-inversion  Heqt.
-inversion  Heqt.
-inversion  Heqt.
-Qed.
-
-
-Lemma TmVar_ext: forall Gamma T,
-  Gamma |-- TmVar : T ->
-  exists Psi S, Gamma = (Psi,,S).
-Proof.
-intros.
-
-remember TmVar.
-induction H;  try solve [clear_inversion Heqt].
-eexists.
-eexists.
-eauto.
-
-edestruct IHWtTm.
-auto.
-destruct H1.
-eexists.
-eexists.
-eauto.
-Qed.  
-
-Lemma tmVar_ext: forall i Gamma T,
-  Gamma |-- tmVar i : T ->
-  exists Psi S, Gamma = (Psi,,S).
-Proof.
-induction i; intros.
-simpl in *.
-eapply TmVar_ext.
-eauto.
-
-simpl in H.
-edestruct Inversion_SB as [Delta [C [HX1 [HX2 HX3]]]].
-eauto.
-clear_inversion HX1.
-eexists.
-eexists.
-eauto.
-Qed.
-
-(*
-Lemma tmVar_cxt: forall i Gamma Delta T,
-  Gamma |-- tmVar i : T ->
-  Gamma |-- [Sups i] : Delta ->
-  exists A Psi,
-    Psi,,A |-- TmVar : TmSb A Sup /\ Delta = (Psi,,A) /\ Gamma |-- TmSb A (Sups (S i)) === T
-.
-Proof.
-induction i; intros.
-
-simpl in *.
-clear_inversion H0.
-
-edestruct TmVar_ext.
-eauto.
-edestruct H0.
-subst.
-rename x into CXT.
-rename x0 into C.
-exists C.
-exists CXT.
-split; auto.
-split; auto.
-
-edestruct TmVar_ext as [DCXT [D] ].
-eauto.
-inversion H2; subst.
-
-
-(**)
-
-simpl in *.
-
-edestruct Inversion_SB as [Sigma [C [HX1 [HX2 HX3]  ] ] ].
-eauto.
-clear_inversion HX1.
-clear_inversion H0.
-clear_inversion H5.
-
-specialize (IHi _ _ _ HX2 H7).
-
-destruct IHi as [TA [Tpsi [IH1 IH2] ] ].
-exists TA.
-exists Tpsi.
-subst.
-
-split; auto.
-
-Qed.
-*)
-
-(*
-Lemma tmVar_sups: forall i Gamma Delta T,
-  Gamma |-- tmVar i : T ->
-  Gamma |-- [Sups i] : Delta ->
-  Gamma |-- tmVar i === TmSb TmVar (Sups i) : T
-.
-Proof.
-induction i; intros.
-simpl in *.
-
-eapply EQ_SYM.
-eapply EQ_SBID.
-eauto.
-
-edestruct tmVar_ext as [Psi [C HPsi]].
-eauto.
-subst.
-simpl.
-
-assert (Psi,, C |--) as HX2.
-eauto.
-
-clear_inversion HX2.
-simpl in *.
-
-clear_inversion H0.
-clear_inversion H6.
-
-edestruct Inversion_SB.
-eauto.
-destruct H0.
-destruct H0.
-destruct H2.
-rename x into Gamma.
-clear_inversion H0.
-rename x0 into TT.
-
-edestruct tmVar_cxt as [TA [TCXT [HT1 HT2] ] ].
-eauto.
-eauto.
-subst.
-
-
-eapply EQ_SYM.
-eapply EQ_TRANS.
-eapply EQ_SYM.
-eapply EQ_CONV.
-eapply EQ_SBSEQ.
-eauto.
-eauto.
-eauto.
-
-
-Qed.
-*)
-
-(*
-Lemma tmVar_sups: forall j Gamma i T,
-  Gamma |-- tmVar i : T ->
-  Gamma |-- TmSb (tmVar i) (Sups j) === tmVar (i+j) : TmSb T (Sups j)
-.
-Proof.
-induction j.
-intros.
-simpl.
-rewrite plus_comm.
-simpl.
-eapply EQ_SBID.
-eapply CONV.
-eauto.
-eapply EQ_TP_SYM.
-eapply EQ_TP_SBID.
-eauto.
-
-intros.
-simpl.
-rewrite plus_comm.
-simpl.
-
-edestruct tmVar_ext as [Psi [S HPsi]].
-eauto.
-
-subst.
-
-assert (Psi,, S |--) as HX2.
-eauto.
-
-clear_inversion HX2.
-
-destruct i.
-simpl in *.
-rewrite plus_comm; simpl.
-eapply EQ_SYM.
-eapply EQ_TRANS.
-eapply EQ_CONV.
-eapply EQ_CONG_SB.
-eapply EQ_SB_REFL.
-eauto.
-
-eapply EQ_SYM.
-eapply IHj.
-eauto.
-
-eauto.
-
-
-Qed.
-*)
-
-Lemma RbNe_Lift: forall d nd Gamma,
-  RbNe (length Gamma) d nd -> forall Delta nd' A i,
-  Gamma |-- A === nd ->
-  CxtShift Gamma i Delta ->
-  RbNe (length Delta) d nd' ->
-  Delta |-- nd' === TmSb nd (Sups i)
-.
-Proof.
-intros d nd Gamma H1.
-remember (length Gamma).
-induction H1; intros.
-(**)
-
-clear_inversion H1.
-induction i.
-clear_inversion H0.
-admit.
-
-
-
-admit.
-
-(**)
-absurd (Gamma |-- TmApp ne nd).
-eapply NoApp_On_Tp.
-eauto.
-(**)
-absurd (Gamma |-- TmApp TmS n).
-eapply NoApp_On_Tp.
-eauto.
-(**)
-absurd (Gamma |-- TmApp (TmAbsurd A) n).
-eapply NoApp_On_Tp.
-eauto.
-Qed.
-
+ 
 
 
 Theorem Rel_Fundamental_Absurd: forall Gamma A Delta SB denv DT DT' (HDT : DT === DT' #in# PerType) dt,
 clear_inversion H8.
 clear_inversion H3.
 
-dependent inversion HDT; subst.
+2dependent inversion HDT; subst.
 
 rename i into HDempty.
 rename i0 into HInterp.
 eauto.
 clear_inversion HXXX4.
 inversion H5; subst.
-
+ 
 edestruct H10 as [ne [Hne1 Hne2]].
 edestruct H8 as [NFA [HNFA1 HNFA2]].
 eexists.
 
 (**)
 
+
+
+assert (Delta1 |-- TmSb (TmApp (TmSb (TmSb (TmAbsurd A) SB) (Sups i)) a) (Sups i0) === TmApp (TmAbsurd (TmSb A (Sseq SB (Sups (i + i0))))) (TmSb a (Sups i0)) : TmSb (TmSb (TmSb A (Sseq SB Sup)) (Sext (Sups i) a)) (Sups i0)) as HZZ3.
+
+eapply EQ_TRANS.
+eapply EQ_CONG_SB.
+eauto.
+eapply EQ_CONV.
+eapply EQ_CONG_FUN_E.
+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_REFL.
+eapply FUN_F.
+eapply SB_F.
+eauto.
+eauto.
+
+eapply SB_F.
+eauto.
+eapply SB_F.
+eauto.
+eauto.
+eapply EQ_REFL.
+eauto.
+
+
+(*
 destruct RelType_Reify_ as [NFA' [HNFA1' HNFA''] ].
 renamer.
-admit.
+*)
+
+
 
 Qed.
 

Nbe/Model/Valid.v

 
 (* App *)
 
-admit.
-(* WEIRD rule 
 constructor 1; auto; intros; extract_vals; reds; eauto.
 
 compute_sth; apply_valenvs.
 program_simpl.
 reds.
 compute_sth.
-renamer.
-clear_inversion H24.
+renamer. 
+clear_inversion H25.
 repeat progress (elim_extdeter; clear_dups).
 
 assert (DN_env0 === DN_env1 #in# PDA_env0).
-apply H5; eauto.
+apply H0; eauto.
 
 destruct H with DN_env0 DN_env1 as [y1 HH].
-apply H2; eauto.
+apply H0; eauto.
 destruct HH as [y2 HH].
 destruct HH as [Y HH].
 program_simpl; renamer.
 repeat split; eauto.
 red.
 intuition.
-destruct H34 with DN_env0; eauto. 
+destruct H35 with DN_env0; eauto. 
 
 exists x; repeat split.
 apply evalSb with (Dext env0 DN_env0).
 unfold Ssing; eauto.
 clear_inversion H15; eauto.
-apply H27 with DN_env0. eauto. auto. auto.
-*)
+eauto.
 
 (* 0 *)
 

Nbe/Syntax/System.v

 
 Combined Scheme System_ind from WfCxt_dind, WfTp_dind, WtTm_dind, WtSb_dind, WtTpEq_dind, WtTmEq_dind, WtSbEq_dind.
 
+Lemma EQ_TP_SBSEQ3: forall SB1 SB2 SB3 Delta1 Delta2 Delta3 Gamma A,
+   
+    Gamma |-- [SB1] : Delta1 ->
+    Delta1 |-- [SB2] : Delta2 ->
+    Delta2 |-- [SB3] : Delta3 ->   
+    Delta3 |-- A ->
+    Gamma |-- TmSb (TmSb (TmSb A SB3) SB2) SB1 === TmSb A (Sseq SB3 (Sseq SB2 SB1))
+.
+Proof.
+intros.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+eauto.
+Qed.
+
 
 (******************************************************************************
  * Test :)
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.