Commit 5088d5b0 authored by Robbert's avatar Robbert

Merge branch 'robbert/big_op_proper' into 'master'

More proper/non-expansiveness results for maps, lists, and big ops

See merge request iris/iris!359
parents 62d3e6cb 0b36eb76
This diff is collapsed.
......@@ -44,32 +44,28 @@ Proof. intros ? m m' ? i. by apply (discrete _). Qed.
Global Instance gmapO_leibniz: LeibnizEquiv A LeibnizEquiv gmapO.
Proof. intros; change (LeibnizEquiv (gmap K A)); apply _. Qed.
Global Instance lookup_ne k :
NonExpansive (lookup k : gmap K A option A).
Global Instance lookup_ne k : NonExpansive (lookup k : gmap K A option A).
Proof. by intros m1 m2. Qed.
Global Instance lookup_proper k :
Proper (() ==> ()) (lookup k : gmap K A option A) := _.
Global Instance alter_ne (f : A A) (k : K) n :
Proper (dist n ==> dist n) f Proper (dist n ==> dist n) (alter f k).
Global Instance partial_alter_ne n :
Proper ((dist n ==> dist n) ==> (=) ==> dist n ==> dist n)
(partial_alter (M:=gmap K A)).
Proof.
intros ? m m' Hm k'.
by destruct (decide (k = k')); simplify_map_eq; rewrite (Hm k').
Qed.
Global Instance insert_ne i :
NonExpansive2 (insert (M:=gmap K A) i).
Proof.
intros n x y ? m m' ? j; destruct (decide (i = j)); simplify_map_eq;
[by constructor|by apply lookup_ne].
by intros f1 f2 Hf i ? <- m1 m2 Hm j; destruct (decide (i = j)) as [->|];
rewrite ?lookup_partial_alter ?lookup_partial_alter_ne //;
try apply Hf; apply lookup_ne.
Qed.
Global Instance singleton_ne i :
NonExpansive (singletonM i : A gmap K A).
Global Instance insert_ne i : NonExpansive2 (insert (M:=gmap K A) i).
Proof. intros n x y ? m m' ? j; apply partial_alter_ne; by try constructor. Qed.
Global Instance singleton_ne i : NonExpansive (singletonM i : A gmap K A).
Proof. by intros ????; apply insert_ne. Qed.
Global Instance delete_ne i :
NonExpansive (delete (M:=gmap K A) i).
Global Instance delete_ne i : NonExpansive (delete (M:=gmap K A) i).
Proof.
intros n m m' ? j; destruct (decide (i = j)); simplify_map_eq;
[by constructor|by apply lookup_ne].
Qed.
Global Instance alter_ne (f : A A) (k : K) n :
Proper (dist n ==> dist n) f Proper (dist n ==> dist n) (alter f k).
Proof. intros ? m m' Hm k'. by apply partial_alter_ne; [solve_proper|..]. Qed.
Global Instance gmap_empty_discrete : Discrete ( : gmap K A).
Proof.
......@@ -99,6 +95,63 @@ End cofe.
Arguments gmapO _ {_ _} _.
(** Non-expansiveness of higher-order map functions and big-ops *)
Lemma merge_ne `{Countable K} {A B C : ofeT} (f g : option A option B option C)
`{!DiagNone f, !DiagNone g} n :
((dist n) ==> (dist n) ==> (dist n))%signature f g
((dist n) ==> (dist n) ==> (dist n))%signature (merge (M:=gmap K) f) (merge g).
Proof. by intros Hf ?? Hm1 ?? Hm2 i; rewrite !lookup_merge //; apply Hf. Qed.
Instance union_with_proper `{Countable K} {A : ofeT} n :
Proper (((dist n) ==> (dist n) ==> (dist n)) ==>
(dist n) ==> (dist n) ==>(dist n)) (union_with (M:=gmap K A)).
Proof.
intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ne _ _); auto.
by do 2 destruct 1; first [apply Hf | constructor].
Qed.
Instance map_fmap_proper `{Countable K} {A B : ofeT} (f : A B) n :
Proper (dist n ==> dist n) f Proper (dist n ==> dist n) (fmap (M:=gmap K) f).
Proof. intros ? m m' ? k; rewrite !lookup_fmap. by repeat f_equiv. Qed.
Instance map_zip_with_proper `{Countable K} {A B C : ofeT} (f : A B C) n :
Proper (dist n ==> dist n ==> dist n) f
Proper (dist n ==> dist n ==> dist n) (map_zip_with (M:=gmap K) f).
Proof.
intros Hf m1 m1' Hm1 m2 m2' Hm2. apply merge_ne; try done.
destruct 1; destruct 1; repeat f_equiv; constructor || done.
Qed.
Lemma big_opM_ne_2 `{Monoid M o} `{Countable K} {A : ofeT} (f g : K A M) m1 m2 n :
m1 {n} m2
( k y1 y2,
m1 !! k = Some y1 m2 !! k = Some y2 y1 {n} y2 f k y1 {n} g k y2)
([^o map] k y m1, f k y) {n} ([^o map] k y m2, g k y).
Proof.
intros Hl Hf. apply big_opM_gen_proper_2; try (apply _ || done).
{ by intros ?? ->. }
{ apply monoid_ne. }
intros k. assert (m1 !! k {n} m2 !! k) as Hlk by (by f_equiv).
destruct (m1 !! k) eqn:?, (m2 !! k) eqn:?; inversion Hlk; naive_solver.
Qed.
Lemma big_sepM2_ne_2 {PROP : bi} `{Countable K} (A B : ofeT)
(Φ Ψ : K A B PROP) m1 m2 m1' m2' n :
m1 {n} m1' m2 {n} m2'
( k y1 y1' y2 y2',
m1 !! k = Some y1 m1' !! k = Some y1' y1 {n} y1'
m2 !! k = Some y2 m2' !! k = Some y2' y2 {n} y2'
Φ k y1 y2 {n} Ψ k y1' y2')
([ map] k y1;y2 m1;m2, Φ k y1 y2)%I {n} ([ map] k y1;y2 m1';m2', Ψ k y1 y2)%I.
Proof.
intros Hm1 Hm2 Hf. rewrite big_sepM2_eq /big_sepM2_def. f_equiv.
{ f_equiv; split; intros Hm k.
- trans (is_Some (m1 !! k)); [symmetry; apply: is_Some_ne; by f_equiv|].
rewrite Hm. apply: is_Some_ne; by f_equiv.
- trans (is_Some (m1' !! k)); [apply: is_Some_ne; by f_equiv|].
rewrite Hm. symmetry. apply: is_Some_ne; by f_equiv. }
apply big_opM_ne_2; [by f_equiv|].
intros k [x1 y1] [x2 y2] (?&?&[=<- <-]&?&?)%map_lookup_zip_with_Some
(?&?&[=<- <-]&?&?)%map_lookup_zip_with_Some [??]; naive_solver.
Qed.
(* CMRA *)
Section cmra.
Context `{Countable K} {A : cmraT}.
......
......@@ -94,13 +94,64 @@ End cofe.
Arguments listO : clear implicits.
(** Non-expansiveness of higher-order list functions and big-ops *)
Instance list_fmap_ne {A B : ofeT} (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.
Instance list_omap_ne {A B : ofeT} (f : A option B) n :
Proper (dist n ==> dist n) f Proper (dist n ==> dist n) (omap (M:=list) f).
Proof.
intros Hf. induction 1 as [|x1 x2 l1 l2 Hx Hl]; csimpl; [constructor|].
destruct (Hf _ _ Hx); [f_equiv|]; auto.
Qed.
Instance imap_ne {A B : ofeT} (f : nat A B) n :
( i, Proper (dist n ==> dist n) (f i)) Proper (dist n ==> dist n) (imap f).
Proof.
intros Hf l1 l2 Hl. revert f Hf.
induction Hl; intros f Hf; simpl; [constructor|f_equiv; naive_solver].
Qed.
Instance list_bind_ne {A B : ofeT} (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.
Instance list_join_ne {A : ofeT} : NonExpansive (mjoin (M:=list) (A:=A)).
Proof. induction 1; simpl; [constructor|solve_proper]. Qed.
Instance zip_with_ne {A B C : ofeT} (f : A B C) :
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 : ofeT} (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).
Proof.
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.
Qed.
Lemma big_sepL2_ne_2 {PROP : bi} {A B : ofeT}
(Φ Ψ : nat A B PROP) l1 l2 l1' l2' n :
l1 {n} l1' l2 {n} l2'
( k y1 y1' y2 y2',
l1 !! k = Some y1 l1' !! k = Some y1' y1 {n} y1'
l2 !! k = Some y2 l2' !! k = Some y2' y2 {n} y2'
Φ k y1 y2 {n} Ψ k y1' y2')
([ list] k y1;y2 l1;l2, Φ k y1 y2)%I {n} ([ list] k y1;y2 l1';l2', Ψ k y1 y2)%I.
Proof.
intros Hl1 Hl2 Hf. rewrite !big_sepL2_alt. f_equiv.
{ do 2 f_equiv; by apply: length_ne. }
apply big_opL_ne_2; [by f_equiv|].
intros k [x1 y1] [x2 y2] (?&?&[=<- <-]&?&?)%lookup_zip_with_Some
(?&?&[=<- <-]&?&?)%lookup_zip_with_Some [??]; naive_solver.
Qed.
(** Functor *)
Lemma list_fmap_ext_ne {A} {B : ofeT} (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, Forall_true. Qed.
Instance list_fmap_ne {A B : ofeT} (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.
Definition listO_map {A B} (f : A -n> B) : listO A -n> listO B :=
OfeMor (fmap f : listO A listO B).
Instance listO_map_ne A B : NonExpansive (@listO_map A B).
......
This diff is collapsed.
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