Commit 65ab1289 by Robbert Krebbers

### 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.```
parent 8e636f20
 ... ... @@ -54,7 +54,7 @@ Global Instance auth_timeless (x : auth A) : Timeless (authoritative x) → Timeless (own x) → Timeless x. Proof. by intros ?? [??] [??]; split; simpl in *; apply (timeless _). Qed. Global Instance auth_leibniz : LeibnizEquiv A → LeibnizEquiv (auth A). Proof. by intros ? [??] [??] [??]; f_equal'; apply leibniz_equiv. Qed. Proof. by intros ? [??] [??] [??]; f_equal/=; apply leibniz_equiv. Qed. End cofe. Arguments authC : clear implicits. ... ...
 ... ... @@ -29,13 +29,13 @@ Hint Extern 0 (_ ≡{_}≡ _) => symmetry; assumption. Tactic Notation "cofe_subst" ident(x) := repeat match goal with | _ => progress simplify_equality' | _ => progress simplify_eq/= | H:@dist ?A ?d ?n x _ |- _ => setoid_subst_aux (@dist A d n) x | H:@dist ?A ?d ?n _ x |- _ => symmetry in H;setoid_subst_aux (@dist A d n) x end. Tactic Notation "cofe_subst" := repeat match goal with | _ => progress simplify_equality' | _ => progress simplify_eq/= | H:@dist ?A ?d ?n ?x _ |- _ => setoid_subst_aux (@dist A d n) x | H:@dist ?A ?d ?n _ ?x |- _ => symmetry in H;setoid_subst_aux (@dist A d n) x end. ... ...
 ... ... @@ -115,15 +115,15 @@ Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed. Lemma gg_gg {k i i1 i2 j} (H1 : k = i + j) (H2 : k = i2 + (i1 + j)) (x : A k) : gg i (coerce H1 x) = gg i1 (gg i2 (coerce H2 x)). Proof. assert (i = i2 + i1) by lia; simplify_equality'. revert j x H1. induction i2 as [|i2 IH]; intros j X H1; simplify_equality'; assert (i = i2 + i1) by lia; simplify_eq/=. revert j x H1. induction i2 as [|i2 IH]; intros j X H1; simplify_eq/=; [by rewrite coerce_id|by rewrite g_coerce IH]. Qed. Lemma ff_ff {k i i1 i2 j} (H1 : i + k = j) (H2 : i1 + (i2 + k) = j) (x : A k) : coerce H1 (ff i x) = coerce H2 (ff i1 (ff i2 x)). Proof. assert (i = i1 + i2) by lia; simplify_equality'. induction i1 as [|i1 IH]; simplify_equality'; assert (i = i1 + i2) by lia; simplify_eq/=. induction i1 as [|i1 IH]; simplify_eq/=; [by rewrite coerce_id|by rewrite coerce_f IH]. Qed. ... ... @@ -159,7 +159,7 @@ Proof. - assert (H : S k = S (k - i) + (0 + i)) by lia; rewrite (gg_gg _ H) /=. by erewrite g_coerce, gf, coerce_proper by done. - assert (S k = 0 + (0 + i)) as H by lia. rewrite (gg_gg _ H); simplify_equality'. rewrite (gg_gg _ H); simplify_eq/=. by rewrite (ff_ff _ (eq_refl (1 + (0 + k)))). - exfalso; lia. - assert (H : (i - S k) + (1 + k) = i) by lia; rewrite (ff_ff _ H) /=. ... ...
 ... ... @@ -40,7 +40,7 @@ Program Definition excl_chain {| chain_car n := match c n return _ with Excl y => y | _ => x end |}. Next Obligation. intros c x ? n [|i] ?; [omega|]; simpl. destruct (c 1) eqn:?; simplify_equality'. destruct (c 1) eqn:?; simplify_eq/=. by feed inversion (chain_cauchy c n (S i)). Qed. Instance excl_compl : Compl (excl A) := λ c, ... ... @@ -60,13 +60,13 @@ Proof. - by inversion_clear 1; constructor; apply dist_S. - intros c n; unfold compl, excl_compl. destruct (Some_dec (maybe Excl (c 1))) as [[x Hx]|]. { assert (c 1 = Excl x) by (by destruct (c 1); simplify_equality'). { assert (c 1 = Excl x) by (by destruct (c 1); simplify_eq/=). assert (∃ y, c (S n) = Excl y) as [y Hy]. { feed inversion (chain_cauchy c 0 (S n)); eauto with lia congruence. } rewrite Hy; constructor. by rewrite (conv_compl (excl_chain c x Hx) n) /= Hy. } feed inversion (chain_cauchy c 0 (S n)); first lia; constructor; destruct (c 1); simplify_equality'. constructor; destruct (c 1); simplify_eq/=. Qed. Canonical Structure exclC : cofeT := CofeT excl_cofe_mixin. ... ...
 ... ... @@ -43,12 +43,12 @@ Global Instance alter_ne f k n : Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (alter f k). Proof. intros ? m m' Hm k'. by destruct (decide (k = k')); simplify_map_equality; rewrite (Hm k'). by destruct (decide (k = k')); simplify_map_eq; rewrite (Hm k'). Qed. Global Instance insert_ne i n : Proper (dist n ==> dist n ==> dist n) (insert (M:=gmap K A) i). Proof. intros x y ? m m' ? j; destruct (decide (i = j)); simplify_map_equality; intros x y ? m m' ? j; destruct (decide (i = j)); simplify_map_eq; [by constructor|by apply lookup_ne]. Qed. Global Instance singleton_ne i n : ... ... @@ -57,7 +57,7 @@ Proof. by intros ???; apply insert_ne. Qed. Global Instance delete_ne i n : Proper (dist n ==> dist n) (delete (M:=gmap K A) i). Proof. intros m m' ? j; destruct (decide (i = j)); simplify_map_equality; intros m m' ? j; destruct (decide (i = j)); simplify_map_eq; [by constructor|by apply lookup_ne]. Qed. ... ... @@ -79,7 +79,7 @@ Qed. Global Instance map_insert_timeless m i x : Timeless x → Timeless m → Timeless (<[i:=x]>m). Proof. intros ?? m' Hm j; destruct (decide (i = j)); simplify_map_equality. intros ?? m' Hm j; destruct (decide (i = j)); simplify_map_eq. { by apply (timeless _); rewrite -Hm lookup_insert. } by apply (timeless _); rewrite -Hm lookup_insert_ne. Qed. ... ... @@ -193,13 +193,13 @@ Proof. by move=> /(_ i) Hm Hi; move:Hm; rewrite Hi. Qed. Lemma map_lookup_valid m i x : ✓ m → m !! i ≡ Some x → ✓ x. Proof. move=>Hm Hi n. move:(Hm n i). by rewrite Hi. Qed. Lemma map_insert_validN n m i x : ✓{n} x → ✓{n} m → ✓{n} <[i:=x]>m. Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_equality. Qed. Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_eq. Qed. Lemma map_insert_valid m i x : ✓ x → ✓ m → ✓ <[i:=x]>m. Proof. intros ?? n j; apply map_insert_validN; auto. Qed. Lemma map_singleton_validN n i x : ✓{n} ({[ i := x ]} : gmap K A) ↔ ✓{n} x. Proof. split; [|by intros; apply map_insert_validN, cmra_empty_valid]. by move=>/(_ i); simplify_map_equality. by move=>/(_ i); simplify_map_eq. Qed. Lemma map_singleton_valid i x : ✓ ({[ i := x ]} : gmap K A) ↔ ✓ x. Proof. split; intros ? n; eapply map_singleton_validN; eauto. Qed. ... ... @@ -234,7 +234,7 @@ Proof. destruct (m' !! i) as [y|]; [exists (x ⋅ y)|exists x]; eauto using cmra_included_l. - intros (y&Hi&?); rewrite map_includedN_spec=>j. destruct (decide (i = j)); simplify_map_equality. destruct (decide (i = j)); simplify_map_eq. + by rewrite Hi; apply Some_Some_includedN, cmra_included_includedN. + apply None_includedN. Qed. ... ... @@ -250,10 +250,10 @@ Lemma map_insert_updateP (P : A → Prop) (Q : gmap K A → Prop) m i x : Proof. intros Hx%option_updateP' HP mf n Hm. destruct (Hx (mf !! i) n) as ([y|]&?&?); try done. { by generalize (Hm i); rewrite lookup_op; simplify_map_equality. } { by generalize (Hm i); rewrite lookup_op; simplify_map_eq. } exists (<[i:=y]> m); split; first by auto. intros j; move: (Hm j)=>{Hm}; rewrite !lookup_op=>Hm. destruct (decide (i = j)); simplify_map_equality'; auto. destruct (decide (i = j)); simplify_map_eq/=; auto. Qed. Lemma map_insert_updateP' (P : A → Prop) m i x : x ~~>: P → <[i:=x]>m ~~>: λ m', ∃ y, m' = <[i:=y]>m ∧ P y. ... ...
 ... ... @@ -13,7 +13,7 @@ Program Definition option_chain {| chain_car n := from_option x (c n) |}. Next Obligation. intros c x ? n [|i] ?; [omega|]; simpl. destruct (c 1) eqn:?; simplify_equality'. destruct (c 1) eqn:?; simplify_eq/=. by feed inversion (chain_cauchy c n (S i)). Qed. Instance option_compl : Compl (option A) := λ c, ... ...
 ... ... @@ -355,7 +355,7 @@ Lemma sts_update_frag S1 S2 T : closed S2 T → S1 ⊆ S2 → sts_frag S1 T ~~> sts_frag S2 T. Proof. rewrite /sts_frag=> HS Hcl. apply validity_update. inversion 3 as [|? S ? Tf|]; simplify_equality'. inversion 3 as [|? S ? Tf|]; simplify_eq/=. - split; first done. constructor; [solve_elem_of|done]. - split; first done. constructor; solve_elem_of. Qed. ... ...
 ... ... @@ -239,18 +239,18 @@ Inductive prim_step (** Basic properties about the language *) Lemma to_of_val v : to_val (of_val v) = Some v. Proof. by induction v; simplify_option_equality. Qed. Proof. by induction v; simplify_option_eq. Qed. Lemma of_to_val e v : to_val e = Some v → of_val v = e. Proof. revert v; induction e; intros; simplify_option_equality; auto with f_equal. revert v; induction e; intros; simplify_option_eq; auto with f_equal. Qed. Instance: Inj (=) (=) of_val. Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed. Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki). Proof. destruct Ki; intros ???; simplify_equality'; auto with f_equal. Qed. Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed. Instance ectx_fill_inj K : Inj (=) (=) (fill K). Proof. red; induction K as [|Ki K IH]; naive_solver. Qed. ... ... @@ -261,7 +261,7 @@ Proof. revert e; induction K1; simpl; auto with f_equal. Qed. Lemma fill_val K e : is_Some (to_val (fill K e)) → is_Some (to_val e). Proof. intros [v' Hv']; revert v' Hv'. induction K as [|[]]; intros; simplify_option_equality; eauto. induction K as [|[]]; intros; simplify_option_eq; eauto. Qed. Lemma fill_not_val K e : to_val e = None → to_val (fill K e) = None. ... ... @@ -297,13 +297,13 @@ Qed. Lemma head_ctx_step_val Ki e σ1 e2 σ2 ef : head_step (fill_item Ki e) σ1 e2 σ2 ef → is_Some (to_val e). Proof. destruct Ki; inversion_clear 1; simplify_option_equality; eauto. Qed. Proof. destruct Ki; inversion_clear 1; simplify_option_eq; eauto. Qed. Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 : to_val e1 = None → to_val e2 = None → fill_item Ki1 e1 = fill_item Ki2 e2 → Ki1 = Ki2. Proof. destruct Ki1, Ki2; intros; try discriminate; simplify_equality'; destruct Ki1, Ki2; intros; try discriminate; simplify_eq/=; repeat match goal with | H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H end; auto. ... ... @@ -318,7 +318,7 @@ Lemma step_by_val K K' e1 e1' σ1 e2 σ2 ef : Proof. intros Hfill Hred Hnval; revert K' Hfill. induction K as [|Ki K IH]; simpl; intros K' Hfill; auto using prefix_of_nil. destruct K' as [|Ki' K']; simplify_equality'. destruct K' as [|Ki' K']; simplify_eq/=. { exfalso; apply (eq_None_not_Some (to_val (fill K e1))); eauto using fill_not_val, head_ctx_step_val. } cut (Ki = Ki'); [naive_solver eauto using prefix_of_cons|]. ... ...
 ... ... @@ -102,14 +102,14 @@ Arguments of_val : simpl never. Lemma gsubst_None e x v : gsubst_go e x (of_val v) = None → e = subst e x v. Proof. induction e; simpl; unfold gsubst_lift; intros; repeat (simplify_option_equality || case_match); f_equal; auto. repeat (simplify_option_eq || case_match); f_equal; auto. Qed. Lemma gsubst_correct e x v : gsubst e x (of_val v) = subst e x v. Proof. unfold gsubst; destruct (gsubst_go e x (of_val v)) as [e'|] eqn:He; simpl; last by apply gsubst_None. revert e' He; induction e; simpl; unfold gsubst_lift; intros; repeat (simplify_option_equality || case_match); repeat (simplify_option_eq || case_match); f_equal; auto using gsubst_None. Qed. ... ...
 ... ... @@ -10,7 +10,7 @@ to conversions from and to values, and finite map operations. This tactic is slightly ad-hoc and tuned for proving our lifting lemmas. *) Ltac inv_step := repeat match goal with | _ => progress simplify_map_equality' (* simplify memory stuff *) | _ => progress simplify_map_eq/= (* simplify memory stuff *) | H : to_val _ = Some _ |- _ => apply of_to_val in H | H : context [to_val (of_val _)] |- _ => rewrite to_of_val in H | H : prim_step _ _ _ _ _ |- _ => destruct H; subst ... ...
 ... ... @@ -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. ... ...
 ... ... @@ -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. ... ...
 ... ... @@ -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. ... ...
 ... ... @@ -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 ... ...
 ... ... @@ -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 ≡ ∅. ... ...
 ... ... @@ -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. ... ...
 ... ... @@ -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.