Commit 361308c7 authored by Robbert Krebbers's avatar Robbert Krebbers

Lots of refactoring. and new results on permutations and list containment.

The refactoring includes:
* Use infix notations for the various list relations
* More consistent naming
* Put lemmas on one line whenever possible
* Change proofs into one-liners when possible
* Make better use of the "Implicit Types" command
* Improve the order of the list module by placing all definitions at the start,
  then the proofs, and finally the tactics.

Besides, there is some new machinery for proofs by reflection on lists. It is
used for a decision procedure for permutations and list containment.
parent 2783aea9
......@@ -107,17 +107,11 @@ Instance unit_inhabited: Inhabited unit := populate ().
Instance list_inhabited {A} : Inhabited (list A) := populate [].
Instance prod_inhabited {A B} (iA : Inhabited A)
(iB : Inhabited B) : Inhabited (A * B) :=
match iA, iB with
| populate x, populate y => populate (x,y)
end.
match iA, iB with populate x, populate y => populate (x,y) end.
Instance sum_inhabited_l {A B} (iA : Inhabited A) : Inhabited (A + B) :=
match iA with
| populate x => populate (inl x)
end.
match iA with populate x => populate (inl x) end.
Instance sum_inhabited_r {A B} (iB : Inhabited A) : Inhabited (A + B) :=
match iB with
| populate y => populate (inl y)
end.
match iB with populate y => populate (inl y) end.
Instance option_inhabited {A} : Inhabited (option A) := populate None.
(** ** Proof irrelevant types *)
......@@ -187,8 +181,7 @@ Notation "(∪)" := union (only parsing) : C_scope.
Notation "( x ∪)" := (union x) (only parsing) : C_scope.
Notation "(∪ x )" := (λ y, union y x) (only parsing) : C_scope.
Definition union_list `{Empty A}
`{Union A} : list A A := fold_right () .
Definition union_list `{Empty A} `{Union A} : list A A := fold_right () .
Arguments union_list _ _ _ !_ /.
Notation "⋃ l" := (union_list l) (at level 20, format "⋃ l") : C_scope.
......@@ -208,9 +201,14 @@ Notation "(∖ x )" := (λ y, difference y x) (only parsing) : C_scope.
Class Singleton A B := singleton: A B.
Instance: Params (@singleton) 3.
Notation "{[ x ]}" := (singleton x) : C_scope.
Notation "{[ x ]}" := (singleton x) (at level 1) : C_scope.
Notation "{[ x ; y ; .. ; z ]}" :=
(union .. (union (singleton x) (singleton y)) .. (singleton z)) : C_scope.
(union .. (union (singleton x) (singleton y)) .. (singleton z))
(at level 1) : C_scope.
Notation "{[ x , y ]}" := (singleton (x,y))
(at level 1, y at next level) : C_scope.
Notation "{[ x , y , z ]}" := (singleton (x,y,z))
(at level 1, y at next level, z at next level) : C_scope.
Class SubsetEq A := subseteq: A A Prop.
Instance: Params (@subseteq) 2.
......@@ -222,6 +220,8 @@ Notation "X ⊈ Y" := (¬X ⊆ Y) (at level 70) : C_scope.
Notation "(⊈)" := (λ X Y, X Y) (only parsing) : C_scope.
Notation "( X ⊈ )" := (λ Y, X Y) (only parsing) : C_scope.
Notation "( ⊈ X )" := (λ Y, Y X) (only parsing) : C_scope.
Infix "⊆*" := (Forall2 subseteq) (at level 70) : C_scope.
Notation "(⊆*)" := (Forall2 subseteq) (only parsing) : C_scope.
Hint Extern 0 (_ _) => reflexivity.
......@@ -251,43 +251,51 @@ Class Disjoint A := disjoint : A → A → Prop.
Instance: Params (@disjoint) 2.
Infix "⊥" := disjoint (at level 70) : C_scope.
Notation "(⊥)" := disjoint (only parsing) : C_scope.
Notation "( X ⊥)" := (disjoint X) (only parsing) : C_scope.
Notation "(⊥ X )" := (λ Y, disjoint Y X) (only parsing) : C_scope.
Inductive list_disjoint `{Empty A} `{Union A}
`{Disjoint A} : list A Prop :=
| disjoint_nil :
list_disjoint []
| disjoint_cons X Xs :
X Xs
list_disjoint Xs
list_disjoint (X :: Xs).
Lemma list_disjoint_cons_inv `{Empty A} `{Union A} `{Disjoint A} X Xs :
list_disjoint (X :: Xs)
X Xs list_disjoint Xs.
Proof. inversion_clear 1; auto. Qed.
Class Filter A B :=
filter: (P : A Prop) `{ x, Decision (P x)}, B B.
(* Arguments filter {_ _ _} _ {_} !_ / : simpl nomatch. *)
Notation "( X ⊥.)" := (disjoint X) (only parsing) : C_scope.
Notation "(.⊥ X )" := (λ Y, disjoint Y X) (only parsing) : C_scope.
Class DisjointList A := disjoint_list : list A Prop.
Instance: Params (@disjoint_list) 2.
Notation "⊥ l" := (disjoint_list l) (at level 20, format "⊥ l") : C_scope.
Section default_disjoint_list.
Context `{Empty A} `{Union A} `{Disjoint A}.
Inductive default_disjoint_list : DisjointList A :=
| disjoint_nil_2 : []
| disjoint_cons_2 X Xs : X Xs Xs (X :: Xs).
Global Existing Instance default_disjoint_list.
Lemma disjoint_list_nil : @nil A True.
Proof. split; constructor. Qed.
Lemma disjoint_list_cons X Xs : (X :: Xs) X Xs Xs.
Proof. split. inversion_clear 1; auto. intros [??]. constructor; auto. Qed.
End default_disjoint_list.
Class Filter A B := filter: (P : A Prop) `{ x, Decision (P x)}, B B.
(** We define variants of the relations [(≡)] and [(⊆)] that are indexed by
an environment. *)
Class EquivEnv A B := equiv_env : A relation B.
Notation "X ≡@{ E } Y" := (equiv_env E X Y)
(at level 70, format "X ≡@{ E } Y") : C_scope.
Notation "(≡@{ E } )" := (equiv_env E)
(E at level 1, only parsing) : C_scope.
Notation "(≡@{ E } )" := (equiv_env E) (E at level 1, only parsing) : C_scope.
Instance: Params (@equiv_env) 4.
Class SubsetEqEnv A B := subseteq_env : A relation B.
Notation "X ⊆@{ E } Y" := (subseteq_env E X Y)
(at level 70, format "X ⊆@{ E } Y") : C_scope.
Notation "(⊆@{ E } )" := (subseteq_env E)
Instance: Params (@subseteq_env) 4.
Notation "X ⊑@{ E } Y" := (subseteq_env E X Y)
(at level 70, format "X ⊑@{ E } Y") : C_scope.
Notation "(⊑@{ E } )" := (subseteq_env E)
(E at level 1, only parsing) : C_scope.
Notation "X ⊑@{ E }* Y" := (Forall2 (subseteq_env E) X Y)
(at level 70, format "X ⊑@{ E }* Y") : C_scope.
Notation "(⊑@{ E }*)" := (Forall2 (subseteq_env E))
(E at level 1, only parsing) : C_scope.
Instance: Params (@subseteq_env) 4.
Hint Extern 0 (_ @{_} _) => reflexivity.
Hint Extern 0 (_ @{_} _) => reflexivity.
(** ** Monadic operations *)
(** We define operational type classes for the monadic operations bind, join
and fmap. These type classes are defined in a non-standard way by taking the
......@@ -314,16 +322,16 @@ Arguments mret {_ _ _} _.
Class MBindD (M : Type Type) {A B} (f : A M B) := mbind: M A M B.
Notation MBind M := ( {A B} (f : A M B), MBindD M f)%type.
Instance: Params (@mbind) 5.
Arguments mbind {_ _ _} _ {_} !_ / : simpl nomatch.
Arguments mbind {_ _ _} _ {_} !_ /.
Class MJoin (M : Type Type) := mjoin: {A}, M (M A) M A.
Instance: Params (@mjoin) 3.
Arguments mjoin {_ _ _} !_ / : simpl nomatch.
Arguments mjoin {_ _ _} !_ /.
Class FMapD (M : Type Type) {A B} (f : A B) := fmap: M A M B.
Notation FMap M := ( {A B} (f : A B), FMapD M f)%type.
Instance: Params (@fmap) 6.
Arguments fmap {_ _ _} _ {_} !_ / : simpl nomatch.
Arguments fmap {_ _ _} _ {_} !_ /.
Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : C_scope.
Notation "( m ≫=)" := (λ f, mbind f m) (only parsing) : C_scope.
......@@ -331,21 +339,22 @@ Notation "(≫= f )" := (mbind f) (only parsing) : C_scope.
Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : C_scope.
Notation "x ← y ; z" := (y = (λ x : _, z))
(at level 65, only parsing, next at level 35, right associativity) : C_scope.
(at level 65, next at level 35, only parsing, right associativity) : C_scope.
Infix "<$>" := fmap (at level 60, right associativity) : C_scope.
Class MGuard (M : Type Type) :=
mguard: P {dec : Decision P} {A}, M A M A.
Notation "'guard' P ; o" := (mguard P o)
(at level 65, only parsing, next at level 35, right associativity) : C_scope.
Arguments mguard _ _ _ !_ _ !_ / : simpl nomatch.
mguard: P {dec : Decision P} {A}, (P M A) M A.
Arguments mguard _ _ _ !_ _ _ /.
Notation "'guard' P ; o" := (mguard P (λ _, o))
(at level 65, next at level 35, only parsing, right associativity) : C_scope.
Notation "'guard' P 'as' H ; o" := (mguard P (λ H, o))
(at level 65, next at level 35, only parsing, right associativity) : C_scope.
(** ** Operations on maps *)
(** In this section we define operational type classes for the operations
on maps. In the file [fin_maps] we will axiomatize finite maps.
The function look up [m !! k] should yield the element at key [k] in [m]. *)
Class Lookup (K A M : Type) :=
lookup: K M option A.
Class Lookup (K A M : Type) := lookup: K M option A.
Instance: Params (@lookup) 4.
Notation "m !! i" := (lookup i m) (at level 20) : C_scope.
......@@ -356,8 +365,7 @@ Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch.
(** The function insert [<[k:=a]>m] should update the element at key [k] with
value [a] in [m]. *)
Class Insert (K A M : Type) :=
insert: K A M M.
Class Insert (K A M : Type) := insert: K A M M.
Instance: Params (@insert) 4.
Notation "<[ k := a ]>" := (insert k a)
(at level 5, right associativity, format "<[ k := a ]>") : C_scope.
......@@ -366,15 +374,13 @@ Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch.
(** The function delete [delete k m] should delete the value at key [k] in
[m]. If the key [k] is not a member of [m], the original map should be
returned. *)
Class Delete (K M : Type) :=
delete: K M M.
Class Delete (K M : Type) := delete: K M M.
Instance: Params (@delete) 3.
Arguments delete _ _ _ !_ !_ / : simpl nomatch.
(** The function [alter f k m] should update the value at key [k] using the
function [f], which is called with the original value. *)
Class AlterD (K A M : Type) (f : A A) :=
alter: K M M.
Class AlterD (K A M : Type) (f : A A) := alter: K M M.
Notation Alter K A M := ( (f : A A), AlterD K A M f)%type.
Instance: Params (@alter) 5.
Arguments alter {_ _ _} _ {_} !_ !_ / : simpl nomatch.
......@@ -409,9 +415,8 @@ Definition delete_list `{Delete K M} (l : list K) (m : M) : M :=
fold_right delete m l.
Instance: Params (@delete_list) 3.
Definition insert_consecutive `{Insert nat A M}
(i : nat) (l : list A) (m : M) : M :=
fold_right (λ x f i, <[i:=x]>(f (S i))) (λ _, m) l i.
Definition insert_consecutive `{Insert nat A M} (i : nat) (l : list A)
(m : M) : M := fold_right (λ x f i, <[i:=x]>(f (S i))) (λ _, m) l i.
Instance: Params (@insert_consecutive) 3.
(** The function [union_with f m1 m2] is supposed to yield the union of [m1]
......@@ -441,8 +446,11 @@ Arguments intersection_with_list _ _ _ _ _ !_ /.
(** These operational type classes allow us to refer to common mathematical
properties in a generic way. For example, for injectivity of [(k ++)] it
allows us to write [injective (k ++)] instead of [app_inv_head k]. *)
Class Injective {A B} (R : relation A) S (f : A B) : Prop :=
injective: x y : A, S (f x) (f y) R x y.
Class Injective {A B} (R : relation A) (S : relation B) (f : A B) : Prop :=
injective: x y, S (f x) (f y) R x y.
Class Injective2 {A B C} (R1 : relation A) (R2 : relation B)
(S : relation C) (f : A B C) : Prop :=
injective2: x1 x2 y1 y2, S (f x1 x2) (f y1 y2) R1 x1 y1 R2 x2 y2.
Class Idempotent {A} (R : relation A) (f : A A A) : Prop :=
idempotent: x, R (f x x) x.
Class Commutative {A B} (R : relation A) (f : B B A) : Prop :=
......@@ -461,11 +469,12 @@ Class LeftDistr {A} (R : relation A) (f g : A → A → A) : Prop :=
left_distr: x y z, R (f x (g y z)) (g (f x y) (f x z)).
Class RightDistr {A} (R : relation A) (f g : A A A) : Prop :=
right_distr: y z x, R (f (g y z) x) (g (f y x) (f z x)).
Class AntiSymmetric {A} (R : relation A) : Prop :=
anti_symmetric: x y, R x y R y x x = y.
Class AntiSymmetric {A} (R S : relation A) : Prop :=
anti_symmetric: x y, S x y S y x R x y.
Arguments irreflexivity {_} _ {_} _ _.
Arguments injective {_ _ _ _} _ {_} _ _ _.
Arguments injective2 {_ _ _ _ _ _} _ {_} _ _ _ _ _.
Arguments idempotent {_ _} _ {_} _.
Arguments commutative {_ _ _} _ {_} _ _.
Arguments left_id {_ _} _ _ {_} _.
......@@ -475,8 +484,10 @@ Arguments left_absorb {_ _} _ _ {_} _.
Arguments right_absorb {_ _} _ _ {_} _.
Arguments left_distr {_ _} _ _ {_} _ _ _.
Arguments right_distr {_ _} _ _ {_} _ _ _.
Arguments anti_symmetric {_} _ {_} _ _ _ _.
Arguments anti_symmetric {_ _} _ {_} _ _ _ _.
Lemma impl_transitive (P Q R : Prop) : (P Q) (Q R) (P R).
Proof. tauto. Qed.
Instance: Commutative () (@eq A).
Proof. red. intuition. Qed.
Instance: Commutative () (λ x y, @eq A y x).
......@@ -524,34 +535,31 @@ Proof. red. intuition. Qed.
Instance: RightDistr () () ().
Proof. red. intuition. Qed.
(** The following lemmas are more specific versions of the projections of the
above type classes. These lemmas allow us to enforce Coq not to use the setoid
rewriting mechanism. *)
Lemma idempotent_eq {A} (f : A A A) `{!Idempotent (=) f} x :
f x x = x.
(** The following lemmas are specific versions of the projections of the above
type classes for Leibniz equality. These lemmas allow us to enforce Coq not to
use the setoid rewriting mechanism. *)
Lemma idempotent_L {A} (f : A A A) `{!Idempotent (=) f} x : f x x = x.
Proof. auto. Qed.
Lemma commutative_eq {A B} (f : B B A) `{!Commutative (=) f} x y :
Lemma commutative_L {A B} (f : B B A) `{!Commutative (=) f} x y :
f x y = f y x.
Proof. auto. Qed.
Lemma left_id_eq {A} (i : A) (f : A A A) `{!LeftId (=) i f} x :
f i x = x.
Lemma left_id_L {A} (i : A) (f : A A A) `{!LeftId (=) i f} x : f i x = x.
Proof. auto. Qed.
Lemma right_id_eq {A} (i : A) (f : A A A) `{!RightId (=) i f} x :
f x i = x.
Lemma right_id_L {A} (i : A) (f : A A A) `{!RightId (=) i f} x : f x i = x.
Proof. auto. Qed.
Lemma associative_eq {A} (f : A A A) `{!Associative (=) f} x y z :
Lemma associative_L {A} (f : A A A) `{!Associative (=) f} x y z :
f x (f y z) = f (f x y) z.
Proof. auto. Qed.
Lemma left_absorb_eq {A} (i : A) (f : A A A) `{!LeftAbsorb (=) i f} x :
Lemma left_absorb_L {A} (i : A) (f : A A A) `{!LeftAbsorb (=) i f} x :
f i x = i.
Proof. auto. Qed.
Lemma right_absorb_eq {A} (i : A) (f : A A A) `{!RightAbsorb (=) i f} x :
Lemma right_absorb_L {A} (i : A) (f : A A A) `{!RightAbsorb (=) i f} x :
f x i = i.
Proof. auto. Qed.
Lemma left_distr_eq {A} (f g : A A A) `{!LeftDistr (=) f g} x y z :
Lemma left_distr_L {A} (f g : A A A) `{!LeftDistr (=) f g} x y z :
f x (g y z) = g (f x y) (f x z).
Proof. auto. Qed.
Lemma right_distr_eq {A} (f g : A A A) `{!RightDistr (=) f g} y z x :
Lemma right_distr_L {A} (f g : A A A) `{!RightDistr (=) f g} y z x :
f (g y z) x = g (f y x) (f z x).
Proof. auto. Qed.
......@@ -561,9 +569,9 @@ Class BoundedPreOrder A `{Empty A} `{SubsetEq A} : Prop := {
bounded_preorder :>> PreOrder ();
subseteq_empty x : x
}.
Class PartialOrder A `{SubsetEq A} : Prop := {
po_preorder :>> PreOrder ();
po_antisym :> AntiSymmetric ()
Class PartialOrder {A} (R : relation A) : Prop := {
po_preorder :> PreOrder R;
po_antisym :> AntiSymmetric (=) R
}.
(** We do not include equality in the following interfaces so as to avoid the
......@@ -663,12 +671,10 @@ Class CollectionMonad M `{∀ A, ElemOf A (M A)}
collection_monad_simple A :> SimpleCollection A (M A);
elem_of_bind {A B} (f : A M B) (X : M A) (x : B) :
x X = f y, x f y y X;
elem_of_ret {A} (x y : A) :
x mret y x = y;
elem_of_ret {A} (x y : A) : x mret y x = y;
elem_of_fmap {A B} (f : A B) (X : M A) (x : B) :
x f <$> X y, x = f y y X;
elem_of_join {A} (X : M (M A)) (x : A) :
x mjoin X Y, x Y Y X
elem_of_join {A} (X : M (M A)) (x : A) : x mjoin X Y, x Y Y X
}.
(** The function [fresh X] yields an element that is not contained in [X]. We
......
......@@ -42,8 +42,7 @@ Section simple_collection.
Global Instance elem_of_proper: Proper ((=) ==> () ==> iff) () | 5.
Proof. intros ???. subst. firstorder. Qed.
Lemma elem_of_union_list (Xs : list C) (x : A) :
x Xs X, X Xs x X.
Lemma elem_of_union_list Xs x : x Xs X, X Xs x X.
Proof.
split.
* induction Xs; simpl; intros HXs.
......@@ -249,13 +248,11 @@ Section collection.
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.
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.
rewrite elem_of_difference. destruct (decide (x Y)); tauto.
Qed.
Lemma union_difference X Y : X Y Y X Y X.
Proof.
......@@ -303,19 +300,18 @@ Section collection_ops.
( 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 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.
End collection_ops.
(** * Sets without duplicates up to an equivalence *)
Section no_dup.
Section NoDup.
Context `{SimpleCollection A B} (R : relation A) `{!Equivalence R}.
Definition elem_of_upto (x : A) (X : B) := y, y X R x y.
Definition no_dup (X : B) := x y, x X y X R x y x = y.
Definition set_NoDup (X : B) := x y, x X y X R x y x = y.
Global Instance: Proper (() ==> iff) (elem_of_upto x).
Proof. intros ??? E. unfold elem_of_upto. by setoid_rewrite E. Qed.
......@@ -325,7 +321,7 @@ Section no_dup.
* rewrite <-E1, <-E2; intuition.
* rewrite E1, E2; intuition.
Qed.
Global Instance: Proper (() ==> iff) no_dup.
Global Instance: Proper (() ==> iff) set_NoDup.
Proof. firstorder. Qed.
Lemma elem_of_upto_elem_of x X : x X elem_of_upto x X.
......@@ -341,60 +337,63 @@ Section no_dup.
Lemma not_elem_of_upto x X : ¬elem_of_upto x X y, y X ¬R x y.
Proof. unfold elem_of_upto. esolve_elem_of. Qed.
Lemma no_dup_empty: no_dup .
Proof. unfold no_dup. solve_elem_of. Qed.
Lemma no_dup_add x X : ¬elem_of_upto x X no_dup X no_dup ({[ x ]} X).
Proof. unfold no_dup, elem_of_upto. esolve_elem_of. Qed.
Lemma no_dup_inv_add x X : x X no_dup ({[ x ]} X) ¬elem_of_upto x X.
Lemma set_NoDup_empty: set_NoDup .
Proof. unfold set_NoDup. solve_elem_of. Qed.
Lemma set_NoDup_add x X :
¬elem_of_upto x X set_NoDup X set_NoDup ({[ x ]} X).
Proof. unfold set_NoDup, elem_of_upto. esolve_elem_of. Qed.
Lemma set_NoDup_inv_add x X :
x X set_NoDup ({[ x ]} X) ¬elem_of_upto x X.
Proof.
intros Hin Hnodup [y [??]].
rewrite (Hnodup x y) in Hin; solve_elem_of.
Qed.
Lemma no_dup_inv_union_l X Y : no_dup (X Y) no_dup X.
Proof. unfold no_dup. solve_elem_of. Qed.
Lemma no_dup_inv_union_r X Y : no_dup (X Y) no_dup Y.
Proof. unfold no_dup. solve_elem_of. Qed.
End no_dup.
Lemma set_NoDup_inv_union_l X Y : set_NoDup (X Y) set_NoDup X.
Proof. unfold set_NoDup. solve_elem_of. Qed.
Lemma set_NoDup_inv_union_r X Y : set_NoDup (X Y) set_NoDup Y.
Proof. unfold set_NoDup. solve_elem_of. Qed.
End NoDup.
(** * Quantifiers *)
Section quantifiers.
Context `{SimpleCollection A B} (P : A Prop).
Definition cforall X := x, x X P x.
Definition cexists X := x, x X P x.
Lemma cforall_empty : cforall .
Proof. unfold cforall. solve_elem_of. Qed.
Lemma cforall_singleton x : cforall {[ x ]} P x.
Proof. unfold cforall. solve_elem_of. Qed.
Lemma cforall_union X Y : cforall X cforall Y cforall (X Y).
Proof. unfold cforall. solve_elem_of. Qed.
Lemma cforall_union_inv_1 X Y : cforall (X Y) cforall X.
Proof. unfold cforall. solve_elem_of. Qed.
Lemma cforall_union_inv_2 X Y : cforall (X Y) cforall Y.
Proof. unfold cforall. solve_elem_of. Qed.
Lemma cexists_empty : ¬cexists .
Proof. unfold cexists. esolve_elem_of. Qed.
Lemma cexists_singleton x : cexists {[ x ]} P x.
Proof. unfold cexists. esolve_elem_of. Qed.
Lemma cexists_union_1 X Y : cexists X cexists (X Y).
Proof. unfold cexists. esolve_elem_of. Qed.
Lemma cexists_union_2 X Y : cexists Y cexists (X Y).
Proof. unfold cexists. esolve_elem_of. Qed.
Lemma cexists_union_inv X Y : cexists (X Y) cexists X cexists Y.
Proof. unfold cexists. esolve_elem_of. Qed.
Definition set_Forall X := x, x X P x.
Definition set_Exists X := x, x X P x.
Lemma set_Forall_empty : set_Forall .
Proof. unfold set_Forall. solve_elem_of. Qed.
Lemma set_Forall_singleton x : set_Forall {[ x ]} P x.
Proof. unfold set_Forall. solve_elem_of. Qed.
Lemma set_Forall_union X Y : set_Forall X set_Forall Y set_Forall (X Y).
Proof. unfold set_Forall. solve_elem_of. Qed.
Lemma set_Forall_union_inv_1 X Y : set_Forall (X Y) set_Forall X.
Proof. unfold set_Forall. solve_elem_of. Qed.
Lemma set_Forall_union_inv_2 X Y : set_Forall (X Y) set_Forall Y.
Proof. unfold set_Forall. solve_elem_of. Qed.
Lemma set_Exists_empty : ¬set_Exists .
Proof. unfold set_Exists. esolve_elem_of. Qed.
Lemma set_Exists_singleton x : set_Exists {[ x ]} P x.
Proof. unfold set_Exists. esolve_elem_of. Qed.
Lemma set_Exists_union_1 X Y : set_Exists X set_Exists (X Y).
Proof. unfold set_Exists. esolve_elem_of. Qed.
Lemma set_Exists_union_2 X Y : set_Exists Y set_Exists (X Y).
Proof. unfold set_Exists. esolve_elem_of. Qed.
Lemma set_Exists_union_inv X Y :
set_Exists (X Y) set_Exists X set_Exists Y.
Proof. unfold set_Exists. esolve_elem_of. Qed.
End quantifiers.
Section more_quantifiers.
Context `{Collection A B}.
Lemma cforall_weaken (P Q : A Prop) (Hweaken : x, P x Q x) X :
cforall P X cforall Q X.
Proof. unfold cforall. naive_solver. Qed.
Lemma cexists_weaken (P Q : A Prop) (Hweaken : x, P x Q x) X :
cexists P X cexists Q X.
Proof. unfold cexists. naive_solver. Qed.
Lemma set_Forall_weaken (P Q : A Prop) (Hweaken : x, P x Q x) X :
set_Forall P X set_Forall Q X.
Proof. unfold set_Forall. naive_solver. Qed.
Lemma set_Exists_weaken (P Q : A Prop) (Hweaken : x, P x Q x) X :
set_Exists P X set_Exists Q X.
Proof. unfold set_Exists. naive_solver. Qed.
End more_quantifiers.
(** * Fresh elements *)
......@@ -417,8 +416,7 @@ Section fresh.
Global Instance fresh_list_proper: Proper ((=) ==> () ==> (=)) fresh_list.
Proof.
intros ? n ?. subst.
induction n; simpl; intros ?? E; f_equal.
intros ? n ?. subst. induction n; simpl; intros ?? E; f_equal.
* by rewrite E.
* apply IHn. by rewrite E.
Qed.
......@@ -437,10 +435,8 @@ Section fresh.
Lemma fresh_list_nodup n X : NoDup (fresh_list n X).
Proof.
revert X.
induction n; simpl; constructor; auto.
intros Hin. apply fresh_list_is_fresh in Hin.
solve_elem_of.
revert X. induction n; simpl; constructor; auto.
intros Hin. apply fresh_list_is_fresh in Hin. solve_elem_of.
Qed.
End fresh.
......@@ -455,7 +451,10 @@ Section collection_monad.
Context `{CollectionMonad M}.
Global Instance collection_guard: MGuard M := λ P dec A x,
if dec then x else .
match dec with
| left H => x H
| _ =>
end.
Global Instance collection_fmap_proper {A B} (f : A B) :
Proper (() ==> ()) (fmap f).
......@@ -495,8 +494,7 @@ Section collection_monad.
Proof. revert l; induction k; esolve_elem_of. Qed.
Lemma elem_of_mapM_fmap {A B} (f : A B) (g : B M A) l k :
Forall (λ x, y, y g x f y = x) l
k mapM g l fmap f k = l.
Forall (λ x, y, y g x f y = x) l k mapM g l fmap f k = l.
Proof.
intros Hl. revert k.
induction Hl; simpl; intros;
......@@ -504,14 +502,10 @@ Section collection_monad.
Qed.
Lemma elem_of_mapM_Forall {A B} (f : A M B) (P : B Prop) l k :
l mapM f k
Forall (λ x, y, y f x P y) k
Forall P l.
l mapM f k Forall (λ x, y, y f x P y) k Forall P l.
Proof. rewrite elem_of_mapM. apply Forall2_Forall_l. Qed.
Lemma elem_of_mapM_Forall2_l {A B C} (f : A M B)
(P : B C Prop) l1 l2 k :
l1 mapM f k
Forall2 (λ x y, z, z f x P z y) k l2
Lemma elem_of_mapM_Forall2_l {A B C} (f : A M B) (P: B C Prop) l1 l2 k :
l1 mapM f k Forall2 (λ x y, z, z f x P z y) k l2
Forall2 P l1 l2.
Proof.
rewrite elem_of_mapM. intros Hl1. revert l2.
......
......@@ -76,6 +76,7 @@ Notation cast_if_and3 S1 S2 S3 := (if S1 then cast_if_and S2 S3 else right _).
Notation cast_if_and4 S1 S2 S3 S4 :=
(if S1 then cast_if_and3 S2 S3 S4 else right _).
Notation cast_if_or S1 S2 := (if S1 then left _ else cast_if S2).
Notation cast_if_or3 S1 S2 S3 := (if S1 then left _ else cast_if_or S2 S3).
Notation cast_if_not_or S1 S2 := (if S1 then cast_if S2 else left _).
Notation cast_if_not S := (if S then right _ else left _).
......
......@@ -13,7 +13,7 @@ Definition collection_fold `{Elements A C} {B}
Section fin_collection.
Context `{FinCollection A C}.
Global Instance elements_proper: Proper (() ==> Permutation) elements.
Global Instance elements_proper: Proper (() ==> (≡ₚ)) elements.
Proof.
intros ?? E. apply NoDup_Permutation.
* apply elements_nodup.
......@@ -176,10 +176,8 @@ Proof.
apply Hadd. solve_elem_of. apply IH. esolve_elem_of.
Qed.
Lemma collection_fold_proper {B} (R : relation B)
`{!Equivalence R}
(f : A B B) (b : B)
`{!Proper ((=) ==> R ==> R) f}
Lemma collection_fold_proper {B} (R : relation B) `{!Equivalence R}
(f : A B B) (b : B) `{!Proper ((=) ==> R ==> R) f}
(Hf : a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
Proper (() ==> R) (collection_fold f b).
Proof.
......@@ -188,22 +186,22 @@ Proof.
* by rewrite E.
Qed.
Global Instance cforall_dec `(P : A Prop)
`{ x, Decision (P x)} X : Decision (cforall P X) | 100.
Global Instance set_Forall_dec `(P : A Prop)
`{ x, Decision (P x)} X : Decision (set_Forall P X) | 100.
Proof.
refine (cast_if (decide (Forall P (elements X))));
abstract (unfold cforall; setoid_rewrite elements_spec;
abstract (unfold set_Forall; setoid_rewrite elements_spec;
by rewrite <-Forall_forall).
Defined.
Global Instance cexists_dec `(P : A Prop) `{ x, Decision (P x)} X :
Decision (cexists P X) | 100.