Commit 5912f8b1 authored by Robbert Krebbers's avatar Robbert Krebbers

Let simplify_equality perform injection less eagerly.

Now it only performs injection on hypotheses of the shape f .. = f ..
parent 1aec4451
......@@ -940,3 +940,4 @@ Section sig_map.
apply (injective f) in Hxy; subst. rewrite (proof_irrel _ Hy). auto.
Qed.
End sig_map.
Arguments sig_map _ _ _ _ _ _ !_ /.
......@@ -41,6 +41,9 @@ Tactic Notation "case_error_guard" :=
Tactic Notation "simplify_error_equality" :=
repeat match goal with
| _ => progress simplify_equality'
| H : appcontext [@mret (sum ?E) _ ?A] |- _ =>
change (@mret (sum E) _ A) with (@inr E A) in H
| |- appcontext [@mret (sum ?E) _ ?A] => change (@mret _ _ A) with (@inr E A)
| H : error_of_option ?o ?e = ?x |- _ => apply error_of_option_inr in H
| H : mbind (M:=sum _) ?f ?o = ?x |- _ =>
apply bind_inr in H; destruct H as (?&?&?)
......@@ -71,8 +74,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:?; simpl; [discriminate|].
destruct (mapM f l); intros; simplify_equality. constructor; auto.
* destruct (f x) eqn:?; intros; simplify_error_equality; auto.
Qed.
Lemma mapM_inr_2 l k : Forall2 (λ x y, f x = inr y) l k mapM f l = inr k.
Proof.
......
......@@ -49,7 +49,7 @@ 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_equality'.
rewrite (nil_length_inv l), !elem_of_list_singleton by done. congruence.
Qed.
Lemma collection_choose_or_empty X : ( x, x X) X .
......
......@@ -734,7 +734,7 @@ 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_equality'; 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;
by eapply bool_decide_unpack, Hm.
......
......@@ -164,7 +164,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_equality'.
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.
......@@ -272,10 +272,10 @@ 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_equality'. destruct Hx. revert Hxk2.
induction xs as [|x' xs IH]; simpl in *; [by rewrite elem_of_nil |].
rewrite elem_of_app, elem_of_list_fmap, elem_of_cons.
intros [([??]&?&?)|?]; simplify_equality; auto.
intros [([??]&?&?)|?]; simplify_equality'; auto.
* apply IH.
Qed.
Next Obligation.
......
......@@ -1253,7 +1253,7 @@ 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.
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_equality'. 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 (associative_L (++)). Qed.
Lemma prefix_of_app_alt k1 k2 l1 l2 :
......@@ -1407,7 +1407,7 @@ 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.
right. simplify_equality'. 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.
......@@ -2463,7 +2463,7 @@ Section fmap.
(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_equality'; 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).
......@@ -2652,8 +2652,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:?; simpl; [|discriminate].
destruct (mapM f l); intros; simplify_equality. constructor; auto.
* destruct (f x) eqn:?; intros; simplify_option_equality; auto.
Qed.
Lemma mapM_Some_2 l k : Forall2 (λ x y, f x = Some y) l k mapM f l = Some k.
Proof.
......@@ -3229,7 +3228,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_equality'
end.
(** The [solve_suffix_of] tactic tries to solve goals involving [suffix_of]. It
......
......@@ -171,10 +171,10 @@ 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|].
right. rewrite Nat.add_succ_comm. by apply (IH i (S j)).
+ destruct i as [|i]; simplify_equality.
rewrite Nat.add_succ_comm. by apply (IH i (S j)).
+ destruct i as [|i]; simplify_equality'; [left|].
right. rewrite <-Nat.add_succ_r. by apply (IH i (S j)).
+ destruct i as [|i]; simplify_equality'.
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 :
(i,x) natmap_to_list_raw 0 l mjoin (l !! i) = Some x.
......
......@@ -63,10 +63,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; simpl; [done |].
intros [? | [[??] [??]]]; simplify_equality'; [done |].
by apply elem_of_map_to_list.
- rewrite elem_of_list_fmap.
intros [[??] [??]]; simplify_equality; simpl.
- rewrite elem_of_list_fmap; intros [[??] [??]]; simplify_equality'.
by apply elem_of_map_to_list.
+ destruct t as [[y|] t]; simpl.
- rewrite elem_of_cons, elem_of_list_fmap.
......
......@@ -209,6 +209,9 @@ Tactic Notation "simpl_option_monad" "by" tactic3(tac) :=
assert (o = Some x') as H by tac
| assert (o = None) as H by tac ]
in repeat match goal with
| H : appcontext [@mret _ _ ?A] |- _ =>
change (@mret _ _ A) with (@Some A) in H
| |- appcontext [@mret _ _ ?A] => change (@mret _ _ A) with (@Some A)
| H : context [mbind (M:=option) (A:=?A) ?f ?o] |- _ =>
let Hx := fresh in assert_Some_None A o Hx; rewrite Hx in H; clear Hx
| H : context [fmap (M:=option) (A:=?A) ?f ?o] |- _ =>
......
......@@ -141,7 +141,7 @@ Proof.
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'; constructor; eauto.
rewrite elem_of_list_fmap; intros ([p' x']&?&?); simplify_equality.
rewrite elem_of_list_fmap; intros ([p' x']&?&?); simplify_equality'.
cut (string_to_pos (string_of_pos p') = p'); [congruence|].
rewrite Forall_forall in Hm'. eapply (Hm' (_,_)); eauto.
* intros A [m Hm] s x; unfold map_to_list, lookup; simpl.
......
......@@ -205,7 +205,12 @@ Ltac simplify_equality := repeat
| H : ?f _ = ?f _ |- _ => apply (injective f) in H
| H : ?f _ _ = ?f _ _ |- _ => apply (injective2 f) in H; destruct H
(* before [injection'] to circumvent bug #2939 in some situations *)
| H : _ = _ |- _ => injection' H
| H : ?f _ = ?f _ |- _ => injection' H
| H : ?f _ _ = ?f _ _ |- _ => injection' H
| H : ?f _ _ _ = ?f _ _ _ |- _ => injection' H
| H : ?f _ _ _ _ = ?f _ _ _ _ |- _ => injection' H
| H : ?f _ _ _ _ _ = ?f _ _ _ _ _ |- _ => injection' H
| H : ?f _ _ _ _ _ _ = ?f _ _ _ _ _ _ |- _ => injection' H
| H : ?x = ?x |- _ => clear H
(* unclear how to generalize the below *)
| H1 : ?o = Some ?x, H2 : ?o = Some ?y |- _ =>
......
......@@ -73,7 +73,7 @@ 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; simpl; [done| |];
intros [?|[[[??][??]]|[[??][??]]]]; simplify_equality'; [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.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment