1. Paweł Wieczorek
  2. MgrCoq

Commits

Paweł Wieczorek  committed 29ad72f

copy

  • Participants
  • Parent commits d7b738e
  • Branches another_weird_rule

Comments (0)

Files changed (2)

File Nbe/Model/LogRelSb.v

View file
+
 (******************************************************************************
  * Pawel Wieczorek
  *)
 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,
   Gamma |-- A ->
 
 (**)
 
+destruct RelType_Reify_ as [NFA' [HNFA1' HNFA''] ].
+renamer.
+
 
 Qed.
 

File Nbe/Model/LogRelTm.v

View file
  *)
 
 
-(*
-Lemma RelTerm_Var: forall DT DT' (HDT : DT === DT' #in# PerType) Gamma T,
-  
-  Gamma ||- TmVar : T #aeq# Dup DT (Dvar (length Gamma)) #in# HDT
-.
-
-  var := Dvar (length Gamma) : DNe
-  dv := Dup DA var : D
-*)
-
 Lemma TmVar_Sups_tmVar: forall i Delta  Gamma A,
   CxtShift Delta i (Gamma,,A) ->
   Delta |-- TmSb TmVar (Sups i) === tmVar i : TmSb (TmSb A Sup) (Sups i)