Skip to content
GitLab
Commit ccfa0a08 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Better SetUnfold.

parent a8e9b673
Hide whitespace changes
Inline Side-by-side
theories/fin_sets.v
View file @ ccfa0a08
......@@ -60,8 +60,8 @@ Defined.
(** * The [elements] operation *)
Global Instance set_unfold_elements X x P :
SetUnfold (x ∈ X) P → SetUnfold (x ∈ elements X) P.
Proof. constructor. by rewrite elem_of_elements, (set_unfold (x ∈ X) P). Qed.
SetUnfoldElemOf x X P → SetUnfoldElemOf x (elements X) P.
Proof. constructor. by rewrite elem_of_elements, (set_unfold_elem_of x X P). Qed.
Global Instance elements_proper: Proper ((≡) ==> (≡ₚ)) (elements (C:=C)).
Proof.
......@@ -278,9 +278,9 @@ Section filter.
by rewrite elem_of_list_to_set, elem_of_list_filter, elem_of_elements.
Qed.
Global Instance set_unfold_filter X Q :
SetUnfold (x ∈ X) Q → SetUnfold (x ∈ filter P X) (P x ∧ Q).
SetUnfoldElemOf x X Q → SetUnfoldElemOf x (filter P X) (P x ∧ Q).
Proof.
intros ??; constructor. by rewrite elem_of_filter, (set_unfold (x ∈ X) Q).
intros ??; constructor. by rewrite elem_of_filter, (set_unfold_elem_of x X Q).
Qed.
Lemma filter_empty : filter P (∅:C) ≡ ∅.
......@@ -316,8 +316,8 @@ Section map.
by setoid_rewrite elem_of_elements.
Qed.
Global Instance set_unfold_map (f : A → B) (X : C) (P : A → Prop) :
(∀ y, SetUnfold (y ∈ X) (P y)) →
SetUnfold (x ∈ set_map (D:=D) f X) (∃ y, x = f y ∧ P y).
(∀ y, SetUnfoldElemOf y X (P y)) →
SetUnfoldElemOf x (set_map (D:=D) f X) (∃ y, x = f y ∧ P y).
Proof. constructor. rewrite elem_of_map; naive_solver. Qed.
Global Instance set_map_proper :
......
theories/gmultiset.v
View file @ ccfa0a08
......@@ -136,10 +136,11 @@ Lemma gmultiset_elem_of_disj_union X Y x : x ∈ X ⊎ Y ↔ x ∈ X ∨ x ∈ Y
Proof. rewrite !elem_of_multiplicity, multiplicity_disj_union. lia. Qed.
Global Instance set_unfold_gmultiset_disj_union x X Y P Q :
SetUnfold (x ∈ X) P → SetUnfold (x ∈ Y) Q → SetUnfold (x ∈ X ⊎ Y) (P ∨ Q).
SetUnfoldElemOf x X P → SetUnfoldElemOf x Y Q →
SetUnfoldElemOf x (X ⊎ Y) (P ∨ Q).
Proof.
intros ??; constructor. rewrite gmultiset_elem_of_disj_union.
by rewrite <-(set_unfold (x ∈ X) P), <-(set_unfold (x ∈ Y) Q).
by rewrite <-(set_unfold_elem_of x X P), <-(set_unfold_elem_of x Y Q).
Qed.
(* Algebraic laws *)
......
theories/propset.v
View file @ ccfa0a08
......@@ -44,10 +44,10 @@ Instance propset_join : MJoin propset := λ A (XX : propset (propset A)),
Instance propset_monad_set : MonadSet propset.
Proof. by split; try apply _. Qed.
Instance set_unfold_propset_top {A} (x : A) : SetUnfold (x ∈ (⊤ : propset A)) True.
Instance set_unfold_propset_top {A} (x : A) : SetUnfoldElemOf x (⊤ : propset A) True.
Proof. by constructor. Qed.
Instance set_unfold_PropSet {A} (P : A → Prop) x Q :
SetUnfoldSimpl (P x) Q → SetUnfold (x ∈ PropSet P) Q.
SetUnfoldSimpl (P x) Q → SetUnfoldElemOf x (PropSet P) Q.
Proof. intros HPQ. constructor. apply HPQ. Qed.
Global Opaque propset_elem_of propset_top propset_empty propset_singleton.
......
theories/sets.v
View file @ ccfa0a08
......@@ -96,6 +96,18 @@ Class SetUnfold (P Q : Prop) := { set_unfold : P ↔ Q }.
Arguments set_unfold _ _ {_} : assert.
Hint Mode SetUnfold + - : typeclass_instances.
Class SetUnfoldElemOf `{ElemOf A C} (x : A) (X : C) (Q : Prop) :=
{ set_unfold_elem_of : x ∈ X ↔ Q }.
Arguments set_unfold_elem_of {_ _ _} _ _ _ {_} : assert.
Hint Mode SetUnfoldElemOf + + + - + - : typeclass_instances.
Instance set_unfold_elem_of_default `{ElemOf A C} (x : A) (X : C) :
SetUnfoldElemOf x X (x ∈ X) | 1000.
Proof. done. Qed.
Instance set_unfold_elem_of_set_unfold `{ElemOf A C} (x : A) (X : C) Q :
SetUnfoldElemOf x X Q → SetUnfold (x ∈ X) Q.
Proof. by destruct 1; constructor. Qed.
Class SetUnfoldSimpl (P Q : Prop) := { set_unfold_simpl : SetUnfold P Q }.
Hint Extern 0 (SetUnfoldSimpl _ _) => csimpl; constructor : typeclass_instances.
......@@ -146,47 +158,49 @@ Section set_unfold_simple.
Implicit Types x y : A.
Implicit Types X Y : C.
Global Instance set_unfold_empty x : SetUnfold (x ∈ (∅ : C)) False.
Global Instance set_unfold_empty x : SetUnfoldElemOf x (∅ : C) False.
Proof. constructor. split. apply not_elem_of_empty. done. Qed.
Global Instance set_unfold_singleton x y : SetUnfold (x ∈ ({[ y ]} : C)) (x = y).
Global Instance set_unfold_singleton x y : SetUnfoldElemOf x ({[ y ]} : C) (x = y).
Proof. constructor; apply elem_of_singleton. Qed.
Global Instance set_unfold_union x X Y P Q :
SetUnfold (x ∈ X) P → SetUnfold (x ∈ Y) Q → SetUnfold (x ∈ X ∪ Y) (P ∨ Q).
SetUnfoldElemOf x X P → SetUnfoldElemOf x Y Q →
SetUnfoldElemOf x (X ∪ Y) (P ∨ Q).
Proof.
intros ??; constructor.
by rewrite elem_of_union, (set_unfold (x ∈ X) P), (set_unfold (x ∈ Y) Q).
by rewrite elem_of_union,
(set_unfold_elem_of x X P), (set_unfold_elem_of x Y Q).
Qed.
Global Instance set_unfold_equiv_same X : SetUnfold (X ≡ X) True | 1.
Proof. done. Qed.
Global Instance set_unfold_equiv_empty_l X (P : A → Prop) :
(∀ x, SetUnfold (x ∈ X) (P x)) → SetUnfold (∅ ≡ X) (∀ x, ¬P x) | 5.
(∀ x, SetUnfoldElemOf x X (P x)) → SetUnfold (∅ ≡ X) (∀ x, ¬P x) | 5.
Proof.
intros ?; constructor. unfold equiv, set_equiv.
pose proof (not_elem_of_empty (C:=C)); naive_solver.
Qed.
Global Instance set_unfold_equiv_empty_r (P : A → Prop) X :
(∀ x, SetUnfold (x ∈ X) (P x)) → SetUnfold (X ≡ ∅) (∀ x, ¬P x) | 5.
(∀ x, SetUnfoldElemOf x X (P x)) → SetUnfold (X ≡ ∅) (∀ x, ¬P x) | 5.
Proof.
intros ?; constructor. unfold equiv, set_equiv.
pose proof (not_elem_of_empty (C:=C)); naive_solver.
Qed.
Global Instance set_unfold_equiv (P Q : A → Prop) X :
(∀ x, SetUnfold (x ∈ X) (P x)) → (∀ x, SetUnfold (x ∈ Y) (Q x)) →
(∀ x, SetUnfoldElemOf x X (P x)) → (∀ x, SetUnfoldElemOf x Y (Q x)) →
SetUnfold (X ≡ Y) (∀ x, P x ↔ Q x) | 10.
Proof. constructor. apply forall_proper; naive_solver. Qed.
Global Instance set_unfold_subseteq (P Q : A → Prop) X Y :
(∀ x, SetUnfold (x ∈ X) (P x)) → (∀ x, SetUnfold (x ∈ Y) (Q x)) →
(∀ x, SetUnfoldElemOf x X (P x)) → (∀ x, SetUnfoldElemOf x Y (Q x)) →
SetUnfold (X ⊆ Y) (∀ x, P x → Q x).
Proof. constructor. apply forall_proper; naive_solver. Qed.
Global Instance set_unfold_subset (P Q : A → Prop) X :
(∀ x, SetUnfold (x ∈ X) (P x)) → (∀ x, SetUnfold (x ∈ Y) (Q x)) →
(∀ x, SetUnfoldElemOf x X (P x)) → (∀ x, SetUnfoldElemOf x Y (Q x)) →
SetUnfold (X ⊂ Y) ((∀ x, P x → Q x) ∧ ¬∀ x, Q x → P x).
Proof.
constructor. unfold strict.
repeat f_equiv; apply forall_proper; naive_solver.
Qed.
Global Instance set_unfold_disjoint (P Q : A → Prop) X Y :
(∀ x, SetUnfold (x ∈ X) (P x)) → (∀ x, SetUnfold (x ∈ Y) (Q x)) →
(∀ x, SetUnfoldElemOf x X (P x)) → (∀ x, SetUnfoldElemOf x Y (Q x)) →
SetUnfold (X ## Y) (∀ x, P x → Q x → False).
Proof. constructor. unfold disjoint, set_disjoint. naive_solver. Qed.
......@@ -194,13 +208,13 @@ Section set_unfold_simple.
Global Instance set_unfold_equiv_same_L X : SetUnfold (X = X) True | 1.
Proof. done. Qed.
Global Instance set_unfold_equiv_empty_l_L X (P : A → Prop) :
(∀ x, SetUnfold (x ∈ X) (P x)) → SetUnfold (∅ = X) (∀ x, ¬P x) | 5.
(∀ x, SetUnfoldElemOf x X (P x)) → SetUnfold (∅ = X) (∀ x, ¬P x) | 5.
Proof. constructor. unfold_leibniz. by apply set_unfold_equiv_empty_l. Qed.
Global Instance set_unfold_equiv_empty_r_L (P : A → Prop) X :
(∀ x, SetUnfold (x ∈ X) (P x)) → SetUnfold (X = ∅) (∀ x, ¬P x) | 5.
(∀ x, SetUnfoldElemOf x X (P x)) → SetUnfold (X = ∅) (∀ x, ¬P x) | 5.
Proof. constructor. unfold_leibniz. by apply set_unfold_equiv_empty_r. Qed.
Global Instance set_unfold_equiv_L (P Q : A → Prop) X Y :
(∀ x, SetUnfold (x ∈ X) (P x)) → (∀ x, SetUnfold (x ∈ Y) (Q x)) →
(∀ x, SetUnfoldElemOf x X (P x)) → (∀ x, SetUnfoldElemOf x Y (Q x)) →
SetUnfold (X = Y) (∀ x, P x ↔ Q x) | 10.
Proof. constructor. unfold_leibniz. by apply set_unfold_equiv. Qed.
End set_unfold_simple.
......@@ -211,16 +225,18 @@ Section set_unfold.
Implicit Types X Y : C.
Global Instance set_unfold_intersection x X Y P Q :
SetUnfold (x ∈ X) P → SetUnfold (x ∈ Y) Q → SetUnfold (x ∈ X ∩ Y) (P ∧ Q).
SetUnfoldElemOf x X P → SetUnfoldElemOf x Y Q →
SetUnfoldElemOf x (X ∩ Y) (P ∧ Q).
Proof.
intros ??; constructor. rewrite elem_of_intersection.
by rewrite (set_unfold (x ∈ X) P), (set_unfold (x ∈ Y) Q).
by rewrite (set_unfold_elem_of x X P), (set_unfold_elem_of x Y Q).
Qed.
Global Instance set_unfold_difference x X Y P Q :
SetUnfold (x ∈ X) P → SetUnfold (x ∈ Y) Q → SetUnfold (x ∈ X ∖ Y) (P ∧ ¬Q).
SetUnfoldElemOf x X P → SetUnfoldElemOf x Y Q →
SetUnfoldElemOf x (X ∖ Y) (P ∧ ¬Q).
Proof.
intros ??; constructor. rewrite elem_of_difference.
by rewrite (set_unfold (x ∈ X) P), (set_unfold (x ∈ Y) Q).
by rewrite (set_unfold_elem_of x X P), (set_unfold_elem_of x Y Q).
Qed.
End set_unfold.
......@@ -228,18 +244,19 @@ Section set_unfold_monad.
Context `{MonadSet M}.
Global Instance set_unfold_ret {A} (x y : A) :
SetUnfold (x ∈ mret (M:=M) y) (x = y).
SetUnfoldElemOf x (mret (M:=M) y) (x = y).
Proof. constructor; apply elem_of_ret. Qed.
Global Instance set_unfold_bind {A B} (f : A → M B) X (P Q : A → Prop) :
(∀ y, SetUnfold (y ∈ X) (P y)) → (∀ y, SetUnfold (x ∈ f y) (Q y)) →
SetUnfold (x ∈ X ≫= f) (∃ y, Q y ∧ P y).
(∀ y, SetUnfoldElemOf y X (P y)) → (∀ y, SetUnfoldElemOf x (f y) (Q y)) →
SetUnfoldElemOf x (X ≫= f) (∃ y, Q y ∧ P y).
Proof. constructor. rewrite elem_of_bind; naive_solver. Qed.
Global Instance set_unfold_fmap {A B} (f : A → B) (X : M A) (P : A → Prop) :
(∀ y, SetUnfold (y ∈ X) (P y)) →
SetUnfold (x ∈ f <$> X) (∃ y, x = f y ∧ P y).
(∀ y, SetUnfoldElemOf y X (P y)) →
SetUnfoldElemOf x (f <$> X) (∃ y, x = f y ∧ P y).
Proof. constructor. rewrite elem_of_fmap; naive_solver. Qed.
Global Instance set_unfold_join {A} (X : M (M A)) (P : M A → Prop) :
(∀ Y, SetUnfold (Y ∈ X) (P Y)) → SetUnfold (x ∈ mjoin X) (∃ Y, x ∈ Y ∧ P Y).
(∀ Y, SetUnfoldElemOf Y X (P Y)) →
SetUnfoldElemOf x (mjoin X) (∃ Y, x ∈ Y ∧ P Y).
Proof. constructor. rewrite elem_of_join; naive_solver. Qed.
End set_unfold_monad.
......@@ -248,19 +265,20 @@ Section set_unfold_list.
Implicit Types x : A.
Implicit Types l : list A.
Global Instance set_unfold_nil x : SetUnfold (x ∈ []) False.
Global Instance set_unfold_nil x : SetUnfoldElemOf x [] False.
Proof. constructor; apply elem_of_nil. Qed.
Global Instance set_unfold_cons x y l P :
SetUnfold (x ∈ l) P → SetUnfold (x ∈ y :: l) (x = y ∨ P).
Proof. constructor. by rewrite elem_of_cons, (set_unfold (x ∈ l) P). Qed.
SetUnfoldElemOf x l P → SetUnfoldElemOf x (y :: l) (x = y ∨ P).
Proof. constructor. by rewrite elem_of_cons, (set_unfold_elem_of x l P). Qed.
Global Instance set_unfold_app x l k P Q :
SetUnfold (x ∈ l) P → SetUnfold (x ∈ k) Q → SetUnfold (x ∈ l ++ k) (P ∨ Q).
SetUnfoldElemOf x l P → SetUnfoldElemOf x k Q →
SetUnfoldElemOf x (l ++ k) (P ∨ Q).
Proof.
intros ??; constructor.
by rewrite elem_of_app, (set_unfold (x ∈ l) P), (set_unfold (x ∈ k) Q).
by rewrite elem_of_app, (set_unfold_elem_of x l P), (set_unfold_elem_of x k Q).
Qed.
Global Instance set_unfold_included l k (P Q : A → Prop) :
(∀ x, SetUnfold (x ∈ l) (P x)) → (∀ x, SetUnfold (x ∈ k) (Q x)) →
(∀ x, SetUnfoldElemOf x l (P x)) → (∀ x, SetUnfoldElemOf x k (Q x)) →
SetUnfold (l ⊆ k) (∀ x, P x → Q x).
Proof.
constructor; unfold subseteq, list_subseteq.
......@@ -768,10 +786,10 @@ Section option_and_list_to_set.
Proof. by rewrite elem_of_list_to_set. Qed.
Global Instance set_unfold_option_to_set (mx : option A) x :
SetUnfold (x ∈ option_to_set (C:=C) mx) (mx = Some x).
SetUnfoldElemOf x (option_to_set (C:=C) mx) (mx = Some x).
Proof. constructor; apply elem_of_option_to_set. Qed.
Global Instance set_unfold_list_to_set (l : list A) x P :
SetUnfold (x ∈ l) P → SetUnfold (x ∈ list_to_set (C:=C) l) P.
SetUnfoldElemOf x l P → SetUnfoldElemOf x (list_to_set (C:=C) l) P.
Proof. constructor. by rewrite elem_of_list_to_set, (set_unfold (x ∈ l) P). Qed.
Lemma list_to_set_nil : list_to_set [] =@{C} ∅.
......@@ -812,7 +830,7 @@ Section set_monad_base.
destruct (decide P); naive_solver.
Qed.
Global Instance set_unfold_guard `{Decision P} {A} (x : A) (X : M A) Q :
SetUnfold (x ∈ X) Q → SetUnfold (x ∈ guard P; X) (P ∧ Q).
SetUnfoldElemOf x X Q → SetUnfoldElemOf x (guard P; X) (P ∧ Q).
Proof. constructor. by rewrite elem_of_guard, (set_unfold (x ∈ X) Q). Qed.
Lemma bind_empty {A B} (f : A → M B) X :
X ≫= f ≡ ∅ ↔ X ≡ ∅ ∨ ∀ x, x ∈ X → f x ≡ ∅.
......@@ -1029,7 +1047,7 @@ Section set_seq.
- rewrite elem_of_union, elem_of_singleton, IH. lia.
Qed.
Global Instance set_unfold_seq start len :
SetUnfold (x ∈ set_seq (C:=C) start len) (start ≤ x < start + len).
SetUnfoldElemOf x (set_seq (C:=C) start len) (start ≤ x < start + len).
Proof. constructor; apply elem_of_set_seq. Qed.
Lemma set_seq_plus_disjoint start len1 len2 :
......
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