From 20690605ffbf5709b5760560167e3adf9fa0602b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 17 Feb 2016 16:21:26 +0100
Subject: [PATCH] Rename simplify_equality like tactics.
simplify_equality => simplify_eq
simplify_equality' => simplify_eq/=
simplify_map_equality => simplify_map_eq
simplify_map_equality' => simplify_map_eq/=
simplify_option_equality => simplify_option_eq
simplify_list_equality => simplify_list_eq
f_equal' => f_equal/=
The /= suffixes (meaning: do simpl) are inspired by ssreflect.
---
theories/co_pset.v | 10 +-
theories/collections.v | 10 +-
theories/countable.v | 16 +-
theories/error.v | 4 +-
theories/fin_collections.v | 2 +-
theories/fin_map_dom.v | 4 +-
theories/fin_maps.v | 56 +++---
theories/finite.v | 18 +-
theories/gmap.v | 16 +-
theories/hashset.v | 14 +-
theories/lexico.v | 2 +-
theories/list.v | 384 ++++++++++++++++++-------------------
theories/listset.v | 2 +-
theories/mapset.v | 2 +-
theories/natmap.v | 10 +-
theories/nmap.v | 4 +-
theories/numbers.v | 8 +-
theories/option.v | 12 +-
theories/orders.v | 4 +-
theories/pmap.v | 14 +-
theories/pretty.v | 2 +-
theories/stringmap.v | 2 +-
theories/strings.v | 4 +-
theories/tactics.v | 16 +-
theories/vector.v | 12 +-
theories/zmap.v | 4 +-
26 files changed, 313 insertions(+), 319 deletions(-)
diff --git a/theories/co_pset.v b/theories/co_pset.v
index a14659a2..82d12f98 100644
--- a/theories/co_pset.v
+++ b/theories/co_pset.v
@@ -120,7 +120,7 @@ Lemma elem_to_Pset_singleton p q : e_of p (coPset_singleton_raw q) ↔ p = q.
Proof.
split; [|by intros <-; induction p; simpl; rewrite ?coPset_elem_of_node].
by revert q; induction p; intros [?|?|]; simpl;
- rewrite ?coPset_elem_of_node; intros; f_equal'; auto.
+ rewrite ?coPset_elem_of_node; intros; f_equal/=; auto.
Qed.
Lemma elem_to_Pset_union t1 t2 p : e_of p (t1 ∪ t2) = e_of p t1 || e_of p t2.
Proof.
@@ -226,13 +226,13 @@ Definition coPpick (X : coPset) : positive := from_option 1 (coPpick_raw (`X)).
Lemma coPpick_raw_elem_of t i : coPpick_raw t = Some i → e_of i t.
Proof.
- revert i; induction t as [[]|[] l ? r]; intros i ?; simplify_equality'; auto.
- destruct (coPpick_raw l); simplify_option_equality; auto.
+ revert i; induction t as [[]|[] l ? r]; intros i ?; simplify_eq/=; auto.
+ destruct (coPpick_raw l); simplify_option_eq; auto.
Qed.
Lemma coPpick_raw_None t : coPpick_raw t = None → coPset_finite t.
Proof.
- induction t as [[]|[] l ? r]; intros i; simplify_equality'; auto.
- destruct (coPpick_raw l); simplify_option_equality; auto.
+ induction t as [[]|[] l ? r]; intros i; simplify_eq/=; auto.
+ destruct (coPpick_raw l); simplify_option_eq; auto.
Qed.
Lemma coPpick_elem_of X : ¬set_finite X → coPpick X ∈ X.
Proof.
diff --git a/theories/collections.v b/theories/collections.v
index 3cb2d5bd..bafb7ed5 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -359,9 +359,9 @@ Section collection_ops.
- 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).
+ eexists (x1 :: xs), y. intuition (simplify_option_eq; auto).
- intros (xs & y & Hxs & ? & Hx). revert x Hx.
- induction Hxs; intros; simplify_option_equality; [done |].
+ induction Hxs; intros; simplify_option_eq; [done |].
rewrite elem_of_intersection_with. naive_solver.
Qed.
@@ -371,7 +371,7 @@ Section collection_ops.
(∀ x y z, Q x → P y → f x y = Some z → P z) →
∀ x, x ∈ intersection_with_list f Y Xs → P x.
Proof.
- intros HY HXs Hf. induction Xs; simplify_option_equality; [done |].
+ intros HY HXs Hf. induction Xs; simplify_option_eq; [done |].
intros x Hx. rewrite elem_of_intersection_with in Hx.
decompose_Forall. destruct Hx as (? & ? & ? & ? & ?). eauto.
Qed.
@@ -490,7 +490,7 @@ Section fresh.
Global Instance fresh_list_proper:
Proper ((=) ==> (≡) ==> (=)) (fresh_list (C:=C)).
Proof.
- intros ? n ->. induction n as [|n IH]; intros ?? E; f_equal'; [by rewrite E|].
+ intros ? n ->. induction n as [|n IH]; intros ?? E; f_equal/=; [by rewrite E|].
apply IH. by rewrite E.
Qed.
@@ -585,7 +585,7 @@ Section collection_monad.
Forall (λ x, ∀ y, y ∈ g x → f y = x) l → k ∈ mapM g l → fmap f k = l.
Proof.
intros Hl. revert k. induction Hl; simpl; intros;
- decompose_elem_of; f_equal'; auto.
+ decompose_elem_of; f_equal/=; auto.
Qed.
Lemma elem_of_mapM_Forall {A B} (f : A → M B) (P : B → Prop) l k :
l ∈ mapM f k → Forall (λ x, ∀ y, y ∈ f x → P y) k → Forall P l.
diff --git a/theories/countable.v b/theories/countable.v
index 9a5808b5..879885f0 100644
--- a/theories/countable.v
+++ b/theories/countable.v
@@ -149,18 +149,18 @@ Fixpoint prod_decode_snd (p : positive) : option positive :=
Lemma prod_decode_encode_fst p q : prod_decode_fst (prod_encode p q) = Some p.
Proof.
assert (∀ p, prod_decode_fst (prod_encode_fst p) = Some p).
- { intros p'. by induction p'; simplify_option_equality. }
+ { intros p'. by induction p'; simplify_option_eq. }
assert (∀ p, prod_decode_fst (prod_encode_snd p) = None).
- { intros p'. by induction p'; simplify_option_equality. }
- revert q. by induction p; intros [?|?|]; simplify_option_equality.
+ { intros p'. by induction p'; simplify_option_eq. }
+ revert q. by induction p; intros [?|?|]; simplify_option_eq.
Qed.
Lemma prod_decode_encode_snd p q : prod_decode_snd (prod_encode p q) = Some q.
Proof.
assert (∀ p, prod_decode_snd (prod_encode_snd p) = Some p).
- { intros p'. by induction p'; simplify_option_equality. }
+ { intros p'. by induction p'; simplify_option_eq. }
assert (∀ p, prod_decode_snd (prod_encode_fst p) = None).
- { intros p'. by induction p'; simplify_option_equality. }
- revert q. by induction p; intros [?|?|]; simplify_option_equality.
+ { intros p'. by induction p'; simplify_option_eq. }
+ revert q. by induction p; intros [?|?|]; simplify_option_eq.
Qed.
Program Instance prod_countable `{Countable A} `{Countable B} :
Countable (A * B)%type := {|
@@ -191,7 +191,7 @@ Fixpoint list_decode `{Countable A} (acc : list A)
| p~1 => x ↠decode_nat n; list_decode (x :: acc) O p
end.
Lemma x0_iter_x1 n acc : Nat.iter n (~0) acc~1 = acc ++ Nat.iter n (~0) 3.
-Proof. by induction n; f_equal'. Qed.
+Proof. by induction n; f_equal/=. Qed.
Lemma list_encode_app' `{Countable A} (l1 l2 : list A) acc :
list_encode acc (l1 ++ l2) = list_encode acc l1 ++ list_encode 1 l2.
Proof.
@@ -226,7 +226,7 @@ Lemma list_encode_suffix_eq `{Countable A} q1 q2 (l1 l2 : list A) :
length l1 = length l2 → q1 ++ encode l1 = q2 ++ encode l2 → l1 = l2.
Proof.
revert q1 q2 l2; induction l1 as [|a1 l1 IH];
- intros q1 q2 [|a2 l2] ?; simplify_equality'; auto.
+ intros q1 q2 [|a2 l2] ?; simplify_eq/=; auto.
rewrite !list_encode_cons, !(assoc _); intros Hl.
assert (l1 = l2) as <- by eauto; clear IH; f_equal.
apply (inj encode_nat); apply (inj (++ encode l1)) in Hl; revert Hl; clear.
diff --git a/theories/error.v b/theories/error.v
index 6a6ddbdb..47374889 100644
--- a/theories/error.v
+++ b/theories/error.v
@@ -87,7 +87,7 @@ Tactic Notation "simplify_error_equality" :=
| H : (gets _ ≫= _) _ = _ |- _ => rewrite error_left_gets in H
| H : (modify _ ≫= _) _ = _ |- _ => rewrite error_left_modify in H
| H : error_guard _ _ _ _ = _ |- _ => apply error_guard_ret in H; destruct H
- | _ => progress simplify_equality'
+ | _ => progress simplify_eq/=
| H : error_of_option _ _ _ = _ |- _ =>
apply error_of_option_ret in H; destruct H
| H : mbind (M:=error _ _) _ _ _ = _ |- _ =>
@@ -117,7 +117,7 @@ Tactic Notation "error_proceed" :=
| H : ((_ ≫= _) ≫= _) _ = _ |- _ => rewrite error_assoc in H
| H : (error_guard _ _ _) _ = _ |- _ =>
let H' := fresh in apply error_guard_ret in H; destruct H as [H' H]
- | _ => progress simplify_equality'
+ | _ => progress simplify_eq/=
| H : maybe _ ?x = Some _ |- _ => is_var x; destruct x
| H : maybe2 _ ?x = Some _ |- _ => is_var x; destruct x
| H : maybe3 _ ?x = Some _ |- _ => is_var x; destruct x
diff --git a/theories/fin_collections.v b/theories/fin_collections.v
index 59a8b55c..87400877 100644
--- a/theories/fin_collections.v
+++ b/theories/fin_collections.v
@@ -67,7 +67,7 @@ Proof. unfold size, collection_size. simpl. by rewrite elements_singleton. Qed.
Lemma size_singleton_inv X x y : size X = 1 → x ∈ X → y ∈ X → x = y.
Proof.
unfold size, collection_size. simpl. rewrite <-!elem_of_elements.
- generalize (elements X). intros [|? l]; intro; simplify_equality'.
+ generalize (elements X). intros [|? l]; intro; simplify_eq/=.
rewrite (nil_length_inv l), !elem_of_list_singleton by done; congruence.
Qed.
Lemma collection_choose_or_empty X : (∃ x, x ∈ X) ∨ X ≡ ∅.
diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index 311b0cd7..9b2245d4 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -32,7 +32,7 @@ Proof.
intros [Hss1 Hss2]; split; [by apply subseteq_dom |].
contradict Hss2. rewrite map_subseteq_spec. intros i x Hi.
specialize (Hss2 i). rewrite !elem_of_dom in Hss2.
- destruct Hss2; eauto. by simplify_map_equality.
+ destruct Hss2; eauto. by simplify_map_eq.
Qed.
Lemma dom_empty {A} : dom D (@empty (M A) _) ≡ ∅.
Proof.
@@ -47,7 +47,7 @@ Qed.
Lemma dom_alter {A} f (m : M A) i : dom D (alter f i m) ≡ dom D m.
Proof.
apply elem_of_equiv; intros j; rewrite !elem_of_dom; unfold is_Some.
- destruct (decide (i = j)); simplify_map_equality'; eauto.
+ destruct (decide (i = j)); simplify_map_eq/=; eauto.
destruct (m !! j); naive_solver.
Qed.
Lemma dom_insert {A} (m : M A) i x : dom D (<[i:=x]>m) ≡ {[ i ]} ∪ dom D m.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 10e76cdf..7ac4cf42 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -198,7 +198,7 @@ Global Instance: ∀ {A} (R : relation A), PreOrder R → PreOrder (map_included
Proof.
split; [intros m i; by destruct (m !! i); simpl|].
intros m1 m2 m3 Hm12 Hm23 i; specialize (Hm12 i); specialize (Hm23 i).
- destruct (m1 !! i), (m2 !! i), (m3 !! i); simplify_equality';
+ destruct (m1 !! i), (m2 !! i), (m3 !! i); simplify_eq/=;
done || etransitivity; eauto.
Qed.
Global Instance: PartialOrder ((⊆) : relation (M A)).
@@ -288,7 +288,7 @@ Qed.
(** ** Properties of the [alter] operation *)
Lemma alter_ext {A} (f g : A → A) (m : M A) i :
(∀ x, m !! i = Some x → f x = g x) → alter f i m = alter g i m.
-Proof. intro. apply partial_alter_ext. intros [x|] ?; f_equal'; auto. Qed.
+Proof. intro. apply partial_alter_ext. intros [x|] ?; f_equal/=; auto. Qed.
Lemma lookup_alter {A} (f : A → A) m i : alter f i m !! i = f <$> m !! i.
Proof. unfold alter. apply lookup_partial_alter. Qed.
Lemma lookup_alter_ne {A} (f : A → A) m i j : i ≠j → alter f i m !! j = m !! j.
@@ -307,7 +307,7 @@ 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. naive_solver (simplify_option_eq; eauto).
- rewrite lookup_alter_ne by done. naive_solver.
Qed.
Lemma lookup_alter_None {A} (f : A → A) m i j :
@@ -320,7 +320,7 @@ Lemma alter_id {A} (f : A → A) m i :
(∀ x, m !! i = Some x → f x = x) → alter f i m = m.
Proof.
intros Hi; apply map_eq; intros j; destruct (decide (i = j)) as [->|?].
- { rewrite lookup_alter; destruct (m !! j); f_equal'; auto. }
+ { rewrite lookup_alter; destruct (m !! j); f_equal/=; auto. }
by rewrite lookup_alter_ne by done.
Qed.
@@ -583,7 +583,7 @@ Lemma elem_of_map_of_list_1_help {A} (l : list (K * A)) i x :
Proof.
induction l as [|[j y] l IH]; csimpl; [by rewrite elem_of_nil|].
setoid_rewrite elem_of_cons.
- intros [?|?] Hdup; simplify_equality; [by rewrite lookup_insert|].
+ intros [?|?] Hdup; simplify_eq; [by rewrite lookup_insert|].
destruct (decide (i = j)) as [->|].
- rewrite lookup_insert; f_equal; eauto.
- rewrite lookup_insert_ne by done; eauto.
@@ -616,7 +616,7 @@ Lemma not_elem_of_map_of_list_2 {A} (l : list (K * A)) i :
map_of_list l !! i = None → i ∉ l.*1.
Proof.
induction l as [|[j y] l IH]; csimpl; [rewrite elem_of_nil; tauto|].
- rewrite elem_of_cons. destruct (decide (i = j)); simplify_equality.
+ rewrite elem_of_cons. destruct (decide (i = j)); simplify_eq.
- by rewrite lookup_insert.
- by rewrite lookup_insert_ne; intuition.
Qed.
@@ -708,16 +708,16 @@ 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_eq/=.
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]. }
+ [by apply elem_of_map_to_list|by simplify_option_eq]. }
intros y'; rewrite elem_of_list_omap; intros ([i' x']&Hi'&?).
- by rewrite elem_of_map_to_list in Hi'; simplify_option_equality.
+ by rewrite elem_of_map_to_list in Hi'; simplify_option_eq.
- apply not_elem_of_map_of_list; rewrite elem_of_list_fmap.
- intros ([i' x]&->&Hi'); simplify_equality'.
+ intros ([i' x]&->&Hi'); simplify_eq/=.
rewrite elem_of_list_omap in Hi'; destruct Hi' as ([j y]&Hj&?).
- rewrite elem_of_map_to_list in Hj; simplify_option_equality.
+ rewrite elem_of_map_to_list in Hj; simplify_option_eq.
Qed.
(** ** Properties of conversion from collections *)
@@ -729,11 +729,11 @@ Proof.
{ induction (NoDup_elements X) as [|i' l]; csimpl; [constructor|].
destruct (f i') as [x'|]; csimpl; auto; constructor; auto.
rewrite elem_of_list_fmap. setoid_rewrite elem_of_list_omap.
- by intros (?&?&?&?&?); simplify_option_equality. }
+ by intros (?&?&?&?&?); simplify_option_eq. }
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_eq; eauto.
+ - intros [??]; exists i; simplify_option_eq; eauto.
Qed.
(** ** Induction principles *)
@@ -936,9 +936,9 @@ Proof.
split.
- 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.
+ simplify_eq/=; auto using bool_decide_pack.
- intros Hm i. specialize (Hm i). rewrite lookup_merge in Hm by done.
- destruct (m1 !! i), (m2 !! i); simplify_equality'; auto;
+ destruct (m1 !! i), (m2 !! i); simplify_eq/=; auto;
by eapply bool_decide_unpack, Hm.
Qed.
Global Instance map_relation_dec `{∀ x y, Decision (R x y), ∀ x, Decision (P x),
@@ -961,7 +961,7 @@ Proof.
destruct (m1 !! i), (m2 !! i); naive_solver auto 2 using bool_decide_pack.
- unfold map_relation, option_relation.
by intros [i[(x&y&?&?&?)|[(x&?&?&?)|(y&?&?&?)]]] Hm;
- specialize (Hm i); simplify_option_equality.
+ specialize (Hm i); simplify_option_eq.
Qed.
End Forall2.
@@ -1081,7 +1081,7 @@ Lemma alter_union_with_l (g : A → A) m1 m2 i :
alter g i (union_with f m1 m2) = union_with f (alter g i m1) m2.
Proof.
intros. apply (partial_alter_merge_l _).
- destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; f_equal'; auto.
+ destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; f_equal/=; auto.
Qed.
Lemma alter_union_with_r (g : A → A) m1 m2 i :
(∀ x y, m1 !! i = Some x → m2 !! i = Some y → g <$> f x y = f x (g y)) →
@@ -1089,7 +1089,7 @@ Lemma alter_union_with_r (g : A → A) m1 m2 i :
alter g i (union_with f m1 m2) = union_with f m1 (alter g i m2).
Proof.
intros. apply (partial_alter_merge_r _).
- destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; f_equal'; auto.
+ destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; f_equal/=; auto.
Qed.
Lemma delete_union_with m1 m2 i :
delete i (union_with f m1 m2) = union_with f (delete i m1) (delete i m2).
@@ -1558,11 +1558,11 @@ Hint Extern 80 (<[_:=_]> _ !! _ = Some _) => apply lookup_insert : simpl_map.
(** Now we take everything together and also discharge conflicting look ups,
simplify overlapping look ups, and perform cancellations of equalities
involving unions. *)
-Tactic Notation "simplify_map_equality" "by" tactic3(tac) :=
+Tactic Notation "simplify_map_eq" "by" tactic3(tac) :=
decompose_map_disjoint;
repeat match goal with
| _ => progress simpl_map by tac
- | _ => progress simplify_equality
+ | _ => progress simplify_eq/=
| _ => progress simpl_option by tac
| H : {[ _ := _ ]} !! _ = None |- _ => rewrite lookup_singleton_None in H
| H : {[ _ := _ ]} !! _ = Some _ |- _ =>
@@ -1582,11 +1582,11 @@ Tactic Notation "simplify_map_equality" "by" tactic3(tac) :=
| H : ∅ = {[?i := ?x]} |- _ => by destruct (map_non_empty_singleton i x)
| H : ?m !! ?i = Some _, H2 : ?m !! ?j = None |- _ =>
unless (i ≠j) by done;
- assert (i ≠j) by (by intros ?; simplify_equality)
+ assert (i ≠j) by (by intros ?; simplify_eq)
end.
-Tactic Notation "simplify_map_equality'" "by" tactic3(tac) :=
- repeat (progress csimpl in * || simplify_map_equality by tac).
-Tactic Notation "simplify_map_equality" :=
- simplify_map_equality by eauto with simpl_map map_disjoint.
-Tactic Notation "simplify_map_equality'" :=
- simplify_map_equality' by eauto with simpl_map map_disjoint.
+Tactic Notation "simplify_map_eq" "/=" "by" tactic3(tac) :=
+ repeat (progress csimpl in * || simplify_map_eq by tac).
+Tactic Notation "simplify_map_eq" :=
+ simplify_map_eq by eauto with simpl_map map_disjoint.
+Tactic Notation "simplify_map_eq" "/=" :=
+ simplify_map_eq/= by eauto with simpl_map map_disjoint.
diff --git a/theories/finite.v b/theories/finite.v
index 26aac4f7..ccb41220 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -48,7 +48,7 @@ Lemma find_Some `{finA: Finite A} P `{∀ x, Decision (P x)} x :
find P = Some x → P x.
Proof.
destruct finA as [xs Hxs HA]; unfold find, decode_nat, decode; simpl.
- intros Hx. destruct (list_find _ _) as [[i y]|] eqn:Hi; simplify_equality'.
+ intros Hx. destruct (list_find _ _) as [[i y]|] eqn:Hi; simplify_eq/=.
rewrite !Nat2Pos.id in Hx by done.
destruct (list_find_Some P xs i y); naive_solver.
Qed.
@@ -57,13 +57,13 @@ Lemma find_is_Some `{finA: Finite A} P `{∀ x, Decision (P x)} x :
Proof.
destruct finA as [xs Hxs HA]; unfold find, decode; simpl.
intros Hx. destruct (list_find_elem_of P xs x) as [[i y] Hi]; auto.
- rewrite Hi. destruct (list_find_Some P xs i y); simplify_equality'; auto.
+ rewrite Hi. destruct (list_find_Some P xs i y); simplify_eq/=; auto.
exists y. by rewrite !Nat2Pos.id by done.
Qed.
Lemma card_0_inv P `{finA: Finite A} : card A = 0 → A → P.
Proof.
- intros ? x. destruct finA as [[|??] ??]; simplify_equality.
+ intros ? x. destruct finA as [[|??] ??]; simplify_eq.
by destruct (not_elem_of_nil x).
Qed.
Lemma finite_inhabited A `{finA: Finite A} : 0 < card A → Inhabited A.
@@ -166,7 +166,7 @@ Section enc_finite.
Next Obligation.
apply NoDup_alt. intros i j x. rewrite !list_lookup_fmap. intros Hi Hj.
destruct (seq _ _ !! i) as [i'|] eqn:Hi',
- (seq _ _ !! j) as [j'|] eqn:Hj'; simplify_equality'.
+ (seq _ _ !! j) as [j'|] eqn:Hj'; simplify_eq/=.
destruct (lookup_seq_inv _ _ _ _ Hi'), (lookup_seq_inv _ _ _ _ Hj'); subst.
rewrite <-(to_of_nat i), <-(to_of_nat j) by done. by f_equal.
Qed.
@@ -239,11 +239,11 @@ Next Obligation.
{ constructor. }
apply NoDup_app; split_ands.
- by apply (NoDup_fmap_2 _), NoDup_enum.
- - intros [? y]. rewrite elem_of_list_fmap. intros (?&?&?); simplify_equality.
+ - intros [? y]. rewrite elem_of_list_fmap. intros (?&?&?); simplify_eq.
clear IH. induction Hxs as [|x' xs ?? IH]; simpl.
{ rewrite elem_of_nil. tauto. }
rewrite elem_of_app, elem_of_list_fmap.
- intros [(?&?&?)|?]; simplify_equality.
+ intros [(?&?&?)|?]; simplify_eq.
+ destruct Hx. by left.
+ destruct IH. by intro; destruct Hx; right. auto.
- done.
@@ -274,15 +274,15 @@ Next Obligation.
apply NoDup_app; split_ands.
- 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.
+ intros ([k2 Hk2]&?&?) Hxk2; simplify_eq/=. destruct Hx. revert Hxk2.
induction xs as [|x' xs IH]; simpl in *; [by rewrite elem_of_nil |].
rewrite elem_of_app, elem_of_list_fmap, elem_of_cons.
- intros [([??]&?&?)|?]; simplify_equality'; auto.
+ intros [([??]&?&?)|?]; simplify_eq/=; auto.
- apply IH.
Qed.
Next Obligation.
intros ???? [l Hl]. revert l Hl.
- induction n as [|n IH]; intros [|x l] ?; simpl; simplify_equality.
+ induction n as [|n IH]; intros [|x l] ?; simpl; simplify_eq.
{ apply elem_of_list_singleton. by apply (sig_eq_pi _). }
revert IH. generalize (list_enum (enum A) n). intros k Hk.
induction (elem_of_enum x) as [x xs|x xs]; simpl in *.
diff --git a/theories/gmap.v b/theories/gmap.v
index ee040a24..9c852ff4 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -19,7 +19,7 @@ Arguments gmap_car {_ _ _ _} _.
Lemma gmap_eq `{Countable K} {A} (m1 m2 : gmap K A) :
m1 = m2 ↔ gmap_car m1 = gmap_car m2.
Proof.
- split; [by intros ->|intros]. destruct m1, m2; simplify_equality'.
+ split; [by intros ->|intros]. destruct m1, m2; simplify_eq/=.
f_equal; apply proof_irrel.
Qed.
Instance gmap_eq_eq `{Countable K} `{∀ x y : A, Decision (x = y)}
@@ -83,9 +83,9 @@ Proof.
apply bool_decide_unpack in Hm1; apply bool_decide_unpack in Hm2.
apply option_eq; intros x; split; intros Hi.
+ pose proof (Hm1 i x Hi); simpl in *.
- by destruct (decode i); simplify_equality'; rewrite <-Hm.
+ by destruct (decode i); simplify_eq/=; rewrite <-Hm.
+ pose proof (Hm2 i x Hi); simpl in *.
- by destruct (decode i); simplify_equality'; rewrite Hm.
+ by destruct (decode i); simplify_eq/=; 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).
@@ -94,16 +94,16 @@ Proof.
- 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|].
- destruct (decode p) as [i|] eqn:?; simplify_equality'; constructor; eauto.
- rewrite elem_of_list_omap; intros ([p' x']&?&?); simplify_equality'.
+ inversion 1 as [|??? Hm']; simplify_eq/=; [by constructor|].
+ destruct (decode p) as [i|] eqn:?; simplify_eq/=; constructor; eauto.
+ rewrite elem_of_list_omap; intros ([p' x']&?&?); simplify_eq/=.
feed pose proof (proj1 (Forall_forall _ _) Hm' (p',x')); simpl in *; auto.
- by destruct (decode p') as [i'|]; simplify_equality'.
+ by destruct (decode p') as [i'|]; simplify_eq/=.
- 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'.
+ by destruct (decode p') as [i'|] eqn:?; simplify_eq/=.
+ 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).
diff --git a/theories/hashset.v b/theories/hashset.v
index 446abf38..bd5884f5 100644
--- a/theories/hashset.v
+++ b/theories/hashset.v
@@ -33,7 +33,7 @@ Program Instance hashset_union: Union (hashset hash) := λ m1 m2,
Hashset (union_with (λ l k, Some (list_union l k)) m1 m2) _.
Next Obligation.
intros _ _ m1 Hm1 m2 Hm2 n l'; rewrite lookup_union_with_Some.
- intros [[??]|[[??]|(l&k&?&?&?)]]; simplify_equality'; auto.
+ intros [[??]|[[??]|(l&k&?&?&?)]]; simplify_eq/=; auto.
split; [apply Forall_list_union|apply NoDup_list_union];
first [by eapply Hm1; eauto | by eapply Hm2; eauto].
Qed.
@@ -43,7 +43,7 @@ Program Instance hashset_intersection: Intersection (hashset hash) := λ m1 m2,
let l' := list_intersection l k in guard (l' ≠[]); Some l') m1 m2) _.
Next Obligation.
intros _ _ m1 Hm1 m2 Hm2 n l'. rewrite lookup_intersection_with_Some.
- intros (?&?&?&?&?); simplify_option_equality.
+ intros (?&?&?&?&?); simplify_option_eq.
split; [apply Forall_list_intersection|apply NoDup_list_intersection];
first [by eapply Hm1; eauto | by eapply Hm2; eauto].
Qed.
@@ -53,7 +53,7 @@ Program Instance hashset_difference: Difference (hashset hash) := λ m1 m2,
let l' := list_difference l k in guard (l' ≠[]); Some l') m1 m2) _.
Next Obligation.
intros _ _ m1 Hm1 m2 Hm2 n l'. rewrite lookup_difference_with_Some.
- intros [[??]|(?&?&?&?&?)]; simplify_option_equality; auto.
+ intros [[??]|(?&?&?&?&?)]; simplify_option_eq; auto.
split; [apply Forall_list_difference|apply NoDup_list_difference];
first [by eapply Hm1; eauto | by eapply Hm2; eauto].
Qed.
@@ -63,7 +63,7 @@ Instance hashset_elems: Elements A (hashset hash) := λ m,
Global Instance: FinCollection A (hashset hash).
Proof.
split; [split; [split| |]| |].
- - intros ? (?&?&?); simplify_map_equality'.
+ - intros ? (?&?&?); simplify_map_eq/=.
- 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. }
@@ -71,7 +71,7 @@ Proof.
- 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.
+ { intros (?&[[]|[[]|(l&k&?&?&?)]]&Hx); simplify_eq/=; eauto.
rewrite elem_of_list_union in Hx; destruct Hx; eauto. }
intros [(l&?&?)|(k&?&?)].
+ destruct (m2 !! hash x) as [k|]; eauto.
@@ -81,7 +81,7 @@ Proof.
- 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.
+ { intros (?&(l&k&?&?&?)&Hx); simplify_option_eq.
rewrite elem_of_list_intersection in Hx; naive_solver. }
intros [(l&?&?) (k&?&?)]. assert (x ∈ list_intersection l k)
by (by rewrite elem_of_list_intersection).
@@ -90,7 +90,7 @@ Proof.
- 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;
+ { intros (l'&[[??]|(l&k&?&?&?)]&Hx); simplify_option_eq;
rewrite ?elem_of_list_difference in Hx; naive_solver. }
intros [(l&?&?) Hm2]; destruct (m2 !! hash x) as [k|] eqn:?; eauto.
destruct (decide (x ∈ k)); [destruct Hm2; eauto|].
diff --git a/theories/lexico.v b/theories/lexico.v
index f2a0f015..f0536131 100644
--- a/theories/lexico.v
+++ b/theories/lexico.v
@@ -41,7 +41,7 @@ Lemma prod_lexico_transitive `{Lexico A, Lexico B, !Transitive (@lexico A _)}
(lexico y1 y2 → lexico y2 y3 → lexico y1 y3) → lexico (x1,y1) (x3,y3).
Proof.
intros Hx12 Hx23 ?; revert Hx12 Hx23. unfold lexico, prod_lexico.
- intros [|[??]] [?|[??]]; simplify_equality'; auto.
+ intros [|[??]] [?|[??]]; simplify_eq/=; auto.
by left; transitivity x2.
Qed.
diff --git a/theories/list.v b/theories/list.v
index ec81c5f6..91675636 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -325,18 +325,16 @@ Section list_set.
End list_set.
(** * Basic tactics on lists *)
-(** The tactic [discriminate_list_equality] discharges a goal if it contains
+(** The tactic [discriminate_list] discharges a goal if it contains
a list equality involving [(::)] and [(++)] of two lists that have a different
length as one of its hypotheses. *)
-Tactic Notation "discriminate_list_equality" hyp(H) :=
+Tactic Notation "discriminate_list" hyp(H) :=
apply (f_equal length) in H;
repeat (csimpl in H || rewrite app_length in H); exfalso; lia.
-Tactic Notation "discriminate_list_equality" :=
- match goal with
- | H : @eq (list _) _ _ |- _ => discriminate_list_equality H
- end.
+Tactic Notation "discriminate_list" :=
+ match goal with H : @eq (list _) _ _ |- _ => discriminate_list H end.
-(** The tactic [simplify_list_equality] simplifies hypotheses involving
+(** The tactic [simplify_list_eq] simplifies hypotheses involving
equalities on lists using injectivity of [(::)] and [(++)]. Also, it simplifies
lookups in singleton lists. *)
Lemma app_inj_1 {A} (l1 k1 l2 k2 : list A) :
@@ -348,9 +346,9 @@ Proof.
intros ? Hl. apply app_inj_1; auto.
apply (f_equal length) in Hl. rewrite !app_length in Hl. lia.
Qed.
-Ltac simplify_list_equality :=
+Ltac simplify_list_eq :=
repeat match goal with
- | _ => progress simplify_equality'
+ | _ => progress simplify_eq/=
| H : _ ++ _ = _ ++ _ |- _ => first
[ apply app_inv_head in H | apply app_inv_tail in H
| apply app_inj_1 in H; [destruct H|done]
@@ -434,13 +432,13 @@ Lemma lookup_tail l i : tail l !! i = l !! S i.
Proof. by destruct l. Qed.
Lemma lookup_lt_Some l i x : l !! i = Some x → i < length l.
Proof.
- revert i. induction l; intros [|?] ?; simplify_equality'; auto with arith.
+ revert i. induction l; intros [|?] ?; simplify_eq/=; auto with arith.
Qed.
Lemma lookup_lt_is_Some_1 l i : is_Some (l !! i) → i < length l.
Proof. intros [??]; eauto using lookup_lt_Some. Qed.
Lemma lookup_lt_is_Some_2 l i : i < length l → is_Some (l !! i).
Proof.
- revert i. induction l; intros [|?] ?; simplify_equality'; eauto with lia.
+ revert i. induction l; intros [|?] ?; simplify_eq/=; eauto with lia.
Qed.
Lemma lookup_lt_is_Some l i : is_Some (l !! i) ↔ i < length l.
Proof. split; auto using lookup_lt_is_Some_1, lookup_lt_is_Some_2. Qed.
@@ -473,7 +471,7 @@ Lemma lookup_app_Some l1 l2 i x :
Proof.
split.
- revert i. induction l1 as [|y l1 IH]; intros [|i] ?;
- simplify_equality'; auto with lia.
+ simplify_eq/=; auto with lia.
destruct (IH i) as [?|[??]]; auto with lia.
- intros [?|[??]]; auto using lookup_app_l_Some. by rewrite lookup_app_r.
Qed.
@@ -482,11 +480,11 @@ Lemma list_lookup_middle l1 l2 x n :
Proof. intros ->. by induction l1. Qed.
Lemma list_insert_alter l i x : <[i:=x]>l = alter (λ _, x) i l.
-Proof. by revert i; induction l; intros []; intros; f_equal'. Qed.
+Proof. by revert i; induction l; intros []; intros; f_equal/=. Qed.
Lemma alter_length f l i : length (alter f i l) = length l.
-Proof. revert i. by induction l; intros [|?]; f_equal'. Qed.
+Proof. revert i. by induction l; intros [|?]; f_equal/=. Qed.
Lemma insert_length l i x : length (<[i:=x]>l) = length l.
-Proof. revert i. by induction l; intros [|?]; f_equal'. Qed.
+Proof. revert i. by induction l; intros [|?]; f_equal/=. Qed.
Lemma list_lookup_alter f l i : alter f i l !! i = f <$> l !! i.
Proof. revert i. induction l. done. intros [|i]. done. apply (IHl i). Qed.
Lemma list_lookup_alter_ne f l i j : i ≠j → alter f i l !! j = l !! j.
@@ -494,7 +492,7 @@ Proof.
revert i j. induction l; [done|]. intros [][] ?; csimpl; auto with congruence.
Qed.
Lemma list_lookup_insert l i x : i < length l → <[i:=x]>l !! i = Some x.
-Proof. revert i. induction l; intros [|?] ?; f_equal'; auto with lia. Qed.
+Proof. revert i. induction l; intros [|?] ?; f_equal/=; auto with lia. Qed.
Lemma list_lookup_insert_ne l i j x : i ≠j → <[i:=x]>l !! j = l !! j.
Proof.
revert i j. induction l; [done|]. intros [] [] ?; simpl; auto with congruence.
@@ -512,20 +510,20 @@ Proof.
Qed.
Lemma list_insert_commute l i j x y :
i ≠j → <[i:=x]>(<[j:=y]>l) = <[j:=y]>(<[i:=x]>l).
-Proof. revert i j. by induction l; intros [|?] [|?] ?; f_equal'; auto. Qed.
+Proof. revert i j. by induction l; intros [|?] [|?] ?; f_equal/=; auto. Qed.
Lemma list_lookup_other l i x :
length l ≠1 → l !! i = Some x → ∃ j y, j ≠i ∧ l !! j = Some y.
Proof.
- intros. destruct i, l as [|x0 [|x1 l]]; simplify_equality'.
+ intros. destruct i, l as [|x0 [|x1 l]]; simplify_eq/=.
- 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.
-Proof. revert i. induction l1; intros [|?] ?; f_equal'; auto with lia. Qed.
+Proof. revert i. induction l1; intros [|?] ?; f_equal/=; auto with lia. Qed.
Lemma alter_app_r f l1 l2 i :
alter f (length l1 + i) (l1 ++ l2) = l1 ++ alter f i l2.
-Proof. revert i. induction l1; intros [|?]; f_equal'; auto. Qed.
+Proof. revert i. induction l1; intros [|?]; f_equal/=; auto. Qed.
Lemma alter_app_r_alt f l1 l2 i :
length l1 ≤ i → alter f i (l1 ++ l2) = l1 ++ alter f (i - length l1) l2.
Proof.
@@ -533,21 +531,21 @@ Proof.
rewrite Hi at 1. by apply alter_app_r.
Qed.
Lemma list_alter_id f l i : (∀ x, f x = x) → alter f i l = l.
-Proof. intros ?. revert i. induction l; intros [|?]; f_equal'; auto. Qed.
+Proof. intros ?. revert i. induction l; intros [|?]; f_equal/=; auto. Qed.
Lemma list_alter_ext f g l k i :
(∀ x, l !! i = Some x → f x = g x) → l = k → alter f i l = alter g i k.
-Proof. intros H ->. revert i H. induction k; intros [|?] ?; f_equal'; auto. Qed.
+Proof. intros H ->. revert i H. induction k; intros [|?] ?; f_equal/=; auto. Qed.
Lemma list_alter_compose f g l i :
alter (f ∘ g) i l = alter f i (alter g i l).
-Proof. revert i. induction l; intros [|?]; f_equal'; auto. Qed.
+Proof. revert i. induction l; intros [|?]; f_equal/=; auto. Qed.
Lemma list_alter_commute f g l i j :
i ≠j → alter f i (alter g j l) = alter g j (alter f i l).
-Proof. revert i j. induction l; intros [|?][|?] ?; f_equal'; auto with lia. Qed.
+Proof. revert i j. induction l; intros [|?][|?] ?; f_equal/=; auto with lia. Qed.
Lemma insert_app_l l1 l2 i x :
i < length l1 → <[i:=x]>(l1 ++ l2) = <[i:=x]>l1 ++ l2.
-Proof. revert i. induction l1; intros [|?] ?; f_equal'; auto with lia. Qed.
+Proof. revert i. induction l1; intros [|?] ?; f_equal/=; auto with lia. Qed.
Lemma insert_app_r l1 l2 i x : <[length l1+i:=x]>(l1 ++ l2) = l1 ++ <[i:=x]>l2.
-Proof. revert i. induction l1; intros [|?]; f_equal'; auto. Qed.
+Proof. revert i. induction l1; intros [|?]; f_equal/=; auto. Qed.
Lemma insert_app_r_alt l1 l2 i x :
length l1 ≤ i → <[i:=x]>(l1 ++ l2) = l1 ++ <[i - length l1:=x]>l2.
Proof.
@@ -555,7 +553,7 @@ Proof.
rewrite Hi at 1. by apply insert_app_r.
Qed.
Lemma delete_middle l1 l2 x : delete (length l1) (l1 ++ x :: l2) = l1 ++ l2.
-Proof. induction l1; f_equal'; auto. Qed.
+Proof. induction l1; f_equal/=; auto. Qed.
Lemma inserts_length l i k : length (list_inserts i k l) = length l.
Proof.
@@ -643,7 +641,7 @@ Proof.
Qed.
Lemma elem_of_list_lookup_2 l i x : l !! i = Some x → x ∈ l.
Proof.
- revert i. induction l; intros [|i] ?; simplify_equality'; constructor; eauto.
+ revert i. induction l; intros [|i] ?; simplify_eq/=; constructor; eauto.
Qed.
Lemma elem_of_list_lookup l x : x ∈ l ↔ ∃ i, l !! i = Some x.
Proof. firstorder eauto using elem_of_list_lookup_1, elem_of_list_lookup_2. Qed.
@@ -654,7 +652,7 @@ Proof.
- 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;
- simplify_equality; try constructor; auto.
+ simplify_eq; try constructor; auto.
Qed.
(** ** Properties of the [NoDup] predicate *)
@@ -687,8 +685,8 @@ Lemma NoDup_lookup l i j x :
NoDup l → l !! i = Some x → l !! j = Some x → i = j.
Proof.
intros Hl. revert i j. induction Hl as [|x' l Hx Hl IH].
- { intros; simplify_equality. }
- intros [|i] [|j] ??; simplify_equality'; eauto with f_equal;
+ { intros; simplify_eq. }
+ intros [|i] [|j] ??; simplify_eq/=; eauto with f_equal;
exfalso; eauto using elem_of_list_lookup_2.
Qed.
Lemma NoDup_alt l :
@@ -720,7 +718,7 @@ Section no_dup_dec.
Lemma elem_of_remove_dups l x : x ∈ remove_dups l ↔ x ∈ l.
Proof.
split; induction l; simpl; repeat case_decide;
- rewrite ?elem_of_cons; intuition (simplify_equality; auto).
+ rewrite ?elem_of_cons; intuition (simplify_eq; auto).
Qed.
Lemma NoDup_remove_dups l : NoDup (remove_dups l).
Proof.
@@ -815,11 +813,11 @@ Section find.
Proof.
revert i; induction l; intros [] ?;
repeat (match goal with x : prod _ _ |- _ => destruct x end
- || simplify_option_equality); eauto.
+ || simplify_option_eq); eauto.
Qed.
Lemma list_find_elem_of l x : x ∈ l → P x → is_Some (list_find P l).
Proof.
- induction 1 as [|x y l ? IH]; intros; simplify_option_equality; eauto.
+ induction 1 as [|x y l ? IH]; intros; simplify_option_eq; eauto.
by destruct IH as [[i x'] ->]; [|exists (S i, x')].
Qed.
End find.
@@ -876,32 +874,32 @@ Definition take_drop i l : take i l ++ drop i l = l := firstn_skipn i l.
Lemma take_drop_middle l i x :
l !! i = Some x → take i l ++ x :: drop (S i) l = l.
Proof.
- revert i x. induction l; intros [|?] ??; simplify_equality'; f_equal; auto.
+ revert i x. induction l; intros [|?] ??; simplify_eq/=; f_equal; auto.
Qed.
Lemma take_nil n : take n (@nil A) = [].
Proof. by destruct n. Qed.
Lemma take_app l k : take (length l) (l ++ k) = l.
-Proof. induction l; f_equal'; auto. Qed.
+Proof. induction l; f_equal/=; auto. Qed.
Lemma take_app_alt l k n : n = length l → take n (l ++ k) = l.
Proof. intros ->. by apply take_app. Qed.
Lemma take_app3_alt l1 l2 l3 n : n = length l1 → take n ((l1 ++ l2) ++ l3) = l1.
Proof. intros ->. by rewrite <-(assoc_L (++)), take_app. Qed.
Lemma take_app_le l k n : n ≤ length l → take n (l ++ k) = take n l.
-Proof. revert n. induction l; intros [|?] ?; f_equal'; auto with lia. Qed.
+Proof. revert n. induction l; intros [|?] ?; f_equal/=; auto with lia. Qed.
Lemma take_plus_app l k n m :
length l = n → take (n + m) (l ++ k) = l ++ take m k.
-Proof. intros <-. induction l; f_equal'; auto. Qed.
+Proof. intros <-. induction l; f_equal/=; auto. Qed.
Lemma take_app_ge l k n :
length l ≤ n → take n (l ++ k) = l ++ take (n - length l) k.
-Proof. revert n. induction l; intros [|?] ?; f_equal'; auto with lia. Qed.
+Proof. revert n. induction l; intros [|?] ?; f_equal/=; auto with lia. Qed.
Lemma take_ge l n : length l ≤ n → take n l = l.
-Proof. revert n. induction l; intros [|?] ?; f_equal'; auto with lia. Qed.
+Proof. revert n. induction l; intros [|?] ?; f_equal/=; auto with lia. Qed.
Lemma take_take l n m : take n (take m l) = take (min n m) l.
-Proof. revert n m. induction l; intros [|?] [|?]; f_equal'; auto. Qed.
+Proof. revert n m. induction l; intros [|?] [|?]; f_equal/=; auto. Qed.
Lemma take_idemp l n : take n (take n l) = take n l.
Proof. by rewrite take_take, Min.min_idempotent. Qed.
Lemma take_length l n : length (take n l) = min n (length l).
-Proof. revert n. induction l; intros [|?]; f_equal'; done. Qed.
+Proof. revert n. induction l; intros [|?]; f_equal/=; done. Qed.
Lemma take_length_le l n : n ≤ length l → length (take n l) = n.
Proof. rewrite take_length. apply Min.min_l. Qed.
Lemma take_length_ge l n : length l ≤ n → length (take n l) = length l.
@@ -933,7 +931,7 @@ Proof. done. Qed.
Lemma drop_nil n : drop n (@nil A) = [].
Proof. by destruct n. Qed.
Lemma drop_length l n : length (drop n l) = length l - n.
-Proof. revert n. by induction l; intros [|i]; f_equal'. Qed.
+Proof. revert n. by induction l; intros [|i]; f_equal/=. Qed.
Lemma drop_ge l n : length l ≤ n → drop n l = [].
Proof. revert n. induction l; intros [|??]; simpl in *; auto with lia. Qed.
Lemma drop_all l : drop (length l) l = [].
@@ -972,13 +970,13 @@ Proof.
by rewrite !lookup_drop, !list_lookup_insert_ne by lia.
Qed.
Lemma delete_take_drop l i : delete i l = take i l ++ drop (S i) l.
-Proof. revert i. induction l; intros [|?]; f_equal'; auto. Qed.
+Proof. revert i. induction l; intros [|?]; f_equal/=; auto. Qed.
Lemma take_take_drop l n m : take n l ++ take m (drop n l) = take (n + m) l.
-Proof. revert n m. induction l; intros [|?] [|?]; f_equal'; auto. Qed.
+Proof. revert n m. induction l; intros [|?] [|?]; f_equal/=; auto. Qed.
Lemma drop_take_drop l n m : n ≤ m → drop n (take m l) ++ drop m l = drop n l.
Proof.
revert n m. induction l; intros [|?] [|?] ?;
- f_equal'; auto using take_drop with lia.
+ f_equal/=; auto using take_drop with lia.
Qed.
(** ** Properties of the [replicate] function *)
@@ -1004,27 +1002,27 @@ Proof.
- 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.
+Proof. revert i. induction n; intros [|?]; f_equal/=; auto. Qed.
Lemma elem_of_replicate_inv x n y : x ∈ replicate n y → x = y.
Proof. induction n; simpl; rewrite ?elem_of_nil, ?elem_of_cons; intuition. Qed.
Lemma replicate_S n x : replicate (S n) x = x :: replicate n x.
Proof. done. Qed.
Lemma replicate_plus n m x :
replicate (n + m) x = replicate n x ++ replicate m x.
-Proof. induction n; f_equal'; auto. Qed.
+Proof. induction n; f_equal/=; auto. Qed.
Lemma take_replicate n m x : take n (replicate m x) = replicate (min n m) x.
-Proof. revert m. by induction n; intros [|?]; f_equal'. Qed.
+Proof. revert m. by induction n; intros [|?]; f_equal/=. Qed.
Lemma take_replicate_plus n m x : take n (replicate (n + m) x) = replicate n x.
Proof. by rewrite take_replicate, min_l by lia. Qed.
Lemma drop_replicate n m x : drop n (replicate m x) = replicate (m - n) x.
-Proof. revert m. by induction n; intros [|?]; f_equal'. Qed.
+Proof. revert m. by induction n; intros [|?]; f_equal/=. Qed.
Lemma drop_replicate_plus n m x : drop n (replicate (n + m) x) = replicate m x.
Proof. rewrite drop_replicate. f_equal. lia. Qed.
Lemma replicate_as_elem_of x n l :
replicate n x = l ↔ length l = n ∧ ∀ y, y ∈ l → y = x.
Proof.
split; [intros <-; eauto using elem_of_replicate_inv, replicate_length|].
- intros [<- Hl]. symmetry. induction l as [|y l IH]; f_equal'.
+ intros [<- Hl]. symmetry. induction l as [|y l IH]; f_equal/=.
- apply Hl. by left.
- apply IH. intros ??. apply Hl. by right.
Qed.
@@ -1039,11 +1037,11 @@ Proof. intros <-. by induction βs; simpl; constructor. Qed.
(** ** Properties of the [resize] function *)
Lemma resize_spec l n x : resize n x l = take n l ++ replicate (n - length l) x.
-Proof. revert n. induction l; intros [|?]; f_equal'; auto. Qed.
+Proof. revert n. induction l; intros [|?]; f_equal/=; auto. Qed.
Lemma resize_0 l x : resize 0 x l = [].
Proof. by destruct l. Qed.
Lemma resize_nil n x : resize n x [] = replicate n x.
-Proof. rewrite resize_spec. rewrite take_nil. f_equal'. lia. Qed.
+Proof. rewrite resize_spec. rewrite take_nil. f_equal/=. lia. Qed.
Lemma resize_ge l n x :
length l ≤ n → resize n x l = l ++ replicate (n - length l) x.
Proof. intros. by rewrite resize_spec, take_ge. Qed.
@@ -1059,7 +1057,7 @@ Proof. intros ->. by rewrite resize_all. Qed.
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.
+ revert n m. induction l; intros [|?] [|?]; f_equal/=; auto.
- by rewrite Nat.add_0_r, (right_id_L [] (++)).
- by rewrite replicate_plus.
Qed.
@@ -1082,22 +1080,22 @@ Qed.
Lemma resize_length l n x : length (resize n x l) = n.
Proof. rewrite resize_spec, app_length, replicate_length, take_length. lia. Qed.
Lemma resize_replicate x n m : resize n x (replicate m x) = replicate n x.
-Proof. revert m. induction n; intros [|?]; f_equal'; auto. Qed.
+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 [|?] [|?] ?; 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.
Lemma resize_take_le l n m x : n ≤ m → resize n x (take m l) = resize n x l.
-Proof. revert n m. induction l; intros [|?][|?] ?; f_equal'; auto with lia. Qed.
+Proof. revert n m. induction l; intros [|?][|?] ?; f_equal/=; auto with lia. Qed.
Lemma resize_take_eq l n x : resize n x (take n l) = resize n x l.
Proof. by rewrite resize_take_le. Qed.
Lemma take_resize l n m x : take n (resize m x l) = resize (min n m) x l.
Proof.
- revert n m. induction l; intros [|?][|?]; f_equal'; auto using take_replicate.
+ revert n m. induction l; intros [|?][|?]; f_equal/=; auto using take_replicate.
Qed.
Lemma take_resize_le l n m x : n ≤ m → take n (resize m x l) = resize n x l.
Proof. intros. by rewrite take_resize, Min.min_l. Qed.
@@ -1139,7 +1137,7 @@ Implicit Types l k : list A.
(** ** Properties of the [reshape] function *)
Lemma reshape_length szs l : length (reshape szs l) = length szs.
-Proof. revert l. by induction szs; intros; f_equal'. Qed.
+Proof. revert l. by induction szs; intros; f_equal/=. Qed.
Lemma join_reshape szs l :
sum_list szs = length l → mjoin (reshape szs l) = l.
Proof.
@@ -1153,7 +1151,7 @@ Proof. induction m; simpl; auto. Qed.
Lemma sublist_lookup_length l i n k :
sublist_lookup i n l = Some k → length k = n.
Proof.
- unfold sublist_lookup; intros; simplify_option_equality.
+ unfold sublist_lookup; intros; simplify_option_eq.
rewrite take_length, drop_length; lia.
Qed.
Lemma sublist_lookup_all l n : length l = n → sublist_lookup 0 n l = Some l.
@@ -1163,10 +1161,10 @@ Proof.
Qed.
Lemma sublist_lookup_Some l i n :
i + n ≤ length l → sublist_lookup i n l = Some (take n (drop i l)).
-Proof. by unfold sublist_lookup; intros; simplify_option_equality. Qed.
+Proof. by unfold sublist_lookup; intros; simplify_option_eq. Qed.
Lemma sublist_lookup_None l i n :
length l < i + n → sublist_lookup i n l = None.
-Proof. by unfold sublist_lookup; intros; simplify_option_equality by lia. Qed.
+Proof. by unfold sublist_lookup; intros; simplify_option_eq by lia. Qed.
Lemma sublist_eq l k n :
(n | length l) → (n | length k) →
(∀ i, sublist_lookup (i * n) n l = sublist_lookup (i * n) n k) → l = k.
@@ -1181,7 +1179,7 @@ Proof.
(nil_length_inv k) by eauto using Nat.divide_0_l. }
apply list_eq; intros i. specialize (Hlookup (i `div` n)).
rewrite (Nat.mul_comm _ n) in Hlookup.
- unfold sublist_lookup in *; simplify_option_equality;
+ unfold sublist_lookup in *; simplify_option_eq;
[|by rewrite !lookup_ge_None_2 by auto].
apply (f_equal (!! i `mod` n)) in Hlookup.
by rewrite !lookup_take, !lookup_drop, <-!Nat.div_mod in Hlookup
@@ -1207,12 +1205,12 @@ Proof.
intros Hn Hl. unfold sublist_lookup. apply option_eq; intros x; split.
- 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.
+ induction m as [|m IH]; intros [|i] l ??; simplify_eq/=; 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_eq/=.
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.
@@ -1221,7 +1219,7 @@ Lemma sublist_lookup_compose l1 l2 l3 i n j m :
sublist_lookup i n l1 = Some l2 → sublist_lookup j m l2 = Some l3 →
sublist_lookup (i + j) m l1 = Some l3.
Proof.
- unfold sublist_lookup; intros; simplify_option_equality;
+ unfold sublist_lookup; intros; simplify_option_eq;
repeat match goal with
| H : _ ≤ length _ |- _ => rewrite take_length, drop_length in H
end; rewrite ?take_drop_commute, ?drop_drop, ?take_take,
@@ -1231,7 +1229,7 @@ Lemma sublist_alter_length f l i n k :
sublist_lookup i n l = Some k → length (f k) = n →
length (sublist_alter f i n l) = length l.
Proof.
- unfold sublist_alter, sublist_lookup. intros Hk ?; simplify_option_equality.
+ unfold sublist_alter, sublist_lookup. intros Hk ?; simplify_option_eq.
rewrite !app_length, Hk, !take_length, !drop_length; lia.
Qed.
Lemma sublist_lookup_alter f l i n k :
@@ -1239,7 +1237,7 @@ Lemma sublist_lookup_alter f l i n k :
sublist_lookup i n (sublist_alter f i n l) = f <$> sublist_lookup i n l.
Proof.
unfold sublist_lookup. intros Hk ?. erewrite sublist_alter_length by eauto.
- unfold sublist_alter; simplify_option_equality.
+ unfold sublist_alter; simplify_option_eq.
by rewrite Hk, drop_app_alt, take_app_alt by (rewrite ?take_length; lia).
Qed.
Lemma sublist_lookup_alter_ne f l i j n k :
@@ -1247,7 +1245,7 @@ Lemma sublist_lookup_alter_ne f l i j n k :
sublist_lookup i n (sublist_alter f j n l) = sublist_lookup i n l.
Proof.
unfold sublist_lookup. intros Hk Hi ?. erewrite sublist_alter_length by eauto.
- unfold sublist_alter; simplify_option_equality; f_equal; rewrite Hk.
+ unfold sublist_alter; simplify_option_eq; f_equal; rewrite Hk.
apply list_eq; intros ii.
destruct (decide (ii < length (f k))); [|by rewrite !lookup_take_ge by lia].
rewrite !lookup_take, !lookup_drop by done. destruct (decide (i + ii < j)).
@@ -1264,7 +1262,7 @@ Lemma sublist_alter_compose f g l i n k :
sublist_lookup i n l = Some k → length (f k) = n → length (g k) = n →
sublist_alter (f ∘ g) i n l = sublist_alter f i n (sublist_alter g i n l).
Proof.
- unfold sublist_alter, sublist_lookup. intros Hk ??; simplify_option_equality.
+ unfold sublist_alter, sublist_lookup. intros Hk ??; simplify_option_eq.
by rewrite !take_app_alt, drop_app_alt, !(assoc_L (++)), drop_app_alt,
take_app_alt by (rewrite ?app_length, ?take_length, ?Hk; lia).
Qed.
@@ -1273,52 +1271,52 @@ Qed.
Lemma mask_nil f βs : mask f βs (@nil A) = [].
Proof. by destruct βs. Qed.
Lemma mask_length f βs l : length (mask f βs l) = length l.
-Proof. revert βs. induction l; intros [|??]; f_equal'; auto. Qed.
+Proof. revert βs. induction l; intros [|??]; f_equal/=; auto. Qed.
Lemma mask_true f l n : length l ≤ n → mask f (replicate n true) l = f <$> l.
-Proof. revert n. induction l; intros [|?] ?; f_equal'; auto with lia. Qed.
+Proof. revert n. induction l; intros [|?] ?; f_equal/=; auto with lia. Qed.
Lemma mask_false f l n : mask f (replicate n false) l = l.
-Proof. revert l. induction n; intros [|??]; f_equal'; auto. Qed.
+Proof. revert l. induction n; intros [|??]; f_equal/=; auto. Qed.
Lemma mask_app f βs1 βs2 l :
mask f (βs1 ++ βs2) l
= mask f βs1 (take (length βs1) l) ++ mask f βs2 (drop (length βs1) l).
-Proof. revert l. induction βs1;intros [|??]; f_equal'; auto using mask_nil. Qed.
+Proof. revert l. induction βs1;intros [|??]; f_equal/=; auto using mask_nil. Qed.
Lemma mask_app_2 f βs l1 l2 :
mask f βs (l1 ++ l2)
= mask f (take (length l1) βs) l1 ++ mask f (drop (length l1) βs) l2.
-Proof. revert βs. induction l1; intros [|??]; f_equal'; auto. Qed.
+Proof. revert βs. induction l1; intros [|??]; f_equal/=; auto. Qed.
Lemma take_mask f βs l n : take n (mask f βs l) = mask f (take n βs) (take n l).
-Proof. revert n βs. induction l; intros [|?] [|[] ?]; f_equal'; auto. Qed.
+Proof. revert n βs. induction l; intros [|?] [|[] ?]; f_equal/=; auto. Qed.
Lemma drop_mask f βs l n : drop n (mask f βs l) = mask f (drop n βs) (drop n l).
Proof.
- revert n βs. induction l; intros [|?] [|[] ?]; f_equal'; auto using mask_nil.
+ revert n βs. induction l; intros [|?] [|[] ?]; f_equal/=; auto using mask_nil.
Qed.
Lemma sublist_lookup_mask f βs l i n :
sublist_lookup i n (mask f βs l)
= mask f (take n (drop i βs)) <$> sublist_lookup i n l.
Proof.
- unfold sublist_lookup; rewrite mask_length; simplify_option_equality; auto.
+ unfold sublist_lookup; rewrite mask_length; simplify_option_eq; auto.
by rewrite drop_mask, take_mask.
Qed.
Lemma mask_mask f g βs1 βs2 l :
(∀ x, f (g x) = f x) → βs1 =.>* βs2 →
mask f βs2 (mask g βs1 l) = mask f βs2 l.
Proof.
- intros ? Hβs. revert l. by induction Hβs as [|[] []]; intros [|??]; f_equal'.
+ intros ? Hβs. revert l. by induction Hβs as [|[] []]; intros [|??]; f_equal/=.
Qed.
Lemma lookup_mask f βs l i :
βs !! i = Some true → mask f βs l !! i = f <$> l !! i.
Proof.
- revert i βs. induction l; intros [] [] ?; simplify_equality'; f_equal; auto.
+ revert i βs. induction l; intros [] [] ?; simplify_eq/=; f_equal; auto.
Qed.
Lemma lookup_mask_notin f βs l i :
βs !! i ≠Some true → mask f βs l !! i = l !! i.
Proof.
- revert i βs. induction l; intros [] [|[]] ?; simplify_equality'; auto.
+ revert i βs. induction l; intros [] [|[]] ?; simplify_eq/=; auto.
Qed.
(** ** Properties of the [seq] function *)
Lemma fmap_seq j n : S <$> seq j n = seq (S j) n.
-Proof. revert j. induction n; intros; f_equal'; auto. Qed.
+Proof. revert j. induction n; intros; f_equal/=; auto. Qed.
Lemma lookup_seq j n i : i < n → seq j n !! i = Some (j + i).
Proof.
revert j i. induction n as [|n IH]; intros j [|i] ?; simpl; auto with lia.
@@ -1374,7 +1372,7 @@ Proof.
Qed.
Lemma delete_Permutation l i x : l !! i = Some x → l ≡ₚ x :: delete i l.
Proof.
- revert i; induction l as [|y l IH]; intros [|i] ?; simplify_equality'; auto.
+ revert i; induction l as [|y l IH]; intros [|i] ?; simplify_eq/=; auto.
by rewrite Permutation_swap, <-(IH i).
Qed.
@@ -1395,10 +1393,10 @@ Lemma prefix_of_cons_alt x y l1 l2 :
x = y → l1 `prefix_of` l2 → x :: l1 `prefix_of` y :: l2.
Proof. intros ->. apply prefix_of_cons. Qed.
Lemma prefix_of_cons_inv_1 x y l1 l2 : x :: l1 `prefix_of` y :: l2 → x = y.
-Proof. by intros [k ?]; simplify_equality'. Qed.
+Proof. by intros [k ?]; simplify_eq/=. Qed.
Lemma prefix_of_cons_inv_2 x y l1 l2 :
x :: l1 `prefix_of` y :: l2 → l1 `prefix_of` l2.
-Proof. intros [k ?]; simplify_equality'. by exists k. Qed.
+Proof. intros [k ?]; simplify_eq/=. by exists k. Qed.
Lemma prefix_of_app k l1 l2 : l1 `prefix_of` l2 → k ++ l1 `prefix_of` k ++ l2.
Proof. intros [k' ->]. exists k'. by rewrite (assoc_L (++)). Qed.
Lemma prefix_of_app_alt k1 k2 l1 l2 :
@@ -1411,7 +1409,7 @@ Proof. intros [k ->]. exists (k ++ l3). by rewrite (assoc_L (++)). Qed.
Lemma prefix_of_length l1 l2 : l1 `prefix_of` l2 → length l1 ≤ length l2.
Proof. intros [? ->]. rewrite app_length. lia. Qed.
Lemma prefix_of_snoc_not l x : ¬l ++ [x] `prefix_of` l.
-Proof. intros [??]. discriminate_list_equality. Qed.
+Proof. intros [??]. discriminate_list. Qed.
Global Instance: PreOrder (@suffix_of A).
Proof.
split.
@@ -1440,13 +1438,13 @@ Section prefix_ops.
l1 = (max_prefix_of l1 l2).2 ++ (max_prefix_of l1 l2).1.1.
Proof.
revert l2. induction l1; intros [|??]; simpl;
- repeat case_decide; f_equal'; auto.
+ repeat case_decide; f_equal/=; auto.
Qed.
Lemma max_prefix_of_fst_alt l1 l2 k1 k2 k3 :
max_prefix_of l1 l2 = (k1, k2, k3) → l1 = k3 ++ k1.
Proof.
intros. pose proof (max_prefix_of_fst l1 l2).
- by destruct (max_prefix_of l1 l2) as [[]?]; simplify_equality.
+ by destruct (max_prefix_of l1 l2) as [[]?]; simplify_eq.
Qed.
Lemma max_prefix_of_fst_prefix l1 l2 : (max_prefix_of l1 l2).2 `prefix_of` l1.
Proof. eexists. apply max_prefix_of_fst. Qed.
@@ -1457,13 +1455,13 @@ Section prefix_ops.
l2 = (max_prefix_of l1 l2).2 ++ (max_prefix_of l1 l2).1.2.
Proof.
revert l2. induction l1; intros [|??]; simpl;
- repeat case_decide; f_equal'; auto.
+ repeat case_decide; f_equal/=; auto.
Qed.
Lemma max_prefix_of_snd_alt l1 l2 k1 k2 k3 :
max_prefix_of l1 l2 = (k1, k2, k3) → l2 = k3 ++ k2.
Proof.
intro. pose proof (max_prefix_of_snd l1 l2).
- by destruct (max_prefix_of l1 l2) as [[]?]; simplify_equality.
+ by destruct (max_prefix_of l1 l2) as [[]?]; simplify_eq.
Qed.
Lemma max_prefix_of_snd_prefix l1 l2 : (max_prefix_of l1 l2).2 `prefix_of` l2.
Proof. eexists. apply max_prefix_of_snd. Qed.
@@ -1481,7 +1479,7 @@ Section prefix_ops.
k `prefix_of` l1 → k `prefix_of` l2 → k `prefix_of` k3.
Proof.
intro. pose proof (max_prefix_of_max l1 l2 k).
- by destruct (max_prefix_of l1 l2) as [[]?]; simplify_equality.
+ by destruct (max_prefix_of l1 l2) as [[]?]; simplify_eq.
Qed.
Lemma max_prefix_of_max_snoc l1 l2 k1 k2 k3 x1 x2 :
max_prefix_of l1 l2 = (x1 :: k1, x2 :: k2, k3) → x1 ≠x2.
@@ -1508,7 +1506,7 @@ Proof. by rewrite prefix_suffix_reverse, !reverse_involutive. Qed.
Lemma suffix_of_nil l : [] `suffix_of` l.
Proof. exists l. by rewrite (right_id_L [] (++)). Qed.
Lemma suffix_of_nil_inv l : l `suffix_of` [] → l = [].
-Proof. by intros [[|?] ?]; simplify_list_equality. Qed.
+Proof. by intros [[|?] ?]; simplify_list_eq. Qed.
Lemma suffix_of_cons_nil_inv x l : ¬x :: l `suffix_of` [].
Proof. by intros [[] ?]. Qed.
Lemma suffix_of_snoc l1 l2 x :
@@ -1524,21 +1522,16 @@ Lemma suffix_of_app_alt l1 l2 k1 k2 :
Proof. intros ->. apply suffix_of_app. Qed.
Lemma suffix_of_snoc_inv_1 x y l1 l2 :
l1 ++ [x] `suffix_of` l2 ++ [y] → x = y.
-Proof.
- intros [k' E]. rewrite (assoc_L (++)) in E.
- by simplify_list_equality.
-Qed.
+Proof. intros [k' E]. rewrite (assoc_L (++)) in E. by simplify_list_eq. Qed.
Lemma suffix_of_snoc_inv_2 x y l1 l2 :
l1 ++ [x] `suffix_of` l2 ++ [y] → l1 `suffix_of` l2.
Proof.
- intros [k' E]. exists k'. rewrite (assoc_L (++)) in E.
- by simplify_list_equality.
+ intros [k' E]. exists k'. rewrite (assoc_L (++)) in E. by simplify_list_eq.
Qed.
Lemma suffix_of_app_inv l1 l2 k :
l1 ++ k `suffix_of` l2 ++ k → l1 `suffix_of` l2.
Proof.
- intros [k' E]. exists k'. rewrite (assoc_L (++)) in E.
- by simplify_list_equality.
+ intros [k' E]. exists k'. rewrite (assoc_L (++)) in E. by simplify_list_eq.
Qed.
Lemma suffix_of_cons_l l1 l2 x : x :: l1 `suffix_of` l2 → l1 `suffix_of` l2.
Proof. intros [k ->]. exists (k ++ [x]). by rewrite <-(assoc_L (++)). Qed.
@@ -1551,13 +1544,12 @@ Proof. intros [k ->]. exists (l3 ++ k). by rewrite (assoc_L (++)). Qed.
Lemma suffix_of_cons_inv l1 l2 x y :
x :: l1 `suffix_of` y :: l2 → x :: l1 = y :: l2 ∨ x :: l1 `suffix_of` l2.
Proof.
- intros [[|? k] E]; [by left|].
- right. simplify_equality'. by apply suffix_of_app_r.
+ intros [[|? k] E]; [by left|]. right. simplify_eq/=. by apply suffix_of_app_r.
Qed.
Lemma suffix_of_length l1 l2 : l1 `suffix_of` l2 → length l1 ≤ length l2.
Proof. intros [? ->]. rewrite app_length. lia. Qed.
Lemma suffix_of_cons_not x l : ¬x :: l `suffix_of` l.
-Proof. intros [??]. discriminate_list_equality. Qed.
+Proof. intros [??]. discriminate_list. Qed.
Global Instance suffix_of_dec `{∀ x y, Decision (x = y)} l1 l2 :
Decision (l1 `suffix_of` l2).
Proof.
@@ -1580,7 +1572,7 @@ Section max_suffix_of.
max_suffix_of l1 l2 = (k1, k2, k3) → l1 = k1 ++ k3.
Proof.
intro. pose proof (max_suffix_of_fst l1 l2).
- by destruct (max_suffix_of l1 l2) as [[]?]; simplify_equality.
+ by destruct (max_suffix_of l1 l2) as [[]?]; simplify_eq.
Qed.
Lemma max_suffix_of_fst_suffix l1 l2 : (max_suffix_of l1 l2).2 `suffix_of` l1.
Proof. eexists. apply max_suffix_of_fst. Qed.
@@ -1599,7 +1591,7 @@ Section max_suffix_of.
max_suffix_of l1 l2 = (k1,k2,k3) → l2 = k2 ++ k3.
Proof.
intro. pose proof (max_suffix_of_snd l1 l2).
- by destruct (max_suffix_of l1 l2) as [[]?]; simplify_equality.
+ by destruct (max_suffix_of l1 l2) as [[]?]; simplify_eq.
Qed.
Lemma max_suffix_of_snd_suffix l1 l2 : (max_suffix_of l1 l2).2 `suffix_of` l2.
Proof. eexists. apply max_suffix_of_snd. Qed.
@@ -1619,7 +1611,7 @@ Section max_suffix_of.
k `suffix_of` l1 → k `suffix_of` l2 → k `suffix_of` k3.
Proof.
intro. pose proof (max_suffix_of_max l1 l2 k).
- by destruct (max_suffix_of l1 l2) as [[]?]; simplify_equality.
+ by destruct (max_suffix_of l1 l2) as [[]?]; simplify_eq.
Qed.
Lemma max_suffix_of_max_snoc l1 l2 k1 k2 k3 x1 x2 :
max_suffix_of l1 l2 = (k1 ++ [x1], k2 ++ [x2], k3) → x1 ≠x2.
@@ -1689,7 +1681,7 @@ Qed.
Lemma sublist_app_inv_l k l1 l2 : k ++ l1 `sublist` k ++ l2 → l1 `sublist` l2.
Proof.
induction k as [|y k IH]; simpl; [done |].
- rewrite sublist_cons_r. intros [Hl12|(?&?&?)]; [|simplify_equality; eauto].
+ rewrite sublist_cons_r. intros [Hl12|(?&?&?)]; [|simplify_eq; eauto].
rewrite sublist_cons_l in Hl12. destruct Hl12 as (k1&k2&Hk&?).
apply IH. rewrite Hk. eauto using sublist_inserts_l, sublist_cons.
Qed.
@@ -1701,7 +1693,7 @@ Proof.
{ by rewrite <-!(assoc_L (++)). }
rewrite sublist_app_l in Hl12. destruct Hl12 as (k1&k2&E&?&Hk2).
destruct k2 as [|z k2] using rev_ind; [inversion Hk2|].
- rewrite (assoc_L (++)) in E; simplify_list_equality.
+ rewrite (assoc_L (++)) in E; simplify_list_eq.
eauto using sublist_inserts_r.
Qed.
Global Instance: PartialOrder (@sublist A).
@@ -1715,7 +1707,7 @@ Proof.
+ intros ?. rewrite sublist_cons_l. intros (?&?&?&?); subst.
eauto using sublist_inserts_l, sublist_cons.
- intros l1 l2 Hl12 Hl21. apply sublist_length in Hl21.
- induction Hl12; f_equal'; auto with arith.
+ induction Hl12; f_equal/=; auto with arith.
apply sublist_length in Hl12. lia.
Qed.
Lemma sublist_take l i : take i l `sublist` l.
@@ -1977,10 +1969,10 @@ Section contains_dec.
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.
- 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.
+ - case_decide; simplify_eq; eauto.
+ destruct (list_remove x l1) as [l|] eqn:?; simplify_eq.
+ destruct (IH l) as (?&?&?); simplify_option_eq; eauto.
+ - simplify_option_eq; eauto using Permutation_swap.
- destruct (IH1 k1) as (k2&?&?); trivial.
destruct (IH2 k2) as (k3&?&?); trivial.
exists k3. split; eauto. by transitivity k2.
@@ -1988,7 +1980,7 @@ Section contains_dec.
Lemma list_remove_Some l k x : list_remove x l = Some k → l ≡ₚ x :: k.
Proof.
revert k. induction l as [|y l IH]; simpl; intros k ?; [done |].
- simplify_option_equality; auto. by rewrite Permutation_swap, <-IH.
+ simplify_option_eq; auto. by rewrite Permutation_swap, <-IH.
Qed.
Lemma list_remove_Some_inv l k x :
l ≡ₚ x :: k → ∃ k', list_remove x l = Some k' ∧ k ≡ₚ k'.
@@ -2006,11 +1998,11 @@ Section contains_dec.
{ 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.
+ simplify_option_eq. apply IH. by rewrite <-Hk2.
- 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.
+ destruct (list_remove x l2) as [k'|] eqn:?; intros; simplify_eq.
rewrite contains_cons_l. eauto using list_remove_Some.
Qed.
Global Instance contains_dec l1 l2 : Decision (l1 `contains` l2).
@@ -2137,21 +2129,21 @@ Section Forall_Exists.
Lemma Forall_sublist_lookup l i n k :
sublist_lookup i n l = Some k → Forall P l → Forall P k.
Proof.
- unfold sublist_lookup. intros; simplify_option_equality.
+ unfold sublist_lookup. intros; simplify_option_eq.
auto using Forall_take, Forall_drop.
Qed.
Lemma Forall_sublist_alter f l i n k :
Forall P l → sublist_lookup i n l = Some k → Forall P (f k) →
Forall P (sublist_alter f i n l).
Proof.
- unfold sublist_alter, sublist_lookup. intros; simplify_option_equality.
+ unfold sublist_alter, sublist_lookup. intros; simplify_option_eq.
auto using Forall_app_2, Forall_drop, Forall_take.
Qed.
Lemma Forall_sublist_alter_inv f l i n k :
sublist_lookup i n l = Some k →
Forall P (sublist_alter f i n l) → Forall P (f k).
Proof.
- unfold sublist_alter, sublist_lookup. intros ?; simplify_option_equality.
+ unfold sublist_alter, sublist_lookup. intros ?; simplify_option_eq.
rewrite !Forall_app; tauto.
Qed.
Lemma Forall_reshape l szs : Forall P l → Forall (Forall P) (reshape szs l).
@@ -2255,16 +2247,16 @@ Section Forall2.
Lemma Forall2_true l k :
(∀ x y, P x y) → length l = length k → Forall2 P l k.
Proof.
- intro. revert k. induction l; intros [|??] ?; simplify_equality'; auto.
+ intro. revert k. induction l; intros [|??] ?; simplify_eq/=; auto.
Qed.
Lemma Forall2_same_length l k :
Forall2 (λ _ _, True) l k ↔ length l = length k.
Proof.
- split; [by induction 1; f_equal'|].
- revert k. induction l; intros [|??] ?; simplify_equality'; auto.
+ split; [by induction 1; f_equal/=|].
+ revert k. induction l; intros [|??] ?; simplify_eq/=; auto.
Qed.
Lemma Forall2_length l k : Forall2 P l k → length l = length k.
- Proof. by induction 1; f_equal'. Qed.
+ Proof. by induction 1; f_equal/=. Qed.
Lemma Forall2_length_l l k n : Forall2 P l k → length l = n → length k = n.
Proof. intros ? <-; symmetry. by apply Forall2_length. Qed.
Lemma Forall2_length_r l k n : Forall2 P l k → length k = n → length l = n.
@@ -2334,17 +2326,17 @@ Section Forall2.
Lemma Forall2_lookup_lr l k i x y :
Forall2 P l k → l !! i = Some x → k !! i = Some y → P x y.
Proof.
- intros H. revert i. induction H; intros [|?] ??; simplify_equality'; eauto.
+ intros H. revert i. induction H; intros [|?] ??; simplify_eq/=; eauto.
Qed.
Lemma Forall2_lookup_l l k i x :
Forall2 P l k → l !! i = Some x → ∃ y, k !! i = Some y ∧ P x y.
Proof.
- intros H. revert i. induction H; intros [|?] ?; simplify_equality'; eauto.
+ intros H. revert i. induction H; intros [|?] ?; simplify_eq/=; eauto.
Qed.
Lemma Forall2_lookup_r l k i y :
Forall2 P l k → k !! i = Some y → ∃ x, l !! i = Some x ∧ P x y.
Proof.
- intros H. revert i. induction H; intros [|?] ?; simplify_equality'; eauto.
+ intros H. revert i. induction H; intros [|?] ?; simplify_eq/=; eauto.
Qed.
Lemma Forall2_lookup_2 l k :
length l = length k →
@@ -2440,7 +2432,7 @@ Section Forall2.
∃ k', sublist_lookup n i k = Some k' ∧ Forall2 P l' k'.
Proof.
unfold sublist_lookup. intros Hlk Hl.
- exists (take i (drop n k)); simplify_option_equality.
+ exists (take i (drop n k)); simplify_option_eq.
- auto using Forall2_take, Forall2_drop.
- apply Forall2_length in Hlk; lia.
Qed.
@@ -2449,7 +2441,7 @@ Section Forall2.
∃ l', sublist_lookup n i l = Some l' ∧ Forall2 P l' k'.
Proof.
intro. unfold sublist_lookup.
- erewrite Forall2_length by eauto; intros; simplify_option_equality.
+ erewrite Forall2_length by eauto; intros; simplify_option_eq.
eauto using Forall2_take, Forall2_drop.
Qed.
Lemma Forall2_sublist_alter f g l k i n l' k' :
@@ -2458,7 +2450,7 @@ Section Forall2.
Forall2 P (sublist_alter f i n l) (sublist_alter g i n k).
Proof.
intro. unfold sublist_alter, sublist_lookup.
- erewrite Forall2_length by eauto; intros; simplify_option_equality.
+ erewrite Forall2_length by eauto; intros; simplify_option_eq.
auto using Forall2_app, Forall2_drop, Forall2_take.
Qed.
Lemma Forall2_sublist_alter_l f l k i n l' k' :
@@ -2467,7 +2459,7 @@ Section Forall2.
Forall2 P (sublist_alter f i n l) k.
Proof.
intro. unfold sublist_lookup, sublist_alter.
- erewrite <-Forall2_length by eauto; intros; simplify_option_equality.
+ erewrite <-Forall2_length by eauto; intros; simplify_option_eq.
apply Forall2_app_l;
rewrite ?take_length_le by lia; auto using Forall2_take.
apply Forall2_app_l; erewrite Forall2_length, take_length,
@@ -2574,32 +2566,32 @@ Section Forall3.
Forall3 P l k k' → (∀ x y z, P x y z → Q x y z) → Forall3 Q l k k'.
Proof. intros Hl ?; induction Hl; auto. Defined.
Lemma Forall3_length_lm l k k' : Forall3 P l k k' → length l = length k.
- Proof. by induction 1; f_equal'. Qed.
+ Proof. by induction 1; f_equal/=. Qed.
Lemma Forall3_length_lr l k k' : Forall3 P l k k' → length l = length k'.
- Proof. by induction 1; f_equal'. Qed.
+ Proof. by induction 1; f_equal/=. Qed.
Lemma Forall3_lookup_lmr l k k' i x y z :
Forall3 P l k k' →
l !! i = Some x → k !! i = Some y → k' !! i = Some z → P x y z.
Proof.
- intros H. revert i. induction H; intros [|?] ???; simplify_equality'; eauto.
+ intros H. revert i. induction H; intros [|?] ???; simplify_eq/=; eauto.
Qed.
Lemma Forall3_lookup_l l k k' i x :
Forall3 P l k k' → l !! i = Some x →
∃ y z, k !! i = Some y ∧ k' !! i = Some z ∧ P x y z.
Proof.
- intros H. revert i. induction H; intros [|?] ?; simplify_equality'; eauto.
+ intros H. revert i. induction H; intros [|?] ?; simplify_eq/=; eauto.
Qed.
Lemma Forall3_lookup_m l k k' i y :
Forall3 P l k k' → k !! i = Some y →
∃ x z, l !! i = Some x ∧ k' !! i = Some z ∧ P x y z.
Proof.
- intros H. revert i. induction H; intros [|?] ?; simplify_equality'; eauto.
+ intros H. revert i. induction H; intros [|?] ?; simplify_eq/=; eauto.
Qed.
Lemma Forall3_lookup_r l k k' i z :
Forall3 P l k k' → k' !! i = Some z →
∃ x y, l !! i = Some x ∧ k !! i = Some y ∧ P x y z.
Proof.
- intros H. revert i. induction H; intros [|?] ?; simplify_equality'; eauto.
+ intros H. revert i. induction H; intros [|?] ?; simplify_eq/=; eauto.
Qed.
Lemma Forall3_alter_lm f g l k k' i :
Forall3 P l k k' →
@@ -2614,35 +2606,35 @@ Section fmap.
Context {A B : Type} (f : A → B).
Lemma list_fmap_id (l : list A) : id <$> l = l.
- Proof. induction l; f_equal'; auto. Qed.
+ Proof. induction l; f_equal/=; auto. Qed.
Lemma list_fmap_compose {C} (g : B → C) l : g ∘ f <$> l = g <$> f <$> l.
- Proof. induction l; f_equal'; auto. Qed.
+ Proof. induction l; f_equal/=; auto. Qed.
Lemma list_fmap_ext (g : A → B) (l1 l2 : list A) :
(∀ x, f x = g x) → l1 = l2 → fmap f l1 = fmap g l2.
- Proof. intros ? <-. induction l1; f_equal'; auto. Qed.
+ Proof. intros ? <-. induction l1; f_equal/=; auto. Qed.
Global Instance: Inj (=) (=) f → Inj (=) (=) (fmap f).
Proof.
intros ? l1. induction l1 as [|x l1 IH]; [by intros [|??]|].
- intros [|??]; intros; f_equal'; simplify_equality; auto.
+ intros [|??]; intros; f_equal/=; simplify_eq; auto.
Qed.
Definition fmap_nil : f <$> [] = [] := eq_refl.
Definition fmap_cons x l : f <$> x :: l = f x :: f <$> l := eq_refl.
Lemma fmap_app l1 l2 : f <$> l1 ++ l2 = (f <$> l1) ++ (f <$> l2).
- Proof. by induction l1; f_equal'. Qed.
+ Proof. by induction l1; f_equal/=. Qed.
Lemma fmap_nil_inv k : f <$> k = [] → k = [].
Proof. by destruct k. Qed.
Lemma fmap_cons_inv y l k :
f <$> l = y :: k → ∃ x l', y = f x ∧ k = f <$> l' ∧ l = x :: l'.
- Proof. intros. destruct l; simplify_equality'; eauto. Qed.
+ Proof. intros. destruct l; simplify_eq/=; eauto. Qed.
Lemma fmap_app_inv l k1 k2 :
f <$> l = k1 ++ k2 → ∃ l1 l2, k1 = f <$> l1 ∧ k2 = f <$> l2 ∧ l = l1 ++ l2.
Proof.
revert l. induction k1 as [|y k1 IH]; simpl; [intros l ?; by eexists [],l|].
- intros [|x l] ?; simplify_equality'.
+ intros [|x l] ?; simplify_eq/=.
destruct (IH l) as (l1&l2&->&->&->); [done|]. by exists (x :: l1), l2.
Qed.
Lemma fmap_length l : length (f <$> l) = length l.
- Proof. by induction l; f_equal'. Qed.
+ Proof. by induction l; f_equal/=. Qed.
Lemma fmap_reverse l : f <$> reverse l = reverse (f <$> l).
Proof.
induction l as [|?? IH]; csimpl; by rewrite ?reverse_cons, ?fmap_app, ?IH.
@@ -2652,29 +2644,29 @@ Section fmap.
Lemma fmap_last l : last (f <$> l) = f <$> last l.
Proof. induction l as [|? []]; simpl; auto. Qed.
Lemma fmap_replicate n x : f <$> replicate n x = replicate n (f x).
- Proof. by induction n; f_equal'. Qed.
+ Proof. by induction n; f_equal/=. Qed.
Lemma fmap_take n l : f <$> take n l = take n (f <$> l).
- Proof. revert n. by induction l; intros [|?]; f_equal'. Qed.
+ Proof. revert n. by induction l; intros [|?]; f_equal/=. Qed.
Lemma fmap_drop n l : f <$> drop n l = drop n (f <$> l).
- Proof. revert n. by induction l; intros [|?]; f_equal'. Qed.
+ Proof. revert n. by induction l; intros [|?]; f_equal/=. Qed.
Lemma fmap_resize n x l : f <$> resize n x l = resize n (f x) (f <$> l).
Proof.
- revert n. induction l; intros [|?]; f_equal'; auto using fmap_replicate.
+ revert n. induction l; intros [|?]; f_equal/=; auto using fmap_replicate.
Qed.
Lemma const_fmap (l : list A) (y : B) :
(∀ x, f x = y) → f <$> l = replicate (length l) y.
- Proof. intros; induction l; f_equal'; auto. Qed.
+ Proof. intros; induction l; f_equal/=; auto. Qed.
Lemma list_lookup_fmap l i : (f <$> l) !! i = f <$> (l !! i).
Proof. revert i. induction l; by intros [|]. Qed.
Lemma list_lookup_fmap_inv l i x :
(f <$> l) !! i = Some x → ∃ y, x = f y ∧ l !! i = Some y.
Proof.
intros Hi. rewrite list_lookup_fmap in Hi.
- destruct (l !! i) eqn:?; simplify_equality'; eauto.
+ destruct (l !! i) eqn:?; simplify_eq/=; eauto.
Qed.
Lemma list_alter_fmap (g : A → A) (h : B → B) l i :
Forall (λ x, f (g x) = h (f x)) l → f <$> alter g i l = alter h i (f <$> l).
- Proof. intros Hl. revert i. by induction Hl; intros [|i]; f_equal'. Qed.
+ Proof. intros Hl. revert i. by induction Hl; intros [|i]; f_equal/=. Qed.
Lemma elem_of_list_fmap_1 l x : x ∈ l → f x ∈ f <$> l.
Proof. induction 1; csimpl; rewrite elem_of_cons; intuition. Qed.
Lemma elem_of_list_fmap_1_alt l x y : x ∈ l → y = f x → y ∈ f <$> l.
@@ -2709,12 +2701,12 @@ Section fmap.
Proof. induction 1; simpl; econstructor; eauto. Qed.
Lemma Forall_fmap_ext_1 (g : A → B) (l : list A) :
Forall (λ x, f x = g x) l → fmap f l = fmap g l.
- Proof. by induction 1; f_equal'. Qed.
+ Proof. by induction 1; f_equal/=. Qed.
Lemma Forall_fmap_ext (g : A → B) (l : list A) :
Forall (λ x, f x = g x) l ↔ fmap f l = fmap g l.
Proof.
split; [auto using Forall_fmap_ext_1|].
- induction l; simpl; constructor; simplify_equality; auto.
+ induction l; simpl; constructor; simplify_eq; auto.
Qed.
Lemma Forall_fmap (P : B → Prop) l : Forall P (f <$> l) ↔ Forall (P ∘ f) l.
Proof. split; induction l; inversion_clear 1; constructor; auto. Qed.
@@ -2740,7 +2732,7 @@ Section fmap.
Forall2 P (f <$> l1) (g <$> l2) ↔ Forall2 (λ x1 x2, P (f x1) (g x2)) l1 l2.
Proof. split; auto using Forall2_fmap_1, Forall2_fmap_2. Qed.
Lemma list_fmap_bind {C} (g : B → list C) l : (f <$> l) ≫= g = l ≫= g ∘ f.
- Proof. by induction l; f_equal'. Qed.
+ Proof. by induction l; f_equal/=. Qed.
End fmap.
Lemma list_alter_fmap_mono {A} (f : A → A) (g : A → A) l i :
@@ -2761,10 +2753,10 @@ Section bind.
Lemma list_bind_ext (g : A → list B) l1 l2 :
(∀ x, f x = g x) → l1 = l2 → l1 ≫= f = l2 ≫= g.
- Proof. intros ? <-. by induction l1; f_equal'. Qed.
+ Proof. intros ? <-. by induction l1; f_equal/=. Qed.
Lemma Forall_bind_ext (g : A → list B) (l : list A) :
Forall (λ x, f x = g x) l → l ≫= f = l ≫= g.
- Proof. by induction 1; f_equal'. Qed.
+ Proof. by induction 1; f_equal/=. Qed.
Global Instance bind_sublist: Proper (sublist ==> sublist) (mbind f).
Proof.
induction 1; simpl; auto;
@@ -2818,7 +2810,7 @@ Section ret_join.
Context {A : Type}.
Lemma list_join_bind (ls : list (list A)) : mjoin ls = ls ≫= id.
- Proof. by induction ls; f_equal'. Qed.
+ Proof. by induction ls; f_equal/=. Qed.
Global Instance mjoin_Permutation:
Proper (@Permutation (list A) ==> (≡ₚ)) mjoin.
Proof. intros ?? E. by rewrite !list_join_bind, E. Qed.
@@ -2859,7 +2851,7 @@ Section mapM.
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) eqn:?; intros; simplify_option_eq; auto.
Qed.
Lemma mapM_Some_2 l k : Forall2 (λ x y, f x = Some y) l k → mapM f l = Some k.
Proof.
@@ -2896,12 +2888,12 @@ Section mapM.
Proof. split; auto using mapM_is_Some_1, mapM_is_Some_2. Qed.
Lemma mapM_fmap_Some (g : B → A) (l : list B) :
(∀ x, f (g x) = Some x) → mapM f (g <$> l) = Some l.
- Proof. intros. by induction l; simpl; simplify_option_equality. Qed.
+ Proof. intros. by induction l; simpl; simplify_option_eq. Qed.
Lemma mapM_fmap_Some_inv (g : B → A) (l : list B) (k : list A) :
(∀ x y, f y = Some x → y = g x) → mapM f k = Some l → k = g <$> l.
Proof.
intros Hgf. revert l; induction k as [|??]; intros [|??] ?;
- simplify_option_equality; f_equiv; eauto.
+ simplify_option_eq; f_equiv; eauto.
Qed.
End mapM.
@@ -2946,7 +2938,7 @@ Section permutations.
change (interleave x2 [x1]) with ([[x2; x1]] ++ [[x1; x2]]).
by rewrite (comm (++)), elem_of_list_singleton. }
rewrite elem_of_cons, elem_of_list_fmap.
- intros Hl1 [? | [l2' [??]]]; simplify_equality'.
+ intros Hl1 [? | [l2' [??]]]; simplify_eq/=.
- 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.
@@ -2969,7 +2961,7 @@ Section permutations.
{ rewrite elem_of_list_singleton. intros Hl1 ->. eexists [].
by rewrite elem_of_list_singleton. }
rewrite elem_of_cons, elem_of_list_fmap.
- intros Hl1 [? | [l2' [? Hl2']]]; simplify_equality'.
+ intros Hl1 [? | [l2' [? Hl2']]]; simplify_eq/=.
- 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.
@@ -3021,43 +3013,43 @@ Section zip_with.
Lemma zip_with_app l1 l2 k1 k2 :
length l1 = length k1 →
zip_with f (l1 ++ l2) (k1 ++ k2) = zip_with f l1 k1 ++ zip_with f l2 k2.
- Proof. rewrite <-Forall2_same_length. induction 1; f_equal'; auto. Qed.
+ Proof. rewrite <-Forall2_same_length. induction 1; f_equal/=; auto. Qed.
Lemma zip_with_app_l l1 l2 k :
zip_with f (l1 ++ l2) k
= zip_with f l1 (take (length l1) k) ++ zip_with f l2 (drop (length l1) k).
Proof.
- revert k. induction l1; intros [|??]; f_equal'; auto. by destruct l2.
+ revert k. induction l1; intros [|??]; f_equal/=; auto. by destruct l2.
Qed.
Lemma zip_with_app_r l k1 k2 :
zip_with f l (k1 ++ k2)
= zip_with f (take (length k1) l) k1 ++ zip_with f (drop (length k1) l) k2.
- Proof. revert l. induction k1; intros [|??]; f_equal'; auto. Qed.
+ Proof. revert l. induction k1; intros [|??]; f_equal/=; auto. Qed.
Lemma zip_with_flip l k : zip_with (flip f) k l = zip_with f l k.
- Proof. revert k. induction l; intros [|??]; f_equal'; auto. Qed.
+ Proof. revert k. induction l; intros [|??]; f_equal/=; auto. Qed.
Lemma zip_with_ext (g : A → B → C) l1 l2 k1 k2 :
(∀ x y, f x y = g x y) → l1 = l2 → k1 = k2 →
zip_with f l1 k1 = zip_with g l2 k2.
- Proof. intros ? <-<-. revert k1. by induction l1; intros [|??]; f_equal'. Qed.
+ Proof. intros ? <-<-. revert k1. by induction l1; intros [|??]; f_equal/=. Qed.
Lemma Forall_zip_with_ext_l (g : A → B → C) l k1 k2 :
Forall (λ x, ∀ y, f x y = g x y) l → k1 = k2 →
zip_with f l k1 = zip_with g l k2.
- Proof. intros Hl <-. revert k1. by induction Hl; intros [|??]; f_equal'. Qed.
+ Proof. intros Hl <-. revert k1. by induction Hl; intros [|??]; f_equal/=. Qed.
Lemma Forall_zip_with_ext_r (g : A → B → C) l1 l2 k :
l1 = l2 → Forall (λ y, ∀ x, f x y = g x y) k →
zip_with f l1 k = zip_with g l2 k.
- Proof. intros <- Hk. revert l1. by induction Hk; intros [|??]; f_equal'. Qed.
+ Proof. intros <- Hk. revert l1. by induction Hk; intros [|??]; f_equal/=. Qed.
Lemma zip_with_fmap_l {D} (g : D → A) lD k :
zip_with f (g <$> lD) k = zip_with (λ z, f (g z)) lD k.
- Proof. revert k. by induction lD; intros [|??]; f_equal'. Qed.
+ Proof. revert k. by induction lD; intros [|??]; f_equal/=. Qed.
Lemma zip_with_fmap_r {D} (g : D → B) l kD :
zip_with f l (g <$> kD) = zip_with (λ x z, f x (g z)) l kD.
- Proof. revert kD. by induction l; intros [|??]; f_equal'. Qed.
+ Proof. revert kD. by induction l; intros [|??]; f_equal/=. Qed.
Lemma zip_with_nil_inv l k : zip_with f l k = [] → l = [] ∨ k = [].
- Proof. destruct l, k; intros; simplify_equality'; auto. Qed.
+ Proof. destruct l, k; intros; simplify_eq/=; auto. Qed.
Lemma zip_with_cons_inv l k z lC :
zip_with f l k = z :: lC →
∃ x y l' k', z = f x y ∧ lC = zip_with f l' k' ∧ l = x :: l' ∧ k = y :: k'.
- Proof. intros. destruct l, k; simplify_equality'; repeat eexists. Qed.
+ Proof. intros. destruct l, k; simplify_eq/=; repeat eexists. Qed.
Lemma zip_with_app_inv l k lC1 lC2 :
zip_with f l k = lC1 ++ lC2 →
∃ l1 k1 l2 k2, lC1 = zip_with f l1 k1 ∧ lC2 = zip_with f l2 k2 ∧
@@ -3065,7 +3057,7 @@ Section zip_with.
Proof.
revert l k. induction lC1 as [|z lC1 IH]; simpl.
{ intros l k ?. by eexists [], [], l, k. }
- intros [|x l] [|y k] ?; simplify_equality'.
+ intros [|x l] [|y k] ?; simplify_eq/=.
destruct (IH l k) as (l1&k1&l2&k2&->&->&->&->&?); [done |].
exists (x :: l1), (y :: k1), l2, k2; simpl; auto with congruence.
Qed.
@@ -3100,48 +3092,48 @@ Section zip_with.
Lemma lookup_zip_with l k i :
zip_with f l k !! i = x ↠l !! i; y ↠k !! i; Some (f x y).
Proof.
- revert k i. induction l; intros [|??] [|?]; f_equal'; auto.
+ revert k i. induction l; intros [|??] [|?]; f_equal/=; auto.
by destruct (_ !! _).
Qed.
Lemma insert_zip_with l k i x y :
<[i:=f x y]>(zip_with f l k) = zip_with f (<[i:=x]>l) (<[i:=y]>k).
- Proof. revert i k. induction l; intros [|?] [|??]; f_equal'; auto. Qed.
+ Proof. revert i k. induction l; intros [|?] [|??]; f_equal/=; auto. Qed.
Lemma fmap_zip_with_l (g : C → A) l k :
(∀ x y, g (f x y) = x) → length l ≤ length k → g <$> zip_with f l k = l.
- Proof. revert k. induction l; intros [|??] ??; f_equal'; auto with lia. Qed.
+ Proof. revert k. induction l; intros [|??] ??; f_equal/=; auto with lia. Qed.
Lemma fmap_zip_with_r (g : C → B) l k :
(∀ x y, g (f x y) = y) → length k ≤ length l → g <$> zip_with f l k = k.
- Proof. revert l. induction k; intros [|??] ??; f_equal'; auto with lia. Qed.
+ Proof. revert l. induction k; intros [|??] ??; f_equal/=; auto with lia. Qed.
Lemma zip_with_zip l k : zip_with f l k = curry f <$> zip l k.
- Proof. revert k. by induction l; intros [|??]; f_equal'. Qed.
+ Proof. revert k. by induction l; intros [|??]; f_equal/=. Qed.
Lemma zip_with_fst_snd lk : zip_with f (lk.*1) (lk.*2) = curry f <$> lk.
- Proof. by induction lk as [|[]]; f_equal'. Qed.
+ Proof. by induction lk as [|[]]; f_equal/=. Qed.
Lemma zip_with_replicate n x y :
zip_with f (replicate n x) (replicate n y) = replicate n (f x y).
- Proof. by induction n; f_equal'. Qed.
+ Proof. by induction n; f_equal/=. Qed.
Lemma zip_with_replicate_l n x k :
length k ≤ n → zip_with f (replicate n x) k = f x <$> k.
- Proof. revert n. induction k; intros [|?] ?; f_equal'; auto with lia. Qed.
+ Proof. revert n. induction k; intros [|?] ?; f_equal/=; auto with lia. Qed.
Lemma zip_with_replicate_r n y l :
length l ≤ n → zip_with f l (replicate n y) = flip f y <$> l.
- Proof. revert n. induction l; intros [|?] ?; f_equal'; auto with lia. Qed.
+ Proof. revert n. induction l; intros [|?] ?; f_equal/=; auto with lia. Qed.
Lemma zip_with_replicate_r_eq n y l :
length l = n → zip_with f l (replicate n y) = flip f y <$> l.
Proof. intros; apply zip_with_replicate_r; lia. Qed.
Lemma zip_with_take n l k :
take n (zip_with f l k) = zip_with f (take n l) (take n k).
- Proof. revert n k. by induction l; intros [|?] [|??]; f_equal'. Qed.
+ Proof. revert n k. by induction l; intros [|?] [|??]; f_equal/=. Qed.
Lemma zip_with_drop n l k :
drop n (zip_with f l k) = zip_with f (drop n l) (drop n k).
Proof.
- revert n k. induction l; intros [] []; f_equal'; auto using zip_with_nil_r.
+ revert n k. induction l; intros [] []; f_equal/=; auto using zip_with_nil_r.
Qed.
Lemma zip_with_take_l n l k :
length k ≤ n → zip_with f (take n l) k = zip_with f l k.
- Proof. revert n k. induction l; intros [] [] ?; f_equal'; auto with lia. Qed.
+ Proof. revert n k. induction l; intros [] [] ?; f_equal/=; auto with lia. Qed.
Lemma zip_with_take_r n l k :
length l ≤ n → zip_with f l (take n k) = zip_with f l k.
- Proof. revert n k. induction l; intros [] [] ?; f_equal'; auto with lia. Qed.
+ Proof. revert n k. induction l; intros [] [] ?; f_equal/=; auto with lia. Qed.
Lemma Forall_zip_with_fst (P : A → Prop) (Q : C → Prop) l k :
Forall P l → Forall (λ y, ∀ x, P x → Q (f x y)) k →
Forall Q (zip_with f l k).
@@ -3159,7 +3151,7 @@ Lemma zip_with_sublist_alter {A B} (f : A → B → A) g l k i n l' k' :
zip_with f (sublist_alter g i n l) k = sublist_alter g i n (zip_with f l k).
Proof.
unfold sublist_lookup, sublist_alter. intros Hlen; rewrite Hlen.
- intros ?? Hl' Hk'. simplify_option_equality.
+ intros ?? Hl' Hk'. simplify_option_eq.
by rewrite !zip_with_app_l, !zip_with_drop, Hl', drop_drop, !zip_with_take,
!take_length_le, Hk' by (rewrite ?drop_length; auto with lia).
Qed.
@@ -3173,7 +3165,7 @@ Section zip.
Lemma snd_zip l k : length k ≤ length l → (zip l k).*2 = k.
Proof. by apply fmap_zip_with_r. Qed.
Lemma zip_fst_snd (lk : list (A * B)) : zip (lk.*1) (lk.*2) = lk.
- Proof. by induction lk as [|[]]; f_equal'. Qed.
+ Proof. by induction lk as [|[]]; f_equal/=. Qed.
Lemma Forall2_fst P l1 l2 k1 k2 :
length l2 = length k2 → Forall2 P l1 k1 →
Forall2 (λ x y, P (x.1) (y.1)) (zip l1 l2) (zip k1 k2).
@@ -3323,16 +3315,16 @@ Ltac decompose_elem_of_list := repeat
| H : _ ∈ _ ++ _ |- _ => apply elem_of_app in H; destruct H
end.
Ltac solve_length :=
- simplify_equality';
+ simplify_eq/=;
repeat (rewrite fmap_length || rewrite app_length);
repeat match goal with
| H : @eq (list _) _ _ |- _ => apply (f_equal length) in H
| H : Forall2 _ _ _ |- _ => apply Forall2_length in H
| H : context[length (_ <$> _)] |- _ => rewrite fmap_length in H
end; done || congruence.
-Ltac simplify_list_equality ::= repeat
+Ltac simplify_list_eq ::= repeat
match goal with
- | _ => progress simplify_equality'
+ | _ => progress simplify_eq/=
| H : [?x] !! ?i = Some ?y |- _ =>
destruct i; [change (Some x = Some y) in H | discriminate]
| H : _ <$> _ = [] |- _ => apply fmap_nil_inv in H
@@ -3394,7 +3386,7 @@ Ltac decompose_Forall_hyps :=
| H : Forall2 _ ?l (_ ++ _) |- _ =>
let l1 := fresh l "_1" in let l2 := fresh l "_2" in
apply Forall2_app_inv_r in H; destruct H as (l1&l2&?&?&->)
- | _ => progress simplify_equality'
+ | _ => progress simplify_eq/=
| H : Forall3 _ _ (_ :: _) _ |- _ =>
apply Forall3_cons_inv_m in H; destruct H as (?&?&?&?&?&?&?&?)
| H : Forall2 _ (_ :: _) ?k |- _ =>
@@ -3442,10 +3434,10 @@ Ltac decompose_Forall_hyps :=
end
end.
Ltac list_simplifier :=
- simplify_equality';
+ simplify_eq/=;
repeat match goal with
| _ => progress decompose_Forall_hyps
- | _ => progress simplify_list_equality
+ | _ => progress simplify_list_eq
| H : _ <$> _ = _ :: _ |- _ =>
apply fmap_cons_inv in H; destruct H as (?&?&?&?&?)
| H : _ :: _ = _ <$> _ |- _ => symmetry in H
@@ -3498,7 +3490,7 @@ Ltac simplify_suffix_of := repeat
| H : suffix_of ?x ?x |- _ => clear H
| H : suffix_of ?x (_ :: ?x) |- _ => clear H
| H : suffix_of ?x (_ ++ ?x) |- _ => clear H
- | _ => progress simplify_equality'
+ | _ => progress simplify_eq/=
end.
(** The [solve_suffix_of] tactic tries to solve goals involving [suffix_of]. It
diff --git a/theories/listset.v b/theories/listset.v
index 362bcbd5..09eb5e3a 100644
--- a/theories/listset.v
+++ b/theories/listset.v
@@ -27,7 +27,7 @@ Proof.
Qed.
Lemma listset_empty_alt X : X ≡ ∅ ↔ listset_car X = [].
Proof.
- destruct X as [l]; split; [|by intros; simplify_equality'].
+ destruct X as [l]; split; [|by intros; simplify_eq/=].
intros [Hl _]; destruct l as [|x l]; [done|]. feed inversion (Hl x); left.
Qed.
Global Instance listset_empty_dec (X : listset A) : Decision (X ≡ ∅).
diff --git a/theories/mapset.v b/theories/mapset.v
index b8dfca09..8b980784 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -50,7 +50,7 @@ Proof.
- unfold empty, elem_of, mapset_empty, mapset_elem_of.
simpl. intros. by simpl_map.
- unfold singleton, elem_of, mapset_singleton, mapset_elem_of.
- simpl. by split; intros; simplify_map_equality.
+ simpl. by split; intros; simplify_map_eq.
- unfold union, elem_of, mapset_union, mapset_elem_of.
intros [m1] [m2] ?. simpl. rewrite lookup_union_Some_raw.
destruct (m1 !! x) as [[]|]; tauto.
diff --git a/theories/natmap.v b/theories/natmap.v
index 707bb749..9c7e8995 100644
--- a/theories/natmap.v
+++ b/theories/natmap.v
@@ -34,7 +34,7 @@ Lemma natmap_eq {A} (m1 m2 : natmap A) :
m1 = m2 ↔ natmap_car m1 = natmap_car m2.
Proof.
split; [by intros ->|intros]; destruct m1 as [t1 ?], m2 as [t2 ?].
- simplify_equality'; f_equal; apply proof_irrel.
+ simplify_eq/=; f_equal; apply proof_irrel.
Qed.
Global Instance natmap_eq_dec `{∀ x y : A, Decision (x = y)}
(m1 m2 : natmap A) : Decision (m1 = m2) :=
@@ -51,7 +51,7 @@ Fixpoint natmap_singleton_raw {A} (i : nat) (x : A) : natmap_raw A :=
match i with 0 => [Some x]| S i => None :: natmap_singleton_raw i x end.
Lemma natmap_singleton_wf {A} (i : nat) (x : A) :
natmap_wf (natmap_singleton_raw i x).
-Proof. unfold natmap_wf. induction i as [|[]]; simplify_equality'; eauto. Qed.
+Proof. unfold natmap_wf. induction i as [|[]]; simplify_eq/=; eauto. Qed.
Lemma natmap_lookup_singleton_raw {A} (i : nat) (x : A) :
mjoin (natmap_singleton_raw i x !! i) = Some x.
Proof. induction i; simpl; auto. Qed.
@@ -162,7 +162,7 @@ Proof.
split.
- revert j. induction l as [|[y|] l IH]; intros j; simpl.
+ by rewrite elem_of_nil.
- + rewrite elem_of_cons. intros [?|?]; simplify_equality.
+ + rewrite elem_of_cons. intros [?|?]; simplify_eq.
* by exists 0.
* destruct (IH (S j)) as (i'&?&?); auto.
exists (S i'); simpl; auto with lia.
@@ -171,9 +171,9 @@ Proof.
- 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|].
+ + destruct i as [|i]; simplify_eq/=; [left|].
right. rewrite <-Nat.add_succ_r. by apply (IH i (S j)).
- + destruct i as [|i]; simplify_equality'.
+ + destruct i as [|i]; simplify_eq/=.
rewrite <-Nat.add_succ_r. by apply (IH i (S j)).
Qed.
Lemma natmap_elem_of_to_list_raw {A} (l : natmap_raw A) i x :
diff --git a/theories/nmap.v b/theories/nmap.v
index 61aac7af..c839a659 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -64,9 +64,9 @@ Proof.
- intros ? t i x. unfold map_to_list. split.
+ destruct t as [[y|] t]; simpl.
* rewrite elem_of_cons, elem_of_list_fmap.
- intros [? | [[??] [??]]]; simplify_equality'; [done |].
+ intros [? | [[??] [??]]]; simplify_eq/=; [done |].
by apply elem_of_map_to_list.
- * rewrite elem_of_list_fmap; intros [[??] [??]]; simplify_equality'.
+ * rewrite elem_of_list_fmap; intros [[??] [??]]; simplify_eq/=.
by apply elem_of_map_to_list.
+ destruct t as [[y|] t]; simpl.
* rewrite elem_of_cons, elem_of_list_fmap.
diff --git a/theories/numbers.v b/theories/numbers.v
index c77bb160..374ff1b8 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -138,13 +138,13 @@ Fixpoint Preverse_go (p1 p2 : positive) : positive :=
Definition Preverse : positive → positive := Preverse_go 1.
Global Instance: LeftId (=) 1 (++).
-Proof. intros p. by induction p; intros; f_equal'. Qed.
+Proof. intros p. by induction p; intros; f_equal/=. Qed.
Global Instance: RightId (=) 1 (++).
Proof. done. Qed.
Global Instance: Assoc (=) (++).
-Proof. intros ?? p. by induction p; intros; f_equal'. Qed.
+Proof. intros ?? p. by induction p; intros; f_equal/=. Qed.
Global Instance: ∀ p : positive, Inj (=) (=) (++ p).
-Proof. intros p ???. induction p; simplify_equality; auto. Qed.
+Proof. intros p ???. induction p; simplify_eq; auto. Qed.
Lemma Preverse_go_app p1 p2 p3 :
Preverse_go p1 (p2 ++ p3) = Preverse_go p1 p3 ++ Preverse_go 1 p2.
@@ -166,7 +166,7 @@ Proof Preverse_app p (1~1).
Fixpoint Plength (p : positive) : nat :=
match p with 1 => 0%nat | p~0 | p~1 => S (Plength p) end.
Lemma Papp_length p1 p2 : Plength (p1 ++ p2) = (Plength p2 + Plength p1)%nat.
-Proof. by induction p2; f_equal'. Qed.
+Proof. by induction p2; f_equal/=. Qed.
Close Scope positive_scope.
diff --git a/theories/option.v b/theories/option.v
index c7f8ffec..76d4a80e 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -162,7 +162,7 @@ Lemma option_bind_assoc {A B C} (f : A → option B)
Proof. by destruct x; simpl. Qed.
Lemma option_bind_ext {A B} (f g : A → option B) x y :
(∀ a, f a = g a) → x = y → x ≫= f = y ≫= g.
-Proof. intros. destruct x, y; simplify_equality; csimpl; auto. Qed.
+Proof. intros. destruct x, y; simplify_eq; csimpl; auto. Qed.
Lemma option_bind_ext_fun {A B} (f g : A → option B) x :
(∀ a, f a = g a) → x ≫= f = x ≫= g.
Proof. intros. by apply option_bind_ext. Qed.
@@ -173,7 +173,7 @@ Lemma bind_None {A B} (f : A → option B) (x : option A) :
x ≫= f = None ↔ x = None ∨ ∃ a, x = Some a ∧ f a = None.
Proof.
split; [|by intros [->|(?&->&?)]].
- destruct x; intros; simplify_equality'; eauto.
+ destruct x; intros; simplify_eq/=; eauto.
Qed.
Lemma bind_with_Some {A} (x : option A) : x ≫= Some = x.
Proof. by destruct x. Qed.
@@ -224,7 +224,7 @@ Instance option_difference_with {A} : DifferenceWith A (option A) := λ f x y,
Instance option_union {A} : Union (option A) := union_with (λ x _, Some x).
Lemma option_union_Some {A} (x y : option A) z :
x ∪ y = Some z → x = Some z ∨ y = Some z.
-Proof. destruct x, y; intros; simplify_equality; auto. Qed.
+Proof. destruct x, y; intros; simplify_eq; auto. Qed.
Section option_union_intersection_difference.
Context {A} (f : A → A → option A).
@@ -317,9 +317,9 @@ Tactic Notation "simpl_option" "by" tactic3(tac) :=
| |- context [None ∪ _] => rewrite (left_id_L None (∪))
| |- context [_ ∪ None] => rewrite (right_id_L None (∪))
end.
-Tactic Notation "simplify_option_equality" "by" tactic3(tac) :=
+Tactic Notation "simplify_option_eq" "by" tactic3(tac) :=
repeat match goal with
- | _ => progress simplify_equality'
+ | _ => progress simplify_eq/=
| _ => progress simpl_option by tac
| _ : maybe _ ?x = Some _ |- _ => is_var x; destruct x
| _ : maybe2 _ ?x = Some _ |- _ => is_var x; destruct x
@@ -349,4 +349,4 @@ Tactic Notation "simplify_option_equality" "by" tactic3(tac) :=
| _ => progress case_decide
| _ => progress case_option_guard
end.
-Tactic Notation "simplify_option_equality" := simplify_option_equality by eauto.
+Tactic Notation "simplify_option_eq" := simplify_option_eq by eauto.
diff --git a/theories/orders.v b/theories/orders.v
index 2bb3a1aa..67fa70ee 100644
--- a/theories/orders.v
+++ b/theories/orders.v
@@ -93,7 +93,7 @@ End strict_orders.
Ltac simplify_order := repeat
match goal with
- | _ => progress simplify_equality
+ | _ => progress simplify_eq/=
| H : ?R ?x ?x |- _ => by destruct (irreflexivity _ _ H)
| H1 : ?R ?x ?y |- _ =>
match goal with
@@ -161,7 +161,7 @@ Section sorted.
{ rewrite Forall_forall in Hx1, Hx2.
assert (x2 ∈ x1 :: l1) as Hx2' by (by rewrite E; left).
assert (x1 ∈ x2 :: l2) as Hx1' by (by rewrite <-E; left).
- inversion Hx1'; inversion Hx2'; simplify_equality; auto. }
+ inversion Hx1'; inversion Hx2'; simplify_eq; auto. }
f_equal. by apply IH, (inj (x2 ::)).
Qed.
Lemma Sorted_unique `{!Transitive R, !AntiSymm (=) R} l1 l2 :
diff --git a/theories/pmap.v b/theories/pmap.v
index 8dc8ae4e..38ee6226 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -176,7 +176,7 @@ 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.
+ - rewrite elem_of_cons. intros [?|?]; simplify_eq.
{ 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 _). }
@@ -194,13 +194,13 @@ Proof.
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'.
+ - rewrite elem_of_cons. destruct i as [i|i|]; simplify_eq/=.
+ 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_eq/=.
+ apply help. specialize (IHr (j~1) i).
rewrite Preverse_xI, (assoc_L _) in IHr. by apply IHr.
+ specialize (IHl (j~0) i).
@@ -264,7 +264,7 @@ Arguments pmap_prf {_} _.
Lemma Pmap_eq {A} (m1 m2 : Pmap A) : m1 = m2 ↔ pmap_car m1 = pmap_car m2.
Proof.
split; [by intros ->|intros]; destruct m1 as [t1 ?], m2 as [t2 ?].
- simplify_equality'; f_equal; apply proof_irrel.
+ simplify_eq/=; f_equal; apply proof_irrel.
Qed.
Instance Pmap_eq_dec `{∀ x y : A, Decision (x = y)}
(m1 m2 : Pmap A) : Decision (m1 = m2) :=
@@ -341,14 +341,14 @@ Lemma Pfresh_at_depth_fresh {A} (m : Pmap_raw A) d i :
Proof.
revert i m; induction d as [|d IH].
{ intros i [|[] l r] ?; naive_solver. }
- intros i [|o l r] ?; simplify_equality'.
+ intros i [|o l r] ?; simplify_eq/=.
destruct (Pfresh_at_depth l d) as [i'|] eqn:?,
- (Pfresh_at_depth r d) as [i''|] eqn:?; simplify_equality'; auto.
+ (Pfresh_at_depth r d) as [i''|] eqn:?; simplify_eq/=; auto.
Qed.
Lemma Pfresh_go_fresh {A} (m : Pmap_raw A) d i :
Pfresh_go m d = Some i → m !! i = None.
Proof.
- induction d as [|d IH]; intros; simplify_equality'.
+ induction d as [|d IH]; intros; simplify_eq/=.
destruct (Pfresh_go m d); eauto using Pfresh_at_depth_fresh.
Qed.
Lemma Pfresh_depth {A} (m : Pmap_raw A) :
diff --git a/theories/pretty.v b/theories/pretty.v
index c7b8d50e..e7f0b645 100644
--- a/theories/pretty.v
+++ b/theories/pretty.v
@@ -57,7 +57,7 @@ Proof.
{ intros -> Hlen; edestruct help; rewrite Hlen; simpl; lia. }
{ intros <- Hlen; edestruct help; rewrite <-Hlen; simpl; lia. }
intros Hs Hlen; apply IH in Hs; destruct Hs;
- simplify_equality'; split_ands'; auto using N.div_lt_upper_bound with lia.
+ simplify_eq/=; split_ands'; auto using N.div_lt_upper_bound with lia.
rewrite (N.div_mod x 10), (N.div_mod y 10) by done.
auto using N.mod_lt with f_equal.
Qed.
diff --git a/theories/stringmap.v b/theories/stringmap.v
index e320a190..7050cddb 100644
--- a/theories/stringmap.v
+++ b/theories/stringmap.v
@@ -24,7 +24,7 @@ Proof.
cut (n2 - 1 < n2); [|lia]. clear n1 Hn Hs; revert IH; generalize (n2 - 1).
intros n1. induction 1 as [n2 _ IH]; constructor; intros n3 [??].
apply IH; [|lia]; split; [lia|].
- by rewrite lookup_delete_ne by (intros ?; simplify_equality'; lia).
+ by rewrite lookup_delete_ne by (intros ?; simplify_eq/=; lia).
Qed.
Definition fresh_string_go {A} (s : string) (m : stringmap A) (n : N)
(go : ∀ n', R s m n' n → string) : string :=
diff --git a/theories/strings.v b/theories/strings.v
index 9fa15499..355e966a 100644
--- a/theories/strings.v
+++ b/theories/strings.v
@@ -15,7 +15,7 @@ Instance assci_eq_dec : ∀ a1 a2, Decision (a1 = a2) := ascii_dec.
Instance string_eq_dec (s1 s2 : string) : Decision (s1 = s2).
Proof. solve_decision. Defined.
Instance: Inj (=) (=) (String.append s1).
-Proof. intros s1 ???. induction s1; simplify_equality'; f_equal'; auto. Qed.
+Proof. intros s1 ???. induction s1; simplify_eq/=; f_equal/=; auto. Qed.
(* Reverse *)
Fixpoint string_rev_app (s1 s2 : string) : string :=
@@ -65,7 +65,7 @@ Definition string_of_pos (p : positive) : string :=
string_of_digits (digits_of_pos p).
Lemma string_of_to_pos s : string_of_pos (string_to_pos s) = s.
Proof.
- unfold string_of_pos. by induction s as [|[[][][][][][][][]]]; f_equal'.
+ unfold string_of_pos. by induction s as [|[[][][][][][][][]]]; f_equal/=.
Qed.
Program Instance string_countable : Countable string := {|
encode := string_to_pos; decode p := Some (string_of_pos p)
diff --git a/theories/tactics.v b/theories/tactics.v
index 79382c3c..2962abb1 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -117,8 +117,7 @@ does the converse. *)
Ltac var_eq x1 x2 := match x1 with x2 => idtac | _ => fail 1 end.
Ltac var_neq x1 x2 := match x1 with x2 => fail 1 | _ => idtac end.
-(** The tactic [simplify_equality] repeatedly substitutes, discriminates,
-and injects equalities, and tries to contradict impossible inequalities. *)
+(** Hacks to let simpl fold type class projections *)
Ltac fold_classes :=
repeat match goal with
| |- appcontext [ ?F ] =>
@@ -161,7 +160,9 @@ Tactic Notation "csimpl" := try (progress simpl; fold_classes).
Tactic Notation "csimpl" "in" "*" :=
repeat_on_hyps (fun H => csimpl in H); csimpl.
-Ltac simplify_equality := repeat
+(* The tactic [simplify_eq] repeatedly substitutes, discriminates,
+and injects equalities, and tries to contradict impossible inequalities. *)
+Tactic Notation "simplify_eq" := repeat
match goal with
| H : _ ≠_ |- _ => by destruct H
| H : _ = _ → False |- _ => by destruct H
@@ -184,8 +185,9 @@ Ltac simplify_equality := repeat
assert (y = x) by congruence; clear H2
| H1 : ?o = Some ?x, H2 : ?o = None |- _ => congruence
end.
-Ltac simplify_equality' := repeat (progress csimpl in * || simplify_equality).
-Ltac f_equal' := csimpl in *; f_equal.
+Tactic Notation "simplify_eq" "/=" :=
+ repeat (progress csimpl in * || simplify_eq).
+Tactic Notation "f_equal" "/=" := csimpl in *; f_equal.
Ltac setoid_subst_aux R x :=
match goal with
@@ -202,7 +204,7 @@ Ltac setoid_subst_aux R x :=
end.
Ltac setoid_subst :=
repeat match goal with
- | _ => progress simplify_equality'
+ | _ => progress simplify_eq/=
| H : @equiv ?A ?e ?x _ |- _ => setoid_subst_aux (@equiv A e) x
| H : @equiv ?A ?e _ ?x |- _ => symmetry in H; setoid_subst_aux (@equiv A e) x
end.
@@ -315,7 +317,7 @@ Tactic Notation "naive_solver" tactic(tac) :=
| H : ∃ _, _ |- _ => destruct H
| H : ?P → ?Q, H2 : ?P |- _ => specialize (H H2)
(**i simplify and solve equalities *)
- | |- _ => progress simplify_equality'
+ | |- _ => progress simplify_eq/=
(**i solve the goal *)
| |- _ =>
solve
diff --git a/theories/vector.v b/theories/vector.v
index 445a383e..e1b00a72 100644
--- a/theories/vector.v
+++ b/theories/vector.v
@@ -73,7 +73,7 @@ Instance: Inj (=) (=) (@FS n).
Proof. intros n i j. apply Fin.FS_inj. Qed.
Instance: Inj (=) (=) (@fin_to_nat n).
Proof.
- intros n i. induction i; intros j; inv_fin j; intros; f_equal'; auto with lia.
+ intros n i. induction i; intros j; inv_fin j; intros; f_equal/=; auto with lia.
Qed.
Lemma fin_to_nat_lt {n} (i : fin n) : fin_to_nat i < n.
Proof. induction i; simpl; lia. Qed.
@@ -203,9 +203,9 @@ Lemma vec_to_list_cons {A n} x (v : vec A n) :
Proof. done. Qed.
Lemma vec_to_list_app {A n m} (v : vec A n) (w : vec A m) :
vec_to_list (v +++ w) = vec_to_list v ++ vec_to_list w.
-Proof. by induction v; f_equal'. Qed.
+Proof. by induction v; f_equal/=. Qed.
Lemma vec_to_list_of_list {A} (l : list A): vec_to_list (list_to_vec l) = l.
-Proof. by induction l; f_equal'. Qed.
+Proof. by induction l; f_equal/=. Qed.
Lemma vec_to_list_length {A n} (v : vec A n) : length (vec_to_list v) = n.
Proof. induction v; simpl; by f_equal. Qed.
Lemma vec_to_list_same_length {A B n} (v : vec A n) (w : vec B n) :
@@ -215,13 +215,13 @@ Lemma vec_to_list_inj1 {A n m} (v : vec A n) (w : vec A m) :
vec_to_list v = vec_to_list w → n = m.
Proof.
revert m w. induction v; intros ? [|???] ?;
- simplify_equality'; f_equal; eauto.
+ simplify_eq/=; f_equal; eauto.
Qed.
Lemma vec_to_list_inj2 {A n} (v : vec A n) (w : vec A n) :
vec_to_list v = vec_to_list w → v = w.
Proof.
revert w. induction v; intros w; inv_vec w; intros;
- simplify_equality'; f_equal; eauto.
+ simplify_eq/=; f_equal; eauto.
Qed.
Lemma vlookup_middle {A n m} (v : vec A n) (w : vec A m) x :
∃ i : fin (n + S m), x = (v +++ x ::: w) !!! i.
@@ -327,4 +327,4 @@ Proof.
intros. apply IHi. congruence.
Qed.
Lemma vlookup_insert_self {A n} i (v : vec A n) : vinsert i (v !!! i) v = v.
-Proof. by induction v; inv_fin i; intros; f_equal'. Qed.
+Proof. by induction v; inv_fin i; intros; f_equal/=. Qed.
diff --git a/theories/zmap.v b/theories/zmap.v
index 0b14cba4..58a7059d 100644
--- a/theories/zmap.v
+++ b/theories/zmap.v
@@ -73,10 +73,10 @@ Proof.
- 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.
- intros [?|[[[??][??]]|[[??][??]]]]; simplify_equality'; [done| |];
+ intros [?|[[[??][??]]|[[??][??]]]]; simplify_eq/=; [done| |];
by apply elem_of_map_to_list.
* rewrite elem_of_app, !elem_of_list_fmap. intros [[[??][??]]|[[??][??]]];
- simplify_equality'; by apply elem_of_map_to_list.
+ simplify_eq/=; 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.
destruct i as [|i|i]; simpl; [intuition congruence| |].
--
GitLab