Commit f7b78e01 authored by Dan Frumin's avatar Dan Frumin
Browse files

Use ProofMode's iDestruct to eliminate intuitionistic conjunction

parent 1769a63f
...@@ -163,12 +163,12 @@ Section CG_Counter. ...@@ -163,12 +163,12 @@ Section CG_Counter.
unfold FG_increment. unlock. simpl. unfold FG_increment. unlock. simpl.
iLöb as "IH". iLöb as "IH".
rel_rec_l. rel_rec_l.
rel_bind_l (Load (Loc x)).
iPoseProof "H" as "H2". (* lolwhat *) iPoseProof "H" as "H2". (* lolwhat *)
rel_bind_l (Load #x).
iApply (bin_log_related_load_l). iApply (bin_log_related_load_l).
iMod "H" as (n) "[Hx [HR Hrev]]". iModIntro. iMod "H" as (n) "[Hx [HR Hrev]]". iModIntro.
iExists (#nv n). iFrame. iNext. iIntros "Hx". iExists (#nv n). iFrame. iNext. iIntros "Hx".
rewrite ->uPred.and_elim_l. iDestruct "Hrev" as "[Hrev _]".
iApply fupd_logrel. iApply fupd_logrel.
iMod ("Hrev" with "[HR Hx]"). iMod ("Hrev" with "[HR Hx]").
{ iExists _. iFrame. } iModIntro. simpl. { iExists _. iFrame. } iModIntro. simpl.
...@@ -181,15 +181,15 @@ Section CG_Counter. ...@@ -181,15 +181,15 @@ Section CG_Counter.
- iExists (#nv n'). iFrame. - iExists (#nv n'). iFrame.
iSplitR; eauto. { iDestruct 1 as %Hfoo. exfalso. done. } iSplitR; eauto. { iDestruct 1 as %Hfoo. exfalso. done. }
iIntros "_ !> Hx". simpl. iIntros "_ !> Hx". simpl.
rewrite ->uPred.and_elim_r. iDestruct "HQ" as "[_ HQ]".
iSpecialize ("HQ" $! n' with "[Hx HR]"). { iFrame. } iSpecialize ("HQ" $! n' with "[Hx HR]"). { iFrame. }
iApply (bin_log_related_if_true_masked_l _ _ _ K); auto. iApply (bin_log_related_if_true_masked_l _ _ _ K); auto.
- iExists (#nv n'). iFrame. - iExists (#nv n'). iFrame.
iSplitL; eauto; last first. iSplitL; eauto; last first.
{ iDestruct 1 as %Hfoo. exfalso. simplify_eq. } { iDestruct 1 as %Hfoo. exfalso. simplify_eq. }
iIntros "_ !> Hx". simpl. iIntros "_ !> Hx". simpl.
iApply (bin_log_related_if_false_masked_l _ _ _ K); auto. iApply (bin_log_related_if_false_masked_l _ _ _ K); auto.
rewrite ->uPred.and_elim_l. iDestruct "HQ" as "[HQ _]".
iMod ("HQ" with "[Hx HR]"). iMod ("HQ" with "[Hx HR]").
{ iExists _; iFrame. } { iExists _; iFrame. }
iApply "IH". iApply "IH".
...@@ -205,12 +205,12 @@ Section CG_Counter. ...@@ -205,12 +205,12 @@ Section CG_Counter.
Proof. Proof.
iIntros "#H". iIntros "#H".
unfold counter_read. unlock. simpl. unfold counter_read. unlock. simpl.
iApply (bin_log_related_rec_l _ E1 _); auto. iNext. simpl. rel_rec_l.
iApply (bin_log_related_load_l). iApply (bin_log_related_load_l).
iMod "H" as (n) "[Hx [HR Hfin]]". iModIntro. iMod "H" as (n) "[Hx [HR Hfin]]". iModIntro.
iExists _; iFrame "Hx". iNext. iExists _; iFrame "Hx". iNext.
iIntros "Hx". iIntros "Hx".
rewrite ->uPred.and_elim_r. (* TODO: a tactic for this *) iDestruct "Hfin" as "[_ Hfin]".
iApply "Hfin". by iFrame. iApply "Hfin". by iFrame.
Qed. 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