Commit 38c5bcec authored by Ralf Jung's avatar Ralf Jung

Merge branch 'ralf/string-ident' into 'master'

use string-ident plugin a bit

See merge request iris/examples!32
parents 0a8f1911 61034040
......@@ -11,6 +11,7 @@ synopsis: "A collection of case studies for Iris"
depends: [
"coq-iris" { (= "dev.2020-04-07.7.64bed0ca") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
"coq-iris-string-ident"
]
build: [make "-j%{jobs}%"]
......
......@@ -4,6 +4,7 @@ From iris.program_logic Require Export atomic.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
From iris_examples.logatom.rdcss Require Import spec.
From iris_string_ident Require ltac2_string_ident.
Import uPred bi List Decidable.
Set Default Proof Using "Type".
......@@ -439,8 +440,8 @@ Section rdcss.
wp_apply (wp_resolve with "Hp"); first done; wp_cmpxchg_suc.
iIntros (vs'' ->). simpl.
iDestruct "State" as "[Pending | Accepted]".
+ iDestruct "Pending" as "[_ [Hvs _]]". iDestruct "Hvs" as %Hvs. by inversion Hvs.
+ iDestruct "Accepted" as "[_ [_ Hvs]]". iDestruct "Hvs" as %Hvs. by inversion Hvs.
+ iDestruct "Pending" as "[_ [%Hvs _]]". by inversion Hvs.
+ iDestruct "Accepted" as "[_ [_ %Hvs]]". by inversion Hvs.
}
(* So, we know our protocol is [Done]. *)
(* It must be that (state_to_val s) ≠ (InjRV l_descr) because we are in the failing thread. *)
......
......@@ -5,6 +5,7 @@ From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export atomic.
From iris.heap_lang Require Import proofmode notation par.
From iris_examples.logatom.snapshot Require Import spec.
From iris_string_ident Require ltac2_string_ident.
Set Default Proof Using "Type".
(** Specifying snapshots with histories
......@@ -341,8 +342,7 @@ Section atomic_snapshot.
(* duplicate timestamp T_y *)
iMod (timestamp_dupl with "Ht_y") as "[Ht_y● Ht_y◯]".
(* show that T_x <= T_y *)
iDestruct (timestamp_sub with "[Ht_y● Ht_x1◯]") as "#Hs"; first by iFrame.
iDestruct "Hs" as %Hs.
iDestruct (timestamp_sub with "[Ht_y● Ht_x1◯]") as "%Hs"; first by iFrame.
iModIntro. iModIntro.
(* closing invariant *)
iSplitR "HΦ Hl1' Ht_x1◯ Ht_y◯ Hpr".
......@@ -356,8 +356,7 @@ Section atomic_snapshot.
iDestruct "Hl1'_x2" as "[Hl1'_x2 Hl1'_x2_frag]".
wp_load.
(* show that T_y <= T_x2 *)
iDestruct (timestamp_sub with "[Ht_x2 Ht_y◯]") as "#Hs'"; first by iFrame.
iDestruct "Hs'" as %Hs'.
iDestruct (timestamp_sub with "[Ht_x2 Ht_y◯]") as "%Hs'"; first by iFrame.
iModIntro. iSplitR "HΦ Hl1'_x2_frag Hpr". {
iNext. unfold snapshot_inv. eauto 8 with iFrame.
}
......
......@@ -2,6 +2,7 @@ From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris_string_ident Require ltac2_string_ident.
Set Default Proof Using "Type".
Fixpoint val_of_list (vs : list (val * val)) : val :=
......@@ -44,8 +45,8 @@ Section one_shot.
WP e @ s; E {{ r, v = w - Φ r }} -
WP Resolve e (Val $ LitV $ LitProphecy p) (Val w) @ s; E {{ Φ }}.
Proof.
iIntros (A He) "Hp Wpe". iDestruct "Hp" as (vs) "[Hp HEq]".
iDestruct "HEq" as %HEq. wp_apply (wp_resolve with "Hp"); try done.
iIntros (A He) "Hp Wpe". iDestruct "Hp" as (vs) "[Hp %HEq]".
wp_apply (wp_resolve with "Hp"); try done.
iApply wp_mono; last done. iIntros (v0) "H". iIntros (pvs ->) "Hp".
by iApply "H".
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