Paweł Wieczorek avatar Paweł Wieczorek committed 3e9806a

Specialized directory for LogRelTm

Comments (0)

Files changed (17)

 Nbe/Model/Interp.v
 Nbe/Model/Valid.v
 Nbe/Model/Terminating.v
-Nbe/Model/LogRelTm_Def.v
-Nbe/Model/LogRelTm_BasicFacts.v
-Nbe/Model/LogRelTm_ProofIrrelevance.v
-Nbe/Model/LogRelTm_ClosedForConversion.v
-Nbe/Model/LogRelTm_ClosedUnderPer.v
-Nbe/Model/LogRelTm_Lift.v
-Nbe/Model/LogRelTm_Back.v
+Nbe/Model/LogRelTm/Def.v
+Nbe/Model/LogRelTm/BasicFacts.v
+Nbe/Model/LogRelTm/ProofIrrelevance.v
+Nbe/Model/LogRelTm/ClosedForConversion.v
+Nbe/Model/LogRelTm/ClosedUnderPer.v
+Nbe/Model/LogRelTm/Lift.v
+Nbe/Model/LogRelTm/Back.v
 Nbe/Model/LogRelTm.v
 Nbe/Model/LogRelSb_Def.v
 Nbe/Model/LogRelSb_BasicFacts.v
   Nbe/Model/Interp.v\
   Nbe/Model/Valid.v\
   Nbe/Model/Terminating.v\
-  Nbe/Model/LogRelTm_Def.v\
-  Nbe/Model/LogRelTm_BasicFacts.v\
-  Nbe/Model/LogRelTm_ProofIrrelevance.v\
-  Nbe/Model/LogRelTm_ClosedForConversion.v\
-  Nbe/Model/LogRelTm_ClosedUnderPer.v\
-  Nbe/Model/LogRelTm_Lift.v\
-  Nbe/Model/LogRelTm_Back.v\
+  Nbe/Model/LogRelTm/Def.v\
+  Nbe/Model/LogRelTm/BasicFacts.v\
+  Nbe/Model/LogRelTm/ProofIrrelevance.v\
+  Nbe/Model/LogRelTm/ClosedForConversion.v\
+  Nbe/Model/LogRelTm/ClosedUnderPer.v\
+  Nbe/Model/LogRelTm/Lift.v\
+  Nbe/Model/LogRelTm/Back.v\
   Nbe/Model/LogRelTm.v\
   Nbe/Model/LogRelSb_Def.v\
   Nbe/Model/LogRelSb_BasicFacts.v\

Nbe/Model/LogRelTm.v

  *)
 Add Rec LoadPath "../../Nbe" as Nbe.
 
-Require Export Nbe.Model.LogRelTm_Def.
-Require Export Nbe.Model.LogRelTm_BasicFacts.
-Require Export Nbe.Model.LogRelTm_ProofIrrelevance.
-Require Export Nbe.Model.LogRelTm_ClosedForConversion.
-Require Export Nbe.Model.LogRelTm_ClosedUnderPer.
-Require Export Nbe.Model.LogRelTm_Lift.
-Require Export Nbe.Model.LogRelTm_Back.
+Require Export Nbe.Model.LogRelTm.Def.
+Require Export Nbe.Model.LogRelTm.BasicFacts.
+Require Export Nbe.Model.LogRelTm.ProofIrrelevance.
+Require Export Nbe.Model.LogRelTm.ClosedForConversion.
+Require Export Nbe.Model.LogRelTm.ClosedUnderPer.
+Require Export Nbe.Model.LogRelTm.Lift.
+Require Export Nbe.Model.LogRelTm.Back.
 

Nbe/Model/LogRelTm/Back.v

