1. Paweł Wieczorek
  2. MgrCoq

Commits

Paweł Wieczorek  committed e744f36

less admits!

  • Participants
  • Parent commits 17af9db
  • Branches another_weird_rule

Comments (0)

Files changed (1)

File Nbe/Model/LogRelSb.v

View file
  • Ignore whitespace
 eauto.
 
 (* Dfun *)
+
+simpl.
+repeat (split; eauto).
+simpl in H1.
+
+destruct H1 as [TA [TF HREST]].
+exists TA TF.
+
+assert (exists PT, Interp (Dfun DA DF) PT) as HPT.
+eauto.
+destruct HPT as [PT HPT].
+exists PT.
+
+destruct HREST as [HF1 HREST].
+destruct HREST as [HF2 HREST].
+
+repeat (split; eauto).
+
+eapply Reflect_Characterization.
+eauto.
+eauto.
+eauto.
+
+(**)
+
+intros.
+
+exists (Dup DB (Dapp (Dvar (length Gamma)) (Ddown DA da))).
+split.
+
+unfold Dup at 1.
+simpl.
+eauto.
+(*.*)
+
+eapply RelTerm_Back.
+eauto.
+
+constructor 1.
+intros.
+
+assert (exists nv, RbNe m (Dvar (length Gamma)) nv) as Hnv.
+eexists.
+eauto.
+
+assert (exists na, RbNf m (Ddown DA da) na) as Hna.
+assert (Ddown DA da === Ddown DA da #in# PerNf) as HDAda.
+eapply Reify_Characterization.
+eauto.
+eauto.
+eauto.
+
+clear_inversion HDAda.
+destruct (H5 m).
+destruct H6.
+eauto.
+
+destruct Hnv as [nv].
+destruct Hna as [na].
+exists (TmApp nv na).
+
+split; auto.
+(***)
+intros.
+
+set (m := length Delta0).
+
+assert (exists nv, RbNe m (Dvar (length Gamma)) nv) as Hnv.
+eexists.
+eauto.
+
+assert (exists na, RbNf m (Ddown DA da) na) as Hna.
+assert (Ddown DA da === Ddown DA da #in# PerNf) as HDAda.
+eapply Reify_Characterization.
+eauto.
+eauto.
+eauto.
+clear_inversion HDAda.
+destruct (H6 m).
+destruct H7.
+eauto.
+
+destruct Hnv as [nv].
+destruct Hna as [na].
+exists (TmApp nv na).
+
+split.
+eauto.
+
+
 admit.
 
 (* Dempty *)
 
 Qed.
 
+(***********************)
+
+
 Lemma RelSid: forall Gamma denv,
   Gamma |-- -> EvalCxt Gamma denv -> Gamma ||- [Sid] : Gamma #aeq# denv
 .