1. Paweł Wieczorek
  2. MgrCoq

Commits

Paweł Wieczorek  committed 6989058

Finished natural-number-case in the Rel_Fundamental_S lemma

  • Participants
  • Parent commits 6193de5
  • Branches another_weird_rule

Comments (0)

Files changed (1)

File Nbe/Model/LogRelSb.v

View file
 
 Qed.
 
+
+
+
+Lemma fromDnv_subst: forall k Psi sigma Sigma, Psi |-- [sigma] : Sigma -> Psi |-- TmSb (fromDnv k) sigma === fromDnv k : TmNat.
+induction k.
+intros.
+simpl.
+eapply EQ_SBNAT0.
+eauto.
+
+intros.
+simpl.
+eapply EQ_TRANS.
+eapply EQ_CONV.
+eapply EQ_SBAPP.
+eauto.
+eapply NS.
+eauto.
+eauto.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_REFL.
+eapply SEXT.
+eauto.
+eauto.
+eapply CONV.
+specialize (IHk Psi sigma Sigma H).
+assert (Psi |-- TmSb (fromDnv k) sigma : TmNat) as HYY1.
+eauto.
+eauto.
+
+eapply EQ_TP_SYM.
+eapply EQ_TP_SB_NAT.
+eauto.
+eapply EQ_TP_SB_NAT.
+eauto.
+eapply EQ_TP_SB_NAT.
+eapply SEXT.
+eauto.
+eauto.
+eapply System.SB.
+eauto.
+eauto.
+
+eapply EQ_CONV.
+eapply EQ_CONG_FUN_E.
+eapply EQ_SBNATS.
+eauto.
+eauto.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+unfold Ssing.
+eapply SEXT.
+eauto.
+eauto.
+
+eapply CONV.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SB_NAT.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_SB_NAT.
+eapply SSEQ.
+unfold Ssing.
+eapply SEXT.
+eauto.
+eauto.
+
+eapply CONV.
+
+specialize (IHk Psi sigma Sigma H).
+assert (Psi |-- TmSb (fromDnv k) sigma : TmNat) as HYY1.
+eauto.
+eauto.
+
+eapply EQ_TP_SYM.
+eapply EQ_TP_SB_NAT.
+eauto.
+eauto.
+Qed.
+
 Theorem Rel_Fundamental_S: forall Gamma Delta SB denv dt DT DT' (HDT : DT === DT' #in# PerType),
   Gamma |-- ->
   Delta ||-  [SB]:Gamma #aeq# denv ->
 inversion Hda; subst.
 
 (**)
-  
+   
 exists (Dnv (S n)).
 repeat (split; auto).
  
 eapply SUP.
 eauto.
 
-
+ 
 (**)
 
 eapply EQ_TP_TRANS.
 
 (**)
 
+eapply EQ_CONV.
+eapply EQ_SBNATS.
+eauto.
+unfold TmArr.
+eapply EQ_TP_CONG_FUN.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SB_NAT.
+eauto.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SB_NAT.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_CONG_SB.
+eauto.
+eapply EQ_TP_SB_NAT.
+eauto.
+eapply EQ_TP_SB_NAT.
+eauto.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SB_NAT.
+eauto.
+eapply EQ_TP_SYM.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_REFL.
+eauto.
+eapply EQ_TP_SB_NAT.
+eauto.
+eapply EQ_TP_SB_NAT.
+eauto.
+
+eapply EQ_CONV.
+eapply EQ_TRANS.
+eapply EQ_CONG_SB.
+eapply EQ_SB_REFL.
+eauto.
+eauto.
+
+(**)
+
+eapply EQ_CONV.
+eapply fromDnv_subst.
+eauto.
+eapply EQ_TP_SYM.
+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_REFL.
+eauto.
+
+(**)
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+unfold Ssing.
+eapply SEXT.
+eauto.
+eauto.
+
+eapply CONV.
+eapply System.SB.
+eauto.
+eauto.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SB_NAT.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SB_NAT.
+eauto.
+eauto.
+eapply SB_F.
+eauto.
+eauto.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eapply SSEQ.
+unfold Ssing.
+eapply SEXT.
+eauto.
+eauto.
+
+
+eapply CONV.
+eapply System.SB.
+eauto.
+eauto.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SB_NAT.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SB_NAT.
+eauto.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_SB_NAT.
+eapply SSEQ.
+eapply SSEQ.
+unfold Ssing.
+eapply SEXT.
+eauto.
+eauto.
+
+eapply CONV.
+eapply System.SB.
+eauto.
+eauto.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SB_NAT.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SB_NAT.
+eauto.
+eauto.
+eauto.
+
+(* SECOND CASE *)
+
 admit.
+
+Qed.
+
+
+Theorem Rel_Fundamental_Absurd: forall Gamma A Delta SB denv DT DT' (HDT : DT === DT' #in# PerType) dt,
+  Gamma |-- A ->
+  (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) ->
+  Delta ||-  [SB]:Gamma #aeq# denv ->
+  EvalTm (TmArr TmEmpty A) denv DT ->
+  EvalTm (TmAbsurd A) denv dt ->
+  Delta ||- TmSb (TmAbsurd A) SB : TmSb (TmArr TmEmpty A) SB #aeq# dt
+   #in# HDT
+.
+Proof.
+intros.
+(*
+unfold TmArr in *.
+clear_inversion H2.
+clear_inversion H8.
+clear_inversion H3.
+
+dependent inversion HDT; subst.
+
+rename i into HDempty.
+rename i0 into HInterp.
+rename e into HappDF.
+rename e0 into HappDF'.
+rename i1 into HREC.
+
+inversion HInterp; subst.
+
+(**)
+
+assert (Delta |-- [SB] : Gamma) as HYY1.
+eapply RelSb_wellformed.
+eauto.
+
+simpl.
+split.
+
+eapply System.SB.
+eauto.
+eapply EMPTY_E.
+auto.
+
+exists TmEmpty.
+exists (TmSb A Sup).
+
+assert (exists PT, Interp (Dfun Dempty (Dclo (TmSb A Sup) denv)) PT) as HYY2.
+eauto.
+
+destruct HYY2 as [PT HPT].
+exists PT.
+split; auto.
+
+clear_inversion HPT.
+clear_inversion H5.
+
+split.
+
+(**)
+
+constructor 1.
+intros.
+clear_inversion H2.
+
+exists (Dup DA (DneAbsurd (DdownN DA) e)).
+exists (Dup DA (DneAbsurd (DdownN DA) e')).
+
+clear_inversion H6.
+clear_inversion po_ro.
+destruct ro_resp_ex with (Dup Dempty e) as [Y HY].
+eauto.
+
+exists Y.
+split.
+eauto.
+
+split.
+unfold Dup at 1. simpl. 
+eauto.
+
+split.
+unfold Dup at 1. simpl. 
+eauto.
+
+assert (Gamma |= A).
+eapply Valid_for_WfTp.
+eauto.
+
+clear_inversion H2.
+assert ([denv] === [denv] #in# Gamma).
+eapply RelSb_valenv.
+eauto.
+
+specialize (H6 _ _ H2).
+destruct H6.
+destruct H6.
+destruct H6.
+destruct H8.
+renamer.
+elim_deters.
+
+eapply Reflect_Characterization.
+eauto.
+
+(**)
+*)
 admit.
-admit.
-admit.
-(* SECOND CASE *)
+
 Qed.
 
 Theorem Rel_Fundamental: 
 eauto.
 
 (* TmAbsurd *)
-admit.
+
+eapply Rel_Fundamental_Absurd; eauto.
 
 (* SB: Sid *)
 clear_inversion H1.