Skip to content
Snippets Groups Projects
Commit d1dd2c55 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Do not use agree_car in wsat anymore.

Also, remove some unused lemmas about agree.
parent 5529638a
No related branches found
No related tags found
No related merge requests found
...@@ -3,7 +3,7 @@ From iris.algebra Require Import upred. ...@@ -3,7 +3,7 @@ From iris.algebra Require Import upred.
Local Hint Extern 10 (_ _) => omega. Local Hint Extern 10 (_ _) => omega.
Record agree (A : Type) : Type := Agree { Record agree (A : Type) : Type := Agree {
agree_car :> nat A; agree_car : nat A;
agree_is_valid : nat Prop; agree_is_valid : nat Prop;
agree_valid_S n : agree_is_valid (S n) agree_is_valid n agree_valid_S n : agree_is_valid (S n) agree_is_valid n
}. }.
...@@ -15,7 +15,7 @@ Section agree. ...@@ -15,7 +15,7 @@ Section agree.
Context {A : cofeT}. Context {A : cofeT}.
Instance agree_validN : ValidN (agree A) := λ n x, Instance agree_validN : ValidN (agree A) := λ n x,
agree_is_valid x n n', n' n x n {n'} x n'. agree_is_valid x n n', n' n agree_car x n {n'} agree_car x n'.
Instance agree_valid : Valid (agree A) := λ x, n, {n} x. Instance agree_valid : Valid (agree A) := λ x, n, {n} x.
Lemma agree_valid_le n n' (x : agree A) : Lemma agree_valid_le n n' (x : agree A) :
...@@ -24,12 +24,13 @@ Proof. induction 2; eauto using agree_valid_S. Qed. ...@@ -24,12 +24,13 @@ Proof. induction 2; eauto using agree_valid_S. Qed.
Instance agree_equiv : Equiv (agree A) := λ x y, Instance agree_equiv : Equiv (agree A) := λ x y,
( n, agree_is_valid x n agree_is_valid y n) ( n, agree_is_valid x n agree_is_valid y n)
( n, agree_is_valid x n x n {n} y n). ( n, agree_is_valid x n agree_car x n {n} agree_car y n).
Instance agree_dist : Dist (agree A) := λ n x y, Instance agree_dist : Dist (agree A) := λ n x y,
( n', n' n agree_is_valid x n' agree_is_valid y n') ( n', n' n agree_is_valid x n' agree_is_valid y n')
( n', n' n agree_is_valid x n' x n' {n'} y n'). ( n', n' n agree_is_valid x n' agree_car x n' {n'} agree_car y n').
Program Instance agree_compl : Compl (agree A) := λ c, Program Instance agree_compl : Compl (agree A) := λ c,
{| agree_car n := c n n; agree_is_valid n := agree_is_valid (c n) n |}. {| agree_car n := agree_car (c n) n;
agree_is_valid n := agree_is_valid (c n) n |}.
Next Obligation. Next Obligation.
intros c n ?. apply (chain_cauchy c n (S n)), agree_valid_S; auto. intros c n ?. apply (chain_cauchy c n (S n)), agree_valid_S; auto.
Qed. Qed.
...@@ -44,20 +45,15 @@ Proof. ...@@ -44,20 +45,15 @@ Proof.
+ by intros x y Hxy; split; intros; symmetry; apply Hxy; auto; apply Hxy. + by intros x y Hxy; split; intros; symmetry; apply Hxy; auto; apply Hxy.
+ intros x y z Hxy Hyz; split; intros n'; intros. + intros x y z Hxy Hyz; split; intros n'; intros.
* trans (agree_is_valid y n'). by apply Hxy. by apply Hyz. * trans (agree_is_valid y n'). by apply Hxy. by apply Hyz.
* trans (y n'). by apply Hxy. by apply Hyz, Hxy. * trans (agree_car y n'). by apply Hxy. by apply Hyz, Hxy.
- intros n x y Hxy; split; intros; apply Hxy; auto. - intros n x y Hxy; split; intros; apply Hxy; auto.
- intros n c; apply and_wlog_r; intros; - intros n c; apply and_wlog_r; intros;
symmetry; apply (chain_cauchy c); naive_solver. symmetry; apply (chain_cauchy c); naive_solver.
Qed. Qed.
Canonical Structure agreeC := CofeT (agree A) agree_cofe_mixin. Canonical Structure agreeC := CofeT (agree A) agree_cofe_mixin.
Lemma agree_car_ne n (x y : agree A) : {n} x x {n} y x n {n} y n.
Proof. by intros [??] Hxy; apply Hxy. Qed.
Lemma agree_cauchy n (x : agree A) i : {n} x i n x n {i} x i.
Proof. by intros [? Hx]; apply Hx. Qed.
Program Instance agree_op : Op (agree A) := λ x y, Program Instance agree_op : Op (agree A) := λ x y,
{| agree_car := x; {| agree_car := agree_car x;
agree_is_valid n := agree_is_valid x n agree_is_valid y n x {n} y |}. agree_is_valid n := agree_is_valid x n agree_is_valid y n x {n} y |}.
Next Obligation. naive_solver eauto using agree_valid_S, dist_S. Qed. Next Obligation. naive_solver eauto using agree_valid_S, dist_S. Qed.
Instance agree_pcore : PCore (agree A) := Some. Instance agree_pcore : PCore (agree A) := Some.
...@@ -127,13 +123,19 @@ Proof. by constructor. Qed. ...@@ -127,13 +123,19 @@ Proof. by constructor. Qed.
Program Definition to_agree (x : A) : agree A := Program Definition to_agree (x : A) : agree A :=
{| agree_car n := x; agree_is_valid n := True |}. {| agree_car n := x; agree_is_valid n := True |}.
Solve Obligations with done. Solve Obligations with done.
Global Instance to_agree_ne n : Proper (dist n ==> dist n) to_agree. Global Instance to_agree_ne n : Proper (dist n ==> dist n) to_agree.
Proof. intros x1 x2 Hx; split; naive_solver eauto using @dist_le. Qed. Proof. intros x1 x2 Hx; split; naive_solver eauto using @dist_le. Qed.
Global Instance to_agree_proper : Proper (() ==> ()) to_agree := ne_proper _. Global Instance to_agree_proper : Proper (() ==> ()) to_agree := ne_proper _.
Global Instance to_agree_inj n : Inj (dist n) (dist n) (to_agree). Global Instance to_agree_inj n : Inj (dist n) (dist n) (to_agree).
Proof. by intros x y [_ Hxy]; apply Hxy. Qed. Proof. by intros x y [_ Hxy]; apply Hxy. Qed.
Lemma to_agree_car n (x : agree A) : {n} x to_agree (x n) {n} x.
Proof. intros [??]; split; naive_solver eauto using agree_valid_le. Qed. Lemma to_agree_uninj n (x : agree A) : {n} x y : A, to_agree y {n} x.
Proof.
intros [??]. exists (agree_car x n).
split; naive_solver eauto using agree_valid_le.
Qed.
(** Internalized properties *) (** Internalized properties *)
Lemma agree_equivI {M} a b : to_agree a to_agree b ⊣⊢ (a b : uPred M). Lemma agree_equivI {M} a b : to_agree a to_agree b ⊣⊢ (a b : uPred M).
...@@ -148,7 +150,7 @@ Arguments agreeC : clear implicits. ...@@ -148,7 +150,7 @@ Arguments agreeC : clear implicits.
Arguments agreeR : clear implicits. Arguments agreeR : clear implicits.
Program Definition agree_map {A B} (f : A B) (x : agree A) : agree B := Program Definition agree_map {A B} (f : A B) (x : agree A) : agree B :=
{| agree_car n := f (x n); agree_is_valid := agree_is_valid x; {| agree_car n := f (agree_car x n); agree_is_valid := agree_is_valid x;
agree_valid_S := agree_valid_S _ x |}. agree_valid_S := agree_valid_S _ x |}.
Lemma agree_map_id {A} (x : agree A) : agree_map id x = x. Lemma agree_map_id {A} (x : agree A) : agree_map id x = x.
Proof. by destruct x. Qed. Proof. by destruct x. Qed.
......
...@@ -51,17 +51,17 @@ Lemma wsat_le n n' E σ r : wsat n E σ r → n' ≤ n → wsat n' E σ r. ...@@ -51,17 +51,17 @@ Lemma wsat_le n n' E σ r : wsat n E σ r → n' ≤ n → wsat n' E σ r.
Proof. Proof.
destruct n as [|n], n' as [|n']; simpl; try by (auto with lia). destruct n as [|n], n' as [|n']; simpl; try by (auto with lia).
intros [rs [Hval HE Hwld]] ?; exists rs; constructor; auto. intros [rs [Hval HE Hwld]] ?; exists rs; constructor; auto.
intros i P ? HiP; destruct (wld (r big_opM rs) !! i) as [P'|] eqn:HP'; intros i P ? (P'&HiP&HP')%dist_Some_inv_r'.
[apply (inj Some) in HiP|inversion_clear HiP]. destruct (to_agree_uninj (S n) P') as [laterP' HlaterP'].
{ apply (lookup_validN_Some _ (wld (r big_opM rs)) i); rewrite ?HiP; auto. }
assert (P' {S n} to_agree $ Next $ iProp_unfold $ assert (P' {S n} to_agree $ Next $ iProp_unfold $
iProp_fold $ later_car $ P' (S n)) as HPiso. iProp_fold $ later_car $ laterP') as HPiso.
{ rewrite iProp_unfold_fold later_eta to_agree_car //. { by rewrite iProp_unfold_fold later_eta HlaterP'. }
apply (lookup_validN_Some _ (wld (r big_opM rs)) i); rewrite ?HP'; auto. } assert (P {n'} iProp_fold (later_car laterP')) as HPP'.
assert (P {n'} iProp_fold (later_car (P' (S n)))) as HPP'.
{ apply (inj iProp_unfold), (inj Next), (inj to_agree). { apply (inj iProp_unfold), (inj Next), (inj to_agree).
by rewrite -HiP -(dist_le _ _ _ _ HPiso). } by rewrite HP' -(dist_le _ _ _ _ HPiso). }
destruct (Hwld i (iProp_fold (later_car (P' (S n))))) as (r'&?&?); auto. destruct (Hwld i (iProp_fold (later_car laterP'))) as (r'&?&?); auto.
{ by rewrite HP' -HPiso. } { by rewrite HiP -HPiso. }
assert ({S n} r') by (apply (big_opM_lookup_valid _ rs i); auto). assert ({S n} r') by (apply (big_opM_lookup_valid _ rs i); auto).
exists r'; split; [done|]. apply HPP', uPred_closed with n; auto. exists r'; split; [done|]. apply HPP', uPred_closed with n; auto.
Qed. Qed.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment