Commit de5f0f84 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Let set_solver not use eauto by default.

In most cases there is a lot of duplicate proof search performed by
both naive_solver and eauto. Especially since naive_solver calls its
tactic (in the case of set_solver this used to be eauto) quite eagerly
this made it very slow.

Note that set_solver is this too slow and should be improved.
parent b7b455bd
......@@ -240,26 +240,15 @@ Proof.
- by destruct 1; simpl; intros ?; setoid_subst.
- by intros ? [|]; destruct 1; inversion_clear 1; constructor; setoid_subst.
- by do 2 destruct 1; constructor; setoid_subst.
- (* (* assert ( T T' S s,
closed S T s S tok s T' tok s (T T') ).
{ intros S T T' s [??]. set_solver. } *)
destruct 3; simpl in *; destruct_conjs;
repeat match goal with H : closed _ _ |- _ => destruct H end; eauto using closed_op with sts.
split. auto with sts.
destruct_conjs. eauto using closed_op with sts.
admit.
eapply H. eauto. eauto. *) admit.
- destruct 3; simpl in *; destruct_conjs; eauto using closed_op;
match goal with H : closed _ _ |- _ => destruct H end; set_solver.
- intros []; simpl; intros; destruct_conjs; split;
eauto using closed_up, up_non_empty, closed_up_set, up_set_empty with sts.
- intros ???? (z&Hy&?&Hxz); destruct Hxz; inversion Hy; clear Hy;
setoid_subst; destruct_conjs; split_and?;
rewrite disjoint_union_difference //;
eauto using up_set_non_empty, up_non_empty, closed_up, closed_disjoint; [].
eapply closed_up_set. intros.
eapply closed_disjoint; eauto with sts.
eapply closed_up_set=> s ?; eapply closed_disjoint; eauto with sts.
- intros [] [] []; constructor; rewrite ?assoc; auto with sts.
- destruct 4; inversion_clear 1; constructor; auto with sts.
- destruct 4; inversion_clear 1; constructor; auto with sts.
......@@ -396,8 +385,8 @@ Qed.
Lemma sts_update_auth s1 s2 T1 T2 :
steps (s1,T1) (s2,T2) sts_auth s1 T1 ~~> sts_auth s2 T2.
Proof.
intros ?; apply validity_update; inversion 3 as [|? S ? Tf|]; subst.
simpl in *. destruct_conjs.
intros ?; apply validity_update.
inversion 3 as [|? S ? Tf|]; simplify_eq/=; destruct_conjs.
destruct (steps_closed s1 s2 T1 T2 S Tf) as (?&?&?); auto; [].
repeat (done || constructor).
Qed.
......
......@@ -262,7 +262,7 @@ Tactic Notation "set_solver" "-" hyp_list(Hs) "/" tactic3(tac) :=
clear Hs; set_solver tac.
Tactic Notation "set_solver" "+" hyp_list(Hs) "/" tactic3(tac) :=
revert Hs; clear; set_solver tac.
Tactic Notation "set_solver" := set_solver eauto.
Tactic Notation "set_solver" := set_solver idtac.
Tactic Notation "set_solver" "-" hyp_list(Hs) := clear Hs; set_solver.
Tactic Notation "set_solver" "+" hyp_list(Hs) :=
revert Hs; clear; set_solver.
......@@ -537,10 +537,10 @@ Section collection_monad.
Global Instance collection_fmap_mono {A B} :
Proper (pointwise_relation _ (=) ==> () ==> ()) (@fmap M _ A B).
Proof. intros f g ? X Y ?; set_solver. Qed.
Proof. intros f g ? X Y ?; set_solver eauto. Qed.
Global Instance collection_fmap_proper {A B} :
Proper (pointwise_relation _ (=) ==> () ==> ()) (@fmap M _ A B).
Proof. intros f g ? X Y [??]; split; set_solver. Qed.
Proof. intros f g ? X Y [??]; split; set_solver eauto. Qed.
Global Instance collection_bind_mono {A B} :
Proper (((=) ==> ()) ==> () ==> ()) (@mbind M _ A B).
Proof. unfold respectful; intros f g Hfg X Y ?; set_solver. Qed.
......@@ -575,12 +575,12 @@ Section collection_monad.
l mapM f k Forall2 (λ x y, x f y) l k.
Proof.
split.
- revert l. induction k; set_solver.
- revert l. induction k; set_solver eauto.
- induction 1; set_solver.
Qed.
Lemma collection_mapM_length {A B} (f : A M B) l k :
l mapM f k length l = length k.
Proof. revert l; induction k; set_solver. Qed.
Proof. revert l; induction k; set_solver eauto. Qed.
Lemma elem_of_mapM_fmap {A B} (f : A B) (g : B M A) l k :
Forall (λ x, y, y g x f y = x) l k mapM g l fmap f k = l.
Proof.
......
......@@ -102,7 +102,7 @@ Proof.
{ by rewrite (comm _ rP) -assoc big_opM_insert. }
exists (<[i:=rP]>rs); constructor; rewrite ?Hr; auto.
- intros j; rewrite Hr lookup_insert_is_Some=>-[?|[??]]; subst.
+ rewrite !lookup_op HiP !op_is_Some; set_solver +.
+ split. set_solver. rewrite !lookup_op HiP !op_is_Some; eauto.
+ destruct (HE j) as [Hj Hj']; auto; set_solver +Hj Hj'.
- intros j P'; rewrite Hr elem_of_union elem_of_singleton=>-[?|?]; subst.
+ rewrite !lookup_wld_op_l ?HiP; auto=> HP.
......@@ -162,7 +162,8 @@ Proof.
+ by rewrite lookup_op lookup_singleton_ne // left_id.
- by rewrite -assoc Hr /= left_id.
- intros j; rewrite -assoc Hr; destruct (decide (j = i)) as [->|].
+ rewrite /= !lookup_op lookup_singleton !op_is_Some; set_solver +Hi.
+ intros _; split; first set_solver +Hi.
rewrite /= !lookup_op lookup_singleton !op_is_Some; eauto.
+ rewrite lookup_insert_ne //.
rewrite lookup_op lookup_singleton_ne // left_id; eauto.
- intros j P'; rewrite -assoc Hr; destruct (decide (j=i)) as [->|].
......
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