Commit 3c9e6825 authored by Robbert Krebbers's avatar Robbert Krebbers

A more understandable proof that lists form a COFE.

This proof also more easily scales to other recursive types, like
trees etc.
parent 17bc1af5
......@@ -11,5 +11,5 @@ install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [
"coq" { (>= "8.7.1" & < "8.10~") | (= "dev") }
"coq-stdpp" { (= "1.2.0") | (= "dev") }
"coq-stdpp" { (= "dev.2019-05-03.0.09f69b7c") | (= "dev") }
]
......@@ -19,7 +19,7 @@ Global Instance length_ne n : Proper (dist n ==> (=)) (@length A) := _.
Global Instance tail_ne : NonExpansive (@tail A) := _.
Global Instance take_ne : NonExpansive (@take A n) := _.
Global Instance drop_ne : NonExpansive (@drop A n) := _.
Global Instance list_head_ne : NonExpansive (head (A:=A)).
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).
......@@ -63,28 +63,30 @@ Proof.
Qed.
Canonical Structure listC := OfeT (list A) list_ofe_mixin.
Program Definition list_chain
(c : chain listC) (x : A) (k : nat) : chain A :=
{| chain_car n := default x (c n !! k) |}.
Next Obligation. intros c x k n i ?. by rewrite /= (chain_cauchy c n i). Qed.
Definition list_compl `{!Cofe A} : Compl listC := λ c,
match c 0 with
(** 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 listC) : listC :=
match c0 with
| [] => []
| x :: _ => compl list_chain c x <$> seq 0 (length (c 0))
| x :: c0 => compl (chain_map (default x head) c) :: list_compl_go c0 (chain_map tail c)
end.
Global Program Instance list_cofe `{!Cofe A} : Cofe listC :=
{| compl := list_compl |}.
{| compl c := list_compl_go (c 0) c |}.
Next Obligation.
intros ? n c; rewrite /compl /list_compl.
destruct (c 0) as [|x l] eqn:Hc0 at 1.
{ by destruct (chain_cauchy c 0 n); auto with lia. }
rewrite -(λ H, length_ne _ _ _ (chain_cauchy c 0 n H)); last lia.
apply Forall2_lookup=> i. rewrite -dist_option_Forall2 list_lookup_fmap.
destruct (decide (i < length (c n))); last first.
{ rewrite lookup_seq_ge ?lookup_ge_None_2; auto with lia. }
rewrite lookup_seq //= (conv_compl n (list_chain c _ _)) /=.
destruct (lookup_lt_is_Some_2 (c n) i) as [? Hcn]; first done.
by rewrite Hcn.
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 //.
Qed.
Global Instance list_ofe_discrete : OfeDiscrete A OfeDiscrete listC.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment