Commit 0d471f47 authored by Ralf Jung's avatar Ralf Jung

show lemma about big_sepL and zip_with

parent 1c9e8581
Pipeline #3447 passed with stage
in 10 minutes and 55 seconds
......@@ -312,6 +312,34 @@ Section list.
Proof. rewrite /big_opL. apply _. Qed.
End list.
Section list2.
Context {A : Type}.
Implicit Types l : list A.
Implicit Types Φ Ψ : nat A uPred M.
(* Some lemmas depend on the generalized versions of the above ones. *)
Lemma big_sepL_zip_with {B C} Φ f (l1 : list B) (l2 : list C) :
([ list] kx zip_with f l1 l2, Φ k x) ⊣⊢ ([ list] kx l1, y, l2 !! k = Some y Φ k (f x y)).
Proof.
revert Φ l2; induction l1; intros Φ l2; first by rewrite /= big_sepL_nil.
destruct l2; simpl.
{ rewrite big_sepL_nil. apply (anti_symm _); last exact: True_intro.
(* TODO: Can this be done simpler? *)
rewrite -(big_sepL_mono (λ _ _, True%I)).
- rewrite big_sepL_forall. apply forall_intro=>k. apply forall_intro=>b.
apply impl_intro_r. apply True_intro.
- intros k b _. apply forall_intro=>c. apply impl_intro_l. rewrite right_id.
apply pure_elim'. done.
}
rewrite !big_sepL_cons. apply sep_proper; last exact: IHl1.
apply (anti_symm _).
- apply forall_intro=>c'. simpl. apply impl_intro_r.
eapply pure_elim; first exact: and_elim_r. intros [=->].
apply and_elim_l.
- rewrite (forall_elim c). simpl. eapply impl_elim; first done.
apply pure_intro. done.
Qed.
End list2.
(** ** Big ops over finite maps *)
Section gmap.
......
......@@ -64,7 +64,7 @@ Lemma wp_bind {E e} K Φ :
WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} WP fill K e @ E {{ Φ }}.
Proof. exact: wp_ectx_bind. Qed.
Lemma wp_bind_ctxi {E e} Ki Φ :
Lemma wp_bindi {E e} Ki Φ :
WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }}
WP fill_item Ki e @ E {{ Φ }}.
Proof. exact: weakestpre.wp_bind. Qed.
......
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