1. Paweł Wieczorek
  2. MgrCoq

Commits

Paweł Wieczorek  committed 1f95407

The _Fun case in the fundamental lemma of logical relations is completed

  • Participants
  • Parent commits 2cc1b25
  • Branches another_weird_rule

Comments (0)

Files changed (1)

File Nbe/Model/LogRelSb.v

View file
 Qed.
 
 
+Theorem Rel_Fundamental_Fun: forall Gamma A  B Delta SB denv DT DT' (HDT : DT === DT' #in# PerType),
+  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) ->
+  Gamma,, A |-- B ->
+  ( forall (Delta : Cxt) (SB : Sb) (denv : DEnv),
+       Delta ||-  [SB]:Gamma,, A #aeq# denv ->
+       forall (DT DT' : D) (HDT : DT === DT' #in# PerType),
+       EvalTm B denv DT -> Delta ||- TmSb B SB #in# HDT) ->
+  Delta ||-  [SB]:Gamma #aeq# denv ->
+  EvalTm (TmFun A B) denv DT ->
+  Delta ||- TmSb (TmFun A B) SB #in# HDT
+.
+Proof.
+intros.
+
+assert (Delta |-- [SB] : Gamma) by (eapply RelSb_wellformed; eauto).
+
+destruct HDT; try solve [clear_inversion H4].
+simpl.
+exists (TmSb A SB).
+exists (TmSb B (Sext (Sseq SB Sup) TmVar)).
+split.
+
+eapply EQ_TP_SB_FUN.
+eauto.
+auto.
+auto.
+
+split.
+eapply H0.
+eauto.
+clear_inversion H4.
+auto.
+
+(**)
+
+intros.
+
+rename i1 into HREC.
+rename e into HappDF.
+rename e0 into HappDF'.
+rename i into HDA.
+rename i2 into i.
+
+assert (Delta0 |-- a : TmSb (TmSb A SB) (Sups i)) as HYY1.
+eapply RelTerm_implies_WtTm; eauto.
+
+assert (Delta0 |-- TmSb (TmSb A SB) (Sups i) === TmSb A (Sseq SB (Sups i))) as HYY2.
+eapply EQ_TP_SBSEQ; eauto.
+
+rename H2 into Hgoal.
+
+assert (Delta0 |-- [Sext (Sseq SB (Sups i)) a] : Gamma,,A) as HYY3.
+eapply SEXT; eauto. 
+
+clear_inversion H4.
+renamer.
+
+assert ( [denv] === [denv] #in# Gamma) as HYY4.
+eapply RelSb_valenv.
+eauto.
+
+assert ( [Dext denv da] === [Dext denv da] #in# Gamma,,A ) as HYY5.
+econstructor 2.
+eauto.
+exists DA_denv.
+split; eauto.
+auto.
+
+assert (Delta0 ||- [Sseq SB (Sups i)] : Gamma #aeq# denv) as HYY6.
+eapply RelSb_ClosedUnderLift.
+eauto.
+eauto.
+
+assert (Delta0 ||- a : TmSb A (Sseq SB (Sups i)) #aeq# da #in# HDA) as HYY7.
+eapply RelTerm_ClosedForConversion.
+eauto.
+eauto.
+eauto.
+eauto.
+
+assert (Delta0 ||- [Sext (Sseq SB (Sups i)) a] : Gamma,,A #aeq# Dext denv da) as HYY8.
+econstructor 2; eauto.
+
+inversion Happ; subst.
+
+move Hgoal at bottom.
+specialize (Hgoal _ _ _ HYY8).
+specialize (Hgoal _ _ (HREC da da DB DB' PDA_denv HPA Hda Happ Happ') H11).
+
+
+assert (Delta ||- TmSb A SB #in# HDA) as HYYY1.
+eauto.
+
+(**)
+assert (Delta0 |-- TmSb (TmSb B (Sext (Sseq SB Sup) TmVar)) (Sext (Sups i) a) === TmSb B (Sext (Sseq SB (Sups i)) a)) as HYY10.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eapply SEXT.
+eauto.
+eauto.
+eapply RelTerm_implies_WtTm.
+eauto.
+eapply SEXT.
+eapply SSEQ.
+eauto.
+eauto.
+eauto.
+
+eapply CONV.
+eapply HYP.
+eapply EXT.
+eauto.
+eapply RelType_implies_WfTp.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_CONG_SB.
+
+eapply EQ_SB_TRANS.
+eapply EQ_SB_SEXT.
+eapply SEXT.
+eauto.
+eauto.
+eapply RelTerm_implies_WtTm.
+eauto.
+eapply SEXT.
+eapply SSEQ.
+eauto.
+eauto.
+eauto.
+
+eapply CONV.
+eapply HYP.
+eapply EXT.
+eauto.
+eapply RelType_implies_WfTp.
+eauto.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+assert ( Delta0 |-- a : TmSb (TmSb A SB) (Sups i)) as HZZZ0.
+eapply RelTerm_implies_WtTm.
+eauto.
+
+assert (Delta0 |--  [Sext (Sups i) a]: Delta,,TmSb A SB) as HZZZ1.
+eapply SEXT.
+eauto.
+eauto.
+auto.
+
+
+
+assert (Delta0 |-- [Sseq (Sseq SB Sup) (Sext (Sups i) a)] === [Sseq SB (Sups i)] : Gamma ) as HZZ1.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_COMM.
+eauto.
+eauto.
+eauto.
+eauto.
+
+(**)
+eapply EQ_SB_CONG_SEXT.
+apply HZZ1.
+eauto.
+(**)
+
+assert (Delta0 |-- TmSb TmVar (Sext (Sups i) a) === a
+   : TmSb A (Sseq (Sseq SB Sup) (Sext (Sups i) a))) as HZZZ2.
+
+eapply EQ_CONV.
+eapply EQ_SBVAR.
+eauto.
+eauto.
+eapply RelTerm_implies_WtTm.
+eauto.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_SYM.
+apply HZZ1.
+eauto.
+eauto.
+eauto.
+
+(**)
+
+
+eapply RelType_ClosedForConversion; eauto.
+
+Qed.
+
 Theorem Rel_Fundamental: 
     (forall Gamma, Gamma |-- -> True) /\
 
 simpl.
 eauto.
 (* TP: TmFun *)
-assert (Delta |-- [SB] : Gamma) by (eapply RelSb_wellformed; eauto).
-
-destruct HDT; try solve [clear_inversion H2].
-simpl.
-exists (TmSb A SB).
-exists (TmSb B (Sext (Sseq SB Sup) TmVar)).
-split.
-
-eapply EQ_TP_SB_FUN.
-eauto.
-auto.
-auto.
-
-split.
-eapply H.
-eauto.
-clear_inversion H2.
-auto.
-
-(**)
-
-intros.
-admit.
+
+eapply Rel_Fundamental_Fun; eauto.
 
  
 (* TP: TmSb *)
 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 *)