diff --git a/theories/fin_maps.v b/theories/fin_maps.v index ecb3ef766e5665b61474aa05e38ec15be289bc19..aaed1ad0a216389cb9c2371306a05272f77d5ebf 100644 --- a/theories/fin_maps.v +++ b/theories/fin_maps.v @@ -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) : diff --git a/theories/list.v b/theories/list.v index 4bdc361c729cc46aef1e657fce7a674a94b718c5..50dcc652b12992cd9fb68e1481db1989ce369579 100644 --- a/theories/list.v +++ b/theories/list.v @@ -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.