Commits

committed 1f95407

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

• Participants
• Parent commits 2cc1b25
• Branches another_weird_rule

File Nbe/Model/LogRelSb.v

` 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 *)`