diff --git a/algebra/agree.v b/algebra/agree.v index a62b288f26eaad80b7dc805c42eba32bdddfcb69..a85d59e8f795968981919624de76fdc98b47ae0c 100644 --- a/algebra/agree.v +++ b/algebra/agree.v @@ -3,7 +3,7 @@ From iris.algebra Require Import upred. Local Hint Extern 10 (_ ≤ _) => omega. Record agree (A : Type) : Type := Agree { - agree_car :> nat → A; + agree_car : nat → A; agree_is_valid : nat → Prop; agree_valid_S n : agree_is_valid (S n) → agree_is_valid n }. @@ -15,7 +15,7 @@ Section agree. Context {A : cofeT}. 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. Lemma agree_valid_le n n' (x : agree A) : @@ -24,12 +24,13 @@ Proof. induction 2; eauto using agree_valid_S. Qed. 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 → 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, (∀ 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, - {| 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. intros c n ?. apply (chain_cauchy c n (S n)), agree_valid_S; auto. Qed. @@ -44,20 +45,15 @@ Proof. + by intros x y Hxy; split; intros; symmetry; apply Hxy; auto; apply Hxy. + intros x y z Hxy Hyz; split; intros n'; intros. * 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 c; apply and_wlog_r; intros; symmetry; apply (chain_cauchy c); naive_solver. Qed. 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, - {| 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 |}. Next Obligation. naive_solver eauto using agree_valid_S, dist_S. Qed. Instance agree_pcore : PCore (agree A) := Some. @@ -127,13 +123,19 @@ Proof. by constructor. Qed. Program Definition to_agree (x : A) : agree A := {| agree_car n := x; agree_is_valid n := True |}. Solve Obligations with done. + 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. Global Instance to_agree_proper : Proper ((≡) ==> (≡)) to_agree := ne_proper _. + Global Instance to_agree_inj n : Inj (dist n) (dist n) (to_agree). 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 *) Lemma agree_equivI {M} a b : to_agree a ≡ to_agree b ⊣⊢ (a ≡ b : uPred M). @@ -148,7 +150,7 @@ Arguments agreeC : clear implicits. Arguments agreeR : clear implicits. 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 |}. Lemma agree_map_id {A} (x : agree A) : agree_map id x = x. Proof. by destruct x. Qed. diff --git a/program_logic/wsat.v b/program_logic/wsat.v index 650238ddd5f910f70db52d1ad6c6e925b097d6a4..0392bd540d540693f8d5f132c8faa2e6afe28f3b 100644 --- a/program_logic/wsat.v +++ b/program_logic/wsat.v @@ -51,17 +51,17 @@ Lemma wsat_le n n' E σ r : wsat n E σ r → n' ≤ n → wsat n' E σ r. Proof. destruct n as [|n], n' as [|n']; simpl; try by (auto with lia). intros [rs [Hval Hσ HE Hwld]] ?; exists rs; constructor; auto. - intros i P ? HiP; destruct (wld (r ⋅ big_opM rs) !! i) as [P'|] eqn:HP'; - [apply (inj Some) in HiP|inversion_clear HiP]. + intros i P ? (P'&HiP&HP')%dist_Some_inv_r'. + 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 \$ - iProp_fold \$ later_car \$ P' (S n)) as HPiso. - { rewrite iProp_unfold_fold later_eta to_agree_car //. - apply (lookup_validN_Some _ (wld (r ⋅ big_opM rs)) i); rewrite ?HP'; auto. } - assert (P ≡{n'}≡ iProp_fold (later_car (P' (S n)))) as HPP'. + iProp_fold \$ later_car \$ laterP') as HPiso. + { by rewrite iProp_unfold_fold later_eta HlaterP'. } + assert (P ≡{n'}≡ iProp_fold (later_car laterP')) as HPP'. { apply (inj iProp_unfold), (inj Next), (inj to_agree). - by rewrite -HiP -(dist_le _ _ _ _ HPiso). } - destruct (Hwld i (iProp_fold (later_car (P' (S n))))) as (r'&?&?); auto. - { by rewrite HP' -HPiso. } + by rewrite HP' -(dist_le _ _ _ _ HPiso). } + destruct (Hwld i (iProp_fold (later_car laterP'))) as (r'&?&?); auto. + { by rewrite HiP -HPiso. } assert (✓{S n} r') by (apply (big_opM_lookup_valid _ rs i); auto). exists r'; split; [done|]. apply HPP', uPred_closed with n; auto. Qed.