Library iris.unstable.algebra.list

This file is still experimental. See its tracking issue for details on remaining issues before stabilization.
From stdpp Require Export list.
From iris.algebra Require Export cmra list.
From iris.algebra Require Import updates local_updates big_op.
From iris.prelude Require Import options.

Section cmra.
  Context {A : ucmra}.
  Implicit Types l : list A.
  Local Arguments op _ _ !_ !_ / : simpl nomatch.

  Local Instance list_op_instance : Op (list A) :=
    fix go l1 l2 := let _ : Op _ := @go in
    match l1, l2 with
    | [], _l2
    | _, []l1
    | x :: l1, y :: l2x y :: l1 l2
  Local Instance list_pcore_instance : PCore (list A) := λ l, Some (core <$> l).

  Local Instance list_valid_instance : Valid (list A) := Forall (λ x, x).
  Local Instance list_validN_instance : ValidN (list A) := λ n, Forall (λ x, ✓{n} x).

  Lemma cons_valid l x : (x :: l) x l.
  Proof. apply Forall_cons. Qed.
  Lemma cons_validN n l x : ✓{n} (x :: l) ✓{n} x ✓{n} l.
  Proof. apply Forall_cons. Qed.
  Lemma app_valid l1 l2 : (l1 ++ l2) l1 l2.
  Proof. apply Forall_app. Qed.
  Lemma app_validN n l1 l2 : ✓{n} (l1 ++ l2) ✓{n} l1 ✓{n} l2.
  Proof. apply Forall_app. Qed.

  Lemma list_lookup_valid l : l i, (l !! i).
    rewrite {1}/valid /list_valid_instance Forall_lookup; split.
    - intros Hl i. by destruct (l !! i) as [x|] eqn:?; [apply (Hl i)|].
    - intros Hl i x Hi. move: (Hl i); by rewrite Hi.
  Lemma list_lookup_validN n l : ✓{n} l i, ✓{n} (l !! i).
    rewrite {1}/validN /list_validN_instance Forall_lookup; split.
    - intros Hl i. by destruct (l !! i) as [x|] eqn:?; [apply (Hl i)|].
    - intros Hl i x Hi. move: (Hl i); by rewrite Hi.
  Lemma list_lookup_op l1 l2 i : (l1 l2) !! i = l1 !! i l2 !! i.
    revert i l2. induction l1 as [|x l1]; intros [|i] [|y l2];
      by rewrite /= ?left_id_L ?right_id_L.
  Lemma list_lookup_core l i : core l !! i = core (l !! i).
    rewrite /core /= list_lookup_fmap.
    destruct (l !! i); by rewrite /= ?Some_core.

  Lemma list_lookup_included l1 l2 : l1 l2 i, l1 !! i l2 !! i.
    { intros [l Hl] i. (l !! i). by rewrite Hl list_lookup_op. }
    revert l1. induction l2 as [|y l2 IH]=>-[|x l1] Hl.
    - by [].
    - destruct (Hl 0) as [[z|] Hz]; inversion Hz.
    - by (y :: l2).
    - destruct (IH l1) as [l3 ?]; first (intros i; apply (Hl (S i))).
      destruct (Hl 0) as [[z|] Hz]; inversion_clear Hz; simplify_eq/=.
      + (z :: l3); by constructor.
      + (core x :: l3); constructor; by rewrite ?cmra_core_r.

  Definition list_cmra_mixin : CmraMixin (list A).
    apply cmra_total_mixin.
    - eauto.
    - intros n l l1 l2; rewrite !list_dist_lookupHl i.
      by rewrite !list_lookup_op Hl.
    - intros n l1 l2 Hl; by rewrite /core /= Hl.
    - intros n l1 l2; rewrite !list_dist_lookup !list_lookup_validNHl ? i.
      by rewrite -Hl.
    - intros l. rewrite list_lookup_valid. setoid_rewrite list_lookup_validN.
      setoid_rewrite cmra_valid_validN. naive_solver.
    - intros n x. rewrite !list_lookup_validN. auto using cmra_validN_S.
    - intros l1 l2 l3; rewrite list_equiv_lookupi.
      by rewrite !list_lookup_op assoc.
    - intros l1 l2; rewrite list_equiv_lookupi.
      by rewrite !list_lookup_op comm.
    - intros l; rewrite list_equiv_lookupi.
      by rewrite list_lookup_op list_lookup_core cmra_core_l.
    - intros l; rewrite list_equiv_lookupi.
      by rewrite !list_lookup_core cmra_core_idemp.
    - intros l1 l2; rewrite !list_lookup_includedHl i.
      rewrite !list_lookup_core. by apply cmra_core_mono.
    - intros n l1 l2. rewrite !list_lookup_validN.
      setoid_rewrite list_lookup_op. eauto using cmra_validN_op_l.
    - intros n l.
      induction l as [|x l IH]=> -[|y1 l1] [|y2 l2] Hl Heq;
        (try by exfalso; inversion Heq).
      + by [], [].
      + [], (x :: l); inversion Heq; by repeat constructor.
      + (x :: l), []; inversion Heq; by repeat constructor.
      + destruct (IH l1 l2) as (l1'&l2'&?&?&?),
          (cmra_extend n x y1 y2) as (y1'&y2'&?&?&?);
          [by inversion_clear Heq; inversion_clear Hl..|].
         (y1' :: l1'), (y2' :: l2'); repeat constructor; auto.
  Canonical Structure listR := Cmra (list A) list_cmra_mixin.

  Global Instance list_unit_instance : Unit (list A) := [].
  Definition list_ucmra_mixin : UcmraMixin (list A).
    - constructor.
    - by intros l.
    - by constructor.
  Canonical Structure listUR := Ucmra (list A) list_ucmra_mixin.

  Global Instance list_cmra_discrete : CmraDiscrete A CmraDiscrete listR.
    split; [apply _|]=> l; rewrite list_lookup_valid list_lookup_validNHl i.
    by apply cmra_discrete_valid.

  Lemma list_core_id' l : ( x, x l CoreId x) CoreId l.
    intros Hyp. constructor. apply list_equiv_lookupi.
    rewrite list_lookup_core.
    destruct (l !! i) eqn:E; last done.
    by eapply Hyp, elem_of_list_lookup_2.

  Global Instance list_core_id l : ( x : A, CoreId x) CoreId l.
  Proof. intros Hyp; by apply list_core_id'. Qed.

