Commits

Paweł Wieczorek committed ca18e60

Added _weird* and _tail\ Nbe/Syntax/CxtShift.v

Comments (0)

Files changed (2)

Nbe/Model/LogRelSb.v

 eauto.
 Qed.
 
+(*
 Lemma tmVar_cxt: forall i Gamma Delta T,
   Gamma |-- tmVar i : T ->
   Gamma |-- [Sups i] : Delta ->
 split; auto.
 
 Qed.
-
+*)
+
+(*
 Lemma tmVar_sups: forall i Gamma Delta T,
   Gamma |-- tmVar i : T ->
   Gamma |-- [Sups i] : Delta ->
 
 
 Qed.
-
+*)
+
+(*
 Lemma tmVar_sups: forall j Gamma i T,
   Gamma |-- tmVar i : T ->
   Gamma |-- TmSb (tmVar i) (Sups j) === tmVar (i+j) : TmSb T (Sups j)
 
 
 Qed.
+*)
 
 Lemma RbNe_Lift: forall d nd Gamma,
   RbNe (length Gamma) d nd -> forall Delta nd' A i,
 
 destruct RelType_Reify_ as [NFA' [HNFA1' HNFA''] ].
 renamer.
-
+admit.
 
 Qed.
 
+
 Theorem Rel_Fundamental: 
     (forall Gamma, Gamma |-- -> True) /\
 
 (******************************************************************************
  * Identity environments
  *)
-
+ 
 
 Lemma RelSid_Var: forall DT DT' (HDT : DT === DT' #in# PerType) Gamma T denv,
   Gamma,,T |-- TmVar : TmSb T Sup ->
 split.
 unfold Ddown; unfold Dup; simpl.
 eauto.
-red in H3.
+red in H3. 
+eapply EQ_CONV.
+
+simpl in H0.
+
+eapply CxtShift_TmVarSups.
+eauto.
+eauto.
+
 admit.
 
 
 admit.
 
 Qed.
- 
+*) 
+
+
 
 Lemma RelSid: forall Gamma denv,
   Gamma |-- -> EvalCxt Gamma denv -> Gamma ||- [Sid] : Gamma #aeq# denv
 eapply EQ_SB_SIDL.
 auto.
 apply RelSb_lift1; auto.
+(**)
+
+
+
+(*old*)
+
+apply RelSb_ClosedUnderEq with (sb1 := Sext Sup TmVar); auto.
+econstructor 2.
+eapply HSup. 
+
+eapply Rel_Fundamental_Tp with (Gamma := Gamma) (T := A) (Delta := (Gamma,,A)) (SB := Sup) (denv := denv); auto.
+eauto.
+renamer.
+assert (DA_denv0 = DA_denv) by eauto.
+subst. clear_dups.
+
+
+eauto.
+eapply RelSid_Var; eauto.
 
 (*
 eapply Rel_Fundamental_Tp with (Gamma := Gamma) (T := A) (Delta := (Gamma,,A)) (SB := Sup) (denv := denv); auto.

Nbe/Syntax/CxtShift.v

 Qed.
 
 
+
+Fact Sups_tail': forall i Gamma T Delta,
+  CxtShift Delta i (Gamma,,T) ->
+  Delta |-- [Sseq (Sups i) Sup] === [Sseq Sup (Sups i)] : Gamma
+.
+Proof.
+intros.
+red in H.
+
+assert (Gamma,,T |--) as HGT.
+eauto.
+
+clear_inversion HGT.
+
+
+
+assert (Delta |-- [Sseq Sup (Sups i)] : Gamma) as Hsseq.
+eapply SSEQ.
+eauto.
+simpl.
+eapply SUP.
+eauto.
+
+
+eapply Sups_tail.
+simpl.
+eapply Sups_tail_iff.
+eauto.
+Qed.
+
+
+
 (******************************************************************************
  * Basic properties
  *)
 (******************************************************************************
  *)
 
+(*
+ Gamma : list Tm
+  T : Tm
+  denv : DEnv
+  H : Gamma,, T |-- TmVar : TmSb T Sup
+  H0 : Gamma,, T |-- TmSb T Sup === TmNat
+  H1 : EvalCxt Gamma denv
+  H2 : EvalTm T denv Dnat
+  Delta : Cxt
+  i : nat
+  H3 : Delta |--  [Sups i]:Gamma,, T
+  ============================
+   Delta |-- TmSb T (Sseq (Sups i) Sup) === TmNat
+
+
+*)
+
+Lemma Sups_weird: forall Gamma T Delta i,
+  CxtShift Delta i (Gamma,,T) ->
+  Delta |-- TmSb T (Sseq (Sups i) Sup) === TmSb T (Sseq Sup (Sups i))
+.
+Proof.
+intros.
+eapply EQ_TP_CONG_SB.
+eapply Sups_tail'.
+eauto.
+red in H.
+eapply EQ_TP_REFL.
+assert (Gamma,,T |--).
+eauto.
+clear_inversion H0.
+auto.
+Qed.
+
+Lemma Sups_weird': forall Gamma T Delta i,
+  CxtShift Delta i (Gamma,,T) ->
+  Delta |-- TmSb T (Sseq (Sups i) Sup) === TmSb (TmSb T Sup) (Sups i)
+.
+Proof.
+intros.
+
+assert (Gamma,,T |--).
+eauto.
+clear_inversion H0.
+
+
+eapply EQ_TP_TRANS.
+eapply Sups_weird.
+eauto.
+eapply EQ_TP_SYM.
+eapply EQ_TP_SBSEQ.
+eauto.
+eapply SUP.
+eauto.
+eauto.
+Qed.
+
+
+Lemma Sups_weird'': forall Gamma T A Delta i,
+  CxtShift Delta i (Gamma,,T) ->
+  Gamma,,T |-- TmSb T Sup === A ->
+  Delta |-- TmSb T (Sseq (Sups i) Sup) === TmSb A (Sups i)
+.
+Proof.
+intros.
+
+assert (Gamma,,T |--).
+eauto.
+clear_inversion H1.
+
+eapply EQ_TP_TRANS.
+eapply Sups_weird'.
+eauto.
+
+eapply EQ_TP_CONG_SB.
+eauto.
+eauto.
+Qed.
 
 (******************************************************************************
  * Lengths