Library iris.algebra.list

From stdpp Require Export list.
From iris.algebra Require Export ofe.
From iris.algebra Require Import big_op.
From iris.prelude Require Import options.

Section ofe.
Context {A : ofe}.
Implicit Types l : list A.

Local Instance list_dist : Dist (list A) := λ n, Forall2 (dist n).

Lemma list_dist_lookup n l1 l2 : l1 ≡{n}≡ l2 i, l1 !! i ≡{n}≡ l2 !! i.
Proof. setoid_rewrite dist_option_Forall2. apply Forall2_lookup. Qed.

Global Instance cons_ne : NonExpansive2 (@cons A) := _.
Global Instance app_ne : NonExpansive2 (@app A) := _.
Global Instance length_ne n : Proper (dist n ==> (=)) (@length A) := _.
Global Instance tail_ne : NonExpansive (@tail A) := _.
Global Instance take_ne n : NonExpansive (@take A n) := _.
Global Instance drop_ne n : NonExpansive (@drop A n) := _.
Global Instance head_ne : NonExpansive (head (A:=A)).
Proof. destruct 1; by constructor. Qed.
Global Instance list_lookup_ne i : NonExpansive (lookup (M:=list A) i).
Proof. intros ????. by apply dist_option_Forall2, Forall2_lookup. Qed.
Global Instance list_lookup_total_ne `{!Inhabited A} i :
  NonExpansive (lookup_total (M:=list A) i).
Proof. intros ???. rewrite !list_lookup_total_alt. by intros →. Qed.
Global Instance list_alter_ne n f i :
  Proper (dist n ==> dist n) f
  Proper (dist n ==> dist n) (alter (M:=list A) f i) := _.
Global Instance list_insert_ne i : NonExpansive2 (insert (M:=list A) i) := _.
Global Instance list_inserts_ne i : NonExpansive2 (@list_inserts A i) := _.
Global Instance list_delete_ne i : NonExpansive (delete (M:=list A) i) := _.
Global Instance option_list_ne : NonExpansive (@option_list A).
Proof. intros ????; by apply Forall2_option_list, dist_option_Forall2. Qed.
Global Instance list_filter_ne n P `{ x, Decision (P x)} :
  Proper (dist n ==> iff) P
  Proper (dist n ==> dist n) (filter (B:=list A) P) := _.
Global Instance replicate_ne n : NonExpansive (@replicate A n) := _.
Global Instance reverse_ne : NonExpansive (@reverse A) := _.
Global Instance last_ne : NonExpansive (@last A).
Proof. intros ????; by apply dist_option_Forall2, Forall2_last. Qed.
Global Instance resize_ne n : NonExpansive2 (@resize A n) := _.

Lemma list_dist_cons_inv_l n x l k :
  x :: l ≡{n}≡ k y k', x ≡{n}≡ y l ≡{n}≡ k' k = y :: k'.
Proof. apply Forall2_cons_inv_l. Qed.
Lemma list_dist_cons_inv_r n l k y :
  l ≡{n}≡ y :: k x l', x ≡{n}≡ y l' ≡{n}≡ k l = x :: l'.
Proof. apply Forall2_cons_inv_r. Qed.

Definition list_ofe_mixin : OfeMixin (list A).
  - intros l k. rewrite equiv_Forall2 -Forall2_forall.
    split; induction 1; constructor; intros; try apply equiv_dist; auto.
  - apply _.
  - rewrite /dist /list_dist. eauto using Forall2_impl, dist_S.
Canonical Structure listO := Ofe (list A) list_ofe_mixin.

To define compl : chain (list A) list A we make use of the fact that given a given chain c0, c1, c2, ... of lists, the list c0 completely determines the shape (i.e. the length) of all lists in the chain. So, the compl operation is defined by structural recursion on c0, and takes the completion of the elements of all lists in the chain point-wise. We use head and tail as the inverse of cons.
Fixpoint list_compl_go `{!Cofe A} (c0 : list A) (c : chain listO) : listO :=
  match c0 with
  | [][]
  | x :: c0compl (chain_map (default x head) c) :: list_compl_go c0 (chain_map tail c)

Global Program Instance list_cofe `{!Cofe A} : Cofe listO :=
  {| compl c := list_compl_go (c 0) c |}.
Next Obligation.
  intros ? n c; rewrite /compl.
  assert (c 0 ≡{0}≡ c n) as Hc0 by (symmetry; apply chain_cauchy; lia).
  revert Hc0. generalize (c 0)=> c0. revert c.
  induction c0 as [|x c0 IH]=> c Hc0 /=.
  { by inversion Hc0. }
  apply list_dist_cons_inv_l in Hc0 as (x' & xs' & Hx & Hc0 & Hcn).
  rewrite Hcn. f_equiv.
  - by rewrite conv_compl /= Hcn /=.
  - rewrite IH /= ?Hcn //.