+
+(******************************************************************************
+ * Pawel Wieczorek
+ *)
+
+Set Implicit Arguments.
+
+(*
+Add Rec LoadPath "../../Nbe" as Nbe.
+ *)
+Add Rec LoadPath "../../Nbe" as Nbe.
+
+Require Import Arith.
+Require Import Arith.Plus.
+
+Require Import Program.
+Require Import Program.Tactics.
+Require Import Program.Equality.
+Require Import Setoid.
+Require Import Relations.Relation_Definitions.
+Require Import Classes.RelationClasses.
+
+
+Require Import Nbe.Syntax.
+Require Import Nbe.Domain.
+Require Import Nbe.Utils.
+Require Import Nbe.Model.PER.
+Require Import Nbe.Model.Interp.
+Require Import Nbe.Model.Valid.
+Require Import Nbe.Model.Terminating.
+Require Import Nbe.Model.LogRelTm.Def.
+Require Import Nbe.Model.LogRelTm.BasicFacts.
+Require Import Nbe.Model.LogRelTm.ProofIrrelevance.
+Require Import Nbe.Model.LogRelTm.ClosedForConversion.
+Require Import Nbe.Model.LogRelTm.ClosedUnderPer.
+Require Import Nbe.Model.LogRelTm.Lift.
+
+(******************************************************************************
+ * Each
+ *)
+
+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)
+.
+Proof.
+induction i; intros.
+
+clear_inversion H.
+simpl.
+clear_inversion H0.
+apply EQ_SBID.
+eapply CONV.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SBID.
+eauto.
+
+(**)
+
+clear_inversion H.
+clear_inversion H3.
+rename A0 into B.
+simpl.
+
+specialize (IHi Gamma__1 Gamma A H5).
+eapply EQ_CONV.
+ 
+eapply EQ_TRANS.
+eapply EQ_SYM.
+eapply EQ_SBSEQ.
+
+eauto.
+eauto.
+eauto.
+eapply EQ_CONG_SB.
+eauto.
+apply IHi.
+
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+Qed.
+
+(******************************************************************************
+ *)
+
+
+Lemma TmVar_Sups_tmVar': forall i Delta  Gamma A,
+  CxtShift Delta i (Gamma,,A) ->
+  Delta |-- TmSb TmVar (Sups i) === tmVar i : TmSb (TmSb A (Sups 1)) (Sups i)
+.
+Proof.
+intros.
+simpl in *.
+
+assert (Gamma,,A |--).
+eauto.
+clear_inversion H0.
+
+eapply EQ_CONV.
+eapply TmVar_Sups_tmVar.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_CONG_SB.
+eauto.
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_SIDL.
+apply SUP.
+eauto.
+eauto.
+Qed.
+
+(******************************************************************************
+ * Reification1
+ *)
+
+Theorem RelReify1: forall Gamma T DT DT' (HDT : DT === DT' #in# PerType),
+  Gamma ||- T #in# HDT ->
+    (exists A, RbNf (length Gamma) (DdownN DT) A /\ Gamma |-- T === A
+    ) /\
+
+    (forall t dt, Gamma ||- t : T #aeq# dt #in# HDT ->
+      (exists v, RbNf (length Gamma) (Ddown DT dt) v /\ Gamma |-- t === v : T)
+    ) /\
+
+    (forall t k, k === k #in# PerNe ->
+      (forall Delta i, CxtShift Delta i Gamma -> exists tv,
+        RbNe (length Delta) k tv /\
+        Delta |-- TmSb t (Sups i) === tv : TmSb T (Sups i))
+      ->
+      Gamma ||- t : T #aeq# (Dup DT k) #in# HDT
+    )
+.
+Proof.
+do 5 intro.
+generalize dependent T.
+generalize dependent Gamma.
+induction HDT using PerType_dind; split; try split; intros.
+
+(*Dnat a) *)
+
+exists TmNat; auto.
+
+(*Dnat b) *)
+
+simpl in H0.
+decompose record H0.
+specialize (H4 Gamma 0).
+destruct H4; try red; eauto.
+exists x. simpl in *.
+decompose record H2.
+split; auto.
+eapply EQ_TRANS.
+eapply EQ_SYM.
+eapply EQ_SBID; eauto.
+eapply EQ_CONV; eauto.
+auto.
+
+(*Dnat c) *)
+
+simpl; repeat split; auto.
+intros.
+edestruct H1.
+eauto.
+program_simpl.
+exists x.
+split; auto.
+unfold Ddown; unfold Dup; simpl.
+apply reifyNf_ne; auto.
+simpl in H.
+eapply EQ_CONV.
+apply H4.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_REFL.
+red in H2. eauto.
+eauto.
+eapply EQ_TP_SB_NAT.
+eauto.
+
+(*Dunit a) *)
+
+exists TmUnit; auto.
+
+(*Dunit b) *)
+
+simpl in H0.
+decompose record H0.
+specialize (H4 Gamma 0).
+destruct H4; try red; eauto.
+exists x. simpl in *.
+decompose record H2.
+split; auto.
+eapply EQ_TRANS.
+eapply EQ_SYM.
+eapply EQ_SBID; eauto.
+eapply EQ_CONV; eauto.
+
+(*Dunit c) *)
+
+simpl; repeat split; auto.
+intros.
+
+exists Tm1.
+split; auto.
+unfold Ddown; unfold Dup; simpl; eauto.
+apply EQ_Unit_Eta.
+
+edestruct H1.
+eauto.
+program_simpl.
+simpl in H.
+eapply CONV.
+eauto.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_REFL.
+red in H2. eauto.
+eauto.
+eapply EQ_TP_SB_UNIT.
+eauto.
+
+(*Dfun a) *)
+
+renamer; intros.
+rename i into HDA.
+rename i1 into HREC.
+rename i0 into HPDA.
+rename e0 into e'.
+
+simpl in H0.
+destruct H0 as [A [F [HS1 [HS2 HS3]]]].
+
+move IHHDT at bottom.
+set (IHHDT2 := IHHDT).
+specialize (IHHDT2).
+specialize (IHHDT Gamma A HS2).
+destruct IHHDT as [HI1 [HI2 HI3]].
+destruct HI1 as [NFA HNFA].
+destruct HNFA as [HNFA1 HNFA2].
+
+ 
+move H at bottom.
+
+
+set (var := Dvar (length Gamma)).
+set (dv  := Dup DA var).
+
+assert (var === var #in# PerNe) as HvarNe.
+unfold var.
+apply PerNe_intro.
+intros.
+exists (tmVar (m - S (length Gamma))); split; auto.
+
+assert (dv === dv #in# PDA) as HdvPDA.
+apply Reflect_Characterization; eauto.
+
+
+assert (CxtShift Gamma 0 Gamma) as HCxtShift0 by eauto.
+assert (CxtShift (Gamma,,A) 1 Gamma) as HCxtShift1 by (eapply SSEQ; eauto).
+
+specialize (HI3 TmVar var HvarNe).
+
+edestruct e as [DB Happ]; [ eauto | ].
+edestruct e' as [DB' Happ']; [ eauto | ].
+
+
+assert (Gamma,,A ||- TmSb A (Sups 1) #in# HDA) as HDAliftA by (eapply RelTypeLifting; eauto).
+
+assert (Gamma,,A ||- TmVar : TmSb A (Sups 1) #aeq# Dup DA var #in# HDA) as Ha.
+set (IHHDT3 := IHHDT2).
+specialize IHHDT3.
+specialize (IHHDT2 (Gamma,,A) (TmSb A (Sups 1)) HDAliftA). 
+destruct IHHDT2 as [HI1' [HI2' HI3']].
+specialize (HI3' TmVar var HvarNe).
+apply HI3'.
+intros.
+exists (tmVar (length Delta - (S (length Gamma)))).
+unfold var.
+split; auto.
+rewrite CxtShift_length with (i := i) (Gamma := Gamma,,A).
+simpl.
+rewrite minus_plus.
+eapply TmVar_Sups_tmVar'; eauto.
+eauto.
+
+move HS3 at bottom.
+
+assert (CxtShift (Gamma,,NFA) 1 Gamma) as HCxtShift1'.
+red.
+simpl.
+eapply SSEQ.
+eauto.
+eauto.
+
+specialize (HS3 (Gamma,,A) 1 TmVar dv DB DB' PDA HPDA). 
+specialize (HS3 HdvPDA Happ Happ' HCxtShift1 Ha).
+
+move H at bottom.
+specialize (H dv dv DB DB' PDA HPDA HdvPDA Happ Happ' _ _ HS3).
+
+destruct H as [HF1 [HF2 HF3]].
+destruct HF1 as [NFF [HF1' HF1'']].
+set (NT := TmFun NFA NFF). 
+exists NT.
+split.
+apply reifyNf_fun with DB.
+auto.
+auto.
+auto.
+
+(*
+assert (Gamma,,A |-- NFF).
+eauto.
+
+assert (Gamma |-- NT).
+apply FUN_F.
+eauto.
+
+
+eapply WfTp_from_WfTpEq2.
+eauto.
+*)
+
+assert (Gamma |-- TmFun A F) as HZZ1.
+eauto.
+
+clear_inversion HZZ1.
+auto.
+ 
+
+assert (Gamma,,A |-- TmSb F (Sext (Sups 1) TmVar) === F) as HZZ2.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_SYM.
+simpl.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_SIDSUP.
+eauto.
+eapply EQ_SB_CONG_SEXT.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_REFL.
+auto.
+apply EQ_TP_SBID.
+auto.
+
+(**)
+ 
+move NFA at bottom.
+move NFF at bottom.
+  
+eapply EQ_TP_TRANS.
+eauto.
+eapply EQ_TP_CONG_FUN.
+auto.
+
+(**)
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SYM.
+eauto.
+auto.
+
+(**)
+
+(*
+assert (Gamma,,NFA |-- TmSb F (Sext (Sups 1) TmVar) === F) as HZZ3.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_SYM.
+simpl.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_SIDSUP.
+eauto.
+eapply EQ_SB_CONG_SEXT.
+eauto.
+eauto.
+eapply EQ_REFL.
+eauto.
+eapply EQ_TP_REFL.
+auto.
+
+apply EQ_TP_SBID.
+auto.
+
+
+
+*)
+
+admit.
+
+(*Dfun b) *)
+ 
+renamer; intros.
+rename i into HDA.
+rename i1 into HREC.
+rename i0 into HPDA.
+rename e0 into e'.
+
+simpl in H1.
+
+destruct H1 as [HS1 [A [F [PT [HS2 [HS3 [HS4 [HS5 HS6]]]]]]]].
+
+move IHHDT at bottom.
+set (IHHDT2 := IHHDT).
+move H at bottom.
+set (var := Dvar (length Gamma)).
+set (dv  := Dup DA var).
+
+assert (var === var #in# PerNe) as HvarNe.
+unfold var.
+apply PerNe_intro.
+intros.
+exists (tmVar (m - S (length Gamma))); split; auto.
+
+assert (dv === dv #in# PDA) as HdvPDA.
+apply Reflect_Characterization; eauto.
+
+assert (Gamma |-- TmFun A F) as HfunAF by eauto.
+clear_inversion HfunAF.
+
+assert (CxtShift Gamma 0 Gamma) as HCxtShift0 by eauto.
+assert (CxtShift (Gamma,,A) 1 Gamma) as HCxtShift1 by (eapply SSEQ; eauto).
+
+edestruct e as [DB Happ]; [ eauto | ].
+edestruct e' as [DB' Happ']; [ eauto | ].
+
+assert (Gamma,,A ||- TmSb A (Sups 1) #in# HDA) as HDAliftA by (eapply RelTypeLifting; eauto).
+
+assert (Gamma,,A ||- TmVar : TmSb A (Sups 1) #aeq# Dup DA var #in# HDA) as Ha.
+specialize (IHHDT (Gamma,,A) (TmSb A (Sups 1)) HDAliftA).
+destruct IHHDT as [HI1' [HI2' HI3']].
+specialize (HI3' TmVar var HvarNe).
+apply HI3'.
+intros.
+exists (tmVar (length Delta - (S (length Gamma)))).
+unfold var.
+split; auto.
+rewrite CxtShift_length with (i := i) (Gamma := Gamma,,A).
+simpl.
+rewrite minus_plus.
+eapply TmVar_Sups_tmVar'; eauto.
+eauto.
+
+move HS6 at bottom.
+specialize (HS6 (Gamma,,A) 1 TmVar dv DB DB' PDA HPDA). 
+specialize (HS6 HdvPDA Happ Happ' HCxtShift1 Ha).
+destruct HS6 as [dy [HS6' HS6'']].
+
+assert ( Gamma,, A ||-  TmSb F (Sext (Sups 1) TmVar)  #in# HREC dv dv DB DB' PDA HPDA HdvPDA Happ Happ'  )  as Htype .
+eapply RelTerm_implies_RelType.
+eauto.
+
+move H at bottom.
+specialize (H dv dv DB DB' PDA HPDA HdvPDA Happ Happ' _ _ Htype).
+destruct H as [HF1 [HF2 HF3]].
+edestruct HF2 as [nft Hnft].
+eauto.
+destruct Hnft as [Hnft1 Hft2].
+
+destruct HF1 as [HNF [HNF1 HNF2]].
+
+specialize (IHHDT Gamma A).
+destruct IHHDT as [HI1 [HI2 HI3]].
+auto.
+destruct HI1 as [NFA HNFA].
+destruct HNFA as [HNFA1 HNFA2].
+
+(*
+move HS2 at bottom. 
+clear_inversion HS2.
+clear_inversion HS3.
+destruct H with dv dv as [db [db' [PB [Hdb1 [Hdb2 [Hdb3 Hdb4]]]]]].
+find_extdeters.
+eauto.
+*)
+
+set (NT := TmAbs NFA nft).
+ 
+assert (Gamma |-- t : TmFun A F) as HtAF.
+eapply CONV.
+eauto.
+auto.
+ 
+assert (Gamma,, A |-- TmSb (TmFun A F) Sup === TmFun (TmSb A Sup) (TmSb F (Sext (Sseq Sup Sup) TmVar))) as HX1.
+eapply EQ_TP_SB_FUN.
+eauto.
+eauto.
+eauto.
+
+assert (  Gamma,, A |-- TmSb A Sup ) as HX2.
+eauto.
+
+assert (  Gamma,, A |-- TmVar : TmSb A Sup ) as HX3.
+eauto.
+
+assert (Gamma,, A |-- [Ssing TmVar] : Gamma,, A,,TmSb A Sup) as HX4.
+eapply SEXT.
+eauto.
+eauto.
+eapply CONV.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SBID.
+eauto.
+
+assert (Gamma,, A,, TmSb A Sup |--  [Sseq Sup Sup]: Gamma)  as HX5 by eauto.
+
+assert ( Gamma,, A,, TmSb A Sup |--  [Sext (Sseq Sup Sup) TmVar] : Gamma ,, A ) as HX6.
+eapply SEXT.
+eauto.
+eauto.
+eapply CONV.
+eapply HYP; eauto.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+
+
+assert ( Gamma,, A |-- TmVar : TmSb A (Sseq Sup Sid)) as HX7.
+eapply CONV.
+eauto.
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_SYM.
+eapply EQ_SB_SIDR.
+eauto.
+eauto.
+
+assert ( Gamma,, A |-- TmVar : TmSb A (Sseq Sid Sup)) as HX7'.
+eapply CONV.
+eapply HYP.
+eauto.
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_SYM.
+eapply EQ_SB_SIDL.
+eauto.
+eauto.
+
+assert( Gamma,, A |--  [Sext (Sseq Sup Sid) TmVar]=== [Sid]:Gamma,, A) as HX8.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_CONG_SEXT.
+eapply EQ_SB_SIDR.
+eauto.
+eauto.
+eapply EQ_REFL.
+eauto.
+eapply EQ_SB_SYM.
+eapply EQ_SB_SIDSUP.
+eauto.
+
+assert( Gamma,, A |--  [Sext (Sseq Sid Sup) TmVar]=== [Sid]:Gamma,, A) as HX8'.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_CONG_SEXT.
+eapply EQ_SB_SIDL.
+eauto.
+eauto.
+eapply EQ_REFL.
+eauto.
+eapply EQ_SB_SYM.
+eapply EQ_SB_SIDSUP.
+eauto.
+
+assert( Gamma,, A |--  [Sseq Sup Sid]=== [Sseq (Sseq Sup Sup) (Ssing TmVar)] : Gamma ) as HX9.
+eapply EQ_SB_SYM.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_COMM.
+eauto.
+eauto.
+eauto.
+eapply EQ_SB_CONG_SSEQ.
+eapply EQ_SB_SUP.
+eauto.
+eauto.
+eauto.
+eauto.
+eauto.
+
+assert (Gamma,, A |-- TmSb (TmSb F (Sext (Sseq Sup Sup) TmVar)) (Ssing TmVar) === F) as HX10.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SBID.
+auto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_SEXT.
+eauto.
+eauto.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_CONG_SEXT.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_COMM.
+eauto.
+eauto.
+eauto.
+eapply EQ_SB_CONG_SSEQ.
+eapply EQ_SB_SUP.
+eauto.
+eauto.
+eauto.
+eauto.
+eauto.
+eapply EQ_CONV.
+eapply EQ_SBVAR.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_CONG_SB.
+eauto.
+eauto.
+eauto.
+eauto.
+
+assert (Gamma,,A |-- TmSb F (Sext (Sups 1) TmVar) === F ) as HX11.
+simpl.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_CONG_SB.
+eauto.
+eauto.
+eauto.
+
+(**!*)
+
+exists NT.
+split; auto.
+unfold Ddown; simpl.
+eapply reifyNf_abs with (db := dy) (DB := DB); auto.
+ 
+eapply EQ_CONV with (A := TmFun A F); [ | eauto ].
+eapply EQ_TRANS.
+eapply EQ_FUN_Eta.
+auto.
+eapply EQ_CONG_FUN_I; auto.
+eapply EQ_TRANS.
+eapply EQ_CONV.
+eapply EQ_CONG_FUN_E.
+eapply EQ_REFL.
+eapply CONV.
+eapply SB.
+auto.
+apply HtAF.
+eauto.
+eauto.
+eauto.
+
+(**)
+
+assert ( Gamma,, A |-- TmApp (TmSb t (Sups 1)) TmVar === nft : F) as HX12.
+eapply EQ_CONV.
+eauto.
+eauto.
+ 
+eapply EQ_TRANS; [ | apply HX12 ].
+eapply EQ_CONV.
+eapply EQ_CONG_FUN_E.
+eapply EQ_CONV.
+eapply EQ_CONG_SB.
+simpl.
+eauto.
+eauto.
+eauto.
+eapply EQ_REFL.
+eauto.
+eauto.
+
+(**)
+
+admit.
+
+(* Dfun c *)
+
+  
+renamer; intros.
+rename i into HDA.
+rename i1 into HREC.
+rename i0 into HPDA.
+rename e0 into e'.
+ 
+simpl in H0.
+destruct H0 as [A [F [HS1 [HS2 HS3]]]].
+
+assert (
+ exists PT : relation D,
+     Interp (Dfun DA DF) PT
+) as HPT.
+
+assert (Dfun DA DF === Dfun DA' DF' #in# PerType).
+apply PerType_arr with PDA; auto.
+eauto.
+
+destruct HPT as [PT HPT].
+
+assert (Gamma |-- t : T) as HtT.
+destruct (H2 Gamma 0) as [tt [Htt1 Htt2]].
+red; eauto.
+assert (Gamma |-- TmSb t (Sups 0) : TmSb T (Sups 0)) by eauto.
+apply SBID_inv.
+apply CONV with (A := TmSb T Sid); eauto.
+
+split; auto.
+exists A F PT; repeat (split; auto).
+
+clear_inversion HPT.
+apply RelProd_intro; intros.
+
+edestruct e with (a := a0) as [DB0 HDB0] .
+find_extdeters.
+close_doms.
+apply H3; eauto.
+
+edestruct e with (a := a1) as [DB1 HDB1] .
+find_extdeters.
+close_doms.
+apply H3; eauto.
+ 
+
+clear_inversion H5.
+clear_inversion po_ro.
+destruct ro_resp_ex with (a := a0) as [Y HY].
+eauto.
+
+set (y0 := (Dup DB0 (Dapp k (Ddown DA a0)))).
+set (y1 := (Dup DB1 (Dapp k (Ddown DA a1)))).
+ 
+exists y0 y1 Y.
+unfold Dup; simpl.
+repeat (split; auto).
+apply appFun; auto.
+apply appFun; auto.
+ 
+assert (DB0 === DB1 #in# PerType) as HDBPerType.
+assert (Dfun DA DF === Dfun DA' DF' #in# PerType).
+apply PerType_arr with PDA; auto.
+find_extdeters.
+close_doms.
+
+edestruct e' with (a := a0) as [DB0' HDB0'] .
+apply H5; eauto.
+
+eapply PER_Transitive with DB0'.
+
+eapply HREC with (a0 := a0) (a1 := a0) (P := PDA); auto.
+apply H5; eauto.
+
+symmetry.
+eapply HREC with (a0 := a1) (a1 := a0) (P := PDA); auto.
+apply H5.
+symmetry.
+apply H0.
+
+
+apply Reflect_Characterization.
+auto.
+eauto.
+apply PerNe_intro; intros.
+
+assert (Ddown DA a0 === Ddown DA a1 #in# PerNf).
+eapply Reify_Characterization.
+eauto.
+eauto.
+eauto.
+clear_inversion H3.
+destruct H5 with m as [nd [Hnd1 Hnd2]].
+
+clear_inversion H1.
+destruct H3 with m as [nk [Hnk1 Hnk2]].
+ 
+set (n := TmApp nk nd).
+exists n.
+repeat (split; auto).
+apply reifyNe_app; auto.
+apply reifyNe_app; auto.
+
+(**)
+
+intros.
+simpl in H3.
+simpl.
+
+clear_inversion HPT.
+set (dy := Dup DB (Dapp k (Ddown DA da))).
+exists dy.
+split; auto.
+unfold Dup; simpl.
+apply appFun.
+auto.
+
+move HS3 at bottom.
+specialize (HS3 Delta i a da DB DB' PA HPA Hda Happ Happ' H0 H3).
+
+move H at bottom.
+specialize (H da da DB DB').
+specialize (H PA HPA Hda Happ Happ' Delta _ HS3).
+destruct H as [HF1 [HF2 HF3]].
+
+(* try HF3 *)
+
+assert (Ddown DA da === Ddown DA da #in# PerNf).
+eapply Reify_Characterization.
+eauto.
+eauto.
+eauto.
+
+apply HF3.
+
+ 
+apply PerNe_intro.
+intros.
+
+
+clear_inversion H.
+destruct H4 with m as [nd [Hnd1 Hnd2]].
+
+clear_inversion H1.
+destruct H with m as [ne [Hne1 Hne2]].
+
+set (n := TmApp ne nd).
+exists n.
+repeat (split; auto).
+apply reifyNe_app; auto.
+apply reifyNe_app; auto.
+
+(**)
+
+intros.
+move H2 at bottom.
+rename i0 into j.
+destruct H2 with (Delta := Delta0) (i := j + i) as [ne [Hne1 Hne2]].
+eapply CxtShift_comp; eauto.
+
+clear_inversion H.
+destruct H5 with (m := length Delta0) as [nd [Hnd1 Hnd2]].
+set (tv := TmApp ne nd).
+
+exists tv.
+repeat (split; auto).
+apply reifyNe_app; auto.
+
+subst.
+admit.
+
+(*Dempty a) *)
+
+exists TmEmpty; auto.
+
+(*Dempty a) *)
+
+simpl in H0.
+decompose record H0.
+specialize (H4 Gamma 0).
+destruct H4; try red; eauto.
+exists x. simpl in *.
+decompose record H2.
+split; auto.
+eapply EQ_TRANS.
+eapply EQ_SYM.
+eapply EQ_SBID; eauto.
+eapply EQ_CONV; eauto.
+
+(*Dempty c) *)
+
+simpl; repeat (split; auto).
+intros.
+
+edestruct H1.
+eauto.
+program_simpl.
+simpl in H.
+unfold Ddown; unfold Dup.
+simpl.
+exists x.
+split.
+auto.
+eapply EQ_CONV.
+apply H4.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_REFL.
+red in H2. eauto.
+eauto.
+eapply EQ_TP_SB_EMPTY.
+eauto.
+Qed.
+
+(******************************************************************************
+ * Reification (unpack)
+ *)
+
+
+Theorem RelType_Reify: forall Gamma T DT DT' (HDT : DT === DT' #in# PerType),
+  Gamma ||- T #in# HDT ->
+    (exists A, RbNf (length Gamma) (DdownN DT) A /\ Gamma |-- T === A)
+.
+Proof.
+intros.
+edestruct RelReify1; intuition; eauto.
+Qed.
+
+
+Theorem RelTerm_Reify: forall Gamma T DT DT' (HDT : DT === DT' #in# PerType),
+  Gamma ||- T #in# HDT ->
+    (forall t dt, Gamma ||- t : T #aeq# dt #in# HDT ->
+      (exists v, RbNf (length Gamma) (Ddown DT dt) v /\ Gamma |-- t === v : T)
+    )
+.
+Proof.
+intros.
+edestruct RelReify1; intuition; eauto.
+Qed.
+
+Theorem RelTerm_Back: forall Gamma T DT DT' (HDT : DT === DT' #in# PerType),
+  Gamma ||- T #in# HDT ->
+    (forall t k, k === k #in# PerNe ->
+      (forall Delta i, CxtShift Delta i Gamma -> exists tv,
+        RbNe (length Delta) k tv /\
+        Delta |-- TmSb t (Sups i) === tv : TmSb T (Sups i))
+      ->
+      Gamma ||- t : T #aeq# (Dup DT k) #in# HDT
+    )
+.
+Proof.
+intros.
+edestruct RelReify1; intuition; eauto.
+Qed.
+

Nbe/Model/LogRelTm/BasicFacts.v

+
+(******************************************************************************
+ * Pawel Wieczorek
+ *)
+
+Set Implicit Arguments.
+
+(*
+Add Rec LoadPath "../../Nbe" as Nbe.
+ *)
+Add Rec LoadPath "../../Nbe" as Nbe.
+
+Require Import Arith.
+Require Import Arith.Plus.
+
+Require Import Program.
+Require Import Program.Tactics.
+Require Import Program.Equality.
+Require Import Setoid.
+Require Import Relations.Relation_Definitions.
+Require Import Classes.RelationClasses.
+
+
+Require Import Nbe.Syntax.
+Require Import Nbe.Domain.
+Require Import Nbe.Utils.
+Require Import Nbe.Model.PER.
+Require Import Nbe.Model.Interp.
+Require Import Nbe.Model.Valid.
+Require Import Nbe.Model.Terminating.
+Require Import Nbe.Model.LogRelTm.Def.
+
+(******************************************************************************
+ * RelTerm implies RelType
+ *
+ * The logical relation between judgement 'Gamma |-- t : T' and 'dt #in# (Interp DT)'
+ * should be satisfied only when relation between 'Gamma |-- T' and 'DT' holds.
+ *)
+
+Fact RelTerm_implies_RelType: forall Gamma t T dt DT DT' (HDT : DT === DT' #in# PerType),
+  Gamma ||- t : T #aeq# dt #in# HDT ->
+  Gamma ||- T #in# HDT
+.
+Proof.
+intros.
+
+generalize dependent Gamma.
+generalize dependent t.
+generalize dependent T.
+generalize dependent dt.
+
+induction HDT using PerType_dind.
+
+intros.
+simpl in *; intros.
+program_simpl.
+
+intros.
+simpl in *.
+program_simpl.
+
+intros.
+simpl in *; intros.
+destruct H0 as [_H0 H0].
+destruct H0 as [A [F [? [? ?]]]].
+exists A F. repeat split; program_simpl; auto.
+program_simpl; auto.
+intros.
+edestruct H6 as [y]; eauto.
+program_simpl.
+eapply H. eauto.
+
+intros.
+simpl in *; intros.
+program_simpl.
+Qed.
+Hint Resolve RelTerm_implies_RelType.
+
+(******************************************************************************
+ * 
+ *)
+
+Fact RelTerm_has_Interp: forall Gamma t T dt DT DT' (HDT: DT === DT' #in# PerType),
+  Gamma ||- t : T #aeq# dt #in# HDT ->
+  exists PT, Interp DT PT 
+.
+Proof.
+intros.
+cut (Gamma ||- T #in# HDT); intros; eauto.
+Qed.
+Hint Resolve RelTerm_has_Interp.
+
+(******************************************************************************
+ * RelTerm respects Interp
+ *)
+
+Fact RelTerm_resp_Interp: forall Gamma t T dt DT DT' (HDT: DT === DT' #in# PerType) PT,
+  Gamma ||- t : T #aeq# dt #in# HDT ->
+ Interp DT PT ->
+ dt === dt #in# PT
+.
+Proof.
+intros.
+generalize dependent PT.
+induction HDT using PerType_dind; intros; simpl in *.
+(**)
+program_simpl; 
+clear_inversion H0;
+auto.
+(**)
+program_simpl; 
+clear_inversion H0;
+auto.
+(**)
+program_simpl.
+find_extdeters.
+apply H10.
+eauto.
+(**)
+program_simpl.
+clear_inversion H0.
+auto.
+Qed.
+Hint Resolve RelTerm_resp_Interp.
+
+(******************************************************************************
+ * RelType implies type judgemement
+ *)
+
+Fact RelType_implies_WfTp: forall Gamma T DT DT' (HDT : DT === DT' #in# PerType),
+  Gamma ||- T #in# HDT ->
+  Gamma |-- T
+.
+Proof.
+intros.
+induction HDT using PerType_dind; intros.
+
+simpl in H;eauto.
+simpl in H;eauto.
+simpl in H.
+program_simpl.
+eauto.
+
+simpl in H;eauto.
+Qed.
+Hint Resolve RelTerm_resp_Interp.
+
+Lemma SBID_inv: forall t T Gamma,
+  Gamma |-- TmSb t Sid : T ->
+  Gamma |-- t : T
+.
+Proof.
+intros.
+remember (TmSb t Sid).
+induction H; clear_inversion Heqt0.
+
+clear_inversion H.
+eapply CONV. eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SBID.
+eauto.
+eapply CONV.
+apply IHWtTm; eauto.
+eauto.
+Qed.
+Hint Resolve SBID_inv.
+
+(******************************************************************************
+ * RelTerm implies term judgemement
+ *)
+
+Fact RelTerm_implies_WtTm: forall Gamma t T dt DT DT' (HDT : DT === DT' #in# PerType),
+  Gamma ||- t : T #aeq# dt #in# HDT ->
+  Gamma |-- t : T
+.
+Proof.
+intros.
+induction HDT using PerType_dind; intros.
+(**)
+simpl in H; program_simpl.
+specialize (H1 Gamma 0).
+destruct H1. red; eauto.
+program_simpl.
+
+simpl in *.
+assert (Gamma |-- TmSb t Sid : TmNat).
+eapply WtTm_from_WtTmEq1; eauto.
+
+apply SBID_inv. 
+apply CONV with TmNat. auto.
+eauto.
+(**)
+simpl in H; program_simpl.
+specialize (H1 Gamma 0).
+destruct H1. red; eauto.
+program_simpl.
+
+simpl in *.
+assert (Gamma |-- TmSb t Sid : TmUnit).
+eapply WtTm_from_WtTmEq1; eauto.
+
+apply SBID_inv. 
+apply CONV with TmUnit. auto.
+eauto.
+(**)
+simpl in H.
+program_simpl.
+(**)
+simpl in H; program_simpl.
+specialize (H1 Gamma 0).
+destruct H1. red; eauto.
+program_simpl.
+
+simpl in *.
+assert (Gamma |-- TmSb t Sid : TmEmpty).
+eapply WtTm_from_WtTmEq1; eauto.
+
+apply SBID_inv. 
+apply CONV with TmEmpty. auto.
+eauto.
+Qed.
+
+(******************************************************************************
+ * RelTerm implies type judgemement
+ *)
+
+Fact RelTerm_implies_WfTp: forall Gamma t T dt DT DT' (HDT : DT === DT' #in# PerType),
+  Gamma ||- t : T #aeq# dt #in# HDT ->
+  Gamma |-- T
+.
+Proof.
+intros.
+eapply RelType_implies_WfTp.
+eapply RelTerm_implies_RelType.
+eauto.
+Qed.
+
+(******************************************************************************
+ * Proof irrelevance for Logical Relations
+ *
+ * Shape of the proof 'DT === DT #in# PerType' is irrelevant for satisfability
+ * of the relation.
+ *)
+
+Theorem Rel_ProofIrrelevance: forall Gamma T DT DT' (HDT HDT': DT === DT' #in# PerType),
+  (Gamma ||- T #in# HDT ->  Gamma ||- T #in# HDT') /\
+  (forall t dt, Gamma ||- t : T #aeq# dt #in# HDT -> Gamma ||- t : T #aeq# dt #in# HDT')
+.
+Proof.
+(* We need stronger induction hypothesis, with equivalence, not just implication *)
+cut (forall Gamma T DT DT' (HDT : DT === DT' #in# PerType), 
+  (forall DT_ DT_', DT = DT_ -> DT' = DT_' -> forall (HDT_ : DT_ === DT_' #in# PerType),
+    Gamma ||- T #in# HDT <-> Gamma ||- T #in# HDT_) /\
+  (forall t dt, 
+  forall DT_ DT_', DT = DT_ -> DT' = DT_' -> forall (HDT_ : DT_ === DT_' #in# PerType),
+    Gamma ||- t : T #aeq# dt #in# HDT <-> Gamma ||- t : T #aeq# dt #in# HDT_) 
+).
+intros; edestruct H; eauto.
+split; intros.
+apply H0; eauto.
+apply H1; eauto.
+(**)
+intros until HDT.
+generalize dependent Gamma.
+generalize dependent T.
+induction HDT using PerType_dind; 
+  try solve [
+    intros; split; intros; split; intros;
+    induction HDT_ using PerType_dind; intros; try solve [try clear_inversion H0; try clear_inversion H1];
+     auto
+  ].
+
+renamer.
+rename i into HDAPerType.
+rename e into HAppDF.
+rename e0 into HAppDF'.
+rename i1 into HAppPerType.
+rename IHHDT into IH1.
+rename H into IH2.
+rename i0 into HPDA.
+
+split; intros.
+
+(* Dfun RelType *)
+induction HDT_ using PerType_dind; intros; try solve [clear_inversion H0].
+symmetry in H0.
+symmetry in H.
+clear_inversion H0.
+clear_inversion H.
+rename e into HAppDF2.
+rename e0 into HAppDF'2.
+renamer; intros.
+rename i1 into HAppPerType2.
+rename i2 into HPDA0.
+rename i into HDAPerType2.
+rename i0 into WEIRD.
+
+(* -> *)
+split. intro HRelT.
+
+simpl in HRelT.
+destruct HRelT as [A [F HRelT]].
+exists A F.
+program_simpl.
+repeat (split; eauto).
+(**)
+destruct IH1 with (T := A) (Gamma := Gamma) as [IH1a IH1b].
+apply IH1a; auto.
+(**)
+intros.
+move IH2 at bottom.
+specialize (IH2 da da DB DB' PA).
+specialize (IH2 HPA Hda Happ Happ').
+specialize (IH2 (TmSb F (Sext (Sups i) a))).
+specialize (IH2 Delta).
+destruct IH2 as [IH2a IH2b].
+apply IH2a; auto.
+apply H2; auto.
+move IH1 at bottom.
+specialize (IH1 (TmSb A (Sups i))).
+specialize (IH1 Delta).
+destruct IH1 as [IH1a IH1b].
+edestruct IH1b as [IH1b' IH1b'']; eauto.
+
+(* <- *)
+intro HRelT.
+
+simpl in HRelT.
+destruct HRelT as [A [F HRelT]].
+exists A F.
+program_simpl.
+repeat (split; eauto).
+(**)
+destruct IH1 with (T := A) (Gamma := Gamma) as [IH1a IH1b].
+edestruct IH1a as [IH1a' IH1a'']; eauto.
+(**)
+intros.
+move IH2 at bottom.
+specialize (IH2 da da DB DB' PA).
+specialize (IH2 HPA Hda Happ Happ').
+specialize (IH2 (TmSb F (Sext (Sups i) a))).
+specialize (IH2 Delta).
+destruct IH2 as [IH2a IH2b].
+specialize (IH2a DB DB' eq_refl eq_refl).
+specialize (IH2a (HAppPerType2 da da DB DB' PA HPA Hda Happ Happ')).
+destruct (IH2a) as [IH2a' IH2a''].
+
+apply IH2a''; auto.
+apply H2; auto.
+move IH1 at bottom.
+specialize (IH1 (TmSb A (Sups i))).
+specialize (IH1 Delta).
+destruct IH1 as [IH1a IH1b].
+apply IH1b; auto.
+
+(* Dfun RelType *)
+induction HDT_ using PerType_dind; intros; try solve [clear_inversion H0].
+symmetry in H0.
+symmetry in H.
+clear_inversion H0.
+clear_inversion H.
+rename e into HAppDF2.
+rename e0 into HAppDF'2.
+renamer; intros.
+rename i1 into HAppPerType2.
+rename i2 into HPDA0.
+rename i into HDAPerType2.
+rename i0 into WEIRD.
+split.
+
+(* -> *)
+intro HRelT.
+
+simpl in HRelT.
+destruct HRelT as [HDeriv [A [F [PT HRelT]]]].
+split; auto.
+exists A F PT.
+program_simpl.
+repeat (split; eauto).
+(**)
+destruct IH1 with (T := A) (Gamma := Gamma) as [IH1a IH1b].
+apply IH1a; auto.
+(**)
+intros.
+edestruct H4 as [dy]; eauto.
+destruct IH1 with (T := TmSb A (Sups i)) (Gamma := Delta) as [IH1a IH1b].
+specialize (IH1b a da DA DA' eq_refl eq_refl).
+specialize (IH1b HDAPerType2).
+destruct IH1b as [IH1b' IH1b''].
+apply IH1b''.
+auto.
+
+destruct H7.
+exists dy. split; auto.
+
+move IH2 at bottom.
+specialize (IH2 da da DB DB' PA).
+specialize (IH2 HPA Hda Happ Happ').
+specialize (IH2 (TmSb F (Sext (Sups i) a))).
+specialize (IH2 Delta).
+destruct IH2 as [IH2a IH2b].
+apply IH2b; auto.
+eauto.
+
+(* <- *)
+intro HRelT.
+
+simpl in HRelT.
+destruct HRelT as [HDeriv [A [F [PT HRelT]]]].
+split; auto.
+exists A F PT.
+program_simpl.
+repeat (split; eauto).
+(**)
+destruct IH1 with (T := A) (Gamma := Gamma) as [IH1a IH1b].
+edestruct IH1a as [IH1a' IH1a'']; eauto.
+(**)
+intros.
+edestruct H4 as [dy]; eauto.
+destruct IH1 with (T := TmSb A (Sups i)) (Gamma := Delta) as [IH1a IH1b].
+apply IH1b; auto. eauto.
+destruct H7.
+exists dy. split; auto.
+move IH2 at bottom.
+specialize (IH2 da da DB DB' PA).
+specialize (IH2 HPA Hda Happ Happ').
+specialize (IH2 (TmSb F (Sext (Sups i) a))).
+specialize (IH2 Delta).
+destruct IH2 as [IH2a IH2b].
+specialize (IH2b ( TmApp (TmSb t (Sups i)) a) dy DB DB' eq_refl eq_refl).
+specialize (IH2b (HAppPerType2 da da DB DB' PA HPA Hda Happ Happ')).
+destruct IH2b as [IH2b' IH2b''].
+apply IH2b''; auto.
+eauto.
+Qed.
+

Nbe/Model/LogRelTm/ClosedForConversion.v

+
+(******************************************************************************
+ * Pawel Wieczorek
+ *)
+
+Set Implicit Arguments.
+
+(*
+Add Rec LoadPath "../../Nbe" as Nbe.
+ *)
+Add Rec LoadPath "../../Nbe" as Nbe.
+
+Require Import Arith.
+Require Import Arith.Plus.
+
+Require Import Program.
+Require Import Program.Tactics.
+Require Import Program.Equality.
+Require Import Setoid.
+Require Import Relations.Relation_Definitions.
+Require Import Classes.RelationClasses.
+
+
+Require Import Nbe.Syntax.
+Require Import Nbe.Domain.
+Require Import Nbe.Utils.
+Require Import Nbe.Model.PER.
+Require Import Nbe.Model.Interp.
+Require Import Nbe.Model.Valid.
+Require Import Nbe.Model.Terminating.
+Require Import Nbe.Model.LogRelTm.Def.
+Require Import Nbe.Model.LogRelTm.BasicFacts.
+Require Import Nbe.Model.LogRelTm.ProofIrrelevance.
+
+
+(******************************************************************************
+ * Closure under conversion
+ *)
+
+Theorem ClosedForConversion: forall Gamma T DT DT' (HDT: DT === DT' #in# PerType),
+  Gamma ||- T #in# HDT -> forall T',
+  Gamma |-- T === T' ->
+  (Gamma ||- T' #in# HDT) /\
+  (forall dt t t', Gamma ||- t : T #aeq# dt #in# HDT ->  Gamma |-- t === t' : T ->  Gamma ||- t' : T' #aeq# dt #in# HDT)
+.
+Proof.
+do 5 intro.
+generalize dependent Gamma.
+generalize dependent T.
+induction HDT using PerType_dind; intros.
+
+
+(* Dnat *)
+simpl in *; program_simpl.
+repeat split; eauto; intros.
+decompose record H1.
+eauto.
+decompose record H1.
+edestruct H7; eauto.
+exists x. program_simpl; repeat split.
+assumption.
+eapply EQ_TRANS; eauto using H8.
+eapply EQ_CONV; eauto.
+
+(* Dunit *)
+simpl in *.
+repeat split; eauto; intros.
+decompose record H1.
+eauto.
+decompose record H1.
+edestruct H7; eauto.
+exists x. program_simpl; repeat split.
+assumption.
+eapply EQ_TRANS; eauto using H8.
+eapply EQ_CONV; eauto.
+
+(* Dfun *)
+
+repeat split.
+simpl in *.
+
+destruct H0 as [A [F [? ?]]].
+exists A F.
+program_simpl.
+repeat split; auto.
+eapply EQ_TP_TRANS; eauto using H0.
+
+(**)
+
+eauto.
+
+(**)
+
+intros.
+renamer.
+rename i into HDA.
+rename i1 into HDB.
+rename i0 into HPA.
+intros.
+
+simpl.
+rename H0 into K_T.
+rename H2 into K_t.
+
+set (H_t := K_t).
+specialize (H_t).
+simpl in H_t.
+destruct H_t as [_H_t H_t].
+destruct H_t as [A [F [PT ?]]].
+program_simpl.
+renamer.
+intros.
+exists A F PT.
+repeat split; auto.
+eapply EQ_TP_TRANS; eauto using H1.
+
+intros.
+find_extdeters.
+close_extdeters.
+close_doms.
+renamer; intros.
+
+edestruct (H6 Delta i a da DB DB' PDA0 HPA1 Hda Happ Happ') as [dy ?]; eauto.
+exists dy.
+program_simpl.
+repeat split; auto.
+
+move H at bottom.
+specialize (H da da DB DB' PDA0).
+
+specialize (H HPA1 Hda).
+specialize (H Happ Happ').
+specialize (H (TmSb F (Sext (Sups i) a)) Delta).
+
+assert (Delta ||- TmSb F (Sext (Sups i) a) #in# HDB da da DB DB' PDA0 HPA1 Hda Happ Happ' ).
+eapply RelTerm_implies_RelType; eauto.
+specialize (H H15).
+specialize (H (TmSb F (Sext (Sups i) a))).
+
+assert (Delta |-- TmSb F (Sext (Sups i) a) === TmSb F (Sext (Sups i) a)).
+eapply EQ_TP_REFL.
+
+eapply RelType_implies_WfTp.
+eauto.
+
+specialize (H H16).
+destruct H.
+specialize (H17 dy (TmApp (TmSb t (Sups i)) a)).
+specialize (H17 (TmApp (TmSb t' (Sups i)) a)).
+apply H17.
+auto.
+
+(**)
+
+assert (Gamma |-- A /\ Gamma,,A |-- F).
+eapply Inversion_FUN_E.
+eauto.
+destruct H18.
+
+
+
+assert (Delta |-- a : TmSb A (Sups i)).
+eapply RelTerm_implies_WtTm.
+eauto.
+
+assert (Delta |-- TmSb A (Sups i)).
+eapply WfTp_from_WtTm.
+eauto.
+
+assert (Delta |-- a : TmSb (TmSb A (Sups i)) Sid).
+eapply CONV.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SBID.
+auto.
+
+assert (Delta,, TmSb A (Sups i) |-- TmVar : TmSb A (Sseq (Sups i) Sup)).
+eapply CONV.
+eapply HYP.
+eauto.
+eauto.
+
+assert (Delta |--  [Sext Sid a]: Delta,,TmSb A (Sups i)) by eauto.
+
+
+assert (Delta |-- TmSb F (Sext (Sups i) a) === TmSb (TmSb F (Sext (Sups (S i)) TmVar)) (Ssing a)).
+
+
+eapply EQ_TP_SYM.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+unfold Ssing.
+eauto.
+eapply SEXT.
+simpl.
+eapply SSEQ.
+eapply SUP.
+assumption.
+apply H7.
+eauto.
+simpl.
+eauto.
+eauto.
+eapply EQ_TP_CONG_SB.
+unfold Ssing.
+eapply EQ_SB_TRANS.
+eapply EQ_SB_SEXT.
+eauto.
+eapply SEXT.
+simpl.
+eapply SSEQ.
+eauto.
+apply H7.
+eauto.
+simpl.
+auto.
+
+assert (   Delta,, TmSb A (Sups i) |--  [Sups (S i)]=== [Sseq Sup (Sups i)]:Gamma).
+apply Sups_tail.
+simpl.
+eapply SSEQ.
+eauto.
+eauto.
+
+eapply EQ_SB_CONG_SEXT.
+eapply EQ_SB_TRANS.
+
+simpl.
+eapply EQ_SB_COMM.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_SB_TRANS.
+eapply EQ_SB_CONG_SSEQ.
+eapply EQ_SB_SUP.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_SB_REFL.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_CONV.
+eapply EQ_SBVAR.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_TP_TRANS.
+eapply EQ_TP_SBSEQ.
+eauto.
+eauto.
+eauto.
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_SYM.
+simpl.
+
+eapply EQ_SB_TRANS.
+eapply EQ_SB_COMM.
+eauto.
+eauto.
+eauto.
+
+eapply EQ_SB_CONG_SSEQ.
+eapply EQ_SB_SUP.
+eauto.
+eauto.
+eauto.
+eapply EQ_SB_REFL.
+eauto.
+eauto.
+eauto.
+
+(**)
+
+eapply EQ_CONV.
+eapply EQ_CONG_FUN_E.
+eapply EQ_CONV.
+eapply EQ_CONG_SB.
+eapply EQ_SB_REFL.
+eauto.
+eauto.
+eapply EQ_TP_TRANS.
+eapply EQ_TP_CONG_SB.
+eapply EQ_SB_REFL.
+eauto.
+eauto.
+eauto.
+eapply EQ_REFL.
+eauto.
+
+(**)
+
+auto.
+
+(* Dempty *)
+simpl in *.
+repeat split; eauto; intros.
+decompose record H1.
+eauto.
+decompose record H1.
+edestruct H7; eauto.
+exists x. program_simpl; repeat split.
+assumption.
+eapply EQ_TRANS; eauto using H8.
+eapply EQ_CONV; eauto.
+Qed.
+
+(******************************************************************************
+ * Closure under conversion (unpacking)
+ *)
+
+Corollary RelType_ClosedForConversion: forall Gamma T DT DT' (HDT: DT === DT' #in# PerType) T',
+  Gamma ||- T #in# HDT ->
+  Gamma |-- T === T' ->
+  (Gamma ||- T' #in# HDT)
+.
+Proof.
+intros.
+edestruct ClosedForConversion; eauto.
+Qed.
+
+Corollary RelTerm_ClosedForConversion: forall Gamma T DT DT' (HDT: DT === DT' #in# PerType) T' dt t t',
+  Gamma ||- T #in# HDT -> 
+  Gamma |-- T === T' ->
+  Gamma ||- t : T #aeq# dt #in# HDT ->  Gamma |-- t === t' : T ->  Gamma ||- t' : T' #aeq# dt #in# HDT
+.
+Proof.
+intros.
+edestruct ClosedForConversion; eauto.
+Qed.
+

Nbe/Model/LogRelTm/ClosedUnderPer.v

+
+(******************************************************************************
+ * Pawel Wieczorek
+ *)
+
+Set Implicit Arguments.
+
+(*
+Add Rec LoadPath "../../Nbe" as Nbe.
+ *)
+Add Rec LoadPath "../../Nbe" as Nbe.
+
+Require Import Arith.
+Require Import Arith.Plus.
+
+Require Import Program.
+Require Import Program.Tactics.
+Require Import Program.Equality.
+Require Import Setoid.
+Require Import Relations.Relation_Definitions.
+Require Import Classes.RelationClasses.
+
+
+Require Import Nbe.Syntax.
+Require Import Nbe.Domain.
+Require Import Nbe.Utils.
+Require Import Nbe.Model.PER.
+Require Import Nbe.Model.Interp.
+Require Import Nbe.Model.Valid.
+Require Import Nbe.Model.Terminating.
+
+Require Import Nbe.Model.LogRelTm.Def.
+Require Import Nbe.Model.LogRelTm.BasicFacts.
+Require Import Nbe.Model.LogRelTm.ProofIrrelevance.
+Require Import Nbe.Model.LogRelTm.ClosedForConversion.
+
+(******************************************************************************
+ * Closure under PERs
+ *)
+
+Lemma Reflects_same: forall dt dt' DT PT n v,
+  DT === DT #in# PerType ->
+  Interp DT PT ->
+  dt === dt' #in# PT ->
+  RbNf n (Ddown DT dt) v ->
+  RbNf n (Ddown DT dt') v
+.
+Proof.
+intros.
+
+assert (Ddown DT dt === Ddown DT dt' #in# PerNf).
+eapply Reify_Characterization; eauto.
+clear_inversion H3.
+destruct (H4 n) as [v'].
+program_simpl.
+assert (v = v').
+eapply RbNf_deter; eauto.
+subst.
+assumption.
+Qed.  
+Hint Resolve Reflects_same.
+
+
+Theorem ClosedUnderPer: forall Gamma T DT DT' (HDT : DT === DT' #in# PerType),
+  Gamma ||- T #in# HDT -> 
+  forall DT'' (HDT' : DT' === DT'' #in# PerType),
+  Gamma ||- T #in# HDT' /\
+ (forall t dt dt' PT, Gamma ||- t : T #aeq# dt #in# HDT -> dt === dt' #in# PT -> Interp DT PT ->
+   Gamma ||- t : T #aeq# dt' #in# HDT').
+
+Proof.
+(* Stronger induction hypothesis is required *)
+cut (forall Gamma T DT DT' (HDT : DT === DT' #in# PerType),
+  forall DT'' (HDT' : DT' === DT'' #in# PerType), (Gamma ||- T #in# HDT <-> Gamma ||- T #in# HDT')
+/\
+  (forall t dt dt' PT, dt === dt' #in# PT -> Interp DT PT ->
+    (Gamma ||- t : T #aeq# dt #in# HDT <-> Gamma ||- t : T #aeq# dt' #in# HDT'))
+).
+intros.
+specialize (H Gamma T DT DT' HDT DT'' HDT').
+program_simpl.
+repeat (split; auto).
+apply H.
+auto.
+
+intros.
+eapply H1; eauto.
+(**)
+
+intros until HDT.
+cut (DT' = DT'); auto.
+generalize DT' at 1 3 5 7 as DT'_.
+generalize dependent Gamma.
+generalize dependent T.
+(* Theorem for RelType for base types are solved by simple destruction and inversion! *)
+induction HDT using PerType_dind; split; intros;
+  try solve [
+    destruct HDT'; try solve [ clear_inversion H ];
+    split; auto
+      ].
+
+(* RelTerm Dnat *)
+
+destruct HDT'; try solve [clear_inversion H ].
+clear_inversion H1.
+
+split; intro;
+close_doms; auto; split; auto; intros;
+split; intros; simpl in *; program_simpl; auto;
+edestruct H6 as [v]; program_simpl; eauto.
+
+(* <- *)
+
+exists v. split; auto.
+apply Reflects_same with dt' PerNat; auto.
+symmetry; auto.
+
+(* RelTerm Dunit *)
+
+destruct HDT'; try solve [clear_inversion H ].
+clear_inversion H1.
+
+split; intro;
+close_doms; auto; split; auto; intros;
+split; intros; simpl in *; program_simpl; auto;
+edestruct H6 as [v]; program_simpl; eauto.
+
+(* RelType Dfun  *)
+
+renamer.
+rename i into HDA.
+rename i0 into HPDA.
+rename i1 into H_PDB.
+destruct HDT'; try solve [clear_inversion H0].
+clear_inversion H0.
+renamer.
+rename i0 into HPDA'.
+rename i1 into H_PDB'.
+rename i into HDA'.
+rename e1 into e'.
+rename e2 into e0'.
+
+(* ->  *)
+
+split; intro HS.
+simpl in HS.
+destruct HS as [A [F [HS1 [HS2 HS3 ]]]].
+simpl. exists A F.
+repeat (split; auto).
+
+specialize (IHHDT A Gamma _ eq_refl).
+edestruct IHHDT as [IHHDT_Type IHHDT_Term].
+(*specialize (IHHDT_Type _ HDA').*)
+apply IHHDT_Type; auto.
+
+(**)
+
+intros.
+renamer.
+assert (Interp DA' PDA) by (eapply Interp_resp_PerType; eauto).
+find_extdeters.
+close_doms.
+
+destruct e with da as [DB_].
+eauto.
+
+destruct e' with da as [DB_'].
+eauto.
+
+
+specialize (HS3 Delta i a da DB_ DB_' PDA).
+specialize (HS3 HPDA).
+assert (da === da #in# PDA) as HdadaPDA.
+apply H3.
+auto.
+specialize (HS3 HdadaPDA H9 H10 H0).
+
+assert ( Delta ||- a : TmSb A (Sups i) #aeq# da #in# HDA ) as HS1_P.
+specialize (IHHDT (TmSb A (Sups i)) Delta _ eq_refl).
+edestruct IHHDT as [IHHDT_Type IHHDT_Term].
+move IHHDT_Term at bottom.
+specialize (IHHDT_Term a da da PDA HdadaPDA HPDA).
+apply IHHDT_Term.
+eauto.
+
+specialize (HS3 HS1_P).
+
+move H at bottom.
+
+assert (DB_' = DB) by eauto 2; subst.
+
+
+specialize (H _ _ _ _ PDA HPDA HdadaPDA H9 H10).
+specialize (H ( TmSb F (Sext (Sups i) a))).
+specialize (H Delta _ eq_refl _ (H_PDB' da da DB DB' PDA'0 HPA Hda Happ Happ' ) ).
+destruct H.
+eapply H; auto.
+
+(* <- *)
+
+simpl in HS.
+destruct HS as [A [F [HS1 [HS2 HS3 ]]]].
+simpl. exists A F.
+repeat (split; auto).
+
+specialize (IHHDT A Gamma _ eq_refl).
+edestruct IHHDT as [IHHDT_Type IHHDT_Term].
+(*specialize (IHHDT_Type _ HDA').*)
+apply IHHDT_Type; eauto.
+
+(**)
+
+intros.
+renamer.
+assert (Interp DA PDA').
+eapply Interp_resp_PerType.
+eauto 1.
+symmetry; auto.
+
+find_extdeters.
+close_doms.
+ 
+destruct e' with da as [DB_].
+eauto.
+
+destruct e0' with da as [DB_'].
+eauto.
+
+specialize (HS3 Delta i a da DB_ DB_' PDA').
+specialize (HS3 HPDA').
+assert (da === da #in# PDA') as HdadaPDA'.
+eauto.
+
+assert (DB' = DB_) by eauto 2; subst.
+
+specialize (HS3 HdadaPDA' H9 H10 H0).  
+
+assert ( Delta ||- a : TmSb A (Sups i) #aeq# da #in# HDA' ) as HS1_P.
+specialize (IHHDT (TmSb A (Sups i)) Delta _ eq_refl).
+edestruct IHHDT as [IHHDT_Type IHHDT_Term].
+move IHHDT_Term at bottom.
+specialize (IHHDT_Term a da da _ HdadaPDA' H2).
+apply IHHDT_Term.
+eauto.
+
+
+specialize (HS3 HS1_P).
+
+move H at bottom.
+
+specialize (H _ _ _ _ PDA0 HPA Hda Happ Happ').
+specialize (H ( TmSb F (Sext (Sups i) a))).
+specialize (H Delta _ eq_refl).
+specialize (H _ ( H_PDB' da da DB_ DB_' PDA' HPDA' HdadaPDA' H9 H10 )).
+destruct H.
+eapply H; auto.
+
+(* RelTerm Dfun *)
+
+renamer.
+rename i into HDA.
+rename i0 into HPDA.
+rename i1 into H_PDB.
+destruct HDT'; try solve [clear_inversion H0].
+clear_inversion H0.
+renamer.
+rename i0 into HPDA'.
+rename i1 into H_PDB'.
+rename i into HDA'.
+rename e1 into e'.
+rename e2 into e0'.
+
+(* ->  *)
+
+split; intro HS.
+simpl in HS.
+destruct HS as [? [A [F [Pfun [HS1 [HS2 [HS3 [HS4 HS5]]]]]]]].
+simpl. split; auto. exists A F Pfun.
+repeat (split; auto).
+
+apply Interp_resp_PerType with (DA := Dfun DA DF); auto.
+eapply PerType_arr; eauto 4.
+find_extdeters.
+close_extdeters.
+eauto.
+
+(**)
+
+specialize (IHHDT A Gamma _ eq_refl).
+edestruct IHHDT as [IHHDT_Type IHHDT_Term].
+(*specialize (IHHDT_Type _ HDA').*)
+apply IHHDT_Type; auto.
+
+(**)
+
+intros.
+renamer.
+assert (Interp DA' PDA) by (eapply Interp_resp_PerType; eauto).
+find_extdeters.
+close_doms.
+
+destruct e with da as [DB_].
+eauto.
+
+destruct e' with da as [DB_'].
+eauto.
+
+
+specialize (HS5 Delta i a da DB_ DB_' PDA).
+specialize (HS5 HPDA).
+assert (da === da #in# PDA) as HdadaPDA.
+eauto.
+specialize (HS5 HdadaPDA H15 H16 H3).
+
+assert ( Delta ||- a : TmSb A (Sups i) #aeq# da #in# HDA ) as HS1_P.
+specialize (IHHDT (TmSb A (Sups i)) Delta _ eq_refl).
+edestruct IHHDT as [IHHDT_Type IHHDT_Term].
+move IHHDT_Term at bottom.
+specialize (IHHDT_Term a da da PDA HdadaPDA HPDA).
+apply IHHDT_Term.
+eauto.
+
+specialize (HS5 HS1_P).
+clear_inversion H2.
+
+clear_inversion H1.
+find_extdeters.
+close_extdeters.
+specialize (H2 da da H17).
+destruct H2 as [y0 [y1 [Y HY]]].
+destruct HY as [HY [Hy0 [Hy1 HyyY]]].
+destruct HS5 as [dy HS6].
+program_simpl.
+assert (dy = y0) by eauto 2; subst.
+exists y1.
+split; auto.
+
+move H at bottom.
+
+assert (DB_' = DB) by eauto 2; subst.
+
+
+specialize (H _ _ _ _ PDA HPDA HdadaPDA H15 H16).
+specialize (H ( TmSb F (Sext (Sups i) a))).
+specialize (H Delta _ eq_refl _ (H_PDB' da da DB DB' PDA'0 HPA Hda Happ Happ' ) ).
+destruct H.
+eapply H25.
+eauto.
+eauto.
+eauto.
+
+(* <- *)
+
+simpl in HS.
+destruct HS as [? [A [F [Pfun [HS1 [HS2 [HS3 [HS4 HS5]]]]]]]].
+simpl. split; auto. exists A F Pfun.
+
+assert (Interp (Dfun DA DF) Pfun).
+apply Interp_resp_PerType with (DA := Dfun DA' DF'); auto.
+symmetry.
+eapply PerType_arr; eauto 4.
+
+
+repeat (split; auto).
+find_extdeters.
+close_extdeters.
+eauto.
+
+(**)
+
+specialize (IHHDT A Gamma _ eq_refl).
+edestruct IHHDT as [IHHDT_Type IHHDT_Term].
+(*specialize (IHHDT_Type _ HDA').*)
+apply IHHDT_Type; eauto.
+
+(**)
+
+intros.
+renamer.
+
+assert (Interp DA PDA').
+eapply Interp_resp_PerType.
+eauto 1.
+symmetry; auto.
+
+find_extdeters.
+close_doms.
+ 
+destruct e' with da as [DB_].
+eauto.
+
+destruct e0' with da as [DB_'].
+eauto.
+
+assert (DB' = DB_) by eauto 2; subst.
+
+specialize (HS5 Delta i a da DB_ DB_' PDA').
+specialize (HS5 HPDA').
+assert (da === da #in# PDA') as HdadaPDA'.
+eauto.
+specialize (HS5 HdadaPDA' H16 H17 H4).
+
+
+assert ( Delta ||- a : TmSb A (Sups i) #aeq# da #in# HDA' ) as HS1_P.
+specialize (IHHDT (TmSb A (Sups i)) Delta _ eq_refl).
+edestruct IHHDT as [IHHDT_Type IHHDT_Term].
+move IHHDT_Term at bottom.
+specialize (IHHDT_Term a da da _ HdadaPDA' H6).
+eauto.
+apply IHHDT_Term.
+eauto.
+
+
+specialize (HS5 HS1_P).
+clear_inversion H2.
+clear_inversion H1.
+find_extdeters.
+close_extdeters.
+specialize (H2 da da H23).
+destruct H2 as [y0 [y1 [Y HY]]].
+destruct HY as [HY [Hy0 [Hy1 HyyY]]].
+destruct HS5 as [dy HS6].
+program_simpl.
+assert (dy = y1) by eauto 2; subst.
+exists y0.
+split; auto.
+
+move H at bottom.
+
+specialize (H _ _ _ _ _ HPA Hda Happ Happ').
+specialize (H ( TmSb F (Sext (Sups i) a))).
+specialize (H Delta _ eq_refl _ (H_PDB' da da _ _ PDA' HPDA' HdadaPDA' H16 H17 ) ).
+destruct H.
+eapply H28.
+eauto.
+eauto.
+eauto.
+
+(* RelTerm Dempty *)
+
+destruct HDT'; try solve [clear_inversion H ].
+clear_inversion H1.
+
+split; intro;
+close_doms; auto; split; auto; intros;
+split; intros; simpl in *; program_simpl; auto;
+edestruct H6 as [v]; program_simpl; eauto.
+
+(* <- *)
+
+exists v. split; auto.
+apply Reflects_same with dt' PerEmpty; auto.
+symmetry; auto.
+
+Qed.
+
+
+(***************************************************************************
+ * Unpacking and helpers.
+ *)
+