Commit b01ac5a8 authored by Ralf Jung's avatar Ralf Jung

the rewrite problem now has an issue number

parent a5ff3f99
......@@ -326,6 +326,7 @@ Section lemmas.
iModIntro. destruct (γ' x'); iApply "HPas"; done.
- iIntros (y) "Hβ". iMod "Hclose''" as "_".
iMod ("Hclose'" with "Hβ") as "Hβ'".
(* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
rewrite ->!tele_app_bind. iDestruct "Hβ'" as "[Hβ' HΦ]".
iMod ("Hclose" with "Hβ'") as "Hγ'".
iModIntro. destruct (γ' x'); iApply "HΦ"; done.
......@@ -361,6 +362,7 @@ Section lemmas.
iMod ("Hclose" with "Hα"). iApply "Hupd". auto.
- iIntros (y') "Hβ'". iDestruct "Hclose'" as "[_ Hclose']".
iMod ("Hclose'" with "Hβ'") as "Hres".
(* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
rewrite ->!tele_app_bind. iDestruct "Hres" as "[[Hα HΦ']|Hcont]".
+ (* Abort the step we are eliminating *)
iDestruct "Hclose" as "[Hclose _]".
......@@ -399,6 +401,7 @@ Section lemmas.
iIntros (?) "Hupd Hstep". iApply (aacc_aupd with "Hupd"); first done.
iIntros (x) "Hα". iApply atomic_acc_wand; last first.
{ iApply "Hstep". done. }
(* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
iSplit; first by eauto. iIntros (??) "?". rewrite ->!tele_app_bind. by iRight.
Qed.
......@@ -414,6 +417,7 @@ Section lemmas.
iIntros (?) "Hupd Hstep". iApply (aacc_aupd with "Hupd"); first done.
iIntros (x) "Hα". iApply atomic_acc_wand; last first.
{ iApply "Hstep". done. }
(* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
iSplit; first by eauto. iIntros (??) "?". rewrite ->!tele_app_bind. by iLeft.
Qed.
......
......@@ -105,7 +105,7 @@ Section lemmas.
rewrite ->tforall_forall in HL.
iIntros "Hwp" (Φ x) "Hα HΦ". iApply ("Hwp" with "[HΦ]"); first iAccu.
iAuIntro. iAaccIntro with "Hα"; first by eauto. iIntros (y) "Hβ !>".
(* FIXME: Using ssreflect rewrite does not work? *)
(* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
rewrite ->!tele_app_bind. iIntros "HΦ". iApply "HΦ". done.
Qed.
......@@ -120,6 +120,7 @@ Section lemmas.
iMod ("HΦ") as "[#Hα [Hclose _]]". iMod ("Hclose" with "Hα") as "HΦ".
iApply wp_fupd. iApply ("Hwp" with "Hα"). iIntros "!>" (y) "Hβ".
iMod ("HΦ") as "[_ [_ Hclose]]". iMod ("Hclose" with "Hβ") as "HΦ".
(* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
rewrite ->!tele_app_bind. iApply "HΦ". done.
Qed.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment