Commit b9447cc1 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'set_unfold_list_bind' into 'master'

Add set_unfold_list_bind (+ test)

See merge request iris/stdpp!366
parents ebfb79dd 221197c4
......@@ -2,3 +2,8 @@ From stdpp Require Import sets.
Lemma foo `{Set_ A C} (x : A) (X Y : C) : x X Y x X.
Proof. intros Hx. set_unfold in Hx. tauto. Qed.
(** Test [set_unfold_list_bind]. *)
Lemma elem_of_list_bind_again {A B} (x : B) (l : list A) f :
x l = f y, x f y y l.
Proof. set_solver. Qed.
......@@ -308,6 +308,10 @@ Section set_unfold_list.
SetUnfoldElemOf x l P SetUnfoldElemOf x (rotate n l) P.
Proof. constructor. by rewrite elem_of_rotate, (set_unfold_elem_of x l P). Qed.
Global Instance set_unfold_list_bind {B} (f : A list B) l P Q y :
( x, SetUnfoldElemOf x l (P x)) ( x, SetUnfoldElemOf y (f x) (Q x))
SetUnfoldElemOf y (l = f) ( x, Q x P x).
Proof. constructor. rewrite elem_of_list_bind. naive_solver. Qed.
End set_unfold_list.
Tactic Notation "set_unfold" :=
Supports Markdown
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