Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • iris/stdpp
  • johannes/stdpp
  • proux1/stdpp
  • dosualdo/stdpp
  • benoit/coq-stdpp
  • dfrumin/coq-stdpp
  • haidang/stdpp
  • amintimany/coq-stdpp
  • swasey/coq-stdpp
  • simongregersen/stdpp
  • proux/stdpp
  • janno/coq-stdpp
  • amaurremi/coq-stdpp
  • msammler/stdpp
  • tchajed/stdpp
  • YaZko/stdpp
  • maximedenes/stdpp
  • jakobbotsch/stdpp
  • Blaisorblade/stdpp
  • simonspies/stdpp
  • lepigre/stdpp
  • devilhena/stdpp
  • simonfv/stdpp
  • jihgfee/stdpp
  • snyke7/stdpp
  • Armael/stdpp
  • gmalecha/stdpp
  • olaure01/stdpp
  • sarahzrf/stdpp
  • atrieu/stdpp
  • herbelin/stdpp
  • arthuraa/stdpp
  • lgaeher/stdpp
  • mrhaandi/stdpp
  • mattam82/stdpp
  • Quarkbeast/stdpp
  • aa755/stdpp
  • gmevel/stdpp
  • lstefane/stdpp
  • jung/stdpp
  • vsiles/stdpp
  • dlesbre/stdpp
  • bergwerf/stdpp
  • marijnvanwezel/stdpp
  • ivanbakel/stdpp
  • tperami/stdpp
  • adamAndMath/stdpp
  • Villetaneuse/stdpp
  • sanjit/stdpp
  • yiyunliu/stdpp
  • thomas-lamiaux/stdpp
  • Tragicus/stdpp
  • kbedarka/stdpp
