hax.v 4.66 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11
(* the contents of this file sould belong elsewhere *)
From iris.proofmode Require Import tactics.
From iris_logrel.F_mu_ref_conc Require Import lang subst tactics rules rules_binary logrel_binary.

Definition lamsubst (e : expr) (v : val) : expr :=
  match e with
  | Rec (BNamed f) x e' => lang.subst f e (subst' x (of_val v) e')
  | Rec BAnon x e' => subst' x (of_val v) e'
  | _ => e
  end.

12 13
Notation "e $/ v" := (lamsubst e%E v%V) (at level 80) : expr_scope.

14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30
Ltac inv_head_step :=
  repeat match goal with
  | _ => progress simplify_map_eq/= (* simplify memory stuff *)
  | H : to_val _ = Some _ |- _ => apply of_to_val in H
  | H : _ = of_val ?v |- _ =>
     is_var v; destruct v; first[discriminate H|injection H as H]
  | H : head_step ?e _ _ _ _ |- _ =>
     try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
     and can thus better be avoided. *)
     inversion H; subst; clear H
  end.

Section hax.
  Context `{heapIG Σ, cfgSG Σ}.
  Notation D := (prodC valC valC -n> iProp Σ).
  Implicit Types Δ : listC D.

31
  Lemma bin_log_related_arrow Γ E (f x f' x' : binder) (e e' : expr) (τ τ' : type)
32 33 34 35
    (Hclosed  : Closed  (rec: f x := e)%E )
    (Hclosed' : Closed  (rec: f' x' := e')%E) :

    ( Δ vv,  τ  Δ vv -
36 37
      Γ  App (Rec f x e) (of_val (vv.1)) log App (Rec f' x' e') (of_val (vv.2)) : τ') -
    {E,E;Γ}  (Rec f x e) log (Rec f' x' e') : TArrow τ τ'.
38 39
  Proof.
    iIntros "#H".
40
    rewrite bin_log_related_eq.
41
    iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj".
42 43 44 45
    cbn-[subst_p].
    iModIntro.
    rewrite {2}/env_subst Closed_subst_p_id.
    iApply wp_value.
46
    { simpl. erewrite decide_left. done. }
47 48
    rewrite /env_subst Closed_subst_p_id.
    iExists (RecV f' x' e').
49 50 51
    iFrame "Hj". iAlways. iIntros (vv) "Hvv".
    iSpecialize ("H" $! Δ vv with "Hvv").
    iSpecialize ("H" $! Δ with "Hs []").
52 53 54 55 56 57 58 59 60
    { iAlways. iApply "HΓ". }    
    Unshelve. all: trivial.
    assert (Closed  ((rec: f x := e) (vv.1))%E).
    { revert Hclosed. unfold Closed. simpl.
      intros. split_and?; auto. apply of_val_closed. }
    assert (Closed  ((rec: f' x' := e') (vv.2))%E).
    { revert Hclosed'. unfold Closed. simpl.
      intros. split_and?; auto. apply of_val_closed. }
    rewrite /env_subst. rewrite !Closed_subst_p_id. done.
61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120
  Qed.

  Lemma weird_bind e Q :
    WP App e #() {{ Q }}  WP e {{ v, WP (App v #()) {{ Q }} }}.
  Proof.
    (* ugh, turns out this is just the inverse bind:
       Check (wp_bind_inv (fun v => App v #())). *)
    iLöb as "IH" forall (e).
    iIntros "wp".
    rewrite (wp_unfold _ e) /wp_pre /=.
    remember (to_val e) as eval. destruct eval.
    - symmetry in Heqeval. rewrite -(of_to_val _ _ Heqeval). eauto.
    - iIntros (σ1) "Hσ1".
      rewrite wp_unfold /wp_pre /=.
      iMod ("wp" $! σ1 with "Hσ1") as "[r wp]". iModIntro.
      iDestruct "r" as %er.
      assert (reducible e σ1).
      { symmetry in Heqeval.
        unfold reducible in er.
        destruct er as (e2 & σ2 & efs & Hpst).
        inversion Hpst; simpl in *; subst; clear Hpst.
        admit. }
      iSplitR; eauto.
      iNext.
      iIntros (e2 σ2 efs) "Hpst". iDestruct "Hpst" as %Hpst.
      iSpecialize ("wp" $! (App e2 #()) σ2 efs).
      iAssert (prim_step (e #()%E) σ1 (e2 #()%E) σ2 efs)%I as "Hprim'".
      { iPureIntro.
        inversion Hpst; simpl in *; subst; clear Hpst.
        eapply (Ectx_step _ σ1 _ σ2 efs (K++[AppLCtx (#())%E])); simpl; eauto.
          by rewrite fill_app.
          by rewrite fill_app. }
      iMod ("wp" with "Hprim'") as "[$ [wp $]]". iModIntro.
      by iApply "IH".
  Admitted.

  (* Lemma wp_step_back Γ (e t : expr) (x : string) (v ev : val) τ : *)
  (*   Closed  (Lam x e)  *)
  (*   to_val (lang.subst x (of_val v) e) = Some ev  *)
  (*   Γ  (App (Lam x e) v) log t : τ *)
  (*    Γ  (lang.subst x (of_val v) e) log t : τ. *)
  (* Proof. *)
  (*   iIntros (??) "Hr". *)
  (*   Transparent bin_log_related. *)
  (*   iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj". *)
  (*   cbn-[subst_p].  *)
  (*   (* assert (Closed  (lang.subst x v e)). *) *)
  (*   (* { eapply is_closed_subst_preserve; eauto. solve_closed. } *) *)
  (*   rewrite /env_subst !Closed_subst_p_id. *)
  (*   iSpecialize ("Hr" with "Hs []"). *)
  (*   { iAlways. by iFrame. } *)
  (*   rewrite /env_subst. erewrite (Closed_subst_p_id (fst <$> vvs)); last first. *)
  (*   { rewrite /Closed. simpl. *)
  (*     rewrite /Closed /= in H1. split_and; eauto; try solve_closed. } *)
  (*   iMod ("Hr" with "Hj") as "Hr". *)
  (*   iModIntro. simpl. *)
  (*   rewrite {1}wp_unfold /wp_pre /=. *)
  (*   iApply wp_value; eauto. *)
  (*   iApply (wp_bind_inv in "Hr". *)
End hax.