Global Instance list_ofe_discrete : OfeDiscrete A OfeDiscrete listO.
Proof. induction 2; constructor; try apply (discrete _); auto. Qed.

Global Instance nil_discrete : Discrete (@nil A).
Proof. inversion_clear 1; constructor. Qed.
Global Instance cons_discrete x l : Discrete x Discrete l Discrete (x :: l).
Proof. intros ??; inversion_clear 1; constructor; by apply discrete. Qed.

End ofe.

Global Arguments listO : clear implicits.

Non-expansiveness of higher-order list functions and big-ops
Global Instance list_fmap_ne {A B : ofe} (f : A B) n :
  Proper (dist n ==> dist n) f Proper (dist n ==> dist n) (fmap (M:=list) f).
Proof. intros Hf l k ?; by eapply Forall2_fmap, Forall2_impl; eauto. Qed.
Global Instance list_omap_ne {A B : ofe} (f : A option B) n :
  Proper (dist n ==> dist n) f Proper (dist n ==> dist n) (omap (M:=list) f).
  intros Hf. induction 1 as [|x1 x2 l1 l2 Hx Hl]; csimpl; [constructor|].
  destruct (Hf _ _ Hx); [f_equiv|]; auto.
Global Instance imap_ne {A B : ofe} (f : nat A B) n :
  ( i, Proper (dist n ==> dist n) (f i)) Proper (dist n ==> dist n) (imap f).
  intros Hf l1 l2 Hl. revert f Hf.
  induction Hl; intros f Hf; simpl; [constructor|f_equiv; naive_solver].
Global Instance list_bind_ne {A B : ofe} (f : A list A) n :
  Proper (dist n ==> dist n) f Proper (dist n ==> dist n) (mbind f).
Proof. induction 2; simpl; [constructor|solve_proper]. Qed.
Global Instance list_join_ne {A : ofe} : NonExpansive (mjoin (M:=list) (A:=A)).
Proof. induction 1; simpl; [constructor|solve_proper]. Qed.
Global Instance zip_with_ne {A B C : ofe} (f : A B C) n :
  Proper (dist n ==> dist n ==> dist n) f
  Proper (dist n ==> dist n ==> dist n) (zip_with f).
Proof. induction 2; destruct 1; simpl; [constructor..|f_equiv; [f_equiv|]; auto]. Qed.

Lemma big_opL_ne_2 `{Monoid M o} {A : ofe} (f g : nat A M) l1 l2 n :
  l1 ≡{n}≡ l2
  ( k y1 y2,
    l1 !! k = Some y1 l2 !! k = Some y2 y1 ≡{n}≡ y2 f k y1 ≡{n}≡ g k y2)
  ([^o list] k y l1, f k y) ≡{n}≡ ([^o list] k y l2, g k y).
  intros Hl Hf. apply big_opL_gen_proper_2; try (apply _ || done).
  { apply monoid_ne. }
  intros k. assert (l1 !! k ≡{n}≡ l2 !! k) as Hlk by (by f_equiv).
  destruct (l1 !! k) eqn:?, (l2 !! k) eqn:?; inversion Hlk; naive_solver.

Lemma list_fmap_ext_ne {A} {B : ofe} (f g : A B) (l : list A) n :
  ( x, f x ≡{n}≡ g x) f <$> l ≡{n}≡ g <$> l.
Proof. intros Hf. by apply Forall2_fmap, Forall_Forall2_diag, Forall_true. Qed.
Definition listO_map {A B} (f : A -n> B) : listO A -n> listO B :=
  OfeMor (fmap f : listO A listO B).
Global Instance listO_map_ne A B : NonExpansive (@listO_map A B).
Proof. intros n f g ? l. by apply list_fmap_ext_ne. Qed.

Program Definition listOF (F : oFunctor) : oFunctor := {|
  oFunctor_car A _ B _ := listO (oFunctor_car F A B);
  oFunctor_map A1 _ A2 _ B1 _ B2 _ fg := listO_map (oFunctor_map F fg)
Next Obligation.
  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, oFunctor_map_ne.
Next Obligation.
  intros F A ? B ? x. rewrite /= -{2}(list_fmap_id x).
  apply list_fmap_equiv_exty. apply oFunctor_map_id.
Next Obligation.
  intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -list_fmap_compose.
  apply list_fmap_equiv_exty; apply oFunctor_map_compose.

Global Instance listOF_contractive F :
  oFunctorContractive F oFunctorContractive (listOF F).
  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, oFunctor_map_contractive.