Commit 30758ade by Ralf Jung

### introduce "fast_done", a tactic that *quickly* tries to solve the goal

parent 68b961a8
 ... ... @@ -6,14 +6,14 @@ Import uPred. Ltac wp_bind K := lazymatch eval hnf in K with | [] => idtac | _ => etrans; [|solve [ apply (wp_bind K) ]]; simpl | _ => etrans; [|fast_by apply (wp_bind K)]; simpl end. Ltac wp_finish := let rec go := match goal with | |- _ ⊑ ▷ _ => etrans; [|apply later_mono; go; reflexivity] | |- _ ⊑ ▷ _ => etrans; [|fast_by apply later_mono; go] | |- _ ⊑ wp _ _ _ => etrans; [|eapply wp_value_pvs; reflexivity]; etrans; [|eapply wp_value_pvs; fast_done]; (* sometimes, we will have to do a final view shift, so only apply pvs_intro if we obtain a consecutive wp *) try (eapply pvs_intro; ... ... @@ -31,7 +31,7 @@ Tactic Notation "wp_rec" ">" := (* hnf does not reduce through an of_val *) (* match eval hnf in e1 with Rec _ _ _ => *) wp_bind K; etrans; [|eapply wp_rec'; repeat rewrite /= to_of_val; reflexivity]; [|eapply wp_rec'; repeat rewrite /= to_of_val; fast_done]; simpl_subst; wp_finish (* end *) end) end). ... ... @@ -43,7 +43,7 @@ Tactic Notation "wp_lam" ">" := match eval hnf in e' with App ?e1 _ => (* match eval hnf in e1 with Rec BAnon _ _ => *) wp_bind K; etrans; [|eapply wp_lam; repeat (reflexivity || rewrite /= to_of_val)]; [|eapply wp_lam; repeat (fast_done || rewrite /= to_of_val)]; simpl_subst; wp_finish (* end *) end) end. ... ... @@ -62,9 +62,9 @@ Tactic Notation "wp_op" ">" := | BinOp LeOp _ _ => wp_bind K; apply wp_le; wp_finish | BinOp EqOp _ _ => wp_bind K; apply wp_eq; wp_finish | BinOp _ _ _ => wp_bind K; etrans; [|eapply wp_bin_op; reflexivity]; wp_finish wp_bind K; etrans; [|fast_by eapply wp_bin_op]; wp_finish | UnOp _ _ => wp_bind K; etrans; [|eapply wp_un_op; reflexivity]; wp_finish wp_bind K; etrans; [|fast_by eapply wp_un_op]; wp_finish end) end. Tactic Notation "wp_op" := wp_op>; try strip_later. ... ...
 ... ... @@ -265,7 +265,7 @@ Ltac set_unfold := [set_solver] already. We use the [naive_solver] tactic as a substitute. This tactic either fails or proves the goal. *) Tactic Notation "set_solver" "by" tactic3(tac) := try (reflexivity || eassumption); try fast_done; intros; setoid_subst; set_unfold; intros; setoid_subst; ... ...
 ... ... @@ -34,6 +34,13 @@ is rather efficient when having big hint databases, or expensive [Hint Extern] declarations as the ones above. *) Tactic Notation "intuition" := intuition auto. (* [done] can get slow as it calls "trivial". [fast_done] can solve way less goals, but it will also always finish quickly. *) Ltac fast_done := solve [ reflexivity | eassumption | symmetry; eassumption ]. Tactic Notation "fast_by" tactic(tac) := tac; fast_done. (** A slightly modified version of Ssreflect's finishing tactic [done]. It also performs [reflexivity] and uses symmetry of negated equalities. Compared to Ssreflect's [done], it does not compute the goal's [hnf] so as to avoid ... ... @@ -42,10 +49,9 @@ Coq's [easy] tactic as it does not perform [inversion]. *) Ltac done := trivial; intros; solve [ repeat first [ solve [trivial] [ fast_done | solve [trivial] | solve [symmetry; trivial] | eassumption | reflexivity | discriminate | contradiction | solve [apply not_symmetry; trivial] ... ... @@ -288,7 +294,7 @@ Ltac auto_proper := (* Normalize away equalities. *) simplify_eq; (* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *) try (f_equiv; assumption || (symmetry; assumption) || auto_proper). try (f_equiv; fast_done || auto_proper). (** solve_proper solves goals of the form "Proper (R1 ==> R2)", for any number of relations. All the actual work is done by f_equiv; ... ...
Supports Markdown
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