Commit 20690605 authored by Robbert Krebbers's avatar 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 8f0d5ae3
...@@ -120,7 +120,7 @@ Lemma elem_to_Pset_singleton p q : e_of p (coPset_singleton_raw q) ↔ p = q. ...@@ -120,7 +120,7 @@ Lemma elem_to_Pset_singleton p q : e_of p (coPset_singleton_raw q) ↔ p = q.
Proof. Proof.
split; [|by intros <-; induction p; simpl; rewrite ?coPset_elem_of_node]. split; [|by intros <-; induction p; simpl; rewrite ?coPset_elem_of_node].
by revert q; induction p; intros [?|?|]; simpl; 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. Qed.
Lemma elem_to_Pset_union t1 t2 p : e_of p (t1 t2) = e_of p t1 || e_of p t2. Lemma elem_to_Pset_union t1 t2 p : e_of p (t1 t2) = e_of p t1 || e_of p t2.
Proof. Proof.
...@@ -226,13 +226,13 @@ Definition coPpick (X : coPset) : positive := from_option 1 (coPpick_raw (`X)). ...@@ -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. Lemma coPpick_raw_elem_of t i : coPpick_raw t = Some i e_of i t.
Proof. Proof.
revert i; induction t as [[]|[] l ? r]; intros i ?; simplify_equality'; auto. revert i; induction t as [[]|[] l ? r]; intros i ?; simplify_eq/=; auto.
destruct (coPpick_raw l); simplify_option_equality; auto. destruct (coPpick_raw l); simplify_option_eq; auto.
Qed. Qed.
Lemma coPpick_raw_None t : coPpick_raw t = None coPset_finite t. Lemma coPpick_raw_None t : coPpick_raw t = None coPset_finite t.
Proof. Proof.
induction t as [[]|[] l ? r]; intros i; simplify_equality'; auto. induction t as [[]|[] l ? r]; intros i; simplify_eq/=; auto.
destruct (coPpick_raw l); simplify_option_equality; auto. destruct (coPpick_raw l); simplify_option_eq; auto.
Qed. Qed.
Lemma coPpick_elem_of X : ¬set_finite X coPpick X X. Lemma coPpick_elem_of X : ¬set_finite X coPpick X X.
Proof. Proof.
......
...@@ -359,9 +359,9 @@ Section collection_ops. ...@@ -359,9 +359,9 @@ Section collection_ops.
- revert x. induction Xs; simpl; intros x HXs; [eexists [], x; intuition|]. - revert x. induction Xs; simpl; intros x HXs; [eexists [], x; intuition|].
rewrite elem_of_intersection_with in HXs; destruct HXs as (x1&x2&?&?&?). rewrite elem_of_intersection_with in HXs; destruct HXs as (x1&x2&?&?&?).
destruct (IHXs x2) as (xs & y & hy & ? & ?); trivial. 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. - 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. rewrite elem_of_intersection_with. naive_solver.
Qed. Qed.
...@@ -371,7 +371,7 @@ Section collection_ops. ...@@ -371,7 +371,7 @@ Section collection_ops.
( x y z, Q x P y f x y = Some z P z) ( x y z, Q x P y f x y = Some z P z)
x, x intersection_with_list f Y Xs P x. x, x intersection_with_list f Y Xs P x.
Proof. 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. intros x Hx. rewrite elem_of_intersection_with in Hx.
decompose_Forall. destruct Hx as (? & ? & ? & ? & ?). eauto. decompose_Forall. destruct Hx as (? & ? & ? & ? & ?). eauto.
Qed. Qed.
...@@ -490,7 +490,7 @@ Section fresh. ...@@ -490,7 +490,7 @@ Section fresh.
Global Instance fresh_list_proper: Global Instance fresh_list_proper:
Proper ((=) ==> () ==> (=)) (fresh_list (C:=C)). Proper ((=) ==> () ==> (=)) (fresh_list (C:=C)).
Proof. 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. apply IH. by rewrite E.
Qed. Qed.
...@@ -585,7 +585,7 @@ Section collection_monad. ...@@ -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. Forall (λ x, y, y g x f y = x) l k mapM g l fmap f k = l.
Proof. Proof.
intros Hl. revert k. induction Hl; simpl; intros; intros Hl. revert k. induction Hl; simpl; intros;
decompose_elem_of; f_equal'; auto. decompose_elem_of; f_equal/=; auto.
Qed. Qed.
Lemma elem_of_mapM_Forall {A B} (f : A M B) (P : B Prop) l k : 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. 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 := ...@@ -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. Lemma prod_decode_encode_fst p q : prod_decode_fst (prod_encode p q) = Some p.
Proof. Proof.
assert ( p, prod_decode_fst (prod_encode_fst p) = Some p). 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). assert ( p, prod_decode_fst (prod_encode_snd p) = None).
{ intros p'. by induction p'; simplify_option_equality. } { intros p'. by induction p'; simplify_option_eq. }
revert q. by induction p; intros [?|?|]; simplify_option_equality. revert q. by induction p; intros [?|?|]; simplify_option_eq.
Qed. Qed.
Lemma prod_decode_encode_snd p q : prod_decode_snd (prod_encode p q) = Some q. Lemma prod_decode_encode_snd p q : prod_decode_snd (prod_encode p q) = Some q.
Proof. Proof.
assert ( p, prod_decode_snd (prod_encode_snd p) = Some p). 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). assert ( p, prod_decode_snd (prod_encode_fst p) = None).
{ intros p'. by induction p'; simplify_option_equality. } { intros p'. by induction p'; simplify_option_eq. }
revert q. by induction p; intros [?|?|]; simplify_option_equality. revert q. by induction p; intros [?|?|]; simplify_option_eq.
Qed. Qed.
Program Instance prod_countable `{Countable A} `{Countable B} : Program Instance prod_countable `{Countable A} `{Countable B} :
Countable (A * B)%type := {| Countable (A * B)%type := {|
...@@ -191,7 +191,7 @@ Fixpoint list_decode `{Countable A} (acc : list A) ...@@ -191,7 +191,7 @@ Fixpoint list_decode `{Countable A} (acc : list A)
| p~1 => x decode_nat n; list_decode (x :: acc) O p | p~1 => x decode_nat n; list_decode (x :: acc) O p
end. end.
Lemma x0_iter_x1 n acc : Nat.iter n (~0) acc~1 = acc ++ Nat.iter n (~0) 3. 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 : Lemma list_encode_app' `{Countable A} (l1 l2 : list A) acc :
list_encode acc (l1 ++ l2) = list_encode acc l1 ++ list_encode 1 l2. list_encode acc (l1 ++ l2) = list_encode acc l1 ++ list_encode 1 l2.
Proof. Proof.
...@@ -226,7 +226,7 @@ Lemma list_encode_suffix_eq `{Countable A} q1 q2 (l1 l2 : list A) : ...@@ -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. length l1 = length l2 q1 ++ encode l1 = q2 ++ encode l2 l1 = l2.
Proof. Proof.
revert q1 q2 l2; induction l1 as [|a1 l1 IH]; 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. rewrite !list_encode_cons, !(assoc _); intros Hl.
assert (l1 = l2) as <- by eauto; clear IH; f_equal. assert (l1 = l2) as <- by eauto; clear IH; f_equal.
apply (inj encode_nat); apply (inj (++ encode l1)) in Hl; revert Hl; clear. apply (inj encode_nat); apply (inj (++ encode l1)) in Hl; revert Hl; clear.
......
...@@ -87,7 +87,7 @@ Tactic Notation "simplify_error_equality" := ...@@ -87,7 +87,7 @@ Tactic Notation "simplify_error_equality" :=
| H : (gets _ = _) _ = _ |- _ => rewrite error_left_gets in H | H : (gets _ = _) _ = _ |- _ => rewrite error_left_gets in H
| H : (modify _ = _) _ = _ |- _ => rewrite error_left_modify in H | H : (modify _ = _) _ = _ |- _ => rewrite error_left_modify in H
| H : error_guard _ _ _ _ = _ |- _ => apply error_guard_ret in H; destruct H | H : error_guard _ _ _ _ = _ |- _ => apply error_guard_ret in H; destruct H
| _ => progress simplify_equality' | _ => progress simplify_eq/=
| H : error_of_option _ _ _ = _ |- _ => | H : error_of_option _ _ _ = _ |- _ =>
apply error_of_option_ret in H; destruct H apply error_of_option_ret in H; destruct H
| H : mbind (M:=error _ _) _ _ _ = _ |- _ => | H : mbind (M:=error _ _) _ _ _ = _ |- _ =>
...@@ -117,7 +117,7 @@ Tactic Notation "error_proceed" := ...@@ -117,7 +117,7 @@ Tactic Notation "error_proceed" :=
| H : ((_ = _) = _) _ = _ |- _ => rewrite error_assoc in H | H : ((_ = _) = _) _ = _ |- _ => rewrite error_assoc in H
| H : (error_guard _ _ _) _ = _ |- _ => | H : (error_guard _ _ _) _ = _ |- _ =>
let H' := fresh in apply error_guard_ret in H; destruct H as [H' H] 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 : maybe _ ?x = Some _ |- _ => is_var x; destruct x
| H : maybe2 _ ?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 | H : maybe3 _ ?x = Some _ |- _ => is_var x; destruct x
......
...@@ -67,7 +67,7 @@ Proof. unfold size, collection_size. simpl. by rewrite elements_singleton. Qed. ...@@ -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. Lemma size_singleton_inv X x y : size X = 1 x X y X x = y.
Proof. Proof.
unfold size, collection_size. simpl. rewrite <-!elem_of_elements. 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. rewrite (nil_length_inv l), !elem_of_list_singleton by done; congruence.
Qed. Qed.
Lemma collection_choose_or_empty X : ( x, x X) X . Lemma collection_choose_or_empty X : ( x, x X) X .
......
...@@ -32,7 +32,7 @@ Proof. ...@@ -32,7 +32,7 @@ Proof.
intros [Hss1 Hss2]; split; [by apply subseteq_dom |]. intros [Hss1 Hss2]; split; [by apply subseteq_dom |].
contradict Hss2. rewrite map_subseteq_spec. intros i x Hi. contradict Hss2. rewrite map_subseteq_spec. intros i x Hi.
specialize (Hss2 i). rewrite !elem_of_dom in Hss2. specialize (Hss2 i). rewrite !elem_of_dom in Hss2.
destruct Hss2; eauto. by simplify_map_equality. destruct Hss2; eauto. by simplify_map_eq.
Qed. Qed.
Lemma dom_empty {A} : dom D (@empty (M A) _) . Lemma dom_empty {A} : dom D (@empty (M A) _) .
Proof. Proof.
...@@ -47,7 +47,7 @@ Qed. ...@@ -47,7 +47,7 @@ Qed.
Lemma dom_alter {A} f (m : M A) i : dom D (alter f i m) dom D m. Lemma dom_alter {A} f (m : M A) i : dom D (alter f i m) dom D m.
Proof. Proof.
apply elem_of_equiv; intros j; rewrite !elem_of_dom; unfold is_Some. 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. destruct (m !! j); naive_solver.
Qed. Qed.
Lemma dom_insert {A} (m : M A) i x : dom D (<[i:=x]>m) {[ i ]} dom D m. 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 ...@@ -198,7 +198,7 @@ Global Instance: ∀ {A} (R : relation A), PreOrder R → PreOrder (map_included
Proof. Proof.
split; [intros m i; by destruct (m !! i); simpl|]. split; [intros m i; by destruct (m !! i); simpl|].
intros m1 m2 m3 Hm12 Hm23 i; specialize (Hm12 i); specialize (Hm23 i). 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. done || etransitivity; eauto.
Qed. Qed.
Global Instance: PartialOrder (() : relation (M A)). Global Instance: PartialOrder (() : relation (M A)).
...@@ -288,7 +288,7 @@ Qed. ...@@ -288,7 +288,7 @@ Qed.
(** ** Properties of the [alter] operation *) (** ** Properties of the [alter] operation *)
Lemma alter_ext {A} (f g : A A) (m : M A) i : 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. ( 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. 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. 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. 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 : ...@@ -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). (i = j x, m !! j = Some x y = f x) (i j m !! j = Some y).
Proof. Proof.
destruct (decide (i = j)) as [->|?]. 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. - rewrite lookup_alter_ne by done. naive_solver.
Qed. Qed.
Lemma lookup_alter_None {A} (f : A A) m i j : Lemma lookup_alter_None {A} (f : A A) m i j :
...@@ -320,7 +320,7 @@ Lemma alter_id {A} (f : A → A) m i : ...@@ -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. ( x, m !! i = Some x f x = x) alter f i m = m.
Proof. Proof.
intros Hi; apply map_eq; intros j; destruct (decide (i = j)) as [->|?]. 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. by rewrite lookup_alter_ne by done.
Qed. Qed.
...@@ -583,7 +583,7 @@ Lemma elem_of_map_of_list_1_help {A} (l : list (K * A)) i x : ...@@ -583,7 +583,7 @@ Lemma elem_of_map_of_list_1_help {A} (l : list (K * A)) i x :
Proof. Proof.
induction l as [|[j y] l IH]; csimpl; [by rewrite elem_of_nil|]. induction l as [|[j y] l IH]; csimpl; [by rewrite elem_of_nil|].
setoid_rewrite elem_of_cons. 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 [->|]. destruct (decide (i = j)) as [->|].
- rewrite lookup_insert; f_equal; eauto. - rewrite lookup_insert; f_equal; eauto.
- rewrite lookup_insert_ne by done; 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 : ...@@ -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. map_of_list l !! i = None i l.*1.
Proof. Proof.
induction l as [|[j y] l IH]; csimpl; [rewrite elem_of_nil; tauto|]. 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.
- by rewrite lookup_insert_ne; intuition. - by rewrite lookup_insert_ne; intuition.
Qed. Qed.
...@@ -708,16 +708,16 @@ Lemma lookup_imap {A B} (f : K → A → option B) m i : ...@@ -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. map_imap f m !! i = m !! i = f i.
Proof. Proof.
unfold map_imap; destruct (m !! i = f i) as [y|] eqn:Hi; simpl. 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_map_of_list_1_help.
{ apply elem_of_list_omap; exists (i,x); split; { 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'&?). 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. - 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_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. Qed.
(** ** Properties of conversion from collections *) (** ** Properties of conversion from collections *)
...@@ -729,11 +729,11 @@ Proof. ...@@ -729,11 +729,11 @@ Proof.
{ induction (NoDup_elements X) as [|i' l]; csimpl; [constructor|]. { induction (NoDup_elements X) as [|i' l]; csimpl; [constructor|].
destruct (f i') as [x'|]; csimpl; auto; constructor; auto. destruct (f i') as [x'|]; csimpl; auto; constructor; auto.
rewrite elem_of_list_fmap. setoid_rewrite elem_of_list_omap. 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. unfold map_of_collection; rewrite <-elem_of_map_of_list by done.
rewrite elem_of_list_omap. setoid_rewrite elem_of_elements; split. rewrite elem_of_list_omap. setoid_rewrite elem_of_elements; split.
- intros (?&?&?); simplify_option_equality; eauto. - intros (?&?&?); simplify_option_eq; eauto.
- intros [??]; exists i; simplify_option_equality; eauto. - intros [??]; exists i; simplify_option_eq; eauto.
Qed. Qed.
(** ** Induction principles *) (** ** Induction principles *)
...@@ -936,9 +936,9 @@ Proof. ...@@ -936,9 +936,9 @@ Proof.
split. split.
- intros Hm i P'; rewrite lookup_merge by done; intros. - intros Hm i P'; rewrite lookup_merge by done; intros.
specialize (Hm i). destruct (m1 !! i), (m2 !! i); 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. - 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. by eapply bool_decide_unpack, Hm.
Qed. Qed.
Global Instance map_relation_dec `{ x y, Decision (R x y), x, Decision (P x), Global Instance map_relation_dec `{ x y, Decision (R x y), x, Decision (P x),
...@@ -961,7 +961,7 @@ Proof. ...@@ -961,7 +961,7 @@ Proof.
destruct (m1 !! i), (m2 !! i); naive_solver auto 2 using bool_decide_pack. destruct (m1 !! i), (m2 !! i); naive_solver auto 2 using bool_decide_pack.
- unfold map_relation, option_relation. - unfold map_relation, option_relation.
by intros [i[(x&y&?&?&?)|[(x&?&?&?)|(y&?&?&?)]]] Hm; by intros [i[(x&y&?&?&?)|[(x&?&?&?)|(y&?&?&?)]]] Hm;
specialize (Hm i); simplify_option_equality. specialize (Hm i); simplify_option_eq.
Qed. Qed.
End Forall2. End Forall2.
...@@ -1081,7 +1081,7 @@ Lemma alter_union_with_l (g : A → A) m1 m2 i : ...@@ -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. alter g i (union_with f m1 m2) = union_with f (alter g i m1) m2.
Proof. Proof.
intros. apply (partial_alter_merge_l _). 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. Qed.
Lemma alter_union_with_r (g : A A) m1 m2 i : 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)) ( 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 : ...@@ -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). alter g i (union_with f m1 m2) = union_with f m1 (alter g i m2).
Proof. Proof.
intros. apply (partial_alter_merge_r _). 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. Qed.
Lemma delete_union_with m1 m2 i : Lemma delete_union_with m1 m2 i :
delete i (union_with f m1 m2) = union_with f (delete i m1) (delete i m2). 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. ...@@ -1558,11 +1558,11 @@ Hint Extern 80 (<[_:=_]> _ !! _ = Some _) => apply lookup_insert : simpl_map.
(** Now we take everything together and also discharge conflicting look ups, (** Now we take everything together and also discharge conflicting look ups,
simplify overlapping look ups, and perform cancellations of equalities simplify overlapping look ups, and perform cancellations of equalities
involving unions. *) involving unions. *)
Tactic Notation "simplify_map_equality" "by" tactic3(tac) := Tactic Notation "simplify_map_eq" "by" tactic3(tac) :=
decompose_map_disjoint; decompose_map_disjoint;
repeat match goal with repeat match goal with
| _ => progress simpl_map by tac | _ => progress simpl_map by tac
| _ => progress simplify_equality | _ => progress simplify_eq/=
| _ => progress simpl_option by tac | _ => progress simpl_option by tac
| H : {[ _ := _ ]} !! _ = None |- _ => rewrite lookup_singleton_None in H | H : {[ _ := _ ]} !! _ = None |- _ => rewrite lookup_singleton_None in H
| H : {[ _ := _ ]} !! _ = Some _ |- _ => | H : {[ _ := _ ]} !! _ = Some _ |- _ =>
...@@ -1582,11 +1582,11 @@ Tactic Notation "simplify_map_equality" "by" tactic3(tac) := ...@@ -1582,11 +1582,11 @@ Tactic Notation "simplify_map_equality" "by" tactic3(tac) :=
| H : = {[?i := ?x]} |- _ => by destruct (map_non_empty_singleton i x) | H : = {[?i := ?x]} |- _ => by destruct (map_non_empty_singleton i x)
| H : ?m !! ?i = Some _, H2 : ?m !! ?j = None |- _ => | H : ?m !! ?i = Some _, H2 : ?m !! ?j = None |- _ =>
unless (i j) by done; unless (i j) by done;
assert (i j) by (by intros ?; simplify_equality) assert (i j) by (by intros ?; simplify_eq)
end. end.
Tactic Notation "simplify_map_equality'" "by" tactic3(tac) := Tactic Notation "simplify_map_eq" "/=" "by" tactic3(tac) :=
repeat (progress csimpl in * || simplify_map_equality by tac). repeat (progress csimpl in * || simplify_map_eq by tac).
Tactic Notation "simplify_map_equality" := Tactic Notation "simplify_map_eq" :=
simplify_map_equality by eauto with simpl_map map_disjoint. simplify_map_eq by eauto with simpl_map map_disjoint.
Tactic Notation "simplify_map_equality'" := Tactic Notation "simplify_map_eq" "/=" :=
simplify_map_equality' by eauto with simpl_map map_disjoint. simplify_map_eq/= by eauto with simpl_map map_disjoint.
...@@ -48,7 +48,7 @@ Lemma find_Some `{finA: Finite A} P `{∀ x, Decision (P x)} x : ...@@ -48,7 +48,7 @@ Lemma find_Some `{finA: Finite A} P `{∀ x, Decision (P x)} x :
find P = Some x P x. find P = Some x P x.
Proof. Proof.
destruct finA as [xs Hxs HA]; unfold find, decode_nat, decode; simpl. 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. rewrite !Nat2Pos.id in Hx by done.
destruct (list_find_Some P xs i y); naive_solver. destruct (list_find_Some P xs i y); naive_solver.
Qed. Qed.
...@@ -57,13 +57,13 @@ Lemma find_is_Some `{finA: Finite A} P `{∀ x, Decision (P x)} x : ...@@ -57,13 +57,13 @@ Lemma find_is_Some `{finA: Finite A} P `{∀ x, Decision (P x)} x :
Proof. Proof.
destruct finA as [xs Hxs HA]; unfold find, decode; simpl. 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. 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. exists y. by rewrite !Nat2Pos.id by done.
Qed. Qed.
Lemma card_0_inv P `{finA: Finite A} : card A = 0 A P. Lemma card_0_inv P `{finA: Finite A} : card A = 0 A P.
Proof. Proof.
intros ? x. destruct finA as [[|??] ??]; simplify_equality. intros ? x. destruct finA as [[|??] ??]; simplify_eq.
by destruct (not_elem_of_nil x). by destruct (not_elem_of_nil x).
Qed. Qed.
Lemma finite_inhabited A `{finA: Finite A} : 0 < card A Inhabited A. Lemma finite_inhabited A `{finA: Finite A} : 0 < card A Inhabited A.
...@@ -166,7 +166,7 @@ Section enc_finite. ...@@ -166,7 +166,7 @@ Section enc_finite.
Next Obligation. Next Obligation.
apply NoDup_alt. intros i j x. rewrite !list_lookup_fmap. intros Hi Hj. apply NoDup_alt. intros i j x. rewrite !list_lookup_fmap. intros Hi Hj.
destruct (seq _ _ !! i) as [i'|] eqn:Hi', 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. destruct (lookup_seq_inv _ _ _ _ Hi'), (lookup_seq_inv _ _ _ _ Hj'); subst.
rewrite <-(to_of_nat i), <-(to_of_nat j) by done. by f_equal. rewrite <-(to_of_nat i), <-(to_of_nat j) by done. by f_equal.
Qed. Qed.
...@@ -239,11 +239,11 @@ Next Obligation. ...@@ -239,11 +239,11 @@ Next Obligation.
{ constructor. } { constructor. }
apply NoDup_app; split_ands. apply NoDup_app; split_ands.
- by apply (NoDup_fmap_2 _), NoDup_enum. - 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. clear IH. induction Hxs as [|x' xs ?? IH]; simpl.
{ rewrite elem_of_nil. tauto. } { rewrite elem_of_nil. tauto. }
rewrite elem_of_app, elem_of_list_fmap. rewrite elem_of_app, elem_of_list_fmap.
intros [(?&?&?)|?]; simplify_equality. intros [(?&?&?)|?]; simplify_eq.
+ destruct Hx. by left. + destruct Hx. by left.
+ destruct IH. by intro; destruct Hx; right. auto. + destruct IH. by intro; destruct Hx; right. auto.
- done. - done.
...@@ -274,15 +274,15 @@ Next Obligation. ...@@ -274,15 +274,15 @@ Next Obligation.
apply NoDup_app; split_ands. apply NoDup_app; split_ands.
- by apply (NoDup_fmap_2 _). - by apply (NoDup_fmap_2 _).
- intros [k1 Hk1]. clear Hxs IH. rewrite elem_of_list_fmap. - 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 |]. induction xs as [|x' xs IH]; simpl in *; [by rewrite elem_of_nil |].
rewrite elem_of_app, elem_of_list_fmap, elem_of_cons. rewrite elem_of_app, elem_of_list_fmap, elem_of_cons.
intros [([??]&?&?)|?]; simplify_equality'; auto. intros [([??]&?&?)|?]; simplify_eq/=; auto.
- apply IH. - apply IH.
Qed. Qed.
Next Obligation. Next Obligation.
intros ???? [l Hl]. revert l Hl. 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 _). } { apply elem_of_list_singleton. by apply (sig_eq_pi _). }
revert IH. generalize (list_enum (enum A) n). intros k Hk. revert IH. generalize (list_enum (enum A) n). intros k Hk.
induction (elem_of_enum x) as [x xs|x xs]; simpl in *.