Commit 94ab527c authored by Ralf Jung's avatar Ralf Jung
Browse files

add an omega auto database

parent a3d083c7
...@@ -100,7 +100,7 @@ Lemma wp_le_true E n1 n2 Q : ...@@ -100,7 +100,7 @@ Lemma wp_le_true E n1 n2 Q :
Q LitTrueV wp E (Le (LitNat n1) (LitNat n2)) Q. Q LitTrueV wp E (Le (LitNat n1) (LitNat n2)) Q.
Proof. Proof.
intros; rewrite -(wp_lift_pure_det_step (Le _ _) LitTrue None) ?right_id //; intros; rewrite -(wp_lift_pure_det_step (Le _ _) LitTrue None) ?right_id //;
last by intros; inv_step; eauto with lia. last by intros; inv_step; eauto with omega.
by rewrite -wp_value'. by rewrite -wp_value'.
Qed. Qed.
...@@ -109,7 +109,7 @@ Lemma wp_le_false E n1 n2 Q : ...@@ -109,7 +109,7 @@ Lemma wp_le_false E n1 n2 Q :
Q LitFalseV wp E (Le (LitNat n1) (LitNat n2)) Q. Q LitFalseV wp E (Le (LitNat n1) (LitNat n2)) Q.
Proof. Proof.
intros; rewrite -(wp_lift_pure_det_step (Le _ _) LitFalse None) ?right_id //; intros; rewrite -(wp_lift_pure_det_step (Le _ _) LitFalse None) ?right_id //;
last by intros; inv_step; eauto with lia. last by intros; inv_step; eauto with omega.
by rewrite -wp_value'. by rewrite -wp_value'.
Qed. Qed.
...@@ -155,7 +155,7 @@ Lemma wp_le E n1 n2 P Q : ...@@ -155,7 +155,7 @@ Lemma wp_le E n1 n2 P Q :
Proof. Proof.
intros; destruct (decide (n1 n2)). intros; destruct (decide (n1 n2)).
* rewrite -wp_le_true; auto. * rewrite -wp_le_true; auto.
* rewrite -wp_le_false; auto with lia. * rewrite -wp_le_false; auto with omega.
Qed. Qed.
End lifting. End lifting.
...@@ -90,7 +90,7 @@ Module LiftingTests. ...@@ -90,7 +90,7 @@ Module LiftingTests.
* rewrite -wp_case_inr //. * rewrite -wp_case_inr //.
rewrite -!later_intro -wp_value' //. rewrite -!later_intro -wp_value' //.
rewrite and_elim_r. apply const_elim_l=>Hle. rewrite and_elim_r. apply const_elim_l=>Hle.
by replace n1 with (pred n2) by lia. by replace n1 with (pred n2) by omega.
Qed. Qed.
Lemma Pred_spec n E Q : Lemma Pred_spec n E Q :
...@@ -101,10 +101,10 @@ Module LiftingTests. ...@@ -101,10 +101,10 @@ Module LiftingTests.
apply later_mono, wp_le=> Hn. apply later_mono, wp_le=> Hn.
- rewrite -wp_case_inl //. - rewrite -wp_case_inl //.
rewrite -!later_intro -wp_value' //. rewrite -!later_intro -wp_value' //.
by replace n with 0 by lia. by replace n with 0 by omega.
- rewrite -wp_case_inr //. - rewrite -wp_case_inr //.
rewrite -!later_intro -FindPred_spec. rewrite -!later_intro -FindPred_spec.
auto using and_intro, const_intro with lia. auto using and_intro, const_intro with omega.
Qed. Qed.
Goal E, Goal E,
......
...@@ -2,6 +2,7 @@ ...@@ -2,6 +2,7 @@
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
(** This file collects general purpose tactics that are used throughout (** This file collects general purpose tactics that are used throughout
the development. *) the development. *)
Require Import Omega.
Require Export Psatz. Require Export Psatz.
Require Export prelude.base. Require Export prelude.base.
...@@ -24,6 +25,7 @@ to be combined in combination with other hint database. *) ...@@ -24,6 +25,7 @@ to be combined in combination with other hint database. *)
Hint Extern 998 (_ = _) => f_equal : f_equal. Hint Extern 998 (_ = _) => f_equal : f_equal.
Hint Extern 999 => congruence : congruence. Hint Extern 999 => congruence : congruence.
Hint Extern 1000 => lia : lia. Hint Extern 1000 => lia : lia.
Hint Extern 1000 => omega : omega.
(** The tactic [intuition] expands to [intuition auto with *] by default. This (** The tactic [intuition] expands to [intuition auto with *] by default. This
is rather efficient when having big hint databases, or expensive [Hint Extern] is rather efficient when having big hint databases, or expensive [Hint Extern]
......
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