53 results
Show changes
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 10702 additions and 382 deletions
theories/coGset.v → stdpp/coGset.v
View file @ 9274984b
......@@ -6,16 +6,19 @@ Note that [coGset positive] cannot represent all elements of [coPset]
infinite sets that cannot be represented). *)
From stdpp Require Export sets countable.
From stdpp Require Import decidable finite gmap coPset.
(* Set Default Proof Using "Type". *)
From stdpp Require Import options.
(* Pick up extra assumptions from section parameters. *)
Set Default Proof Using "Type*".
Inductive coGset `{Countable A} :=
| FinGSet (X : gset A)
| CoFinGset (X : gset A).
Arguments coGset _ {_ _} : assert.
Global Arguments coGset _ {_ _} : assert.
Instance coGset_eq_dec `{Countable A} : EqDecision (coGset A).
Global Instance coGset_eq_dec `{Countable A} : EqDecision (coGset A).
Proof. solve_decision. Defined.
Instance coGset_countable `{Countable A} : Countable (coGset A).
Global Instance coGset_countable `{Countable A} : Countable (coGset A).
Proof.
apply (inj_countable'
(λ X, match X with FinGSet X => inl X | CoFinGset X => inr X end)
......@@ -77,7 +80,7 @@ Section coGset.
Qed.
End coGset.
Instance coGset_elem_of_dec `{Countable A} : RelDecision (∈@{coGset A}) :=
Global Instance coGset_elem_of_dec `{Countable A} : RelDecision (∈@{coGset A}) :=
λ x X,
match X with
| FinGSet X => decide_rel elem_of x X
......@@ -89,7 +92,7 @@ Section infinite.
Global Instance coGset_leibniz : LeibnizEquiv (coGset A).
Proof.
intros [X|X] [Y|Y]; rewrite elem_of_equiv;
intros [X|X] [Y|Y]; rewrite set_equiv;
unfold elem_of, coGset_elem_of; simpl; intros HXY.
- f_equal. by apply leibniz_equiv.
- by destruct (exist_fresh (X ∪ Y)) as [? [? ?%HXY]%not_elem_of_union].
......@@ -135,11 +138,12 @@ End infinite.
Definition coGpick `{Countable A, Infinite A} (X : coGset A) : A :=
fresh (match X with FinGSet _ => ∅ | CoFinGset X => X end).
Lemma coGpick_elem_of `{Countable A, Infinite A} X :
Lemma coGpick_elem_of `{Countable A, Infinite A} (X : coGset A) :
¬set_finite X → coGpick X ∈ X.
Proof.
unfold coGpick. destruct X as [X|X]; rewrite coGset_finite_spec; simpl.
done. by intros _; apply is_fresh.
unfold coGpick.
destruct X as [X|X]; rewrite coGset_finite_spec; simpl; [done|].
by intros _; apply is_fresh.
Qed.
(** * Conversion to and from gset *)
......@@ -148,13 +152,16 @@ Definition coGset_to_gset `{Countable A} (X : coGset A) : gset A :=
Definition gset_to_coGset `{Countable A} : gset A → coGset A := FinGSet.
Section to_gset.
Context `{Countable A, Infinite A}.
Context `{Countable A}.
Lemma elem_of_gset_to_coGset (X : gset A) x : x ∈ gset_to_coGset X ↔ x ∈ X.
Proof. done. Qed.
Context `{Infinite A}.
Lemma elem_of_coGset_to_gset (X : coGset A) x :
set_finite X → x ∈ coGset_to_gset X ↔ x ∈ X.
Proof. rewrite coGset_finite_spec. by destruct X. Qed.
Lemma elem_of_gset_to_coGset (X : gset A) x : x ∈ gset_to_coGset X ↔ x ∈ X.
Proof. done. Qed.
Lemma gset_to_coGset_finite (X : gset A) : set_finite (gset_to_coGset X).
Proof. by rewrite coGset_finite_spec. Qed.
End to_gset.
......@@ -168,8 +175,8 @@ Definition coGset_to_coPset (X : coGset positive) : coPset :=
Lemma elem_of_coGset_to_coPset X x : x ∈ coGset_to_coPset X ↔ x ∈ X.
Proof.
destruct X as [X|X]; simpl.
by rewrite elem_of_gset_to_coPset.
by rewrite elem_of_difference, elem_of_gset_to_coPset, (left_id True (∧)).
- by rewrite elem_of_gset_to_coPset.
- by rewrite elem_of_difference, elem_of_gset_to_coPset, (left_id True (∧)).
Qed.
(** * Inefficient conversion to arbitrary sets with a top element *)
......@@ -185,15 +192,5 @@ Lemma elem_of_coGset_to_top_set `{Countable A, TopSet A C} X x :
x ∈@{C} coGset_to_top_set X ↔ x ∈ X.
Proof. destruct X; set_solver. Qed.
(** * Domain of finite maps *)
Instance coGset_dom `{Countable K} {A} : Dom (gmap K A) (coGset K) := λ m,
gset_to_coGset (dom _ m).
Instance coGset_dom_spec `{Countable K} : FinMapDom K (gmap K) (coGset K).
Proof.
split; try apply _. intros B m i. unfold dom, coGset_dom.
by rewrite elem_of_gset_to_coGset, elem_of_dom.
Qed.
Typeclasses Opaque coGset_elem_of coGset_empty coGset_top coGset_singleton.
Typeclasses Opaque coGset_union coGset_intersection coGset_difference.
Typeclasses Opaque coGset_dom.
Global Typeclasses Opaque coGset_elem_of coGset_empty coGset_top coGset_singleton.
Global Typeclasses Opaque coGset_union coGset_intersection coGset_difference.
theories/coPset.v → stdpp/coPset.v
View file @ 9274984b
......@@ -11,14 +11,14 @@ Since [positive]s are bitstrings, we encode [coPset]s as trees that correspond
to the decision function that map bitstrings to bools. *)
From stdpp Require Export sets.
From stdpp Require Import pmap gmap mapset.
Set Default Proof Using "Type".
From stdpp Require Import options.
Local Open Scope positive_scope.
(** * The tree data structure *)
Inductive coPset_raw :=
| coPLeaf : bool → coPset_raw
| coPNode : bool → coPset_raw → coPset_raw → coPset_raw.
Instance coPset_raw_eq_dec : EqDecision coPset_raw.
Global Instance coPset_raw_eq_dec : EqDecision coPset_raw.
Proof. solve_decision. Defined.
Fixpoint coPset_wf (t : coPset_raw) : bool :=
......@@ -26,9 +26,16 @@ Fixpoint coPset_wf (t : coPset_raw) : bool :=
| coPLeaf _ => true
| coPNode true (coPLeaf true) (coPLeaf true) => false
| coPNode false (coPLeaf false) (coPLeaf false) => false
| coPNode b l r => coPset_wf l && coPset_wf r
| coPNode _ l r => coPset_wf l && coPset_wf r
end.
Arguments coPset_wf !_ / : simpl nomatch, assert.
Global Arguments coPset_wf !_ / : simpl nomatch, assert.
Lemma coPNode_wf b l r :
coPset_wf l → coPset_wf r →
(l = coPLeaf true → r = coPLeaf true → b = true → False) →
(l = coPLeaf false → r = coPLeaf false → b = false → False) →
coPset_wf (coPNode b l r).
Proof. destruct b, l as [[]|], r as [[]|]; naive_solver. Qed.
Lemma coPNode_wf_l b l r : coPset_wf (coPNode b l r) → coPset_wf l.
Proof. destruct b, l as [[]|],r as [[]|]; simpl; rewrite ?andb_True; tauto. Qed.
......@@ -42,10 +49,10 @@ Definition coPNode' (b : bool) (l r : coPset_raw) : coPset_raw :=
| false, coPLeaf false, coPLeaf false => coPLeaf false
| _, _, _ => coPNode b l r
end.
Arguments coPNode' : simpl never.
Lemma coPNode_wf b l r : coPset_wf l → coPset_wf r → coPset_wf (coPNode' b l r).
Global Arguments coPNode' : simpl never.
Lemma coPNode'_wf b l r : coPset_wf l → coPset_wf r → coPset_wf (coPNode' b l r).
Proof. destruct b, l as [[]|], r as [[]|]; simpl; auto. Qed.
Hint Resolve coPNode_wf : core.
Global Hint Resolve coPNode'_wf : core.
Fixpoint coPset_elem_of_raw (p : positive) (t : coPset_raw) {struct t} : bool :=
match t, p with
......@@ -55,7 +62,7 @@ Fixpoint coPset_elem_of_raw (p : positive) (t : coPset_raw) {struct t} : bool :=
| coPNode _ _ r, p~1 => coPset_elem_of_raw p r
end.
Local Notation e_of := coPset_elem_of_raw.
Arguments coPset_elem_of_raw _ !_ / : simpl nomatch, assert.
Global Arguments coPset_elem_of_raw _ !_ / : simpl nomatch, assert.
Lemma coPset_elem_of_node b l r p :
e_of p (coPNode' b l r) = e_of p (coPNode b l r).
Proof. by destruct p, b, l as [[]|], r as [[]|]. Qed.
......@@ -87,7 +94,7 @@ Fixpoint coPset_singleton_raw (p : positive) : coPset_raw :=
| p~0 => coPNode' false (coPset_singleton_raw p) (coPLeaf false)
| p~1 => coPNode' false (coPLeaf false) (coPset_singleton_raw p)
end.
Instance coPset_union_raw : Union coPset_raw :=
Global Instance coPset_union_raw : Union coPset_raw :=
fix go t1 t2 := let _ : Union _ := @go in
match t1, t2 with
| coPLeaf false, coPLeaf false => coPLeaf false
......@@ -98,7 +105,7 @@ Instance coPset_union_raw : Union coPset_raw :=
| coPNode b1 l1 r1, coPNode b2 l2 r2 => coPNode' (b1||b2) (l1 ∪ l2) (r1 ∪ r2)
end.
Local Arguments union _ _!_ !_ / : assert.
Instance coPset_intersection_raw : Intersection coPset_raw :=
Global Instance coPset_intersection_raw : Intersection coPset_raw :=
fix go t1 t2 := let _ : Intersection _ := @go in
match t1, t2 with
| coPLeaf true, coPLeaf true => coPLeaf true
......@@ -152,22 +159,22 @@ Qed.
(** * Packed together + set operations *)
Definition coPset := { t | coPset_wf t }.
Instance coPset_singleton : Singleton positive coPset := λ p,
Global Instance coPset_singleton : Singleton positive coPset := λ p,
coPset_singleton_raw p ↾ coPset_singleton_wf _.
Instance coPset_elem_of : ElemOf positive coPset := λ p X, e_of p (`X).
Instance coPset_empty : Empty coPset := coPLeaf false ↾ I.
Instance coPset_top : Top coPset := coPLeaf true ↾ I.
Instance coPset_union : Union coPset := λ X Y,
Global Instance coPset_elem_of : ElemOf positive coPset := λ p X, e_of p (`X).
Global Instance coPset_empty : Empty coPset := coPLeaf false ↾ I.
Global Instance coPset_top : Top coPset := coPLeaf true ↾ I.
Global Instance coPset_union : Union coPset := λ X Y,
let (t1,Ht1) := X in let (t2,Ht2) := Y in
(t1 ∪ t2) ↾ coPset_union_wf _ _ Ht1 Ht2.
Instance coPset_intersection : Intersection coPset := λ X Y,
Global Instance coPset_intersection : Intersection coPset := λ X Y,
let (t1,Ht1) := X in let (t2,Ht2) := Y in
(t1 ∩ t2) ↾ coPset_intersection_wf _ _ Ht1 Ht2.
Instance coPset_difference : Difference coPset := λ X Y,
Global Instance coPset_difference : Difference coPset := λ X Y,
let (t1,Ht1) := X in let (t2,Ht2) := Y in
(t1 ∩ coPset_opp_raw t2) ↾ coPset_intersection_wf _ _ Ht1 (coPset_opp_wf _).
Instance coPset_top_set : TopSet positive coPset.
Global Instance coPset_top_set : TopSet positive coPset.
Proof.
split; [split; [split| |]|].
- by intros ??.
......@@ -184,25 +191,25 @@ Qed.
(** Iris and specifically [solve_ndisj] heavily rely on this hint. *)
Local Definition coPset_top_subseteq := top_subseteq (C:=coPset).
Hint Resolve coPset_top_subseteq : core.
Global Hint Resolve coPset_top_subseteq : core.
Instance coPset_leibniz : LeibnizEquiv coPset.
Global Instance coPset_leibniz : LeibnizEquiv coPset.
Proof.
intros X Y; rewrite elem_of_equiv; intros HXY.
intros X Y; rewrite set_equiv; intros HXY.
apply (sig_eq_pi _), coPset_eq; try apply @proj2_sig.
intros p; apply eq_bool_prop_intro, (HXY p).
Qed.
Instance coPset_elem_of_dec : RelDecision (∈@{coPset}).
Global Instance coPset_elem_of_dec : RelDecision (∈@{coPset}).
Proof. solve_decision. Defined.
Instance coPset_equiv_dec : RelDecision (≡@{coPset}).
Global Instance coPset_equiv_dec : RelDecision (≡@{coPset}).
Proof. refine (λ X Y, cast_if (decide (X = Y))); abstract (by fold_leibniz). Defined.
Instance mapset_disjoint_dec : RelDecision (##@{coPset}).
Global Instance mapset_disjoint_dec : RelDecision (##@{coPset}).
Proof.
refine (λ X Y, cast_if (decide (X ∩ Y = ∅)));
abstract (by rewrite disjoint_intersection_L).
Defined.
Instance mapset_subseteq_dec : RelDecision (⊆@{coPset}).
Global Instance mapset_subseteq_dec : RelDecision (⊆@{coPset}).
Proof.
refine (λ X Y, cast_if (decide (X ∪ Y = Y))); abstract (by rewrite subseteq_union_L).
Defined.
......@@ -221,7 +228,7 @@ Proof.
unfold set_finite, elem_of at 1, coPset_elem_of; simpl; clear Ht; split.
- induction t as [b|b l IHl r IHr]; simpl.
{ destruct b; simpl; [intros [l Hl]|done].
by apply (is_fresh (list_to_set l : Pset)), elem_of_list_to_set, Hl. }
by apply (infinite_is_fresh l), Hl. }
intros [ll Hll]; rewrite andb_True; split.
+ apply IHl; exists (omap (maybe (~0)) ll); intros i.
rewrite elem_of_list_omap; intros; exists (i~0); auto.
......@@ -232,14 +239,17 @@ Proof.
exists ([1] ++ ((~0) <$> ll) ++ ((~1) <$> rl))%list; intros [i|i|]; simpl;
rewrite elem_of_cons, elem_of_app, !elem_of_list_fmap; naive_solver.
Qed.
Instance coPset_finite_dec (X : coPset) : Decision (set_finite X).
Global Instance coPset_finite_dec (X : coPset) : Decision (set_finite X).
Proof.
refine (cast_if (decide (coPset_finite (`X)))); by rewrite coPset_finite_spec.
Defined.
(** * Pick element from infinite sets *)
(* Implemented using depth-first search, which results in very unbalanced
trees. *)
(* The function [coPpick X] gives an element that is in the set [X], provided
that the set [X] is infinite. Note that [coPpick] function is implemented by
depth-first search, so using it repeatedly to obtain elements [x], and
inserting these elements [x] into the set [X], will give rise to a very
unbalanced tree. *)
Fixpoint coPpick_raw (t : coPset_raw) : option positive :=
match t with
| coPLeaf true | coPNode true _ _ => Some 1
......@@ -269,89 +279,109 @@ Proof.
Qed.
(** * Conversion to psets *)
Fixpoint coPset_to_Pset_raw (t : coPset_raw) : Pmap_raw () :=
Fixpoint coPset_to_Pset_raw (t : coPset_raw) : Pmap () :=
match t with
| coPLeaf _ => PLeaf
| coPNode false l r => PNode' None (coPset_to_Pset_raw l) (coPset_to_Pset_raw r)
| coPNode true l r => PNode (Some ()) (coPset_to_Pset_raw l) (coPset_to_Pset_raw r)
| coPLeaf _ => PEmpty
| coPNode false l r => pmap.PNode (coPset_to_Pset_raw l) None (coPset_to_Pset_raw r)
| coPNode true l r => pmap.PNode (coPset_to_Pset_raw l) (Some ()) (coPset_to_Pset_raw r)
end.
Lemma coPset_to_Pset_wf t : coPset_wf t → Pmap_wf (coPset_to_Pset_raw t).
Proof. induction t as [|[]]; simpl; eauto using PNode_wf. Qed.
Definition coPset_to_Pset (X : coPset) : Pset :=
let (t,Ht) := X in Mapset (PMap (coPset_to_Pset_raw t) (coPset_to_Pset_wf _ Ht)).
let (t,Ht) := X in Mapset (coPset_to_Pset_raw t).
Lemma elem_of_coPset_to_Pset X i : set_finite X → i ∈ coPset_to_Pset X ↔ i ∈ X.
Proof.
rewrite coPset_finite_spec; destruct X as [t Ht].
change (coPset_finite t → coPset_to_Pset_raw t !! i = Some () ↔ e_of i t).
clear Ht; revert i; induction t as [[]|[] l IHl r IHr]; intros [i|i|];
simpl; rewrite ?andb_True, ?PNode_lookup; naive_solver.
simpl; rewrite ?andb_True, ?pmap.Pmap_lookup_PNode; naive_solver.
Qed.
(** * Conversion from psets *)
Fixpoint Pset_to_coPset_raw (t : Pmap_raw ()) : coPset_raw :=
match t with
| PLeaf => coPLeaf false
| PNode None l r => coPNode false (Pset_to_coPset_raw l) (Pset_to_coPset_raw r)
| PNode (Some _) l r => coPNode true (Pset_to_coPset_raw l) (Pset_to_coPset_raw r)
end.
Lemma Pset_to_coPset_wf t : Pmap_wf t → coPset_wf (Pset_to_coPset_raw t).
Definition Pset_to_coPset_raw_aux (go : Pmap_ne () → coPset_raw)
(mt : Pmap ()) : coPset_raw :=
match mt with PNodes t => go t | PEmpty => coPLeaf false end.
Fixpoint Pset_ne_to_coPset_raw (t : Pmap_ne ()) : coPset_raw :=
pmap.Pmap_ne_case t $ λ ml mx mr,
coPNode match mx with Some _ => true | None => false end
(Pset_to_coPset_raw_aux Pset_ne_to_coPset_raw ml)
(Pset_to_coPset_raw_aux Pset_ne_to_coPset_raw mr).
Definition Pset_to_coPset_raw : Pmap () → coPset_raw :=
Pset_to_coPset_raw_aux Pset_ne_to_coPset_raw.
Lemma Pset_to_coPset_raw_PNode ml mx mr :
pmap.PNode_valid ml mx mr →
Pset_to_coPset_raw (pmap.PNode ml mx mr) =
coPNode match mx with Some _ => true | None => false end
(Pset_to_coPset_raw ml) (Pset_to_coPset_raw mr).
Proof. by destruct ml, mx, mr. Qed.
Lemma Pset_to_coPset_raw_wf t : coPset_wf (Pset_to_coPset_raw t).
Proof.
induction t as [|[] l IHl r IHr]; simpl; rewrite ?andb_True; auto.
- intros [??]; destruct l as [|[]], r as [|[]]; simpl in *; auto.
- destruct l as [|[]], r as [|[]]; simpl in *; rewrite ?andb_true_r;
rewrite ?andb_True; rewrite ?andb_True in IHl, IHr; intuition.
induction t as [|ml mx mr] using pmap.Pmap_ind; [done|].
rewrite Pset_to_coPset_raw_PNode by done.
apply coPNode_wf; [done|done|..];
destruct mx; destruct ml using pmap.Pmap_ind; destruct mr using pmap.Pmap_ind;
rewrite ?Pset_to_coPset_raw_PNode by done; naive_solver.
Qed.
Lemma elem_of_Pset_to_coPset_raw i t : e_of i (Pset_to_coPset_raw t) ↔ t !! i = Some ().
Proof. by revert i; induction t as [|[[]|]]; intros []; simpl; auto; split. Qed.
Proof.
revert i. induction t as [|ml mx mr] using pmap.Pmap_ind; [done|].
intros []; rewrite Pset_to_coPset_raw_PNode,
pmap.Pmap_lookup_PNode by done; destruct mx as [[]|]; naive_solver.
Qed.
Lemma Pset_to_coPset_raw_finite t : coPset_finite (Pset_to_coPset_raw t).
Proof. induction t as [|[[]|]]; simpl; rewrite ?andb_True; auto. Qed.
Proof.
induction t as [|ml mx mr] using pmap.Pmap_ind; [done|].
rewrite Pset_to_coPset_raw_PNode by done. destruct mx; naive_solver.
Qed.
Definition Pset_to_coPset (X : Pset) : coPset :=
let 'Mapset (PMap t Ht) := X in Pset_to_coPset_raw t ↾ Pset_to_coPset_wf _ Ht.
let 'Mapset t := X in Pset_to_coPset_raw t ↾ Pset_to_coPset_raw_wf _.
Lemma elem_of_Pset_to_coPset X i : i ∈ Pset_to_coPset X ↔ i ∈ X.
Proof. destruct X as [[t ?]]; apply elem_of_Pset_to_coPset_raw. Qed.
Proof. destruct X; apply elem_of_Pset_to_coPset_raw. Qed.
Lemma Pset_to_coPset_finite X : set_finite (Pset_to_coPset X).
Proof.
apply coPset_finite_spec; destruct X as [[t ?]]; apply Pset_to_coPset_raw_finite.
Qed.
Proof. apply coPset_finite_spec; destruct X; apply Pset_to_coPset_raw_finite. Qed.
(** * Conversion to and from gsets of positives *)
Lemma coPset_to_gset_wf (m : Pmap ()) : gmap_wf positive m.
Proof. unfold gmap_wf. by rewrite bool_decide_spec. Qed.
Definition coPset_to_gset (X : coPset) : gset positive :=
let 'Mapset m := coPset_to_Pset X in
Mapset (GMap m (coPset_to_gset_wf m)).
Mapset (pmap_to_gmap m).
Definition gset_to_coPset (X : gset positive) : coPset :=
let 'Mapset (GMap (PMap t Ht) _) := X in Pset_to_coPset_raw t ↾ Pset_to_coPset_wf _ Ht.
let 'Mapset m := X in
Pset_to_coPset_raw (gmap_to_pmap m) ↾ Pset_to_coPset_raw_wf _.
Lemma elem_of_coPset_to_gset X i : set_finite X → i ∈ coPset_to_gset X ↔ i ∈ X.
Proof.
intros ?. rewrite <-elem_of_coPset_to_Pset by done.
unfold coPset_to_gset. by destruct (coPset_to_Pset X).
intros ?. rewrite <-elem_of_coPset_to_Pset by done. destruct X as [X ?].
unfold elem_of, gset_elem_of, mapset_elem_of, coPset_to_gset; simpl.
by rewrite lookup_pmap_to_gmap.
Qed.
Lemma elem_of_gset_to_coPset X i : i ∈ gset_to_coPset X ↔ i ∈ X.
Proof. destruct X as [[[t ?]]]; apply elem_of_Pset_to_coPset_raw. Qed.
Proof.
destruct X as [m]. unfold elem_of, coPset_elem_of; simpl.
by rewrite elem_of_Pset_to_coPset_raw, lookup_gmap_to_pmap.
Qed.
Lemma gset_to_coPset_finite X : set_finite (gset_to_coPset X).
Proof.
apply coPset_finite_spec; destruct X as [[[t ?]]]; apply Pset_to_coPset_raw_finite.
apply coPset_finite_spec; destruct X as [[?]]; apply Pset_to_coPset_raw_finite.
Qed.
(** * Domain of finite maps *)
Instance Pmap_dom_coPset {A} : Dom (Pmap A) coPset := λ m, Pset_to_coPset (dom _ m).
Instance Pmap_dom_coPset_spec: FinMapDom positive Pmap coPset.
(** * Infinite sets *)
Lemma coPset_infinite_finite (X : coPset) : set_infinite X ↔ ¬set_finite X.
Proof.
split; try apply _; intros A m i; unfold dom, Pmap_dom_coPset.
by rewrite elem_of_Pset_to_coPset, elem_of_dom.
split; [intros ??; by apply (set_not_infinite_finite X)|].
intros Hfin xs. exists (coPpick (X ∖ list_to_set xs)).
cut (coPpick (X ∖ list_to_set xs) ∈ X ∖ list_to_set xs); [set_solver|].
apply coPpick_elem_of; intros Hfin'.
apply Hfin, (difference_finite_inv _ (list_to_set xs)), Hfin'.
apply list_to_set_finite.
Qed.
Instance gmap_dom_coPset {A} : Dom (gmap positive A) coPset := λ m,
gset_to_coPset (dom _ m).
Instance gmap_dom_coPset_spec: FinMapDom positive (gmap positive) coPset.
Lemma coPset_finite_infinite (X : coPset) : set_finite X ↔ ¬set_infinite X.
Proof. rewrite coPset_infinite_finite. split; [tauto|apply dec_stable]. Qed.
Global Instance coPset_infinite_dec (X : coPset) : Decision (set_infinite X).
Proof.
split; try apply _; intros A m i; unfold dom, gmap_dom_coPset.
by rewrite elem_of_gset_to_coPset, elem_of_dom.
Qed.
refine (cast_if (decide (¬set_finite X))); by rewrite coPset_infinite_finite.
Defined.
(** * Suffix sets *)
Fixpoint coPset_suffixes_raw (p : positive) : coPset_raw :=
......@@ -410,7 +440,7 @@ Proof.
Qed.
Lemma coPset_lr_union X : coPset_l X ∪ coPset_r X = X.
Proof.
apply elem_of_equiv_L; intros p; apply eq_bool_prop_elim.
apply set_eq; intros p; apply eq_bool_prop_elim.
destruct X as [t Ht]; simpl; clear Ht; rewrite coPset_elem_of_union.
revert p; induction t as [[]|[]]; intros [?|?|]; simpl;
rewrite ?coPset_elem_of_node; simpl;
......@@ -433,3 +463,10 @@ Proof.
exists (coPset_l X), (coPset_r X); eauto 10 using coPset_lr_union,
coPset_lr_disjoint, coPset_l_finite, coPset_r_finite.
Qed.
Lemma coPset_split_infinite (X : coPset) :
set_infinite X →
∃ X1 X2, X = X1 ∪ X2 ∧ X1 ∩ X2 = ∅ ∧ set_infinite X1 ∧ set_infinite X2.
Proof.
setoid_rewrite coPset_infinite_finite.
eapply coPset_split.
Qed.
theories/countable.v → stdpp/countable.v
View file @ 9274984b
From Coq.QArith Require Import QArith_base Qcanon.
From stdpp Require Export list numbers list_numbers.
Set Default Proof Using "Type".
From stdpp Require Export list numbers list_numbers fin.
From stdpp Require Import well_founded.
From stdpp Require Import options.
Local Open Scope positive.
(** Note that [Countable A] gives rise to [EqDecision A] by checking equality of
the results of [encode]. This instance of [EqDecision A] is very inefficient, so
the native decider is typically preferred for actual computation. To avoid
overlapping instances, we include [EqDecision A] explicitly as a parameter of
[Countable A]. *)
Class Countable A `{EqDecision A} := {
encode : A → positive;
decode : positive → option A;
decode_encode x : decode (encode x) = Some x
}.
Hint Mode Countable ! - : typeclass_instances.
Arguments encode : simpl never.
Arguments decode : simpl never.
Global Hint Mode Countable ! - : typeclass_instances.
Global Arguments encode : simpl never.
Global Arguments decode : simpl never.
Instance encode_inj `{Countable A} : Inj (=) (=) (encode (A:=A)).
Global Instance encode_inj `{Countable A} : Inj (=) (=) (encode (A:=A)).
Proof.
intros x y Hxy; apply (inj Some).
by rewrite <-(decode_encode x), Hxy, decode_encode.
......@@ -22,7 +28,7 @@ Definition encode_nat `{Countable A} (x : A) : nat :=
pred (Pos.to_nat (encode x)).
Definition decode_nat `{Countable A} (i : nat) : option A :=
decode (Pos.of_nat (S i)).
Instance encode_nat_inj `{Countable A} : Inj (=) (=) (encode_nat (A:=A)).
Global Instance encode_nat_inj `{Countable A} : Inj (=) (=) (encode_nat (A:=A)).
Proof. unfold encode_nat; intros x y Hxy; apply (inj encode); lia. Qed.
Lemma decode_encode_nat `{Countable A} (x : A) : decode_nat (encode_nat x) = Some x.
Proof.
......@@ -35,7 +41,7 @@ Definition encode_Z `{Countable A} (x : A) : Z :=
Zpos (encode x).
Definition decode_Z `{Countable A} (i : Z) : option A :=
match i with Zpos i => decode i | _ => None end.
Instance encode_Z_inj `{Countable A} : Inj (=) (=) (encode_Z (A:=A)).
Global Instance encode_Z_inj `{Countable A} : Inj (=) (=) (encode_Z (A:=A)).
Proof. unfold encode_Z; intros x y Hxy; apply (inj encode); lia. Qed.
Lemma decode_encode_Z `{Countable A} (x : A) : decode_Z (encode_Z x) = Some x.
Proof. apply decode_encode. Qed.
......@@ -53,12 +59,11 @@ Section choice.
intros [x Hx]. cut (∀ i p,
i ≤ encode x → 1 + encode x = p + i → Acc choose_step p).
{ intros help. by apply (help (encode x)). }
induction i as [|i IH] using Pos.peano_ind; intros p ??.
intros i. induction i as [|i IH] using Pos.peano_ind; intros p ??.
{ constructor. intros j. assert (p = encode x) by lia; subst.
inversion 1 as [? Hd|?? Hd]; subst;
rewrite decode_encode in Hd; congruence. }
inv 1 as [? Hd|?? Hd]; rewrite decode_encode in Hd; congruence. }
constructor. intros j.
inversion 1 as [? Hd|? y Hd]; subst; auto with lia.
inv 1 as [? Hd|? y Hd]; auto with lia.
Qed.
Context `{∀ x, Decision (P x)}.
......@@ -84,6 +89,25 @@ Section choice.
Definition choice (HA : ∃ x, P x) : { x | P x } := _↾choose_correct HA.
End choice.
Section choice_proper.
Context `{Countable A}.
Context (P1 P2 : A → Prop) `{∀ x, Decision (P1 x)} `{∀ x, Decision (P2 x)}.
Context (Heq : ∀ x, P1 x ↔ P2 x).
Lemma choose_go_proper {i} (acc1 acc2 : Acc (choose_step _) i) :
choose_go P1 acc1 = choose_go P2 acc2.
Proof using Heq.
induction acc1 as [i a1 IH] using Acc_dep_ind;
destruct acc2 as [acc2]; simpl.
destruct (Some_dec _) as [[x Hx]|]; [|done].
do 2 case_decide; done || exfalso; naive_solver.
Qed.
Lemma choose_proper p1 p2 :
choose P1 p1 = choose P2 p2.
Proof using Heq. apply choose_go_proper. Qed.
End choice_proper.
Lemma surj_cancel `{Countable A} `{EqDecision B}
(f : A → B) `{!Surj (=) f} : { g : B → A & Cancel (=) f g }.
Proof.
......@@ -97,7 +121,7 @@ Section inj_countable.
Context `{Countable A, EqDecision B}.
Context (f : B → A) (g : A → option B) (fg : ∀ x, g (f x) = Some x).
Program Instance inj_countable : Countable B :=
Program Definition inj_countable : Countable B :=
{| encode y := encode (f y); decode p := x ← decode p; g x |}.
Next Obligation. intros y; simpl; rewrite decode_encode; eauto. Qed.
End inj_countable.
......@@ -106,29 +130,29 @@ Section inj_countable'.
Context `{Countable A, EqDecision B}.
Context (f : B → A) (g : A → B) (fg : ∀ x, g (f x) = x).
Program Instance inj_countable' : Countable B := inj_countable f (Some ∘ g) _.
Program Definition inj_countable' : Countable B := inj_countable f (Some ∘ g) _.
Next Obligation. intros x. by f_equal/=. Qed.
End inj_countable'.
(** ** Empty *)
Program Instance Empty_set_countable : Countable Empty_set :=
Global Program Instance Empty_set_countable : Countable Empty_set :=
{| encode u := 1; decode p := None |}.
Next Obligation. by intros []. Qed.
(** ** Unit *)
Program Instance unit_countable : Countable unit :=
Global Program Instance unit_countable : Countable unit :=
{| encode u := 1; decode p := Some () |}.
Next Obligation. by intros []. Qed.
(** ** Bool *)
Program Instance bool_countable : Countable bool := {|
Global Program Instance bool_countable : Countable bool := {|
encode b := if b then 1 else 2;
decode p := Some match p return bool with 1 => true | _ => false end
|}.
Next Obligation. by intros []. Qed.
(** ** Option *)
Program Instance option_countable `{Countable A} : Countable (option A) := {|
Global Program Instance option_countable `{Countable A} : Countable (option A) := {|
encode o := match o with None => 1 | Some x => Pos.succ (encode x) end;
decode p := if decide (p = 1) then Some None else Some <$> decode (Pos.pred p)
|}.
......@@ -138,7 +162,7 @@ Next Obligation.
Qed.
(** ** Sums *)
Program Instance sum_countable `{Countable A} `{Countable B} :
Global Program Instance sum_countable `{Countable A} `{Countable B} :
Countable (A + B)%type := {|
encode xy :=
match xy with inl x => (encode x)~0 | inr y => (encode y)~1 end;
......@@ -211,7 +235,7 @@ Proof.
{ intros p'. by induction p'; simplify_option_eq. }
revert q. by induction p; intros [?|?|]; simplify_option_eq.
Qed.
Program Instance prod_countable `{Countable A} `{Countable B} :
Global Program Instance prod_countable `{Countable A} `{Countable B} :
Countable (A * B)%type := {|
encode xy := prod_encode (encode (xy.1)) (encode (xy.2));
decode p :=
......@@ -238,9 +262,9 @@ Next Obligation.
Qed.
(** ** Numbers *)
Instance pos_countable : Countable positive :=
Global Instance pos_countable : Countable positive :=
{| encode := id; decode := Some; decode_encode x := eq_refl |}.
Program Instance N_countable : Countable N := {|
Global Program Instance N_countable : Countable N := {|
encode x := match x with N0 => 1 | Npos p => Pos.succ p end;
decode p := if decide (p = 1) then Some 0%N else Some (Npos (Pos.pred p))
|}.
......@@ -248,12 +272,12 @@ Next Obligation.
intros [|p]; simpl; [done|].
by rewrite decide_False, Pos.pred_succ by (by destruct p).
Qed.
Program Instance Z_countable : Countable Z := {|
Global Program Instance Z_countable : Countable Z := {|
encode x := match x with Z0 => 1 | Zpos p => p~0 | Zneg p => p~1 end;
decode p := Some match p with 1 => Z0 | p~0 => Zpos p | p~1 => Zneg p end
|}.
Next Obligation. by intros [|p|p]. Qed.
Program Instance nat_countable : Countable nat :=
Global Program Instance nat_countable : Countable nat :=
{| encode x := encode (N.of_nat x); decode p := N.to_nat <$> decode p |}.
Next Obligation.
by intros x; lazy beta; rewrite decode_encode; csimpl; rewrite Nat2N.id.
......@@ -269,23 +293,45 @@ Qed.
Global Program Instance Qp_countable : Countable Qp :=
inj_countable
Qp_car
(λ p : Qc, guard (0 < p)%Qc as Hp; Some (mk_Qp p Hp)) _.
Qp_to_Qc
(λ p : Qc, Hp ← guard (0 < p)%Qc; Some (mk_Qp p Hp)) _.
Next Obligation.
intros [p Hp]. case_guard; simplify_eq/=; [|done].
f_equal. by apply Qp.to_Qc_inj_iff.
Qed.
Global Program Instance fin_countable n : Countable (fin n) :=
inj_countable
fin_to_nat
(λ m : nat, Hm ← guard (m < n)%nat; Some (nat_to_fin Hm)) _.
Next Obligation.
intros [p Hp]. unfold mguard, option_guard; simpl.
case_match; [|done]. f_equal. by apply Qp_eq.
intros n i; simplify_option_eq.
- by rewrite nat_to_fin_to_nat.
- by pose proof (fin_to_nat_lt i).
Qed.
(** ** Generic trees *)
Local Close Scope positive.
(** This type can help you construct a [Countable] instance for an arbitrary
(even recursive) inductive datatype. The idea is tht you make [T] something like
[T1 + T2 + ...], covering all the data types that can be contained inside your
type.
- Each non-recursive constructor to a [GenLeaf]. Different constructors must use
different variants of [T] to ensure they remain distinguishable!
- Each recursive constructor to a [GenNode] where the [nat] is a (typically
small) constant representing the constructor itself, and then all the data in
the constructor (recursive or otherwise) is put into child nodes.
This data type is the same as [GenTree.tree] in mathcomp, see
https://github.com/math-comp/math-comp/blob/master/ssreflect/choice.v *)
Inductive gen_tree (T : Type) : Type :=
| GenLeaf : T → gen_tree T
| GenNode : nat → list (gen_tree T) → gen_tree T.
Arguments GenLeaf {_} _ : assert.
Arguments GenNode {_} _ _ : assert.
Global Arguments GenLeaf {_} _ : assert.
Global Arguments GenNode {_} _ _ : assert.
Instance gen_tree_dec `{EqDecision T} : EqDecision (gen_tree T).
Global Instance gen_tree_dec `{EqDecision T} : EqDecision (gen_tree T).
Proof.
refine (
fix go t1 t2 := let _ : EqDecision _ := @go in
......@@ -320,13 +366,22 @@ Proof.
- rewrite <-(assoc_L _). revert k. generalize ([inl (length ts, n)] ++ l).
induction ts as [|t ts'' IH]; intros k ts'''; csimpl; auto.
rewrite reverse_cons, <-!(assoc_L _), FIX; simpl; auto.
- simpl. by rewrite take_app_alt, drop_app_alt, reverse_involutive
by (by rewrite reverse_length).
- simpl. by rewrite take_app_length', drop_app_length', reverse_involutive
by (by rewrite length_reverse).
Qed.
Program Instance gen_tree_countable `{Countable T} : Countable (gen_tree T) :=
Global Program Instance gen_tree_countable `{Countable T} : Countable (gen_tree T) :=
inj_countable gen_tree_to_list (gen_tree_of_list []) _.
Next Obligation.
intros T ?? t.
by rewrite <-(right_id_L [] _ (gen_tree_to_list _)), gen_tree_of_to_list.
Qed.
(** ** Sigma *)
Global Program Instance countable_sig `{Countable A} (P : A → Prop)
`{!∀ x, Decision (P x), !∀ x, ProofIrrel (P x)} :
Countable { x : A | P x } :=
inj_countable proj1_sig (λ x, Hx ← guard (P x); Some (x ↾ Hx)) _.
Next Obligation.
intros A ?? P ?? [x Hx]. by erewrite (option_guard_True_pi (P x)).
Qed.
theories/decidable.v → stdpp/decidable.v
View file @ 9274984b
......@@ -2,14 +2,17 @@
with a decidable equality. Such propositions are collected by the [Decision]
type class. *)
From stdpp Require Export proof_irrel.
From stdpp Require Import options.
(* Pick up extra assumptions from section parameters. *)
Set Default Proof Using "Type*".
Lemma dec_stable `{Decision P} : ¬¬P → P.
Proof. firstorder. Qed.
Lemma Is_true_reflect (b : bool) : reflect b b.
Proof. destruct b. left; constructor. right. intros []. Qed.
Instance: Inj (=) (↔) Is_true.
Proof. destruct b; [left; constructor | right; intros []]. Qed.
Global Instance: Inj (=) (↔) Is_true.
Proof. intros [] []; simpl; intuition. Qed.
Lemma decide_True {A} `{Decision P} (x y : A) :
......@@ -18,13 +21,13 @@ Proof. destruct (decide P); tauto. Qed.
Lemma decide_False {A} `{Decision P} (x y : A) :
¬P → (if decide P then x else y) = y.
Proof. destruct (decide P); tauto. Qed.
Lemma decide_iff {A} P Q `{Decision P, Decision Q} (x y : A) :
Lemma decide_ext {A} P Q `{Decision P, Decision Q} (x y : A) :
(P ↔ Q) → (if decide P then x else y) = (if decide Q then x else y).
Proof. intros [??]. destruct (decide P), (decide Q); tauto. Qed.
Lemma decide_left `{Decision P, !ProofIrrel P} (HP : P) : decide P = left HP.
Lemma decide_True_pi `{Decision P, !ProofIrrel P} (HP : P) : decide P = left HP.
Proof. destruct (decide P); [|contradiction]. f_equal. apply proof_irrel. Qed.
Lemma decide_right `{Decision P, !ProofIrrel (¬ P)} (HP : ¬ P) : decide P = right HP.
Lemma decide_False_pi `{Decision P, !ProofIrrel (¬ P)} (HP : ¬ P) : decide P = right HP.
Proof. destruct (decide P); [contradiction|]. f_equal. apply proof_irrel. Qed.
(** The tactic [destruct_decide] destructs a sumbool [dec]. If one of the
......@@ -82,6 +85,79 @@ 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 _).
(** * Instances of [Decision] *)
(** Instances of [Decision] for operators of propositional logic. *)
(** The instances for [True] and [False] have a very high cost. If they are
applied too eagerly, HO-unification could wrongfully instantiate TC instances
with [λ .., True] or [λ .., False].
See https://gitlab.mpi-sws.org/iris/stdpp/-/issues/165 *)
Global Instance True_dec: Decision True | 1000 := left I.
Global Instance False_dec: Decision False | 1000 := right (False_rect False).
Global Instance Is_true_dec b : Decision (Is_true b).
Proof. destruct b; simpl; apply _. Defined.
Section prop_dec.
Context `(P_dec : Decision P) `(Q_dec : Decision Q).
Global Instance not_dec: Decision (¬P).
Proof. refine (cast_if_not P_dec); intuition. Defined.
Global Instance and_dec: Decision (P ∧ Q).
Proof. refine (cast_if_and P_dec Q_dec); intuition. Defined.
Global Instance or_dec: Decision (P ∨ Q).
Proof. refine (cast_if_or P_dec Q_dec); intuition. Defined.
Global Instance impl_dec: Decision (P → Q).
Proof. refine (if P_dec then cast_if Q_dec else left _); intuition. Defined.
End prop_dec.
Global Instance iff_dec `(P_dec : Decision P) `(Q_dec : Decision Q) :
Decision (P ↔ Q) := and_dec _ _.
(** Instances of [Decision] for common data types. *)
Global Instance bool_eq_dec : EqDecision bool.
Proof. solve_decision. Defined.
Global Instance unit_eq_dec : EqDecision unit.
Proof. solve_decision. Defined.
Global Instance Empty_set_eq_dec : EqDecision Empty_set.
Proof. solve_decision. Defined.
Global Instance prod_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A * B).
Proof. solve_decision. Defined.
Global Instance sum_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A + B).
Proof. solve_decision. Defined.
Global Instance uncurry_dec `(P_dec : ∀ (x : A) (y : B), Decision (P x y)) p :
Decision (uncurry P p) :=
match p as p return Decision (uncurry P p) with
| (x,y) => P_dec x y
end.
Global Instance sig_eq_dec `(P : A → Prop) `{∀ x, ProofIrrel (P x), EqDecision A} :
EqDecision (sig P).
Proof.
refine (λ x y, cast_if (decide (`x = `y))); rewrite sig_eq_pi; trivial.
Defined.
(** Some laws for decidable propositions *)
Lemma not_and_l {P Q : Prop} `{Decision P} : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q.
Proof. destruct (decide P); tauto. Qed.
Lemma not_and_r {P Q : Prop} `{Decision Q} : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q.
Proof. destruct (decide Q); tauto. Qed.
Lemma not_and_l_alt {P Q : Prop} `{Decision P} : ¬(P ∧ Q) ↔ ¬P ∨ (¬Q ∧ P).
Proof. destruct (decide P); tauto. Qed.
Lemma not_and_r_alt {P Q : Prop} `{Decision Q} : ¬(P ∧ Q) ↔ (¬P ∧ Q) ∨ ¬Q.
Proof. destruct (decide Q); tauto. Qed.
Program Definition inj_eq_dec `{EqDecision A} {B} (f : B → A)
`{!Inj (=) (=) f} : EqDecision B := λ x y, cast_if (decide (f x = f y)).
Solve Obligations with firstorder congruence.
(** * Instances of [RelDecision] *)
Definition flip_dec {A} (R : relation A) `{!RelDecision R} :
RelDecision (flip R) := λ x y, decide_rel R y x.
(** We do not declare this as an actual instance since Coq can unify [flip ?R]
with any relation. Coq's standard library is carrying out the same approach for
the [Reflexive], [Transitive], etc, instance of [flip]. *)
Global Hint Extern 3 (RelDecision (flip _)) => apply flip_dec : typeclass_instances.
(** We can convert decidable propositions to booleans. *)
Definition bool_decide (P : Prop) {dec : Decision P} : bool :=
if dec then true else false.
......@@ -96,7 +172,7 @@ Lemma decide_bool_decide P {Hdec: Decision P} {X : Type} (x1 x2 : X):
(if decide P then x1 else x2) = (if bool_decide P then x1 else x2).
Proof. unfold bool_decide, decide. destruct Hdec; reflexivity. Qed.
Tactic Notation "case_bool_decide" "as" ident (Hd) :=
Tactic Notation "case_bool_decide" "as" ident(Hd) :=
match goal with
| H : context [@bool_decide ?P ?dec] |- _ =>
destruct_decide (@bool_decide_reflect P dec) as Hd
......@@ -112,15 +188,15 @@ Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P → P.
Proof. rewrite bool_decide_spec; trivial. Qed.
Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P → bool_decide P.
Proof. rewrite bool_decide_spec; trivial. Qed.
Hint Resolve bool_decide_pack : core.
Global Hint Resolve bool_decide_pack : core.
Lemma bool_decide_eq_true (P : Prop) `{Decision P} : bool_decide P = true ↔ P.
Proof. case_bool_decide; intuition discriminate. Qed.
Lemma bool_decide_eq_false (P : Prop) `{Decision P} : bool_decide P = false ↔ ¬P.
Proof. case_bool_decide; intuition discriminate. Qed.
Lemma bool_decide_iff (P Q : Prop) `{Decision P, Decision Q} :
Lemma bool_decide_ext (P Q : Prop) `{Decision P, Decision Q} :
(P ↔ Q) → bool_decide P = bool_decide Q.
Proof. repeat case_bool_decide; tauto. Qed.
Proof. apply decide_ext. Qed.
Lemma bool_decide_eq_true_1 P `{!Decision P}: bool_decide P = true → P.
Proof. apply bool_decide_eq_true. Qed.
......@@ -132,6 +208,40 @@ Proof. apply bool_decide_eq_false. Qed.
Lemma bool_decide_eq_false_2 P `{!Decision P}: ¬P → bool_decide P = false.
Proof. apply bool_decide_eq_false. Qed.
Lemma bool_decide_True : bool_decide True = true.
Proof. reflexivity. Qed.
Lemma bool_decide_False : bool_decide False = false.
Proof. reflexivity. Qed.
Lemma bool_decide_not P `{Decision P} :
bool_decide (¬ P) = negb (bool_decide P).
Proof. repeat case_bool_decide; intuition. Qed.
Lemma bool_decide_or P Q `{Decision P, Decision Q} :
bool_decide (P ∨ Q) = bool_decide P || bool_decide Q.
Proof. repeat case_bool_decide; intuition. Qed.
Lemma bool_decide_and P Q `{Decision P, Decision Q} :
bool_decide (P ∧ Q) = bool_decide P && bool_decide Q.
Proof. repeat case_bool_decide; intuition. Qed.
Lemma bool_decide_impl P Q `{Decision P, Decision Q} :
bool_decide (P → Q) = implb (bool_decide P) (bool_decide Q).
Proof. repeat case_bool_decide; intuition. Qed.
Lemma bool_decide_iff P Q `{Decision P, Decision Q} :
bool_decide (P ↔ Q) = eqb (bool_decide P) (bool_decide Q).
Proof. repeat case_bool_decide; intuition. Qed.
(** The tactic [compute_done] solves the following kinds of goals:
- Goals [P] where [Decidable P] can be derived.
- Goals that compute to [True] or [x = x].
The goal must be a ground term for this, i.e., not contain variables (that do
not compute away). The goal is solved by using [vm_compute] and then using a
trivial proof term ([I]/[eq_refl]). *)
Tactic Notation "compute_done" :=
try apply (bool_decide_unpack _);
vm_compute;
first [ exact I | exact eq_refl ].
Tactic Notation "compute_by" tactic(tac) :=
tac; compute_done.
(** Backwards compatibility notations. *)
Notation bool_decide_true := bool_decide_eq_true_2.
Notation bool_decide_false := bool_decide_eq_false_2.
......@@ -154,71 +264,3 @@ Proof. apply (sig_eq_pi _). Qed.
Lemma dexists_proj1 `(P : A → Prop) `{∀ x, Decision (P x)} (x : dsig P) p :
dexist (`x) p = x.
Proof. apply dsig_eq; reflexivity. Qed.
(** * Instances of [Decision] *)
(** Instances of [Decision] for operators of propositional logic. *)
Instance True_dec: Decision True := left I.
Instance False_dec: Decision False := right (False_rect False).
Instance Is_true_dec b : Decision (Is_true b).
Proof. destruct b; simpl; apply _. Defined.
Section prop_dec.
Context `(P_dec : Decision P) `(Q_dec : Decision Q).
Global Instance not_dec: Decision (¬P).
Proof. refine (cast_if_not P_dec); intuition. Defined.
Global Instance and_dec: Decision (P ∧ Q).
Proof. refine (cast_if_and P_dec Q_dec); intuition. Defined.
Global Instance or_dec: Decision (P ∨ Q).
Proof. refine (cast_if_or P_dec Q_dec); intuition. Defined.
Global Instance impl_dec: Decision (P → Q).
Proof. refine (if P_dec then cast_if Q_dec else left _); intuition. Defined.
End prop_dec.
Instance iff_dec `(P_dec : Decision P) `(Q_dec : Decision Q) :
Decision (P ↔ Q) := and_dec _ _.
(** Instances of [Decision] for common data types. *)
Instance bool_eq_dec : EqDecision bool.
Proof. solve_decision. Defined.
Instance unit_eq_dec : EqDecision unit.
Proof. solve_decision. Defined.
Instance Empty_set_eq_dec : EqDecision Empty_set.
Proof. solve_decision. Defined.
Instance prod_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A * B).
Proof. solve_decision. Defined.
Instance sum_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A + B).
Proof. solve_decision. Defined.
Instance curry_dec `(P_dec : ∀ (x : A) (y : B), Decision (P x y)) p :
Decision (curry P p) :=
match p as p return Decision (curry P p) with
| (x,y) => P_dec x y
end.
Instance sig_eq_dec `(P : A → Prop) `{∀ x, ProofIrrel (P x), EqDecision A} :
EqDecision (sig P).
Proof.
refine (λ x y, cast_if (decide (`x = `y))); rewrite sig_eq_pi; trivial.
Defined.
(** Some laws for decidable propositions *)
Lemma not_and_l {P Q : Prop} `{Decision P} : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q.
Proof. destruct (decide P); tauto. Qed.
Lemma not_and_r {P Q : Prop} `{Decision Q} : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q.
Proof. destruct (decide Q); tauto. Qed.
Lemma not_and_l_alt {P Q : Prop} `{Decision P} : ¬(P ∧ Q) ↔ ¬P ∨ (¬Q ∧ P).
Proof. destruct (decide P); tauto. Qed.
Lemma not_and_r_alt {P Q : Prop} `{Decision Q} : ¬(P ∧ Q) ↔ (¬P ∧ Q) ∨ ¬Q.
Proof. destruct (decide Q); tauto. Qed.
Program Definition inj_eq_dec `{EqDecision A} {B} (f : B → A)
`{!Inj (=) (=) f} : EqDecision B := λ x y, cast_if (decide (f x = f y)).
Solve Obligations with firstorder congruence.
(** * Instances of [RelDecision] *)
Definition flip_dec {A} (R : relation A) `{!RelDecision R} :
RelDecision (flip R) := λ x y, decide_rel R y x.
(** We do not declare this as an actual instance since Coq can unify [flip ?R]
with any relation. Coq's standard library is carrying out the same approach for
the [Reflexive], [Transitive], etc, instance of [flip]. *)
Hint Extern 3 (RelDecision (flip _)) => apply flip_dec : typeclass_instances.
stdpp/dune 0 → 100644
View file @ 9274984b
(include_subdirs qualified)
(coq.theory
(name stdpp)
(package coq-stdpp))
theories/fin.v → stdpp/fin.v
View file @ 9274984b
......@@ -3,7 +3,7 @@
renames or changes their notations, so that it becomes more consistent with the
naming conventions in this development. *)
From stdpp Require Export base tactics.
Set Default Proof Using "Type".
From stdpp Require Import options.
(** * The fin type *)
(** The type [fin n] represents natural numbers [i] with [0 ≤ i < n]. We
......@@ -15,15 +15,15 @@ ambiguity. *)
Notation fin := Fin.t.
Notation FS := Fin.FS.
Declare Scope fin_scope.
Delimit Scope fin_scope with fin.
Arguments Fin.FS _ _%fin : assert.
Bind Scope fin_scope with fin.
Global Arguments Fin.FS _ _%fin : assert.
Notation "0" := Fin.F1 : fin_scope. Notation "1" := (FS 0) : fin_scope.
Notation "2" := (FS 1) : fin_scope. Notation "3" := (FS 2) : fin_scope.
Notation "4" := (FS 3) : fin_scope. Notation "5" := (FS 4) : fin_scope.
Notation "6" := (FS 5) : fin_scope. Notation "7" := (FS 6) : fin_scope.
Notation "8" := (FS 7) : fin_scope. Notation "9" := (FS 8) : fin_scope.
Notation "10" := (FS 9) : fin_scope.
(** Allow any non-negative number literal to be parsed as a [fin]. For example
[42%fin : fin 64], or [42%fin : fin _], or [42%fin : fin (43 + _)]. *)
Number Notation fin Nat.of_num_uint Nat.to_num_uint (via nat
mapping [[Fin.F1] => O, [Fin.FS] => S]) : fin_scope.
Fixpoint fin_to_nat {n} (i : fin n) : nat :=
match i with 0%fin => 0 | FS i => S (fin_to_nat i) end.
......@@ -32,7 +32,7 @@ Coercion fin_to_nat : fin >-> nat.
Notation nat_to_fin := Fin.of_nat_lt.
Notation fin_rect2 := Fin.rect2.
Instance fin_dec {n} : EqDecision (fin n).
Global Instance fin_dec {n} : EqDecision (fin n).
Proof.
refine (fin_rect2
(λ n (i j : fin n), { i = j } + { i ≠ j })
......@@ -64,17 +64,19 @@ Ltac inv_fin i :=
| fin ?n =>
match eval hnf in n with
| 0 =>
revert dependent i; match goal with |- ∀ i, @?P i => apply (fin_0_inv P) end
generalize dependent i;
match goal with |- ∀ i, @?P i => apply (fin_0_inv P) end
| S ?n =>
revert dependent i; match goal with |- ∀ i, @?P i => apply (fin_S_inv P) end
generalize dependent i;
match goal with |- ∀ i, @?P i => apply (fin_S_inv P) end
end
end.
Instance FS_inj: Inj (=) (=) (@FS n).
Proof. intros n i j. apply Fin.FS_inj. Qed.
Instance fin_to_nat_inj : Inj (=) (=) (@fin_to_nat n).
Global Instance FS_inj {n} : Inj (=) (=) (@FS n).
Proof. intros i j. apply Fin.FS_inj. Qed.
Global Instance fin_to_nat_inj {n} : Inj (=) (=) (@fin_to_nat n).
Proof.
intros n i. induction i; intros j; inv_fin j; intros; f_equal/=; auto with lia.
intros i. induction i; intros j; inv_fin j; intros; f_equal/=; auto with lia.
Qed.
Lemma fin_to_nat_lt {n} (i : fin n) : fin_to_nat i < n.
......@@ -86,26 +88,26 @@ Qed.
Lemma nat_to_fin_to_nat {n} (i : fin n) H : @nat_to_fin (fin_to_nat i) n H = i.
Proof. apply (inj fin_to_nat), fin_to_nat_to_fin. Qed.
Fixpoint fin_plus_inv {n1 n2} : ∀ (P : fin (n1 + n2) → Type)
Fixpoint fin_add_inv {n1 n2} : ∀ (P : fin (n1 + n2) → Type)
(H1 : ∀ i1 : fin n1, P (Fin.L n2 i1))
(H2 : ∀ i2, P (Fin.R n1 i2)) (i : fin (n1 + n2)), P i :=
match n1 with
| 0 => λ P H1 H2 i, H2 i
| S n => λ P H1 H2, fin_S_inv P (H1 0%fin) (fin_plus_inv _ (λ i, H1 (FS i)) H2)
| S n => λ P H1 H2, fin_S_inv P (H1 0%fin) (fin_add_inv _ (λ i, H1 (FS i)) H2)
end.
Lemma fin_plus_inv_L {n1 n2} (P : fin (n1 + n2) → Type)
Lemma fin_add_inv_l {n1 n2} (P : fin (n1 + n2) → Type)
(H1: ∀ i1 : fin n1, P (Fin.L _ i1)) (H2: ∀ i2, P (Fin.R _ i2)) (i: fin n1) :
fin_plus_inv P H1 H2 (Fin.L n2 i) = H1 i.
fin_add_inv P H1 H2 (Fin.L n2 i) = H1 i.
Proof.
revert P H1 H2 i.
induction n1 as [|n1 IH]; intros P H1 H2 i; inv_fin i; simpl; auto.
intros i. apply (IH (λ i, P (FS i))).
Qed.
Lemma fin_plus_inv_R {n1 n2} (P : fin (n1 + n2) → Type)
Lemma fin_add_inv_r {n1 n2} (P : fin (n1 + n2) → Type)
(H1: ∀ i1 : fin n1, P (Fin.L _ i1)) (H2: ∀ i2, P (Fin.R _ i2)) (i: fin n2) :
fin_plus_inv P H1 H2 (Fin.R n1 i) = H2 i.
fin_add_inv P H1 H2 (Fin.R n1 i) = H2 i.
Proof.
revert P H1 H2 i; induction n1 as [|n1 IH]; intros P H1 H2 i; simpl; auto.
apply (IH (λ i, P (FS i))).
......
theories/fin_maps.v → stdpp/fin_maps.v
View file @ 9274984b
This diff is collapsed.
theories/fin_sets.v → stdpp/fin_sets.v
View file @ 9274984b
This diff is collapsed.
theories/finite.v → stdpp/finite.v
View file @ 9274984b
From stdpp Require Export countable vector.
Set Default Proof Using "Type".
From stdpp Require Import options.
Class Finite A `{EqDecision A} := {
enum : list A;
......@@ -7,11 +7,11 @@ Class Finite A `{EqDecision A} := {
NoDup_enum : NoDup enum;
elem_of_enum x : x ∈ enum
}.
Hint Mode Finite ! - : typeclass_instances.
Arguments enum : clear implicits.
Arguments enum _ {_ _} : assert.
Arguments NoDup_enum : clear implicits.
Arguments NoDup_enum _ {_ _} : assert.
Global Hint Mode Finite ! - : typeclass_instances.
Global Arguments enum : clear implicits.
Global Arguments enum _ {_ _} : assert.
Global Arguments NoDup_enum : clear implicits.
Global Arguments NoDup_enum _ {_ _} : assert.
Definition card A `{Finite A} := length (enum A).
Program Definition finite_countable `{Finite A} : Countable A := {|
......@@ -19,16 +19,15 @@ Program Definition finite_countable `{Finite A} : Countable A := {|
Pos.of_nat $ S $ default 0 $ fst <$> list_find (x =.) (enum A);
decode := λ p, enum A !! pred (Pos.to_nat p)
|}.
Arguments Pos.of_nat : simpl never.
Next Obligation.
intros ?? [xs Hxs HA] x; unfold encode, decode; simpl.
destruct (list_find_elem_of (x =.) xs x) as [[i y] Hi]; auto.
rewrite Nat2Pos.id by done; simpl; rewrite Hi; simpl.
destruct (list_find_Some (x =.) xs i y); naive_solver.
Qed.
Hint Immediate finite_countable : typeclass_instances.
Global Hint Immediate finite_countable : typeclass_instances.
Definition find `{Finite A} P `{∀ x, Decision (P x)} : option A :=
Definition find `{Finite A} (P : A → Prop) `{∀ x, Decision (P x)} : option A :=
list_find P (enum A) ≫= decode_nat ∘ fst.
Lemma encode_lt_card `{finA: Finite A} (x : A) : encode_nat x < card A.
......@@ -37,7 +36,8 @@ Proof.
rewrite Nat2Pos.id by done; simpl.
destruct (list_find _ xs) as [[i y]|] eqn:HE; simpl.
- apply list_find_Some in HE as (?&?&?); eauto using lookup_lt_Some.
- destruct xs; simpl. exfalso; eapply not_elem_of_nil, (HA x). lia.
- destruct xs; simpl; [|lia].
exfalso; eapply not_elem_of_nil, (HA x).
Qed.
Lemma encode_decode A `{finA: Finite A} i :
i < card A → ∃ x : A, decode_nat i = Some x ∧ encode_nat x = i.
......@@ -50,7 +50,7 @@ Proof.
split; [done|]; rewrite Hj; simpl.
apply list_find_Some in Hj as (?&->&?). eauto using NoDup_lookup.
Qed.
Lemma find_Some `{finA: Finite A} P `{∀ x, Decision (P x)} (x : A) :
Lemma find_Some `{finA: Finite A} (P : A → Prop) `{∀ x, Decision (P x)} (x : A) :
find P = Some x → P x.
Proof.
destruct finA as [xs Hxs HA]; unfold find, decode_nat, decode; simpl.
......@@ -58,13 +58,13 @@ Proof.
rewrite !Nat2Pos.id in Hx by done.
destruct (list_find_Some P xs i y); naive_solver.
Qed.
Lemma find_is_Some `{finA: Finite A} P `{∀ x, Decision (P x)} (x : A) :
Lemma find_is_Some `{finA: Finite A} (P : A → Prop) `{∀ x, Decision (P x)} (x : A) :
P x → ∃ y, find P = Some y ∧ P y.
Proof.
destruct finA as [xs Hxs HA]; unfold find, decode; simpl.
intros Hx. destruct (list_find_elem_of P xs x) as [[i y] Hi]; auto.
rewrite Hi; simpl. rewrite !Nat2Pos.id by done. simpl.
apply list_find_Some in Hi; naive_solver.
rewrite Hi; unfold decode_nat, decode; simpl. rewrite !Nat2Pos.id by done.
simpl. apply list_find_Some in Hi; naive_solver.
Qed.
Definition encode_fin `{Finite A} (x : A) : fin (card A) :=
......@@ -118,9 +118,9 @@ Qed.
Lemma finite_inj_Permutation `{Finite A} `{Finite B} (f : A → B)
`{!Inj (=) (=) f} : card A = card B → f <$> enum A ≡ₚ enum B.
Proof.
intros. apply submseteq_Permutation_length_eq.
- by rewrite fmap_length.
intros. apply submseteq_length_Permutation.
- by apply finite_inj_submseteq.
- rewrite length_fmap. by apply Nat.eq_le_incl.
Qed.
Lemma finite_inj_surj `{Finite A} `{Finite B} (f : A → B)
`{!Inj (=) (=) f} : card A = card B → Surj (=) f.
......@@ -146,7 +146,7 @@ Proof.
{ exists (card_0_inv B HA). intros y. apply (card_0_inv _ HA y). }
destruct (finite_surj A B) as (g&?); auto with lia.
destruct (surj_cancel g) as (f&?). exists f. apply cancel_inj.
- intros [f ?]. unfold card. rewrite <-(fmap_length f).
- intros [f ?]. unfold card. rewrite <-(length_fmap f).
by apply submseteq_length, (finite_inj_submseteq f).
Qed.
Lemma finite_bijective A `{Finite A} B `{Finite B} :
......@@ -203,7 +203,7 @@ Section enc_finite.
Context (to_nat_c : ∀ x, to_nat x < c).
Context (to_of_nat : ∀ i, i < c → to_nat (of_nat i) = i).
Program Instance enc_finite : Finite A := {| enum := of_nat <$> seq 0 c |}.
Local Program Instance enc_finite : Finite A := {| enum := of_nat <$> seq 0 c |}.
Next Obligation.
apply NoDup_alt. intros i j x. rewrite !list_lookup_fmap. intros Hi Hj.
destruct (seq _ _ !! i) as [i'|] eqn:Hi',
......@@ -216,21 +216,41 @@ Section enc_finite.
split; auto. by apply elem_of_list_lookup_2 with (to_nat x), lookup_seq.
Qed.
Lemma enc_finite_card : card A = c.
Proof. unfold card. simpl. by rewrite fmap_length, seq_length. Qed.
Proof. unfold card. simpl. by rewrite length_fmap, length_seq. Qed.
End enc_finite.
(** If we have a surjection [f : A → B] and [A] is finite, then [B] is finite
too. The surjection [f] could map multiple [x : A] on the same [B], so we
need to remove duplicates in [enum]. If [f] is injective, we do not need to do that,
leading to a potentially faster implementation of [enum], see [bijective_finite]
below. *)
Section surjective_finite.
Context `{Finite A, EqDecision B} (f : A → B).
Context `{!Surj (=) f}.
Program Definition surjective_finite: Finite B :=
{| enum := remove_dups (f <$> enum A) |}.
Next Obligation. apply NoDup_remove_dups. Qed.
Next Obligation.
intros y. rewrite elem_of_remove_dups, elem_of_list_fmap.
destruct (surj f y). eauto using elem_of_enum.
Qed.
End surjective_finite.
Section bijective_finite.
Context `{Finite A, EqDecision B} (f : A → B) (g : B → A).
Context `{!Inj (=) (=) f, !Cancel (=) f g}.
Context `{Finite A, EqDecision B} (f : A → B).
Context `{!Inj (=) (=) f, !Surj (=) f}.
Program Instance bijective_finite: Finite B := {| enum := f <$> enum A |}.
Next Obligation. apply (NoDup_fmap_2 _), NoDup_enum. Qed.
Program Definition bijective_finite : Finite B :=
{| enum := f <$> enum A |}.
Next Obligation. apply (NoDup_fmap f), NoDup_enum. Qed.
Next Obligation.
intros y. rewrite elem_of_list_fmap. eauto using elem_of_enum.
intros b. rewrite elem_of_list_fmap. destruct (surj f b).
eauto using elem_of_enum.
Qed.
End bijective_finite.
Program Instance option_finite `{Finite A} : Finite (option A) :=
Global Program Instance option_finite `{Finite A} : Finite (option A) :=
{| enum := None :: (Some <$> enum A) |}.
Next Obligation.
constructor.
......@@ -242,29 +262,29 @@ Next Obligation.
apply elem_of_list_fmap. eauto using elem_of_enum.
Qed.
Lemma option_cardinality `{Finite A} : card (option A) = S (card A).
Proof. unfold card. simpl. by rewrite fmap_length. Qed.
Proof. unfold card. simpl. by rewrite length_fmap. Qed.
Program Instance Empty_set_finite : Finite Empty_set := {| enum := [] |}.
Global Program Instance Empty_set_finite : Finite Empty_set := {| enum := [] |}.
Next Obligation. by apply NoDup_nil. Qed.
Next Obligation. intros []. Qed.
Lemma Empty_set_card : card Empty_set = 0.
Proof. done. Qed.
Program Instance unit_finite : Finite () := {| enum := [tt] |}.
Global Program Instance unit_finite : Finite () := {| enum := [tt] |}.
Next Obligation. apply NoDup_singleton. Qed.
Next Obligation. intros []. by apply elem_of_list_singleton. Qed.
Lemma unit_card : card unit = 1.
Proof. done. Qed.
Program Instance bool_finite : Finite bool := {| enum := [true; false] |}.
Global Program Instance bool_finite : Finite bool := {| enum := [true; false] |}.
Next Obligation.
constructor. by rewrite elem_of_list_singleton. apply NoDup_singleton.
constructor; [ by rewrite elem_of_list_singleton | apply NoDup_singleton ].
Qed.
Next Obligation. intros [|]. left. right; left. Qed.
Next Obligation. intros [|]; [ left | right; left ]. Qed.
Lemma bool_card : card bool = 2.
Proof. done. Qed.
Program Instance sum_finite `{Finite A, Finite B} : Finite (A + B)%type :=
Global Program Instance sum_finite `{Finite A, Finite B} : Finite (A + B)%type :=
{| enum := (inl <$> enum A) ++ (inr <$> enum B) |}.
Next Obligation.
intros. apply NoDup_app; split_and?.
......@@ -277,79 +297,68 @@ Next Obligation.
[left|right]; (eexists; split; [done|apply elem_of_enum]).
Qed.
Lemma sum_card `{Finite A, Finite B} : card (A + B) = card A + card B.
Proof. unfold card. simpl. by rewrite app_length, !fmap_length. Qed.
Proof. unfold card. simpl. by rewrite length_app, !length_fmap. Qed.
Program Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type :=
{| enum := foldr (λ x, (pair x <$> enum B ++.)) [] (enum A) |}.
Global Program Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type :=
{| enum := a ← enum A; (a,.) <$> enum B |}.
Next Obligation.
intros ??????. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl.
{ constructor. }
apply NoDup_app; split_and?.
- by apply (NoDup_fmap_2 _), NoDup_enum.
- intros [? y]. rewrite elem_of_list_fmap. intros (?&?&?); simplify_eq.
clear IH. induction Hxs as [|x' xs ?? IH]; simpl.
{ rewrite elem_of_nil. tauto. }
rewrite elem_of_app, elem_of_list_fmap.
intros [(?&?&?)|?]; simplify_eq.
+ destruct Hx. by left.
+ destruct IH. by intro; destruct Hx; right. auto.
- done.
intros A ?????. apply NoDup_bind.
- intros a1 a2 [a b] ?? (?&?&_)%elem_of_list_fmap (?&?&_)%elem_of_list_fmap.
naive_solver.
- intros a ?. rewrite (NoDup_fmap _). apply NoDup_enum.
- apply NoDup_enum.
Qed.
Next Obligation.
intros ?????? [x y]. induction (elem_of_enum x); simpl.
- rewrite elem_of_app, !elem_of_list_fmap. eauto using elem_of_enum.
- rewrite elem_of_app; eauto.
intros ?????? [a b]. apply elem_of_list_bind.
exists a. eauto using elem_of_enum, elem_of_list_fmap_1.
Qed.
Lemma prod_card `{Finite A} `{Finite B} : card (A * B) = card A * card B.
Proof.
unfold card; simpl. induction (enum A); simpl; auto.
rewrite app_length, fmap_length. auto.
rewrite length_app, length_fmap. auto.
Qed.
Definition list_enum {A} (l : list A) : ∀ n, list { l : list A | length l = n } :=
fix go n :=
Fixpoint vec_enum {A} (l : list A) (n : nat) : list (vec A n) :=
match n with
| 0 => [[]↾eq_refl]
| S n => foldr (λ x, (sig_map (x ::.) (λ _ H, f_equal S H) <$> (go n) ++.)) [] l
| 0 => [[#]]
| S m => a ← l; vcons a <$> vec_enum l m
end.
Program Instance list_finite `{Finite A} n : Finite { l : list A | length l = n } :=
{| enum := list_enum (enum A) n |}.
Global Program Instance vec_finite `{Finite A} n : Finite (vec A n) :=
{| enum := vec_enum (enum A) n |}.
Next Obligation.
intros ????. induction n as [|n IH]; simpl; [apply NoDup_singleton |].
revert IH. generalize (list_enum (enum A) n). intros l Hl.
induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl; auto; [constructor |].
apply NoDup_app; split_and?.
- by apply (NoDup_fmap_2 _).
- intros [k1 Hk1]. clear Hxs IH. rewrite elem_of_list_fmap.
intros ([k2 Hk2]&?&?) Hxk2; simplify_eq/=. destruct Hx. revert Hxk2.
induction xs as [|x' xs IH]; simpl in *; [by rewrite elem_of_nil |].
rewrite elem_of_app, elem_of_list_fmap, elem_of_cons.
intros [([??]&?&?)|?]; simplify_eq/=; auto.
- apply IH.
intros A ?? n. induction n as [|n IH]; csimpl; [apply NoDup_singleton|].
apply NoDup_bind.
- intros x1 x2 y ?? (?&?&_)%elem_of_list_fmap (?&?&_)%elem_of_list_fmap.
congruence.
- intros x ?. rewrite NoDup_fmap by (intros ?; apply vcons_inj_2). done.
- apply NoDup_enum.
Qed.
Next Obligation.
intros ???? [l Hl]. revert l Hl.
induction n as [|n IH]; intros [|x l] ?; simpl; simplify_eq.
{ apply elem_of_list_singleton. by apply (sig_eq_pi _). }
revert IH. generalize (list_enum (enum A) n). intros k Hk.
induction (elem_of_enum x) as [x xs|x xs]; simpl in *.
- rewrite elem_of_app, elem_of_list_fmap. left. injection Hl. intros Hl'.
eexists (l↾Hl'). split. by apply (sig_eq_pi _). done.
- rewrite elem_of_app. eauto.
intros A ?? n v. induction v as [|x n v IH]; csimpl; [apply elem_of_list_here|].
apply elem_of_list_bind. eauto using elem_of_enum, elem_of_list_fmap_1.
Qed.
Lemma list_card `{Finite A} n : card { l : list A | length l = n } = card A ^ n.
Lemma vec_card `{Finite A} n : card (vec A n) = card A ^ n.
Proof.
unfold card; simpl. induction n as [|n IH]; simpl; auto.
rewrite <-IH. clear IH. generalize (list_enum (enum A) n).
induction (enum A) as [|x xs IH]; intros l; simpl; auto.
by rewrite app_length, fmap_length, IH.
unfold card; simpl. induction n as [|n IH]; simpl; [done|].
rewrite <-IH. clear IH. generalize (vec_enum (enum A) n).
induction (enum A) as [|x xs IH]; intros l; csimpl; auto.
by rewrite length_app, length_fmap, IH.
Qed.
Global Instance list_finite `{Finite A} n : Finite { l : list A | length l = n }.
Proof.
refine (bijective_finite (λ v : vec A n, vec_to_list v ↾ length_vec_to_list _)).
- abstract (by intros v1 v2 [= ?%vec_to_list_inj2]).
- abstract (intros [l <-]; exists (list_to_vec l);
apply (sig_eq_pi _), vec_to_list_to_vec).
Defined.
Lemma list_card `{Finite A} n : card { l : list A | length l = n } = card A ^ n.
Proof. unfold card; simpl. rewrite length_fmap. apply vec_card. Qed.
Fixpoint fin_enum (n : nat) : list (fin n) :=
match n with 0 => [] | S n => 0%fin :: (FS <$> fin_enum n) end.
Program Instance fin_finite n : Finite (fin n) := {| enum := fin_enum n |}.
Global Program Instance fin_finite n : Finite (fin n) := {| enum := fin_enum n |}.
Next Obligation.
intros n. induction n; simpl; constructor.
- rewrite elem_of_list_fmap. by intros (?&?&?).
......@@ -360,7 +369,18 @@ Next Obligation.
rewrite elem_of_cons, ?elem_of_list_fmap; eauto.
Qed.
Lemma fin_card n : card (fin n) = n.
Proof. unfold card; simpl. induction n; simpl; rewrite ?fmap_length; auto. Qed.
Proof. unfold card; simpl. induction n; simpl; rewrite ?length_fmap; auto. Qed.
(* shouldn’t be an instance (cycle with [sig_finite]): *)
Lemma finite_sig_dec `{!EqDecision A} (P : A → Prop) `{Finite (sig P)} x :
Decision (P x).
Proof.
assert {xs : list A | ∀ x, P x ↔ x ∈ xs} as [xs ?].
{ clear x. exists (proj1_sig <$> enum _). intros x. split; intros Hx.
- apply elem_of_list_fmap_1_alt with (x ↾ Hx); [apply elem_of_enum|]; done.
- apply elem_of_list_fmap in Hx as [[x' Hx'] [-> _]]; done. }
destruct (decide (x ∈ xs)); [left | right]; naive_solver.
Qed. (* <- could be Defined but this lemma will probably not be used for computing *)
Section sig_finite.
Context {A} (P : A → Prop) `{∀ x, Decision (P x)}.
......@@ -395,5 +415,48 @@ Section sig_finite.
split; [by destruct p | apply elem_of_enum].
Qed.
Lemma sig_card : card (sig P) = length (filter P (enum A)).
Proof. by rewrite <-list_filter_sig_filter, fmap_length. Qed.
Proof. by rewrite <-list_filter_sig_filter, length_fmap. Qed.
End sig_finite.
Lemma finite_pigeonhole `{Finite A} `{Finite B} (f : A → B) :
card B < card A → ∃ x1 x2, x1 ≠ x2 ∧ f x1 = f x2.
Proof.
intros. apply dec_stable; intros Heq.
cut (Inj eq eq f); [intros ?%inj_card; lia|].
intros x1 x2 ?. apply dec_stable. naive_solver.
Qed.
Lemma nat_pigeonhole (f : nat → nat) (n1 n2 : nat) :
n2 < n1 →
(∀ i, i < n1 → f i < n2) →
∃ i1 i2, i1 < i2 < n1 ∧ f i1 = f i2.
Proof.
intros Hn Hf. pose (f' (i : fin n1) := nat_to_fin (Hf _ (fin_to_nat_lt i))).
destruct (finite_pigeonhole f') as (i1&i2&Hi&Hf'); [by rewrite !fin_card|].
apply (not_inj (f:=fin_to_nat)) in Hi. apply (f_equal fin_to_nat) in Hf'.
unfold f' in Hf'. rewrite !fin_to_nat_to_fin in Hf'.
pose proof (fin_to_nat_lt i1); pose proof (fin_to_nat_lt i2).
destruct (decide (i1 < i2)); [exists i1, i2|exists i2, i1]; lia.
Qed.
Lemma list_pigeonhole {A} (l1 l2 : list A) :
l1 ⊆ l2 →
length l2 < length l1 →
∃ i1 i2 x, i1 < i2 ∧ l1 !! i1 = Some x ∧ l1 !! i2 = Some x.
Proof.
intros Hl Hlen.
assert (∀ i : fin (length l1), ∃ (j : fin (length l2)) x,
l1 !! (fin_to_nat i) = Some x ∧
l2 !! (fin_to_nat j) = Some x) as [f Hf]%fin_choice.
{ intros i. destruct (lookup_lt_is_Some_2 l1 i)
as [x Hix]; [apply fin_to_nat_lt|].
assert (x ∈ l2) as [j Hjx]%elem_of_list_lookup_1
by (by eapply Hl, elem_of_list_lookup_2).
exists (nat_to_fin (lookup_lt_Some _ _ _ Hjx)), x.
by rewrite fin_to_nat_to_fin. }
destruct (finite_pigeonhole f) as (i1&i2&Hi&Hf'); [by rewrite !fin_card|].
destruct (Hf i1) as (x1&?&?), (Hf i2) as (x2&?&?).
assert (x1 = x2) as -> by congruence.
apply (not_inj (f:=fin_to_nat)) in Hi. apply (f_equal fin_to_nat) in Hf'.
destruct (decide (i1 < i2)); [exists i1, i2|exists i2, i1]; eauto with lia.
Qed.
theories/functions.v → stdpp/functions.v
View file @ 9274984b
From stdpp Require Export base tactics.
Set Default Proof Using "Type".
From stdpp Require Import options.
Section definitions.
Context {A T : Type} `{EqDecision A}.
......
stdpp/gmap.v 0 → 100644
View file @ 9274984b
This diff is collapsed.
theories/hashset.v → stdpp/hashset.v
View file @ 9274984b
......@@ -3,15 +3,15 @@ using radix-2 search trees. Each hash bucket is thus indexed using an binary
integer of type [Z], and contains an unordered list without duplicates. *)
From stdpp Require Export fin_maps listset.
From stdpp Require Import zmap.
Set Default Proof Using "Type".
From stdpp Require Import options.
Record hashset {A} (hash : A → Z) := Hashset {
hashset_car : Zmap (list A);
hashset_prf :
map_Forall (λ n l, Forall (λ x, hash x = n) l ∧ NoDup l) hashset_car
}.
Arguments Hashset {_ _} _ _ : assert.
Arguments hashset_car {_ _} _ : assert.
Global Arguments Hashset {_ _} _ _ : assert.
Global Arguments hashset_car {_ _} _ : assert.
Section hashset.
Context `{EqDecision A} (hash : A → Z).
......@@ -39,7 +39,7 @@ Qed.
Global Program Instance hashset_intersection: Intersection (hashset hash) := λ m1 m2,
let (m1,Hm1) := m1 in let (m2,Hm2) := m2 in
Hashset (intersection_with (λ l k,
let l' := list_intersection l k in guard (l' ≠ []); Some l') m1 m2) _.
let l' := list_intersection l k in guard (l' ≠ []);; Some l') m1 m2) _.
Next Obligation.
intros _ _ m1 Hm1 m2 Hm2 n l'. rewrite lookup_intersection_with_Some.
intros (?&?&?&?&?); simplify_option_eq.
......@@ -49,7 +49,7 @@ Qed.
Global Program Instance hashset_difference: Difference (hashset hash) := λ m1 m2,
let (m1,Hm1) := m1 in let (m2,Hm2) := m2 in
Hashset (difference_with (λ l k,
let l' := list_difference l k in guard (l' ≠ []); Some l') m1 m2) _.
let l' := list_difference l k in guard (l' ≠ []);; Some l') m1 m2) _.
Next Obligation.
intros _ _ m1 Hm1 m2 Hm2 n l'. rewrite lookup_difference_with_Some.
intros [[??]|(?&?&?&?&?)]; simplify_option_eq; auto.
......@@ -104,8 +104,8 @@ Proof.
intros (l&?&?). exists (hash x, l); simpl. by rewrite elem_of_map_to_list.
- unfold elements, hashset_elements. intros [m Hm]; simpl.
rewrite map_Forall_to_list in Hm. generalize (NoDup_fst_map_to_list m).
induction Hm as [|[n l] m' [??]];
csimpl; inversion_clear 1 as [|?? Hn]; [constructor|].
induction Hm as [|[n l] m' [??] Hm];
csimpl; inv 1 as [|?? Hn]; [constructor|].
apply NoDup_app; split_and?; eauto.
setoid_rewrite elem_of_list_bind; intros x ? ([n' l']&?&?); simpl in *.
assert (hash x = n ∧ hash x = n') as [??]; subst.
......@@ -116,7 +116,7 @@ Proof.
Qed.
End hashset.
Typeclasses Opaque hashset_elem_of.
Global Typeclasses Opaque hashset_elem_of.
Section remove_duplicates.
Context `{EqDecision A} (hash : A → Z).
......@@ -126,7 +126,7 @@ Definition remove_dups_fast (l : list A) : list A :=
| [] => []
| [x] => [x]
| _ =>
let n : Z := length l in
let n : Z := Z.of_nat (length l) in
elements (foldr (λ x, ({[ x ]} ∪.)) ∅ l :
hashset (λ x, hash x `mod` (2 * n))%Z)
end.
......@@ -134,7 +134,7 @@ Lemma elem_of_remove_dups_fast l x : x ∈ remove_dups_fast l ↔ x ∈ l.
Proof.
destruct l as [|x1 [|x2 l]]; try reflexivity.
unfold remove_dups_fast; generalize (x1 :: x2 :: l); clear l; intros l.
generalize (λ x, hash x `mod` (2 * length l))%Z; intros f.
generalize (λ x, hash x `mod` (2 * Z.of_nat (length l)))%Z; intros f.
rewrite elem_of_elements; split.
- revert x. induction l as [|y l IH]; intros x; simpl.
{ by rewrite elem_of_empty. }
......@@ -144,12 +144,14 @@ Qed.
Lemma NoDup_remove_dups_fast l : NoDup (remove_dups_fast l).
Proof.
unfold remove_dups_fast; destruct l as [|x1 [|x2 l]].
apply NoDup_nil_2. apply NoDup_singleton. apply NoDup_elements.
- apply NoDup_nil_2.
- apply NoDup_singleton.
- apply NoDup_elements.
Qed.
Definition listset_normalize (X : listset A) : listset A :=
let (l) := X in Listset (remove_dups_fast l).
Lemma listset_normalize_correct X : listset_normalize X ≡ X.
Proof.
destruct X as [l]. apply elem_of_equiv; intro; apply elem_of_remove_dups_fast.
destruct X as [l]. apply set_equiv; intro; apply elem_of_remove_dups_fast.
Qed.
End remove_duplicates.
theories/hlist.v → stdpp/hlist.v
View file @ 9274984b
This diff is collapsed.
theories/infinite.v → stdpp/infinite.v
View file @ 9274984b
This diff is collapsed.
theories/lexico.v → stdpp/lexico.v
View file @ 9274984b
This diff is collapsed.
stdpp/list.v 0 → 100644
View file @ 9274984b
(** This file re-exports all the list lemmas in std++. Do *not* import the individual
[list_*] modules; their organization may cahnge over time. Always import [list]. *)
From stdpp Require Export list_basics list_relations list_monad list_misc list_tactics list_numbers.
From stdpp Require Import options.
stdpp/list_basics.v 0 → 100644
View file @ 9274984b
This diff is collapsed.
stdpp/list_misc.v 0 → 100644
View file @ 9274984b
This diff is collapsed.