From 9774ce9cad21d62660b07ef54ab9abf8909f7fdd Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 17 Feb 2016 01:03:30 +0100
Subject: [PATCH] Use scheme - then + then * for bullets.
---
theories/bsets.v | 10 +-
theories/co_pset.v | 34 ++--
theories/collections.v | 24 +--
theories/fin_collections.v | 34 ++--
theories/fin_maps.v | 118 ++++++------
theories/finite.v | 46 ++---
theories/gmap.v | 28 +--
theories/hashset.v | 18 +-
theories/lexico.v | 12 +-
theories/list.v | 364 ++++++++++++++++++-------------------
theories/listset.v | 34 ++--
theories/listset_nodup.v | 16 +-
theories/mapset.v | 20 +-
theories/natmap.v | 30 +--
theories/nmap.v | 36 ++--
theories/numbers.v | 20 +-
theories/option.v | 6 +-
theories/orders.v | 42 ++---
theories/pmap.v | 90 ++++-----
theories/relations.v | 6 +-
theories/streams.v | 6 +-
theories/vector.v | 20 +-
theories/zmap.v | 26 +--
23 files changed, 520 insertions(+), 520 deletions(-)
diff --git a/theories/bsets.v b/theories/bsets.v
index 2b486081..e8c0906b 100644
--- a/theories/bsets.v
+++ b/theories/bsets.v
@@ -21,11 +21,11 @@ Instance bset_collection {A} `{∀ x y : A, Decision (x = y)} :
Collection A (bset A).
Proof.
split; [split| |].
- * by intros x ?.
- * by intros x y; rewrite <-(bool_decide_spec (x = y)).
- * split. apply orb_prop_elim. apply orb_prop_intro.
- * split. apply andb_prop_elim. apply andb_prop_intro.
- * intros X Y x; unfold elem_of, bset_elem_of; simpl.
+ - by intros x ?.
+ - by intros x y; rewrite <-(bool_decide_spec (x = y)).
+ - split. apply orb_prop_elim. apply orb_prop_intro.
+ - split. apply andb_prop_elim. apply andb_prop_intro.
+ - intros X Y x; unfold elem_of, bset_elem_of; simpl.
destruct (bset_car X x), (bset_car Y x); simpl; tauto.
Qed.
Instance bset_elem_of_dec {A} x (X : bset A) : Decision (x ∈ X) := _.
diff --git a/theories/co_pset.v b/theories/co_pset.v
index 16692659..a14659a2 100644
--- a/theories/co_pset.v
+++ b/theories/co_pset.v
@@ -65,10 +65,10 @@ Lemma coPset_eq t1 t2 :
Proof.
revert t2.
induction t1 as [b1|b1 l1 IHl r1 IHr]; intros [b2|b2 l2 r2] Ht ??; simpl in *.
- * f_equal; apply (Ht 1).
- * by discriminate (coPLeaf_wf (coPNode b2 l2 r2) b1).
- * by discriminate (coPLeaf_wf (coPNode b1 l1 r1) b2).
- * f_equal; [apply (Ht 1)| |].
+ - f_equal; apply (Ht 1).
+ - by discriminate (coPLeaf_wf (coPNode b2 l2 r2) b1).
+ - by discriminate (coPLeaf_wf (coPNode b1 l1 r1) b2).
+ - f_equal; [apply (Ht 1)| |].
+ apply IHl; try apply (λ x, Ht (x~0)); eauto.
+ apply IHr; try apply (λ x, Ht (x~1)); eauto.
Qed.
@@ -163,13 +163,13 @@ Instance coPset_elem_of_dec (p : positive) (X : coPset) : Decision (p ∈ X) :=
Instance coPset_collection : Collection positive coPset.
Proof.
split; [split| |].
- * by intros ??.
- * intros p q. apply elem_to_Pset_singleton.
- * intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_union; simpl.
+ - by intros ??.
+ - intros p q. apply elem_to_Pset_singleton.
+ - intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_union; simpl.
by rewrite elem_to_Pset_union, orb_True.
- * intros [t] [t'] p; unfold elem_of,coPset_elem_of,coPset_intersection; simpl.
+ - intros [t] [t'] p; unfold elem_of,coPset_elem_of,coPset_intersection; simpl.
by rewrite elem_to_Pset_intersection, andb_True.
- * intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_difference; simpl.
+ - intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_difference; simpl.
by rewrite elem_to_Pset_intersection,
elem_to_Pset_opp, andb_True, negb_True.
Qed.
@@ -192,7 +192,7 @@ Lemma coPset_finite_spec X : set_finite X ↔ coPset_finite (`X).
Proof.
destruct X as [t Ht].
unfold set_finite, elem_of at 1, coPset_elem_of; simpl; clear Ht; split.
- * induction t as [b|b l IHl r IHr]; simpl.
+ - induction t as [b|b l IHl r IHr]; simpl.
{ destruct b; simpl; [intros [l Hl]|done].
by apply (is_fresh (of_list l : Pset)), elem_of_of_list, Hl. }
intros [ll Hll]; rewrite andb_True; split.
@@ -200,7 +200,7 @@ Proof.
rewrite elem_of_list_omap; intros; exists (i~0); auto.
+ apply IHr; exists (omap (maybe (~1)) ll); intros i.
rewrite elem_of_list_omap; intros; exists (i~1); auto.
- * induction t as [b|b l IHl r IHr]; simpl; [by exists []; destruct b|].
+ - induction t as [b|b l IHl r IHr]; simpl; [by exists []; destruct b|].
rewrite andb_True; intros [??]; destruct IHl as [ll ?], IHr as [rl ?]; auto.
exists ([1] ++ ((~0) <$> ll) ++ ((~1) <$> rl))%list; intros [i|i|]; simpl;
rewrite elem_of_cons, elem_of_app, !elem_of_list_fmap; naive_solver.
@@ -237,8 +237,8 @@ Qed.
Lemma coPpick_elem_of X : ¬set_finite X → coPpick X ∈ X.
Proof.
destruct X as [t ?]; unfold coPpick; destruct (coPpick_raw _) as [j|] eqn:?.
- * by intros; apply coPpick_raw_elem_of.
- * by intros []; apply coPset_finite_spec, coPpick_raw_None.
+ - by intros; apply coPpick_raw_elem_of.
+ - by intros []; apply coPset_finite_spec, coPpick_raw_None.
Qed.
(** * Conversion to psets *)
@@ -270,8 +270,8 @@ Fixpoint of_Pset_raw (t : Pmap_raw ()) : coPset_raw :=
Lemma of_Pset_wf t : Pmap_wf t → coPset_wf (of_Pset_raw t).
Proof.
induction t as [|[] l IHl r IHr]; simpl; rewrite ?andb_True; auto.
- * intros [??]; destruct l as [|[]], r as [|[]]; simpl in *; auto.
- * destruct l as [|[]], r as [|[]]; simpl in *; rewrite ?andb_true_r;
+ - intros [??]; destruct l as [|[]], r as [|[]]; simpl in *; auto.
+ - destruct l as [|[]], r as [|[]]; simpl in *; rewrite ?andb_true_r;
rewrite ?andb_True; rewrite ?andb_True in IHl, IHr; intuition.
Qed.
Lemma elem_of_of_Pset_raw i t : e_of i (of_Pset_raw t) ↔ t !! i = Some ().
@@ -327,9 +327,9 @@ Definition coPset_suffixes (p : positive) : coPset :=
Lemma elem_coPset_suffixes p q : p ∈ coPset_suffixes q ↔ ∃ q', p = q' ++ q.
Proof.
unfold elem_of, coPset_elem_of; simpl; split.
- * revert p; induction q; intros [?|?|]; simpl;
+ - revert p; induction q; intros [?|?|]; simpl;
rewrite ?coPset_elem_of_node; naive_solver.
- * by intros [q' ->]; induction q; simpl; rewrite ?coPset_elem_of_node.
+ - by intros [q' ->]; induction q; simpl; rewrite ?coPset_elem_of_node.
Qed.
Lemma coPset_suffixes_infinite p : ¬set_finite (coPset_suffixes p).
Proof.
diff --git a/theories/collections.v b/theories/collections.v
index f83a8e9c..3cb2d5bd 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -48,8 +48,8 @@ Section simple_collection.
Lemma elem_of_subseteq_singleton x X : x ∈ X ↔ {[ x ]} ⊆ X.
Proof.
split.
- * intros ??. rewrite elem_of_singleton. by intros ->.
- * intros Ex. by apply (Ex x), elem_of_singleton.
+ - intros ??. rewrite elem_of_singleton. by intros ->.
+ - intros Ex. by apply (Ex x), elem_of_singleton.
Qed.
Global Instance singleton_proper : Proper ((=) ==> (≡)) (singleton (B:=C)).
Proof. by repeat intro; subst. Qed.
@@ -59,9 +59,9 @@ Section simple_collection.
Lemma elem_of_union_list Xs x : x ∈ ⋃ Xs ↔ ∃ X, X ∈ Xs ∧ x ∈ X.
Proof.
split.
- * induction Xs; simpl; intros HXs; [by apply elem_of_empty in HXs|].
+ - induction Xs; simpl; intros HXs; [by apply elem_of_empty in HXs|].
setoid_rewrite elem_of_cons. apply elem_of_union in HXs. naive_solver.
- * intros [X []]. induction 1; simpl; [by apply elem_of_union_l |].
+ - intros [X []]. induction 1; simpl; [by apply elem_of_union_l |].
intros. apply elem_of_union_r; auto.
Qed.
Lemma non_empty_singleton x : ({[ x ]} : C) ≢ ∅.
@@ -113,9 +113,9 @@ Section of_option_list.
Lemma elem_of_of_list (x : A) l : x ∈ of_list l ↔ x ∈ l.
Proof.
split.
- * induction l; simpl; [by rewrite elem_of_empty|].
+ - induction l; simpl; [by rewrite elem_of_empty|].
rewrite elem_of_union,elem_of_singleton; intros [->|?]; constructor; auto.
- * induction 1; simpl; rewrite elem_of_union, elem_of_singleton; auto.
+ - induction 1; simpl; rewrite elem_of_union, elem_of_singleton; auto.
Qed.
End of_option_list.
@@ -356,11 +356,11 @@ Section collection_ops.
Forall2 (∈) xs Xs ∧ y ∈ Y ∧ foldr (λ x, (≫= f x)) (Some y) xs = Some x.
Proof.
split.
- * revert x. induction Xs; simpl; intros x HXs; [eexists [], x; intuition|].
+ - revert x. induction Xs; simpl; intros x HXs; [eexists [], x; intuition|].
rewrite elem_of_intersection_with in HXs; destruct HXs as (x1&x2&?&?&?).
destruct (IHXs x2) as (xs & y & hy & ? & ?); trivial.
eexists (x1 :: xs), y. intuition (simplify_option_equality; auto).
- * intros (xs & y & Hxs & ? & Hx). revert x Hx.
+ - intros (xs & y & Hxs & ? & Hx). revert x Hx.
induction Hxs; intros; simplify_option_equality; [done |].
rewrite elem_of_intersection_with. naive_solver.
Qed.
@@ -389,8 +389,8 @@ Section NoDup.
Global Instance: Proper (R ==> (≡) ==> iff) elem_of_upto.
Proof.
intros ?? E1 ?? E2. split; intros [z [??]]; exists z.
- * rewrite <-E1, <-E2; intuition.
- * rewrite E1, E2; intuition.
+ - rewrite <-E1, <-E2; intuition.
+ - rewrite E1, E2; intuition.
Qed.
Global Instance: Proper ((≡) ==> iff) set_NoDup.
Proof. firstorder. Qed.
@@ -575,8 +575,8 @@ Section collection_monad.
l ∈ mapM f k ↔ Forall2 (λ x y, x ∈ f y) l k.
Proof.
split.
- * revert l. induction k; solve_elem_of.
- * induction 1; solve_elem_of.
+ - revert l. induction k; solve_elem_of.
+ - induction 1; solve_elem_of.
Qed.
Lemma collection_mapM_length {A B} (f : A → M B) l k :
l ∈ mapM f k → length l = length k.
diff --git a/theories/fin_collections.v b/theories/fin_collections.v
index 7dbbb4b4..60abe908 100644
--- a/theories/fin_collections.v
+++ b/theories/fin_collections.v
@@ -20,9 +20,9 @@ Proof. by exists (elements X); intros; rewrite elem_of_elements. Qed.
Global Instance elements_proper: Proper ((≡) ==> (≡ₚ)) (elements (C:=C)).
Proof.
intros ?? E. apply NoDup_Permutation.
- * apply NoDup_elements.
- * apply NoDup_elements.
- * intros. by rewrite !elem_of_elements, E.
+ - apply NoDup_elements.
+ - apply NoDup_elements.
+ - intros. by rewrite !elem_of_elements, E.
Qed.
Global Instance collection_size_proper: Proper ((≡) ==> (=)) (@size C _).
Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
@@ -45,9 +45,9 @@ Lemma size_singleton (x : A) : size {[ x ]} = 1.
Proof.
change (length (elements {[ x ]}) = length [x]).
apply Permutation_length, NoDup_Permutation.
- * apply NoDup_elements.
- * apply NoDup_singleton.
- * intros y.
+ - apply NoDup_elements.
+ - apply NoDup_singleton.
+ - intros y.
by rewrite elem_of_elements, elem_of_singleton, elem_of_list_singleton.
Qed.
Lemma size_singleton_inv X x y : size X = 1 → x ∈ X → y ∈ X → x = y.
@@ -59,8 +59,8 @@ Qed.
Lemma collection_choose_or_empty X : (∃ x, x ∈ X) ∨ X ≡ ∅.
Proof.
destruct (elements X) as [|x l] eqn:HX; [right|left].
- * apply equiv_empty; intros x. by rewrite <-elem_of_elements, HX, elem_of_nil.
- * exists x. rewrite <-elem_of_elements, HX. by left.
+ - apply equiv_empty; intros x. by rewrite <-elem_of_elements, HX, elem_of_nil.
+ - exists x. rewrite <-elem_of_elements, HX. by left.
Qed.
Lemma collection_choose X : X ≢ ∅ → ∃ x, x ∈ X.
Proof. intros. by destruct (collection_choose_or_empty X). Qed.
@@ -75,17 +75,17 @@ Lemma size_1_elem_of X : size X = 1 → ∃ x, X ≡ {[ x ]}.
Proof.
intros E. destruct (size_pos_elem_of X); auto with lia.
exists x. apply elem_of_equiv. split.
- * rewrite elem_of_singleton. eauto using size_singleton_inv.
- * solve_elem_of.
+ - rewrite elem_of_singleton. eauto using size_singleton_inv.
+ - solve_elem_of.
Qed.
Lemma size_union X Y : X ∩ Y ≡ ∅ → size (X ∪ Y) = size X + size Y.
Proof.
intros [E _]. unfold size, collection_size. simpl. rewrite <-app_length.
apply Permutation_length, NoDup_Permutation.
- * apply NoDup_elements.
- * apply NoDup_app; repeat split; try apply NoDup_elements.
+ - apply NoDup_elements.
+ - apply NoDup_app; repeat split; try apply NoDup_elements.
intros x; rewrite !elem_of_elements; solve_elem_of.
- * intros. by rewrite elem_of_app, !elem_of_elements, elem_of_union.
+ - intros. by rewrite elem_of_app, !elem_of_elements, elem_of_union.
Qed.
Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100.
Proof.
@@ -129,9 +129,9 @@ Proof.
intros ? Hemp Hadd. apply well_founded_induction with (⊂).
{ apply collection_wf. }
intros X IH. destruct (collection_choose_or_empty X) as [[x ?]|HX].
- * rewrite (union_difference {[ x ]} X) by solve_elem_of.
+ - rewrite (union_difference {[ x ]} X) by solve_elem_of.
apply Hadd. solve_elem_of. apply IH; solve_elem_of.
- * by rewrite HX.
+ - by rewrite HX.
Qed.
Lemma collection_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B) :
Proper ((=) ==> (≡) ==> iff) P →
@@ -143,9 +143,9 @@ Proof.
{ intros help ?. apply help; [apply NoDup_elements|].
symmetry. apply elem_of_elements. }
induction 1 as [|x l ?? IH]; simpl.
- * intros X HX. setoid_rewrite elem_of_nil in HX.
+ - intros X HX. setoid_rewrite elem_of_nil in HX.
rewrite equiv_empty. done. solve_elem_of.
- * intros X HX. setoid_rewrite elem_of_cons in HX.
+ - intros X HX. setoid_rewrite elem_of_cons in HX.
rewrite (union_difference {[ x ]} X) by solve_elem_of.
apply Hadd. solve_elem_of. apply IH. solve_elem_of.
Qed.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 2746183b..77aea823 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -121,9 +121,9 @@ Section setoid.
Global Instance map_equivalence : Equivalence ((≡) : relation (M A)).
Proof.
split.
- * by intros m i.
- * by intros m1 m2 ? i.
- * by intros m1 m2 m3 ?? i; transitivity (m2 !! i).
+ - by intros m i.
+ - by intros m1 m2 ? i.
+ - by intros m1 m2 m3 ?? i; transitivity (m2 !! i).
Qed.
Global Instance lookup_proper (i : K) :
Proper ((≡) ==> (≡)) (lookup (M:=M A) i).
@@ -258,9 +258,9 @@ Proof.
{ by rewrite lookup_partial_alter_ne,
!lookup_partial_alter, lookup_partial_alter_ne. }
destruct (decide (jj = i)) as [->|?].
- * by rewrite lookup_partial_alter,
+ - by rewrite lookup_partial_alter,
!lookup_partial_alter_ne, lookup_partial_alter by congruence.
- * by rewrite !lookup_partial_alter_ne by congruence.
+ - by rewrite !lookup_partial_alter_ne by congruence.
Qed.
Lemma partial_alter_self_alt {A} (m : M A) i x :
x = m !! i → partial_alter (λ _, x) i m = m.
@@ -307,8 +307,8 @@ Lemma lookup_alter_Some {A} (f : A → A) m i j y :
(i = j ∧ ∃ x, m !! j = Some x ∧ y = f x) ∨ (i ≠j ∧ m !! j = Some y).
Proof.
destruct (decide (i = j)) as [->|?].
- * rewrite lookup_alter. naive_solver (simplify_option_equality; eauto).
- * rewrite lookup_alter_ne by done. naive_solver.
+ - rewrite lookup_alter. naive_solver (simplify_option_equality; eauto).
+ - rewrite lookup_alter_ne by done. naive_solver.
Qed.
Lemma lookup_alter_None {A} (f : A → A) m i j :
alter f i m !! j = None ↔ m !! j = None.
@@ -333,9 +333,9 @@ Lemma lookup_delete_Some {A} (m : M A) i j y :
delete i m !! j = Some y ↔ i ≠j ∧ m !! j = Some y.
Proof.
split.
- * destruct (decide (i = j)) as [->|?];
+ - destruct (decide (i = j)) as [->|?];
rewrite ?lookup_delete, ?lookup_delete_ne; intuition congruence.
- * intros [??]. by rewrite lookup_delete_ne.
+ - intros [??]. by rewrite lookup_delete_ne.
Qed.
Lemma lookup_delete_is_Some {A} (m : M A) i j :
is_Some (delete i m !! j) ↔ i ≠j ∧ is_Some (m !! j).
@@ -412,9 +412,9 @@ Lemma lookup_insert_Some {A} (m : M A) i j x y :
<[i:=x]>m !! j = Some y ↔ (i = j ∧ x = y) ∨ (i ≠j ∧ m !! j = Some y).
Proof.
split.
- * destruct (decide (i = j)) as [->|?];
+ - destruct (decide (i = j)) as [->|?];
rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence.
- * intros [[-> ->]|[??]]; [apply lookup_insert|]. by rewrite lookup_insert_ne.
+ - intros [[-> ->]|[??]]; [apply lookup_insert|]. by rewrite lookup_insert_ne.
Qed.
Lemma lookup_insert_is_Some {A} (m : M A) i j x :
is_Some (<[i:=x]>m !! j) ↔ i = j ∨ i ≠j ∧ is_Some (m !! j).
@@ -435,8 +435,8 @@ Lemma insert_included {A} R `{!Reflexive R} (m : M A) i x :
(∀ y, m !! i = Some y → R y x) → map_included R m (<[i:=x]>m).
Proof.
intros ? j; destruct (decide (i = j)) as [->|].
- * rewrite lookup_insert. destruct (m !! j); simpl; eauto.
- * rewrite lookup_insert_ne by done. by destruct (m !! j); simpl.
+ - rewrite lookup_insert. destruct (m !! j); simpl; eauto.
+ - rewrite lookup_insert_ne by done. by destruct (m !! j); simpl.
Qed.
Lemma insert_subseteq {A} (m : M A) i x : m !! i = None → m ⊆ <[i:=x]>m.
Proof. apply partial_alter_subseteq. Qed.
@@ -462,8 +462,8 @@ Lemma delete_insert_subseteq {A} (m1 m2 : M A) i x :
Proof.
rewrite !map_subseteq_spec.
intros Hix Hi j y Hj. destruct (decide (i = j)) as [->|?].
- * rewrite lookup_insert. congruence.
- * rewrite lookup_insert_ne by done. apply Hi. by rewrite lookup_delete_ne.
+ - rewrite lookup_insert. congruence.
+ - rewrite lookup_insert_ne by done. apply Hi. by rewrite lookup_delete_ne.
Qed.
Lemma insert_delete_subset {A} (m1 m2 : M A) i x :
m1 !! i = None → <[i:=x]> m1 ⊂ m2 → m1 ⊂ delete i m2.
@@ -477,10 +477,10 @@ Lemma insert_subset_inv {A} (m1 m2 : M A) i x :
∃ m2', m2 = <[i:=x]>m2' ∧ m1 ⊂ m2' ∧ m2' !! i = None.
Proof.
intros Hi Hm1m2. exists (delete i m2). split_ands.
- * rewrite insert_delete. done. eapply lookup_weaken, strict_include; eauto.
+ - rewrite insert_delete. done. eapply lookup_weaken, strict_include; eauto.
by rewrite lookup_insert.
- * eauto using insert_delete_subset.
- * by rewrite lookup_delete.
+ - eauto using insert_delete_subset.
+ - by rewrite lookup_delete.
Qed.
Lemma insert_empty {A} i (x : A) : <[i:=x]>∅ = {[i := x]}.
Proof. done. Qed.
@@ -510,8 +510,8 @@ Qed.
Lemma alter_singleton {A} (f : A → A) i x : alter f i {[i := x]} = {[i := f x]}.
Proof.
intros. apply map_eq. intros i'. destruct (decide (i = i')) as [->|?].
- * by rewrite lookup_alter, !lookup_singleton.
- * by rewrite lookup_alter_ne, !lookup_singleton_ne.
+ - by rewrite lookup_alter, !lookup_singleton.
+ - by rewrite lookup_alter_ne, !lookup_singleton_ne.
Qed.
Lemma alter_singleton_ne {A} (f : A → A) i j x :
i ≠j → alter f i {[j := x]} = {[j := x]}.
@@ -528,15 +528,15 @@ Proof. apply map_empty; intros i. by rewrite lookup_omap, lookup_empty. Qed.
Lemma fmap_insert {A B} (f: A → B) m i x: f <$> <[i:=x]>m = <[i:=f x]>(f <$> m).
Proof.
apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
- * by rewrite lookup_fmap, !lookup_insert.
- * by rewrite lookup_fmap, !lookup_insert_ne, lookup_fmap by done.
+ - by rewrite lookup_fmap, !lookup_insert.
+ - by rewrite lookup_fmap, !lookup_insert_ne, lookup_fmap by done.
Qed.
Lemma omap_insert {A B} (f : A → option B) m i x y :
f x = Some y → omap f (<[i:=x]>m) = <[i:=y]>(omap f m).
Proof.
intros; apply map_eq; intros i'; destruct (decide (i' = i)) as [->|].
- * by rewrite lookup_omap, !lookup_insert.
- * by rewrite lookup_omap, !lookup_insert_ne, lookup_omap by done.
+ - by rewrite lookup_omap, !lookup_insert.
+ - by rewrite lookup_omap, !lookup_insert_ne, lookup_omap by done.
Qed.
Lemma map_fmap_singleton {A B} (f : A → B) i x : f <$> {[i := x]} = {[i := f x]}.
Proof.
@@ -585,8 +585,8 @@ Proof.
setoid_rewrite elem_of_cons.
intros [?|?] Hdup; simplify_equality; [by rewrite lookup_insert|].
destruct (decide (i = j)) as [->|].
- * rewrite lookup_insert; f_equal; eauto.
- * rewrite lookup_insert_ne by done; eauto.
+ - rewrite lookup_insert; f_equal; eauto.
+ - rewrite lookup_insert_ne by done; eauto.
Qed.
Lemma elem_of_map_of_list_1 {A} (l : list (K * A)) i x :
NoDup (l.*1) → (i,x) ∈ l → map_of_list l !! i = Some x.
@@ -617,8 +617,8 @@ Lemma not_elem_of_map_of_list_2 {A} (l : list (K * A)) i :
Proof.
induction l as [|[j y] l IH]; csimpl; [rewrite elem_of_nil; tauto|].
rewrite elem_of_cons. destruct (decide (i = j)); simplify_equality.
- * by rewrite lookup_insert.
- * by rewrite lookup_insert_ne; intuition.
+ - by rewrite lookup_insert.
+ - by rewrite lookup_insert_ne; intuition.
Qed.
Lemma not_elem_of_map_of_list {A} (l : list (K * A)) i :
i ∉ l.*1 ↔ map_of_list l !! i = None.
@@ -665,11 +665,11 @@ Lemma map_to_list_insert {A} (m : M A) i x :
m !! i = None → map_to_list (<[i:=x]>m) ≡ₚ (i,x) :: map_to_list m.
Proof.
intros. apply map_of_list_inj; csimpl.
- * apply NoDup_fst_map_to_list.
- * constructor; auto using NoDup_fst_map_to_list.
+ - apply NoDup_fst_map_to_list.
+ - constructor; auto using NoDup_fst_map_to_list.
rewrite elem_of_list_fmap. intros [[??] [? Hlookup]]; subst; simpl in *.
rewrite elem_of_map_to_list in Hlookup. congruence.
- * by rewrite !map_of_to_list.
+ - by rewrite !map_of_to_list.
Qed.
Lemma map_of_list_nil {A} : map_of_list (@nil (K * A)) = ∅.
Proof. done. Qed.
@@ -702,13 +702,13 @@ Lemma lookup_imap {A B} (f : K → A → option B) m i :
map_imap f m !! i = m !! i ≫= f i.
Proof.
unfold map_imap; destruct (m !! i ≫= f i) as [y|] eqn:Hi; simpl.
- * destruct (m !! i) as [x|] eqn:?; simplify_equality'.
+ - destruct (m !! i) as [x|] eqn:?; simplify_equality'.
apply elem_of_map_of_list_1_help.
{ apply elem_of_list_omap; exists (i,x); split;
[by apply elem_of_map_to_list|by simplify_option_equality]. }
intros y'; rewrite elem_of_list_omap; intros ([i' x']&Hi'&?).
by rewrite elem_of_map_to_list in Hi'; simplify_option_equality.
- * apply not_elem_of_map_of_list; rewrite elem_of_list_fmap.
+ - apply not_elem_of_map_of_list; rewrite elem_of_list_fmap.
intros ([i' x]&->&Hi'); simplify_equality'.
rewrite elem_of_list_omap in Hi'; destruct Hi' as ([j y]&Hj&?).
rewrite elem_of_map_to_list in Hj; simplify_option_equality.
@@ -726,8 +726,8 @@ Proof.
by intros (?&?&?&?&?); simplify_option_equality. }
unfold map_of_collection; rewrite <-elem_of_map_of_list by done.
rewrite elem_of_list_omap. setoid_rewrite elem_of_elements; split.
- * intros (?&?&?); simplify_option_equality; eauto.
- * intros [??]; exists i; simplify_option_equality; eauto.
+ - intros (?&?&?); simplify_option_equality; eauto.
+ - intros [??]; exists i; simplify_option_equality; eauto.
Qed.
(** ** Induction principles *)
@@ -741,8 +741,8 @@ Proof.
{ apply map_to_list_empty_inv_alt in Hml. by subst. }
inversion_clear Hnodup.
apply map_to_list_insert_inv in Hml; subst m. apply Hins.
- * by apply not_elem_of_map_of_list_1.
- * apply IH; auto using map_to_of_list.
+ - by apply not_elem_of_map_of_list_1.
+ - apply IH; auto using map_to_of_list.
Qed.
Lemma map_to_list_length {A} (m1 m2 : M A) :
m1 ⊂ m2 → length (map_to_list m1) < length (map_to_list m2).
@@ -759,8 +759,8 @@ Qed.
Lemma map_wf {A} : wf (strict (@subseteq (M A) _)).
Proof.
apply (wf_projected (<) (length ∘ map_to_list)).
- * by apply map_to_list_length.
- * by apply lt_wf.
+ - by apply map_to_list_length.
+ - by apply lt_wf.
Qed.
(** ** Properties of the [map_Forall] predicate *)
@@ -770,8 +770,8 @@ Context {A} (P : K → A → Prop).
Lemma map_Forall_to_list m : map_Forall P m ↔ Forall (curry P) (map_to_list m).
Proof.
rewrite Forall_forall. split.
- * intros Hforall [i x]. rewrite elem_of_map_to_list. by apply (Hforall i x).
- * intros Hforall i x. rewrite <-elem_of_map_to_list. by apply (Hforall (i,x)).
+ - intros Hforall [i x]. rewrite elem_of_map_to_list. by apply (Hforall i x).
+ - intros Hforall i x. rewrite <-elem_of_map_to_list. by apply (Hforall (i,x)).
Qed.
Lemma map_Forall_empty : map_Forall P ∅.
Proof. intros i x. by rewrite lookup_empty. Qed.
@@ -874,24 +874,24 @@ Lemma partial_alter_merge g g1 g2 m1 m2 i :
merge f (partial_alter g1 i m1) (partial_alter g2 i m2).
Proof.
intro. apply map_eq. intros j. destruct (decide (i = j)); subst.
- * by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _).
- * by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _).
+ - by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _).
+ - by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _).
Qed.
Lemma partial_alter_merge_l g g1 m1 m2 i :
g (f (m1 !! i) (m2 !! i)) = f (g1 (m1 !! i)) (m2 !! i) →
partial_alter g i (merge f m1 m2) = merge f (partial_alter g1 i m1) m2.
Proof.
intro. apply map_eq. intros j. destruct (decide (i = j)); subst.
- * by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _).
- * by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _).
+ - by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _).
+ - by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _).
Qed.
Lemma partial_alter_merge_r g g2 m1 m2 i :
g (f (m1 !! i) (m2 !! i)) = f (m1 !! i) (g2 (m2 !! i)) →
partial_alter g i (merge f m1 m2) = merge f m1 (partial_alter g2 i m2).
Proof.
intro. apply map_eq. intros j. destruct (decide (i = j)); subst.
- * by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _).
- * by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _).
+ - by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _).
+ - by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _).
Qed.
Lemma insert_merge m1 m2 i x y z :
f (Some y) (Some z) = Some x →
@@ -928,10 +928,10 @@ Lemma map_relation_alt (m1 : M A) (m2 : M B) :
map_relation R P Q m1 m2 ↔ map_Forall (λ _, Is_true) (merge f m1 m2).
Proof.
split.
- * intros Hm i P'; rewrite lookup_merge by done; intros.
+ - intros Hm i P'; rewrite lookup_merge by done; intros.
specialize (Hm i). destruct (m1 !! i), (m2 !! i);
simplify_equality'; auto using bool_decide_pack.
- * intros Hm i. specialize (Hm i). rewrite lookup_merge in Hm by done.
+ - intros Hm i. specialize (Hm i). rewrite lookup_merge in Hm by done.
destruct (m1 !! i), (m2 !! i); simplify_equality'; auto;
by eapply bool_decide_unpack, Hm.
Qed.
@@ -950,10 +950,10 @@ Lemma map_not_Forall2 (m1 : M A) (m2 : M B) :
∨ (∃ y, m1 !! i = None ∧ m2 !! i = Some y ∧ ¬Q y).
Proof.
split.
- * rewrite map_relation_alt, (map_not_Forall _). intros (i&?&Hm&?); exists i.
+ - rewrite map_relation_alt, (map_not_Forall _). intros (i&?&Hm&?); exists i.
rewrite lookup_merge in Hm by done.
destruct (m1 !! i), (m2 !! i); naive_solver auto 2 using bool_decide_pack.
- * unfold map_relation, option_relation.
+ - unfold map_relation, option_relation.
by intros [i[(x&y&?&?&?)|[(x&?&?&?)|(y&?&?&?)]]] Hm;
specialize (Hm i); simplify_option_equality.
Qed.
@@ -1003,9 +1003,9 @@ Proof. rewrite (symmetry_iff map_disjoint). apply map_disjoint_Some_l. Qed.
Lemma map_disjoint_singleton_l {A} (m: M A) i x : {[i:=x]} ⊥ₘ m ↔ m !! i = None.
Proof.
split; [|rewrite !map_disjoint_spec].
- * intro. apply (map_disjoint_Some_l {[i := x]} _ _ x);
+ - intro. apply (map_disjoint_Some_l {[i := x]} _ _ x);
auto using lookup_singleton.
- * intros ? j y1 y2. destruct (decide (i = j)) as [->|].
+ - intros ? j y1 y2. destruct (decide (i = j)) as [->|].
+ rewrite lookup_singleton. intuition congruence.
+ by rewrite lookup_singleton_ne.
Qed.
@@ -1238,8 +1238,8 @@ Proof.
apply map_eq. intros j. apply option_eq. intros y.
rewrite lookup_union_Some_raw.
destruct (decide (i = j)); subst.
- * rewrite !lookup_singleton, lookup_insert. intuition congruence.
- * rewrite !lookup_singleton_ne, lookup_insert_ne; intuition congruence.
+ - rewrite !lookup_singleton, lookup_insert. intuition congruence.
+ - rewrite !lookup_singleton_ne, lookup_insert_ne; intuition congruence.
Qed.
Lemma insert_union_singleton_r {A} (m : M A) i x :
m !! i = None → <[i:=x]>m = m ∪ {[i := x]}.
@@ -1290,8 +1290,8 @@ Lemma map_disjoint_union_list_l {A} (ms : list (M A)) (m : M A) :
⋃ ms ⊥ₘ m ↔ Forall (.⊥ₘ m) ms.
Proof.
split.
- * induction ms; simpl; rewrite ?map_disjoint_union_l; intuition.
- * induction 1; simpl; [apply map_disjoint_empty_l |].
+ - induction ms; simpl; rewrite ?map_disjoint_union_l; intuition.
+ - induction 1; simpl; [apply map_disjoint_empty_l |].
by rewrite map_disjoint_union_l.
Qed.
Lemma map_disjoint_union_list_r {A} (ms : list (M A)) (m : M A) :
@@ -1342,8 +1342,8 @@ Lemma map_disjoint_of_list_l {A} (m : M A) ixs :
map_of_list ixs ⊥ₘ m ↔ Forall (λ ix, m !! ix.1 = None) ixs.
Proof.
split.
- * induction ixs; simpl; rewrite ?map_disjoint_insert_l in *; intuition.
- * induction 1; simpl; [apply map_disjoint_empty_l|].
+ - induction ixs; simpl; rewrite ?map_disjoint_insert_l in *; intuition.
+ - induction 1; simpl; [apply map_disjoint_empty_l|].
rewrite map_disjoint_insert_l. auto.
Qed.
Lemma map_disjoint_of_list_r {A} (m : M A) ixs :
diff --git a/theories/finite.v b/theories/finite.v
index 11586869..26aac4f7 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -30,8 +30,8 @@ Proof.
destruct finA as [xs Hxs HA]; unfold encode_nat, encode, card; simpl.
rewrite Nat2Pos.id by done; simpl.
destruct (list_find _ xs) as [[i y]|] eqn:?; simpl.
- * destruct (list_find_Some (x =) xs i y); eauto using lookup_lt_Some.
- * destruct xs; simpl. exfalso; eapply not_elem_of_nil, (HA x). lia.
+ - destruct (list_find_Some (x =) xs i y); eauto using lookup_lt_Some.
+ - destruct xs; simpl. exfalso; eapply not_elem_of_nil, (HA x). lia.
Qed.
Lemma encode_decode A `{finA: Finite A} i :
i < card A → ∃ x, decode_nat i = Some x ∧ encode_nat x = i.
@@ -80,8 +80,8 @@ 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 contains_Permutation_length_eq.
- * by rewrite fmap_length.
- * by apply finite_inj_contains.
+ - by rewrite fmap_length.
+ - by apply finite_inj_contains.
Qed.
Lemma finite_inj_surj `{Finite A} `{Finite B} (f : A → B)
`{!Inj (=) (=) f} : card A = card B → Surj (=) f.
@@ -103,20 +103,20 @@ Lemma finite_inj A `{Finite A} B `{Finite B} :
card A ≤ card B ↔ ∃ f : A → B, Inj (=) (=) f.
Proof.
split.
- * intros. destruct (decide (card A = 0)) as [HA|?].
+ - intros. destruct (decide (card A = 0)) as [HA|?].
{ 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 <-(fmap_length f).
by apply contains_length, (finite_inj_contains f).
Qed.
Lemma finite_bijective A `{Finite A} B `{Finite B} :
card A = card B ↔ ∃ f : A → B, Inj (=) (=) f ∧ Surj (=) f.
Proof.
split.
- * intros; destruct (proj1 (finite_inj A B)) as [f ?]; auto with lia.
+ - intros; destruct (proj1 (finite_inj A B)) as [f ?]; auto with lia.
exists f; auto using (finite_inj_surj f).
- * intros (f&?&?). apply (anti_symm (≤)); apply finite_inj.
+ - intros (f&?&?). apply (anti_symm (≤)); apply finite_inj.
+ by exists f.
+ destruct (surj_cancel f) as (g&?); eauto using cancel_inj.
Qed.
@@ -193,8 +193,8 @@ Program Instance option_finite `{Finite A} : Finite (option A) :=
{| enum := None :: Some <$> enum A |}.
Next Obligation.
constructor.
- * rewrite elem_of_list_fmap. by intros (?&?&?).
- * apply (NoDup_fmap_2 _); auto using NoDup_enum.
+ - rewrite elem_of_list_fmap. by intros (?&?&?).
+ - apply (NoDup_fmap_2 _); auto using NoDup_enum.
Qed.
Next Obligation.
intros ??? [x|]; [right|left]; auto.
@@ -221,9 +221,9 @@ Program Instance sum_finite `{Finite A, Finite B} : Finite (A + B)%type :=
{| enum := (inl <$> enum A) ++ (inr <$> enum B) |}.
Next Obligation.
intros. apply NoDup_app; split_ands.
- * apply (NoDup_fmap_2 _). by apply NoDup_enum.
- * intro. rewrite !elem_of_list_fmap. intros (?&?&?) (?&?&?); congruence.
- * apply (NoDup_fmap_2 _). by apply NoDup_enum.
+ - apply (NoDup_fmap_2 _). by apply NoDup_enum.
+ - intro. rewrite !elem_of_list_fmap. intros (?&?&?) (?&?&?); congruence.
+ - apply (NoDup_fmap_2 _). by apply NoDup_enum.
Qed.
Next Obligation.
intros ?????? [x|y]; rewrite elem_of_app, !elem_of_list_fmap;
@@ -238,20 +238,20 @@ Next Obligation.
intros ??????. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl.
{ constructor. }
apply NoDup_app; split_ands.
- * by apply (NoDup_fmap_2 _), NoDup_enum.
- * intros [? y]. rewrite elem_of_list_fmap. intros (?&?&?); simplify_equality.
+ - by apply (NoDup_fmap_2 _), NoDup_enum.
+ - intros [? y]. rewrite elem_of_list_fmap. intros (?&?&?); simplify_equality.
clear IH. induction Hxs as [|x' xs ?? IH]; simpl.
{ rewrite elem_of_nil. tauto. }
rewrite elem_of_app, elem_of_list_fmap.
intros [(?&?&?)|?]; simplify_equality.
+ destruct Hx. by left.
+ destruct IH. by intro; destruct Hx; right. auto.
- * done.
+ - done.
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.
+ - rewrite elem_of_app, !elem_of_list_fmap. eauto using @elem_of_enum.
+ - rewrite elem_of_app; eauto.
Qed.
Lemma prod_card `{Finite A} `{Finite B} : card (A * B) = card A * card B.
Proof.
@@ -272,13 +272,13 @@ Next Obligation.
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_ands.
- * by apply (NoDup_fmap_2 _).
- * intros [k1 Hk1]. clear Hxs IH. rewrite elem_of_list_fmap.
+ - by apply (NoDup_fmap_2 _).
+ - intros [k1 Hk1]. clear Hxs IH. rewrite elem_of_list_fmap.
intros ([k2 Hk2]&?&?) Hxk2; simplify_equality'. 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_equality'; auto.
- * apply IH.
+ - apply IH.
Qed.
Next Obligation.
intros ???? [l Hl]. revert l Hl.
@@ -286,9 +286,9 @@ Next Obligation.
{ 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'.
+ - rewrite elem_of_app, elem_of_list_fmap. left. injection Hl. intros Hl'.
eexists (l↾Hl'). split. by apply (sig_eq_pi _). done.
- * rewrite elem_of_app. eauto.
+ - rewrite elem_of_app. eauto.
Qed.
Lemma list_card `{Finite A} n : card { l | length l = n } = card A ^ n.
Proof.
diff --git a/theories/gmap.v b/theories/gmap.v
index fe4a18fa..ee040a24 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -37,8 +37,8 @@ Lemma gmap_partial_alter_wf `{Countable K} {A} (f : option A → option A) m i :
gmap_wf m → gmap_wf (partial_alter f (encode i) m).
Proof.
intros Hm p x. destruct (decide (encode i = p)) as [<-|?].
- * rewrite decode_encode; eauto.
- * rewrite lookup_partial_alter_ne by done. by apply Hm.
+ - rewrite decode_encode; eauto.
+ - rewrite lookup_partial_alter_ne by done. by apply Hm.
Qed.
Instance gmap_partial_alter `{Countable K} {A} :
PartialAlter K A (gmap K A) := λ f i m,
@@ -78,7 +78,7 @@ Instance gmap_to_list `{Countable K} {A} : FinMapToList K A (gmap K A) := λ m,
Instance gmap_finmap `{Countable K} : FinMap K (gmap K).
Proof.
split.
- * unfold lookup; intros A [m1 Hm1] [m2 Hm2] Hm.
+ - unfold lookup; intros A [m1 Hm1] [m2 Hm2] Hm.
apply gmap_eq, map_eq; intros i; simpl in *.
apply bool_decide_unpack in Hm1; apply bool_decide_unpack in Hm2.
apply option_eq; intros x; split; intros Hi.
@@ -86,12 +86,12 @@ Proof.
by destruct (decode i); simplify_equality'; rewrite <-Hm.
+ pose proof (Hm2 i x Hi); simpl in *.
by destruct (decode i); simplify_equality'; rewrite Hm.
- * done.
- * intros A f [m Hm] i; apply (lookup_partial_alter f m).
- * intros A f [m Hm] i j Hs; apply (lookup_partial_alter_ne f m).
+ - done.
+ - intros A f [m Hm] i; apply (lookup_partial_alter f m).
+ - intros A f [m Hm] i j Hs; apply (lookup_partial_alter_ne f m).
by contradict Hs; apply (inj encode).
- * intros A B f [m Hm] i; apply (lookup_fmap f m).
- * intros A [m Hm]; unfold map_to_list; simpl.
+ - intros A B f [m Hm] i; apply (lookup_fmap f m).
+ - intros A [m Hm]; unfold map_to_list; simpl.
apply bool_decide_unpack, map_Forall_to_list in Hm; revert Hm.
induction (NoDup_map_to_list m) as [|[p x] l Hpx];
inversion 1 as [|??? Hm']; simplify_equality'; [by constructor|].
@@ -99,15 +99,15 @@ Proof.
rewrite elem_of_list_omap; intros ([p' x']&?&?); simplify_equality'.
feed pose proof (proj1 (Forall_forall _ _) Hm' (p',x')); simpl in *; auto.
by destruct (decode p') as [i'|]; simplify_equality'.
- * intros A [m Hm] i x; unfold map_to_list, lookup; simpl.
+ - intros A [m Hm] i x; unfold map_to_list, lookup; simpl.
apply bool_decide_unpack in Hm; rewrite elem_of_list_omap; split.
+ intros ([p' x']&Hp'&?); apply elem_of_map_to_list in Hp'.
feed pose proof (Hm p' x'); simpl in *; auto.
by destruct (decode p') as [i'|] eqn:?; simplify_equality'.
+ intros; exists (encode i,x); simpl.
by rewrite elem_of_map_to_list, decode_encode.
- * intros A B f [m Hm] i; apply (lookup_omap f m).
- * intros A B C f ? [m1 Hm1] [m2 Hm2] i; unfold merge, lookup; simpl.
+ - intros A B f [m Hm] i; apply (lookup_omap f m).
+ - intros A B C f ? [m1 Hm1] [m2 Hm2] i; unfold merge, lookup; simpl.
set (f' o1 o2 := match o1, o2 with None,None => None | _, _ => f o1 o2 end).
by rewrite lookup_merge by done; destruct (m1 !! _), (m2 !! _).
Qed.
@@ -130,8 +130,8 @@ Instance gset_positive_fresh : Fresh positive (gset positive) := λ X,
Instance gset_positive_fresh_spec : FreshSpec positive (gset positive).
Proof.
split.
- * apply _.
- * by intros X Y; rewrite <-elem_of_equiv_L; intros ->.
- * intros [[m Hm]]; unfold fresh; simpl.
+ - apply _.
+ - by intros X Y; rewrite <-elem_of_equiv_L; intros ->.
+ - intros [[m Hm]]; unfold fresh; simpl.
by intros ?; apply (is_fresh (dom Pset m)), elem_of_dom_2 with ().
Qed.
diff --git a/theories/hashset.v b/theories/hashset.v
index c6f5e4ca..446abf38 100644
--- a/theories/hashset.v
+++ b/theories/hashset.v
@@ -63,12 +63,12 @@ Instance hashset_elems: Elements A (hashset hash) := λ m,
Global Instance: FinCollection A (hashset hash).
Proof.
split; [split; [split| |]| |].
- * intros ? (?&?&?); simplify_map_equality'.
- * unfold elem_of, hashset_elem_of, singleton, hashset_singleton; simpl.
+ - intros ? (?&?&?); simplify_map_equality'.
+ - unfold elem_of, hashset_elem_of, singleton, hashset_singleton; simpl.
intros x y. setoid_rewrite lookup_singleton_Some. split.
{ by intros (?&[? <-]&?); decompose_elem_of_list. }
intros ->; eexists [y]. by rewrite elem_of_list_singleton.
- * unfold elem_of, hashset_elem_of, union, hashset_union.
+ - unfold elem_of, hashset_elem_of, union, hashset_union.
intros [m1 Hm1] [m2 Hm2] x; simpl; setoid_rewrite lookup_union_with_Some.
split.
{ intros (?&[[]|[[]|(l&k&?&?&?)]]&Hx); simplify_equality'; eauto.
@@ -78,7 +78,7 @@ Proof.
exists (list_union l k). rewrite elem_of_list_union. naive_solver.
+ destruct (m1 !! hash x) as [l|]; eauto 6.
exists (list_union l k). rewrite elem_of_list_union. naive_solver.
- * unfold elem_of, hashset_elem_of, intersection, hashset_intersection.
+ - unfold elem_of, hashset_elem_of, intersection, hashset_intersection.
intros [m1 ?] [m2 ?] x; simpl.
setoid_rewrite lookup_intersection_with_Some. split.
{ intros (?&(l&k&?&?&?)&Hx); simplify_option_equality.
@@ -87,7 +87,7 @@ Proof.
by (by rewrite elem_of_list_intersection).
exists (list_intersection l k); split; [exists l, k|]; split_ands; auto.
by rewrite option_guard_True by eauto using elem_of_not_nil.
- * unfold elem_of, hashset_elem_of, intersection, hashset_intersection.
+ - unfold elem_of, hashset_elem_of, intersection, hashset_intersection.
intros [m1 ?] [m2 ?] x; simpl.
setoid_rewrite lookup_difference_with_Some. split.
{ intros (l'&[[??]|(l&k&?&?&?)]&Hx); simplify_option_equality;
@@ -97,13 +97,13 @@ Proof.
assert (x ∈ list_difference l k) by (by rewrite elem_of_list_difference).
exists (list_difference l k); split; [right; exists l,k|]; split_ands; auto.
by rewrite option_guard_True by eauto using elem_of_not_nil.
- * unfold elem_of at 2, hashset_elem_of, elements, hashset_elems.
+ - unfold elem_of at 2, hashset_elem_of, elements, hashset_elems.
intros [m Hm] x; simpl. setoid_rewrite elem_of_list_bind. split.
{ intros ([n l]&Hx&Hn); simpl in *; rewrite elem_of_map_to_list in Hn.
cut (hash x = n); [intros <-; eauto|].
eapply (Forall_forall (λ x, hash x = n) l); eauto. eapply Hm; eauto. }
intros (l&?&?). exists (hash x, l); simpl. by rewrite elem_of_map_to_list.
- * unfold elements, hashset_elems. intros [m Hm]; simpl.
+ - unfold elements, hashset_elems. intros [m Hm]; simpl.
rewrite map_Forall_to_list in Hm. generalize (NoDup_fst_map_to_list m).
induction Hm as [|[n l] m' [??]];
csimpl; inversion_clear 1 as [|?? Hn]; [constructor|].
@@ -152,10 +152,10 @@ Proof.
unfold remove_dups_fast; generalize (x1 :: x2 :: l); clear l; intros l.
generalize (λ x, hash x `mod` (2 * length l))%Z; intros f.
rewrite elem_of_elements; split.
- * revert x. induction l as [|y l IH]; intros x; simpl.
+ - revert x. induction l as [|y l IH]; intros x; simpl.
{ by rewrite elem_of_empty. }
rewrite elem_of_union, elem_of_singleton. intros [->|]; [left|right]; eauto.
- * induction 1; solve_elem_of.
+ - induction 1; solve_elem_of.
Qed.
Lemma NoDup_remove_dups_fast l : NoDup (remove_dups_fast l).
Proof.
diff --git a/theories/lexico.v b/theories/lexico.v
index 05c53138..f2a0f015 100644
--- a/theories/lexico.v
+++ b/theories/lexico.v
@@ -49,9 +49,9 @@ Instance prod_lexico_po `{Lexico A, Lexico B, !StrictOrder (@lexico A _)}
`{!StrictOrder (@lexico B _)} : StrictOrder (@lexico (A * B) _).
Proof.
split.
- * intros [x y]. apply prod_lexico_irreflexive.
+ - intros [x y]. apply prod_lexico_irreflexive.
by apply (irreflexivity lexico y).
- * intros [??] [??] [??] ??.
+ - intros [??] [??] [??] ??.
eapply prod_lexico_transitive; eauto. apply transitivity.
Qed.
Instance prod_lexico_trichotomyT `{Lexico A, tA : !TrichotomyT (@lexico A _)}
@@ -119,8 +119,8 @@ Instance list_lexico_po `{Lexico A, !StrictOrder (@lexico A _)} :
StrictOrder (@lexico (list A) _).
Proof.
split.
- * intros l. induction l. by intros ?. by apply prod_lexico_irreflexive.
- * intros l1. induction l1 as [|x1 l1]; intros [|x2 l2] [|x3 l3] ??; try done.
+ - intros l. induction l. by intros ?. by apply prod_lexico_irreflexive.
+ - intros l1. induction l1 as [|x1 l1]; intros [|x2 l2] [|x3 l3] ??; try done.
eapply prod_lexico_transitive; eauto.
Qed.
Instance list_lexico_trichotomy `{Lexico A, tA : !TrichotomyT (@lexico A _)} :
@@ -142,8 +142,8 @@ Instance sig_lexico_po `{Lexico A, !StrictOrder (@lexico A _)}
(P : A → Prop) `{∀ x, ProofIrrel (P x)} : StrictOrder (@lexico (sig P) _).
Proof.
unfold lexico, sig_lexico. split.
- * intros [x ?] ?. by apply (irreflexivity lexico x).
- * intros [x1 ?] [x2 ?] [x3 ?] ??. by transitivity x2.
+ - intros [x ?] ?. by apply (irreflexivity lexico x).
+ - intros [x1 ?] [x2 ?] [x3 ?] ??. by transitivity x2.
Qed.
Instance sig_lexico_trichotomy `{Lexico A, tA : !TrichotomyT (@lexico A _)}
(P : A → Prop) `{∀ x, ProofIrrel (P x)} : TrichotomyT (@lexico (sig P) _).
diff --git a/theories/list.v b/theories/list.v
index 0614f0ab..ec81c5f6 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -370,9 +370,9 @@ Section setoid.
Global Instance map_equivalence : Equivalence ((≡) : relation (list A)).
Proof.
split.
- * intros l; induction l; constructor; auto.
- * induction 1; constructor; auto.
- * intros l1 l2 l3 Hl; revert l3.
+ - intros l; induction l; constructor; auto.
+ - induction 1; constructor; auto.
+ - intros l1 l2 l3 Hl; revert l3.
induction Hl; inversion_clear 1; constructor; try etransitivity; eauto.
Qed.
Global Instance cons_proper : Proper ((≡) ==> (≡) ==> (≡)) (@cons A).
@@ -409,10 +409,10 @@ Proof. done. Qed.
Lemma list_eq l1 l2 : (∀ i, l1 !! i = l2 !! i) → l1 = l2.
Proof.
revert l2. induction l1; intros [|??] H.
- * done.
- * discriminate (H 0).
- * discriminate (H 0).
- * f_equal; [by injection (H 0)|]. apply (IHl1 _ $ λ i, H (S i)).
+ - done.
+ - discriminate (H 0).
+ - discriminate (H 0).
+ - f_equal; [by injection (H 0)|]. apply (IHl1 _ $ λ i, H (S i)).
Qed.
Global Instance list_eq_dec {dec : ∀ x y, Decision (x = y)} : ∀ l k,
Decision (l = k) := list_eq_dec dec.
@@ -455,10 +455,10 @@ Lemma list_eq_same_length l1 l2 n :
(∀ i x y, i < n → l1 !! i = Some x → l2 !! i = Some y → x = y) → l1 = l2.
Proof.
intros <- Hlen Hl; apply list_eq; intros i. destruct (l2 !! i) as [x|] eqn:Hx.
- * destruct (lookup_lt_is_Some_2 l1 i) as [y Hy].
+ - destruct (lookup_lt_is_Some_2 l1 i) as [y Hy].
{ rewrite Hlen; eauto using lookup_lt_Some. }
rewrite Hy; f_equal; apply (Hl i); eauto using lookup_lt_Some.
- * by rewrite lookup_ge_None, Hlen, <-lookup_ge_None.
+ - by rewrite lookup_ge_None, Hlen, <-lookup_ge_None.
Qed.
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.
@@ -472,10 +472,10 @@ Lemma lookup_app_Some l1 l2 i x :
l1 !! i = Some x ∨ length l1 ≤ i ∧ l2 !! (i - length l1) = Some x.
Proof.
split.
- * revert i. induction l1 as [|y l1 IH]; intros [|i] ?;
+ - revert i. induction l1 as [|y l1 IH]; intros [|i] ?;
simplify_equality'; auto with lia.
destruct (IH i) as [?|[??]]; auto with lia.
- * intros [?|[??]]; auto using lookup_app_l_Some. by rewrite lookup_app_r.
+ - intros [?|[??]]; auto using lookup_app_l_Some. by rewrite lookup_app_r.
Qed.
Lemma list_lookup_middle l1 l2 x n :
n = length l1 → (l1 ++ x :: l2) !! n = Some x.
@@ -505,10 +505,10 @@ Lemma list_lookup_insert_Some l i x j y :
Proof.
destruct (decide (i = j)) as [->|];
[split|rewrite list_lookup_insert_ne by done; tauto].
- * intros Hy. assert (j < length l).
+ - intros Hy. assert (j < length l).
{ rewrite <-(insert_length l j x); eauto using lookup_lt_Some. }
rewrite list_lookup_insert in Hy by done; naive_solver.
- * intros [(?&?&?)|[??]]; rewrite ?list_lookup_insert; naive_solver.
+ - intros [(?&?&?)|[??]]; rewrite ?list_lookup_insert; naive_solver.
Qed.
Lemma list_insert_commute l i j x y :
i ≠j → <[i:=x]>(<[j:=y]>l) = <[j:=y]>(<[i:=x]>l).
@@ -517,8 +517,8 @@ 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]]; simplify_equality'.
- * by exists 1, x1.
- * by exists 0, x0.
+ - by exists 1, x1.
+ - by exists 0, x0.
Qed.
Lemma alter_app_l f l1 l2 i :
i < length l1 → alter f i (l1 ++ l2) = alter f i l1 ++ l2.
@@ -594,10 +594,10 @@ Proof.
destruct (decide (i + length k ≤ j)).
{ rewrite list_lookup_inserts_ge by done; intuition lia. }
split.
- * intros Hy. assert (j < length l).
+ - intros Hy. assert (j < length l).
{ rewrite <-(inserts_length l i k); eauto using lookup_lt_Some. }
rewrite list_lookup_inserts in Hy by lia. intuition lia.
- * intuition. by rewrite list_lookup_inserts by lia.
+ - intuition. by rewrite list_lookup_inserts by lia.
Qed.
Lemma list_insert_inserts_lt l i j x k :
i < j → <[i:=x]>(list_inserts j k l) = list_inserts j k (<[i:=x]>l).
@@ -622,8 +622,8 @@ Proof. rewrite elem_of_cons. tauto. Qed.
Lemma elem_of_app l1 l2 x : x ∈ l1 ++ l2 ↔ x ∈ l1 ∨ x ∈ l2.
Proof.
induction l1.
- * split; [by right|]. intros [Hx|]; [|done]. by destruct (elem_of_nil x).
- * simpl. rewrite !elem_of_cons, IHl1. tauto.
+ - split; [by right|]. intros [Hx|]; [|done]. by destruct (elem_of_nil x).
+ - simpl. rewrite !elem_of_cons, IHl1. tauto.
Qed.
Lemma not_elem_of_app l1 l2 x : x ∉ l1 ++ l2 ↔ x ∉ l1 ∧ x ∉ l2.
Proof. rewrite elem_of_app. tauto. Qed.
@@ -651,9 +651,9 @@ Lemma elem_of_list_omap {B} (f : A → option B) l (y : B) :
y ∈ omap f l ↔ ∃ x, x ∈ l ∧ f x = Some y.
Proof.
split.
- * induction l as [|x l]; csimpl; repeat case_match; inversion 1; subst;
+ - induction l as [|x l]; csimpl; repeat case_match; inversion 1; subst;
setoid_rewrite elem_of_cons; naive_solver.
- * intros (x&Hx&?). by induction Hx; csimpl; repeat case_match;
+ - intros (x&Hx&?). by induction Hx; csimpl; repeat case_match;
simplify_equality; try constructor; auto.
Qed.
@@ -671,17 +671,17 @@ Proof. constructor. apply not_elem_of_nil. constructor. Qed.
Lemma NoDup_app l k : NoDup (l ++ k) ↔ NoDup l ∧ (∀ x, x ∈ l → x ∉ k) ∧ NoDup k.
Proof.
induction l; simpl.
- * rewrite NoDup_nil. setoid_rewrite elem_of_nil. naive_solver.
- * rewrite !NoDup_cons.
+ - rewrite NoDup_nil. setoid_rewrite elem_of_nil. naive_solver.
+ - 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 | |].
- * by rewrite !NoDup_nil.
- * by rewrite !NoDup_cons, IH, Hlk.
- * rewrite !NoDup_cons, !elem_of_cons. intuition.
- * intuition.
+ - by rewrite !NoDup_nil.
+ - by rewrite !NoDup_cons, IH, Hlk.
+ - rewrite !NoDup_cons, !elem_of_cons. intuition.
+ - intuition.
Qed.
Lemma NoDup_lookup l i j x :
NoDup l → l !! i = Some x → l !! j = Some x → i = j.
@@ -696,9 +696,9 @@ Lemma NoDup_alt l :
Proof.
split; eauto using NoDup_lookup.
induction l as [|x l IH]; intros Hl; constructor.
- * rewrite elem_of_list_lookup. intros [i ?].
+ - 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 (inj S), (Hl (S i) (S j) x').
+ - apply IH. intros i j x' ??. by apply (inj S), (Hl (S i) (S j) x').
Qed.
Section no_dup_dec.
@@ -740,9 +740,9 @@ Section list_set.
Lemma NoDup_list_difference l k : NoDup l → NoDup (list_difference l k).
Proof.
induction 1; simpl; try case_decide.
- * constructor.
- * done.
- * constructor. rewrite elem_of_list_difference; intuition. done.
+ - constructor.
+ - done.
+ - constructor. rewrite elem_of_list_difference; intuition. done.
Qed.
Lemma elem_of_list_union l k x : x ∈ list_union l k ↔ x ∈ l ∨ x ∈ k.
Proof.
@@ -752,9 +752,9 @@ Section list_set.
Lemma NoDup_list_union l k : NoDup l → NoDup k → NoDup (list_union l k).
Proof.
intros. apply NoDup_app. repeat split.
- * by apply NoDup_list_difference.
- * intro. rewrite elem_of_list_difference. intuition.
- * done.
+ - by apply NoDup_list_difference.
+ - intro. rewrite elem_of_list_difference. intuition.
+ - done.
Qed.
Lemma elem_of_list_intersection l k x :
x ∈ list_intersection l k ↔ x ∈ l ∧ x ∈ k.
@@ -765,23 +765,23 @@ Section list_set.
Lemma NoDup_list_intersection l k : NoDup l → NoDup (list_intersection l k).
Proof.
induction 1; simpl; try case_decide.
- * constructor.
- * constructor. rewrite elem_of_list_intersection; intuition. done.
- * done.
+ - constructor.
+ - constructor. rewrite elem_of_list_intersection; intuition. done.
+ - done.
Qed.
Lemma elem_of_list_intersection_with f l k x :
x ∈ list_intersection_with f l k ↔ ∃ x1 x2,
x1 ∈ l ∧ x2 ∈ k ∧ f x1 x2 = Some x.
Proof.
split.
- * induction l as [|x1 l IH]; simpl; [by rewrite elem_of_nil|].
+ - induction l as [|x1 l IH]; simpl; [by rewrite elem_of_nil|].
intros Hx. setoid_rewrite elem_of_cons.
cut ((∃ x2, x2 ∈ k ∧ f x1 x2 = Some x)
∨ x ∈ list_intersection_with f l k); [naive_solver|].
clear IH. revert Hx. generalize (list_intersection_with f l k).
induction k; simpl; [by auto|].
case_match; setoid_rewrite elem_of_cons; naive_solver.
- * intros (x1&x2&Hx1&Hx2&Hx). induction Hx1 as [x1|x1 ? l ? IH]; simpl.
+ - intros (x1&x2&Hx1&Hx2&Hx). induction Hx1 as [x1|x1 ? l ? IH]; simpl.
+ generalize (list_intersection_with f l k).
induction Hx2; simpl; [by rewrite Hx; left |].
case_match; simpl; try setoid_rewrite elem_of_cons; auto.
@@ -917,14 +917,14 @@ Proof. revert n i. induction l; intros [|?] [|?] ?; simpl; auto with lia. Qed.
Lemma take_alter f l n i : n ≤ i → take n (alter f i l) = take n l.
Proof.
intros. apply list_eq. intros j. destruct (le_lt_dec n j).
- * by rewrite !lookup_take_ge.
- * by rewrite !lookup_take, !list_lookup_alter_ne by lia.
+ - by rewrite !lookup_take_ge.
+ - by rewrite !lookup_take, !list_lookup_alter_ne by lia.
Qed.
Lemma take_insert l n i x : n ≤ i → take n (<[i:=x]>l) = take n l.
Proof.
intros. apply list_eq. intros j. destruct (le_lt_dec n j).
- * by rewrite !lookup_take_ge.
- * by rewrite !lookup_take, !list_lookup_insert_ne by lia.
+ - by rewrite !lookup_take_ge.
+ - by rewrite !lookup_take, !list_lookup_insert_ne by lia.
Qed.
(** ** Properties of the [drop] function *)
@@ -988,8 +988,8 @@ Lemma lookup_replicate n x y i :
replicate n x !! i = Some y ↔ y = x ∧ i < n.
Proof.
split.
- * revert i. induction n; intros [|?]; naive_solver auto with lia.
- * intros [-> Hi]. revert i Hi.
+ - revert i. induction n; intros [|?]; naive_solver auto with lia.
+ - intros [-> Hi]. revert i Hi.
induction n; intros [|?]; naive_solver auto with lia.
Qed.
Lemma lookup_replicate_1 n x y i :
@@ -1000,8 +1000,8 @@ Proof. by rewrite lookup_replicate. 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. rewrite lookup_replicate in Hx'; tauto.
- * intros Hx ?. destruct Hx. exists x; auto using lookup_replicate_2.
+ - intros Hin [x' Hx']; destruct Hin. rewrite lookup_replicate in Hx'; tauto.
+ - intros Hx ?. destruct Hx. exists x; auto using lookup_replicate_2.
Qed.
Lemma insert_replicate x n i : <[i:=x]>(replicate n x) = replicate n x.
Proof. revert i. induction n; intros [|?]; f_equal'; auto. Qed.
@@ -1025,8 +1025,8 @@ Lemma replicate_as_elem_of x n l :
Proof.
split; [intros <-; eauto using elem_of_replicate_inv, replicate_length|].
intros [<- Hl]. symmetry. induction l as [|y l IH]; f_equal'.
- * apply Hl. by left.
- * apply IH. intros ??. apply Hl. by right.
+ - 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.
@@ -1060,8 +1060,8 @@ 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 [|?] [|?]; f_equal'; auto.
- * by rewrite Nat.add_0_r, (right_id_L [] (++)).
- * by rewrite replicate_plus.
+ - by rewrite Nat.add_0_r, (right_id_L [] (++)).
+ - by rewrite replicate_plus.
Qed.
Lemma resize_plus_eq l n m x :
length l = n → resize (n + m) x l = l ++ replicate m x.
@@ -1086,8 +1086,8 @@ Proof. revert m. induction n; intros [|?]; f_equal'; auto. 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.
- * intros. by rewrite !resize_nil, resize_replicate.
- * intros [|?] [|?] ?; f_equal'; auto with lia.
+ - intros. by rewrite !resize_nil, resize_replicate.
+ - intros [|?] [|?] ?; f_equal'; auto with lia.
Qed.
Lemma resize_idemp l n x : resize n x (resize n x l) = resize n x l.
Proof. by rewrite resize_resize. Qed.
@@ -1109,8 +1109,8 @@ Lemma drop_resize_le l n m x :
n ≤ m → drop n (resize m x l) = resize (m - n) x (drop n l).
Proof.
revert n m. induction l; simpl.
- * intros. by rewrite drop_nil, !resize_nil, drop_replicate.
- * intros [|?] [|?] ?; simpl; try case_match; auto with lia.
+ - intros. by rewrite drop_nil, !resize_nil, drop_replicate.
+ - intros [|?] [|?] ?; simpl; try case_match; auto with lia.
Qed.
Lemma drop_resize_plus l n m x :
drop n (resize (n + m) x l) = resize m x (drop n l).
@@ -1118,8 +1118,8 @@ Proof. rewrite drop_resize_le by lia. f_equal. lia. 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.
+ - 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.
@@ -1205,14 +1205,14 @@ Lemma sublist_lookup_reshape l i n m :
reshape (replicate m n) l !! i = sublist_lookup (i * n) n l.
Proof.
intros Hn Hl. unfold sublist_lookup. apply option_eq; intros x; split.
- * intros Hx. case_option_guard as Hi.
+ - intros Hx. case_option_guard as Hi.
{ f_equal. clear Hi. revert i l Hl Hx.
induction m as [|m IH]; intros [|i] l ??; simplify_equality'; auto.
rewrite <-drop_drop. apply IH; rewrite ?drop_length; auto with lia. }
destruct Hi. rewrite Hl, <-Nat.mul_succ_l.
apply Nat.mul_le_mono_r, Nat.le_succ_l. apply lookup_lt_Some in Hx.
by rewrite reshape_length, replicate_length in Hx.
- * intros Hx. case_option_guard as Hi; simplify_equality'.
+ - intros Hx. case_option_guard as Hi; simplify_equality'.
revert i l Hl Hi. induction m as [|m IH]; [auto with lia|].
intros [|i] l ??; simpl; [done|]. rewrite <-drop_drop.
rewrite IH; rewrite ?drop_length; auto with lia.
@@ -1347,8 +1347,8 @@ Proof. induction 1; simpl; auto with lia. Qed.
Global Instance: Comm (≡ₚ) (@app A).
Proof.
intros l1. induction l1 as [|x l1 IH]; intros l2; simpl.
- * by rewrite (right_id_L [] (++)).
- * rewrite Permutation_middle, IH. simpl. by rewrite Permutation_middle.
+ - by rewrite (right_id_L [] (++)).
+ - rewrite Permutation_middle, IH. simpl. by rewrite Permutation_middle.
Qed.
Global Instance: ∀ x : A, Inj (≡ₚ) (≡ₚ) (x ::).
Proof. red. eauto using Permutation_cons_inv. Qed.
@@ -1364,8 +1364,8 @@ Qed.
Lemma replicate_Permutation n x l : replicate n x ≡ₚ l → replicate n x = l.
Proof.
intros Hl. apply replicate_as_elem_of. split.
- * by rewrite <-Hl, replicate_length.
- * intros y. rewrite <-Hl. by apply elem_of_replicate_inv.
+ - by rewrite <-Hl, replicate_length.
+ - intros y. rewrite <-Hl. by apply elem_of_replicate_inv.
Qed.
Lemma reverse_Permutation l : reverse l ≡ₚ l.
Proof.
@@ -1382,8 +1382,8 @@ Qed.
Global Instance: PreOrder (@prefix_of A).
Proof.
split.
- * intros ?. eexists []. by rewrite (right_id_L [] (++)).
- * intros ???[k1->] [k2->]. exists (k1 ++ k2). by rewrite (assoc_L (++)).
+ - intros ?. eexists []. by rewrite (right_id_L [] (++)).
+ - intros ???[k1->] [k2->]. exists (k1 ++ k2). by rewrite (assoc_L (++)).
Qed.
Lemma prefix_of_nil l : [] `prefix_of` l.
Proof. by exists l. Qed.
@@ -1415,8 +1415,8 @@ Proof. intros [??]. discriminate_list_equality. Qed.
Global Instance: PreOrder (@suffix_of A).
Proof.
split.
- * intros ?. by eexists [].
- * intros ???[k1->] [k2->]. exists (k2 ++ k1). by rewrite (assoc_L (++)).
+ - intros ?. by eexists [].
+ - intros ???[k1->] [k2->]. exists (k2 ++ k1). by rewrite (assoc_L (++)).
Qed.
Global Instance prefix_of_dec `{∀ x y, Decision (x = y)} : ∀ l1 l2,
Decision (l1 `prefix_of` l2) := fix go l1 l2 :=
@@ -1488,9 +1488,9 @@ Section prefix_ops.
Proof.
intros Hl ->. destruct (prefix_of_snoc_not k3 x2).
eapply max_prefix_of_max_alt; eauto.
- * rewrite (max_prefix_of_fst_alt _ _ _ _ _ Hl).
+ - rewrite (max_prefix_of_fst_alt _ _ _ _ _ Hl).
apply prefix_of_app, prefix_of_cons, prefix_of_nil.
- * rewrite (max_prefix_of_snd_alt _ _ _ _ _ Hl).
+ - rewrite (max_prefix_of_snd_alt _ _ _ _ _ Hl).
apply prefix_of_app, prefix_of_cons, prefix_of_nil.
Qed.
End prefix_ops.
@@ -1499,8 +1499,8 @@ Lemma prefix_suffix_reverse l1 l2 :
l1 `prefix_of` l2 ↔ reverse l1 `suffix_of` reverse l2.
Proof.
split; intros [k E]; exists (reverse k).
- * by rewrite E, reverse_app.
- * by rewrite <-(reverse_involutive l2), E, reverse_app, reverse_involutive.
+ - by rewrite E, reverse_app.
+ - by rewrite <-(reverse_involutive l2), E, reverse_app, reverse_involutive.
Qed.
Lemma suffix_prefix_reverse l1 l2 :
l1 `suffix_of` l2 ↔ reverse l1 `prefix_of` reverse l2.
@@ -1626,9 +1626,9 @@ Section max_suffix_of.
Proof.
intros Hl ->. destruct (suffix_of_cons_not x2 k3).
eapply max_suffix_of_max_alt; eauto.
- * rewrite (max_suffix_of_fst_alt _ _ _ _ _ Hl).
+ - rewrite (max_suffix_of_fst_alt _ _ _ _ _ Hl).
by apply (suffix_of_app [x2]), suffix_of_app_r.
- * rewrite (max_suffix_of_snd_alt _ _ _ _ _ Hl).
+ - rewrite (max_suffix_of_snd_alt _ _ _ _ _ Hl).
by apply (suffix_of_app [x2]), suffix_of_app_r.
Qed.
End max_suffix_of.
@@ -1654,37 +1654,37 @@ Lemma sublist_cons_l x l k :
x :: l `sublist` k ↔ ∃ k1 k2, k = k1 ++ x :: k2 ∧ l `sublist` k2.
Proof.
split.
- * intros Hlk. induction k as [|y k IH]; inversion Hlk.
+ - intros Hlk. induction k as [|y k IH]; inversion Hlk.
+ eexists [], k. by repeat constructor.
+ destruct IH as (k1&k2&->&?); auto. by exists (y :: k1), k2.
- * intros (k1&k2&->&?). by apply sublist_inserts_l, sublist_skip.
+ - intros (k1&k2&->&?). by apply sublist_inserts_l, sublist_skip.
Qed.
Lemma sublist_app_r l k1 k2 :
l `sublist` k1 ++ k2 ↔
∃ l1 l2, l = l1 ++ l2 ∧ l1 `sublist` k1 ∧ l2 `sublist` k2.
Proof.
split.
- * revert l k2. induction k1 as [|y k1 IH]; intros l k2; simpl.
+ - revert l k2. induction k1 as [|y k1 IH]; intros l k2; simpl.
{ 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_cons.
+ destruct (IH l' k2) as (l1&l2&?&?&?); trivial; subst.
exists (y :: l1), l2. auto using sublist_skip.
- * intros (?&?&?&?&?); subst. auto using sublist_app.
+ - intros (?&?&?&?&?); subst. auto using sublist_app.
Qed.
Lemma sublist_app_l l1 l2 k :
l1 ++ l2 `sublist` k ↔
∃ k1 k2, k = k1 ++ k2 ∧ l1 `sublist` k1 ∧ l2 `sublist` k2.
Proof.
split.
- * revert l2 k. induction l1 as [|x l1 IH]; intros l2 k; simpl.
+ - revert l2 k. induction l1 as [|x l1 IH]; intros l2 k; simpl.
{ eexists [], k. by repeat constructor. }
rewrite sublist_cons_l. intros (k1 & k2 &?&?); subst.
destruct (IH l2 k2) as (h1 & h2 &?&?&?); trivial; subst.
exists (k1 ++ x :: h1), h2. rewrite <-(assoc_L (++)).
auto using sublist_inserts_l, sublist_skip.
- * intros (?&?&?&?&?); subst. auto using sublist_app.
+ - intros (?&?&?&?&?); subst. auto using sublist_app.
Qed.
Lemma sublist_app_inv_l k l1 l2 : k ++ l1 `sublist` k ++ l2 → l1 `sublist` l2.
Proof.
@@ -1707,14 +1707,14 @@ Qed.
Global Instance: PartialOrder (@sublist A).
Proof.
split; [split|].
- * intros l. induction l; constructor; auto.
- * intros l1 l2 l3 Hl12. revert l3. induction Hl12.
+ - intros l. induction l; constructor; auto.
+ - intros l1 l2 l3 Hl12. revert l3. induction Hl12.
+ auto using sublist_nil_l.
+ 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_cons.
- * intros l1 l2 Hl12 Hl21. apply sublist_length in Hl21.
+ - intros l1 l2 Hl12 Hl21. apply sublist_length in Hl21.
induction Hl12; f_equal'; auto with arith.
apply sublist_length in Hl12. lia.
Qed.
@@ -1735,10 +1735,10 @@ Proof.
intros Hl12. cut (∀ k, ∃ is, k ++ l1 = foldr delete (k ++ l2) is).
{ intros help. apply (help []). }
induction Hl12 as [|x l1 l2 _ IH|x l1 l2 _ IH]; intros k.
- * by eexists [].
- * destruct (IH (k ++ [x])) as [is His]. exists is.
+ - by eexists [].
+ - destruct (IH (k ++ [x])) as [is His]. exists is.
by rewrite <-!(assoc_L (++)) in His.
- * destruct (IH k) as [is His]. exists (is ++ [length k]).
+ - destruct (IH k) as [is His]. exists (is ++ [length k]).
rewrite fold_right_app. simpl. by rewrite delete_middle.
Qed.
Lemma Permutation_sublist l1 l2 l3 :
@@ -1746,16 +1746,16 @@ Lemma Permutation_sublist l1 l2 l3 :
Proof.
intros Hl1l2. revert l3.
induction Hl1l2 as [|x l1 l2 ? IH|x y l1|l1 l1' l2 ? IH1 ? IH2].
- * intros l3. by exists l3.
- * intros l3. rewrite sublist_cons_l. intros (l3'&l3''&?&?); subst.
+ - intros l3. by exists l3.
+ - intros l3. rewrite sublist_cons_l. intros (l3'&l3''&?&?); subst.
destruct (IH l3'') as (l4&?&Hl4); auto. exists (l3' ++ x :: l4).
split. by apply sublist_inserts_l, sublist_skip. by rewrite Hl4.
- * intros l3. rewrite sublist_cons_l. intros (l3'&l3''&?& Hl3); subst.
+ - intros l3. rewrite sublist_cons_l. intros (l3'&l3''&?& Hl3); subst.
rewrite sublist_cons_l in Hl3. destruct Hl3 as (l5'&l5''&?& Hl5); subst.
exists (l3' ++ y :: l5' ++ x :: l5''). split.
- - by do 2 apply sublist_inserts_l, sublist_skip.
- - by rewrite !Permutation_middle, Permutation_swap.
- * intros l3 ?. destruct (IH2 l3) as (l3'&?&?); trivial.
+ + by do 2 apply sublist_inserts_l, sublist_skip.
+ + by rewrite !Permutation_middle, Permutation_swap.
+ - intros l3 ?. destruct (IH2 l3) as (l3'&?&?); trivial.
destruct (IH1 l3') as (l3'' &?&?); trivial. exists l3''.
split. done. etransitivity; eauto.
Qed.
@@ -1764,19 +1764,19 @@ Lemma sublist_Permutation l1 l2 l3 :
Proof.
intros Hl1l2 Hl2l3. revert l1 Hl1l2.
induction Hl2l3 as [|x l2 l3 ? IH|x y l2|l2 l2' l3 ? IH1 ? IH2].
- * intros l1. by exists l1.
- * intros l1. rewrite sublist_cons_r. intros [?|(l1'&l1''&?)]; subst.
+ - intros l1. by exists l1.
+ - intros l1. rewrite sublist_cons_r. intros [?|(l1'&l1''&?)]; subst.
{ destruct (IH l1) as (l4&?&?); trivial.
exists l4. split. done. by constructor. }
destruct (IH l1') as (l4&?&Hl4); auto. exists (x :: l4).
split. by constructor. by constructor.
- * intros l1. rewrite sublist_cons_r. intros [Hl1|(l1'&l1''&Hl1)]; subst.
+ - intros l1. rewrite sublist_cons_r. intros [Hl1|(l1'&l1''&Hl1)]; subst.
{ exists l1. split; [done|]. rewrite sublist_cons_r in Hl1.
destruct Hl1 as [?|(l1'&?&?)]; subst; by repeat constructor. }
rewrite sublist_cons_r in Hl1. destruct Hl1 as [?|(l1''&?&?)]; subst.
+ exists (y :: l1'). by repeat constructor.
+ exists (x :: y :: l1''). by repeat constructor.
- * intros l1 ?. destruct (IH1 l1) as (l3'&?&?); trivial.
+ - intros l1 ?. destruct (IH1 l1) as (l3'&?&?); trivial.
destruct (IH2 l3') as (l3'' &?&?); trivial. exists l3''.
split; [|done]. etransitivity; eauto.
Qed.
@@ -1794,8 +1794,8 @@ Qed.
Global Instance: PreOrder (@contains A).
Proof.
split.
- * intros l. induction l; constructor; auto.
- * red. apply contains_trans.
+ - intros l. induction l; constructor; auto.
+ - red. apply contains_trans.
Qed.
Lemma Permutation_contains l1 l2 : l1 ≡ₚ l2 → l1 `contains` l2.
Proof. induction 1; econstructor; eauto. Qed.
@@ -1805,18 +1805,18 @@ Lemma contains_Permutation l1 l2 : l1 `contains` l2 → ∃ k, l2 ≡ₚ l1 ++ k
Proof.
induction 1 as
[|x y l ? [k Hk]| |x l1 l2 ? [k Hk]|l1 l2 l3 ? [k Hk] ? [k' Hk']].
- * by eexists [].
- * exists k. by rewrite Hk.
- * eexists []. rewrite (right_id_L [] (++)). by constructor.
- * exists (x :: k). by rewrite Hk, Permutation_middle.
- * exists (k ++ k'). by rewrite Hk', Hk, (assoc_L (++)).
+ - by eexists [].
+ - exists k. by rewrite Hk.
+ - eexists []. rewrite (right_id_L [] (++)). by constructor.
+ - exists (x :: k). by rewrite Hk, Permutation_middle.
+ - exists (k ++ k'). by rewrite Hk', Hk, (assoc_L (++)).
Qed.
Lemma contains_Permutation_length_le l1 l2 :
length l2 ≤ length l1 → l1 `contains` l2 → l1 ≡ₚ l2.
Proof.
intros Hl21 Hl12. destruct (contains_Permutation l1 l2) as [[|??] Hk]; auto.
- * by rewrite Hk, (right_id_L [] (++)).
- * rewrite Hk, app_length in Hl21; simpl in Hl21; lia.
+ - by rewrite Hk, (right_id_L [] (++)).
+ - rewrite Hk, app_length in Hl21; simpl in Hl21; lia.
Qed.
Lemma contains_Permutation_length_eq l1 l2 :
length l2 = length l1 → l1 `contains` l2 → l1 ≡ₚ l2.
@@ -1824,9 +1824,9 @@ Proof. intro. apply contains_Permutation_length_le. lia. Qed.
Global Instance: Proper ((≡ₚ) ==> (≡ₚ) ==> iff) (@contains A).
Proof.
intros l1 l2 ? k1 k2 ?. split; intros.
- * transitivity l1. by apply Permutation_contains.
+ - transitivity l1. by apply Permutation_contains.
transitivity k1. done. by apply Permutation_contains.
- * transitivity l2. by apply Permutation_contains.
+ - transitivity l2. by apply Permutation_contains.
transitivity k2. done. by apply Permutation_contains.
Qed.
Global Instance: AntiSymm (≡ₚ) (@contains A).
@@ -1844,11 +1844,11 @@ Lemma contains_sublist_l l1 l3 :
Proof.
split.
{ intros Hl13. elim Hl13; clear l1 l3 Hl13.
- * by eexists [].
- * intros x l1 l3 ? (l2&?&?). exists (x :: l2). by repeat constructor.
- * intros x y l. exists (y :: x :: l). by repeat constructor.
- * intros x l1 l3 ? (l2&?&?). exists (x :: l2). by repeat constructor.
- * intros l1 l3 l5 ? (l2&?&?) ? (l4&?&?).
+ - by eexists [].
+ - intros x l1 l3 ? (l2&?&?). exists (x :: l2). by repeat constructor.
+ - intros x y l. exists (y :: x :: l). by repeat constructor.
+ - intros x l1 l3 ? (l2&?&?). exists (x :: l2). by repeat constructor.
+ - intros l1 l3 l5 ? (l2&?&?) ? (l4&?&?).
destruct (Permutation_sublist l2 l3 l4) as (l3'&?&?); trivial.
exists l3'. split; etransitivity; eauto. }
intros (l2&?&?).
@@ -1877,41 +1877,41 @@ Lemma contains_cons_r x l k :
l `contains` x :: k ↔ l `contains` k ∨ ∃ l', l ≡ₚ x :: l' ∧ l' `contains` k.
Proof.
split.
- * rewrite contains_sublist_r. intros (l'&E&Hl').
+ - rewrite contains_sublist_r. intros (l'&E&Hl').
rewrite sublist_cons_r in Hl'. destruct Hl' as [?|(?&?&?)]; subst.
+ left. rewrite E. eauto using sublist_contains.
+ right. eauto using sublist_contains.
- * intros [?|(?&E&?)]; [|rewrite E]; by constructor.
+ - intros [?|(?&E&?)]; [|rewrite E]; by constructor.
Qed.
Lemma contains_cons_l x l k :
x :: l `contains` k ↔ ∃ k', k ≡ₚ x :: k' ∧ l `contains` k'.
Proof.
split.
- * rewrite contains_sublist_l. intros (l'&Hl'&E).
+ - rewrite contains_sublist_l. intros (l'&Hl'&E).
rewrite sublist_cons_l in Hl'. destruct Hl' as (k1&k2&?&?); subst.
exists (k1 ++ k2). split; eauto using contains_inserts_l, sublist_contains.
by rewrite Permutation_middle.
- * intros (?&E&?). rewrite E. by constructor.
+ - intros (?&E&?). rewrite E. by constructor.
Qed.
Lemma contains_app_r l k1 k2 :
l `contains` k1 ++ k2 ↔ ∃ l1 l2,
l ≡ₚ l1 ++ l2 ∧ l1 `contains` k1 ∧ l2 `contains` k2.
Proof.
split.
- * rewrite contains_sublist_r. intros (l'&E&Hl').
+ - rewrite contains_sublist_r. intros (l'&E&Hl').
rewrite sublist_app_r in Hl'. destruct Hl' as (l1&l2&?&?&?); subst.
exists l1, l2. eauto using sublist_contains.
- * intros (?&?&E&?&?). rewrite E. eauto using contains_app.
+ - intros (?&?&E&?&?). rewrite E. eauto using contains_app.
Qed.
Lemma contains_app_l l1 l2 k :
l1 ++ l2 `contains` k ↔ ∃ k1 k2,
k ≡ₚ k1 ++ k2 ∧ l1 `contains` k1 ∧ l2 `contains` k2.
Proof.
split.
- * rewrite contains_sublist_l. intros (l'&Hl'&E).
+ - rewrite contains_sublist_l. intros (l'&Hl'&E).
rewrite sublist_app_l in Hl'. destruct Hl' as (k1&k2&?&?&?); subst.
exists k1, k2. split. done. eauto using sublist_contains.
- * intros (?&?&E&?&?). rewrite E. eauto using contains_app.
+ - intros (?&?&E&?&?). rewrite E. eauto using contains_app.
Qed.
Lemma contains_app_inv_l l1 l2 k :
k ++ l1 `contains` k ++ l2 → l1 `contains` l2.
@@ -1947,8 +1947,8 @@ Lemma Permutation_alt l1 l2 :
l1 ≡ₚ l2 ↔ length l1 = length l2 ∧ l1 `contains` l2.
Proof.
split.
- * by intros Hl; rewrite Hl.
- * intros [??]; auto using contains_Permutation_length_eq.
+ - by intros Hl; rewrite Hl.
+ - intros [??]; auto using contains_Permutation_length_eq.
Qed.
Lemma NoDup_contains l k : NoDup l → (∀ x, x ∈ l → x ∈ k) → l `contains` k.
@@ -1976,12 +1976,12 @@ Section contains_dec.
Proof.
intros Hl. revert k1. induction Hl
as [|y l1 l2 ? IH|y1 y2 l|l1 l2 l3 ? IH1 ? IH2]; simpl; intros k1 Hk1.
- * done.
- * case_decide; simplify_equality; eauto.
+ - done.
+ - case_decide; simplify_equality; eauto.
destruct (list_remove x l1) as [l|] eqn:?; simplify_equality.
destruct (IH l) as (?&?&?); simplify_option_equality; eauto.
- * simplify_option_equality; eauto using Permutation_swap.
- * destruct (IH1 k1) as (k2&?&?); trivial.
+ - simplify_option_equality; eauto using Permutation_swap.
+ - destruct (IH1 k1) as (k2&?&?); trivial.
destruct (IH2 k2) as (k3&?&?); trivial.
exists k3. split; eauto. by transitivity k2.
Qed.
@@ -1994,20 +1994,20 @@ Section contains_dec.
l ≡ₚ x :: k → ∃ k', list_remove x l = Some k' ∧ k ≡ₚ k'.
Proof.
intros. destruct (list_remove_Permutation (x :: k) l k x) as (k'&?&?).
- * done.
- * simpl; by case_decide.
- * by exists k'.
+ - done.
+ - simpl; by case_decide.
+ - by exists k'.
Qed.
Lemma list_remove_list_contains l1 l2 :
l1 `contains` l2 ↔ is_Some (list_remove_list l1 l2).
Proof.
split.
- * revert l2. induction l1 as [|x l1 IH]; simpl.
+ - revert l2. induction l1 as [|x l1 IH]; simpl.
{ intros l2 _. by exists l2. }
intros l2. rewrite contains_cons_l. intros (k&Hk&?).
destruct (list_remove_Some_inv l2 k x) as (k2&?&Hk2); trivial.
simplify_option_equality. apply IH. by rewrite <-Hk2.
- * intros [k Hk]. revert l2 k Hk.
+ - intros [k Hk]. revert l2 k Hk.
induction l1 as [|x l1 IH]; simpl; intros l2 k.
{ intros. apply contains_nil_l. }
destruct (list_remove x l2) as [k'|] eqn:?; intros; simplify_equality.
@@ -2168,8 +2168,8 @@ Section Forall_Exists.
Lemma Exists_exists l : Exists P l ↔ ∃ x, x ∈ l ∧ P x.
Proof.
split.
- * induction 1 as [x|y ?? [x [??]]]; exists x; by repeat constructor.
- * intros [x [Hin ?]]. induction l; [by destruct (not_elem_of_nil x)|].
+ - induction 1 as [x|y ?? [x [??]]]; exists x; by repeat constructor.
+ - intros [x [Hin ?]]. induction l; [by destruct (not_elem_of_nil x)|].
inversion Hin; subst. by left. right; auto.
Qed.
Lemma Exists_inv x l : Exists P (x :: l) → P x ∨ Exists P l.
@@ -2177,8 +2177,8 @@ Section Forall_Exists.
Lemma Exists_app l1 l2 : Exists P (l1 ++ l2) ↔ Exists P l1 ∨ Exists P l2.
Proof.
split.
- * induction l1; inversion 1; intuition.
- * intros [H|H]; [induction H | induction l1]; simpl; intuition.
+ - induction l1; inversion 1; intuition.
+ - intros [H|H]; [induction H | induction l1]; simpl; intuition.
Qed.
Lemma Exists_impl (Q : A → Prop) l :
Exists P l → (∀ x, P x → Q x) → Exists Q l.
@@ -2238,9 +2238,9 @@ 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)).
+ - 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.
+ - intros H j x Hj. apply lookup_seq_inv in Hj.
destruct Hj; subst. auto with lia.
Qed.
@@ -2441,8 +2441,8 @@ Section Forall2.
Proof.
unfold sublist_lookup. intros Hlk Hl.
exists (take i (drop n k)); simplify_option_equality.
- * auto using Forall2_take, Forall2_drop.
- * apply Forall2_length in Hlk; lia.
+ - auto using Forall2_take, Forall2_drop.
+ - apply Forall2_length in Hlk; lia.
Qed.
Lemma Forall2_sublist_lookup_r l k n i k' :
Forall2 P l k → sublist_lookup n i k = Some k' →
@@ -2540,9 +2540,9 @@ Section Forall3.
k = k1 ++ k2 ∧ k' = k1' ++ k2' ∧ Forall3 P l1 k1 k1' ∧ Forall3 P l2 k2 k2'.
Proof.
revert k k'. induction l1 as [|x l1 IH]; simpl; inversion_clear 1.
- * by repeat eexists; eauto.
- * by repeat eexists; eauto.
- * edestruct IH as (?&?&?&?&?&?&?&?); eauto; naive_solver.
+ - by repeat eexists; eauto.
+ - by repeat eexists; eauto.
+ - edestruct IH as (?&?&?&?&?&?&?&?); eauto; naive_solver.
Qed.
Lemma Forall3_cons_inv_m l y k k' :
Forall3 P l (y :: k) k' → ∃ x l2 z k2',
@@ -2553,9 +2553,9 @@ Section Forall3.
l = l1 ++ l2 ∧ k' = k1' ++ k2' ∧ Forall3 P l1 k1 k1' ∧ Forall3 P l2 k2 k2'.
Proof.
revert l k'. induction k1 as [|x k1 IH]; simpl; inversion_clear 1.
- * by repeat eexists; eauto.
- * by repeat eexists; eauto.
- * edestruct IH as (?&?&?&?&?&?&?&?); eauto; naive_solver.
+ - by repeat eexists; eauto.
+ - by repeat eexists; eauto.
+ - edestruct IH as (?&?&?&?&?&?&?&?); eauto; naive_solver.
Qed.
Lemma Forall3_cons_inv_r l k z k' :
Forall3 P l k (z :: k') → ∃ x l2 y k2,
@@ -2566,9 +2566,9 @@ Section Forall3.
l = l1 ++ l2 ∧ k = k1 ++ k2 ∧ Forall3 P l1 k1 k1' ∧ Forall3 P l2 k2 k2'.
Proof.
revert l k. induction k1' as [|x k1' IH]; simpl; inversion_clear 1.
- * by repeat eexists; eauto.
- * by repeat eexists; eauto.
- * edestruct IH as (?&?&?&?&?&?&?&?); eauto; naive_solver.
+ - by repeat eexists; eauto.
+ - by repeat eexists; eauto.
+ - edestruct IH as (?&?&?&?&?&?&?&?); eauto; naive_solver.
Qed.
Lemma Forall3_impl (Q : A → B → C → Prop) l k k' :
Forall3 P l k k' → (∀ x y z, P x y z → Q x y z) → Forall3 Q l k k'.
@@ -2682,8 +2682,8 @@ Section fmap.
Lemma elem_of_list_fmap_2 l x : x ∈ f <$> l → ∃ y, x = f y ∧ y ∈ l.
Proof.
induction l as [|y l IH]; simpl; inversion_clear 1.
- * exists y. split; [done | by left].
- * destruct IH as [z [??]]. done. exists z. split; [done | by right].
+ - exists y. split; [done | by left].
+ - destruct IH as [z [??]]. done. exists z. split; [done | by right].
Qed.
Lemma elem_of_list_fmap l x : x ∈ f <$> l ↔ ∃ y, x = f y ∧ y ∈ l.
Proof.
@@ -2750,10 +2750,10 @@ Lemma NoDup_fmap_fst {A B} (l : list (A * B)) :
(∀ x y1 y2, (x,y1) ∈ l → (x,y2) ∈ l → y1 = y2) → NoDup l → NoDup (l.*1).
Proof.
intros Hunique. induction 1 as [|[x1 y1] l Hin Hnodup IH]; csimpl; constructor.
- * rewrite elem_of_list_fmap.
+ - 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.
@@ -2773,17 +2773,17 @@ Section bind.
Global Instance bind_contains: Proper (contains ==> contains) (mbind f).
Proof.
induction 1; csimpl; auto.
- * by apply contains_app.
- * by rewrite !(assoc_L (++)), (comm (++) (f _)).
- * by apply contains_inserts_l.
- * etransitivity; eauto.
+ - by apply contains_app.
+ - by rewrite !(assoc_L (++)), (comm (++) (f _)).
+ - by apply contains_inserts_l.
+ - etransitivity; eauto.
Qed.
Global Instance bind_Permutation: Proper ((≡ₚ) ==> (≡ₚ)) (mbind f).
Proof.
induction 1; csimpl; auto.
- * by f_equiv.
- * by rewrite !(assoc_L (++)), (comm (++) (f _)).
- * etransitivity; eauto.
+ - by f_equiv.
+ - by rewrite !(assoc_L (++)), (comm (++) (f _)).
+ - etransitivity; eauto.
Qed.
Lemma bind_cons x l : (x :: l) ≫= f = f x ++ l ≫= f.
Proof. done. Qed.
@@ -2795,18 +2795,18 @@ Section bind.
x ∈ l ≫= f ↔ ∃ y, x ∈ f y ∧ y ∈ l.
Proof.
split.
- * induction l as [|y l IH]; csimpl; [inversion 1|].
+ - induction l as [|y l IH]; csimpl; [inversion 1|].
rewrite elem_of_app. intros [?|?].
+ exists y. split; [done | by left].
+ destruct IH as [z [??]]. done. exists z. split; [done | by right].
- * intros [y [Hx Hy]]. induction Hy; csimpl; rewrite elem_of_app; intuition.
+ - intros [y [Hx Hy]]. induction Hy; csimpl; rewrite elem_of_app; intuition.
Qed.
Lemma Forall_bind (P : B → Prop) l :
Forall P (l ≫= f) ↔ Forall (Forall P ∘ f) l.
Proof.
split.
- * induction l; csimpl; rewrite ?Forall_app; constructor; csimpl; intuition.
- * induction 1; csimpl; rewrite ?Forall_app; auto.
+ - induction l; csimpl; rewrite ?Forall_app; constructor; csimpl; intuition.
+ - induction 1; csimpl; rewrite ?Forall_app; auto.
Qed.
Lemma Forall2_bind {C D} (g : C → list D) (P : B → D → Prop) l1 l2 :
Forall2 (λ x1 x2, Forall2 P (f x1) (g x2)) l1 l2 →
@@ -2858,8 +2858,8 @@ Section mapM.
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:?; intros; simplify_option_equality; auto.
+ - destruct (f x); simpl; [|discriminate]. by destruct (mapM f l).
+ - destruct (f x) eqn:?; intros; simplify_option_equality; auto.
Qed.
Lemma mapM_Some_2 l k : Forall2 (λ x y, f x = Some y) l k → mapM f l = Some k.
Proof.
@@ -2916,8 +2916,8 @@ Section permutations.
Lemma interleave_Permutation x l l' : l' ∈ interleave x l → l' ≡ₚ x :: l.
Proof.
revert l'. induction l as [|y l IH]; intros l'; simpl.
- * rewrite elem_of_list_singleton. by intros ->.
- * rewrite elem_of_cons, elem_of_list_fmap. intros [->|[? [-> H]]]; [done|].
+ - rewrite elem_of_list_singleton. by intros ->.
+ - rewrite elem_of_cons, elem_of_list_fmap. intros [->|[? [-> H]]]; [done|].
rewrite (IH _ H). constructor.
Qed.
Lemma permutations_refl l : l ∈ permutations l.
@@ -2931,8 +2931,8 @@ Section permutations.
Lemma permutations_swap x y l : y :: x :: l ∈ permutations (x :: y :: l).
Proof.
simpl. apply elem_of_list_bind. exists (y :: l). split; simpl.
- * destruct l; csimpl; rewrite !elem_of_cons; auto.
- * apply elem_of_list_bind. simpl.
+ - destruct l; csimpl; rewrite !elem_of_cons; auto.
+ - apply elem_of_list_bind. simpl.
eauto using interleave_cons, permutations_refl.
Qed.
Lemma permutations_nil l : l ∈ permutations [] ↔ l = [].
@@ -2947,12 +2947,12 @@ Section permutations.
by rewrite (comm (++)), elem_of_list_singleton. }
rewrite elem_of_cons, elem_of_list_fmap.
intros Hl1 [? | [l2' [??]]]; simplify_equality'.
- * rewrite !elem_of_cons, elem_of_list_fmap in Hl1.
+ - rewrite !elem_of_cons, elem_of_list_fmap in Hl1.
destruct Hl1 as [? | [? | [l4 [??]]]]; subst.
+ exists (x1 :: y :: l3). csimpl. rewrite !elem_of_cons. tauto.
+ exists (x1 :: y :: l3). csimpl. rewrite !elem_of_cons. tauto.
+ exists l4. simpl. rewrite elem_of_cons. auto using interleave_cons.
- * rewrite elem_of_cons, elem_of_list_fmap in Hl1.
+ - rewrite elem_of_cons, elem_of_list_fmap in Hl1.
destruct Hl1 as [? | [l1' [??]]]; subst.
+ exists (x1 :: y :: l3). csimpl.
rewrite !elem_of_cons, !elem_of_list_fmap.
@@ -2970,9 +2970,9 @@ Section permutations.
by rewrite elem_of_list_singleton. }
rewrite elem_of_cons, elem_of_list_fmap.
intros Hl1 [? | [l2' [? Hl2']]]; simplify_equality'.
- * rewrite elem_of_list_bind in Hl1.
+ - rewrite elem_of_list_bind in Hl1.
destruct Hl1 as [l1' [??]]. by exists l1'.
- * rewrite elem_of_list_bind in Hl1. setoid_rewrite elem_of_list_bind.
+ - rewrite elem_of_list_bind in Hl1. setoid_rewrite elem_of_list_bind.
destruct Hl1 as [l1' [??]]. destruct (IH l1' l2') as (l1''&?&?); auto.
destruct (interleave_interleave_toggle y x l1 l1' l1'') as (?&?&?); eauto.
Qed.
@@ -2980,19 +2980,19 @@ Section permutations.
l1 ∈ permutations l2 → l2 ∈ permutations l3 → l1 ∈ permutations l3.
Proof.
revert l1 l2. induction l3 as [|x l3 IH]; intros l1 l2; simpl.
- * rewrite !elem_of_list_singleton. intros Hl1 ->; simpl in *.
+ - rewrite !elem_of_list_singleton. intros Hl1 ->; simpl in *.
by rewrite elem_of_list_singleton in Hl1.
- * rewrite !elem_of_list_bind. intros Hl1 [l2' [Hl2 Hl2']].
+ - rewrite !elem_of_list_bind. intros Hl1 [l2' [Hl2 Hl2']].
destruct (permutations_interleave_toggle x l1 l2 l2') as [? [??]]; eauto.
Qed.
Lemma permutations_Permutation l l' : l' ∈ permutations l ↔ l ≡ₚ l'.
Proof.
split.
- * revert l'. induction l; simpl; intros l''.
+ - revert l'. induction l; simpl; intros l''.
+ rewrite elem_of_list_singleton. by intros ->.
+ rewrite elem_of_list_bind. intros [l' [Hl'' ?]].
rewrite (interleave_Permutation _ _ _ Hl''). constructor; auto.
- * induction 1; eauto using permutations_refl,
+ - induction 1; eauto using permutations_refl,
permutations_skip, permutations_swap, permutations_trans.
Qed.
End permutations.
@@ -3195,11 +3195,11 @@ Lemma elem_of_zipped_map {A B} (f : list A → list A → A → B) l k x :
∃ k' k'' y, k = k' ++ [y] ++ k'' ∧ x = f (reverse k' ++ l) k'' y.
Proof.
split.
- * revert l. induction k as [|z k IH]; simpl; intros l; inversion_clear 1.
+ - revert l. induction k as [|z k IH]; simpl; intros l; inversion_clear 1.
{ by eexists [], k, z. }
destruct (IH (z :: l)) as (k'&k''&y&->&->); [done |].
eexists (z :: k'), k'', y. by rewrite reverse_cons, <-(assoc_L (++)).
- * intros (k'&k''&y&->&->). revert l. induction k' as [|z k' IH]; [by left|].
+ - intros (k'&k''&y&->&->). revert l. induction k' as [|z k' IH]; [by left|].
intros l; right. by rewrite reverse_cons, <-!(assoc_L (++)).
Qed.
Section zipped_list_ind.
@@ -3276,9 +3276,9 @@ Section eval.
Lemma eval_alt t : eval E t = to_list t ≫= from_option [] ∘ (E !!).
Proof.
induction t; csimpl.
- * done.
- * by rewrite (right_id_L [] (++)).
- * rewrite bind_app. by f_equal.
+ - done.
+ - by rewrite (right_id_L [] (++)).
+ - rewrite bind_app. by f_equal.
Qed.
Lemma eval_eq t1 t2 : to_list t1 = to_list t2 → eval E t1 = eval E t2.
Proof. intros Ht. by rewrite !eval_alt, Ht. Qed.
diff --git a/theories/listset.v b/theories/listset.v
index bcf8ed89..362bcbd5 100644
--- a/theories/listset.v
+++ b/theories/listset.v
@@ -21,9 +21,9 @@ Global Opaque listset_singleton listset_empty.
Global Instance: SimpleCollection A (listset A).
Proof.
split.
- * by apply not_elem_of_nil.
- * by apply elem_of_list_singleton.
- * intros [?] [?]. apply elem_of_app.
+ - by apply not_elem_of_nil.
+ - by apply elem_of_list_singleton.
+ - intros [?] [?]. apply elem_of_app.
Qed.
Lemma listset_empty_alt X : X ≡ ∅ ↔ listset_car X = [].
Proof.
@@ -50,24 +50,24 @@ Instance listset_filter: Filter A (listset A) := λ P _ l,
Instance: Collection A (listset A).
Proof.
split.
- * apply _.
- * intros [?] [?]. apply elem_of_list_intersection.
- * intros [?] [?]. apply elem_of_list_difference.
+ - apply _.
+ - intros [?] [?]. apply elem_of_list_intersection.
+ - intros [?] [?]. apply elem_of_list_difference.
Qed.
Instance listset_elems: Elements A (listset A) := remove_dups ∘ listset_car.
Global Instance: FinCollection A (listset A).
Proof.
split.
- * apply _.
- * intros. apply elem_of_remove_dups.
- * intros. apply NoDup_remove_dups.
+ - apply _.
+ - intros. apply elem_of_remove_dups.
+ - intros. apply NoDup_remove_dups.
Qed.
Global Instance: CollectionOps A (listset A).
Proof.
split.
- * apply _.
- * intros ? [?] [?]. apply elem_of_list_intersection_with.
- * intros [?] ??. apply elem_of_list_filter.
+ - apply _.
+ - intros ? [?] [?]. apply elem_of_list_intersection_with.
+ - intros [?] ??. apply elem_of_list_filter.
Qed.
End listset.
@@ -102,10 +102,10 @@ Instance listset_join: MJoin listset := λ A, mbind id.
Instance: CollectionMonad listset.
Proof.
split.
- * intros. apply _.
- * intros ??? [?] ?. apply elem_of_list_bind.
- * intros. apply elem_of_list_ret.
- * intros ??? [?]. apply elem_of_list_fmap.
- * intros ? [?] ?. unfold mjoin, listset_join, elem_of, listset_elem_of.
+ - intros. apply _.
+ - intros ??? [?] ?. apply elem_of_list_bind.
+ - intros. apply elem_of_list_ret.
+ - intros ??? [?]. apply elem_of_list_fmap.
+ - intros ? [?] ?. unfold mjoin, listset_join, elem_of, listset_elem_of.
simpl. by rewrite elem_of_list_bind.
Qed.
diff --git a/theories/listset_nodup.v b/theories/listset_nodup.v
index d6850862..6140a103 100644
--- a/theories/listset_nodup.v
+++ b/theories/listset_nodup.v
@@ -39,11 +39,11 @@ Instance listset_nodup_filter: Filter A C := λ P _ l,
Instance: Collection A C.
Proof.
split; [split | | ].
- * by apply not_elem_of_nil.
- * by apply elem_of_list_singleton.
- * intros [??] [??] ?. apply elem_of_list_union.
- * intros [??] [??] ?. apply elem_of_list_intersection.
- * intros [??] [??] ?. apply elem_of_list_difference.
+ - by apply not_elem_of_nil.
+ - by apply elem_of_list_singleton.
+ - intros [??] [??] ?. apply elem_of_list_union.
+ - intros [??] [??] ?. apply elem_of_list_intersection.
+ - intros [??] [??] ?. apply elem_of_list_difference.
Qed.
Global Instance listset_nodup_elems: Elements A C := listset_nodup_car.
@@ -52,11 +52,11 @@ Proof. split. apply _. done. by intros [??]. Qed.
Global Instance: CollectionOps A C.
Proof.
split.
- * apply _.
- * intros ? [??] [??] ?. unfold intersection_with, elem_of,
+ - apply _.
+ - intros ? [??] [??] ?. unfold intersection_with, elem_of,
listset_nodup_intersection_with, listset_nodup_elem_of; simpl.
rewrite elem_of_remove_dups. by apply elem_of_list_intersection_with.
- * intros [??] ???. apply elem_of_list_filter.
+ - intros [??] ???. apply elem_of_list_filter.
Qed.
End list_collection.
diff --git a/theories/mapset.v b/theories/mapset.v
index 700d6281..b8dfca09 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -47,19 +47,19 @@ Proof. solve_decision. Defined.
Instance: Collection K (mapset M).
Proof.
split; [split | | ].
- * unfold empty, elem_of, mapset_empty, mapset_elem_of.
+ - unfold empty, elem_of, mapset_empty, mapset_elem_of.
simpl. intros. by simpl_map.
- * unfold singleton, elem_of, mapset_singleton, mapset_elem_of.
+ - unfold singleton, elem_of, mapset_singleton, mapset_elem_of.
simpl. by split; intros; simplify_map_equality.
- * unfold union, elem_of, mapset_union, mapset_elem_of.
+ - unfold union, elem_of, mapset_union, mapset_elem_of.
intros [m1] [m2] ?. simpl. rewrite lookup_union_Some_raw.
destruct (m1 !! x) as [[]|]; tauto.
- * unfold intersection, elem_of, mapset_intersection, mapset_elem_of.
+ - unfold intersection, elem_of, mapset_intersection, mapset_elem_of.
intros [m1] [m2] ?. simpl. rewrite lookup_intersection_Some.
assert (is_Some (m2 !! x) ↔ m2 !! x = Some ()).
{ split; eauto. by intros [[] ?]. }
naive_solver.
- * unfold difference, elem_of, mapset_difference, mapset_elem_of.
+ - unfold difference, elem_of, mapset_difference, mapset_elem_of.
intros [m1] [m2] ?. simpl. rewrite lookup_difference_Some.
destruct (m2 !! x) as [[]|]; intuition congruence.
Qed.
@@ -68,12 +68,12 @@ Proof. split; try apply _. intros ????. apply mapset_eq. intuition. Qed.
Global Instance: FinCollection K (mapset M).
Proof.
split.
- * apply _.
- * unfold elements, elem_of at 2, mapset_elems, mapset_elem_of.
+ - apply _.
+ - unfold elements, elem_of at 2, mapset_elems, mapset_elem_of.
intros [m] x. simpl. rewrite elem_of_list_fmap. split.
+ intros ([y []] &?& Hy). subst. by rewrite <-elem_of_map_to_list.
+ intros. exists (x, ()). by rewrite elem_of_map_to_list.
- * unfold elements, mapset_elems. intros [m]. simpl.
+ - unfold elements, mapset_elems. intros [m]. simpl.
apply NoDup_fst_map_to_list.
Qed.
@@ -101,8 +101,8 @@ Lemma elem_of_mapset_dom_with {A} (f : A → bool) m i :
Proof.
unfold mapset_dom_with, elem_of, mapset_elem_of.
simpl. rewrite lookup_merge by done. destruct (m !! i) as [a|].
- * destruct (Is_true_reflect (f a)); naive_solver.
- * naive_solver.
+ - destruct (Is_true_reflect (f a)); naive_solver.
+ - naive_solver.
Qed.
Instance mapset_dom {A} : Dom (M A) (mapset M) := mapset_dom_with (λ _, true).
Instance mapset_dom_spec: FinMapDom K M (mapset M).
diff --git a/theories/natmap.v b/theories/natmap.v
index a8ebf6e2..707bb749 100644
--- a/theories/natmap.v
+++ b/theories/natmap.v
@@ -160,15 +160,15 @@ Lemma natmap_elem_of_to_list_raw_aux {A} j (l : natmap_raw A) i x :
(i,x) ∈ natmap_to_list_raw j l ↔ ∃ i', i = i' + j ∧ mjoin (l !! i') = Some x.
Proof.
split.
- * revert j. induction l as [|[y|] l IH]; intros j; simpl.
+ - revert j. induction l as [|[y|] l IH]; intros j; simpl.
+ by rewrite elem_of_nil.
+ rewrite elem_of_cons. intros [?|?]; simplify_equality.
- - by exists 0.
- - destruct (IH (S j)) as (i'&?&?); auto.
+ * by exists 0.
+ * destruct (IH (S j)) as (i'&?&?); auto.
exists (S i'); simpl; auto with lia.
+ intros. destruct (IH (S j)) as (i'&?&?); auto.
exists (S i'); simpl; auto with lia.
- * intros (i'&?&Hi'). subst. revert i' j Hi'.
+ - intros (i'&?&Hi'). subst. revert i' j Hi'.
induction l as [|[y|] l IH]; intros i j ?; simpl.
+ done.
+ destruct i as [|i]; simplify_equality'; [left|].
@@ -210,7 +210,7 @@ Instance natmap_map: FMap natmap := λ A B f m,
Instance: FinMap nat natmap.
Proof.
split.
- * unfold lookup, natmap_lookup. intros A [l1 Hl1] [l2 Hl2] E.
+ - unfold lookup, natmap_lookup. intros A [l1 Hl1] [l2 Hl2] E.
apply natmap_eq. revert l2 Hl1 Hl2 E. simpl.
induction l1 as [|[x|] l1 IH]; intros [|[y|] l2] Hl1 Hl2 E; simpl in *.
+ done.
@@ -223,14 +223,14 @@ Proof.
+ destruct (natmap_wf_lookup (None :: l1)) as (i&?&?); auto with congruence.
+ by specialize (E 0).
+ f_equal. apply IH; eauto using natmap_wf_inv. intros i. apply (E (S i)).
- * done.
- * intros ?? [??] ?. apply natmap_lookup_alter_raw.
- * intros ?? [??] ??. apply natmap_lookup_alter_raw_ne.
- * intros ??? [??] ?. apply natmap_lookup_map_raw.
- * intros ? [??]. by apply natmap_to_list_raw_nodup.
- * intros ? [??] ??. by apply natmap_elem_of_to_list_raw.
- * intros ??? [??] ?. by apply natmap_lookup_omap_raw.
- * intros ????? [??] [??] ?. by apply natmap_lookup_merge_raw.
+ - done.
+ - intros ?? [??] ?. apply natmap_lookup_alter_raw.
+ - intros ?? [??] ??. apply natmap_lookup_alter_raw_ne.
+ - intros ??? [??] ?. apply natmap_lookup_map_raw.
+ - intros ? [??]. by apply natmap_to_list_raw_nodup.
+ - intros ? [??] ??. by apply natmap_elem_of_to_list_raw.
+ - intros ??? [??] ?. by apply natmap_lookup_omap_raw.
+ - intros ????? [??] [??] ?. by apply natmap_lookup_merge_raw.
Qed.
Fixpoint strip_Nones {A} (l : list (option A)) : list (option A) :=
@@ -353,8 +353,8 @@ Lemma natmap_push_pop {A} (m : natmap A) :
natmap_push (m !! 0) (natmap_pop m) = m.
Proof.
apply map_eq. intros i. destruct i.
- * by rewrite lookup_natmap_push_O.
- * by rewrite lookup_natmap_push_S, lookup_natmap_pop.
+ - by rewrite lookup_natmap_push_O.
+ - by rewrite lookup_natmap_push_S, lookup_natmap_pop.
Qed.
Lemma natmap_pop_push {A} o (m : natmap A) : natmap_pop (natmap_push o m) = m.
Proof. apply natmap_eq. by destruct o, m as [[|??]]. Qed.
diff --git a/theories/nmap.v b/theories/nmap.v
index f9f14341..61aac7af 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -49,34 +49,34 @@ Instance Nfmap: FMap Nmap := λ A B f t,
Instance: FinMap N Nmap.
Proof.
split.
- * intros ? [??] [??] H. f_equal; [apply (H 0)|].
+ - intros ? [??] [??] H. f_equal; [apply (H 0)|].
apply map_eq. intros i. apply (H (Npos i)).
- * by intros ? [|?].
- * intros ? f [? t] [|i]; simpl; [done |]. apply lookup_partial_alter.
- * intros ? f [? t] [|i] [|j]; simpl; try intuition congruence.
+ - by intros ? [|?].
+ - intros ? f [? t] [|i]; simpl; [done |]. apply lookup_partial_alter.
+ - intros ? f [? t] [|i] [|j]; simpl; try intuition congruence.
intros. apply lookup_partial_alter_ne. congruence.
- * intros ??? [??] []; simpl. done. apply lookup_fmap.
- * intros ? [[x|] t]; unfold map_to_list; simpl.
+ - intros ??? [??] []; simpl. done. apply lookup_fmap.
+ - intros ? [[x|] t]; unfold map_to_list; simpl.
+ constructor.
- - rewrite elem_of_list_fmap. by intros [[??] [??]].
- - by apply (NoDup_fmap _), NoDup_map_to_list.
+ * rewrite elem_of_list_fmap. by intros [[??] [??]].
+ * by apply (NoDup_fmap _), NoDup_map_to_list.
+ apply (NoDup_fmap _), NoDup_map_to_list.
- * intros ? t i x. unfold map_to_list. split.
+ - intros ? t i x. unfold map_to_list. split.
+ destruct t as [[y|] t]; simpl.
- - rewrite elem_of_cons, elem_of_list_fmap.
+ * rewrite elem_of_cons, elem_of_list_fmap.
intros [? | [[??] [??]]]; simplify_equality'; [done |].
by apply elem_of_map_to_list.
- - rewrite elem_of_list_fmap; intros [[??] [??]]; simplify_equality'.
+ * rewrite elem_of_list_fmap; intros [[??] [??]]; simplify_equality'.
by apply elem_of_map_to_list.
+ destruct t as [[y|] t]; simpl.
- - rewrite elem_of_cons, elem_of_list_fmap.
+ * rewrite elem_of_cons, elem_of_list_fmap.
destruct i as [|i]; simpl; [intuition congruence |].
intros. right. exists (i, x). by rewrite elem_of_map_to_list.
- - rewrite elem_of_list_fmap.
+ * rewrite elem_of_list_fmap.
destruct i as [|i]; simpl; [done |].
intros. exists (i, x). by rewrite elem_of_map_to_list.
- * intros ?? f [??] [|?]; simpl; [done|]; apply (lookup_omap f).
- * intros ??? f ? [??] [??] [|?]; simpl; [done|]; apply (lookup_merge f).
+ - intros ?? f [??] [|?]; simpl; [done|]; apply (lookup_omap f).
+ - intros ??? f ? [??] [??] [|?]; simpl; [done|]; apply (lookup_merge f).
Qed.
(** * Finite sets *)
@@ -96,8 +96,8 @@ Instance Nset_fresh : Fresh N Nset := λ X,
Instance Nset_fresh_spec : FreshSpec N Nset.
Proof.
split.
- * apply _.
- * intros X Y; rewrite <-elem_of_equiv_L. by intros ->.
- * unfold elem_of, mapset_elem_of, fresh; intros [m]; simpl.
+ - apply _.
+ - intros X Y; rewrite <-elem_of_equiv_L. by intros ->.
+ - unfold elem_of, mapset_elem_of, fresh; intros [m]; simpl.
by rewrite Nfresh_fresh.
Qed.
diff --git a/theories/numbers.v b/theories/numbers.v
index d688ae71..c77bb160 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -45,10 +45,10 @@ Proof.
assert (∀ x y (p : x ≤ y) y' (q : x ≤ y'),
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. 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). }
+ - done.
+ - 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 (Eqdep_dec.eq_dep_eq_dec (λ x y, decide (x = y))), aux.
Qed.
@@ -153,8 +153,8 @@ Proof.
cut (∀ p1 p2 p3, Preverse_go (p2 ++ p3) p1 = p2 ++ Preverse_go p3 p1).
{ by intros go p3; induction p3; intros p1 p2; simpl; auto; rewrite <-?go. }
intros p1; induction p1 as [p1 IH|p1 IH|]; intros p2 p3; simpl; auto.
- * apply (IH _ (_~1)).
- * apply (IH _ (_~0)).
+ - apply (IH _ (_~1)).
+ - apply (IH _ (_~0)).
Qed.
Lemma Preverse_app p1 p2 : Preverse (p1 ++ p2) = Preverse p2 ++ Preverse p1.
Proof. unfold Preverse. by rewrite Preverse_go_app. Qed.
@@ -283,11 +283,11 @@ Qed.
Lemma Nat2Z_divide n m : (Z.of_nat n | Z.of_nat m) ↔ (n | m)%nat.
Proof.
split.
- * rewrite <-(Nat2Z.id m) at 2; intros [i ->]; exists (Z.to_nat i).
+ - rewrite <-(Nat2Z.id m) at 2; intros [i ->]; exists (Z.to_nat i).
destruct (decide (0 ≤ i)%Z).
{ by rewrite Z2Nat.inj_mul, Nat2Z.id by lia. }
by rewrite !Z_to_nat_nonpos by auto using Z.mul_nonpos_nonneg with lia.
- * intros [i ->]. exists (Z.of_nat i). by rewrite Nat2Z.inj_mul.
+ - intros [i ->]. exists (Z.of_nat i). by rewrite Nat2Z.inj_mul.
Qed.
Lemma Z2Nat_divide n m :
0 ≤ n → 0 ≤ m → (Z.to_nat n | Z.to_nat m)%nat ↔ (n | m).
@@ -360,8 +360,8 @@ Proof. split; auto using Qclt_not_le, Qcnot_le_lt. Qed.
Lemma Qcplus_le_mono_l (x y z : Qc) : x ≤ y ↔ z + x ≤ z + y.
Proof.
split; intros.
- * by apply Qcplus_le_compat.
- * replace x with ((0 - z) + (z + x)) by ring.
+ - by apply Qcplus_le_compat.
+ - replace x with ((0 - z) + (z + x)) by ring.
replace y with ((0 - z) + (z + y)) by ring.
by apply Qcplus_le_compat.
Qed.
diff --git a/theories/option.v b/theories/option.v
index e7f14fd1..c7f8ffec 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -94,9 +94,9 @@ Section setoids.
Global Instance option_equivalence : Equivalence ((≡) : relation (option A)).
Proof.
split.
- * by intros []; constructor.
- * by destruct 1; constructor.
- * destruct 1; inversion 1; constructor; etransitivity; eauto.
+ - by intros []; constructor.
+ - by destruct 1; constructor.
+ - destruct 1; inversion 1; constructor; etransitivity; eauto.
Qed.
Global Instance Some_proper : Proper ((≡) ==> (≡)) (@Some A).
Proof. by constructor. Qed.
diff --git a/theories/orders.v b/theories/orders.v
index cf17a85d..2bb3a1aa 100644
--- a/theories/orders.v
+++ b/theories/orders.v
@@ -49,8 +49,8 @@ Section orders.
Lemma strict_spec_alt `{!AntiSymm (=) R} X Y : X ⊂ Y ↔ X ⊆ Y ∧ X ≠Y.
Proof.
split.
- * intros [? HYX]. split. done. by intros <-.
- * intros [? HXY]. split. done. by contradict HXY; apply (anti_symm R).
+ - intros [? HYX]. split. done. by intros <-.
+ - intros [? HXY]. split. done. by contradict HXY; apply (anti_symm R).
Qed.
Lemma po_eq_dec `{!PartialOrder R, ∀ X Y, Decision (X ⊆ Y)} (X Y : A) :
Decision (X = Y).
@@ -242,8 +242,8 @@ Section merge_sort_correct.
revert l2. induction l1 as [|x1 l1 IH1]; intros l2;
induction l2 as [|x2 l2 IH2]; rewrite ?list_merge_cons; simpl;
repeat case_decide; auto.
- * by rewrite (right_id_L [] (++)).
- * by rewrite IH2, Permutation_middle.
+ - by rewrite (right_id_L [] (++)).
+ - by rewrite IH2, Permutation_middle.
Qed.
Local Notation stack := (list (option (list A))).
@@ -292,8 +292,8 @@ Section merge_sort_correct.
merge_sort_aux R st l ≡ₚ merge_stack_flatten st ++ l.
Proof.
revert st. induction l as [|?? IH]; simpl; intros.
- * by rewrite (right_id_L [] (++)), merge_stack_Permutation.
- * rewrite IH, merge_list_to_stack_Permutation; simpl.
+ - by rewrite (right_id_L [] (++)), merge_stack_Permutation.
+ - rewrite IH, merge_list_to_stack_Permutation; simpl.
by rewrite Permutation_middle.
Qed.
Lemma Sorted_merge_sort l : Sorted R (merge_sort R l).
@@ -317,21 +317,21 @@ Section preorder.
Instance preorder_equivalence: @Equivalence A (≡).
Proof.
split.
- * done.
- * by intros ?? [??].
- * by intros X Y Z [??] [??]; split; transitivity Y.
+ - done.
+ - by intros ?? [??].
+ - by intros X Y Z [??] [??]; split; transitivity Y.
Qed.
Global Instance: Proper ((≡) ==> (≡) ==> iff) ((⊆) : relation A).
Proof.
unfold equiv, preorder_equiv. intros X1 Y1 ? X2 Y2 ?. split; intro.
- * transitivity X1. tauto. transitivity X2; tauto.
- * transitivity Y1. tauto. transitivity Y2; tauto.
+ - transitivity X1. tauto. transitivity X2; tauto.
+ - transitivity Y1. tauto. transitivity Y2; tauto.
Qed.
Lemma subset_spec (X Y : A) : X ⊂ Y ↔ X ⊆ Y ∧ X ≢ Y.
Proof.
split.
- * intros [? HYX]. split. done. contradict HYX. by rewrite <-HYX.
- * intros [? HXY]. split. done. by contradict HXY.
+ - intros [? HYX]. split. done. contradict HYX. by rewrite <-HYX.
+ - intros [? HXY]. split. done. by contradict HXY.
Qed.
Section dec.
@@ -435,15 +435,15 @@ Section join_semi_lattice.
Lemma empty_union X Y : X ∪ Y ≡ ∅ ↔ X ≡ ∅ ∧ Y ≡ ∅.
Proof.
split.
- * intros HXY. split; apply equiv_empty;
+ - intros HXY. split; apply equiv_empty;
by transitivity (X ∪ Y); [auto | rewrite HXY].
- * intros [HX HY]. by rewrite HX, HY, (left_id _ _).
+ - intros [HX HY]. by rewrite HX, HY, (left_id _ _).
Qed.
Lemma empty_union_list Xs : ⋃ Xs ≡ ∅ ↔ Forall (≡ ∅) Xs.
Proof.
split.
- * induction Xs; simpl; rewrite ?empty_union; intuition.
- * induction 1 as [|?? E1 ? E2]; simpl. done. by apply empty_union.
+ - induction Xs; simpl; rewrite ?empty_union; intuition.
+ - induction 1 as [|?? E1 ? E2]; simpl. done. by apply empty_union.
Qed.
Section leibniz.
@@ -562,20 +562,20 @@ Section lattice.
split; [apply union_least|apply lattice_distr].
{ apply intersection_greatest; auto using union_subseteq_l. }
apply intersection_greatest.
- * apply union_subseteq_r_transitive, intersection_subseteq_l.
- * apply union_subseteq_r_transitive, intersection_subseteq_r.
+ - apply union_subseteq_r_transitive, intersection_subseteq_l.
+ - apply union_subseteq_r_transitive, intersection_subseteq_r.
Qed.
Lemma union_intersection_r (X Y Z : A) : (X ∩ Y) ∪ Z ≡ (X ∪ Z) ∩ (Y ∪ Z).
Proof. by rewrite !(comm _ _ Z), union_intersection_l. Qed.
Lemma intersection_union_l (X Y Z : A) : X ∩ (Y ∪ Z) ≡ (X ∩ Y) ∪ (X ∩ Z).
Proof.
split.
- * rewrite union_intersection_l.
+ - rewrite union_intersection_l.
apply intersection_greatest.
{ apply union_subseteq_r_transitive, intersection_subseteq_l. }
rewrite union_intersection_r.
apply intersection_preserving; auto using union_subseteq_l.
- * apply intersection_greatest.
+ - apply intersection_greatest.
{ apply union_least; auto using intersection_subseteq_l. }
apply union_least.
+ apply intersection_subseteq_r_transitive, union_subseteq_l.
diff --git a/theories/pmap.v b/theories/pmap.v
index 5875a799..8dc8ae4e 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -117,9 +117,9 @@ Lemma Pmap_wf_eq {A} (t1 t2 : Pmap_raw A) :
Proof.
revert t2.
induction t1 as [|o1 l1 IHl r1 IHr]; intros [|o2 l2 r2] Ht ??; simpl; auto.
- * discriminate (Pmap_wf_canon (PNode o2 l2 r2)); eauto.
- * discriminate (Pmap_wf_canon (PNode o1 l1 r1)); eauto.
- * f_equal; [apply (Ht 1)| |].
+ - discriminate (Pmap_wf_canon (PNode o2 l2 r2)); eauto.
+ - discriminate (Pmap_wf_canon (PNode o1 l1 r1)); eauto.
+ - f_equal; [apply (Ht 1)| |].
+ apply IHl; try apply (λ x, Ht (x~0)); eauto.
+ apply IHr; try apply (λ x, Ht (x~1)); eauto.
Qed.
@@ -133,8 +133,8 @@ Lemma Ppartial_alter_wf {A} f i (t : Pmap_raw A) :
Pmap_wf t → Pmap_wf (Ppartial_alter_raw f i t).
Proof.
revert i; induction t as [|o l IHl r IHr]; intros i ?; simpl.
- * destruct (f None); auto using Psingleton_wf.
- * destruct i; simpl; eauto.
+ - destruct (f None); auto using Psingleton_wf.
+ - destruct i; simpl; eauto.
Qed.
Lemma Pfmap_wf {A B} (f : A → B) t : Pmap_wf t → Pmap_wf (Pfmap_raw f t).
Proof.
@@ -157,15 +157,15 @@ Lemma Plookup_alter {A} f i (t : Pmap_raw A) :
Ppartial_alter_raw f i t !! i = f (t !! i).
Proof.
revert i; induction t as [|o l IHl r IHr]; intros i; simpl.
- * by destruct (f None); rewrite ?Plookup_singleton.
- * destruct i; simpl; rewrite PNode_lookup; simpl; auto.
+ - by destruct (f None); rewrite ?Plookup_singleton.
+ - destruct i; simpl; rewrite PNode_lookup; simpl; auto.
Qed.
Lemma Plookup_alter_ne {A} f i j (t : Pmap_raw A) :
i ≠j → Ppartial_alter_raw f i t !! j = t !! j.
Proof.
revert i j; induction t as [|o l IHl r IHr]; simpl.
- * by intros; destruct (f None); rewrite ?Plookup_singleton_ne.
- * by intros [?|?|] [?|?|] ?; simpl; rewrite ?PNode_lookup; simpl; auto.
+ - by intros; destruct (f None); rewrite ?Plookup_singleton_ne.
+ - by intros [?|?|] [?|?|] ?; simpl; rewrite ?PNode_lookup; simpl; auto.
Qed.
Lemma Plookup_fmap {A B} (f : A → B) t i : (Pfmap_raw f t) !! i = f <$> t !! i.
Proof. revert i. by induction t; intros [?|?|]; simpl. Qed.
@@ -175,14 +175,14 @@ Lemma Pelem_of_to_list {A} (t : Pmap_raw A) j i acc x :
Proof.
split.
{ revert j acc. induction t as [|[y|] l IHl r IHr]; intros j acc; simpl.
- * by right.
- * rewrite elem_of_cons. intros [?|?]; simplify_equality.
+ - by right.
+ - rewrite elem_of_cons. intros [?|?]; simplify_equality.
{ left; exists 1. by rewrite (left_id_L 1 (++))%positive. }
destruct (IHl (j~0) (Pto_list_raw j~1 r acc)) as [(i'&->&?)|?]; auto.
{ left; exists (i' ~ 0). by rewrite Preverse_xO, (assoc_L _). }
destruct (IHr (j~1) acc) as [(i'&->&?)|?]; auto.
left; exists (i' ~ 1). by rewrite Preverse_xI, (assoc_L _).
- * intros.
+ - intros.
destruct (IHl (j~0) (Pto_list_raw j~1 r acc)) as [(i'&->&?)|?]; auto.
{ left; exists (i' ~ 0). by rewrite Preverse_xO, (assoc_L _). }
destruct (IHr (j~1) acc) as [(i'&->&?)|?]; auto.
@@ -193,14 +193,14 @@ Proof.
simpl; rewrite ?elem_of_cons; auto. }
intros t j ? acc [(i&->&Hi)|?]; [|by auto]. revert j i acc Hi.
induction t as [|[y|] l IHl r IHr]; intros j i acc ?; simpl.
- * done.
- * rewrite elem_of_cons. destruct i as [i|i|]; simplify_equality'.
+ - done.
+ - rewrite elem_of_cons. destruct i as [i|i|]; simplify_equality'.
+ right. apply help. specialize (IHr (j~1) i).
rewrite Preverse_xI, (assoc_L _) in IHr. by apply IHr.
+ right. specialize (IHl (j~0) i).
rewrite Preverse_xO, (assoc_L _) in IHl. by apply IHl.
+ left. by rewrite (left_id_L 1 (++))%positive.
- * destruct i as [i|i|]; simplify_equality'.
+ - destruct i as [i|i|]; simplify_equality'.
+ apply help. specialize (IHr (j~1) i).
rewrite Preverse_xI, (assoc_L _) in IHr. by apply IHr.
+ specialize (IHl (j~0) i).
@@ -211,8 +211,8 @@ Lemma Pto_list_nodup {A} j (t : Pmap_raw A) acc :
NoDup acc → NoDup (Pto_list_raw j t acc).
Proof.
revert j acc. induction t as [|[y|] l IHl r IHr]; simpl; intros j acc Hin ?.
- * done.
- * repeat constructor.
+ - done.
+ - repeat constructor.
{ rewrite Pelem_of_to_list. intros [(i&Hi&?)|Hj].
{ apply (f_equal Plength) in Hi.
rewrite Preverse_xO, !Papp_length in Hi; simpl in *; lia. }
@@ -221,20 +221,20 @@ Proof.
rewrite Preverse_xI, !Papp_length in Hi; simpl in *; lia. }
specialize (Hin 1 y). rewrite (left_id_L 1 (++))%positive in Hin.
discriminate (Hin Hj). }
- apply IHl.
- { intros i x. rewrite Pelem_of_to_list. intros [(?&Hi&?)|Hi].
- + rewrite Preverse_xO, Preverse_xI, !(assoc_L _) in Hi.
- by apply (inj (++ _)) in Hi.
- + apply (Hin (i~0) x). by rewrite Preverse_xO, (assoc_L _) in Hi. }
- apply IHr; auto. intros i x Hi.
- apply (Hin (i~1) x). by rewrite Preverse_xI, (assoc_L _) in Hi.
- * apply IHl.
- { intros i x. rewrite Pelem_of_to_list. intros [(?&Hi&?)|Hi].
- + rewrite Preverse_xO, Preverse_xI, !(assoc_L _) in Hi.
- by apply (inj (++ _)) in Hi.
- + apply (Hin (i~0) x). by rewrite Preverse_xO, (assoc_L _) in Hi. }
- apply IHr; auto. intros i x Hi.
- apply (Hin (i~1) x). by rewrite Preverse_xI, (assoc_L _) in Hi.
+ apply IHl.
+ { intros i x. rewrite Pelem_of_to_list. intros [(?&Hi&?)|Hi].
+ + rewrite Preverse_xO, Preverse_xI, !(assoc_L _) in Hi.
+ by apply (inj (++ _)) in Hi.
+ + apply (Hin (i~0) x). by rewrite Preverse_xO, (assoc_L _) in Hi. }
+ apply IHr; auto. intros i x Hi.
+ apply (Hin (i~1) x). by rewrite Preverse_xI, (assoc_L _) in Hi.
+ - apply IHl.
+ { intros i x. rewrite Pelem_of_to_list. intros [(?&Hi&?)|Hi].
+ + rewrite Preverse_xO, Preverse_xI, !(assoc_L _) in Hi.
+ by apply (inj (++ _)) in Hi.
+ + apply (Hin (i~0) x). by rewrite Preverse_xO, (assoc_L _) in Hi. }
+ apply IHr; auto. intros i x Hi.
+ apply (Hin (i~1) x). by rewrite Preverse_xI, (assoc_L _) in Hi.
Qed.
Lemma Pomap_lookup {A B} (f : A → option B) t i :
Pomap_raw f t !! i = t !! i ≫= f.
@@ -250,9 +250,9 @@ Proof.
{ rewrite Pomap_lookup. by destruct (t2 !! i). }
unfold compose, flip.
destruct t2 as [|l2 o2 r2]; rewrite PNode_lookup.
- * by destruct i; rewrite ?Pomap_lookup; simpl; rewrite ?Pomap_lookup;
+ - by destruct i; rewrite ?Pomap_lookup; simpl; rewrite ?Pomap_lookup;
match goal with |- ?o ≫= _ = _ => destruct o end.
- * destruct i; rewrite ?Pomap_lookup; simpl; auto.
+ - destruct i; rewrite ?Pomap_lookup; simpl; auto.
Qed.
(** Packed version and instance of the finite map type class *)
@@ -288,18 +288,18 @@ Instance Pmerge : Merge Pmap := λ A B C f m1 m2,
Instance Pmap_finmap : FinMap positive Pmap.
Proof.
split.
- * by intros ? [t1 ?] [t2 ?] ?; apply Pmap_eq, Pmap_wf_eq.
- * by intros ? [].
- * intros ?? [??] ?. by apply Plookup_alter.
- * intros ?? [??] ??. by apply Plookup_alter_ne.
- * intros ??? [??]. by apply Plookup_fmap.
- * intros ? [??]. apply Pto_list_nodup; [|constructor].
+ - by intros ? [t1 ?] [t2 ?] ?; apply Pmap_eq, Pmap_wf_eq.
+ - by intros ? [].
+ - intros ?? [??] ?. by apply Plookup_alter.
+ - intros ?? [??] ??. by apply Plookup_alter_ne.
+ - intros ??? [??]. by apply Plookup_fmap.
+ - intros ? [??]. apply Pto_list_nodup; [|constructor].
intros ??. by rewrite elem_of_nil.
- * intros ? [??] i x; unfold map_to_list, Pto_list.
+ - intros ? [??] i x; unfold map_to_list, Pto_list.
rewrite Pelem_of_to_list, elem_of_nil.
split. by intros [(?&->&?)|]. by left; exists i.
- * intros ?? ? [??] ?. by apply Pomap_lookup.
- * intros ??? ?? [??] [??] ?. by apply Pmerge_lookup.
+ - intros ?? ? [??] ?. by apply Pomap_lookup.
+ - intros ??? ?? [??] [??] ?. by apply Pmerge_lookup.
Qed.
(** * Finite sets *)
@@ -365,8 +365,8 @@ Instance Pset_fresh : Fresh positive Pset := λ X,
Instance Pset_fresh_spec : FreshSpec positive Pset.
Proof.
split.
- * apply _.
- * intros X Y; rewrite <-elem_of_equiv_L. by intros ->.
- * unfold elem_of, mapset_elem_of, fresh; intros [m]; simpl.
+ - apply _.
+ - intros X Y; rewrite <-elem_of_equiv_L. by intros ->.
+ - unfold elem_of, mapset_elem_of, fresh; intros [m]; simpl.
by rewrite Pfresh_fresh.
Qed.
diff --git a/theories/relations.v b/theories/relations.v
index aa94487f..4cad9eac 100644
--- a/theories/relations.v
+++ b/theories/relations.v
@@ -142,9 +142,9 @@ Section rtc.
intros n p1 H. rewrite <-plus_n_Sm.
apply (IH (S n)); [by eauto using bsteps_r |].
intros [|m'] [??]; [lia |]. apply Pstep with x'.
- * apply bsteps_weaken with n; intuition lia.
- * done.
- * apply H; intuition lia.
+ - apply bsteps_weaken with n; intuition lia.
+ - done.
+ - apply H; intuition lia.
Qed.
Lemma tc_transitive x y z : tc R x y → tc R y z → tc R x z.
diff --git a/theories/streams.v b/theories/streams.v
index 8fe09cc5..04a52b82 100644
--- a/theories/streams.v
+++ b/theories/streams.v
@@ -40,9 +40,9 @@ Proof. by constructor. Qed.
Global Instance equal_equivalence : Equivalence (@equiv (stream A) _).
Proof.
split.
- * now cofix; intros [??]; constructor.
- * now cofix; intros ?? [??]; constructor.
- * cofix; intros ??? [??] [??]; constructor; etransitivity; eauto.
+ - now cofix; intros [??]; constructor.
+ - now cofix; intros ?? [??]; constructor.
+ - cofix; intros ??? [??] [??]; constructor; etransitivity; eauto.
Qed.
Global Instance scons_proper x : Proper ((≡) ==> (≡)) (scons x).
Proof. by constructor. Qed.
diff --git a/theories/vector.v b/theories/vector.v
index 18547be4..445a383e 100644
--- a/theories/vector.v
+++ b/theories/vector.v
@@ -87,8 +87,8 @@ Fixpoint fin_enum (n : nat) : list (fin n) :=
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 (NoDup_fmap _).
+ - rewrite elem_of_list_fmap. by intros (?&?&?).
+ - by apply (NoDup_fmap _).
Qed.
Next Obligation.
intros n i. induction i as [|n i IH]; simpl;
@@ -148,8 +148,8 @@ Proof. apply vcons_inj. Qed.
Lemma vec_eq {A n} (v w : vec A n) : (∀ i, v !!! i = w !!! i) → v = w.
Proof.
vec_double_ind v w; [done|]. intros n v w IH x y Hi. f_equal.
- * apply (Hi 0%fin).
- * apply IH. intros i. apply (Hi (FS i)).
+ - apply (Hi 0%fin).
+ - apply IH. intros i. apply (Hi (FS i)).
Qed.
Instance vec_dec {A} {dec : ∀ x y : A, Decision (x = y)} {n} :
@@ -238,8 +238,8 @@ Proof.
rewrite <-vec_to_list_cons, <-vec_to_list_app in H.
pose proof (vec_to_list_inj1 _ _ H); subst.
apply vec_to_list_inj2 in H; subst. induction l. simpl.
- * eexists 0%fin. simpl. by rewrite vec_to_list_of_list.
- * destruct IHl as [i ?]. exists (FS i). simpl. intuition congruence.
+ - eexists 0%fin. simpl. by rewrite vec_to_list_of_list.
+ - destruct IHl as [i ?]. exists (FS i). simpl. intuition congruence.
Qed.
Lemma vec_to_list_drop_lookup {A n} (v : vec A n) (i : fin n) :
drop i v = v !!! i :: drop (S i) v.
@@ -252,10 +252,10 @@ Lemma elem_of_vlookup {A n} (v : vec A n) x :
x ∈ vec_to_list v ↔ ∃ i, v !!! i = x.
Proof.
split.
- * induction v; simpl; [by rewrite elem_of_nil |].
+ - induction v; simpl; [by rewrite elem_of_nil |].
inversion 1; subst; [by eexists 0%fin|].
destruct IHv as [i ?]; trivial. by exists (FS i).
- * intros [i ?]; subst. induction v as [|??? IH]; inv_fin i; [by left|].
+ - intros [i ?]; subst. induction v as [|??? IH]; inv_fin i; [by left|].
right; apply IH.
Qed.
Lemma Forall_vlookup {A} (P : A → Prop) {n} (v : vec A n) :
@@ -275,10 +275,10 @@ Lemma Forall2_vlookup {A B} (P : A → B → Prop) {n}
Forall2 P (vec_to_list v1) (vec_to_list v2) ↔ ∀ i, P (v1 !!! i) (v2 !!! i).
Proof.
split.
- * vec_double_ind v1 v2; [intros _ i; inv_fin i |].
+ - vec_double_ind v1 v2; [intros _ i; inv_fin i |].
intros n v1 v2 IH a b; simpl. inversion_clear 1.
intros i. inv_fin i; simpl; auto.
- * vec_double_ind v1 v2; [constructor|].
+ - vec_double_ind v1 v2; [constructor|].
intros ??? IH ?? H. constructor. apply (H 0%fin). apply IH, (λ i, H (FS i)).
Qed.
diff --git a/theories/zmap.v b/theories/zmap.v
index d2621ba9..0b14cba4 100644
--- a/theories/zmap.v
+++ b/theories/zmap.v
@@ -52,16 +52,16 @@ Instance Nfmap: FMap Zmap := λ A B f t,
Instance: FinMap Z Zmap.
Proof.
split.
- * intros ? [??] [??] H. f_equal.
+ - intros ? [??] [??] H. f_equal.
+ apply (H 0).
+ apply map_eq. intros i. apply (H (Zpos i)).
+ apply map_eq. intros i. apply (H (Zneg i)).
- * by intros ? [].
- * intros ? f [] [|?|?]; simpl; [done| |]; apply lookup_partial_alter.
- * intros ? f [] [|?|?] [|?|?]; simpl; intuition congruence ||
+ - by intros ? [].
+ - intros ? f [] [|?|?]; simpl; [done| |]; apply lookup_partial_alter.
+ - intros ? f [] [|?|?] [|?|?]; simpl; intuition congruence ||
intros; apply lookup_partial_alter_ne; congruence.
- * intros ??? [??] []; simpl; [done| |]; apply lookup_fmap.
- * intros ? [o t t']; unfold map_to_list; simpl.
+ - intros ??? [??] []; simpl; [done| |]; apply lookup_fmap.
+ - intros ? [o t t']; unfold map_to_list; simpl.
assert (NoDup ((prod_map Z.pos id <$> map_to_list t) ++
prod_map Z.neg id <$> map_to_list t')).
{ apply NoDup_app; split_ands.
@@ -70,24 +70,24 @@ Proof.
- apply (NoDup_fmap_2 _), NoDup_map_to_list. }
destruct o; simpl; auto. constructor; auto.
rewrite elem_of_app, !elem_of_list_fmap. naive_solver.
- * intros ? t i x. unfold map_to_list. split.
+ - intros ? t i x. unfold map_to_list. split.
+ destruct t as [[y|] t t']; simpl.
- - rewrite elem_of_cons, elem_of_app, !elem_of_list_fmap.
+ * rewrite elem_of_cons, elem_of_app, !elem_of_list_fmap.
intros [?|[[[??][??]]|[[??][??]]]]; simplify_equality'; [done| |];
by apply elem_of_map_to_list.
- - rewrite elem_of_app, !elem_of_list_fmap. intros [[[??][??]]|[[??][??]]];
+ * rewrite elem_of_app, !elem_of_list_fmap. intros [[[??][??]]|[[??][??]]];
simplify_equality'; by apply elem_of_map_to_list.
+ destruct t as [[y|] t t']; simpl.
- - rewrite elem_of_cons, elem_of_app, !elem_of_list_fmap.
+ * rewrite elem_of_cons, elem_of_app, !elem_of_list_fmap.
destruct i as [|i|i]; simpl; [intuition congruence| |].
{ right; left. exists (i, x). by rewrite elem_of_map_to_list. }
right; right. exists (i, x). by rewrite elem_of_map_to_list.
- - rewrite elem_of_app, !elem_of_list_fmap.
+ * rewrite elem_of_app, !elem_of_list_fmap.
destruct i as [|i|i]; simpl; [done| |].
{ left; exists (i, x). by rewrite elem_of_map_to_list. }
right; exists (i, x). by rewrite elem_of_map_to_list.
- * intros ?? f [??] [|?|?]; simpl; [done| |]; apply (lookup_omap f).
- * intros ??? f ? [??] [??] [|?|?]; simpl; [done| |]; apply (lookup_merge f).
+ - intros ?? f [??] [|?|?]; simpl; [done| |]; apply (lookup_omap f).
+ - intros ??? f ? [??] [??] [|?|?]; simpl; [done| |]; apply (lookup_merge f).
Qed.
(** * Finite sets *)
--
GitLab