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 6853 additions and 633 deletions
theories/countable.v → stdpp/countable.v
View file @ 9274984b
......@@ -61,10 +61,9 @@ Section choice.
{ intros help. by apply (help (encode x)). }
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)}.
......@@ -295,16 +294,16 @@ Qed.
Global Program Instance Qp_countable : Countable Qp :=
inj_countable
Qp_to_Qc
(λ p : Qc, guard (0 < p)%Qc as Hp; Some (mk_Qp p Hp)) _.
(λ p : Qc, Hp ← guard (0 < p)%Qc; Some (mk_Qp p Hp)) _.
Next Obligation.
intros [p Hp]. unfold mguard, option_guard; simpl.
case_match; [|done]. f_equal. by apply Qp_to_Qc_inj_iff.
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, guard (m < n)%nat as Hm; Some (nat_to_fin Hm)) _.
(λ m : nat, Hm ← guard (m < n)%nat; Some (nat_to_fin Hm)) _.
Next Obligation.
intros n i; simplify_option_eq.
- by rewrite nat_to_fin_to_nat.
......@@ -314,6 +313,18 @@ 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.
......@@ -355,8 +366,8 @@ 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.
Global Program Instance gen_tree_countable `{Countable T} : Countable (gen_tree T) :=
......@@ -370,7 +381,7 @@ Qed.
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, guard (P x) as Hx; Some (x ↾ Hx)) _.
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
......@@ -87,8 +87,13 @@ Notation cast_if_not S := (if S then right _ else left _).
(** * Instances of [Decision] *)
(** Instances of [Decision] for operators of propositional logic. *)
Global Instance True_dec: Decision True := left I.
Global Instance False_dec: Decision False := right (False_rect False).
(** 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.
......
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
......@@ -17,14 +17,13 @@ Notation FS := Fin.FS.
Declare Scope fin_scope.
Delimit Scope fin_scope with fin.
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.
......@@ -65,9 +64,11 @@ 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.
......@@ -87,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_map_dom.v → stdpp/fin_map_dom.v
View file @ 9274984b
......@@ -9,11 +9,11 @@ Set Default Proof Using "Type*".
Class FinMapDom K M D `{∀ A, Dom (M A) D, FMap M,
∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A, PartialAlter K A (M A),
OMap M, Merge M, ∀ A, FinMapToList K A (M A), EqDecision K,
OMap M, Merge M, ∀ A, MapFold K A (M A), EqDecision K,
ElemOf K D, Empty D, Singleton K D,
Union D, Intersection D, Difference D} := {
finmap_dom_map :> FinMap K M;
finmap_dom_set :> Set_ K D;
finmap_dom_map :: FinMap K M;
finmap_dom_set :: Set_ K D;
elem_of_dom {A} (m : M A) i : i ∈ dom m ↔ is_Some (m !! i)
}.
......@@ -42,10 +42,14 @@ Lemma elem_of_dom_2 {A} (m : M A) i x : m !! i = Some x → i ∈ dom m.
Proof. rewrite elem_of_dom; eauto. Qed.
Lemma not_elem_of_dom {A} (m : M A) i : i ∉ dom m ↔ m !! i = None.
Proof. by rewrite elem_of_dom, eq_None_not_Some. Qed.
Lemma not_elem_of_dom_1 {A} (m : M A) i : i ∉ dom m → m !! i = None.
Proof. apply not_elem_of_dom. Qed.
Lemma not_elem_of_dom_2 {A} (m : M A) i : m !! i = None → i ∉ dom m.
Proof. apply not_elem_of_dom. Qed.
Lemma subseteq_dom {A} (m1 m2 : M A) : m1 ⊆ m2 → dom m1 ⊆ dom m2.
Proof.
rewrite map_subseteq_spec.
intros ??. rewrite !elem_of_dom. inversion 1; eauto.
intros ??. rewrite !elem_of_dom. inv 1; eauto.
Qed.
Lemma subset_dom {A} (m1 m2 : M A) : m1 ⊂ m2 → dom m1 ⊂ dom m2.
Proof.
......@@ -60,39 +64,46 @@ Lemma dom_filter {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) (X
dom (filter P m) ≡ X.
Proof.
intros HX i. rewrite elem_of_dom, HX.
unfold is_Some. by setoid_rewrite map_filter_lookup_Some.
unfold is_Some. by setoid_rewrite map_lookup_filter_Some.
Qed.
Lemma dom_filter_subseteq {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A):
dom (filter P m) ⊆ dom m.
Proof. apply subseteq_dom, map_filter_subseteq. Qed.
(* FIXME: Once [Equiv] has [Mode !], we can remove all these [D] type annotations at [≡]. *)
Lemma dom_empty {A} : dom (@empty (M A) _) ≡@{D} ∅.
Lemma filter_dom {A} `{!Elements K D, !FinSet K D}
(P : K → Prop) `{!∀ x, Decision (P x)} (m : M A) :
filter P (dom m) ≡ dom (filter (λ kv, P kv.1) m).
Proof.
intros i. rewrite elem_of_filter, !elem_of_dom. unfold is_Some.
setoid_rewrite map_lookup_filter_Some. naive_solver.
Qed.
Lemma dom_empty {A} : dom (@empty (M A) _) ≡ ∅.
Proof.
intros x. rewrite elem_of_dom, lookup_empty, <-not_eq_None_Some. set_solver.
Qed.
Lemma dom_empty_iff {A} (m : M A) : dom m ≡@{D} ∅ ↔ m = ∅.
Lemma dom_empty_iff {A} (m : M A) : dom m ≡ ∅ ↔ m = ∅.
Proof.
split; [|intros ->; by rewrite dom_empty].
intros E. apply map_empty. intros. apply not_elem_of_dom.
rewrite E. set_solver.
Qed.
Lemma dom_empty_inv {A} (m : M A) : dom m ≡@{D} ∅ → m = ∅.
Lemma dom_empty_inv {A} (m : M A) : dom m ≡ ∅ → m = ∅.
Proof. apply dom_empty_iff. Qed.
Lemma dom_alter {A} f (m : M A) i : dom (alter f i m) ≡@{D} dom m.
Lemma dom_alter {A} f (m : M A) i : dom (alter f i m) ≡ dom m.
Proof.
apply set_equiv; intros j; rewrite !elem_of_dom; unfold is_Some.
destruct (decide (i = j)); simplify_map_eq/=; eauto.
destruct (m !! j); naive_solver.
Qed.
Lemma dom_insert {A} (m : M A) i x : dom (<[i:=x]>m) ≡@{D} {[ i ]} ∪ dom m.
Lemma dom_insert {A} (m : M A) i x : dom (<[i:=x]>m) ≡ {[ i ]} ∪ dom m.
Proof.
apply set_equiv. intros j. rewrite elem_of_union, !elem_of_dom.
unfold is_Some. setoid_rewrite lookup_insert_Some.
destruct (decide (i = j)); set_solver.
Qed.
Lemma dom_insert_lookup {A} (m : M A) i x :
is_Some (m !! i) → dom (<[i:=x]>m) ≡@{D} dom m.
is_Some (m !! i) → dom (<[i:=x]>m) ≡ dom m.
Proof.
intros Hindom. assert (i ∈ dom m) by by apply elem_of_dom.
rewrite dom_insert. set_solver.
......@@ -102,9 +113,9 @@ Proof. rewrite (dom_insert _). set_solver. Qed.
Lemma dom_insert_subseteq_compat_l {A} (m : M A) i x X :
X ⊆ dom m → X ⊆ dom (<[i:=x]>m).
Proof. intros. trans (dom m); eauto using dom_insert_subseteq. Qed.
Lemma dom_singleton {A} (i : K) (x : A) : dom ({[i := x]} : M A) ≡@{D} {[ i ]}.
Lemma dom_singleton {A} (i : K) (x : A) : dom ({[i := x]} : M A) ≡ {[ i ]}.
Proof. rewrite <-insert_empty, dom_insert, dom_empty; set_solver. Qed.
Lemma dom_delete {A} (m : M A) i : dom (delete i m) ≡@{D} dom m ∖ {[ i ]}.
Lemma dom_delete {A} (m : M A) i : dom (delete i m) ≡ dom m ∖ {[ i ]}.
Proof.
apply set_equiv. intros j. rewrite elem_of_difference, !elem_of_dom.
unfold is_Some. setoid_rewrite lookup_delete_Some. set_solver.
......@@ -124,24 +135,24 @@ Lemma map_disjoint_dom_1 {A} (m1 m2 : M A) : m1 ##ₘ m2 → dom m1 ## dom m2.
Proof. apply map_disjoint_dom. Qed.
Lemma map_disjoint_dom_2 {A} (m1 m2 : M A) : dom m1 ## dom m2 → m1 ##ₘ m2.
Proof. apply map_disjoint_dom. Qed.
Lemma dom_union {A} (m1 m2 : M A) : dom (m1 ∪ m2) ≡@{D} dom m1 ∪ dom m2.
Lemma dom_union {A} (m1 m2 : M A) : dom (m1 ∪ m2) ≡ dom m1 ∪ dom m2.
Proof.
apply set_equiv. intros i. rewrite elem_of_union, !elem_of_dom.
unfold is_Some. setoid_rewrite lookup_union_Some_raw.
destruct (m1 !! i); naive_solver.
Qed.
Lemma dom_intersection {A} (m1 m2: M A) : dom (m1 ∩ m2) ≡@{D} dom m1 ∩ dom m2.
Lemma dom_intersection {A} (m1 m2: M A) : dom (m1 ∩ m2) ≡ dom m1 ∩ dom m2.
Proof.
apply set_equiv. intros i. rewrite elem_of_intersection, !elem_of_dom.
unfold is_Some. setoid_rewrite lookup_intersection_Some. naive_solver.
Qed.
Lemma dom_difference {A} (m1 m2 : M A) : dom (m1 ∖ m2) ≡@{D} dom m1 ∖ dom m2.
Lemma dom_difference {A} (m1 m2 : M A) : dom (m1 ∖ m2) ≡ dom m1 ∖ dom m2.
Proof.
apply set_equiv. intros i. rewrite elem_of_difference, !elem_of_dom.
unfold is_Some. setoid_rewrite lookup_difference_Some.
destruct (m2 !! i); naive_solver.
Qed.
Lemma dom_fmap {A B} (f : A → B) (m : M A) : dom (f <$> m) ≡@{D} dom m.
Lemma dom_fmap {A B} (f : A → B) (m : M A) : dom (f <$> m) ≡ dom m.
Proof.
apply set_equiv. intros i.
rewrite !elem_of_dom, lookup_fmap, <-!not_eq_None_Some.
......@@ -153,22 +164,41 @@ Proof.
- by apply empty_finite.
- apply union_finite; [apply singleton_finite|done].
Qed.
Global Instance dom_proper `{!Equiv A} : Proper ((≡@{M A}) ==> (≡@{D})) (dom).
Global Instance dom_proper `{!Equiv A} : Proper ((≡@{M A}) ==> (≡)) dom.
Proof.
intros m1 m2 EQm. apply set_equiv. intros i.
rewrite !elem_of_dom, EQm. done.
Qed.
Lemma dom_list_to_map {A} (l : list (K * A)) :
dom (list_to_map l : M A) ≡@{D} list_to_set l.*1.
dom (list_to_map l : M A) ≡ list_to_set l.*1.
Proof.
induction l as [|?? IH].
- by rewrite dom_empty.
- simpl. by rewrite dom_insert, IH.
Qed.
Lemma map_first_key_dom {A B} (m1 : M A) (m2 : M B) i :
dom m1 ≡ dom m2 → map_first_key m1 i ↔ map_first_key m2 i.
Proof.
intros Hm. apply map_first_key_dom'. intros j.
by rewrite <-!elem_of_dom, Hm.
Qed.
Lemma map_first_key_dom_L {A B} (m1 : M A) (m2 : M B) i :
dom m1 = dom m2 → map_first_key m1 i ↔ map_first_key m2 i.
Proof. intros Hm. apply map_first_key_dom. by rewrite Hm. Qed.
Lemma map_Forall2_dom {A B} (P : K → A → B → Prop) (m1 : M A) (m2 : M B) :
map_Forall2 P m1 m2 → dom m1 ≡ dom m2.
Proof.
revert m2. induction m1 as [|i x1 m1 ? IH] using map_ind; intros m2.
{ intros ->%map_Forall2_empty_inv_l. by rewrite !dom_empty. }
intros (x2 & m2' & -> & ? & ? & ?)%map_Forall2_insert_inv_l; last done.
by rewrite !dom_insert, IH by done.
Qed.
(** Alternative definition of [dom] in terms of [map_to_list]. *)
Lemma dom_alt {A} (m : M A) :
dom m ≡@{D} list_to_set (map_to_list m).*1.
dom m ≡ list_to_set (map_to_list m).*1.
Proof.
rewrite <-(list_to_map_to_list m) at 1.
rewrite dom_list_to_map.
......@@ -178,13 +208,46 @@ Qed.
Lemma size_dom `{!Elements K D, !FinSet K D} {A} (m : M A) :
size (dom m) = size m.
Proof.
rewrite dom_alt, size_list_to_set.
2:{ apply NoDup_fst_map_to_list. }
unfold size, map_size. rewrite fmap_length. done.
induction m as [|i x m ? IH] using map_ind.
{ by rewrite dom_empty, map_size_empty, size_empty. }
assert ({[i]} ## dom m).
{ intros j. rewrite elem_of_dom. unfold is_Some. set_solver. }
by rewrite dom_insert, size_union, size_singleton, map_size_insert_None, IH.
Qed.
Lemma dom_subseteq_size {A} (m1 m2 : M A) : dom m2 ⊆ dom m1 → size m2 ≤ size m1.
Proof.
revert m1. induction m2 as [|i x m2 ? IH] using map_ind; intros m1 Hdom.
{ rewrite map_size_empty. lia. }
rewrite dom_insert in Hdom.
assert (i ∉ dom m2) by (by apply not_elem_of_dom).
assert (i ∈ dom m1) as [x' Hx']%elem_of_dom by set_solver.
rewrite <-(insert_delete m1 i x') by done.
rewrite !map_size_insert_None, <-Nat.succ_le_mono by (by rewrite ?lookup_delete).
apply IH. rewrite dom_delete. set_solver.
Qed.
Lemma dom_subset_size {A} (m1 m2 : M A) : dom m2 ⊂ dom m1 → size m2 < size m1.
Proof.
revert m1. induction m2 as [|i x m2 ? IH] using map_ind; intros m1 Hdom.
{ destruct m1 as [|i x m1 ? _] using map_ind.
- rewrite !dom_empty in Hdom. set_solver.
- rewrite map_size_empty, map_size_insert_None by done. lia. }
rewrite dom_insert in Hdom.
assert (i ∉ dom m2) by (by apply not_elem_of_dom).
assert (i ∈ dom m1) as [x' Hx']%elem_of_dom by set_solver.
rewrite <-(insert_delete m1 i x') by done.
rewrite !map_size_insert_None, <-Nat.succ_lt_mono by (by rewrite ?lookup_delete).
apply IH. rewrite dom_delete. split; [set_solver|].
intros ?. destruct Hdom as [? []].
intros j. destruct (decide (i = j)); set_solver.
Qed.
Lemma subseteq_dom_eq {A} (m1 m2 : M A) :
m1 ⊆ m2 → dom m2 ⊆ dom m1 → m1 = m2.
Proof. intros. apply map_subseteq_size_eq; auto using dom_subseteq_size. Qed.
Lemma dom_singleton_inv {A} (m : M A) i :
dom m ≡@{D} {[i]} → ∃ x, m = {[i := x]}.
dom m ≡ {[i]} → ∃ x, m = {[i := x]}.
Proof.
intros Hdom. assert (is_Some (m !! i)) as [x ?].
{ apply (elem_of_dom (D:=D)); set_solver. }
......@@ -194,7 +257,7 @@ Proof.
Qed.
Lemma dom_map_zip_with {A B C} (f : A → B → C) (ma : M A) (mb : M B) :
dom (map_zip_with f ma mb) ≡@{D} dom ma ∩ dom mb.
dom (map_zip_with f ma mb) ≡ dom ma ∩ dom mb.
Proof.
rewrite set_equiv. intros x.
rewrite elem_of_intersection, !elem_of_dom, map_lookup_zip_with.
......@@ -212,13 +275,13 @@ Proof.
{ apply map_disjoint_filter_complement. }
split_and!; [|done| |].
- apply map_eq; intros i. apply option_eq; intros x.
rewrite lookup_union_Some, !map_filter_lookup_Some by done.
rewrite lookup_union_Some, !map_lookup_filter_Some by done.
destruct (decide (i ∈ X1)); naive_solver.
- apply dom_filter; intros i; split; [|naive_solver].
intros. assert (is_Some (m !! i)) as [x ?] by (apply (elem_of_dom (D:=D)); set_solver).
intros. assert (is_Some (m !! i)) as [x ?] by (apply elem_of_dom; set_solver).
naive_solver.
- apply dom_filter; intros i; split.
+ intros. assert (is_Some (m !! i)) as [x ?] by (apply (elem_of_dom (D:=D)); set_solver).
+ intros. assert (is_Some (m !! i)) as [x ?] by (apply elem_of_dom; set_solver).
naive_solver.
+ intros (x&?&?). apply dec_stable; intros ?.
assert (m !! i = None) by (apply not_elem_of_dom; set_solver).
......@@ -234,6 +297,33 @@ Proof.
by setoid_rewrite elem_of_dom.
Qed.
Lemma dom_omap_subseteq {A B} (f : A → option B) (m : M A) :
dom (omap f m) ⊆ dom m.
Proof.
intros a. rewrite !elem_of_dom. intros [c Hm].
apply lookup_omap_Some in Hm. naive_solver.
Qed.
Lemma map_compose_dom_subseteq {C} `{FinMap K' M'} (m: M' C) (n : M K') :
dom (m ∘ₘ n : M C) ⊆@{D} dom n.
Proof. apply dom_omap_subseteq. Qed.
Lemma map_compose_min_r_dom {C} `{FinMap K' M', !RelDecision (∈@{D})}
(m : M C) (n : M' K) :
m ∘ₘ n = m ∘ₘ filter (λ '(_,b), b ∈ dom m) n.
Proof.
rewrite map_compose_min_r. f_equal.
apply map_filter_ext. intros. by rewrite elem_of_dom.
Qed.
Lemma map_compose_empty_iff_dom_img {C} `{FinMap K' M', !RelDecision (∈@{D})}
(m : M C) (n : M' K) :
m ∘ₘ n = ∅ ↔ dom m ## map_img n.
Proof.
rewrite map_compose_empty_iff, elem_of_disjoint.
setoid_rewrite elem_of_dom. setoid_rewrite eq_None_not_Some.
setoid_rewrite elem_of_map_img. naive_solver.
Qed.
(** If [D] has Leibniz equality, we can show an even stronger result. This is a
common case e.g. when having a [gmap K A] where the key [K] has Leibniz equality
(and thus also [gset K], the usual domain) but the value type [A] does not. *)
......@@ -243,10 +333,15 @@ Proof. intros ???. unfold_leibniz. by apply dom_proper. Qed.
Section leibniz.
Context `{!LeibnizEquiv D}.
Lemma dom_filter_L {A} (P : K * A → Prop) `{!∀ x, Decision (P x)} (m : M A) X :
(∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ P (i, x)) →
dom (filter P m) = X.
Proof. unfold_leibniz. apply dom_filter. Qed.
Lemma filter_dom_L {A} `{!Elements K D, !FinSet K D}
(P : K → Prop) `{!∀ x, Decision (P x)} (m : M A) :
filter P (dom m) = dom (filter (λ kv, P kv.1) m).
Proof. unfold_leibniz. apply filter_dom. Qed.
Lemma dom_empty_L {A} : dom (@empty (M A) _) = ∅.
Proof. unfold_leibniz; apply dom_empty. Qed.
Lemma dom_empty_iff_L {A} (m : M A) : dom m = ∅ ↔ m = ∅.
......@@ -273,6 +368,9 @@ Section leibniz.
Proof. unfold_leibniz; apply dom_difference. Qed.
Lemma dom_fmap_L {A B} (f : A → B) (m : M A) : dom (f <$> m) = dom m.
Proof. unfold_leibniz; apply dom_fmap. Qed.
Lemma map_Forall2_dom_L {A B} (P : K → A → B → Prop) (m1 : M A) (m2 : M B) :
map_Forall2 P m1 m2 → dom m1 = dom m2.
Proof. unfold_leibniz. apply map_Forall2_dom. Qed.
Lemma dom_imap_L {A B} (f: K → A → option B) (m: M A) X :
(∀ i, i ∈ X ↔ ∃ x, m !! i = Some x ∧ is_Some (f i x)) →
dom (map_imap f m) = X.
......@@ -350,7 +448,7 @@ Proof. constructor. by rewrite dom_fmap, (set_unfold_elem_of _ (dom _) _). Qed.
End fin_map_dom.
Lemma dom_seq `{FinMapDom nat M D} {A} start (xs : list A) :
dom (map_seq start (M:=M A) xs) ≡@{D} set_seq start (length xs).
dom (map_seq start (M:=M A) xs) ≡ set_seq start (length xs).
Proof.
revert start. induction xs as [|x xs IH]; intros start; simpl.
- by rewrite dom_empty.
......
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
......@@ -10,26 +10,38 @@ Set Default Proof Using "Type*".
(** Operations *)
Global Instance set_size `{Elements A C} : Size C := length ∘ elements.
Typeclasses Opaque set_size.
Global Typeclasses Opaque set_size.
Definition set_fold `{Elements A C} {B}
(f : A → B → B) (b : B) : C → B := foldr f b ∘ elements.
Typeclasses Opaque set_fold.
Global Typeclasses Opaque set_fold.
Global Instance set_filter
`{Elements A C, Empty C, Singleton A C, Union C} : Filter A C := λ P _ X,
list_to_set (filter P (elements X)).
Typeclasses Opaque set_filter.
Global Typeclasses Opaque set_filter.
Definition set_map `{Elements A C, Singleton B D, Empty D, Union D}
(f : A → B) (X : C) : D :=
list_to_set (f <$> elements X).
Typeclasses Opaque set_map.
Global Typeclasses Opaque set_map.
Global Instance: Params (@set_map) 8 := {}.
Definition set_bind `{Elements A SA, Empty SB, Union SB}
(f : A → SB) (X : SA) : SB :=
⋃ (f <$> elements X).
Global Typeclasses Opaque set_bind.
Global Instance: Params (@set_bind) 6 := {}.
Definition set_omap `{Elements A C, Singleton B D, Empty D, Union D}
(f : A → option B) (X : C) : D :=
list_to_set (omap f (elements X)).
Global Typeclasses Opaque set_omap.
Global Instance: Params (@set_omap) 8 := {}.
Global Instance set_fresh `{Elements A C, Fresh A (list A)} : Fresh A C :=
fresh ∘ elements.
Typeclasses Opaque set_fresh.
Global Typeclasses Opaque set_fresh.
(** We generalize the [fresh] operation on sets to generate lists of fresh
elements w.r.t. a set [X]. *)
......@@ -182,7 +194,7 @@ Qed.
Lemma size_union X Y : X ## Y → size (X ∪ Y) = size X + size Y.
Proof.
intros. unfold size, set_size. simpl. rewrite <-app_length.
intros. unfold size, set_size. simpl. rewrite <-length_app.
apply Permutation_length, NoDup_Permutation.
- apply NoDup_elements.
- apply NoDup_app; repeat split; try apply NoDup_elements.
......@@ -207,6 +219,16 @@ Proof.
apply set_size_proper. set_solver.
Qed.
Lemma set_subseteq_size_equiv X1 X2 : X1 ⊆ X2 → size X2 ≤ size X1 → X1 ≡ X2.
Proof.
intros. apply (anti_symm _); [done|].
apply empty_difference_subseteq, size_empty_iff.
rewrite size_difference by done. lia.
Qed.
Lemma set_subseteq_size_eq `{!LeibnizEquiv C} X1 X2 :
X1 ⊆ X2 → size X2 ≤ size X1 → X1 = X2.
Proof. unfold_leibniz. apply set_subseteq_size_equiv. Qed.
Lemma subseteq_size X Y : X ⊆ Y → size X ≤ size Y.
Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed.
Lemma subset_size X Y : X ⊂ Y → size X < size Y.
......@@ -225,10 +247,10 @@ Proof.
Qed.
(** * Induction principles *)
Lemma set_wf : wf (⊂@{C}).
Lemma set_wf : well_founded (⊂@{C}).
Proof. apply (wf_projected (<) size); auto using subset_size, lt_wf. Qed.
Lemma set_ind (P : C → Prop) :
Proper ((≡) ==> iff) P →
Proper ((≡) ==> impl) P →
P ∅ → (∀ x X, x ∉ X → P X → P ({[ x ]} ∪ X)) → ∀ X, P X.
Proof.
intros ? Hemp Hadd. apply well_founded_induction with (⊂).
......@@ -244,7 +266,7 @@ Proof. apply set_ind. by intros ?? ->%leibniz_equiv_iff. Qed.
(** * The [set_fold] operation *)
Lemma set_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B) :
Proper ((=) ==> (≡) ==> iff) P →
(∀ x, Proper ((≡) ==> impl) (P x)) →
P b ∅ → (∀ x X r, x ∉ X → P r X → P (f x r) ({[ x ]} ∪ X)) →
∀ X, P (set_fold f b X) X.
Proof.
......@@ -263,9 +285,9 @@ Lemma set_fold_ind_L `{!LeibnizEquiv C}
{B} (P : B → C → Prop) (f : A → B → B) (b : B) :
P b ∅ → (∀ x X r, x ∉ X → P r X → P (f x r) ({[ x ]} ∪ X)) →
∀ X, P (set_fold f b X) X.
Proof. apply set_fold_ind. by intros ?? -> ?? ->%leibniz_equiv. Qed.
Lemma set_fold_proper {B} (R : relation B) `{!Equivalence R}
(f : A → B → B) (b : B) `{!Proper ((=) ==> R ==> R) f}
Proof. apply set_fold_ind. solve_proper. Qed.
Lemma set_fold_proper {B} (R : relation B) `{!PreOrder R}
(f : A → B → B) (b : B) `{!∀ a, Proper (R ==> R) (f a)}
(Hf : ∀ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
Proper ((≡) ==> R) (set_fold f b : C → B).
Proof. intros ?? E. apply (foldr_permutation R f b); auto. by rewrite E. Qed.
......@@ -276,28 +298,112 @@ Proof. by unfold set_fold; simpl; rewrite elements_empty. Qed.
Lemma set_fold_singleton {B} (f : A → B → B) (b : B) (a : A) :
set_fold f b ({[a]} : C) = f a b.
Proof. by unfold set_fold; simpl; rewrite elements_singleton. Qed.
(** Generalization of [set_fold_disj_union] (below) with a.) a relation [R]
(** The following lemma shows that folding over two sets separately (using the
result of the first fold as input for the second fold) is equivalent to folding
over the union, *if* the function is idempotent for the elements that will be
processed twice ([X ∩ Y]) and does not care about the order in which elements
are processed.
This is a generalization of [set_fold_union] (below) with a.) a relation [R]
instead of equality b.) a function [f : A → B → B] instead of [f : A → A → A],
and c.) premises that ensure the elements are in [X ∪ Y]. *)
Lemma set_fold_disj_union_strong {B} (R : relation B) `{!PreOrder R}
Lemma set_fold_union_strong {B} (R : relation B) `{!PreOrder R}
(f : A → B → B) (b : B) X Y :
(∀ x, Proper (R ==> R) (f x)) →
(∀ x b',
(** This is morally idempotence for elements of [X ∩ Y] *)
x ∈ X ∩ Y →
(** We cannot write this in the usual direction of idempotence properties
(i.e., [R (f x (f x b'))) (f x b')]) because [R] is not symmetric. *)
R (f x b') (f x (f x b'))) →
(∀ x1 x2 b',
(** This is morally commutativity + associativity for elements of [X ∪ Y] *)
x1 ∈ X ∪ Y → x2 ∈ X ∪ Y → x1 ≠ x2 →
R (f x1 (f x2 b')) (f x2 (f x1 b'))) →
X ## Y →
R (set_fold f b (X ∪ Y)) (set_fold f (set_fold f b X) Y).
Proof.
intros ? Hf Hdisj. unfold set_fold; simpl.
rewrite <-foldr_app. apply (foldr_permutation R f b).
- intros j1 x1 j2 x2 b' Hj Hj1 Hj2. apply Hf.
(** This lengthy proof involves various steps by transitivity of [R].
Roughly, we show that the LHS is related to folding over:
elements (Y ∖ X) ++ elements (X ∩ Y) ++ elements (X ∖ Y)
and the RHS is related to folding over:
elements (Y ∖ X) ++ elements (X ∩ Y) ++ elements (X ∩ Y) ++ elements (Y ∖ X)
These steps are justified by lemma [foldr_permutation]. In the middle we
remove the repeated folding over [elements (X ∩ Y)] using [foldr_idemp_strong].
Most of the proof work concerns the side conditions of [foldr_permutation]
and [foldr_idemp_strong], which require relating results about lists and
sets. *)
intros ?.
assert (∀ b1 b2 l, R b1 b2 → R (foldr f b1 l) (foldr f b2 l)) as Hff.
{ intros b1 b2 l Hb. induction l as [|x l]; simpl; [done|]. by f_equiv. }
intros Hfidemp Hfcomm. unfold set_fold; simpl.
trans (foldr f b (elements (Y ∖ X) ++ elements (X ∩ Y) ++ elements (X ∖ Y))).
{ apply (foldr_permutation R f b).
- intros j1 x1 j2 x2 b' Hj Hj1 Hj2. apply Hfcomm.
+ apply elem_of_list_lookup_2 in Hj1. set_solver.
+ apply elem_of_list_lookup_2 in Hj2. set_solver.
+ intros ->. pose proof (NoDup_elements (X ∪ Y)).
by eapply Hj, NoDup_lookup.
- rewrite <-!elements_disj_union by set_solver. f_equiv; intros x.
destruct (decide (x ∈ X)), (decide (x ∈ Y)); set_solver. }
trans (foldr f (foldr f b (elements (X ∩ Y) ++ elements (X ∖ Y)))
(elements (Y ∖ X) ++ elements (X ∩ Y))).
{ rewrite !foldr_app. apply Hff. apply (foldr_idemp_strong (flip R)).
- solve_proper.
- intros j a b' ?%elem_of_list_lookup_2. apply Hfidemp. set_solver.
- intros j1 x1 j2 x2 b' Hj Hj1 Hj2. apply Hfcomm.
+ apply elem_of_list_lookup_2 in Hj2. set_solver.
+ apply elem_of_list_lookup_2 in Hj1. set_solver.
+ intros ->. pose proof (NoDup_elements (X ∩ Y)).
by eapply Hj, NoDup_lookup. }
trans (foldr f (foldr f b (elements (X ∩ Y) ++ elements (X ∖ Y))) (elements Y)).
{ apply (foldr_permutation R f _).
- intros j1 x1 j2 x2 b' Hj Hj1 Hj2. apply Hfcomm.
+ apply elem_of_list_lookup_2 in Hj1. set_solver.
+ apply elem_of_list_lookup_2 in Hj2. set_solver.
+ intros ->. assert (NoDup (elements (Y ∖ X) ++ elements (X ∩ Y))).
{ rewrite <-elements_disj_union by set_solver. apply NoDup_elements. }
by eapply Hj, NoDup_lookup.
- rewrite <-!elements_disj_union by set_solver. f_equiv; intros x.
destruct (decide (x ∈ X)); set_solver. }
apply Hff. apply (foldr_permutation R f _).
- intros j1 x1 j2 x2 b' Hj Hj1 Hj2. apply Hfcomm.
+ apply elem_of_list_lookup_2 in Hj1. set_solver.
+ apply elem_of_list_lookup_2 in Hj2. set_solver.
+ intros ->. pose proof (NoDup_elements (X ∪ Y)).
+ intros ->. assert (NoDup (elements (X ∩ Y) ++ elements (X ∖ Y))).
{ rewrite <-elements_disj_union by set_solver. apply NoDup_elements. }
by eapply Hj, NoDup_lookup.
- by rewrite elements_disj_union, (comm (++)).
- rewrite <-!elements_disj_union by set_solver. f_equiv; intros x.
destruct (decide (x ∈ Y)); set_solver.
Qed.
Lemma set_fold_union (f : A → A → A) (b : A) X Y :
IdemP (=) f →
Comm (=) f →
Assoc (=) f →
set_fold f b (X ∪ Y) = set_fold f (set_fold f b X) Y.
Proof.
intros. apply (set_fold_union_strong _ _ _ _ _ _).
- intros x b' _. by rewrite (assoc_L f), (idemp f).
- intros x1 x2 b' _ _ _. by rewrite !(assoc_L f), (comm_L f x1).
Qed.
(** Generalization of [set_fold_disj_union] (below) with a.) a relation [R]
instead of equality b.) a function [f : A → B → B] instead of [f : A → A → A],
and c.) premises that ensure the elements are in [X ∪ Y]. *)
Lemma set_fold_disj_union_strong {B} (R : relation B) `{!PreOrder R}
(f : A → B → B) (b : B) X Y :
(∀ x, Proper (R ==> R) (f x)) →
(∀ x1 x2 b',
(** This is morally commutativity + associativity for elements of [X ∪ Y] *)
x1 ∈ X ∪ Y → x2 ∈ X ∪ Y → x1 ≠ x2 →
R (f x1 (f x2 b')) (f x2 (f x1 b'))) →
X ## Y →
R (set_fold f b (X ∪ Y)) (set_fold f (set_fold f b X) Y).
Proof. intros. apply set_fold_union_strong; set_solver. Qed.
Lemma set_fold_disj_union (f : A → A → A) (b : A) X Y :
Comm (=) f →
Assoc (=) f →
......@@ -308,8 +414,22 @@ Proof.
intros x1 x2 b' _ _ _. by rewrite !(assoc_L f), (comm_L f x1).
Qed.
Lemma set_fold_comm_acc_strong {B} (R : relation B) `{!PreOrder R}
(f : A → B → B) (g : B → B) (b : B) X :
(∀ x, Proper (R ==> R) (f x)) →
(∀ x y, x ∈ X → R (f x (g y)) (g (f x y))) →
R (set_fold f (g b) X) (g (set_fold f b X)).
Proof.
intros. unfold set_fold; simpl.
apply foldr_comm_acc_strong; [done|solve_proper|set_solver].
Qed.
Lemma set_fold_comm_acc {B} (f : A → B → B) (g : B → B) (b : B) X :
(∀ x y, f x (g y) = g (f x y)) →
set_fold f (g b) X = g (set_fold f b X).
Proof. intros. apply (set_fold_comm_acc_strong _); [solve_proper|auto]. Qed.
(** * Minimal elements *)
Lemma minimal_exists R `{!Transitive R, ∀ x y, Decision (R x y)} (X : C) :
Lemma minimal_exists_elem_of R `{!Transitive R, ∀ x y, Decision (R x y)} (X : C) :
X ≢ ∅ → ∃ x, x ∈ X ∧ minimal R x X.
Proof.
pattern X; apply set_ind; clear X.
......@@ -325,10 +445,20 @@ Proof.
exists x; split; [set_solver|].
rewrite HX, (right_id _ (∪)). apply singleton_minimal.
Qed.
Lemma minimal_exists_L R `{!LeibnizEquiv C, !Transitive R,
Lemma minimal_exists_elem_of_L R `{!LeibnizEquiv C, !Transitive R,
∀ x y, Decision (R x y)} (X : C) :
X ≠ ∅ → ∃ x, x ∈ X ∧ minimal R x X.
Proof. unfold_leibniz. apply (minimal_exists R). Qed.
Proof. unfold_leibniz. apply (minimal_exists_elem_of R). Qed.
Lemma minimal_exists R `{!Transitive R,
∀ x y, Decision (R x y)} `{!Inhabited A} (X : C) :
∃ x, minimal R x X.
Proof.
destruct (set_choose_or_empty X) as [ (y & Ha) | Hne].
- edestruct (minimal_exists_elem_of R X) as (x & Hel & Hmin); first set_solver.
exists x. done.
- exists inhabitant. intros y Hel. set_solver.
Qed.
(** * Filter *)
Lemma elem_of_filter (P : A → Prop) `{!∀ x, Decision (P x)} X x :
......@@ -386,7 +516,7 @@ End filter.
(** * Map *)
Section map.
Context `{Set_ B D}.
Context `{SemiSet B D}.
Lemma elem_of_map (f : A → B) (X : C) y :
y ∈ set_map (D:=D) f X ↔ ∃ x, y = f x ∧ x ∈ X.
......@@ -436,6 +566,139 @@ Section map.
Proof. unfold_leibniz. apply set_map_singleton. Qed.
End map.
(** * Bind *)
Section set_bind.
Context `{SemiSet B SB}.
Local Notation set_bind := (set_bind (A:=A) (SA:=C) (SB:=SB)).
Lemma elem_of_set_bind (f : A → SB) (X : C) y :
y ∈ set_bind f X ↔ ∃ x, x ∈ X ∧ y ∈ f x.
Proof.
unfold set_bind. rewrite !elem_of_union_list. set_solver.
Qed.
Global Instance set_unfold_set_bind (f : A → SB) (X : C)
(y : B) (P : A → B → Prop) (Q : A → Prop) :
(∀ x y, SetUnfoldElemOf y (f x) (P x y)) →
(∀ x, SetUnfoldElemOf x X (Q x)) →
SetUnfoldElemOf y (set_bind f X) (∃ x, Q x ∧ P x y).
Proof.
intros HSU1 HSU2. constructor.
rewrite elem_of_set_bind. set_solver.
Qed.
Global Instance set_bind_proper :
Proper (pointwise_relation _ (≡) ==> (≡) ==> (≡)) set_bind.
Proof. unfold pointwise_relation; intros f1 f2 Hf X1 X2 HX. set_solver. Qed.
Global Instance set_bind_mono :
Proper (pointwise_relation _ (⊆) ==> (⊆) ==> (⊆)) set_bind.
Proof. unfold pointwise_relation; intros f1 f2 Hf X1 X2 HX. set_solver. Qed.
Lemma set_bind_ext (f g : A → SB) (X Y : C) :
(∀ x, x ∈ X → x ∈ Y → f x ≡ g x) → X ≡ Y → set_bind f X ≡ set_bind g Y.
Proof. set_solver. Qed.
Lemma set_bind_singleton f x : set_bind f {[x]} ≡ f x.
Proof. set_solver. Qed.
Lemma set_bind_singleton_L `{!LeibnizEquiv SB} f x : set_bind f {[x]} = f x.
Proof. unfold_leibniz. apply set_bind_singleton. Qed.
Lemma set_bind_disj_union f (X Y : C) :
X ## Y → set_bind f (X ∪ Y) ≡ set_bind f X ∪ set_bind f Y.
Proof. set_solver. Qed.
Lemma set_bind_disj_union_L `{!LeibnizEquiv SB} f (X Y : C) :
X ## Y → set_bind f (X ∪ Y) = set_bind f X ∪ set_bind f Y.
Proof. unfold_leibniz. apply set_bind_disj_union. Qed.
End set_bind.
(** * OMap *)
Section set_omap.
Context `{SemiSet B D}.
Implicit Types (f : A → option B).
Implicit Types (x : A) (y : B).
Notation set_omap := (set_omap (C:=C) (D:=D)).
Lemma elem_of_set_omap f X y : y ∈ set_omap f X ↔ ∃ x, x ∈ X ∧ f x = Some y.
Proof.
unfold set_omap. rewrite elem_of_list_to_set, elem_of_list_omap.
by setoid_rewrite elem_of_elements.
Qed.
Global Instance set_unfold_omap f X (P : A → Prop) y :
(∀ x, SetUnfoldElemOf x X (P x)) →
SetUnfoldElemOf y (set_omap f X) (∃ x, Some y = f x ∧ P x).
Proof. constructor. rewrite elem_of_set_omap; naive_solver. Qed.
Global Instance set_omap_proper :
Proper (pointwise_relation _ (=) ==> (≡) ==> (≡)) set_omap.
Proof. intros f g Hfg X Y. set_unfold. setoid_rewrite Hfg. naive_solver. Qed.
Global Instance set_omap_mono :
Proper (pointwise_relation _ (=) ==> (⊆) ==> (⊆)) set_omap.
Proof. intros f g Hfg X Y. set_unfold. setoid_rewrite Hfg. naive_solver. Qed.
Lemma elem_of_set_omap_1 f X y : y ∈ set_omap f X → ∃ x, Some y = f x ∧ x ∈ X.
Proof. set_solver. Qed.
Lemma elem_of_set_omap_2 f X x y : x ∈ X → f x = Some y → y ∈ set_omap f X.
Proof. set_solver. Qed.
Lemma set_omap_empty f : set_omap f ∅ = ∅.
Proof. unfold set_omap. by rewrite elements_empty. Qed.
Lemma set_omap_empty_iff f X : set_omap f X ≡ ∅ ↔ set_Forall (λ x, f x = None) X.
Proof.
split; set_unfold; unfold set_Forall.
- intros Hi x Hx. destruct (f x) as [y|] eqn:Hy; naive_solver.
- intros Hi y (x & Hf & Hx). specialize (Hi x Hx). by rewrite Hi in Hf.
Qed.
Lemma set_omap_union f X Y : set_omap f (X ∪ Y) ≡ set_omap f X ∪ set_omap f Y.
Proof. set_solver. Qed.
Lemma set_omap_singleton f x :
set_omap f {[ x ]} ≡ match f x with Some y => {[ y ]} | None => ∅ end.
Proof. set_solver. Qed.
Lemma set_omap_singleton_Some f x y : f x = Some y → set_omap f {[ x ]} ≡ {[ y ]}.
Proof. intros Hx. by rewrite set_omap_singleton, Hx. Qed.
Lemma set_omap_singleton_None f x : f x = None → set_omap f {[ x ]} ≡ ∅.
Proof. intros Hx. by rewrite set_omap_singleton, Hx. Qed.
Lemma set_omap_alt f X : set_omap f X ≡ set_bind (λ x, option_to_set (f x)) X.
Proof. set_solver. Qed.
Lemma set_map_alt (f : A → B) X : set_map f X = set_omap (λ x, Some (f x)) X.
Proof. set_solver. Qed.
Lemma set_omap_filter P `{∀ x, Decision (P x)} f X :
(∀ x, x ∈ X → is_Some (f x) → P x) →
set_omap f (filter P X) ≡ set_omap f X.
Proof. set_solver. Qed.
Section leibniz.
Context `{!LeibnizEquiv D}.
Lemma set_omap_union_L f X Y : set_omap f (X ∪ Y) = set_omap f X ∪ set_omap f Y.
Proof. unfold_leibniz. apply set_omap_union. Qed.
Lemma set_omap_singleton_L f x :
set_omap f {[ x ]} = match f x with Some y => {[ y ]} | None => ∅ end.
Proof. unfold_leibniz. apply set_omap_singleton. Qed.
Lemma set_omap_singleton_Some_L f x y :
f x = Some y → set_omap f {[ x ]} = {[ y ]}.
Proof. unfold_leibniz. apply set_omap_singleton_Some. Qed.
Lemma set_omap_singleton_None_L f x : f x = None → set_omap f {[ x ]} = ∅.
Proof. unfold_leibniz. apply set_omap_singleton_None. Qed.
Lemma set_omap_alt_L f X :
set_omap f X = set_bind (λ x, option_to_set (f x)) X.
Proof. unfold_leibniz. apply set_omap_alt. Qed.
Lemma set_omap_filter_L P `{∀ x, Decision (P x)} f X :
(∀ x, x ∈ X → is_Some (f x) → P x) →
set_omap f (filter P X) = set_omap f X.
Proof. unfold_leibniz. apply set_omap_filter. Qed.
End leibniz.
End set_omap.
(** * Decision procedures *)
Lemma set_Forall_elements P X : set_Forall P X ↔ Forall P (elements X).
Proof. rewrite Forall_forall. by setoid_rewrite elem_of_elements. Qed.
......@@ -532,7 +795,7 @@ Section infinite.
Forall_fresh X xs → Y ⊆ X → Forall_fresh Y xs.
Proof. rewrite !Forall_fresh_alt; set_solver. Qed.
Lemma fresh_list_length n X : length (fresh_list n X) = n.
Lemma length_fresh_list n X : length (fresh_list n X) = n.
Proof. revert X. induction n; simpl; auto. Qed.
Lemma fresh_list_is_fresh n X x : x ∈ fresh_list n X → x ∉ X.
Proof.
......@@ -557,5 +820,5 @@ Lemma size_set_seq `{FinSet nat C} start len :
Proof.
rewrite <-list_to_set_seq, size_list_to_set.
2:{ apply NoDup_seq. }
rewrite seq_length. done.
rewrite length_seq. done.
Qed.
theories/finite.v → stdpp/finite.v
View file @ 9274984b
......@@ -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} :
......@@ -216,9 +216,14 @@ 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}.
......@@ -233,12 +238,16 @@ Section surjective_finite.
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}.
Definition bijective_finite : Finite B :=
let _ := cancel_surj (f:=f) (g:=g) in
surjective_finite f.
Program Definition bijective_finite : Finite B :=
{| enum := f <$> enum A |}.
Next Obligation. apply (NoDup_fmap f), NoDup_enum. Qed.
Next Obligation.
intros b. rewrite elem_of_list_fmap. destruct (surj f b).
eauto using elem_of_enum.
Qed.
End bijective_finite.
Global Program Instance option_finite `{Finite A} : Finite (option A) :=
......@@ -253,7 +262,7 @@ 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.
Global Program Instance Empty_set_finite : Finite Empty_set := {| enum := [] |}.
Next Obligation. by apply NoDup_nil. Qed.
......@@ -288,76 +297,65 @@ 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.
Global Program Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type :=
{| enum := foldr (λ x, (pair x <$> enum B ++.)) [] (enum A) |}.
{| enum := a ← enum A; (a,.) <$> enum B |}.
Next Obligation.
intros A ?????. 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 auto ]. by intro; destruct Hx; right.
- 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.
Global 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 A ?? n. 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 A ?? n [l Hl]. revert l Hl.
induction n as [|n IH]; intros [|x l] Hl; 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; [|done]. by apply (sig_eq_pi _).
- 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.
Global Program Instance fin_finite n : Finite (fin n) := {| enum := fin_enum n |}.
......@@ -371,7 +369,7 @@ 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 :
......@@ -417,7 +415,7 @@ 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) :
......
theories/functions.v → stdpp/functions.v
View file @ 9274984b
File moved
stdpp/gmap.v 0 → 100644
View file @ 9274984b
This diff is collapsed.
theories/hashset.v → stdpp/hashset.v
View file @ 9274984b
......@@ -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.
......@@ -105,7 +105,7 @@ Proof.
- 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' [??] Hm];
csimpl; inversion_clear 1 as [|?? Hn]; [constructor|].
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).
......
theories/hlist.v → stdpp/hlist.v
View file @ 9274984b
File moved
theories/infinite.v → stdpp/infinite.v
View file @ 9274984b
......@@ -37,7 +37,7 @@ Section search_infinite.
Context `{!Inj (=) (=) f, !EqDecision B}.
Lemma search_infinite_R_wf xs : wf (R xs).
Lemma search_infinite_R_wf xs : well_founded (R xs).
Proof.
revert xs. assert (help : ∀ xs n n',
Acc (R (filter (.≠ f n') xs)) n → n' < n → Acc (R xs) n).
......@@ -45,7 +45,7 @@ Section search_infinite.
split; [done|]. apply elem_of_list_filter; naive_solver lia. }
intros xs. induction (well_founded_ltof _ length xs) as [xs _ IH].
intros n1; constructor; intros n2 [Hn Hs].
apply help with (n2 - 1); [|lia]. apply IH. eapply filter_length_lt; eauto.
apply help with (n2 - 1); [|lia]. apply IH. eapply length_filter_lt; eauto.
Qed.
Definition search_infinite_go (xs : list B) (n : nat)
......@@ -143,7 +143,7 @@ Global Program Instance list_infinite `{Inhabited A} : Infinite (list A) := {|
Next Obligation.
intros A ? xs ?. destruct (infinite_is_fresh (length <$> xs)).
apply elem_of_list_fmap. eexists; split; [|done].
unfold fresh. by rewrite replicate_length.
unfold fresh. by rewrite length_replicate.
Qed.
Next Obligation. unfold fresh. by intros A ? xs1 xs2 ->. Qed.
......
theories/lexico.v → stdpp/lexico.v
View file @ 9274984b
......@@ -19,7 +19,7 @@ Global Instance bool_lexico : Lexico bool := λ b1 b2,
Global Instance nat_lexico : Lexico nat := (<).
Global Instance N_lexico : Lexico N := (<)%N.
Global Instance Z_lexico : Lexico Z := (<)%Z.
Typeclasses Opaque bool_lexico nat_lexico N_lexico Z_lexico.
Global Typeclasses Opaque bool_lexico nat_lexico N_lexico Z_lexico.
Global Instance list_lexico `{Lexico A} : Lexico (list A) :=
fix go l1 l2 :=
let _ : Lexico (list A) := @go in
......@@ -138,7 +138,7 @@ Proof.
| _ :: _, [] => inright _
| x1 :: l1, x2 :: l2 => cast_trichotomy (trichotomyT lexico (x1,l1) (x2,l2))
end); clear tA go go';
abstract (repeat (done || constructor || congruence || by inversion 1)).
abstract (repeat (done || constructor || congruence || by inv 1)).
Defined.
Global Instance sig_lexico_po `{Lexico A, !StrictOrder (@lexico A _)}
......
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.
stdpp/list_monad.v 0 → 100644
View file @ 9274984b
This diff is collapsed.
theories/list_numbers.v → stdpp/list_numbers.v
View file @ 9274984b
(** This file collects general purpose definitions and theorems on
lists of numbers that are not in the Coq standard library. *)
From stdpp Require Export list.
From stdpp Require Export list_basics list_monad list_misc list_tactics.
From stdpp Require Import options.
(** * Definitions *)
......@@ -51,6 +51,12 @@ Fixpoint little_endian_to_Z (n : Z) (bs : list Z) : Z :=
Section seq.
Implicit Types m n i j : nat.
(* TODO: Coq 8.20 has the same lemma under the same name, so remove our version
once we require Coq 8.20. In Coq 8.19 and before, this lemma is called
[seq_length]. *)
Lemma length_seq m n : length (seq m n) = n.
Proof. revert m. induction n; intros; f_equal/=; auto. Qed.
Lemma fmap_add_seq j j' n : Nat.add j <$> seq j' n = seq (j + j') n.
Proof.
revert j'. induction n as [|n IH]; intros j'; csimpl; [reflexivity|].
......@@ -87,26 +93,44 @@ Section seq.
Qed.
Lemma NoDup_seq j n : NoDup (seq j n).
Proof. apply NoDup_ListNoDup, seq_NoDup. Qed.
(* FIXME: This lemma is in the stdlib since Coq 8.12 *)
Lemma seq_S n j : seq j (S n) = seq j n ++ [j + n].
Proof.
revert j. induction n as [|n IH]; intros j; f_equal/=; [done |].
by rewrite IH, Nat.add_succ_r.
Qed.
Lemma elem_of_seq j n k :
k ∈ seq j n ↔ j ≤ k < j + n.
Proof. rewrite elem_of_list_In, in_seq. done. Qed.
Lemma seq_nil n m : seq n m = [] ↔ m = 0.
Proof. by destruct m. Qed.
Lemma seq_subseteq_mono m n1 n2 : n1 ≤ n2 → seq m n1 ⊆ seq m n2.
Proof. by intros Hle i Hi%elem_of_seq; apply elem_of_seq; lia. Qed.
Lemma Forall_seq (P : nat → Prop) i n :
Forall P (seq i n) ↔ ∀ j, i ≤ j < i + n → P j.
Proof. rewrite Forall_forall. setoid_rewrite elem_of_seq. auto with lia. Qed.
Lemma drop_seq j n m :
drop m (seq j n) = seq (j + m) (n - m).
Proof.
revert j m. induction n as [|n IH]; simpl; intros j m.
- rewrite drop_nil. done.
- destruct m; simpl.
+ rewrite Nat.add_0_r. done.
+ rewrite IH. f_equal; lia.
Qed.
Lemma take_seq j n m :
take m (seq j n) = seq j (m `min` n).
Proof.
revert j m. induction n as [|n IH]; simpl; intros j m.
- rewrite take_nil. replace (m `min` 0) with 0 by lia. done.
- destruct m; simpl; auto with f_equal.
Qed.
End seq.
(** ** Properties of the [seqZ] function *)
Section seqZ.
Implicit Types (m n : Z) (i j : nat).
Local Open Scope Z.
Local Open Scope Z_scope.
Lemma seqZ_nil m n : n ≤ 0 → seqZ m n = [].
Proof. by destruct n. Qed.
......@@ -117,11 +141,11 @@ Section seqZ.
rewrite <-fmap_S_seq, <-list_fmap_compose.
apply map_ext; naive_solver lia.
Qed.
Lemma seqZ_length m n : length (seqZ m n) = Z.to_nat n.
Proof. unfold seqZ; by rewrite fmap_length, seq_length. Qed.
Lemma length_seqZ m n : length (seqZ m n) = Z.to_nat n.
Proof. unfold seqZ; by rewrite length_fmap, length_seq. Qed.
Lemma fmap_add_seqZ m m' n : Z.add m <$> seqZ m' n = seqZ (m + m') n.
Proof.
revert m'. induction n as [|n ? IH|] using (Z_succ_pred_induction 0); intros m'.
revert m'. induction n as [|n ? IH|] using (Z.succ_pred_induction 0); intros m'.
- by rewrite seqZ_nil.
- rewrite (seqZ_cons m') by lia. rewrite (seqZ_cons (m + m')) by lia.
f_equal/=. rewrite Z.pred_succ, IH; simpl. f_equal; lia.
......@@ -129,7 +153,7 @@ Section seqZ.
Qed.
Lemma lookup_seqZ_lt m n i : Z.of_nat i < n → seqZ m n !! i = Some (m + Z.of_nat i).
Proof.
revert m i. induction n as [|n ? IH|] using (Z_succ_pred_induction 0);
revert m i. induction n as [|n ? IH|] using (Z.succ_pred_induction 0);
intros m i Hi; [lia| |lia].
rewrite seqZ_cons by lia. destruct i as [|i]; simpl.
- f_equal; lia.
......@@ -140,7 +164,7 @@ Section seqZ.
Lemma lookup_seqZ_ge m n i : n ≤ Z.of_nat i → seqZ m n !! i = None.
Proof.
revert m i.
induction n as [|n ? IH|] using (Z_succ_pred_induction 0); intros m i Hi; try lia.
induction n as [|n ? IH|] using (Z.succ_pred_induction 0); intros m i Hi; try lia.
- by rewrite seqZ_nil.
- rewrite seqZ_cons by lia.
destruct i as [|i]; simpl; [lia|]. by rewrite Z.pred_succ, IH by lia.
......@@ -164,7 +188,7 @@ Section seqZ.
Proof.
intros. unfold seqZ. rewrite Z2Nat.inj_add, seq_app, fmap_app by done.
f_equal. rewrite Nat.add_comm, <-!fmap_add_seq, <-list_fmap_compose.
apply list_fmap_ext; [|done]; intros j; simpl.
apply list_fmap_ext; intros j n; simpl.
rewrite Nat2Z.inj_add, Z2Nat.id by done. lia.
Qed.
......@@ -206,7 +230,7 @@ Section sum_list.
sum_list szs = length l → mjoin (reshape szs l) = l.
Proof.
revert l. induction szs as [|sz szs IH]; simpl; intros l Hl; [by destruct l|].
by rewrite IH, take_drop by (rewrite drop_length; lia).
by rewrite IH, take_drop by (rewrite length_drop; lia).
Qed.
Lemma sum_list_replicate n m : sum_list (replicate m n) = m * n.
Proof. induction m; simpl; auto. Qed.
......@@ -226,6 +250,10 @@ Section mjoin.
Implicit Types l k : list A.
Implicit Types ls : list (list A).
Lemma length_join ls:
length (mjoin ls) = sum_list (length <$> ls).
Proof. induction ls; [done|]; csimpl. rewrite length_app. lia. Qed.
Lemma join_lookup_Some ls i x :
mjoin ls !! i = Some x ↔ ∃ j l i', ls !! j = Some l ∧ l !! i' = Some x
∧ i = sum_list (length <$> take j ls) + i'.
......@@ -247,7 +275,7 @@ Section mjoin.
intros Hl. rewrite join_lookup_Some.
f_equiv; intros j. f_equiv; intros l. f_equiv; intros i'.
assert (ls !! j = Some l → j < length ls) by eauto using lookup_lt_Some.
rewrite (sum_list_fmap_same n), take_length by auto using Forall_take.
rewrite (sum_list_fmap_same n), length_take by auto using Forall_take.
naive_solver lia.
Qed.
......@@ -260,7 +288,7 @@ Section mjoin.
split; [|naive_solver].
destruct 1 as (j'&l'&i'&?&?&Hj); decompose_Forall.
assert (i' < length l') by eauto using lookup_lt_Some.
apply Nat_mul_split_l in Hj; naive_solver.
apply Nat.mul_split_l in Hj; naive_solver.
Qed.
End mjoin.
......@@ -311,16 +339,16 @@ Section Z_little_endian.
intros -> ?. induction 1 as [|b bs ? ? IH]; [done|]; simpl.
rewrite Nat2Z.inj_succ, Z_to_little_endian_succ by lia. f_equal.
- apply Z.bits_inj_iff'. intros z' ?.
rewrite !Z.land_spec, Z.lor_spec, Z_ones_spec by lia.
rewrite !Z.land_spec, Z.lor_spec, Z.ones_spec by lia.
case_bool_decide.
+ rewrite andb_true_r, Z.shiftl_spec_low, orb_false_r by lia. done.
+ rewrite andb_false_r.
symmetry. eapply (Z_bounded_iff_bits_nonneg n); lia.
symmetry. eapply (Z.bounded_iff_bits_nonneg n); lia.
- rewrite <-IH at 3. f_equal.
apply Z.bits_inj_iff'. intros z' ?.
rewrite Z.shiftr_spec, Z.lor_spec, Z.shiftl_spec by lia.
assert (Z.testbit b (z' + n) = false) as ->.
{ apply (Z_bounded_iff_bits_nonneg n); lia. }
{ apply (Z.bounded_iff_bits_nonneg n); lia. }
rewrite orb_false_l. f_equal. lia.
Qed.
......@@ -330,25 +358,25 @@ Section Z_little_endian.
Proof.
intros ? Hm. rewrite <-Z.land_ones by lia.
revert z.
induction m as [|m ? IH|] using (Z_succ_pred_induction 0); intros z; [..|lia].
induction m as [|m ? IH|] using (Z.succ_pred_induction 0); intros z; [..|lia].
{ Z.bitwise. by rewrite andb_false_r. }
rewrite Z_to_little_endian_succ by lia; simpl. rewrite IH by lia.
apply Z.bits_inj_iff'. intros z' ?.
rewrite Z.land_spec, Z.lor_spec, Z.shiftl_spec, !Z.land_spec by lia.
rewrite (Z_ones_spec n z') by lia. case_bool_decide.
rewrite (Z.ones_spec n z') by lia. case_bool_decide.
- rewrite andb_true_r, (Z.testbit_neg_r _ (z' - n)), orb_false_r by lia. simpl.
by rewrite Z_ones_spec, bool_decide_true, andb_true_r by lia.
by rewrite Z.ones_spec, bool_decide_true, andb_true_r by lia.
- rewrite andb_false_r, orb_false_l.
rewrite Z.shiftr_spec by lia. f_equal; [f_equal; lia|].
rewrite !Z_ones_spec by lia. apply bool_decide_ext. lia.
rewrite !Z.ones_spec by lia. apply bool_decide_ext. lia.
Qed.
Lemma Z_to_little_endian_length m n z :
Lemma length_Z_to_little_endian m n z :
0 ≤ m →
Z.of_nat (length (Z_to_little_endian m n z)) = m.
Proof.
intros. revert z. induction m as [|m ? IH|]
using (Z_succ_pred_induction 0); intros z; [done| |lia].
using (Z.succ_pred_induction 0); intros z; [done| |lia].
rewrite Z_to_little_endian_succ by lia. simpl. by rewrite Nat2Z.inj_succ, IH.
Qed.
......@@ -357,7 +385,7 @@ Section Z_little_endian.
Forall (λ b, 0 ≤ b < 2 ^ n) (Z_to_little_endian m n z).
Proof.
intros. revert z.
induction m as [|m ? IH|] using (Z_succ_pred_induction 0); intros z; [..|lia].
induction m as [|m ? IH|] using (Z.succ_pred_induction 0); intros z; [..|lia].
{ by constructor. }
rewrite Z_to_little_endian_succ by lia.
constructor; [|by apply IH]. rewrite Z.land_ones by lia.
......@@ -370,12 +398,12 @@ Section Z_little_endian.
0 ≤ little_endian_to_Z n bs < 2 ^ (Z.of_nat (length bs) * n).
Proof.
intros ?. induction 1 as [|b bs Hb ? IH]; [done|]; simpl.
apply Z_bounded_iff_bits_nonneg'; [lia|..].
apply Z.bounded_iff_bits_nonneg'; [lia|..].
{ apply Z.lor_nonneg. split; [lia|]. apply Z.shiftl_nonneg. lia. }
intros z' ?. rewrite Z.lor_spec.
rewrite Z_bounded_iff_bits_nonneg' in Hb by lia.
rewrite Z.bounded_iff_bits_nonneg' in Hb by lia.
rewrite Hb, orb_false_l, Z.shiftl_spec by lia.
apply (Z_bounded_iff_bits_nonneg' (Z.of_nat (length bs) * n)); lia.
apply (Z.bounded_iff_bits_nonneg' (Z.of_nat (length bs) * n)); lia.
Qed.
Lemma Z_to_little_endian_lookup_Some m n z (i : nat) x :
......@@ -383,7 +411,7 @@ Section Z_little_endian.
Z_to_little_endian m n z !! i = Some x ↔
Z.of_nat i < m ∧ x = Z.land (z ≫ (Z.of_nat i * n)) (Z.ones n).
Proof.
revert z i. induction m as [|m ? IH|] using (Z_succ_pred_induction 0);
revert z i. induction m as [|m ? IH|] using (Z.succ_pred_induction 0);
intros z i ??; [..|lia].
{ destruct i; simpl; naive_solver lia. }
rewrite Z_to_little_endian_succ by lia. destruct i as [|i]; simpl.
......@@ -411,7 +439,7 @@ Section Z_little_endian.
rewrite Hdiv in Hlookup; simplify_eq/=.
rewrite Z.lor_spec, Z.shiftl_spec, IH by auto with lia.
assert (Z.testbit b' i = false) as ->.
{ apply (Z_bounded_iff_bits_nonneg n); lia. }
{ apply (Z.bounded_iff_bits_nonneg n); lia. }
by rewrite <-Zminus_mod_idemp_r, Z_mod_same_full, Z.sub_0_r.
Qed.
End Z_little_endian.