From stdpp Require Export ssreflect.
From iris.algebra Require Import list gmap.
From iris.bi Require Import bi.
From iris.prelude Require Export options.
(** NOTATIONS *)
Notation "⌜⌜ φ ⌝⌝" := (<affine> ⌜ φ ⌝)%I : bi_scope.
Notation "x ≡≡ y" := (<affine> (x ≡ y))%I (at level 70) : bi_scope.
Reserved Notation "c ↣ p" (at level 20, format "c ↣ p").
(** UPSTREAM to std++ *)
Class TCSimpl {A} (x x' : A) := tc_simpl : x = x'.
Global Hint Extern 0 (TCSimpl _ _) =>
simpl; notypeclasses refine (eq_refl _) : typeclass_instances.
Lemma wf_lt_projected {B} (f : B → nat) : wf (λ x y, f x < f y).
Proof. by apply (wf_projected (<) f), lt_wf. Qed.
Definition prod_swap {A B} : A * B → B * A := λ '(x,y), (y,x).
Lemma elem_of_set_map_prod_swap `{Countable A} (e : gset (A * A)) (x y : A) :
(x, y) ∈@{gset _} set_map prod_swap e ↔ (y, x) ∈ e.
Proof.
rewrite elem_of_map. split.
- intros [[??]]; naive_solver.
- intros. by exists (y,x).
Qed.
Lemma not_rtsc {A} {R : relation A} x y :
(∀ y', ¬R x y' ∧ ¬R y' x) →
rtsc R x y → x = y.
Proof. induction 2 as [|??? []]; naive_solver. Qed.
Lemma rtc_iff {A} (R1 R2 : relation A) x y :
(∀ x y, R1 x y ↔ R2 x y) →
rtc R1 x y ↔ rtc R2 x y.
Proof. split; apply rtc_subrel; naive_solver. Qed.
Lemma sc_or {A} (R : relation A) x y :
sc R x y ↔ R x y ∨ R y x.
Proof. done. Qed.
Lemma lookup_take_spec {A} (xs : list A) k n :
take n xs !! k = if decide (k < n) then xs !! k else None.
Proof. case_decide; eauto using lookup_take, lookup_take_ge with lia. Qed.
Lemma lookup_list_singleton_spec {A} k (x : A) :
[x] !! k = if decide (k = 0) then Some x else None.
Proof. by destruct k. Qed.
Lemma lookup_app_add {A} (l1 l2 : list A) (i : nat) :
(l1 ++ l2) !! (length l1 + i) = l2 !! i.
Proof. by induction l1. Qed.
Lemma lookup_delete_lr {A} (xs : list A) (i j : nat) :
delete i xs !! j = if decide (j < i) then xs !! j else xs !! (S j).
Proof. case_decide; eauto using lookup_delete_lt, lookup_delete_ge with lia. Qed.
Lemma split_first {A} (xs : list A) a :
xs !! 0 = Some a → xs = [a] ++ drop 1 xs.
Proof. destruct xs as [|? []]; naive_solver. Qed.
Lemma split_last {A} (xs : list A) a :
last xs = Some a → xs = take (length xs - 1) xs ++ [a].
Proof.
intros Hlst. rewrite -{1}(take_drop (length xs - 1) xs). f_equal.
apply last_Some in Hlst as [xs' ->].
rewrite app_length /=. replace (length xs' + 1 - 1) with (length xs') by lia.
by rewrite drop_app.
Qed.
Lemma split_both {A} (xs : list A) a :
1 < length xs → xs !! 0 = Some a → last xs = Some a →
xs = a :: drop 1 (take (length xs - 1) xs) ++ [a].
Proof.
intros Hlen Hfst%split_first Hlst%split_last; simplify_eq/=.
rewrite -drop_app_le ?take_length; last lia.
by rewrite -Hlst.
Qed.
Lemma last_take {A} i (xs : list A) :
i < length xs → last (take (S i) xs) = xs !! i.
Proof.
intros. rewrite last_lookup lookup_take ?take_length; last lia.
f_equal; lia.
Qed.
Lemma last_take_Some {A} i (xs : list A) x :
xs !! i = Some x → last (take (S i) xs) = Some x.
Proof. intros. rewrite last_take; eauto using lookup_lt_Some. Qed.
Lemma last_drop {A} (xs : list A) i :
i < length xs → last (drop i xs) = last xs.
Proof. intros. rewrite !last_lookup lookup_drop drop_length. f_equal; lia. Qed.
Lemma lookup_update {A} i j (xs : list A) x :
<[i:=x]> xs !! j = if decide (i = j ∧ j < length xs) then Some x else xs !! j.
Proof.
revert i j. induction xs as [|x' xs IH]; intros [|i] [|j];
simpl; [repeat case_decide; auto with lia..|].
rewrite IH. repeat case_decide; auto with lia.
Qed.
Lemma lookup_insert_spec `{FinMap K M} {A} (m : M A) i j x :
<[i:=x]> m !! j = if (decide (i = j)) then Some x else m !! j.
Proof. case_decide; subst; eauto using lookup_insert, lookup_insert_ne. Qed.
Lemma lookup_delete_spec `{FinMap K M} {A} (m : M A) i j :
delete i m !! j = if (decide (i = j)) then None else m !! j.
Proof. case_decide; [apply lookup_delete_None|apply lookup_delete_ne]; auto. Qed.
(** UPSTREAM to Iris *)
Section quotient.
Context `{Equiv A} (R : A → A → siProp).
Context (Requiv : ∀ x y, x ≡ y ↔ ⊢ R x y).
Context (Rrefl : ∀ x, ⊢ R x x).
Context (Rsymm : ∀ x y, R x y ⊢ R y x).
Context (Rtrans : ∀ x y z, R x y ∧ R y z ⊢ R x z).
Local Instance quotient_dist : Dist A := λ n x y,
siProp_holds (R x y) n.
Lemma quotient_ofe_mixin : OfeMixin A.
Proof using Type*.
split; rewrite /dist /quotient_dist.
- intros x y. rewrite Requiv. split.
+ intros HR n. apply HR. by siProp.unseal.
+ intros HR. split=> n. auto.
- split.
+ intros x. apply Rrefl. by siProp.unseal.
+ intros x y Hxy. by apply Rsymm.
+ intros x y z ??. eapply Rtrans. siProp.unseal. by split.
- intros n m x y ??. eapply siProp_closed; [done|]. lia.
Qed.
Lemma quotient_equiv (x1 x2 : Ofe A quotient_ofe_mixin) : x1 ≡ x2 ⊣⊢ R x1 x2.
Proof. rewrite /internal_eq. by siProp.unseal. Qed.
End quotient.
Lemma later_map_Next {A B : ofe} (f : A → B) x : later_map f (Next x) = Next (f x).
Proof. done. Qed.
Global Instance gmap_union_ne `{Countable K} {A : ofe} :
NonExpansive2 (union (A:=gmap K A)).
Proof. intros n. apply merge_ne. destruct 1,1; simpl; by f_equiv. Qed.
Global Instance gmap_disjoint_ne `{Countable K} {A : ofe} n :
Proper (dist n ==> dist n ==> iff) (map_disjoint (M:=gmap K) (A:=A)).
Proof.
intros m1 m1' Hm1 m2 m2' Hm2; split;
intros Hm i; specialize (Hm i); by destruct (Hm1 i), (Hm2 i).
Qed.
Lemma gmap_union_dist_eq `{Countable K} {A : ofe} (m m1 m2 : gmap K A) n :
m ≡{n}≡ m1 ∪ m2 ↔ ∃ m1' m2', m = m1' ∪ m2' ∧ m1' ≡{n}≡ m1 ∧ m2' ≡{n}≡ m2.
Proof.
split; last first.
{ by intros (m1'&m2'&->&<-&<-). }
intros Hm.
exists (filter (λ '(l,_), is_Some (m1 !! l)) m),
(m2 ∩ m1 ∪ filter (λ '(l,_), is_Some (m2 !! l)) m).
split_and!; [apply map_eq|..]; intros k; move: (Hm k);
rewrite ?lookup_union ?lookup_intersection !map_filter_lookup;
case _ : (m !! k)=> [x|] /=; case _ : (m1 !! k)=> [x1|] /=;
case _ : (m2 !! k)=> [x2|] /=; by inversion 1.
Qed.
Lemma gmap_union_dist_eqI `{!Sbi PROP} `{Countable K}
{A : ofe} (m m1 m2 : gmap K A) :
m ≡ m1 ∪ m2 ⊣⊢@{PROP} ∃ m1' m2', ⌜ m = m1' ∪ m2' ⌝ ∧ m1' ≡ m1 ∧ m2' ≡ m2.
Proof. unfold_sbi=> n. apply gmap_union_dist_eq. Qed.
Lemma gmap_op_union `{Countable K} {A : cmra} (m1 m2 : gmap K A) :
m1 ##ₘ m2 → m1 ⋅ m2 = m1 ∪ m2.
Proof.
intros Hm. apply map_eq=> k. specialize (Hm k).
rewrite lookup_op lookup_union. by destruct (m1 !! k), (m2 !! k).
Qed.
Lemma gmap_op_valid0_disjoint `{Countable K} {A : cmra} (m1 m2 : gmap K A) :
✓{0} (m1 ⋅ m2) → (∀ k x, m1 !! k = Some x → Exclusive x) → m1 ##ₘ m2.
Proof.
unfold Exclusive. intros Hvalid Hexcl k.
specialize (Hvalid k). rewrite lookup_op in Hvalid. specialize (Hexcl k).
destruct (m1 !! k), (m2 !! k); [|done..].
rewrite -Some_op Some_validN in Hvalid. naive_solver.
Qed.
Global Instance cons_dist_inj {A : ofe} n :
Inj2 (dist n) (dist n) (dist n) (@cons A).
Proof. by inversion_clear 1. Qed.
Lemma dist_Forall2 {A : ofe} n (l k : list A) : l ≡{n}≡ k ↔ Forall2 (dist n) l k.
Proof. done. Qed.
Lemma nil_dist_eq {A : ofe} n (l : list A) : l ≡{n}≡ [] ↔ l = [].
Proof. split; by inversion 1. Qed.
Lemma app_dist_eq {A : ofe} n (l k1 k2 : list A) :
l ≡{n}≡ k1 ++ k2 ↔ ∃ k1' k2', l = k1' ++ k2' ∧ k1' ≡{n}≡ k1 ∧ k2' ≡{n}≡ k2.
Proof. rewrite dist_Forall2 Forall2_app_inv_r. naive_solver. Qed.
Lemma list_singleton_dist_eq {A : ofe} n (l : list A) x :
l ≡{n}≡ [x] ↔ ∃ x', l = [x'] ∧ x' ≡{n}≡ x.
Proof.
split; [|by intros (?&->&->)].
intros (?&?&?&->%Forall2_nil_inv_r&->)%dist_Forall2%Forall2_cons_inv_r. eauto.
Qed.
Lemma dist_Permutation {A : ofe} n (l1 l2 l3 : list A) :
l1 ≡{n}≡ l2 → l2 ≡ₚ l3 → ∃ l2', l1 ≡ₚ l2' ∧ l2' ≡{n}≡ l3.
Proof.
intros Hequiv Hperm. revert l1 Hequiv.
induction Hperm as [|x l2 l3 _ IH|x y l2|l2 l3 l4 _ IH1 _ IH2]; intros l1.
- intros ?. by exists l1.
- intros (x'&l2'&?&(l2''&?&?)%IH&->)%list_dist_cons_inv_r.
exists (x' :: l2''). by repeat constructor.
- intros (y'&?&?&(x'&l2'&?&?&->)%list_dist_cons_inv_r&->)%list_dist_cons_inv_r.
exists (x' :: y' :: l2'). by repeat constructor.
- intros (l2'&?&(l3'&?&?)%IH2)%IH1. exists l3'. split; [by etrans|done].
Qed.