End cmra.

Global Arguments listR : clear implicits.
Global Arguments listUR : clear implicits.

Global Instance list_singletonM {A : ucmra} : SingletonM nat A (list A) := λ n x,
  replicate n ε ++ [x].

Section properties.
  Context {A : ucmra}.
  Implicit Types l : list A.
  Implicit Types x y z : A.
  Local Arguments op _ _ !_ !_ / : simpl nomatch.
  Local Arguments cmra_op _ !_ !_ / : simpl nomatch.
  Local Arguments ucmra_op _ !_ !_ / : simpl nomatch.

  Lemma list_lookup_opM l mk i : (l ⋅? mk) !! i = l !! i (mk ≫= (.!! i)).
  Proof. destruct mk; by rewrite /= ?list_lookup_op ?right_id_L. Qed.

  Global Instance list_op_nil_l : LeftId (=) (@nil A) op.
  Proof. done. Qed.
  Global Instance list_op_nil_r : RightId (=) (@nil A) op.
  Proof. by intros []. Qed.

  Lemma list_op_app l1 l2 l3 :
    (l1 ++ l3) l2 = (l1 take (length l1) l2) ++ (l3 drop (length l1) l2).
    revert l2 l3.
    induction l1 as [|x1 l1]=> -[|x2 l2] [|x3 l3]; f_equal/=; auto.
  Lemma list_op_app_le l1 l2 l3 :
    length l2 length l1 (l1 ++ l3) l2 = (l1 l2) ++ l3.
  Proof. intros ?. by rewrite list_op_app take_ge // drop_ge // right_id_L. Qed.

  Lemma list_drop_op l1 l2 i:
    drop i l1 drop i l2 = drop i (l1 l2).
    apply list_eq. intros j.
    rewrite list_lookup_op !lookup_drop -list_lookup_op.

  Lemma list_take_op l1 l2 i:
    take i l1 take i l2 = take i (l1 l2).
    apply list_eq. intros j.
    rewrite list_lookup_op.
    destruct (decide (j < i)%nat).
    - by rewrite !lookup_take // -list_lookup_op.
    - by rewrite !lookup_take_ge //; lia.

  Lemma list_lookup_validN_Some n l i x : ✓{n} l l !! i ≡{n}≡ Some x ✓{n} x.
  Proof. move⇒ /list_lookup_validN /(_ i)=> Hl Hi; move: Hl. by rewrite Hi. Qed.
  Lemma list_lookup_valid_Some l i x : l l !! i Some x x.
  Proof. move⇒ /list_lookup_valid /(_ i)=> Hl Hi; move: Hl. by rewrite Hi. Qed.

  Lemma list_length_op l1 l2 : length (l1 l2) = max (length l1) (length l2).
  Proof. revert l2. induction l1; intros [|??]; f_equal/=; auto. Qed.

  Lemma replicate_valid n (x : A) : x replicate n x.
  Proof. apply Forall_replicate. Qed.
  Global Instance list_singletonM_ne i : NonExpansive (singletonM (M:=list A) i).
  Proof. intros n l1 l2 ?. apply Forall2_app; by repeat constructor. Qed.
  Global Instance list_singletonM_proper i :
    Proper ((≡) ==> (≡)) (singletonM (M:=list A) i) := ne_proper _.

  Lemma elem_of_list_singletonM i z x : z ({[i := x]} : list A) z = ε z = x.
    rewrite elem_of_app elem_of_list_singleton elem_of_replicate. naive_solver.
  Lemma list_lookup_singletonM i x : ({[ i := x ]} : list A) !! i = Some x.
  Proof. induction i; by f_equal/=. Qed.
  Lemma list_lookup_singletonM_lt i i' x:
    (i' < i)%nat ({[ i := x ]} : list A) !! i' = Some ε.
  Proof. move: i'. induction i; intros [|i']; naive_solver auto with lia. Qed.
  Lemma list_lookup_singletonM_gt i i' x:
    (i < i')%nat ({[ i := x ]} : list A) !! i' = None.
  Proof. move: i'. induction i; intros [|i']; naive_solver auto with lia. Qed.
  Lemma list_lookup_singletonM_ne i j x :
    i j
    ({[ i := x ]} : list A) !! j = None ({[ i := x ]} : list A) !! j = Some ε.
  Proof. revert j; induction i; intros [|j]; naive_solver auto with lia. Qed.
  Lemma list_singletonM_validN n i x : ✓{n} ({[ i := x ]} : list A) ✓{n} x.
    rewrite list_lookup_validN. split.
    { move⇒ /(_ i). by rewrite list_lookup_singletonM. }
    intros Hx j; destruct (decide (i = j)); subst.
    - by rewrite list_lookup_singletonM.
    - destruct (list_lookup_singletonM_ne i j x) as [Hi|Hi]; first done;
        rewrite Hi; by try apply (ucmra_unit_validN (A:=A)).
  Lemma list_singletonM_valid i x : ({[ i := x ]} : list A) x.
    rewrite !cmra_valid_validN. by setoid_rewrite list_singletonM_validN.
  Lemma list_singletonM_length i x : length {[ i := x ]} = S i.
    rewrite /singletonM /list_singletonM app_length replicate_length /=; lia.

  Lemma list_singletonM_core i (x : A) : core {[ i := x ]} ≡@{list A} {[ i := core x ]}.
    rewrite /singletonM /list_singletonM.
    by rewrite {1}/core /= fmap_app fmap_replicate (core_id_core _).
  Lemma list_singletonM_op i (x y : A) :
    {[ i := x ]} {[ i := y ]} ≡@{list A} {[ i := x y ]}.
    rewrite /singletonM /list_singletonM /=.
    induction i; constructor; rewrite ?left_id; auto.
  Lemma list_alter_singletonM f i x :
    alter f i ({[i := x]} : list A) = {[i := f x]}.
    rewrite /singletonM /list_singletonM /=. induction i; f_equal/=; auto.
  Global Instance list_singletonM_core_id i (x : A) :
    CoreId x CoreId {[ i := x ]}.
  Proof. by rewrite !core_id_total list_singletonM_core⇒ →. Qed.
  Lemma list_singletonM_snoc l x:
    {[length l := x]} l l ++ [x].
  Proof. elim: l ⇒ //= ?? <-. by rewrite left_id. Qed.
  Lemma list_singletonM_included i x l:
    {[i := x]} l ( x', l !! i = Some x' x x').
    rewrite list_lookup_included. split.
    { move /(_ i). rewrite list_lookup_singletonM option_included_total.
      naive_solver. }
    intros (y&Hi&?) j. destruct (Nat.lt_total j i) as [?|[->|?]].
    - rewrite list_lookup_singletonM_lt //.
      destruct (lookup_lt_is_Some_2 l j) as [z Hz].
      { trans i; eauto using lookup_lt_Some. }
      rewrite Hz. by apply Some_included_mono, ucmra_unit_least.
    - rewrite list_lookup_singletonM Hi. by apply Some_included_mono.
    - rewrite list_lookup_singletonM_gt //. apply: ucmra_unit_least.

  Lemma list_singletonM_updateP (P : A Prop) (Q : list A Prop) x :
    x ~~>: P ( y, P y Q [y]) [x] ~~>: Q.
    rewrite !cmra_total_updatePHup HQ n lf /list_lookup_validN Hv.
    destruct (Hup n (default ε (lf !! 0))) as (y&?&Hv').
    { move: (Hv 0). by destruct lf; rewrite /= ?right_id. }
     [y]; split; first by auto.
    apply list_lookup_validNi.
    move: (Hv i) Hv'. by destruct i, lf; rewrite /= ?right_id.
  Lemma list_singletonM_updateP' (P : A Prop) x :
    x ~~>: P [x] ~~>: λ k, y, k = [y] P y.
  Proof. eauto using list_singletonM_updateP. Qed.
  Lemma list_singletonM_update x y : x ~~> y [x] ~~> [y].
    rewrite !cmra_update_updateP; eauto using list_singletonM_updateP with subst.

  Lemma app_updateP (P1 P2 Q : list A Prop) l1 l2 :
    l1 ~~>: P1 l2 ~~>: P2
    ( k1 k2, P1 k1 P2 k2 length l1 = length k1 Q (k1 ++ k2))
    l1 ++ l2 ~~>: Q.
    rewrite !cmra_total_updatePHup1 Hup2 HQ n lf.
    rewrite list_op_app app_validN⇒ -[??].
    destruct (Hup1 n (take (length l1) lf)) as (k1&?&?); auto.
    destruct (Hup2 n (drop (length l1) lf)) as (k2&?&?); auto.
     (k1 ++ k2). rewrite list_op_app app_validN.
    by destruct (HQ k1 k2) as [<- ?].
  Lemma app_update l1 l2 k1 k2 :
    length l1 = length k1
    l1 ~~> k1 l2 ~~> k2 l1 ++ l2 ~~> k1 ++ k2.
  Proof. rewrite !cmra_update_updateP; eauto using app_updateP with subst. Qed.

  Lemma cons_updateP (P1 : A Prop) (P2 Q : list A Prop) x l :
    x ~~>: P1 l ~~>: P2 ( y k, P1 y P2 k Q (y :: k)) x :: l ~~>: Q.
    intros. eapply (app_updateP _ _ _ [x]);
      naive_solver eauto using list_singletonM_updateP'.
  Lemma cons_updateP' (P1 : A Prop) (P2 : list A Prop) x l :
    x ~~>: P1 l ~~>: P2 x :: l ~~>: λ k, y k', k = y :: k' P1 y P2 k'.
  Proof. eauto 10 using cons_updateP. Qed.
  Lemma cons_update x y l k : x ~~> y l ~~> k x :: l ~~> y :: k.
  Proof. rewrite !cmra_update_updateP; eauto using cons_updateP with subst. Qed.

  Lemma list_middle_updateP (P : A Prop) (Q : list A Prop) l1 x l2 :
    x ~~>: P ( y, P y Q (l1 ++ y :: l2)) l1 ++ x :: l2 ~~>: Q.
    intros. eapply app_updateP.
    - by apply cmra_update_updateP.
    - by eapply cons_updateP', cmra_update_updateP.
    - naive_solver.
  Lemma list_middle_update l1 l2 x y : x ~~> y l1 ++ x :: l2 ~~> l1 ++ y :: l2.
    rewrite !cmra_update_updateP⇒ ?; eauto using list_middle_updateP with subst.

  Lemma list_alloc_singletonM_local_update x l :
     x (l, ε) ¬l~> (l ++ [x], {[length l := x]}).
    move ⇒ ?.
    have → : ({[length l := x]} ≡@{list A} {[length l := x]} ε) by rewrite right_id.
    rewrite -list_singletonM_snoc. apply op_local_update ⇒ ??.
    rewrite list_singletonM_snoc app_validN cons_validN. split_and? ⇒ //; [| constructor].
    by apply cmra_valid_validN.

  Lemma list_lookup_local_update l k l' k':
    ( i, (l !! i, k !! i) ¬l~> (l' !! i, k' !! i))
    (l, k) ¬l~> (l', k').
    intros Hup.
    apply local_update_unitaln z Hlv Hl.
    assert ( i, ✓{n} (l' !! i) l' !! i ≡{n}≡ (k' z) !! i) as Hup'.
    { intros i. destruct (Hup i n (Some (z !! i))); simpl in ×.
      - by apply list_lookup_validN.
      - rewrite -list_lookup_op.
        by apply list_dist_lookup.
      - by rewrite list_lookup_op.
    split; [apply list_lookup_validN | apply list_dist_lookup].
    all: intros i; by destruct (Hup' i).

  Lemma list_alter_local_update i f g l k:
    (l !! i, k !! i) ¬l~> (f <$> (l !! i), g <$> (k !! i))
    (l, k) ¬l~> (alter f i l, alter g i k).
    intros Hup.
    apply list_lookup_local_update.
    intros i'.
    destruct (decide (i = i')) as [->|].
    - rewrite !list_lookup_alter //.
    - rewrite !list_lookup_alter_ne //.

  Lemma app_l_local_update l k k' m m':
    (k, drop (length l) m) ¬l~> (k', m')
    (l ++ k, m) ¬l~> (l ++ k', take (length l) m (replicate (length l) ε ++ m')).
    move /(local_update_unital _) ⇒ HUp.
    apply local_update_unitaln mm /(app_validN _) [Hlv Hkv] Heq.
    move: (HUp n (drop (length l) mm) Hkv).
    intros [Hk'v Hk'eq];
      first by rewrite list_drop_op -Heq drop_app_le // drop_ge //.
    split; first by apply app_validN.
    rewrite Hk'eq.
    apply list_dist_lookup. intros i. rewrite !list_lookup_op.
    destruct (decide (i < length l)%nat) as [HLt|HGe].
    - rewrite !lookup_app_l //; last by rewrite replicate_length.
      rewrite lookup_take; last done.
      rewrite lookup_replicate_2; last done.
      rewrite comm assoc -list_lookup_op.
      rewrite (mixin_cmra_comm _ list_cmra_mixin) -Heq.
      rewrite lookup_app_l; last done.
      apply lookup_lt_is_Some in HLt as [? HEl].
      by rewrite HEl -Some_op ucmra_unit_right_id.
    - assert (length l i)%nat as HLe by lia.
      rewrite !lookup_app_r //; last by rewrite replicate_length.
      rewrite replicate_length.
      rewrite lookup_take_ge; last done.
      replace (mm !! _) with (drop (length l) mm !! (i - length l)%nat);
        last by rewrite lookup_drop; congr (mm !! _); lia.
      rewrite -assoc -list_lookup_op. symmetry.
      clear. move: n. apply equiv_dist. apply: ucmra_unit_left_id.

  Lemma app_l_local_update' l k k' m:
    (k, ε) ¬l~> (k', m)
    (l ++ k, ε) ¬l~> (l ++ k', replicate (length l) ε ++ m).
    remember (app_l_local_update l k k' ε m) as HH eqn:HeqHH.
    clear HeqHH. move: HH.
    by rewrite take_nil drop_nil ucmra_unit_left_id.

  Lemma app_local_update l m:
     m (l, ε) ¬l~> (l ++ m, replicate (length l) ε ++ m).
    move: (app_l_local_update' l [] m m).
    rewrite app_nil_r.
    moveH Hvm. apply H.
    apply local_update_unitaln z _. rewrite ucmra_unit_left_id.
    move=><-. rewrite ucmra_unit_right_id. split; last done.
    by apply cmra_valid_validN.

  Lemma app_r_local_update l l' k m m':
    length l = length l'
    (l, take (length l) m) ¬l~> (l', m')
    (l ++ k, m) ¬l~> (l' ++ k, replicate (length l) ε m' ++ drop (length l) m).
    moveHLen /(local_update_unital _) HUp.
    apply local_update_unitaln mm /(app_validN _) [Hlv Hkv] Heq.
    move: (HUp n (take (length l) mm) Hlv).
    intros [Hl'v Hl'eq];
      first by rewrite list_take_op -Heq take_app_le // take_ge //.
    split; first by apply app_validN.
    assert (k ≡{n}≡ (drop (length l) (m mm))) as
      by rewrite -Heq drop_app_le // drop_ge //.
    move: HLen. rewrite Hl'eq. clear. moveHLen.
    assert (length m' length l)%nat as HLen'.
    { by rewrite list_length_op in HLen; lia. }
    rewrite list_op_app list_length_op replicate_length max_l;
      last lia.
    rewrite list_drop_op -assoc. rewrite HLen. move: HLen'.
    remember (length l) as o. clear.
    rewrite list_length_op.
    remember (length _ `max` length _)%nat as o'.
    assert (m' take o' mm ≡{n}≡ replicate o' ε (m' take o' mm))
      as <-; last done.
    subst. remember (m' take _ _) as m''.
    remember (length m' `max` length (take o mm))%nat as o''.
    assert (o'' length m'')%nat as HLen.
    { by subst; rewrite list_length_op !take_length; lia. }
    move: HLen. clear.
    intros HLen. move: n. apply equiv_dist, list_equiv_lookup.
    intros i. rewrite list_lookup_op.
    remember length as L eqn:HeqL.
    destruct (decide (i < L m''))%nat as [E|E].
    - subst. apply lookup_lt_is_Some in E as [? HEl].
      rewrite HEl.
      destruct (replicate _ _ !! _) eqn:Z; last done.
      apply lookup_replicate in Z as [-> _].
      by rewrite -Some_op ucmra_unit_left_id.
    - rewrite lookup_ge_None_2.
      { rewrite lookup_ge_None_2 //.
        by rewrite replicate_length; lia. }
      rewrite -HeqL. lia.

  Lemma app_r_local_update' l l' k k':
    length l = length l'
    (l, ε) ¬l~> (l', k')
    (l ++ k, ε) ¬l~> (l' ++ k, k').
    moveHLen /(local_update_unital _) HUp.
    apply local_update_unitaln mz /(app_validN _) [Hlv Hkv].
    move: (HUp n l). rewrite !ucmra_unit_left_id.
    intros [Hk'v Hk'eq] <-; [done|done|].
    split; first by apply app_validN.
    move: HLen. rewrite Hk'eq. clear. moveHLen.
    assert (length k' length l)%nat as Hk'Len
        by (rewrite HLen list_length_op; lia).
    rewrite (mixin_cmra_comm _ list_cmra_mixin k' (l ++ k)).
    rewrite list_op_app_le; last done.
    by rewrite (mixin_cmra_comm _ list_cmra_mixin l k').

End properties.

Global Instance list_fmap_cmra_morphism {A B : ucmra} (f : A B)
  `{!CmraMorphism f} : CmraMorphism (fmap f : list A list B).
  split; try apply _.
  - intros n l. rewrite !list_lookup_validNHl i. rewrite list_lookup_fmap.
    by apply (cmra_morphism_validN (fmap f : option A option B)).
  - intros l. apply Some_proper. rewrite -!list_fmap_compose.
    apply list_fmap_equiv_ext=>???. apply cmra_morphism_core, _.
  - intros l1 l2. apply list_equiv_lookupi.
    by rewrite list_lookup_op !list_lookup_fmap list_lookup_op cmra_morphism_op.

Program Definition listURF (F : urFunctor) : urFunctor := {|
  urFunctor_car A _ B _ := listUR (urFunctor_car F A B);
  urFunctor_map A1 _ A2 _ B1 _ B2 _ fg := listO_map (urFunctor_map F fg)
Next Obligation.
  by intros F A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, urFunctor_map_ne.
Next Obligation.
  intros F A ? B ? x. rewrite /= -{2}(list_fmap_id x).
  apply list_fmap_equiv_ext=>???. apply urFunctor_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_ext=>???; apply urFunctor_map_compose.

Global Instance listURF_contractive F :
  urFunctorContractive F urFunctorContractive (listURF F).
  by intros ? A1 ? A2 ? B1 ? B2 ? n f g Hfg; apply listO_map_ne, urFunctor_map_contractive.

Program Definition listRF (F : urFunctor) : rFunctor := {|
  rFunctor_car A _ B _ := listR (urFunctor_car F A B);
  rFunctor_map A1 _ A2 _ B1 _ B2 _ fg := listO_map (urFunctor_map F fg)
Solve Obligations with apply listURF.

Global Instance listRF_contractive F :
  urFunctorContractive F rFunctorContractive (listRF F).
Proof. apply listURF_contractive. Qed.