Commit 47598d44 authored by Robbert Krebbers's avatar Robbert Krebbers

Block simpl for of_val to avoid too much unfolding.

parent 0efe3294
......@@ -8,6 +8,7 @@ Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
in case [e] does not contain the free variable [x] it will return [e] in a
way that is syntactically equal (i.e. without any Coq-level delta reduction
performed) *)
Arguments of_val : simpl never.
Definition gsubst_lift {A B C} (f : A B C)
(x : A) (y : B) (mx : option A) (my : option B) : option C :=
match mx, my with
......
......@@ -92,15 +92,14 @@ Module LiftingTests.
rewrite -(wp_bindi (IfCtx _ _)) /=.
apply later_mono, wp_le=> Hn.
- rewrite -wp_if_true.
rewrite -(wp_bindi (UnOpCtx _)).
rewrite -(wp_bind [AppLCtx _; AppRCtx FindPred]).
rewrite -(wp_bindi (BinOpLCtx _ _)).
rewrite -(wp_bindi (UnOpCtx _)) /=.
rewrite -(wp_bind [AppLCtx _; AppRCtx _]) /=.
rewrite -(wp_bindi (BinOpLCtx _ _)) /=.
rewrite -wp_un_op //=.
rewrite -wp_bin_op //= -!later_intro.
rewrite -FindPred_spec. apply and_intro; first by (apply const_intro; omega).
rewrite -wp_un_op //= -later_intro.
assert (n - 1 = - (- n + 2 - 1)) as EQ by omega.
by rewrite EQ.
by assert (n - 1 = - (- n + 2 - 1)) as -> by omega.
- rewrite -wp_if_false.
rewrite -!later_intro -FindPred_spec.
auto using and_intro, const_intro with omega.
......@@ -112,6 +111,6 @@ Module LiftingTests.
Proof.
intros E.
rewrite -(wp_bindi (LetCtx _ _)) -Pred_spec //= -wp_let //=.
rewrite -Pred_spec -!later_intro /=. by apply const_intro.
by rewrite -Pred_spec -!later_intro /=.
Qed.
End LiftingTests.
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