Commit 9d497b89 authored by Robbert Krebbers's avatar Robbert Krebbers

Let set_solver handle mkSet.

parent 6c6ef520
......@@ -4,6 +4,7 @@
importantly, it implements some tactics to automatically solve goals involving
collections. *)
From stdpp Require Export base tactics orders.
From stdpp Require Import sets.
Instance collection_subseteq `{ElemOf A C} : SubsetEq C := λ X Y,
x, x X x Y.
......@@ -153,6 +154,9 @@ Tactic Notation "decompose_elem_of" hyp(H) :=
let rec go H :=
lazymatch type of H with
| _ => apply elem_of_empty in H; destruct H
| _ => clear H
| _ {[ _ | _ ]} => rewrite elem_of_mkSet in H
| ¬_ {[ _ | _ ]} => rewrite not_elem_of_mkSet in H
| ?x {[ ?y ]} =>
apply elem_of_singleton in H; try first [subst y | subst x]
| ?x {[ ?y ]} =>
......@@ -217,7 +221,9 @@ Ltac set_unfold :=
| context [ _ = ] => setoid_rewrite elem_of_equiv_empty_L in H
| context [ _ = _ ] => setoid_rewrite elem_of_equiv_alt_L in H
| context [ _ ] => setoid_rewrite elem_of_empty in H
| context [ _ ] => setoid_rewrite elem_of_all in H
| context [ _ {[ _ ]} ] => setoid_rewrite elem_of_singleton in H
| context [ _ {[_| _ ]} ] => setoid_rewrite elem_of_mkSet in H; simpl in H
| context [ _ _ _ ] => setoid_rewrite elem_of_union in H
| context [ _ _ _ ] => setoid_rewrite elem_of_intersection in H
| context [ _ _ _ ] => setoid_rewrite elem_of_difference in H
......@@ -237,7 +243,9 @@ Ltac set_unfold :=
| |- context [ _ = ] => setoid_rewrite elem_of_equiv_empty_L
| |- context [ _ = _ ] => setoid_rewrite elem_of_equiv_alt_L
| |- context [ _ ] => setoid_rewrite elem_of_empty
| |- context [ _ ] => setoid_rewrite elem_of_all
| |- context [ _ {[ _ ]} ] => setoid_rewrite elem_of_singleton
| |- context [ _ {[ _ | _ ]} ] => setoid_rewrite elem_of_mkSet; simpl
| |- context [ _ _ _ ] => setoid_rewrite elem_of_union
| |- context [ _ _ _ ] => setoid_rewrite elem_of_intersection
| |- context [ _ _ _ ] => setoid_rewrite elem_of_difference
......
......@@ -23,9 +23,11 @@ Instance set_difference {A} : Difference (set A) := λ X1 X2,
Instance set_collection : Collection A (set A).
Proof. split; [split | |]; by repeat intro. Qed.
Lemma elem_of_mkSet {A} (P : A Prop) x : (x {[ x | P x ]}) = P x.
Lemma elem_of_all {A} (x : A) : x True.
Proof. done. Qed.
Lemma not_elem_of_mkSet {A} (P : A Prop) x : (x {[ x | P x ]}) = (¬P x).
Lemma elem_of_mkSet {A} (P : A Prop) x : x {[ x | P x ]} P x.
Proof. done. Qed.
Lemma not_elem_of_mkSet {A} (P : A Prop) x : x {[ x | P x ]} ¬P x.
Proof. done. Qed.
Instance set_ret : MRet set := λ A (x : A), {[ x ]}.
......@@ -38,4 +40,4 @@ Instance set_join : MJoin set := λ A (XX : set (set A)),
Instance set_collection_monad : CollectionMonad set.
Proof. by split; try apply _. Qed.
Global Opaque set_union set_intersection set_difference.
Global Opaque set_elem_of set_union set_intersection set_difference.
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