Commit e9af95ac authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix mess by my previous commits ...

due to an accidental git commit --amend after a git push.
parent 6146f3c9
Pipeline #76 passed with stage
...@@ -290,7 +290,7 @@ Proof. ...@@ -290,7 +290,7 @@ Proof.
intros s2; rewrite elem_of_intersection. destruct_conjs. intros s2; rewrite elem_of_intersection. destruct_conjs.
unfold up_set; rewrite elem_of_bind; intros (?&s1&?&?&?). unfold up_set; rewrite elem_of_bind; intros (?&s1&?&?&?).
apply closed_steps with T2 s1; auto with sts. apply closed_steps with T2 s1; auto with sts.
Admitted. Qed.
Canonical Structure RA : cmraT := validityRA (car sts). Canonical Structure RA : cmraT := validityRA (car sts).
End sts_dra. End sts_dra. End sts_dra. End sts_dra.
......
...@@ -42,7 +42,7 @@ Module barrier_proto. ...@@ -42,7 +42,7 @@ Module barrier_proto.
Proof. Proof.
split. split.
- move=>[p I]. rewrite /= /tok !mkSet_elem_of /= =>HI. - move=>[p I]. rewrite /= /tok !mkSet_elem_of /= =>HI.
destruct p; set_solver. destruct p; set_solver eauto.
- (* If we do the destruct of the states early, and then inversion - (* If we do the destruct of the states early, and then inversion
on the proof of a transition, it doesn't work - we do not obtain on the proof of a transition, it doesn't work - we do not obtain
the equalities we need. So we destruct the states late, because this the equalities we need. So we destruct the states late, because this
...@@ -57,9 +57,7 @@ Module barrier_proto. ...@@ -57,9 +57,7 @@ Module barrier_proto.
assert (Change i change_tokens I1) as HI1 assert (Change i change_tokens I1) as HI1
by (rewrite mkSet_not_elem_of; set_solver +Hs1). by (rewrite mkSet_not_elem_of; set_solver +Hs1).
assert (Change i change_tokens I2) as HI2. assert (Change i change_tokens I2) as HI2.
{ destruct p. { destruct p; set_solver +Htok Hdisj HI1. }
- set_solver +Htok Hdisj HI1.
- set_solver +Htok Hdisj HI1 / discriminate. }
done. done.
Qed. Qed.
...@@ -92,7 +90,7 @@ Module barrier_proto. ...@@ -92,7 +90,7 @@ Module barrier_proto.
i I sts.steps (State High I, {[ Change i ]}) (State High (I {[ i ]}), ). i I sts.steps (State High I, {[ Change i ]}) (State High (I {[ i ]}), ).
Proof. Proof.
intros. apply rtc_once. intros. apply rtc_once.
constructor; first constructor; rewrite /= /tok /=; [set_solver..|]. constructor; first constructor; rewrite /= /tok /=; [set_solver eauto..|].
(* TODO this proof is rather annoying. *) (* TODO this proof is rather annoying. *)
apply elem_of_equiv=>t. rewrite !elem_of_union. apply elem_of_equiv=>t. rewrite !elem_of_union.
rewrite !mkSet_elem_of /change_tokens /=. rewrite !mkSet_elem_of /change_tokens /=.
...@@ -100,7 +98,7 @@ Module barrier_proto. ...@@ -100,7 +98,7 @@ Module barrier_proto.
rewrite elem_of_difference elem_of_singleton. rewrite elem_of_difference elem_of_singleton.
destruct (decide (i = j)); set_solver. destruct (decide (i = j)); set_solver.
Qed. Qed.
Lemma split_step p i i1 i2 I : Lemma split_step p i i1 i2 I :
i I i1 I i2 I i1 i2 i I i1 I i2 I i1 i2
sts.steps (State p I, {[ Change i ]}) sts.steps (State p I, {[ Change i ]})
......
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