Commit 2db8a61c authored by Robbert Krebbers's avatar Robbert Krebbers

Stronger version of map_fold_insert.

parent ad0bfc51
......@@ -928,15 +928,23 @@ Proof. unfold map_fold; simpl. by rewrite map_to_list_empty. Qed.
Lemma map_fold_insert {A B} (R : relation B) `{!PreOrder R}
(f : K A B B) (b : B) (i : K) (x : A) (m : M A) :
( j z, Proper (R ==> R) (f j z))
( j1 j2 z1 z2 y, R (f j1 z1 (f j2 z2 y)) (f j2 z2 (f j1 z1 y)))
( j1 j2 z1 z2 y,
j1 j2 <[i:=x]> m !! j1 = Some z1 <[i:=x]> m !! j2 = Some z2
R (f j1 z1 (f j2 z2 y)) (f j2 z2 (f j1 z1 y)))
m !! i = None
R (map_fold f b (<[i:=x]> m)) (f i x (map_fold f b m)).
Proof.
intros. unfold map_fold; simpl.
intros Hf_proper Hf Hi. unfold map_fold; simpl.
assert ( kz, Proper (R ==> R) (curry f kz)) by (intros []; apply _).
trans (foldr (curry f) b ((i, x) :: map_to_list m)); [|done].
eapply (foldr_permutation R (curry f) b), map_to_list_insert; auto.
intros [] []; simpl; eauto.
intros j1 [k1 y1] j2 [k2 y2] c Hj Hj1 Hj2. apply Hf.
- intros ->.
eapply Hj, NoDup_lookup; [apply (NoDup_fst_map_to_list (<[i:=x]> m))| | ].
+ by rewrite list_lookup_fmap, Hj1.
+ by rewrite list_lookup_fmap, Hj2.
- by eapply elem_of_map_to_list, elem_of_list_lookup_2.
- by eapply elem_of_map_to_list, elem_of_list_lookup_2.
Qed.
Lemma map_fold_ind {A B} (P : B M A Prop) (f : K A B B) (b : B) :
......
......@@ -3259,10 +3259,26 @@ Lemma foldl_app {A B} (f : A → B → A) (l k : list B) (a : A) :
foldl f a (l ++ k) = foldl f (foldl f a l) k.
Proof. revert a. induction l; simpl; auto. Qed.
Lemma foldr_permutation {A B} (R : relation B) `{!PreOrder R}
(f : A B B) (b : B) `{Hf : ! x, Proper (R ==> R) (f x)} (l1 l2 : list A) :
( j1 a1 j2 a2 b,
j1 j2 l1 !! j1 = Some a1 l1 !! j2 = Some a2
R (f a1 (f a2 b)) (f a2 (f a1 b)))
l1 l2 R (foldr f b l1) (foldr f b l2).
Proof.
intros Hf'. induction 1 as [|x l1 l2 _ IH|x y l|l1 l2 l3 Hl12 IH _ IH']; simpl.
- done.
- apply Hf, IH; eauto.
- apply (Hf' 0 _ 1); eauto.
- etrans; [eapply IH, Hf'|].
apply IH'; intros j1 a1 j2 a2 b' ???.
symmetry in Hl12; apply Permutation_inj in Hl12 as [_ (g&?&Hg)].
apply (Hf' (g j1) _ (g j2)); [naive_solver|by rewrite <-Hg..].
Qed.
Lemma foldr_permutation_proper {A B} (R : relation B) `{!PreOrder R}
(f : A B B) (b : B) `{! x, Proper (R ==> R) (f x)}
(Hf : a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
Proper (() ==> R) (foldr f b).
Proof. induction 1; simpl; [done|by f_equiv|apply Hf|etrans; eauto]. Qed.
Proof. intros l1 l2 Hl. apply foldr_permutation; auto. Qed.
(** ** Properties of the [zip_with] and [zip] functions *)
Section zip_with.
......
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