diff --git a/theories/ars.v b/theories/ars.v
index dd3484a4bb4ca59fda1bf896d493965b676b6cf7..7bbe16d34a02f94c3237dcf32b9b88806821590e 100644
--- a/theories/ars.v
+++ b/theories/ars.v
@@ -170,8 +170,7 @@ Hint Extern 5 (subrelation _ (tc _)) =>
eapply @tc_once_subrel : typeclass_instances.
Hint Resolve
- rtc_once rtc_r
- tc_r
+ rtc_once rtc_r tc_r
bsteps_once bsteps_r bsteps_refl bsteps_trans : ars.
(** * Theorems on sub relations *)
diff --git a/theories/base.v b/theories/base.v
index 10c91ff0296ab8cafb1ff9a863b6de712c82fc5b..dc7953fd512709b44fd5edd2d421eddd6395b063 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -6,7 +6,7 @@ abstract interfaces for ordered structures, collections, and various other data
structures. *)
Global Generalizable All Variables.
Global Set Automatic Coercions Import.
-Require Export Morphisms RelationClasses List Bool Utf8 Program Setoid NArith.
+Require Export Morphisms RelationClasses List Bool Utf8 Program Setoid.
(** * General *)
(** The following coercion allows us to use Booleans as propositions. *)
@@ -17,6 +17,7 @@ applied. *)
Arguments id _ _/.
Arguments compose _ _ _ _ _ _ /.
Arguments flip _ _ _ _ _ _/.
+Typeclasses Transparent id compose flip.
(** Change [True] and [False] into notations in order to enable overloading.
We will use this in the file [assertions] to give [True] and [False] a
@@ -415,10 +416,6 @@ Definition delete_list `{Delete K M} (l : list K) (m : M) : M :=
fold_right delete m l.
Instance: Params (@delete_list) 3.
-Definition insert_consecutive `{Insert nat A M} (i : nat) (l : list A)
- (m : M) : M := fold_right (λ x f i, <[i:=x]>(f (S i))) (λ _, m) l i.
-Instance: Params (@insert_consecutive) 3.
-
(** The function [union_with f m1 m2] is supposed to yield the union of [m1]
and [m2] using the function [f] to combine values of members that are in
both [m1] and [m2]. *)
@@ -451,6 +448,10 @@ Class Injective {A B} (R : relation A) (S : relation B) (f : A → B) : Prop :=
Class Injective2 {A B C} (R1 : relation A) (R2 : relation B)
(S : relation C) (f : A → B → C) : Prop :=
injective2: ∀ x1 x2 y1 y2, S (f x1 x2) (f y1 y2) → R1 x1 y1 ∧ R2 x2 y2.
+Class Cancel {A B} (S : relation B) (f : A → B) (g : B → A) : Prop :=
+ cancel: ∀ x, S (f (g x)) x.
+Class Surjective {A B} (R : relation B) (f : A → B) :=
+ surjective : ∀ y, ∃ x, R (f x) y.
Class Idempotent {A} (R : relation A) (f : A → A → A) : Prop :=
idempotent: ∀ x, R (f x x) x.
Class Commutative {A B} (R : relation A) (f : B → B → A) : Prop :=
@@ -475,6 +476,8 @@ Class AntiSymmetric {A} (R S : relation A) : Prop :=
Arguments irreflexivity {_} _ {_} _ _.
Arguments injective {_ _ _ _} _ {_} _ _ _.
Arguments injective2 {_ _ _ _ _ _} _ {_} _ _ _ _ _.
+Arguments cancel {_ _ _} _ _ {_} _.
+Arguments surjective {_ _ _} _ {_} _.
Arguments idempotent {_ _} _ {_} _.
Arguments commutative {_ _ _} _ {_} _ _.
Arguments left_id {_ _} _ _ {_} _.
@@ -486,55 +489,6 @@ Arguments left_distr {_ _} _ _ {_} _ _ _.
Arguments right_distr {_ _} _ _ {_} _ _ _.
Arguments anti_symmetric {_ _} _ {_} _ _ _ _.
-Lemma impl_transitive (P Q R : Prop) : (P → Q) → (Q → R) → (P → R).
-Proof. tauto. Qed.
-Instance: Commutative (↔) (@eq A).
-Proof. red. intuition. Qed.
-Instance: Commutative (↔) (λ x y, @eq A y x).
-Proof. red. intuition. Qed.
-Instance: Commutative (↔) (↔).
-Proof. red. intuition. Qed.
-Instance: Commutative (↔) (∧).
-Proof. red. intuition. Qed.
-Instance: Associative (↔) (∧).
-Proof. red. intuition. Qed.
-Instance: Idempotent (↔) (∧).
-Proof. red. intuition. Qed.
-Instance: Commutative (↔) (∨).
-Proof. red. intuition. Qed.
-Instance: Associative (↔) (∨).
-Proof. red. intuition. Qed.
-Instance: Idempotent (↔) (∨).
-Proof. red. intuition. Qed.
-Instance: LeftId (↔) True (∧).
-Proof. red. intuition. Qed.
-Instance: RightId (↔) True (∧).
-Proof. red. intuition. Qed.
-Instance: LeftAbsorb (↔) False (∧).
-Proof. red. intuition. Qed.
-Instance: RightAbsorb (↔) False (∧).
-Proof. red. intuition. Qed.
-Instance: LeftId (↔) False (∨).
-Proof. red. intuition. Qed.
-Instance: RightId (↔) False (∨).
-Proof. red. intuition. Qed.
-Instance: LeftAbsorb (↔) True (∨).
-Proof. red. intuition. Qed.
-Instance: RightAbsorb (↔) True (∨).
-Proof. red. intuition. Qed.
-Instance: LeftId (↔) True impl.
-Proof. unfold impl. red. intuition. Qed.
-Instance: RightAbsorb (↔) True impl.
-Proof. unfold impl. red. intuition. Qed.
-Instance: LeftDistr (↔) (∧) (∨).
-Proof. red. intuition. Qed.
-Instance: RightDistr (↔) (∧) (∨).
-Proof. red. intuition. Qed.
-Instance: LeftDistr (↔) (∨) (∧).
-Proof. red. intuition. Qed.
-Instance: RightDistr (↔) (∨) (∧).
-Proof. red. intuition. Qed.
-
(** The following lemmas are specific versions of the projections of the above
type classes for Leibniz equality. These lemmas allow us to enforce Coq not to
use the setoid rewriting mechanism. *)
@@ -696,11 +650,9 @@ Notation "x .½" := (half x) (at level 20, format "x .½") : C_scope.
Lemma proj1_sig_inj {A} (P : A → Prop) x (Px : P x) y (Py : P y) :
x↾Px = y↾Py → x = y.
Proof. injection 1; trivial. Qed.
-Lemma not_symmetry `{R : relation A} `{!Symmetric R} (x y : A) :
- ¬R x y → ¬R y x.
+Lemma not_symmetry `{R : relation A} `{!Symmetric R} x y : ¬R x y → ¬R y x.
Proof. intuition. Qed.
-Lemma symmetry_iff `(R : relation A) `{!Symmetric R} (x y : A) :
- R x y ↔ R y x.
+Lemma symmetry_iff `(R : relation A) `{!Symmetric R} x y : R x y ↔ R y x.
Proof. intuition. Qed.
(** ** Pointwise relations *)
@@ -765,11 +717,15 @@ Section prod_relation.
End prod_relation.
(** ** Other *)
-Definition proj_relation {A B} (R : relation A)
- (f : B → A) : relation B := λ x y, R (f x) (f y).
-Definition proj_relation_equivalence {A B} (R : relation A) (f : B → A) :
- Equivalence R → Equivalence (proj_relation R f).
-Proof. unfold proj_relation. firstorder auto. Qed.
+Definition proj_eq {A B} (f : B → A) : relation B := λ x y, f x = f y.
+Global Instance proj_eq_equivalence `(f : B → A) : Equivalence (proj_eq f).
+Proof. unfold proj_eq. repeat split; red; intuition congruence. Qed.
+Notation "x ~{ f } y" := (proj_eq f x y)
+ (at level 70, format "x ~{ f } y") : C_scope.
+Notation "(~{ f } )" := (proj_eq f) (f at level 10, only parsing) : C_scope.
+
+Hint Extern 0 (_ ~{_} _) => reflexivity.
+Hint Extern 0 (_ ~{_} _) => symmetry; assumption.
Instance: ∀ A B (x : B), Commutative (=) (λ _ _ : A, x).
Proof. red. trivial. Qed.
@@ -799,3 +755,96 @@ Proof. red. trivial. Qed.
Instance idem_propholds {A} (R : relation A) f :
Idempotent R f → ∀ x, PropHolds (R (f x x) x).
Proof. red. trivial. Qed.
+
+Lemma injective_iff {A B} {R : relation A} {S : relation B} (f : A → B)
+ `{!Injective R S f} `{!Proper (R ==> S) f} x y : S (f x) (f y) ↔ R x y.
+Proof. firstorder. Qed.
+Instance: Injective (=) (=) (@inl A B).
+Proof. injection 1; auto. Qed.
+Instance: Injective (=) (=) (@inr A B).
+Proof. injection 1; auto. Qed.
+Instance: Injective2 (=) (=) (=) (@pair A B).
+Proof. injection 1; auto. Qed.
+Instance: ∀ `{Injective2 A B C R1 R2 R3 f} y, Injective R1 R3 (λ x, f x y).
+Proof. repeat intro; edestruct (injective2 f); eauto. Qed.
+Instance: ∀ `{Injective2 A B C R1 R2 R3 f} x, Injective R2 R3 (f x).
+Proof. repeat intro; edestruct (injective2 f); eauto. Qed.
+
+Lemma cancel_injective `{Cancel A B R1 f g}
+ `{!Equivalence R1} `{!Proper (R2 ==> R1) f} : Injective R1 R2 g.
+Proof.
+ intros x y E. rewrite <-(cancel f g x), <-(cancel f g y), E. reflexivity.
+Qed.
+Lemma cancel_surjective `{Cancel A B R1 f g} : Surjective R1 f.
+Proof. intros y. exists (g y). auto. Qed.
+
+Lemma impl_transitive (P Q R : Prop) : (P → Q) → (Q → R) → (P → R).
+Proof. tauto. Qed.
+Instance: Commutative (↔) (@eq A).
+Proof. red. intuition. Qed.
+Instance: Commutative (↔) (λ x y, @eq A y x).
+Proof. red. intuition. Qed.
+Instance: Commutative (↔) (↔).
+Proof. red. intuition. Qed.
+Instance: Commutative (↔) (∧).
+Proof. red. intuition. Qed.
+Instance: Associative (↔) (∧).
+Proof. red. intuition. Qed.
+Instance: Idempotent (↔) (∧).
+Proof. red. intuition. Qed.
+Instance: Commutative (↔) (∨).
+Proof. red. intuition. Qed.
+Instance: Associative (↔) (∨).
+Proof. red. intuition. Qed.
+Instance: Idempotent (↔) (∨).
+Proof. red. intuition. Qed.
+Instance: LeftId (↔) True (∧).
+Proof. red. intuition. Qed.
+Instance: RightId (↔) True (∧).
+Proof. red. intuition. Qed.
+Instance: LeftAbsorb (↔) False (∧).
+Proof. red. intuition. Qed.
+Instance: RightAbsorb (↔) False (∧).
+Proof. red. intuition. Qed.
+Instance: LeftId (↔) False (∨).
+Proof. red. intuition. Qed.
+Instance: RightId (↔) False (∨).
+Proof. red. intuition. Qed.
+Instance: LeftAbsorb (↔) True (∨).
+Proof. red. intuition. Qed.
+Instance: RightAbsorb (↔) True (∨).
+Proof. red. intuition. Qed.
+Instance: LeftId (↔) True impl.
+Proof. unfold impl. red. intuition. Qed.
+Instance: RightAbsorb (↔) True impl.
+Proof. unfold impl. red. intuition. Qed.
+Instance: LeftDistr (↔) (∧) (∨).
+Proof. red. intuition. Qed.
+Instance: RightDistr (↔) (∧) (∨).
+Proof. red. intuition. Qed.
+Instance: LeftDistr (↔) (∨) (∧).
+Proof. red. intuition. Qed.
+Instance: RightDistr (↔) (∨) (∧).
+Proof. red. intuition. Qed.
+Lemma not_injective `{Injective A B R R' f} x y : ¬R x y → ¬R' (f x) (f y).
+Proof. intuition. Qed.
+Instance injective_compose {A B C} R1 R2 R3 (f : A → B) (g : B → C) :
+ Injective R1 R2 f → Injective R2 R3 g → Injective R1 R3 (g ∘ f).
+Proof. red; intuition. Qed.
+Instance surjective_compose {A B C} R (f : A → B) (g : B → C) :
+ Surjective (=) f → Surjective R g → Surjective R (g ∘ f).
+Proof.
+ intros ?? x. unfold compose. destruct (surjective g x) as [y ?].
+ destruct (surjective f y) as [z ?]. exists z. congruence.
+Qed.
+
+Section sig_map.
+ Context `{P : A → Prop} `{Q : B → Prop} (f : A → B) (Hf : ∀ x, P x → Q (f x)).
+ Definition sig_map (x : sig P) : sig Q := f (`x) ↾ Hf _ (proj2_sig x).
+ Global Instance sig_map_injective:
+ (∀ x, ProofIrrel (P x)) → Injective (=) (=) f → Injective (=) (=) sig_map.
+ Proof.
+ intros ?? [x Hx] [y Hy]. injection 1. intros Hxy.
+ apply (injective f) in Hxy; subst. rewrite (proof_irrel _ Hy). auto.
+ Qed.
+End sig_map.
diff --git a/theories/collections.v b/theories/collections.v
index 754efa114f759c49e0477da4f3b01f1331f80073..78f8cd0bb4a0ac758dac13105f253d3ac1ec4b60 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -489,7 +489,7 @@ Section collection_monad.
* revert l. induction k; esolve_elem_of.
* induction 1; esolve_elem_of.
Qed.
- Lemma mapM_length {A B} (f : A → M B) l k :
+ Lemma collection_mapM_length {A B} (f : A → M B) l k :
l ∈ mapM f k → length l = length k.
Proof. revert l; induction k; esolve_elem_of. Qed.
diff --git a/theories/fin_collections.v b/theories/fin_collections.v
index fac0f1bdf63a9dfd127d98fa5be179a220c293d5..ba6f96b1b488b02ee9dcf7aa23b7da435e1075fb 100644
--- a/theories/fin_collections.v
+++ b/theories/fin_collections.v
@@ -3,10 +3,11 @@
(** This file collects definitions and theorems on finite collections. Most
importantly, it implements a fold and size function and some useful induction
principles on finite collections . *)
-Require Import Permutation ars.
-Require Export collections numbers listset.
+Require Import Permutation ars listset.
+Require Export numbers collections.
-Definition choose `{Elements A C} (X : C) : option A := head (elements X).
+Definition collection_choose `{Elements A C} (X : C) : option A :=
+ head (elements X).
Instance collection_size `{Elements A C} : Size C := length ∘ elements.
Definition collection_fold `{Elements A C} {B}
(f : A → B → B) (b : B) : C → B := foldr f b ∘ elements.
@@ -56,23 +57,27 @@ Proof.
rewrite (nil_length l), !elem_of_list_singleton by done. congruence.
Qed.
-Lemma choose_Some X x : choose X = Some x → x ∈ X.
+Lemma collection_choose_Some X x : collection_choose X = Some x → x ∈ X.
Proof.
- unfold choose. destruct (elements X) eqn:E; intros; simplify_equality.
- rewrite elements_spec, E. by left.
+ unfold collection_choose. destruct (elements X) eqn:E; intros;
+ simplify_equality. rewrite elements_spec, E. by left.
Qed.
-Lemma choose_None X : choose X = None → X ≡ ∅.
+Lemma collection_choose_None X : collection_choose X = None → X ≡ ∅.
Proof.
- unfold choose. destruct (elements X) eqn:E; intros; simplify_equality.
+ unfold collection_choose.
+ destruct (elements X) eqn:E; intros; simplify_equality.
apply equiv_empty. intros x. by rewrite elements_spec, E, elem_of_nil.
Qed.
Lemma elem_of_or_empty X : (∃ x, x ∈ X) ∨ X ≡ ∅.
-Proof. destruct (choose X) eqn:?; eauto using choose_Some, choose_None. Qed.
-Lemma choose_is_Some X : X ≢ ∅ ↔ is_Some (choose X).
Proof.
- destruct (choose X) eqn:?.
- * rewrite elem_of_equiv_empty. split; eauto using choose_Some.
- * split. intros []; eauto using choose_None. by intros [??].
+ destruct (collection_choose X) eqn:?;
+ eauto using collection_choose_Some, collection_choose_None.
+Qed.
+Lemma collection_choose_is_Some X : X ≢ ∅ ↔ is_Some (collection_choose X).
+Proof.
+ destruct (collection_choose X) eqn:?.
+ * rewrite elem_of_equiv_empty. split; eauto using collection_choose_Some.
+ * split. intros []; eauto using collection_choose_None. by intros [??].
Qed.
Lemma not_elem_of_equiv_empty X : X ≢ ∅ ↔ (∃ x, x ∈ X).
Proof.
@@ -156,8 +161,7 @@ Qed.
Lemma collection_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B) :
Proper ((=) ==> (≡) ==> iff) P →
- P b ∅ →
- (∀ x X r, x ∉ X → P r X → P (f x r) ({[ x ]} ∪ X)) →
+ P b ∅ → (∀ x X r, x ∉ X → P r X → P (f x r) ({[ x ]} ∪ X)) →
∀ X, P (collection_fold f b X) X.
Proof.
intros ? Hemp Hadd.
@@ -184,7 +188,6 @@ Proof.
abstract (unfold set_Forall; setoid_rewrite elements_spec;
by rewrite <-Forall_forall).
Defined.
-
Global Instance set_Exists_dec `(P : A → Prop) `{∀ x, Decision (P x)} X :
Decision (set_Exists P X) | 100.
Proof.
@@ -192,7 +195,6 @@ Proof.
abstract (unfold set_Exists; setoid_rewrite elements_spec;
by rewrite <-Exists_exists).
Defined.
-
Global Instance rel_elem_of_dec `{∀ x y, Decision (R x y)} x X :
Decision (elem_of_upto R x X) | 100 := decide (set_Exists (R x) X).
End fin_collection.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 81b1f286be80a6d3176ea8f19deb0631984e5b4b..9329ffc3f3e64e57287cb4d74bbd6851de27e14e 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -135,14 +135,21 @@ Lemma map_subset_empty {A} (m : M A) : m ⊄ ∅.
Proof. intros [? []]. intros i x. by rewrite lookup_empty. Qed.
(** ** Properties of the [partial_alter] operation *)
-Lemma partial_alter_compose {A} (m : M A) i f g :
+Lemma partial_alter_ext {A} (f g : option A → option A) (m : M A) i :
+ (∀ x, m !! i = x → f x = g x) → partial_alter f i m = partial_alter g i m.
+Proof.
+ intros Hfg. apply map_eq. intros j. destruct (decide (i = j)); subst.
+ * rewrite !lookup_partial_alter. by apply Hfg.
+ * by rewrite !lookup_partial_alter_ne.
+Qed.
+Lemma partial_alter_compose {A} f g (m : M A) i:
partial_alter (f ∘ g) i m = partial_alter f i (partial_alter g i m).
Proof.
intros. apply map_eq. intros ii. case (decide (i = ii)).
* intros. subst. by rewrite !lookup_partial_alter.
* intros. by rewrite !lookup_partial_alter_ne.
Qed.
-Lemma partial_alter_commute {A} (m : M A) i j f g :
+Lemma partial_alter_commute {A} f g (m : M A) i j :
i ≠j → partial_alter f i (partial_alter g j m) =
partial_alter g j (partial_alter f i m).
Proof.
@@ -164,10 +171,10 @@ Qed.
Lemma partial_alter_self {A} (m : M A) i : partial_alter (λ _, m !! i) i m = m.
Proof. by apply partial_alter_self_alt. Qed.
-Lemma partial_alter_subseteq {A} (m : M A) i f :
+Lemma partial_alter_subseteq {A} f (m : M A) i :
m !! i = None → m ⊆ partial_alter f i m.
Proof. intros Hi j x Hj. rewrite lookup_partial_alter_ne; congruence. Qed.
-Lemma partial_alter_subset {A} (m : M A) i f :
+Lemma partial_alter_subset {A} f (m : M A) i :
m !! i = None → is_Some (f (m !! i)) → m ⊂ partial_alter f i m.
Proof.
intros Hi Hfi. split.
@@ -178,11 +185,26 @@ Proof.
Qed.
(** ** Properties of the [alter] operation *)
+Lemma alter_ext {A} (f g : A → A) (m : M A) i :
+ (∀ x, m !! i = Some x → f x = g x) → alter f i m = alter g i m.
+Proof. intro. apply partial_alter_ext. intros [x|] ?; simpl; f_equal; auto. Qed.
+
Lemma lookup_alter {A} (f : A → A) m i : alter f i m !! i = f <$> m !! i.
Proof. apply lookup_partial_alter. Qed.
Lemma lookup_alter_ne {A} (f : A → A) m i j : i ≠j → alter f i m !! j = m !! j.
Proof. apply lookup_partial_alter_ne. Qed.
+Lemma alter_compose {A} (f g : A → A) (m : M A) i:
+ alter (f ∘ g) i m = alter f i (alter g i m).
+Proof.
+ unfold alter, map_alter. rewrite <-partial_alter_compose.
+ apply partial_alter_ext. by intros [?|].
+Qed.
+
+Lemma alter_commute {A} (f g : A → A) (m : M A) i j :
+ i ≠j → alter f i (alter g j m) = alter g j (alter f i m).
+Proof. apply partial_alter_commute. Qed.
+
Lemma lookup_alter_Some {A} (f : A → A) m i j y :
alter f i m !! j = Some y ↔
(i = j ∧ ∃ x, m !! j = Some x ∧ y = f x) ∨ (i ≠j ∧ m !! j = Some y).
@@ -456,7 +478,7 @@ Lemma map_of_list_inj {A} (l1 l2 : list (K * A)) :
NoDup (fst <$> l1) → NoDup (fst <$> l2) →
map_of_list l1 = map_of_list l2 → l1 ≡ₚ l2.
Proof.
- intros ?? Hl1l2. apply NoDup_Permutation; auto using (NoDup_fmap_1 fst).
+ intros ?? Hl1l2. apply NoDup_Permutation; auto using (fmap_nodup_1 fst).
intros [i x]. by rewrite !elem_of_map_of_list, Hl1l2.
Qed.
Lemma map_of_to_list {A} (m : M A) : map_of_list (map_to_list m) = m.
diff --git a/theories/list.v b/theories/list.v
index f1a045cf1e14bb86e8698e7f002d9769d03e935b..b4f402e433ff290561b2aa515324316bb68d6d5e 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -53,6 +53,10 @@ Instance list_alter {A} (f : A → A) : AlterD nat A (list A) f :=
| x :: l => match i with 0 => f x :: l | S i => x :: @alter _ _ _ f go i l end
end.
+(** The operation [<[i:=x]> l] overwrites the element at position [i] with the
+value [x]. In case [i] is out of bounds, the list is returned unchanged. *)
+Instance list_insert {A} : Insert nat A (list A) := λ i x, alter (λ _, x) i.
+
(** The operation [delete i l] removes the [i]th element of [l] and moves
all consecutive elements one position ahead. In case [i] is out of bounds,
the list is returned unchanged. *)
@@ -63,10 +67,6 @@ Instance list_delete {A} : Delete nat (list A) :=
| x :: l => match i with 0 => l | S i => x :: @delete _ _ go i l end
end.
-(** The operation [<[i:=x]> l] overwrites the element at position [i] with the
-value [x]. In case [i] is out of bounds, the list is returned unchanged. *)
-Instance list_insert {A} : Insert nat A (list A) := λ i x, alter (λ _, x) i.
-
(** The function [option_list o] converts an element [Some x] into the
singleton list [[x]], and [None] into the empty list [[]]. *)
Definition option_list {A} : option A → list A := option_rect _ (λ x, [x]) [].
@@ -82,6 +82,21 @@ Instance list_filter {A} : Filter A (list A) :=
then x :: @filter _ _ (@go) _ _ l
else @filter _ _ (@go) _ _ l
end.
+Fixpoint filter_Some {A} (l : list (option A)) : list A :=
+ match l with
+ | [] => []
+ | Some x :: l => x :: filter_Some l
+ | None :: l => filter_Some l
+ end.
+
+(** The function [list_find P l] returns the first index [i] whose element
+satisfies the predicate [P]. *)
+Definition list_find {A} P `{∀ x, Decision (P x)} : list A → option nat :=
+ fix go l :=
+ match l with
+ | [] => None
+ | x :: l => if decide (P x) then Some 0 else S <$> go l
+ end.
(** The function [replicate n x] generates a list with length [n] of elements
with value [x]. *)
@@ -106,6 +121,11 @@ Fixpoint resize {A} (n : nat) (y : A) (l : list A) : list A :=
end.
Arguments resize {_} !_ _ !_.
+Definition sublist_lookup {A} (i n : nat) (l : list A) : option (list A) :=
+ guard (i + n ≤ length l); Some $ take n $ drop i l.
+Definition sublist_insert {A} (i : nat) (k l : list A) : list A :=
+ take i l ++ take (length l - i) k ++ drop (i + length k) l.
+
(** Functions to fold over a list. We redefine [foldl] with the arguments in
the same order as in Haskell. *)
Notation foldr := fold_right.
@@ -128,6 +148,13 @@ Instance list_bind {A B} (f : A → list B) : MBindD list f :=
Instance list_join: MJoin list :=
fix go A (ls : list (list A)) : list A :=
match ls with [] => [] | l :: ls => l ++ @mjoin _ go _ ls end.
+Definition mapM `{!MBind M} `{!MRet M} {A B}
+ (f : A → M B) : list A → M (list B) :=
+ fix go l :=
+ match l with
+ | [] => mret []
+ | x :: l => y ↠f x; k ↠go l; mret (y :: k)
+ end.
(** We define stronger variants of map and fold that allow the mapped
function to use the index of the elements. *)
@@ -199,12 +226,12 @@ Section prefix_suffix_ops.
Definition strip_suffix (l1 l2 : list A) := snd $ fst $ max_suffix_of l1 l2.
End prefix_suffix_ops.
-(** A list [l1] is a sub list of [l2] if [l2] is obtained by removing elements
+(** A list [l1] is a sublist of [l2] if [l2] is obtained by removing elements
from [l1] without changing the order. *)
Inductive sublist {A} : relation (list A) :=
| sublist_nil : sublist [] []
| sublist_skip x l1 l2 : sublist l1 l2 → sublist (x :: l1) (x :: l2)
- | sublist_insert x l1 l2 : sublist l1 l2 → sublist l1 (x :: l2).
+ | sublist_cons x l1 l2 : sublist l1 l2 → sublist l1 (x :: l2).
Infix "`sublist`" := sublist (at level 70) : C_scope.
(** A list [l2] contains a list [l1] if [l2] is obtained by removing elements
@@ -213,7 +240,7 @@ Inductive contains {A} : relation (list A) :=
| contains_nil : contains [] []
| contains_skip x l1 l2 : contains l1 l2 → contains (x :: l1) (x :: l2)
| contains_swap x y l : contains (y :: x :: l) (x :: y :: l)
- | contains_insert x l1 l2 : contains l1 l2 → contains l1 (x :: l2)
+ | contains_cons x l1 l2 : contains l1 l2 → contains l1 (x :: l2)
| contains_trans l1 l2 l3 : contains l1 l2 → contains l2 l3 → contains l1 l3.
Infix "`contains`" := contains (at level 70) : C_scope.
@@ -312,6 +339,8 @@ Ltac simplify_list_equality :=
destruct i; [change (Some x = Some y) in H | discriminate]
end;
try discriminate_list_equality.
+Ltac simplify_list_equality' :=
+ repeat (progress simpl in * || simplify_list_equality).
(** * General theorems *)
Section general_properties.
@@ -321,10 +350,6 @@ Implicit Types l k : list A.
Global Instance: Injective2 (=) (=) (=) (@cons A).
Proof. by injection 1. Qed.
-Global Instance: ∀ x, Injective (=) (=) (x ::).
-Proof. by injection 1. Qed.
-Global Instance: ∀ l, Injective (=) (=) (:: l).
-Proof. by injection 1. Qed.
Global Instance: ∀ k, Injective (=) (=) (k ++).
Proof. intros ???. apply app_inv_head. Qed.
Global Instance: ∀ k, Injective (=) (=) (++ k).
@@ -375,15 +400,13 @@ Proof. by destruct l. Qed.
Lemma lookup_lt_Some l i x : l !! i = Some x → i < length l.
Proof.
- revert i. induction l; intros [|?] ?;
- simpl in *; simplify_equality; simpl; auto with arith.
+ revert i. induction l; intros [|?] ?; simplify_equality'; auto with arith.
Qed.
Lemma lookup_lt_is_Some_1 l i : is_Some (l !! i) → i < length l.
Proof. intros [??]; eauto using lookup_lt_Some. Qed.
Lemma lookup_lt_is_Some_2 l i : i < length l → is_Some (l !! i).
Proof.
- revert i. induction l; intros [|?] ?;
- simpl in *; simplify_equality; simpl; eauto with lia.
+ revert i. induction l; intros [|?] ?; simplify_equality'; eauto with lia.
Qed.
Lemma lookup_lt_is_Some l i : is_Some (l !! i) ↔ i < length l.
Proof. split; auto using lookup_lt_is_Some_1, lookup_lt_is_Some_2. Qed.
@@ -410,27 +433,22 @@ Lemma lookup_app_l l1 l2 i : i < length l1 → (l1 ++ l2) !! i = l1 !! i.
Proof. revert i. induction l1; intros [|?]; simpl; auto with lia. Qed.
Lemma lookup_app_l_Some l1 l2 i x : l1 !! i = Some x → (l1 ++ l2) !! i = Some x.
Proof. intros. rewrite lookup_app_l; eauto using lookup_lt_Some. Qed.
+
Lemma lookup_app_r l1 l2 i : (l1 ++ l2) !! (length l1 + i) = l2 !! i.
-Proof.
- revert i. induction l1; intros [|i]; simpl in *; simplify_equality; auto.
-Qed.
-Lemma lookup_app_r_alt l1 l2 i :
- length l1 ≤ i → (l1 ++ l2) !! i = l2 !! (i - length l1).
-Proof.
- intros. assert (i = length l1 + (i - length l1)) as Hi by lia.
- rewrite Hi at 1. by apply lookup_app_r.
-Qed.
+Proof. revert i. induction l1; intros [|i]; simplify_equality'; auto. Qed.
+Lemma lookup_app_r_alt l1 l2 i j :
+ j = length l1 → (l1 ++ l2) !! (j + i) = l2 !! i.
+Proof. intros ->. by apply lookup_app_r. Qed.
Lemma lookup_app_r_Some l1 l2 i x :
l2 !! i = Some x → (l1 ++ l2) !! (length l1 + i) = Some x.
Proof. by rewrite lookup_app_r. Qed.
-Lemma lookup_app_r_Some_alt l1 l2 i x :
- length l1 ≤ i → l2 !! (i - length l1) = Some x → (l1 ++ l2) !! i = Some x.
-Proof. intro. by rewrite lookup_app_r_alt. Qed.
+Lemma lookup_app_minus_r l1 l2 i :
+ length l1 ≤ i → (l1 ++ l2) !! i = l2 !! (i - length l1).
+Proof. intros. rewrite <-(lookup_app_r l1 l2). f_equal. lia. Qed.
+
Lemma lookup_app_inv l1 l2 i x :
(l1 ++ l2) !! i = Some x → l1 !! i = Some x ∨ l2 !! (i - length l1) = Some x.
-Proof.
- revert i. induction l1; intros [|i] ?; simpl in *; simplify_equality; auto.
-Qed.
+Proof. revert i. induction l1; intros [|i] ?; simplify_equality'; auto. Qed.
Lemma list_lookup_middle l1 l2 x : (l1 ++ x :: l2) !! length l1 = Some x.
Proof. by induction l1; simpl. Qed.
@@ -457,7 +475,7 @@ Proof. apply list_lookup_alter_ne. Qed.
Lemma list_lookup_other l i x :
length l ≠1 → l !! i = Some x → ∃ j y, j ≠i ∧ l !! j = Some y.
Proof.
- intros. destruct i, l as [|x0 [|x1 l]]; simpl in *; simplify_equality.
+ intros. destruct i, l as [|x0 [|x1 l]]; simplify_equality'.
* by exists 1 x1.
* by exists 0 x0.
Qed.
@@ -476,6 +494,18 @@ Proof.
intros. assert (i = length l1 + (i - length l1)) as Hi by lia.
rewrite Hi at 1. by apply alter_app_r.
Qed.
+Lemma list_alter_ext f g l i :
+ (∀ x, l !! i = Some x → f x = g x) → alter f i l = alter g i l.
+Proof. revert i. induction l; intros [|?] ?; simpl; f_equal; auto. Qed.
+Lemma list_alter_compose f g l i :
+ alter (f ∘ g) i l = alter f i (alter g i l).
+Proof. revert i. induction l; intros [|?]; simpl; f_equal; auto. Qed.
+Lemma list_alter_commute f g l i j :
+ i ≠j → alter f i (alter g j l) = alter g j (alter f i l).
+Proof.
+ revert i j.
+ induction l; intros [|?] [|?]; simpl; auto with f_equal congruence.
+Qed.
Lemma insert_app_l l1 l2 i x :
i < length l1 → <[i:=x]>(l1 ++ l2) = <[i:=x]>l1 ++ l2.
@@ -486,10 +516,6 @@ Lemma insert_app_r_alt l1 l2 i x :
length l1 ≤ i → <[i:=x]>(l1 ++ l2) = l1 ++ <[i - length l1:=x]>l2.
Proof. apply alter_app_r_alt. Qed.
-Lemma insert_consecutive_length l i k :
- length (insert_consecutive i k l) = length l.
-Proof. revert i. by induction k; intros; simpl; rewrite ?insert_length. Qed.
-
Lemma delete_middle l1 l2 x : delete (length l1) (l1 ++ x :: l2) = l1 ++ l2.
Proof. induction l1; simpl; f_equal; auto. Qed.
@@ -536,8 +562,7 @@ Proof.
Qed.
Lemma elem_of_list_lookup_2 l i x : l !! i = Some x → x ∈ l.
Proof.
- revert i. induction l; intros [|i] ?;
- simpl; simplify_equality; constructor; eauto.
+ revert i. induction l; intros [|i] ?; simplify_equality'; constructor; eauto.
Qed.
Lemma elem_of_list_lookup l x : x ∈ l ↔ ∃ i, l !! i = Some x.
Proof. firstorder eauto using elem_of_list_lookup_1, elem_of_list_lookup_2. Qed.
@@ -618,7 +643,6 @@ Proof.
* rewrite !NoDup_cons.
setoid_rewrite elem_of_cons. setoid_rewrite elem_of_app. naive_solver.
Qed.
-
Global Instance NoDup_proper: Proper ((≡ₚ) ==> iff) (@NoDup A).
Proof.
induction 1 as [|x l k Hlk IH | |].
@@ -627,18 +651,20 @@ Proof.
* rewrite !NoDup_cons, !elem_of_cons. intuition.
* intuition.
Qed.
-
-Lemma NoDup_Permutation l k : NoDup l → NoDup k → (∀ x, x ∈ l ↔ x ∈ k) → l ≡ₚ k.
+Lemma NoDup_lookup l i j x : NoDup l → l !! i = Some x → l !! j = Some x → i = j.
+Proof.
+ intros Hl. revert i j. induction Hl as [|x' l Hx Hl IH].
+ { intros; simplify_equality. }
+ intros [|i] [|j] ??; simplify_equality'; eauto with f_equal;
+ exfalso; eauto using elem_of_list_lookup_2.
+Qed.
+Lemma NoDup_alt l : NoDup l ↔ ∀ i j x, l !! i = Some x → l !! j = Some x → i = j.
Proof.
- intros Hl. revert k. induction Hl as [|x l Hin ? IH].
- * intros k _ Hk. rewrite (elem_of_nil_inv k); [done |].
- intros x. rewrite <-Hk, elem_of_nil. intros [].
- * intros k Hk Hlk. destruct (elem_of_list_split k x) as [l1 [l2 ?]]; subst.
- { rewrite <-Hlk. by constructor. }
- rewrite <-Permutation_middle, NoDup_cons in Hk.
- destruct Hk as [??]. apply Permutation_cons_app, IH; [done |].
- intros y. specialize (Hlk y).
- rewrite <-Permutation_middle, !elem_of_cons in Hlk. naive_solver.
+ split; eauto using NoDup_lookup.
+ induction l as [|x l IH]; intros Hl; constructor.
+ * rewrite elem_of_list_lookup. intros [i ?].
+ by feed pose proof (Hl (S i) 0 x); auto.
+ * apply IH. intros i j x' ??. by apply (injective S), (Hl (S i) (S j) x').
Qed.
Section no_dup_dec.
@@ -687,6 +713,33 @@ Section filter.
Qed.
End filter.
+(** ** Properties of the [find] function *)
+Section find.
+ Context (P : A → Prop) `{∀ x, Decision (P x)}.
+
+ Lemma list_find_Some l i : list_find P l = Some i → ∃ x, l !! i = Some x ∧ P x.
+ Proof.
+ revert i. induction l; simpl; repeat case_decide;
+ eauto with simplify_option_equality.
+ Qed.
+ Lemma list_find_elem_of l x : x ∈ l → P x → ∃ i, list_find P l = Some i.
+ Proof.
+ induction 1; simpl; repeat case_decide;
+ naive_solver (by eauto with simplify_option_equality).
+ Qed.
+End find.
+
+Section find_eq.
+ Context `{∀ x y, Decision (x = y)}.
+
+ Lemma list_find_eq_Some l i x : list_find (x =) l = Some i → l !! i = Some x.
+ Proof.
+ intros. destruct (list_find_Some (x =) l i) as (?&?&?); auto with congruence.
+ Qed.
+ Lemma list_find_eq_elem_of l x : x ∈ l → ∃ i, list_find (x=) l = Some i.
+ Proof. eauto using list_find_elem_of. Qed.
+End find_eq.
+
(** ** Properties of the [reverse] function *)
Lemma reverse_nil : reverse [] = @nil A.
Proof. done. Qed.
@@ -702,6 +755,21 @@ Lemma reverse_length l : length (reverse l) = length l.
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_length. Qed.
Lemma reverse_involutive l : reverse (reverse l) = l.
Proof. unfold reverse. rewrite <-!rev_alt. apply rev_involutive. Qed.
+Lemma elem_of_reverse_2 x l : x ∈ l → x ∈ reverse l.
+Proof.
+ induction 1; rewrite reverse_cons, elem_of_app,
+ ?elem_of_list_singleton; intuition.
+Qed.
+Lemma elem_of_reverse x l : x ∈ reverse l ↔ x ∈ l.
+Proof.
+ split; auto using elem_of_reverse_2.
+ intros. rewrite <-(reverse_involutive l). by apply elem_of_reverse_2.
+Qed.
+Global Instance: Injective (=) (=) (@reverse A).
+Proof.
+ intros l1 l2 Hl.
+ by rewrite <-(reverse_involutive l1), <-(reverse_involutive l2), Hl.
+Qed.
(** ** Properties of the [take] function *)
Definition take_drop := @firstn_skipn A.
@@ -733,8 +801,10 @@ Proof. by rewrite take_take, Min.min_idempotent. Qed.
Lemma take_length l n : length (take n l) = min n (length l).
Proof. revert n. induction l; intros [|?]; simpl; f_equal; done. Qed.
-Lemma take_length_alt l n : n ≤ length l → length (take n l) = n.
+Lemma take_length_le l n : n ≤ length l → length (take n l) = n.
Proof. rewrite take_length. apply Min.min_l. Qed.
+Lemma take_length_ge l n : length l ≤ n → length (take n l) = length l.
+Proof. rewrite take_length. apply Min.min_r. Qed.
Lemma lookup_take l n i : i < n → take n l !! i = l !! i.
Proof.
@@ -762,10 +832,10 @@ Lemma drop_app_alt l k n : n = length l → drop n (l ++ k) = k.
Proof. intros Hn. by rewrite Hn, drop_app. Qed.
Lemma drop_length l n : length (drop n l) = length l - n.
Proof. revert n. by induction l; intros [|i]; simpl; f_equal. Qed.
+Lemma drop_ge l n : length l ≤ n → drop n l = [].
+Proof. revert n. induction l; intros [|??]; simpl in *; auto with lia. Qed.
Lemma drop_all l : drop (length l) l = [].
-Proof. induction l; simpl; auto. Qed.
-Lemma drop_all_alt l n : n = length l → drop n l = [].
-Proof. intros. subst. by rewrite drop_all. Qed.
+Proof. by apply drop_ge. Qed.
Lemma lookup_drop l n i : drop n l !! i = l !! (n + i).
Proof. revert n i. induction l; intros [|i] ?; simpl; auto. Qed.
@@ -788,6 +858,16 @@ Proof. revert i. induction n; intros [|?]; naive_solver auto with lia. Qed.
Lemma lookup_replicate_inv n x y i :
replicate n x !! i = Some y → y = x ∧ i < n.
Proof. revert i. induction n; intros [|?]; naive_solver auto with lia. Qed.
+Lemma lookup_replicate_None n x i : n ≤ i ↔ replicate n x !! i = None.
+Proof.
+ rewrite eq_None_not_Some, Nat.le_ngt. split.
+ * intros Hin [x' Hx']; destruct Hin.
+ by destruct (lookup_replicate_inv n x x' i).
+ * intros Hx ?. destruct Hx. exists x; auto using lookup_replicate.
+Qed.
+
+Lemma elem_of_replicate_inv x n y : x ∈ replicate n y → x = y.
+Proof. induction n; simpl; rewrite ?elem_of_nil, ?elem_of_cons; intuition. Qed.
Lemma replicate_S n x : replicate (S n) x = x :: replicate n x.
Proof. done. Qed.
Lemma replicate_plus n m x :
@@ -803,10 +883,19 @@ Proof. revert m. by induction n; intros [|?]; simpl; f_equal. Qed.
Lemma drop_replicate_plus n m x : drop n (replicate (n + m) x) = replicate m x.
Proof. rewrite drop_replicate. f_equal. lia. Qed.
+Lemma replicate_as_elem_of x n l :
+ l = replicate n x ↔ length l = n ∧ ∀ y, y ∈ l → y = x.
+Proof.
+ split.
+ * intros; subst. eauto using elem_of_replicate_inv, replicate_length.
+ * intros [? Hl]; subst. induction l as [|y l IH]; simpl; f_equal.
+ + apply Hl. by left.
+ + apply IH. intros ??. apply Hl. by right.
+Qed.
Lemma reverse_replicate n x : reverse (replicate n x) = replicate n x.
Proof.
- induction n as [|n IH]; [done|]. simpl. rewrite reverse_cons, IH.
- change [x] with (replicate 1 x). by rewrite <-replicate_plus, plus_comm.
+ apply replicate_as_elem_of. rewrite reverse_length, replicate_length. split; auto.
+ intros y. rewrite elem_of_reverse. by apply elem_of_replicate_inv.
Qed.
(** ** Properties of the [resize] function *)
@@ -821,7 +910,7 @@ Lemma resize_ge l n x :
Proof. intros. by rewrite resize_spec, take_ge. Qed.
Lemma resize_le l n x : n ≤ length l → resize n x l = take n l.
Proof.
- intros. rewrite resize_spec, (proj2 (NPeano.Nat.sub_0_le _ _)) by done.
+ intros. rewrite resize_spec, (proj2 (Nat.sub_0_le _ _)) by done.
simpl. by rewrite (right_id_L [] (++)).
Qed.
@@ -834,7 +923,7 @@ Lemma resize_plus l n m x :
resize (n + m) x l = resize n x l ++ resize m x (drop n l).
Proof.
revert n m. induction l; intros [|?] [|?]; simpl; f_equal; auto.
- * by rewrite plus_0_r, (right_id_L [] (++)).
+ * by rewrite Nat.add_0_r, (right_id_L [] (++)).
* by rewrite replicate_plus.
Qed.
Lemma resize_plus_eq l n m x :
@@ -860,6 +949,22 @@ Proof. rewrite resize_spec, app_length, replicate_length, take_length. lia. Qed.
Lemma resize_replicate x n m : resize n x (replicate m x) = replicate n x.
Proof. revert m. induction n; intros [|?]; simpl; f_equal; auto. Qed.
+Lemma lookup_resize l n x i : i < n → i < length l → resize n x l !! i = l !! i.
+Proof.
+ intros ??. destruct (decide (n < length l)).
+ * by rewrite resize_le, lookup_take by lia.
+ * by rewrite resize_ge, lookup_app_l by lia.
+Qed.
+Lemma lookup_resize_new l n x i :
+ length l ≤ i → i < n → resize n x l !! i = Some x.
+Proof.
+ intros ??. rewrite resize_ge by lia.
+ replace i with (length l + (i - length l)) by lia.
+ by rewrite lookup_app_r, lookup_replicate by lia.
+Qed.
+Lemma lookup_resize_old l n x i : n ≤ i → resize n x l !! i = None.
+Proof. intros ?. apply lookup_ge_None_2. by rewrite resize_length. Qed.
+
Lemma resize_resize l n m x : n ≤ m → resize n x (resize m x l) = resize n x l.
Proof.
revert n m. induction l; simpl.
@@ -905,6 +1010,80 @@ Lemma drop_resize_plus l n m x :
drop n (resize (n + m) x l) = resize m x (drop n l).
Proof. rewrite drop_resize_le by lia. f_equal. lia. Qed.
+Lemma sublist_lookup_Some l i n k :
+ sublist_lookup i n l = Some k ↔
+ i + n ≤ length l ∧ length k = n ∧ ∀ j, j < n → l !! (i + j) = k !! j.
+Proof.
+ unfold sublist_lookup in *. split.
+ * intros Hk. simplify_option_equality. split_ands.
+ + done.
+ + by rewrite take_length_le by (rewrite drop_length; lia).
+ + intros j ?. by rewrite lookup_take, lookup_drop by done.
+ * intros (?&?&Hlookup). case_option_guard; [|lia].
+ f_equal; apply list_eq; intros j. destruct (decide (j < n)).
+ + by rewrite <-Hlookup, lookup_take, lookup_drop by done.
+ + by rewrite lookup_take_ge, lookup_ge_None_2 by lia.
+Qed.
+Lemma sublist_lookup_length l i n k :
+ sublist_lookup i n l = Some k → length k = n.
+Proof. rewrite sublist_lookup_Some. intuition. Qed.
+
+Lemma sublist_insert_length l i k :
+ length (sublist_insert i k l) = length l.
+Proof.
+ unfold sublist_insert. intros. rewrite !app_length, drop_length.
+ destruct (decide (i + length k ≤ length l)).
+ * rewrite !take_length_le, !take_length_ge by lia. lia.
+ * destruct (decide (i < length l));
+ rewrite ?take_length_ge, ?take_length_le by lia; lia.
+Qed.
+Lemma sublist_insert_ge l i k : length l ≤ i → sublist_insert i k l = l.
+Proof.
+ unfold sublist_insert. intros ?. rewrite drop_ge by lia.
+ rewrite take_ge, (proj2 (Nat.sub_0_le _ _)) by done; simpl.
+ by rewrite (right_id [] (++)).
+Qed.
+Lemma lookup_sublist_insert l i k j :
+ i + length k ≤ length l →
+ i ≤ j < i + length k → sublist_insert i k l !! j = k !! (j - i).
+Proof.
+ unfold sublist_insert. intros ? [??]. rewrite (take_ge _ (_ - _ )) by lia.
+ rewrite lookup_app_minus_r by (rewrite take_length_le; lia).
+ by rewrite !take_length_le, lookup_app_l by lia.
+Qed.
+Lemma lookup_sublist_insert_ne l i k j :
+ j < i ∨ i + length k ≤ j → sublist_insert i k l !! j = l !! j.
+Proof.
+ destruct (decide (length l ≤ j)).
+ { by rewrite !lookup_ge_None_2 by (by rewrite ?sublist_insert_length). }
+ unfold sublist_insert. intros [?|?].
+ { rewrite lookup_app_l by (rewrite take_length; apply Nat.min_glb_lt; lia).
+ by rewrite lookup_take. }
+ rewrite lookup_app_minus_r by (rewrite take_length_le; lia).
+ rewrite take_length_le by lia.
+ rewrite lookup_app_minus_r by (rewrite take_length_ge; lia).
+ rewrite lookup_drop, take_length_ge by lia. f_equal. lia.
+Qed.
+
+(** ** Properties of the [seq] function *)
+Lemma fmap_seq j n : S <$> seq j n = seq (S j) n.
+Proof. revert j. induction n; simpl; auto with f_equal. Qed.
+Lemma lookup_seq j n i : i < n → seq j n !! i = Some (j + i).
+Proof.
+ revert j i. induction n as [|n IH]; intros j [|i] ?; simpl; auto with lia.
+ rewrite IH; auto with lia.
+Qed.
+Lemma lookup_seq_ge j n i : n ≤ i → seq j n !! i = None.
+Proof.
+ revert j i. induction n as [|n IH]; intros j [|i] ?; simpl; auto with lia.
+Qed.
+Lemma lookup_seq_inv j n i j' : seq j n !! i = Some j' → j' = j + i ∧ i < n.
+Proof.
+ destruct (le_lt_dec n i).
+ * by rewrite lookup_seq_ge.
+ * rewrite lookup_seq by done. intuition congruence.
+Qed.
+
(** ** Properties of the [Permutation] predicate *)
Lemma Permutation_nil l : l ≡ₚ [] ↔ l = [].
Proof. split. by intro; apply Permutation_nil. by intro; subst. Qed.
@@ -934,6 +1113,17 @@ Global Instance: ∀ k : list A, Injective (≡ₚ) (≡ₚ) (++ k).
Proof.
intros k l1 l2. rewrite !(commutative (++) _ k). by apply (injective (k ++)).
Qed.
+Lemma replicate_Permutation n x l : l ≡ₚ replicate n x → l = replicate n x.
+Proof.
+ intros Hl. apply replicate_as_elem_of. split.
+ * by rewrite Hl, replicate_length.
+ * intros y. rewrite Hl. by apply elem_of_replicate_inv.
+Qed.
+Lemma reverse_Permutation l : reverse l ≡ₚ l.
+Proof.
+ induction l as [|x l IH]; [done|].
+ by rewrite reverse_cons, (commutative (++)), IH.
+Qed.
(** ** Properties of the [prefix_of] and [suffix_of] predicates *)
Global Instance: PreOrder (@prefix_of A).
@@ -1267,7 +1457,7 @@ Proof.
{ eexists [], l. by repeat constructor. }
rewrite sublist_cons_r. intros [?|(l' & ? &?)]; subst.
+ destruct (IH l k2) as (l1&l2&?&?&?); trivial; subst.
- exists l1 l2. auto using sublist_insert.
+ exists l1 l2. auto using sublist_cons.
+ destruct (IH l' k2) as (l1&l2&?&?&?); trivial; subst.
exists (y :: l1) l2. auto using sublist_skip.
* intros (?&?&?&?&?); subst. auto using sublist_app.
@@ -1290,7 +1480,7 @@ Proof.
induction k as [|y k IH]; simpl; [done |].
rewrite sublist_cons_r. intros [Hl12|(?&?&?)]; [|simplify_equality; eauto].
rewrite sublist_cons_l in Hl12. destruct Hl12 as (k1&k2&Hk&?).
- apply IH. rewrite Hk. eauto using sublist_inserts_l, sublist_insert.
+ apply IH. rewrite Hk. eauto using sublist_inserts_l, sublist_cons.
Qed.
Lemma sublist_app_inv_r k l1 l2 : l1 ++ k `sublist` l2 ++ k → l1 `sublist` l2.
Proof.
@@ -1313,7 +1503,7 @@ Proof.
+ intros ?. rewrite sublist_cons_l. intros (?&?&?&?); subst.
eauto using sublist_inserts_l, sublist_skip.
+ intros ?. rewrite sublist_cons_l. intros (?&?&?&?); subst.
- eauto using sublist_inserts_l, sublist_insert.
+ eauto using sublist_inserts_l, sublist_cons.
* intros l1 l2 Hl12 Hl21. apply sublist_length in Hl21.
induction Hl12; simpl in *; f_equal; auto with arith.
apply sublist_length in Hl12. lia.
@@ -1557,6 +1747,22 @@ Proof.
split. by intros Hl; rewrite Hl. intros [??]; auto using contains_Permutation.
Qed.
+Lemma NoDup_contains l k : NoDup l → (∀ x, x ∈ l → x ∈ k) → l `contains` k.
+Proof.
+ intros Hl. revert k. induction Hl as [|x l Hx ? IH].
+ { intros k Hk. by apply contains_nil_l. }
+ intros k Hlk. destruct (elem_of_list_split k x) as (l1&l2&?); subst.
+ { apply Hlk. by constructor. }
+ rewrite <-Permutation_middle. apply contains_skip, IH.
+ intros y Hy. rewrite elem_of_app.
+ specialize (Hlk y). rewrite elem_of_app, !elem_of_cons in Hlk.
+ by destruct Hlk as [?|[?|?]]; subst; eauto.
+Qed.
+Lemma NoDup_Permutation l k : NoDup l → NoDup k → (∀ x, x ∈ l ↔ x ∈ k) → l ≡ₚ k.
+Proof.
+ intros. apply (anti_symmetric contains); apply NoDup_contains; naive_solver.
+Qed.
+
Section contains_dec.
Context `{∀ x y, Decision (x = y)}.
@@ -1682,11 +1888,13 @@ Section Forall_Exists.
Proof. split. by inversion 1. intros [??]. by constructor. Qed.
Lemma Forall_singleton x : Forall P [x] ↔ P x.
Proof. rewrite Forall_cons, Forall_nil; tauto. Qed.
+ Lemma Forall_app_2 l1 l2 : Forall P l1 → Forall P l2 → Forall P (l1 ++ l2).
+ Proof. induction 1; simpl; auto. Qed.
Lemma Forall_app l1 l2 : Forall P (l1 ++ l2) ↔ Forall P l1 ∧ Forall P l2.
Proof.
split.
* induction l1; inversion 1; intuition.
- * intros [H ?]. induction H; simpl; intuition.
+ * intros [??]; auto using Forall_app_2.
Qed.
Lemma Forall_true l : (∀ x, P x) → Forall P l.
Proof. induction l; auto. Qed.
@@ -1734,6 +1942,18 @@ Section Forall_Exists.
intros ? Hl. revert n.
induction Hl; intros [|?]; simpl; auto using Forall_replicate.
Qed.
+ Lemma Forall_sublist_lookup l i n k :
+ sublist_lookup i n l = Some k → Forall P l → Forall P k.
+ Proof.
+ unfold sublist_lookup. intros; simplify_option_equality.
+ auto using Forall_take, Forall_drop.
+ Qed.
+ Lemma Forall_sublist_insert l i k :
+ Forall P l → Forall P k → Forall P (sublist_insert i k l).
+ Proof.
+ unfold sublist_insert. auto using Forall_app_2, Forall_drop, Forall_take.
+ Qed.
+
Lemma Exists_exists l : Exists P l ↔ ∃ x, x ∈ l ∧ P x.
Proof.
split.
@@ -1801,9 +2021,22 @@ Section Forall_Exists.
end.
End Forall_Exists.
+Lemma replicate_as_Forall {A} (x : A) n l :
+ l = replicate n x ↔ length l = n ∧ Forall (x =) l.
+Proof. rewrite replicate_as_elem_of, Forall_forall. naive_solver. Qed.
+
Lemma Forall_swap {A B} (Q : A → B → Prop) l1 l2 :
Forall (λ y, Forall (Q y) l1) l2 ↔ Forall (λ x, Forall (flip Q x) l2) l1.
Proof. repeat setoid_rewrite Forall_forall. simpl. split; eauto. Qed.
+Lemma Forall_seq (P : nat → Prop) i n :
+ Forall P (seq i n) ↔ ∀ j, i ≤ j < i + n → P j.
+Proof.
+ rewrite Forall_lookup. split.
+ * intros H j [??]. apply (H (j - i)).
+ rewrite lookup_seq; auto with f_equal lia.
+ * intros H j x Hj. apply lookup_seq_inv in Hj.
+ destruct Hj; subst. auto with lia.
+Qed.
(** ** Properties of the [Forall2] predicate *)
Section Forall2.
@@ -1841,6 +2074,12 @@ Section Forall2.
Lemma Forall2_length l1 l2 : Forall2 P l1 l2 → length l1 = length l2.
Proof. induction 1; simpl; auto. Qed.
+ Lemma Forall2_length_l l1 l2 n :
+ Forall2 P l1 l2 → length l1 = n → length l2 = n.
+ Proof. intros ? <-; symmetry. by apply Forall2_length. Qed.
+ Lemma Forall2_length_r l1 l2 n :
+ Forall2 P l1 l2 → length l2 = n → length l1 = n.
+ Proof. intros ? <-. by apply Forall2_length. Qed.
Lemma Forall2_same_length l1 l2 : Forall2 P l1 l2 → l1 `same_length` l2.
Proof. induction 1; constructor; auto. Qed.
@@ -1867,19 +2106,19 @@ Section Forall2.
Forall2 P l1 l2 → l1 !! i = Some x → l2 !! i = Some y → P x y.
Proof.
intros H. revert i. induction H; [done|].
- intros [|?] ??; simpl in *; simplify_equality; eauto.
+ intros [|?] ??; simplify_equality'; eauto.
Qed.
Lemma Forall2_lookup_l l1 l2 i x :
Forall2 P l1 l2 → l1 !! i = Some x → ∃ y, l2 !! i = Some y ∧ P x y.
Proof.
intros H. revert i. induction H; [done|].
- intros [|?] ?; simpl in *; simplify_equality; eauto.
+ intros [|?] ?; simplify_equality'; eauto.
Qed.
Lemma Forall2_lookup_r l1 l2 i y :
Forall2 P l1 l2 → l2 !! i = Some y → ∃ x, l1 !! i = Some x ∧ P x y.
Proof.
intros H. revert i. induction H; [done|].
- intros [|?] ?; simpl in *; simplify_equality; eauto.
+ intros [|?] ?; simplify_equality'; eauto.
Qed.
Lemma Forall2_lookup_2 l1 l2 :
l1 `same_length` l2 →
@@ -1977,13 +2216,38 @@ Section Forall2.
eauto using Forall_resize, Forall_drop.
Qed.
+ Lemma Forall2_sublist_lookup_l l1 l2 n i k1 :
+ Forall2 P l1 l2 → sublist_lookup n i l1 = Some k1 →
+ ∃ k2, sublist_lookup n i l2 = Some k2 ∧ Forall2 P k1 k2.
+ Proof.
+ unfold sublist_lookup. intros Hl12 Hl1.
+ exists (take i (drop n l2)); simplify_option_equality.
+ * auto using Forall2_take, Forall2_drop.
+ * apply Forall2_length in Hl12; lia.
+ Qed.
+ Lemma Forall2_sublist_lookup_r l1 l2 n i k2 :
+ Forall2 P l1 l2 → sublist_lookup n i l2 = Some k2 →
+ ∃ k1, sublist_lookup n i l1 = Some k1 ∧ Forall2 P k1 k2.
+ Proof.
+ unfold sublist_lookup. intros Hl12 Hl2.
+ exists (take i (drop n l1)); simplify_option_equality.
+ * auto using Forall2_take, Forall2_drop.
+ * apply Forall2_length in Hl12; lia.
+ Qed.
+ Lemma Forall2_sublist_insert l1 l2 i k1 k2 :
+ Forall2 P l1 l2 → Forall2 P k1 k2 →
+ Forall2 P (sublist_insert i k1 l1) (sublist_insert i k2 l2).
+ Proof.
+ unfold sublist_insert. intros. erewrite !Forall2_length by eauto.
+ auto using Forall2_app, Forall2_take, Forall2_drop.
+ Qed.
+
Lemma Forall2_transitive {C} (Q : B → C → Prop) (R : A → C → Prop) l1 l2 l3 :
(∀ x1 x2 x3, P x1 x2 → Q x2 x3 → R x1 x3) →
Forall2 P l1 l2 → Forall2 Q l2 l3 → Forall2 R l1 l3.
Proof.
intros ? Hl1l2. revert l3. induction Hl1l2; inversion_clear 1; eauto.
Qed.
-
Lemma Forall2_Forall (Q : A → A → Prop) l :
Forall (λ x, Q x x) l → Forall2 Q l l.
Proof. induction 1; constructor; auto. Qed.
@@ -2042,9 +2306,9 @@ Section fmap.
Lemma list_fmap_compose {C} (g : B → C) l : g ∘ f <$> l = g <$> f <$> l.
Proof. induction l; simpl; f_equal; auto. Qed.
- Lemma list_fmap_ext (g : A → B) (l : list A) :
- (∀ x, f x = g x) → fmap f l = fmap g l.
- Proof. intro. induction l; simpl; f_equal; auto. Qed.
+ Lemma list_fmap_ext (g : A → B) (l1 l2 : list A) :
+ (∀ x, f x = g x) → l1 = l2 → fmap f l1 = fmap g l2.
+ Proof. intros ? <-. induction l1; simpl; f_equal; auto. Qed.
Global Instance: Injective (=) (=) f → Injective (=) (=) (fmap f).
Proof.
@@ -2059,13 +2323,13 @@ Section fmap.
Proof. by destruct k. Qed.
Lemma fmap_cons_inv y l k :
f <$> l = y :: k → ∃ x l', y = f x ∧ k = f <$> l' ∧ l = x :: l'.
- Proof. intros. destruct l; simpl; simplify_equality; eauto. Qed.
+ Proof. intros. destruct l; simplify_equality'; eauto. Qed.
Lemma fmap_app_inv l k1 k2 :
f <$> l = k1 ++ k2 → ∃ l1 l2, k1 = f <$> l1 ∧ k2 = f <$> l2 ∧ l = l1 ++ l2.
Proof.
revert l. induction k1 as [|y k1 IH]; simpl.
* intros l ?. by eexists [], l.
- * intros [|x l] ?; simpl; simplify_equality.
+ * intros [|x l] ?; simplify_equality'.
destruct (IH l) as [l1 [l2 [? [??]]]]; subst; [done |].
by exists (x :: l1) l2.
Qed.
@@ -2108,18 +2372,18 @@ Section fmap.
firstorder eauto using elem_of_list_fmap_1_alt, elem_of_list_fmap_2.
Qed.
- Lemma NoDup_fmap_1 l : NoDup (f <$> l) → NoDup l.
+ Lemma fmap_nodup_1 l : NoDup (f <$> l) → NoDup l.
Proof.
induction l; simpl; inversion_clear 1; constructor; auto.
rewrite elem_of_list_fmap in *. naive_solver.
Qed.
- Lemma NoDup_fmap_2 `{!Injective (=) (=) f} l : NoDup l → NoDup (f <$> l).
+ Lemma fmap_nodup_2 `{!Injective (=) (=) f} l : NoDup l → NoDup (f <$> l).
Proof.
induction 1; simpl; constructor; trivial. rewrite elem_of_list_fmap.
intros [y [Hxy ?]]. apply (injective f) in Hxy. by subst.
Qed.
- Lemma NoDup_fmap `{!Injective (=) (=) f} l : NoDup (f <$> l) ↔ NoDup l.
- Proof. split; auto using NoDup_fmap_1, NoDup_fmap_2. Qed.
+ Lemma fmap_nodup `{!Injective (=) (=) f} l : NoDup (f <$> l) ↔ NoDup l.
+ Proof. split; auto using fmap_nodup_1, fmap_nodup_2. Qed.
Global Instance fmap_sublist: Proper (sublist ==> sublist) (fmap f).
Proof. induction 1; simpl; econstructor; eauto. Qed.
@@ -2158,15 +2422,8 @@ Section fmap.
Forall2 P (f <$> l1) (g <$> l2) ↔ Forall2 (λ x1 x2, P (f x1) (g x2)) l1 l2.
Proof. split; auto using Forall2_fmap_1, Forall2_fmap_2. Qed.
- Lemma mapM_fmap_Some (g : B → option A) (l : list A) :
- (∀ x, g (f x) = Some x) → mapM g (f <$> l) = Some l.
- Proof. intros. by induction l; simpl; simplify_option_equality. Qed.
- Lemma mapM_fmap_Some_inv (g : B → option A) (l : list A) (k : list B) :
- (∀ x y, g y = Some x → y = f x) → mapM g k = Some l → k = f <$> l.
- Proof.
- intros Hgf. revert l; induction k as [|??]; intros [|??] ?;
- simplify_option_equality; f_equiv; eauto.
- Qed.
+ Lemma list_fmap_bind {C} (g : B → list C) l : (f <$> l) ≫= g = l ≫= g ∘ f.
+ Proof. induction l; simpl; f_equal; auto. Qed.
End fmap.
Lemma NoDup_fmap_fst {A B} (l : list (A * B)) :
@@ -2176,21 +2433,27 @@ Proof.
* rewrite elem_of_list_fmap.
intros [[x2 y2] [??]]; simpl in *; subst. destruct Hin.
rewrite (Hunique x2 y1 y2); rewrite ?elem_of_cons; auto.
- * apply IH. intros.
- eapply Hunique; rewrite ?elem_of_cons; eauto.
+ * apply IH. intros. eapply Hunique; rewrite ?elem_of_cons; eauto.
Qed.
Section bind.
Context {A B : Type} (f : A → list B).
- Global Instance mbind_sublist: Proper (sublist ==> sublist) (mbind f).
+ Lemma list_bind_ext (g : A → list B) l1 l2 :
+ (∀ x, f x = g x) → l1 = l2 → l1 ≫= f = l2 ≫= g.
+ Proof. intros ? <-. induction l1; simpl; f_equal; auto. Qed.
+ Lemma Forall_bind_ext (g : A → list B) (l : list A) :
+ Forall (λ x, f x = g x) l → l ≫= f = l ≫= g.
+ Proof. induction 1; simpl; f_equal; auto. Qed.
+
+ Global Instance bind_sublist: Proper (sublist ==> sublist) (mbind f).
Proof.
induction 1; simpl; auto.
* done.
* by apply sublist_app.
* by apply sublist_inserts_l.
Qed.
- Global Instance mbind_contains: Proper (contains ==> contains) (mbind f).
+ Global Instance bind_contains: Proper (contains ==> contains) (mbind f).
Proof.
induction 1; simpl; auto.
* done.
@@ -2199,7 +2462,7 @@ Section bind.
* by apply contains_inserts_l.
* etransitivity; eauto.
Qed.
- Global Instance mbind_Permutation: Proper ((≡ₚ) ==> (≡ₚ)) (mbind f).
+ Global Instance bind_Permutation: Proper ((≡ₚ) ==> (≡ₚ)) (mbind f).
Proof.
induction 1; simpl; auto.
* by f_equiv.
@@ -2268,13 +2531,12 @@ Section ret_join.
Proof.
intros Hn Hls. revert i. induction Hls as [|l ls ? Hls IH]; simpl; [done |].
intros i. destruct (decide (i < n)) as [Hin|Hin].
- * rewrite <-(NPeano.Nat.div_unique i n 0 i) by lia.
- rewrite <-(NPeano.Nat.mod_unique i n 0 i) by lia.
+ * rewrite <-(Nat.div_unique i n 0 i), <-(Nat.mod_unique i n 0 i) by lia.
simpl. rewrite lookup_app_l; auto with lia.
* replace i with ((i - n) + 1 * n) by lia.
- rewrite NPeano.Nat.div_add, NPeano.Nat.mod_add by done.
- replace (i - n + 1 * n) with i by lia.
- rewrite (plus_comm _ 1), lookup_app_r_alt, IH by lia. by subst.
+ rewrite Nat.div_add, Nat.mod_add by done.
+ replace (i - n + 1 * n) with (length l + (i - n)) by lia.
+ by rewrite (Nat.add_comm _ 1), lookup_app_r, IH.
Qed.
(* This should be provable using the previous lemma in a shorter way *)
@@ -2284,13 +2546,12 @@ Section ret_join.
Proof.
intros Hn Hls. revert i. induction Hls as [|l ls ? Hls IH]; simpl; [done |].
intros i. destruct (decide (i < n)) as [Hin|Hin].
- * rewrite <-(NPeano.Nat.div_unique i n 0 i) by lia.
- rewrite <-(NPeano.Nat.mod_unique i n 0 i) by lia.
+ * rewrite <-(Nat.div_unique i n 0 i), <-(Nat.mod_unique i n 0 i) by lia.
simpl. rewrite alter_app_l; auto with lia.
* replace i with ((i - n) + 1 * n) by lia.
- rewrite NPeano.Nat.div_add, NPeano.Nat.mod_add by done.
+ rewrite Nat.div_add, Nat.mod_add by done.
replace (i - n + 1 * n) with i by lia.
- rewrite (plus_comm _ 1), alter_app_r_alt, IH by lia. by subst.
+ rewrite (Nat.add_comm _ 1), alter_app_r_alt, IH by lia. by subst.
Qed.
Lemma insert_join_same_length (ls : list (list A)) n i x :
n ≠0 → Forall (λ l, length l = n) ls →
@@ -2302,6 +2563,72 @@ Section ret_join.
Proof. induction 1; simpl; auto using Forall2_app. Qed.
End ret_join.
+Section mapM.
+ Context {A B : Type} (f : A → option B).
+
+ Lemma mapM_ext (g : A → option B) l : (∀ x, f x = g x) → mapM f l = mapM g l.
+ Proof. intros Hfg. by induction l; simpl; rewrite ?Hfg, ?IHl. Qed.
+ Lemma Forall2_mapM_ext (g : A → option B) l k :
+ Forall2 (λ x y, f x = g y) l k → mapM f l = mapM g k.
+ Proof. induction 1 as [|???? Hfg ? IH]; simpl. done. by rewrite Hfg, IH. Qed.
+ Lemma Forall_mapM_ext (g : A → option B) l :
+ Forall (λ x, f x = g x) l → mapM f l = mapM g l.
+ Proof. induction 1 as [|?? Hfg ? IH]; simpl. done. by rewrite Hfg, IH. Qed.
+
+ Lemma mapM_Some_1 l k : mapM f l = Some k → Forall2 (λ x y, f x = Some y) l k.
+ Proof.
+ revert k. induction l as [|x l]; intros [|y k]; simpl; try done.
+ * destruct (f x); simpl; [|discriminate]. by destruct (mapM f l).
+ * destruct (f x) eqn:?; simpl; [|discriminate].
+ destruct (mapM f l); intros; simplify_equality. constructor; auto.
+ Qed.
+ Lemma mapM_Some_2 l k : Forall2 (λ x y, f x = Some y) l k → mapM f l = Some k.
+ Proof.
+ induction 1 as [|???? Hf ? IH]; simpl; [done |].
+ rewrite Hf. simpl. by rewrite IH.
+ Qed.
+ Lemma mapM_Some l k : mapM f l = Some k ↔ Forall2 (λ x y, f x = Some y) l k.
+ Proof. split; auto using mapM_Some_1, mapM_Some_2. Qed.
+ Lemma mapM_length l k : mapM f l = Some k → length l = length k.
+ Proof. intros. by eapply Forall2_length, mapM_Some_1. Qed.
+
+ Lemma mapM_None_1 l : mapM f l = None → Exists (λ x, f x = None) l.
+ Proof.
+ induction l as [|x l IH]; simpl; [done|].
+ destruct (f x) eqn:?; simpl; eauto. by destruct (mapM f l); eauto.
+ Qed.
+ Lemma mapM_None_2 l : Exists (λ x, f x = None) l → mapM f l = None.
+ Proof.
+ induction 1 as [x l Hx|x l ? IH]; simpl; [by rewrite Hx|].
+ by destruct (f x); simpl; rewrite ?IH.
+ Qed.
+ Lemma mapM_None l : mapM f l = None ↔ Exists (λ x, f x = None) l.
+ Proof. split; auto using mapM_None_1, mapM_None_2. Qed.
+
+ Lemma mapM_is_Some_1 l : is_Some (mapM f l) → Forall (is_Some ∘ f) l.
+ Proof.
+ unfold compose. setoid_rewrite <-not_eq_None_Some.
+ rewrite mapM_None. apply (not_Exists_Forall _).
+ Qed.
+ Lemma mapM_is_Some_2 l : Forall (is_Some ∘ f) l → is_Some (mapM f l).
+ Proof.
+ unfold compose. setoid_rewrite <-not_eq_None_Some.
+ rewrite mapM_None. apply (Forall_not_Exists _).
+ Qed.
+ Lemma mapM_is_Some l : is_Some (mapM f l) ↔ Forall (is_Some ∘ f) l.
+ Proof. split; auto using mapM_is_Some_1, mapM_is_Some_2. Qed.
+
+ Lemma mapM_fmap_Some (g : B → A) (l : list B) :
+ (∀ x, f (g x) = Some x) → mapM f (g <$> l) = Some l.
+ Proof. intros. by induction l; simpl; simplify_option_equality. Qed.
+ Lemma mapM_fmap_Some_inv (g : B → A) (l : list B) (k : list A) :
+ (∀ x y, f y = Some x → y = g x) → mapM f k = Some l → k = g <$> l.
+ Proof.
+ intros Hgf. revert l; induction k as [|??]; intros [|??] ?;
+ simplify_option_equality; f_equiv; eauto.
+ Qed.
+End mapM.
+
(** ** Properties of the [permutations] function *)
Section permutations.
Context {A : Type}.
@@ -2430,6 +2757,32 @@ Proof. revert n a. induction l1; intros; simpl; f_equal; auto. Qed.
Section zip_with.
Context {A B C : Type} (f : A → B → C).
+ Lemma zip_with_ext (g : A → B → C) l1 l2 k1 k2 :
+ (∀ x y, f x y = g x y) → l1 = l2 → k1 = k2 →
+ zip_with f l1 k1 = zip_with g l2 k2.
+ Proof.
+ intros ? <- <-. revert k1. induction l1; intros [|??]; simpl; f_equal; auto.
+ Qed.
+ Lemma Forall_zip_with_ext_l (g : A → B → C) l k1 k2 :
+ Forall (λ x, ∀ y, f x y = g x y) l → k1 = k2 →
+ zip_with f l k1 = zip_with g l k2.
+ Proof.
+ intros Hl <-. revert k1. induction Hl; intros [|??]; simpl; f_equal; auto.
+ Qed.
+ Lemma Forall_zip_with_ext_r (g : A → B → C) l1 l2 k :
+ l1 = l2 → Forall (λ y, ∀ x, f x y = g x y) k →
+ zip_with f l1 k = zip_with g l2 k.
+ Proof.
+ intros <- Hk. revert l1. induction Hk; intros [|??]; simpl; f_equal; auto.
+ Qed.
+
+ Lemma zip_with_fmap_l {D} (g : D → A) l k :
+ zip_with f (g <$> l) k = zip_with (λ x, f (g x)) l k.
+ Proof. revert k. induction l; intros [|??]; simpl; f_equal; auto. Qed.
+ Lemma zip_with_fmap_r {D} (g : D → B) l k :
+ zip_with f l (g <$> k) = zip_with (λ x y, f x (g y)) l k.
+ Proof. revert k. induction l; intros [|??]; simpl; f_equal; auto. Qed.
+
Lemma zip_with_nil_inv l1 l2 :
zip_with f l1 l2 = [] → l1 = [] ∨ l2 = [].
Proof. destruct l1, l2; simpl; auto with congruence. Qed.
@@ -2437,7 +2790,7 @@ Section zip_with.
zip_with f l1 l2 = y :: k →
∃ x1 x2 l1' l2', y = f x1 x2 ∧ k = zip_with f l1' l2' ∧
l1 = x1 :: l1' ∧ l2 = x2 :: l2'.
- Proof. intros. destruct l1, l2; simpl; simplify_equality; repeat eexists. Qed.
+ Proof. intros. destruct l1, l2; simplify_equality'; repeat eexists. Qed.
Lemma zip_with_app_inv l1 l2 k' k'' :
zip_with f l1 l2 = k' ++ k'' →
∃ l1' l1'' l2' l2'', k' = zip_with f l1' l2' ∧ k'' = zip_with f l1'' l2'' ∧
@@ -2445,7 +2798,7 @@ Section zip_with.
Proof.
revert l1 l2. induction k' as [|y k' IH]; simpl.
* intros l1 l2 ?. by eexists [], l1, [], l2.
- * intros [|x1 l1] [|x2 l2] ?; simpl; simplify_equality.
+ * intros [|x1 l1] [|x2 l2] ?; simplify_equality'.
destruct (IH l1 l2) as (l1'&l1''&l2'&l2''&?&?&?&?); subst; [done |].
by exists (x1 :: l1') l1'' (x2 :: l2') l2''.
Qed.
@@ -2455,8 +2808,8 @@ Section zip_with.
l1 `same_length` l2 → k1 `same_length` k2 →
zip_with f l1 l2 = zip_with f k1 k2 → l1 = k1 ∧ l2 = k2.
Proof.
- intros ? Hl. revert k1 k2. induction Hl; intros ?? [] ?; simpl;
- simplify_equality; f_equal; naive_solver.
+ intros ? Hl. revert k1 k2. induction Hl; intros ?? [] ?;
+ simplify_equality'; f_equal; naive_solver.
Qed.
Lemma zip_with_length l1 l2 :
@@ -2686,7 +3039,6 @@ Ltac decompose_Forall_hyps := repeat
| H : Forall _ (_ :: _) |- _ => rewrite Forall_cons in H; destruct H
| H : Forall _ (_ ++ _) |- _ => rewrite Forall_app in H; destruct H
| H : Forall _ (_ <$> _) |- _ => rewrite Forall_fmap in H
- | H : Forall _ ?l, H' : length ?l ≠0 |- _ => is_var l; destruct H; [done|]
| H : Forall2 _ [] [] |- _ => clear H
| H : Forall2 _ (_ :: _) [] |- _ => destruct (Forall2_cons_nil_inv _ _ _ H)
| H : Forall2 _ [] (_ :: _) |- _ => destruct (Forall2_nil_cons_inv _ _ _ H)
diff --git a/theories/mapset.v b/theories/mapset.v
index 4fc70523fcf589a2aebedd07bcf7539bcb37d376..113f2478004cb0b755370d2a39502934a7cb317c 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -54,8 +54,9 @@ Proof.
destruct (m1 !! x) as [[]|]; tauto.
* unfold intersection, elem_of, mapset_intersection, mapset_elem_of.
intros [m1] [m2] ?. simpl. rewrite lookup_intersection_Some.
- setoid_replace (is_Some (m2 !! x)) with (m2 !! x = Some ()); [done |].
- split; eauto. by intros [[] ?].
+ assert (is_Some (m2 !! x) ↔ m2 !! x = Some ()).
+ { split; eauto. by intros [[] ?]. }
+ naive_solver.
* unfold difference, elem_of, mapset_difference, mapset_elem_of.
intros [m1] [m2] ?. simpl. rewrite lookup_difference_Some.
destruct (m2 !! x) as [[]|]; intuition congruence.
diff --git a/theories/natmap.v b/theories/natmap.v
index 77637da66765a73cdcc553590914ded6cc5e35a0..2d0d1202f34bdfc8041e75bc706ea1e8e7f181d9 100644
--- a/theories/natmap.v
+++ b/theories/natmap.v
@@ -170,14 +170,15 @@ Proof.
induction l as [|[y|] l IH]; intros i j ?; simpl.
+ done.
+ destruct i as [|i]; simplify_equality; [left|].
- right. rewrite NPeano.Nat.add_succ_comm. by apply (IH i (S j)).
+ right. rewrite Nat.add_succ_comm. by apply (IH i (S j)).
+ destruct i as [|i]; simplify_equality.
- rewrite NPeano.Nat.add_succ_comm. by apply (IH i (S j)).
+ rewrite Nat.add_succ_comm. by apply (IH i (S j)).
Qed.
Lemma natmap_elem_of_to_list_raw {A} (l : natmap_raw A) i x :
(i,x) ∈ natmap_to_list_raw 0 l ↔ mjoin (l !! i) = Some x.
Proof.
- rewrite natmap_elem_of_to_list_raw_aux. setoid_rewrite plus_0_r. naive_solver.
+ rewrite natmap_elem_of_to_list_raw_aux. setoid_rewrite Nat.add_0_r.
+ naive_solver.
Qed.
Lemma natmap_to_list_raw_nodup {A} i (l : natmap_raw A) :
NoDup (natmap_to_list_raw i l).
diff --git a/theories/nmap.v b/theories/nmap.v
index 4a79107e320af9acae3ef248c92ae9151497cb2b..0bf1f153402d4113381a2df4f7dbefbeecb55fbb 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -58,8 +58,8 @@ Proof.
* intros ? [[x|] t]; unfold map_to_list; simpl.
+ constructor.
- rewrite elem_of_list_fmap. by intros [[??] [??]].
- - rewrite (NoDup_fmap _). apply map_to_list_nodup.
- + rewrite (NoDup_fmap _). apply map_to_list_nodup.
+ - apply (fmap_nodup _), map_to_list_nodup.
+ + apply (fmap_nodup _), map_to_list_nodup.
* intros ? t i x. unfold map_to_list. split.
+ destruct t as [[y|] t]; simpl.
- rewrite elem_of_cons, elem_of_list_fmap.
diff --git a/theories/numbers.v b/theories/numbers.v
index d0e2c74bdbccb64a6b49694ce034c40418e617f6..5cda50afa878a5505146878dadb3cdc17035b283 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -3,7 +3,7 @@
(** This file collects some trivial facts on the Coq types [nat] and [N] for
natural numbers, and the type [Z] for integers. It also declares some useful
notations. *)
-Require Export Eqdep PArith NArith ZArith.
+Require Export Eqdep PArith NArith ZArith NPeano.
Require Import Qcanon.
Require Export base decidable.
Open Scope nat_scope.
@@ -31,6 +31,10 @@ Instance nat_eq_dec: ∀ x y : nat, Decision (x = y) := eq_nat_dec.
Instance nat_le_dec: ∀ x y : nat, Decision (x ≤ y) := le_dec.
Instance nat_lt_dec: ∀ x y : nat, Decision (x < y) := lt_dec.
Instance nat_inhabited: Inhabited nat := populate 0%nat.
+Instance: Injective (=) (=) S.
+Proof. by injection 1. Qed.
+Instance: PartialOrder (≤).
+Proof. repeat split; repeat intro; auto with lia. Qed.
Instance nat_le_pi: ∀ x y : nat, ProofIrrel (x ≤ y).
Proof.
@@ -38,8 +42,8 @@ Proof.
y = y' → eq_dep nat (le x) y p y' q) as aux.
{ fix 3. intros x ? [|y p] ? [|y' q].
* done.
- * clear nat_le_pi. omega.
- * clear nat_le_pi. omega.
+ * clear nat_le_pi. intros; exfalso; auto with lia.
+ * clear nat_le_pi. intros; exfalso; auto with lia.
* injection 1. intros Hy. by case (nat_le_pi x y p y' q Hy). }
intros x y p q.
by apply (eq_dep_eq_dec (λ x y, decide (x = y))), aux.
@@ -47,11 +51,6 @@ Qed.
Instance nat_lt_pi: ∀ x y : nat, ProofIrrel (x < y).
Proof. apply _. Qed.
-Lemma lt_n_SS n : n < S (S n).
-Proof. auto with arith. Qed.
-Lemma lt_n_SSS n : n < S (S (S n)).
-Proof. auto with arith. Qed.
-
Definition sum_list_with {A} (f : A → nat) : list A → nat :=
fix go l :=
match l with
@@ -60,23 +59,35 @@ Definition sum_list_with {A} (f : A → nat) : list A → nat :=
end.
Notation sum_list := (sum_list_with id).
-Lemma mult_split_eq n x1 x2 y1 y2 :
+Lemma Nat_lt_succ_succ n : n < S (S n).
+Proof. auto with arith. Qed.
+Lemma Nat_mul_split_l n x1 x2 y1 y2 :
x2 < n → y2 < n → x1 * n + x2 = y1 * n + y2 → x1 = y1 ∧ x2 = y2.
Proof.
- intros Hx2 Hy2 E.
- cut (x1 = y1); [intros; subst;lia |].
+ intros Hx2 Hy2 E. cut (x1 = y1); [intros; subst;lia |].
revert y1 E. induction x1; simpl; intros [|?]; simpl; auto with lia.
Qed.
+Lemma Nat_mul_split_r n x1 x2 y1 y2 :
+ x1 < n → y1 < n → x1 + x2 * n = y1 + y2 * n → x1 = y1 ∧ x2 = y2.
+Proof. intros. destruct (Nat_mul_split_l n x2 x1 y2 y1); auto with lia. Qed.
(** * Notations and properties of [positive] *)
Open Scope positive_scope.
-Instance positive_eq_dec: ∀ x y : positive, Decision (x = y) := Pos.eq_dec.
-Instance positive_inhabited: Inhabited positive := populate 1.
-
+Infix "≤" := Pos.le : positive_scope.
+Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z)%positive : positive_scope.
+Notation "x ≤ y < z" := (x ≤ y ∧ y < z)%positive : positive_scope.
+Notation "x < y < z" := (x < y ∧ y < z)%positive : positive_scope.
+Notation "x < y ≤ z" := (x < y ∧ y ≤ z)%positive : positive_scope.
+Notation "(≤)" := Pos.le (only parsing) : positive_scope.
+Notation "(<)" := Pos.lt (only parsing) : positive_scope.
Notation "(~0)" := xO (only parsing) : positive_scope.
Notation "(~1)" := xI (only parsing) : positive_scope.
+Arguments Pos.of_nat _ : simpl never.
+Instance positive_eq_dec: ∀ x y : positive, Decision (x = y) := Pos.eq_dec.
+Instance positive_inhabited: Inhabited positive := populate 1.
+
Instance: Injective (=) (=) (~0).
Proof. by injection 1. Qed.
Instance: Injective (=) (=) (~1).
@@ -178,11 +189,13 @@ Next Obligation. congruence. Qed.
Instance N_inhabited: Inhabited N := populate 1%N.
(** * Notations and properties of [Z] *)
+Open Scope Z_scope.
+
Infix "≤" := Z.le : Z_scope.
-Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z)%Z : Z_scope.
-Notation "x ≤ y < z" := (x ≤ y ∧ y < z)%Z : Z_scope.
-Notation "x < y < z" := (x < y ∧ y < z)%Z : Z_scope.
-Notation "x < y ≤ z" := (x < y ∧ y ≤ z)%Z : Z_scope.
+Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z) : Z_scope.
+Notation "x ≤ y < z" := (x ≤ y ∧ y < z) : Z_scope.
+Notation "x < y < z" := (x < y ∧ y < z) : Z_scope.
+Notation "x < y ≤ z" := (x < y ∧ y ≤ z) : Z_scope.
Notation "(≤)" := Z.le (only parsing) : Z_scope.
Notation "(<)" := Z.lt (only parsing) : Z_scope.
@@ -190,14 +203,28 @@ Infix "`div`" := Z.div (at level 35) : Z_scope.
Infix "`mod`" := Z.modulo (at level 35) : Z_scope.
Infix "`quot`" := Z.quot (at level 35) : Z_scope.
Infix "`rem`" := Z.rem (at level 35) : Z_scope.
+Infix "≪" := Z.shiftl (at level 35) : Z_scope.
+Infix "≫" := Z.shiftr (at level 35) : Z_scope.
Instance Z_eq_dec: ∀ x y : Z, Decision (x = y) := Z.eq_dec.
-Instance Z_le_dec: ∀ x y : Z, Decision (x ≤ y)%Z := Z_le_dec.
-Instance Z_lt_dec: ∀ x y : Z, Decision (x < y)%Z := Z_lt_dec.
-Instance Z_inhabited: Inhabited Z := populate 1%Z.
+Instance Z_le_dec: ∀ x y : Z, Decision (x ≤ y) := Z_le_dec.
+Instance Z_lt_dec: ∀ x y : Z, Decision (x < y) := Z_lt_dec.
+Instance Z_inhabited: Inhabited Z := populate 1.
+
+Lemma Z_pow_pred_r n m : 0 < m → n * n ^ (Z.pred m) = n ^ m.
+Proof.
+ intros. rewrite <-Z.pow_succ_r, Z.succ_pred. done. by apply Z.lt_le_pred.
+Qed.
+Lemma Z_quot_range_nonneg k x y : 0 ≤ x < k → 0 < y → 0 ≤ x `quot` y < k.
+Proof.
+ intros [??] ?.
+ destruct (decide (y = 1)); subst; [rewrite Z.quot_1_r; auto |].
+ destruct (decide (x = 0)); subst; [rewrite Z.quot_0_l; auto with lia |].
+ split. apply Z.quot_pos; lia. transitivity x; auto. apply Z.quot_lt; lia.
+Qed.
(* Note that we cannot disable simpl for [Z.of_nat] as that would break
-[omega] and [lia]. *)
+tactics as [lia]. *)
Arguments Z.to_nat _ : simpl never.
Arguments Z.mul _ _ : simpl never.
Arguments Z.add _ _ : simpl never.
@@ -208,16 +235,41 @@ Arguments Z.modulo _ _ : simpl never.
Arguments Z.quot _ _ : simpl never.
Arguments Z.rem _ _ : simpl never.
-Lemma Zmod_pos a b : (0 < b)%Z → (0 ≤ a `mod` b)%Z.
+Lemma Z_mod_pos a b : 0 < b → 0 ≤ a `mod` b.
Proof. apply Z.mod_pos_bound. Qed.
Hint Resolve Z.lt_le_incl : zpos.
Hint Resolve Z.add_nonneg_pos Z.add_pos_nonneg Z.add_nonneg_nonneg : zpos.
Hint Resolve Z.mul_nonneg_nonneg Z.mul_pos_pos : zpos.
-Hint Resolve Z.pow_pos_nonneg : zpos.
-Hint Resolve Zmod_pos Z.div_pos : zpos.
+Hint Resolve Z.pow_pos_nonneg Z.pow_nonneg: zpos.
+Hint Resolve Z_mod_pos Z.div_pos : zpos.
Hint Extern 1000 => lia : zpos.
+Lemma Z2Nat_inj_pow (x y : nat) : Z.of_nat (x ^ y) = x ^ y.
+Proof.
+ induction y as [|y IH].
+ * by rewrite Z.pow_0_r, Nat.pow_0_r.
+ * by rewrite Nat.pow_succ_r, Nat2Z.inj_succ, Z.pow_succ_r,
+ Nat2Z.inj_mul, IH by auto with zpos.
+Qed.
+Lemma Z2Nat_inj_div x y : Z.of_nat (x `div` y) = x `div` y.
+Proof.
+ destruct (decide (y = 0%nat)); [by subst; destruct x |].
+ apply Z.div_unique with (x `mod` y)%nat.
+ { left. rewrite <-(Nat2Z.inj_le 0), <-Nat2Z.inj_lt.
+ apply Nat.mod_bound_pos; lia. }
+ by rewrite <-Nat2Z.inj_mul, <-Nat2Z.inj_add, <-Nat.div_mod.
+Qed.
+Lemma Z2Nat_inj_mod x y : Z.of_nat (x `mod` y) = x `mod` y.
+Proof.
+ destruct (decide (y = 0%nat)); [by subst; destruct x |].
+ apply Z.mod_unique with (x `div` y)%nat.
+ { left. rewrite <-(Nat2Z.inj_le 0), <-Nat2Z.inj_lt.
+ apply Nat.mod_bound_pos; lia. }
+ by rewrite <-Nat2Z.inj_mul, <-Nat2Z.inj_add, <-Nat.div_mod.
+Qed.
+Close Scope Z_scope.
+
(** * Notations and properties of [Qc] *)
Notation "2" := (1+1)%Qc : Qc_scope.
Infix "≤" := Qcle : Qc_scope.
@@ -263,24 +315,17 @@ Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_r. Qed.
(** * Conversions *)
Lemma Z_to_nat_nonpos x : (x ≤ 0)%Z → Z.to_nat x = 0.
-Proof.
- destruct x; simpl; auto using Z2Nat.inj_neg.
- by intros [].
-Qed.
+Proof. destruct x; simpl; auto using Z2Nat.inj_neg. by intros []. Qed.
(** The function [Z_to_option_N] converts an integer [x] into a natural number
by giving [None] in case [x] is negative. *)
Definition Z_to_option_N (x : Z) : option N :=
match x with
- | Z0 => Some N0
- | Zpos p => Some (Npos p)
- | Zneg _ => None
+ | Z0 => Some N0 | Zpos p => Some (Npos p) | Zneg _ => None
end.
Definition Z_to_option_nat (x : Z) : option nat :=
match x with
- | Z0 => Some 0
- | Zpos p => Some (Pos.to_nat p)
- | Zneg _ => None
+ | Z0 => Some 0 | Zpos p => Some (Pos.to_nat p) | Zneg _ => None
end.
Lemma Z_to_option_N_Some x y :
@@ -333,9 +378,8 @@ Lemma N_to_nat_1 : N.to_nat 1 = 1.
Proof. done. Qed.
Lemma N_to_nat_div x y : N.to_nat (x `div` y) = N.to_nat x `div` N.to_nat y.
Proof.
- destruct (decide (y = 0%N)).
- { subst. by destruct x. }
- apply NPeano.Nat.div_unique with (N.to_nat (x `mod` y)).
+ destruct (decide (y = 0%N)); [by subst; destruct x |].
+ apply Nat.div_unique with (N.to_nat (x `mod` y)).
{ by apply N_to_nat_lt, N.mod_lt. }
rewrite (N.div_unique_exact (x * y) y x), N.div_mul by lia.
by rewrite <-N2Nat.inj_mul, <-N2Nat.inj_add, <-N.div_mod.
@@ -344,7 +388,7 @@ Qed.
Lemma N_to_nat_mod x y :
y ≠0%N → N.to_nat (x `mod` y) = N.to_nat x `mod` N.to_nat y.
Proof.
- intros. apply NPeano.Nat.mod_unique with (N.to_nat (x `div` y)).
+ intros. apply Nat.mod_unique with (N.to_nat (x `div` y)).
{ by apply N_to_nat_lt, N.mod_lt. }
rewrite (N.div_unique_exact (x * y) y x), N.div_mul by lia.
by rewrite <-N2Nat.inj_mul, <-N2Nat.inj_add, <-N.div_mod.
diff --git a/theories/option.v b/theories/option.v
index 5263bc9e413f3e3d68abac3c6b42f8c14a607569..55966090c453ed9d08485f4b1ddb40085f421e17 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -92,14 +92,6 @@ Instance option_fmap: FMap option := @option_map.
Instance option_guard: MGuard option := λ P dec A x,
match dec with left H => x H | _ => None end.
-Definition mapM `{!MBind M} `{!MRet M} {A B}
- (f : A → M B) : list A → M (list B) :=
- fix go l :=
- match l with
- | [] => mret []
- | x :: l => y ↠f x; k ↠go l; mret (y :: k)
- end.
-
Lemma fmap_is_Some {A B} (f : A → B) x : is_Some (f <$> x) ↔ is_Some x.
Proof. unfold is_Some; destruct x; naive_solver. Qed.
Lemma fmap_Some {A B} (f : A → B) x y :
@@ -110,6 +102,9 @@ Proof. by destruct x. Qed.
Lemma option_fmap_id {A} (x : option A) : id <$> x = x.
Proof. by destruct x. Qed.
+Lemma option_fmap_bind {A B C} (f : A → B) (g : B → option C) x :
+ (f <$> x) ≫= g = x ≫= g ∘ f.
+Proof. by destruct x. Qed.
Lemma option_bind_assoc {A B C} (f : A → option B)
(g : B → option C) (x : option A) : (x ≫= f) ≫= g = x ≫= (mbind g ∘ f).
Proof. by destruct x; simpl. Qed.
@@ -119,39 +114,33 @@ Proof. intros. destruct x, y; simplify_equality; simpl; auto. Qed.
Lemma option_bind_ext_fun {A B} (f g : A → option B) x :
(∀ a, f a = g a) → x ≫= f = x ≫= g.
Proof. intros. by apply option_bind_ext. Qed.
+Lemma bind_Some {A B} (f : A → option B) (x : option A) b :
+ x ≫= f = Some b ↔ ∃ a, x = Some a ∧ f a = Some b.
+Proof. split. by destruct x as [a|]; [exists a|]. by intros (?&->&?). Qed.
+Lemma bind_None {A B} (f : A → option B) (x : option A) :
+ x ≫= f = None ↔ x = None ∨ ∃ a, x = Some a ∧ f a = None.
+Proof.
+ split.
+ * destruct x; intros; simplify_equality'; eauto.
+ * by intros [->|(?&->&?)].
+Qed.
-Section mapM.
- Context {A B : Type} (f : A → option B).
-
- Lemma mapM_ext (g : A → option B) l : (∀ x, f x = g x) → mapM f l = mapM g l.
- Proof. intros Hfg. by induction l; simpl; rewrite ?Hfg, ?IHl. Qed.
- Lemma Forall2_mapM_ext (g : A → option B) l k :
- Forall2 (λ x y, f x = g y) l k → mapM f l = mapM g k.
- Proof. induction 1 as [|???? Hfg ? IH]; simpl. done. by rewrite Hfg, IH. Qed.
- Lemma Forall_mapM_ext (g : A → option B) l :
- Forall (λ x, f x = g x) l → mapM f l = mapM g l.
- Proof. induction 1 as [|?? Hfg ? IH]; simpl. done. by rewrite Hfg, IH. Qed.
-
- Lemma mapM_Some_1 l k : mapM f l = Some k → Forall2 (λ x y, f x = Some y) l k.
- Proof.
- revert k. induction l as [|x l]; intros [|y k]; simpl; try done.
- * destruct (f x); simpl; [|discriminate]. by destruct (mapM f l).
- * destruct (f x) eqn:?; simpl; [|discriminate].
- destruct (mapM f l); intros; simplify_equality. constructor; auto.
- Qed.
- Lemma mapM_Some_2 l k : Forall2 (λ x y, f x = Some y) l k → mapM f l = Some k.
- Proof.
- induction 1 as [|???? Hf ? IH]; simpl; [done |].
- rewrite Hf. simpl. by rewrite IH.
- Qed.
- Lemma mapM_Some l k : mapM f l = Some k ↔ Forall2 (λ x y, f x = Some y) l k.
- Proof. split; auto using mapM_Some_1, mapM_Some_2. Qed.
-End mapM.
+Tactic Notation "case_option_guard" "as" ident(Hx) :=
+ match goal with
+ | H : context C [@mguard option _ ?P ?dec _ ?x] |- _ =>
+ let X := context C [ match dec with left H => x H | _ => None end ] in
+ change X in H; destruct_decide dec as Hx
+ | |- context C [@mguard option _ ?P ?dec _ ?x] =>
+ let X := context C [ match dec with left H => x H | _ => None end ] in
+ change X; destruct_decide dec as Hx
+ end.
+Tactic Notation "case_option_guard" :=
+ let H := fresh in case_option_guard as H.
Tactic Notation "simplify_option_equality" "by" tactic3(tac) := repeat
match goal with
| _ => progress (unfold default in *)
- | _ => first [progress simpl in * | progress simplify_equality]
+ | _ => progress simplify_equality'
| H : context [mbind (M:=option) (A:=?A) ?f ?o] |- _ =>
let Hx := fresh in
first
@@ -222,17 +211,10 @@ Tactic Notation "simplify_option_equality" "by" tactic3(tac) := repeat
| assert (o = None) as Hx by tac ];
rewrite Hx; clear Hx
end
- | H : context C [@mguard option _ ?P ?dec _ ?x] |- _ =>
- let X := context C [ match dec with left H => x H | _ => None end ] in
- change X in H; destruct_decide dec
- | |- context C [@mguard option _ ?P ?dec _ ?x] =>
- let X := context C [ match dec with left H => x H | _ => None end ] in
- change X; destruct_decide dec
| H1 : ?o = Some ?x, H2 : ?o = Some ?y |- _ =>
assert (y = x) by congruence; clear H2
- | H1 : ?o = Some ?x, H2 : ?o = None |- _ =>
- congruence
- | H : mapM _ _ = Some _ |- _ => apply mapM_Some in H
+ | H1 : ?o = Some ?x, H2 : ?o = None |- _ => congruence
+ | _ => progress case_option_guard
end.
Tactic Notation "simplify_option_equality" :=
simplify_option_equality by eauto.
diff --git a/theories/tactics.v b/theories/tactics.v
index 150d32d05fb0afc0a45edce8192cecc17fa2bfbe..e9687ca034c98523420ab97fce8c7b63dbfe1523 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -161,12 +161,7 @@ Ltac simplify_equality := repeat
| H : _ = _ |- _ => injection' H
| H : ?x = ?x |- _ => clear H
end.
-
-(** Coq's default [remember] tactic does have an option to name the generated
-equality. The following tactic extends [remember] to do so. *)
-Tactic Notation "remember" constr(t) "as" "(" ident(x) "," ident(E) ")" :=
- remember t as x;
- match goal with E' : x = _ |- _ => rename E' into E end.
+Ltac simplify_equality' := repeat (progress simpl in * || simplify_equality).
(** Given a tactic [tac2] generating a list of terms, [iter tac1 tac2]
runs [tac x] for each element [x] until [tac x] succeeds. If it does not
@@ -264,7 +259,7 @@ Tactic Notation "naive_solver" tactic(tac) :=
unfold iff, not in *;
repeat match goal with
| H : context [∀ _, _ ∧ _ ] |- _ =>
- repeat setoid_rewrite forall_and_distr in H; revert H
+ repeat setoid_rewrite forall_and_distr in H; revert H
end;
let rec go n :=
repeat match goal with
diff --git a/theories/vector.v b/theories/vector.v
index 8c726a5daf8e79d8cced00547f52201d8c858d17..90abce080e33e78759e8408a6dda32b771218857 100644
--- a/theories/vector.v
+++ b/theories/vector.v
@@ -5,7 +5,7 @@
definitions from the standard library, but renames or changes their notations,
so that it becomes more consistent with the naming conventions in this
development. *)
-Require Import list.
+Require Import list finite.
Open Scope vector_scope.
(** * The fin type *)
@@ -35,8 +35,8 @@ Fixpoint fin_to_nat {n} (i : fin n) : nat :=
end.
Coercion fin_to_nat : fin >-> nat.
+Notation fin_of_nat := Fin.of_nat_lt.
Notation fin_rect2 := Fin.rect2.
-Notation FS_inj := Fin.FS_inj.
Instance fin_dec {n} : ∀ i j : fin n, Decision (i = j).
Proof.
@@ -46,7 +46,7 @@ Proof.
(λ _ _, right _)
(λ _ _, right _)
(λ _ _ _ H, cast_if H));
- abstract (f_equal; by auto using FS_inj).
+ abstract (f_equal; by auto using Fin.FS_inj).
Defined.
(** The inversion principle [fin_S_inv] is more convenient than its variant
@@ -77,6 +77,37 @@ Ltac inv_fin i :=
match goal with |- ∀ i, @?P i => apply (fin_S_inv P) end
end.
+Instance: Injective (=) (=) (@FS n).
+Proof. intros n i j. apply Fin.FS_inj. Qed.
+Instance: Injective (=) (=) (@fin_to_nat n).
+Proof.
+ intros n i. induction i; intros j; inv_fin j; simpl; auto with lia f_equal.
+Qed.
+Lemma fin_to_nat_lt {n} (i : fin n) : fin_to_nat i < n.
+Proof. induction i; simpl; lia. Qed.
+Lemma fin_to_of_nat n m (H : n < m) : fin_to_nat (Fin.of_nat_lt H) = n.
+Proof.
+ revert m H. induction n; intros [|?]; simpl; auto; intros; exfalso; lia.
+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 |}.
+Next Obligation.
+ intros n. induction n; simpl; constructor.
+ * rewrite elem_of_list_fmap. by intros (?&?&?).
+ * by apply (fmap_nodup _).
+Qed.
+Next Obligation.
+ intros n i. induction i as [|n i IH]; simpl;
+ 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.
+
(** * Vectors *)
(** The type [vec n] represents lists of consisting of exactly [n] elements.
Whereas the standard library declares exactly the same notations for vectors as
@@ -90,11 +121,16 @@ Notation vapp := Vector.append.
Arguments vcons {_} _ {_} _.
Infix ":::" := vcons (at level 60, right associativity) : vector_scope.
+Notation "(:::)" := vcons (only parsing) : vector_scope.
+Notation "( x :::)" := (vcons x) (only parsing) : vector_scope.
+Notation "(::: v )" := (λ x, vcons x v) (only parsing) : vector_scope.
Notation "[# ] " := vnil : vector_scope.
Notation "[# x ] " := (vcons x vnil) : vector_scope.
Notation "[# x ; .. ; y ] " := (vcons x .. (vcons y vnil) ..) : vector_scope.
-
Infix "+++" := vapp (at level 60, right associativity) : vector_scope.
+Notation "(+++)" := vapp (only parsing) : vector_scope.
+Notation "( v +++)" := (vapp v) (only parsing) : vector_scope.
+Notation "(+++ w )" := (λ v, vapp v w) (only parsing) : vector_scope.
(** Notice that we cannot define [Vector.nth] as an instance of our [Lookup]
type class, as it has a dependent type. *)
@@ -203,13 +239,13 @@ Lemma vec_to_list_inj1 {A n m} (v : vec A n) (w : vec A m) :
vec_to_list v = vec_to_list w → n = m.
Proof.
revert m w. induction v; intros ? [|???] ?;
- simpl in *; simplify_equality; f_equal; eauto.
+ simplify_equality'; f_equal; eauto.
Qed.
Lemma vec_to_list_inj2 {A n} (v : vec A n) (w : vec A n) :
vec_to_list v = vec_to_list w → v = w.
Proof.
revert w. induction v; intros w; inv_vec w; intros;
- simpl in *; simplify_equality; f_equal; eauto.
+ simplify_equality'; f_equal; eauto.
Qed.
Lemma vlookup_middle {A n m} (v : vec A n) (w : vec A m) x :