Commit 3f3ca628 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Update to match the article.

The development now corresponds exactly to the FoSSaCS 2013 paper.
Also, the prelude is updated to the one of the master branch.
parent 4cda26dd
...@@ -4,6 +4,7 @@ ...@@ -4,6 +4,7 @@
These are particularly useful as we define the operational semantics as a These are particularly useful as we define the operational semantics as a
small step semantics. This file defines a hint database [ars] containing small step semantics. This file defines a hint database [ars] containing
some theorems on abstract rewriting systems. *) some theorems on abstract rewriting systems. *)
Require Import Wf_nat.
Require Export tactics base. Require Export tactics base.
(** * Definitions *) (** * Definitions *)
...@@ -47,13 +48,13 @@ Hint Constructors rtc nsteps bsteps tc : ars. ...@@ -47,13 +48,13 @@ Hint Constructors rtc nsteps bsteps tc : ars.
Section rtc. Section rtc.
Context `{R : relation A}. Context `{R : relation A}.
Global Instance: Reflexive (rtc R). Global Instance rtc_reflexive: Reflexive (rtc R).
Proof rtc_refl R. Proof. red. apply rtc_refl. Qed.
Global Instance rtc_trans: Transitive (rtc R). Global Instance rtc_transitive: Transitive (rtc R).
Proof. red; induction 1; eauto with ars. Qed. Proof. red. induction 1; eauto with ars. Qed.
Lemma rtc_once x y : R x y rtc R x y. Lemma rtc_once x y : R x y rtc R x y.
Proof. eauto with ars. Qed. Proof. eauto with ars. Qed.
Global Instance: subrelation R (rtc R). Instance rtc_once_subrel: subrelation R (rtc R).
Proof. exact @rtc_once. Qed. Proof. exact @rtc_once. Qed.
Lemma rtc_r x y z : rtc R x y R y z rtc R x z. Lemma rtc_r x y z : rtc R x y R y z rtc R x z.
Proof. intros. etransitivity; eauto with ars. Qed. Proof. intros. etransitivity; eauto with ars. Qed.
...@@ -62,8 +63,9 @@ Section rtc. ...@@ -62,8 +63,9 @@ Section rtc.
Proof. inversion_clear 1; eauto. Qed. Proof. inversion_clear 1; eauto. Qed.
Lemma rtc_ind_r (P : A A Prop) Lemma rtc_ind_r (P : A A Prop)
(Prefl : x, P x x) (Pstep : x y z, rtc R x y R y z P x y P x z) : (Prefl : x, P x x)
y z, rtc R y z P y z. (Pstep : x y z, rtc R x y R y z P x y P x z) :
x z, rtc R x z P x z.
Proof. Proof.
cut ( y z, rtc R y z x, rtc R x y P x y P x z). cut ( y z, rtc R y z x, rtc R x y P x y P x z).
{ eauto using rtc_refl. } { eauto using rtc_refl. }
...@@ -99,7 +101,7 @@ Section rtc. ...@@ -99,7 +101,7 @@ Section rtc.
bsteps R n x y bsteps R (m + n) x y. bsteps R n x y bsteps R (m + n) x y.
Proof. apply bsteps_weaken. auto with arith. Qed. Proof. apply bsteps_weaken. auto with arith. Qed.
Lemma bsteps_S n x y : bsteps R n x y bsteps R (S n) x y. Lemma bsteps_S n x y : bsteps R n x y bsteps R (S n) x y.
Proof. apply bsteps_weaken. auto with arith. Qed. Proof. apply bsteps_weaken. lia. Qed.
Lemma bsteps_trans n m x y z : Lemma bsteps_trans n m x y z :
bsteps R n x y bsteps R m y z bsteps R (n + m) x z. bsteps R n x y bsteps R m y z bsteps R (n + m) x z.
Proof. induction 1; simpl; eauto using bsteps_plus_l with ars. Qed. Proof. induction 1; simpl; eauto using bsteps_plus_l with ars. Qed.
...@@ -108,7 +110,31 @@ Section rtc. ...@@ -108,7 +110,31 @@ Section rtc.
Lemma bsteps_rtc n x y : bsteps R n x y rtc R x y. Lemma bsteps_rtc n x y : bsteps R n x y rtc R x y.
Proof. induction 1; eauto with ars. Qed. Proof. induction 1; eauto with ars. Qed.
Lemma rtc_bsteps x y : rtc R x y n, bsteps R n x y. Lemma rtc_bsteps x y : rtc R x y n, bsteps R n x y.
Proof. induction 1. exists 0. auto with ars. firstorder eauto with ars. Qed. Proof.
induction 1.
* exists 0. constructor.
* naive_solver eauto with ars.
Qed.
Lemma bsteps_ind_r (P : nat A Prop) (x : A)
(Prefl : n, P n x)
(Pstep : n y z, bsteps R n x y R y z P n y P (S n) z) :
n z, bsteps R n x z P n z.
Proof.
cut ( m y z, bsteps R m y z n,
bsteps R n x y
( m', n m' m' n + m P m' y)
P (n + m) z).
{ intros help ?. change n with (0 + n). eauto with ars. }
induction 1 as [|m x' y z p2 p3 IH]; [by eauto with arith|].
intros n p1 H. rewrite <-plus_n_Sm.
apply (IH (S n)); [by eauto using bsteps_r |].
intros [|m'] [??]; [lia |].
apply Pstep with x'.
* apply bsteps_weaken with n; intuition lia.
* done.
* apply H; intuition lia.
Qed.
Global Instance tc_trans: Transitive (tc R). Global Instance tc_trans: Transitive (tc R).
Proof. red; induction 1; eauto with ars. Qed. Proof. red; induction 1; eauto with ars. Qed.
...@@ -116,7 +142,7 @@ Section rtc. ...@@ -116,7 +142,7 @@ Section rtc.
Proof. intros. etransitivity; eauto with ars. Qed. Proof. intros. etransitivity; eauto with ars. Qed.
Lemma tc_rtc x y : tc R x y rtc R x y. Lemma tc_rtc x y : tc R x y rtc R x y.
Proof. induction 1; eauto with ars. Qed. Proof. induction 1; eauto with ars. Qed.
Global Instance: subrelation (tc R) (rtc R). Instance tc_once_subrel: subrelation (tc R) (rtc R).
Proof. exact @tc_rtc. Qed. Proof. exact @tc_rtc. Qed.
Lemma looping_red x : looping R x red R x. Lemma looping_red x : looping R x red R x.
...@@ -137,23 +163,73 @@ Section rtc. ...@@ -137,23 +163,73 @@ Section rtc.
Qed. Qed.
End rtc. End rtc.
Hint Resolve rtc_once rtc_r tc_r : ars. (* Avoid too eager type class resolution *)
Hint Extern 5 (subrelation _ (rtc _)) =>
eapply @rtc_once_subrel : typeclass_instances.
Hint Extern 5 (subrelation _ (tc _)) =>
eapply @tc_once_subrel : typeclass_instances.
Hint Resolve
rtc_once rtc_r
tc_r
bsteps_once bsteps_r bsteps_refl bsteps_trans : ars.
(** * Theorems on sub relations *) (** * Theorems on sub relations *)
Section subrel. Section subrel.
Context {A} (R1 R2 : relation A) (Hsub : subrelation R1 R2). Context {A} (R1 R2 : relation A) (Hsub : subrelation R1 R2).
Lemma red_subrel x : red R1 x red R2 x. Lemma red_subrel x : red R1 x red R2 x.
Proof. intros [y ?]. exists y. now apply Hsub. Qed. Proof. intros [y ?]. exists y. by apply Hsub. Qed.
Lemma nf_subrel x : nf R2 x nf R1 x. Lemma nf_subrel x : nf R2 x nf R1 x.
Proof. intros H1 H2. destruct H1. now apply red_subrel. Qed. Proof. intros H1 H2. destruct H1. by apply red_subrel. Qed.
Global Instance rtc_subrel: subrelation (rtc R1) (rtc R2). Instance rtc_subrel: subrelation (rtc R1) (rtc R2).
Proof. induction 1; [left|eright]; eauto; now apply Hsub. Qed. Proof. induction 1; [left|eright]; eauto; by apply Hsub. Qed.
Global Instance nsteps_subrel: subrelation (nsteps R1 n) (nsteps R2 n). Instance nsteps_subrel: subrelation (nsteps R1 n) (nsteps R2 n).
Proof. induction 1; [left|eright]; eauto; now apply Hsub. Qed. Proof. induction 1; [left|eright]; eauto; by apply Hsub. Qed.
Global Instance bsteps_subrel: subrelation (bsteps R1 n) (bsteps R2 n). Instance bsteps_subrel: subrelation (bsteps R1 n) (bsteps R2 n).
Proof. induction 1; [left|eright]; eauto; now apply Hsub. Qed. Proof. induction 1; [left|eright]; eauto; by apply Hsub. Qed.
Global Instance tc_subrel: subrelation (tc R1) (tc R2). Instance tc_subrel: subrelation (tc R1) (tc R2).
Proof. induction 1; [left|eright]; eauto; now apply Hsub. Qed. Proof. induction 1; [left|eright]; eauto; by apply Hsub. Qed.
End subrel. End subrel.
Hint Extern 5 (subrelation (rtc _) (rtc _)) =>
eapply @rtc_subrel : typeclass_instances.
Hint Extern 5 (subrelation (nsteps _) (nsteps _)) =>
eapply @nsteps_subrel : typeclass_instances.
Hint Extern 5 (subrelation (bsteps _) (bsteps _)) =>
eapply @bsteps_subrel : typeclass_instances.
Hint Extern 5 (subrelation (tc _) (tc _)) =>
eapply @tc_subrel : typeclass_instances.
Notation wf := well_founded.
Section wf.
Context `{R : relation A}.
(** A trick by Thomas Braibant to compute with well-founded recursions:
it lazily adds [2^n] [Acc_intro] constructors in front of a well foundedness
proof, so that the actual proof is never reached in practise. *)
Fixpoint wf_guard (n : nat) (wfR : wf R) : wf R :=
match n with
| 0 => wfR
| S n => λ x, Acc_intro x (λ y _, wf_guard n (wf_guard n wfR) y)
end.
Lemma wf_projected `(R2 : relation B) (f : A B) :
( x y, R x y R2 (f x) (f y))
wf R2 wf R.
Proof.
intros Hf Hwf.
cut ( y, Acc R2 y x, y = f x Acc R x).
{ intros aux x. apply (aux (f x)); auto. }
induction 1 as [y _ IH]. intros x ?. subst.
constructor. intros. apply (IH (f y)); auto.
Qed.
End wf.
(* Generally we do not want [wf_guard] to be expanded (neither by tactics,
nor by conversion tests in the kernel), but in some cases we do need it for
computation (that is, we cannot make it opaque). We use the [Strategy]
command to make its expanding behavior less eager. *)
Strategy 100 [wf_guard].
This diff is collapsed.
...@@ -6,91 +6,116 @@ collections. *) ...@@ -6,91 +6,116 @@ collections. *)
Require Export base tactics orders. Require Export base tactics orders.
(** * Theorems *) (** * Theorems *)
Section collection. Section simple_collection.
Context `{Collection A B}. Context `{SimpleCollection A C}.
Lemma elem_of_empty x : x False. Lemma elem_of_empty x : x False.
Proof. split. apply not_elem_of_empty. easy. Qed. Proof. split. apply not_elem_of_empty. done. Qed.
Lemma elem_of_union_l x X Y : x X x X Y. Lemma elem_of_union_l x X Y : x X x X Y.
Proof. intros. apply elem_of_union. auto. Qed. Proof. intros. apply elem_of_union. auto. Qed.
Lemma elem_of_union_r x X Y : x Y x X Y. Lemma elem_of_union_r x X Y : x Y x X Y.
Proof. intros. apply elem_of_union. auto. Qed. Proof. intros. apply elem_of_union. auto. Qed.
Lemma not_elem_of_singleton x y : x {[ y ]} x y.
Proof. now rewrite elem_of_singleton. Qed.
Lemma not_elem_of_union x X Y : x X Y x X x Y.
Proof. rewrite elem_of_union. tauto. Qed.
Global Instance collection_subseteq: SubsetEq B := λ X Y, Global Instance collection_subseteq: SubsetEq C := λ X Y,
x, x X x Y. x, x X x Y.
Global Instance: BoundedJoinSemiLattice B. Global Instance: BoundedJoinSemiLattice C.
Proof. firstorder. Qed. Proof. firstorder auto. Qed.
Global Instance: MeetSemiLattice B.
Proof. firstorder. Qed.
Lemma elem_of_subseteq X Y : X Y x, x X x Y. Lemma elem_of_subseteq X Y : X Y x, x X x Y.
Proof. easy. Qed. Proof. done. Qed.
Lemma elem_of_equiv X Y : X Y x, x X x Y. Lemma elem_of_equiv X Y : X Y x, x X x Y.
Proof. firstorder. Qed. Proof. firstorder. Qed.
Lemma elem_of_equiv_alt X Y : Lemma elem_of_equiv_alt X Y :
X Y ( x, x X x Y) ( x, x Y x X). X Y ( x, x X x Y) ( x, x Y x X).
Proof. firstorder. Qed. Proof. firstorder. Qed.
Lemma elem_of_subseteq_singleton x X : x X {[ x ]} X.
Proof.
split.
* intros ??. rewrite elem_of_singleton. intro. by subst.
* intros Ex. by apply (Ex x), elem_of_singleton.
Qed.
Global Instance singleton_proper : Proper ((=) ==> ()) singleton. Global Instance singleton_proper : Proper ((=) ==> ()) singleton.
Proof. repeat intro. now subst. Qed. Proof. repeat intro. by subst. Qed.
Global Instance elem_of_proper: Proper ((=) ==> () ==> iff) (). Global Instance elem_of_proper: Proper ((=) ==> () ==> iff) () | 5.
Proof. intros ???. subst. firstorder. Qed. Proof. intros ???. subst. firstorder. Qed.
Lemma empty_ne_singleton x : {[ x ]}. Lemma elem_of_union_list (Xs : list C) (x : A) :
x Xs X, X Xs x X.
Proof. Proof.
intros [_ E]. apply (elem_of_empty x). split.
apply E. now apply elem_of_singleton. * induction Xs; simpl; intros HXs.
+ by apply elem_of_empty in HXs.
+ setoid_rewrite elem_of_cons.
apply elem_of_union in HXs. naive_solver.
* intros [X []]. induction 1; simpl.
+ by apply elem_of_union_l.
+ intros. apply elem_of_union_r; auto.
Qed. Qed.
End collection.
(** * Theorems about map *) Lemma non_empty_singleton x : {[ x ]} .
Section map. Proof. intros [E _]. by apply (elem_of_empty x), E, elem_of_singleton. Qed.
Context `{Collection A C}.
Lemma elem_of_map_1 (f : A A) (X : C) (x : A) : Lemma not_elem_of_singleton x y : x {[ y ]} x y.
x X f x map f X. Proof. by rewrite elem_of_singleton. Qed.
Proof. intros. apply (elem_of_map _). eauto. Qed. Lemma not_elem_of_union x X Y : x X Y x X x Y.
Lemma elem_of_map_1_alt (f : A A) (X : C) (x : A) y : Proof. rewrite elem_of_union. tauto. Qed.
x X y = f x y map f X.
Proof. intros. apply (elem_of_map _). eauto. Qed. Context `{ X Y : C, Decision (X Y)}.
Lemma elem_of_map_2 (f : A A) (X : C) (x : A) :
x map f X y, x = f y y X. Global Instance elem_of_dec_slow (x : A) (X : C) : Decision (x X) | 100.
Proof. intros. now apply (elem_of_map _). Qed. Proof.
End map. refine (cast_if (decide_rel () {[ x ]} X));
by rewrite elem_of_subseteq_singleton.
Defined.
End simple_collection.
Ltac decompose_empty := repeat
match goal with
| H : _ _ |- _ => apply empty_union in H; destruct H
| H : _ _ |- _ => apply non_empty_union in H; destruct H
| H : {[ _ ]} |- _ => destruct (non_empty_singleton _ H)
end.
(** * Tactics *) (** * Tactics *)
(** The first pass consists of eliminating all occurrences of [(∪)], [(∩)], (** The first pass consists of eliminating all occurrences of [(∪)], [(∩)],
[(∖)], [map], [∅], [{[_]}], [(≡)], and [(⊆)], by rewriting these into [(∖)], [map], [∅], [{[_]}], [(≡)], and [(⊆)], by rewriting these into
logically equivalent propositions. For example we rewrite [A → x ∈ X ∪ ∅] into logically equivalent propositions. For example we rewrite [A → x ∈ X ∪ ∅] into
[A → x ∈ X ∨ False]. *) [A → x ∈ X ∨ False]. *)
Ltac unfold_elem_of := repeat Ltac unfold_elem_of :=
match goal with repeat_on_hyps (fun H =>
| H : context [ _ _ ] |- _ => setoid_rewrite elem_of_subseteq in H repeat match type of H with
| H : context [ _ _ ] |- _ => setoid_rewrite elem_of_equiv_alt in H | context [ _ _ ] => setoid_rewrite elem_of_subseteq in H
| H : context [ _ ] |- _ => setoid_rewrite elem_of_empty in H | context [ _ _ ] => setoid_rewrite subset_spec in H
| H : context [ _ {[ _ ]} ] |- _ => setoid_rewrite elem_of_singleton in H | context [ _ _ ] => setoid_rewrite elem_of_equiv_alt in H
| H : context [ _ _ _ ] |- _ => setoid_rewrite elem_of_union in H | context [ _ ] => setoid_rewrite elem_of_empty in H
| H : context [ _ _ _ ] |- _ => setoid_rewrite elem_of_intersection in H | context [ _ {[ _ ]} ] => setoid_rewrite elem_of_singleton in H
| H : context [ _ _ _ ] |- _ => setoid_rewrite elem_of_difference in H | context [ _ _ _ ] => setoid_rewrite elem_of_union in H
| H : context [ _ map _ _ ] |- _ => setoid_rewrite elem_of_map in H | context [ _ _ _ ] => setoid_rewrite elem_of_intersection in H
| context [ _ _ _ ] => setoid_rewrite elem_of_difference in H
| context [ _ _ <$> _ ] => setoid_rewrite elem_of_fmap in H
| context [ _ mret _ ] => setoid_rewrite elem_of_ret in H
| context [ _ _ = _ ] => setoid_rewrite elem_of_bind in H
| context [ _ mjoin _ ] => setoid_rewrite elem_of_join in H
end);
repeat match goal with
| |- context [ _ _ ] => setoid_rewrite elem_of_subseteq | |- context [ _ _ ] => setoid_rewrite elem_of_subseteq
| |- context [ _ _ ] => setoid_rewrite subset_spec
| |- context [ _ _ ] => setoid_rewrite elem_of_equiv_alt | |- context [ _ _ ] => setoid_rewrite elem_of_equiv_alt
| |- context [ _ ] => setoid_rewrite elem_of_empty | |- context [ _ ] => setoid_rewrite elem_of_empty
| |- context [ _ {[ _ ]} ] => setoid_rewrite elem_of_singleton | |- context [ _ {[ _ ]} ] => setoid_rewrite elem_of_singleton
| |- context [ _ _ _ ] => setoid_rewrite elem_of_union | |- context [ _ _ _ ] => setoid_rewrite elem_of_union
| |- context [ _ _ _ ] => setoid_rewrite elem_of_intersection | |- context [ _ _ _ ] => setoid_rewrite elem_of_intersection
| |- context [ _ _ _ ] => setoid_rewrite elem_of_difference | |- context [ _ _ _ ] => setoid_rewrite elem_of_difference
| |- context [ _ map _ _ ] => setoid_rewrite elem_of_map | |- context [ _ _ <$> _ ] => setoid_rewrite elem_of_fmap
| |- context [ _ mret _ ] => setoid_rewrite elem_of_ret
| |- context [ _ _ = _ ] => setoid_rewrite elem_of_bind
| |- context [ _ mjoin _ ] => setoid_rewrite elem_of_join
end. end.
(** The tactic [solve_elem_of tac] composes the above tactic with [intuition]. (** The tactic [solve_elem_of tac] composes the above tactic with [intuition].
For goals that do not involve [≡], [⊆], [map], or quantifiers this tactic is For goals that do not involve [≡], [⊆], [map], or quantifiers this tactic is
generally powerful enough. This tactic either fails or proves the goal. *) generally powerful enough. This tactic either fails or proves the goal. *)
Tactic Notation "solve_elem_of" tactic(tac) := Tactic Notation "solve_elem_of" tactic3(tac) :=
simpl in *; simpl in *;
unfold_elem_of; unfold_elem_of;
solve [intuition (simplify_equality; tac)]. solve [intuition (simplify_equality; tac)].
...@@ -101,19 +126,20 @@ Tactic Notation "solve_elem_of" := solve_elem_of auto. ...@@ -101,19 +126,20 @@ Tactic Notation "solve_elem_of" := solve_elem_of auto.
fails or loops on very small goals generated by [solve_elem_of] already. We fails or loops on very small goals generated by [solve_elem_of] already. We
use the [naive_solver] tactic as a substitute. This tactic either fails or use the [naive_solver] tactic as a substitute. This tactic either fails or
proves the goal. *) proves the goal. *)
Tactic Notation "esolve_elem_of" tactic(tac) := Tactic Notation "esolve_elem_of" tactic3(tac) :=
simpl in *; simpl in *;
unfold_elem_of; unfold_elem_of;
naive_solver tac. naive_solver tac.
Tactic Notation "esolve_elem_of" := esolve_elem_of eauto. Tactic Notation "esolve_elem_of" := esolve_elem_of eauto.
(** Given an assumption [H : _ ∈ _], the tactic [destruct_elem_of H] will (** Given a hypothesis [H : _ ∈ _], the tactic [destruct_elem_of H] will
recursively split [H] for [(∪)], [(∩)], [(∖)], [map], [∅], [{[_]}]. *) recursively split [H] for [(∪)], [(∩)], [(∖)], [map], [∅], [{[_]}]. *)
Tactic Notation "destruct_elem_of" hyp(H) := Tactic Notation "decompose_elem_of" hyp(H) :=
let rec go H := let rec go H :=
lazymatch type of H with lazymatch type of H with
| _ => apply elem_of_empty in H; destruct H | _ => apply elem_of_empty in H; destruct H
| _ {[ ?l' ]} => apply elem_of_singleton in H; subst l' | ?x {[ ?y ]} =>
apply elem_of_singleton in H; try first [subst y | subst x]
| _ _ _ => | _ _ _ =>
let H1 := fresh in let H2 := fresh in apply elem_of_union in H; let H1 := fresh in let H2 := fresh in apply elem_of_union in H;
destruct H as [H1|H2]; [go H1 | go H2] destruct H as [H1|H2]; [go H1 | go H2]
...@@ -123,21 +149,104 @@ Tactic Notation "destruct_elem_of" hyp(H) := ...@@ -123,21 +149,104 @@ Tactic Notation "destruct_elem_of" hyp(H) :=
| _ _ _ => | _ _ _ =>
let H1 := fresh in let H2 := fresh in apply elem_of_difference in H; let H1 := fresh in let H2 := fresh in apply elem_of_difference in H;
destruct H as [H1 H2]; go H1; go H2 destruct H as [H1 H2]; go H1; go H2
| _ map _ _ => | ?x _ <$> _ =>
let H1 := fresh in apply elem_of_map in H; let H1 := fresh in apply elem_of_fmap in H;
destruct H as [?[? H1]]; go H1 destruct H as [? [? H1]]; try (subst x); go H1
| _ _ = _ =>
let H1 := fresh in let H2 := fresh in apply elem_of_bind in H;
destruct H as [? [H1 H2]]; go H1; go H2
| ?x mret ?y =>
apply elem_of_ret in H; try first [subst y | subst x]
| _ mjoin _ = _ =>
let H1 := fresh in let H2 := fresh in apply elem_of_join in H;
destruct H as [? [H1 H2]]; go H1; go H2
| _ => idtac | _ => idtac
end in go H. end in go H.
Tactic Notation "decompose_elem_of" :=
repeat_on_hyps (fun H => decompose_elem_of H).
Section collection.
Context `{Collection A C}.
Global Instance: LowerBoundedLattice C.
Proof. split. apply _. firstorder auto. Qed.
Lemma intersection_singletons x : {[x]} {[x]} {[x]}.
Proof. esolve_elem_of. Qed.
Lemma difference_twice X Y : (X Y) Y X Y.
Proof. esolve_elem_of. Qed.
Lemma empty_difference X Y : X Y X Y .
Proof. esolve_elem_of. Qed.
Lemma difference_diag X : X X .
Proof. esolve_elem_of. Qed.
Lemma difference_union_distr_l X Y Z : (X Y) Z X Z Y Z.
Proof. esolve_elem_of. Qed.
Lemma difference_intersection_distr_l X Y Z : (X Y) Z X Z Y Z.
Proof. esolve_elem_of. Qed.
Lemma elem_of_intersection_with_list (f : A A option A) Xs Y x :
x intersection_with_list f Y Xs xs y,
Forall2 () xs Xs y Y foldr (λ x, (= f x)) (Some y) xs = Some x.
Proof.
split.
* revert x. induction Xs; simpl; intros x HXs.
+ eexists [], x. intuition.
+ rewrite elem_of_intersection_with in HXs.
destruct HXs as (x1 & x2 & Hx1 & Hx2 & ?).
destruct (IHXs x2) as (xs & y & hy & ? & ?); trivial.
eexists (x1 :: xs), y. intuition (simplify_option_equality; auto).
* intros (xs & y & Hxs & ? & Hx). revert x Hx.
induction Hxs; intros; simplify_option_equality; [done |].
rewrite elem_of_intersection_with. naive_solver.
Qed.
Lemma intersection_with_list_ind (P Q : A Prop) f Xs Y :
( y, y Y P y)
Forall (λ X, x, x X Q x) Xs
( x y z, Q x P y f x y = Some z P z)
x, x intersection_with_list f Y Xs P x.
Proof.
intros HY HXs Hf.
induction Xs; simplify_option_equality; [done |].
intros x Hx. rewrite elem_of_intersection_with in Hx.
decompose_Forall. destruct Hx as (? & ? & ? & ? & ?). eauto.
Qed.
Context `{ X Y : C, Decision (X Y)}.
Lemma not_elem_of_intersection x X Y : x X Y x X x Y.
Proof.
rewrite elem_of_intersection.
destruct (decide (x X)); tauto.
Qed.
Lemma not_elem_of_difference x X Y : x X Y x X x Y.
Proof.
rewrite elem_of_difference.
destruct (decide (x Y)); tauto.
Qed.
Lemma union_difference X Y : X Y Y X Y X.
Proof.
split; intros x; rewrite !elem_of_union, elem_of_difference.