Commit fbdb24f9 authored by Amin Timany's avatar Amin Timany
Browse files

Squashed commit of the following:

commit 3b172ff49534fda906fc569449a27fcf6426ed66
Author: Amin Timany <amintimany@gmail.com>
Date:   Wed May 11 17:20:45 2016 +0200

    Add CMRA structure on lists

commit ffe550b0f3cd074b95940106972865a1be1b708b
Author: Amin Timany <amintimany@gmail.com>
Date:   Tue May 10 21:42:09 2016 +0200

    Progress adding CMRA for lists.
parent 28efb904
From iris.algebra Require Export option.
From iris.prelude Require Export list.
From iris.algebra Require Import cmra option.
From iris.prelude Require Import list.
From iris.algebra Require Import upred.
Section cofe.
Context {A : cofeT}.
......@@ -106,3 +107,382 @@ Instance listCF_contractive F :
Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply listC_map_ne, cFunctor_contractive.
Qed.
(* CMRA *)
Section cmra.
Context {A : cmraT}.
Implicit Types l : list A.
Instance list_core : Core (list A) := map core.
Fixpoint list_op_fix (l1 l2 : list A) : list A :=
match l1 with
| [] => l2
| x :: l1' =>
match l2 with
| [] => x :: l1'
| y :: l2' => op x y :: list_op_fix l1' l2'
end
end.
Instance list_op : Op (list A) := list_op_fix.
Instance list_valid : Valid (list A) := Forall (λ x, x).
Instance list_validN : ValidN (list A) := λ n, Forall (λ x, {n} x).
Lemma list_op_lookup i l1 l2 : (l1 l2) !! i = l1 !! i l2 !! i.
Proof.
revert i l2; induction l1 as [|a l1]; intros i [|z l2]; cbn; trivial.
- destruct ((z :: l2) !! i); trivial.
- destruct ((a :: l1) !! i); trivial.
- destruct i; cbn; trivial.
Qed.
Lemma list_op_ne n (l l' l'' : list A) :
l' {n} l'' l l' {n} l l''.
Proof.
revert l' l''.
induction l; cbn; trivial.
destruct l'; destruct l''; inversion 1; subst; trivial.
constructor; [apply cmra_op_ne|]; trivial.
apply IHl; trivial.
Qed.
Lemma list_op_assoc (l l' l'' : list A) : l (l' l'') l l' l''.
Proof.
revert l' l''.
induction l; cbn; trivial.
destruct l'; cbn; trivial.
destruct l''; cbn; trivial.
rewrite cmra_assoc; constructor; trivial.
Qed.
Lemma list_op_comm (l l' : list A) : l l' l' l.
Proof.
revert l'.
induction l; destruct l'; cbn; trivial.
rewrite cmra_comm; constructor; trivial.
Qed.
Lemma list_op_core_l (l : list A) : core l l l.
Proof.
induction l; cbn; trivial.
constructor; auto using cmra_core_l.
Qed.
Lemma list_included_app (x y : A) (l l' : list A) :
(x :: l) (y :: l') (x y) (l l').
Proof.
split.
- intros [[|z l''] H].
+ inversion H; subst.
split.
* exists (core x); rewrite comm; rewrite cmra_core_l; trivial.
* exists (core l); rewrite list_op_comm; rewrite list_op_core_l; trivial.
+ inversion H; subst. split.
* exists z; trivial.
* exists l''; trivial.
- intros [[z H1] [l'' H2]].
eexists (z :: l''); constructor; trivial.
Qed.
Lemma list_core_preserving (l l' : list A) : l l' core l core l'.
Proof.
revert l'.
induction l; destruct l'; cbn; trivial; intros H.
- inversion H as [l'' H']; inversion H'; subst; cbn in *.
eexists; cbn; trivial.
- inversion H as [[|? ?] H']; inversion H'.
- apply list_included_app; apply list_included_app in H.
intuition auto using cmra_core_preserving.
Qed.
Lemma list_lookup_op l1 l2 i : (l1 l2) !! i = l1 !! i l2 !! i.
Proof.
revert l2 i; induction l1.
- induction l2; cbn in *; trivial.
destruct i as [|i]; cbn; trivial.
- intros [| z l2] i; cbn.
+ destruct i as [|i]; cbn; trivial. destruct (l1 !! i); trivial.
+ destruct i as [|i]; cbn; trivial.
Qed.
Lemma list_lookup_core l i : core l !! i = core (l !! i).
Proof. revert i; induction l; cbn; trivial. intros [|i]; cbn; trivial. Qed.
Lemma list_included_spec (l1 l2 : list A) : l1 l2 i, l1 !! i l2 !! i.
Proof.
split.
- revert l2; induction l1; intros [|z l2] H1; cbn; auto.
+ inversion H1; cbn in *.
intros [|i]; [eexists (Some z)|eexists (l2 !! i)]; cbn; eauto.
destruct (l2 !! i); trivial.
+ inversion H1; destruct x; cbn in *;
match goal with [H : _ _ |- _] => inversion H end.
+ inversion H1; destruct x; cbn in *.
* intros i; eexists None.
match goal with [H : _ _ |- _] => rewrite H end.
destruct ((a :: l1) !! i); trivial.
* intros i.
match goal with [H : _ _ |- _] => rewrite H end.
destruct i; cbn; [eexists (Some c); trivial|].
apply IHl1.
exists x; trivial.
- revert l2; induction l1; intros [|z l2] H1; cbn.
+ eexists []; trivial.
+ eexists; eauto; cbn; trivial.
+ specialize (H1 0); cbn in H1.
inversion H1 as [x H1']; destruct x; inversion H1'.
+ set (H2 := H1 0); clearbody H2; cbn in H2.
apply list_included_app; split.
* inversion H2 as [x H2']; destruct x; inversion H2'; subst;
[eexists|eexists (core a)]; eauto.
rewrite comm; rewrite cmra_core_l; trivial.
* apply IHl1. intros i; apply (H1 (S i)).
Qed.
Definition list_cmra_mixin : CMRAMixin (list A).
Proof.
split.
- intros n l l' l'' H; apply list_op_ne; trivial.
- intros n l l' H ;rewrite H; trivial.
- intros n l l' H1 H2.
apply (Forall2_Forall_r _ _ _ _ H1).
apply Forall_forall => x H3 y H4.
eapply Forall_forall in H2; [|eauto]; rewrite -H4; trivial.
- intros l; split.
+ intros H n; apply Forall_forall => x H2.
eapply Forall_forall in H2; [|eauto]; eapply cmra_valid_validN; trivial.
+ intros H; apply Forall_forall => x H2.
apply cmra_valid_validN => n.
eapply Forall_forall in H; eauto.
- intros n l H. apply Forall_forall; intros.
eapply Forall_forall in H; eauto using cmra_validN_S.
- intros l l' l''; apply list_op_assoc.
- intros l l'; apply list_op_comm.
- intros l; induction l; [|constructor]; cbn; auto using cmra_core_l.
- intros l; induction l; [|constructor]; cbn; auto using cmra_core_idemp.
- apply list_core_preserving.
- intros n l; induction l; intros [|z l'] H; cbn in *; auto.
+ constructor.
+ inversion H; subst; constructor.
eapply cmra_validN_op_l; eauto.
eapply IHl; eauto.
- intros n l; induction l; intros [|z' l']; intros [|z'' l''] H1 H2;
try (exfalso; inversion H2; fail); cbn in *.
+ eexists ([], []); repeat split; trivial; cbn in *.
+ eexists ([], _); repeat split; cbn in *; eauto.
+ eexists (_, []); repeat split; do 2 (cbn in *; eauto).
+ edestruct IHl as [[z1 z2] [H31 [H32 H33]]]; cbn in *.
{ inversion H1; trivial. }
{ inversion H2 as [|? ? ? ? H31 H32]; subst; exact H32. }
edestruct (cmra_extend n a) as [[w1 w2] [H41 [H42 H43]]]; cbn in *.
{ inversion H1; trivial. }
{ inversion H2 as [|? ? ? ? H41 H42]; subst; exact H41. }
eexists (w1 :: z1, w2 :: z2); repeat split; cbn.
* inversion H2; subst; constructor;eauto.
* constructor; auto.
* constructor; auto.
Qed.
Global Instance empty_list {B : Type} : Empty (list B) := [].
Canonical Structure listR : cmraT := CMRAT list_cofe_mixin list_cmra_mixin.
Global Instance list_cmra_unit : CMRAUnit listR.
Proof.
split.
- constructor.
- intros h; reflexivity.
- intros n H; inversion H; subst; trivial.
Qed.
Global Instance list_cmra_discrete : CMRADiscrete A CMRADiscrete listR.
Proof. split; [apply _|]. intros m H1.
apply Forall_forall => x H2; eapply Forall_forall in H1.
- apply cmra_discrete_valid; eauto. - trivial.
Qed.
(** Internalized properties *)
Lemma list_equivI {M} l1 l2 : (l1 l2) ( i, l1 !! i l2 !! i : uPred M).
Proof.
uPred.unseal.
constructor; split => H'.
- induction H'; cbn; auto.
+ constructor.
+ intros [|i]; cbn; auto.
constructor; auto.
- revert l2 H'; induction l1; intros [|z l2] H'.
+ constructor.
+ specialize (H' 0); inversion H'.
+ specialize (H' 0); inversion H'.
+ constructor; auto.
* specialize (H' 0); inversion H'; trivial.
* apply IHl1. intros i; apply (H' (S i)).
Qed.
Lemma list_validI {M} l : ( l) ( i, (l !! i) : uPred M).
Proof.
uPred.unseal.
constructor; split => H'.
- induction H'; cbn; auto.
+ constructor.
+ intros [|i]; cbn; auto.
- revert H'; induction l; intros H'.
+ constructor.
+ constructor; auto.
* specialize (H' 0); trivial.
* apply IHl. intros i; apply (H' (S i)).
Qed.
End cmra.
Arguments listR : clear implicits.
Section properties.
Context {A : cmraT}.
Implicit Types l : list A.
Implicit Types a : A.
Lemma list_lookup_validN n l i x : {n} l l !! i {n} Some x {n} x.
Proof.
intros H1 H2.
destruct (l !! i) as [z|] eqn:Heq; inversion H2; subst.
match goal with [H : _ {n} _ |- _] => rewrite -H end.
eapply Forall_lookup in H1; eauto.
Qed.
Lemma list_lookup_valid l i x : l l !! i Some x x.
Proof.
intros H1 H2.
destruct (l !! i) as [z|] eqn:Heq; inversion H2; subst.
match goal with [H : _ _ |- _] => rewrite -H end.
eapply Forall_lookup in H1; eauto.
Qed.
(* We consider two operations update *)
Lemma list_update_updateP (P : A Prop) (Q : list A Prop) l1 x l2 :
x ~~>: P ( y, P y Q (l1 ++ y :: l2)) l1 ++ x :: l2 ~~>: Q.
Proof.
intros Hx%option_updateP' HP n mf Hm.
destruct (Hx n (mf !! (length l1))) as ([y|]&H1&H2); try done.
{ replace (Some x) with ((l1 ++ x :: l2) !! length l1).
- rewrite -list_op_lookup.
destruct (((l1 ++ x :: l2) mf) !! length l1) eqn:Heq.
+ eapply Forall_lookup in Hm; eauto; trivial.
+ contradict Heq.
rewrite list_op_lookup.
rewrite lookup_app_r; trivial.
replace (length l1 - length l1) with 0 by omega.
match goal with
[|- _ ?A _] => destruct A; unfold op, cmra_op; cbn; congruence
end.
- rewrite lookup_app_r; trivial.
replace (length l1 - length l1) with 0 by omega; trivial.
}
eexists. split.
{ apply HP; apply H1. }
apply Forall_lookup => i z H'.
rewrite list_op_lookup in H'.
destruct (lt_dec i (length l1)).
{ rewrite lookup_app_l in H'; trivial.
eapply Forall_lookup in Hm; eauto.
rewrite list_op_lookup.
rewrite lookup_app_l; eauto.
}
destruct (eq_nat_dec i (length l1)); subst.
{ rewrite lookup_app_r in H'; trivial.
replace (length l1 - length l1) with 0 in H' by omega.
cbn in H'.
rewrite H' in H2; trivial.
}
{
rewrite lookup_app_r in H'; try omega.
destruct (i - length l1) as [|j] eqn:Heq; try omega.
eapply Forall_lookup in Hm; eauto.
rewrite list_op_lookup; trivial.
erewrite (lookup_app_r _ _ i); auto with omega.
rewrite Heq; trivial.
}
Qed.
Lemma list_update_update l1 l2 x y : x ~~> y (l1 ++ x :: l2) ~~> (l1 ++ y :: l2).
Proof.
rewrite !cmra_update_updateP => H; eauto using list_update_updateP with subst.
Qed.
(* Applying a local update at a position we own is a local update. *)
Global Instance list_alter_update `{LocalUpdate A Lv L} i :
LocalUpdate (λ L, x, L !! i = Some x Lv x) (alter L i).
Proof.
split; first apply _.
intros n l1 l2 (x&Hix&?) Hm. apply Forall2_lookup => j.
destruct (decide (i = j)) as [->|Heq].
- revert l1 l2 Hix Hm.
induction j; intros [|z l1] [|z' l2] Hix Hm; cbn;
try congruence; try inversion Hix; subst.
+ constructor; trivial.
+ constructor.
eapply local_updateN; eauto. inversion Hm; trivial.
+ unfold op, cmra_op; cbn.
match goal with [|- option_Forall2 _ ?A ?A] => destruct A; constructor; trivial end.
+ unfold op, cmra_op; cbn.
apply IHj; trivial.
inversion Hm; trivial.
- revert i Heq l1 l2 Hix Hm.
induction j; intros i Heq [|z l1] [|z' l2] Hix Hm; cbn;
try congruence; try inversion Hix; subst.
+ unfold op, cmra_op; destruct i; cbn; constructor; trivial.
+ unfold op, cmra_op; destruct i; cbn; constructor; trivial.
inversion H2; subst.
eapply local_updateN; eauto. inversion Hm; trivial.
+ unfold op, cmra_op; cbn.
unfold op, cmra_op; destruct i; cbn;
match goal with [|- option_Forall2 _ ?A ?A] =>
destruct A; constructor; trivial end.
+ unfold op, cmra_op; destruct i; cbn.
* match goal with [|- option_Forall2 _ ?A ?A] =>
destruct A; constructor; trivial end.
* apply IHj; eauto.
inversion Hm; trivial.
Qed.
End properties.
(** Functor *)
Instance list_fmap_cmra_monotone {A B : cmraT} (f : A B)
`{!CMRAMonotone f} : CMRAMonotone (map f).
Proof.
split; try apply _.
- intros n l H1. induction l; inversion H1; constructor.
+ apply validN_preserving; trivial.
+ apply IHl; trivial.
- intros l1 l2 H1.
apply list_included_spec.
intros i.
do 2 rewrite list_lookup_fmap.
apply included_preserving; eauto.
typeclasses eauto.
apply list_included_spec; trivial.
Qed.
Program Definition listRF (F : rFunctor) : rFunctor := {|
rFunctor_car A B := listR (rFunctor_car F A B);
rFunctor_map A1 A2 B1 B2 fg := listC_map (rFunctor_map F fg)
|}.
Next Obligation.
by intros F ???? n f g Hfg; apply listC_map_ne, rFunctor_ne.
Qed.
Next Obligation.
intros F ?? x; cbn in *.
apply equiv_Forall2, Forall2_fmap_l, Forall_Forall2, Forall_forall;
auto using rFunctor_id.
Qed.
Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' x; cbn in *.
rewrite -list_fmap_compose.
apply equiv_Forall2, Forall2_fmap, Forall_Forall2, Forall_forall.
intros; apply rFunctor_compose.
Qed.
Instance listRF_contractive F :
rFunctorContractive F rFunctorContractive (listRF F).
Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply listC_map_ne, rFunctor_contractive.
Qed.
\ No newline at end of file
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