Commits

Paweł Wieczorek  committed d876514

Working on the _Absurd case

  • Participants
  • Parent commits 8b01b63
  • Branches another_weird_rule

Comments (0)

Files changed (1)

File Nbe/Model/LogRelSb.v

 .
 Proof.
 intros.
-(*
+
 unfold TmArr in *.
 clear_inversion H2.
 clear_inversion H8.
 eapply EMPTY_E.
 auto.
 
-exists TmEmpty.
-exists (TmSb A Sup).
+exists TmEmpty. 
+exists (TmSb A (Sseq SB Sup)).
 
 assert (exists PT, Interp (Dfun Dempty (Dclo (TmSb A Sup) denv)) PT) as HYY2.
 eauto.
 (**)
 
 constructor 1.
-intros.
-clear_inversion H2.
+intros. 
+inversion H2; subst.
+rename H2 into Hempty.
+rename H3 into H2.
 
 exists (Dup DA (DneAbsurd (DdownN DA) e)).
 exists (Dup DA (DneAbsurd (DdownN DA) e')).
 clear_inversion po_ro.
 destruct ro_resp_ex with (Dup Dempty e) as [Y HY].
 eauto.
-
+ 
 exists Y.
 split.
 eauto.
 eapply Valid_for_WfTp.
 eauto.
 
-clear_inversion H2.
+clear_inversion H3.
 assert ([denv] === [denv] #in# Gamma).
 eapply RelSb_valenv.
 eauto.
 
-specialize (H6 _ _ H2).
+specialize (H6 _ _ H3).
 destruct H6.
 destruct H6.
 destruct H6.
 eapply Reflect_Characterization.
 eauto.
 
+assert (Dup Dempty e === Dup Dempty e #in# PerEmpty) as He.
+eauto.
+
+eapply H7.
+
+eapply He.
+eauto.
+eauto.
+
+constructor 1.
+intros.
+
+
+clear_inversion H2.
+
+assert (exists PA, Interp DA_denv1 PA) as HPA.
+eauto.
+destruct HPA as [PA HPA].
+
+assert (DdownN DA_denv1 === DdownN DA_denv1 #in# PerNf) as Htp.
+eapply ReifyTp_Characterization.
+eauto.
+eauto.
+
+clear_inversion Htp.
+
+edestruct H10 as [ne [Hne Hne']].
+edestruct H2 as [NFA [HNFA _]].
+
+eexists.
+split.
+eauto.
+eauto.
+
 (**)
-*)
-admit.
+
+
+assert (Delta,, TmSb TmEmpty SB |--  [Sext (Sseq SB Sup) TmVar]: Gamma,, TmEmpty) as HXX1.
+eapply SEXT.
+eapply SSEQ.
+eauto.
+eauto.
+eauto.
+eapply CONV.
+eapply HYP.
+eapply EXT.
+eauto.
+eapply SB_F.
+eauto.
+eauto.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_REFL.
+eapply SB_F.
+eauto.
+eauto.
+
+(**)
+split.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SB_FUN.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_CONG_FUN.
+eauto.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_SUP.
+eauto.
+eapply EMPTY_F.
+eauto.
+eapply CONV.
+eapply HYP.
+eauto.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+eapply EQ_SB_REFL.
+eauto.
+eauto.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eapply SEXT.
+eauto.
+eapply EMPTY_F.
+eauto.
+eapply CONV.
+eapply HYP.
+eapply EXT.
+eauto.
+eauto.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SB_EMPTY.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SB_EMPTY.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_CONG_SB.
+
+eapply EQ_SB_TRANS.
+eapply EQ_SB_SUP.
+eauto.
+eapply EMPTY_F.
+eauto.
+
+eapply CONV.
+eapply HYP.
+eauto.
+eapply EXT.
+eauto.
+eauto.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SB_EMPTY.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SB_EMPTY.
+eauto.
+eapply EQ_SB_REFL.
+eauto.
+eauto.
+
+(****)
+split.
+
+dependent inversion HDempty.
+subst; simpl.
+eauto.
+
+(*****)
+
+intros.
+inversion HPA; subst.
+inversion Hda; subst.
+
+eexists.
+split.
+unfold Dup; simpl; eauto.
+
+inversion Happ; subst.
+clear_inversion H13.
+clear_inversion H11.
+elim_deters.
+renamer.
+clear_dups.
+
+assert ( Delta0 |-- [Sseq SB (Sups i)] : Gamma ) as HXX2.
+eauto.
+
+assert ( Delta0 ||- [Sseq SB (Sups i)] : Gamma #aeq# envs ) as HXX3.
+eapply RelSb_ClosedUnderLift.
+eauto.
+eauto.
+
+
+specialize (H0 _ _ _ HXX3).
+specialize (H0 _ _ (HREC (Dup Dempty e) (Dup Dempty e) DA_envs0 DB' PerEmpty HPA Hda Happ
+          Happ')).
+specialize (H0 H15).
+ 
+edestruct RelReify1.
+eauto.
+destruct H8 as [RelTerm_Reify_ RelTerm_Back_ ].
+rename H4 into RelType_Reify_.
+
+(**)
+eapply RelTerm_Back_.
+eauto.
+
+assert (Delta0 |-- a :  TmSb TmEmpty (Sups i)) as HXX4.
+eapply RelTerm_implies_WtTm.
+eauto.
+
+assert (Delta0 |-- a :  TmEmpty) as HXX5.
+eapply CONV.
+eauto.
+eapply EQ_TP_SB_EMPTY.
+eauto.
+
+assert (Delta0 |--  [Sext (Sups i) a]: Delta,,TmEmpty) as HXX7.
+eapply SEXT.
+eauto.
+eauto.
+eauto.
+
+
+assert (Delta0 |--  TmSb (TmSb A (Sseq SB Sup)) (Sext (Sups i) a) === TmSb A (Sseq SB (Sups i))) as HXX6.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_COMM.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_SB_CONG_SSEQ.
+eapply EQ_SB_SUP.
+eauto.
+eapply EMPTY_F.
+eauto.
+eauto.
+eapply EQ_SB_REFL.
+eauto.
+eauto.
+
+(**)
+
+specialize (H0 _ _ _ HXX3).
+specialize (H0 _ _ (HREC (Dup Dempty e) (Dup Dempty e) DA_envs0 DB' PerEmpty HPA Hda Happ
+          Happ')).
+specialize (H0 H15).
+
+
+
+eapply RelType_ClosedForConversion.
+eauto.
+eauto.
+
+(****)
+renamer.
+assert (DdownN DA_envs === DdownN DA_envs #in# PerNf) as HXX4.
+
+assert (Gamma |= A) as HXX2.
+eapply Valid_for_WfTp.
+eauto.
+
+
+clear_inversion HXX2.
+assert ([envs] === [envs] #in# Gamma) as HXX3.
+eapply RelSb_valenv.
+eauto.
+
+specialize (H8 _ _ HXX3).
+destruct H8 as [DA_ [ _DA [_HDA [HDA_ HDA]]]].
+
+elim_deters.
+renamer.
+
+assert (exists PT, Interp DA_envs PT) as HPT.
+eauto.
+
+destruct HPT as [PT HPT].
+renamer.
+ 
+eapply ReifyTp_Characterization.
+eauto.
+eauto.
+clear_inversion HXX4.
+
+
+(**)
+constructor 1.
+
+intros.
+
+clear_inversion H5.
+
+edestruct H8 as [ne [Hne1 Hne2]].
+edestruct H4 as [NFA [HNFA1 HNFA2]].
+eexists.
+split.
+eauto.
+eauto.
+
+(*****)
+
+intros.
+renamer.
+assert (DdownN DA_envs === DdownN DA_envs #in# PerNf) as HXX4.
+
+assert (Gamma |= A) as HXX2.
+eapply Valid_for_WfTp.
+eauto.
+
+
+clear_inversion HXX2.
+assert ([envs] === [envs] #in# Gamma) as HXX3.
+eapply RelSb_valenv.
+eauto.
+
+specialize (H10 _ _ HXX3).
+destruct H10 as [DA_ [ _DA [_HDA [HDA_ HDA]]]].
+
+elim_deters.
+renamer.
+
+assert (exists PT, Interp DA_envs PT) as HPT.
+eauto.
+
+destruct HPT as [PT HPT].
+renamer.
+ 
+eapply ReifyTp_Characterization.
+eauto.
+eauto.
+clear_inversion HXX4.
+inversion H5; subst.
+
+edestruct H10 as [ne [Hne1 Hne2]].
+edestruct H8 as [NFA [HNFA1 HNFA2]].
+eexists.
+split.
+eauto.
+
+(**)
+
 
 Qed.