Commit 8d983adf authored by Ralf Jung's avatar Ralf Jung

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents ab9f921d 2ee38008
Pipeline #161 passed with stage
......@@ -146,19 +146,10 @@ Tactic Notation "ecancel" open_constr(Ps) :=
close Ps (@nil (uPred M)) ltac:(fun Qs => cancel Qs)
end.
(* Some more generic uPred tactics.
TODO: Naming. *)
Ltac revert_intros tac :=
lazymatch goal with
| |- _, _ => let H := fresh in intro H; revert_intros tac; revert H
| |- _ => tac
end.
(** Assumes a goal of the shape P ⊑ ▷ Q. Alterantively, if Q
is built of ★, ∧, ∨ with ▷ in all branches; that will work, too.
Will turn this goal into P ⊑ Q and strip ▷ in P below ★, ∧, ∨. *)
Ltac u_strip_later :=
Ltac strip_later :=
let rec strip :=
lazymatch goal with
| |- (_ _) _ =>
......@@ -190,23 +181,22 @@ Ltac u_strip_later :=
| |- _ _ => apply later_mono; reflexivity
(* We fail if we don't find laters in all branches. *)
end
in revert_intros ltac:(etrans; [|shape_Q];
in intros_revert ltac:(etrans; [|shape_Q];
etrans; last eapply later_mono; first solve [ strip ]).
(** Transforms a goal of the form ∀ ..., ?0... → ?1 ⊑ ?2
into True ⊑ ∀..., ■?0... → ?1 → ?2, applies tac, and
the moves all the assumptions back. *)
Ltac u_revert_all :=
(* TODO: this name may be a big too general *)
Ltac revert_all :=
lazymatch goal with
| |- _, _ => let H := fresh in intro H; u_revert_all;
| |- _, _ => let H := fresh in intro H; revert_all;
(* TODO: Really, we should distinguish based on whether this is a
dependent function type or not. Right now, we distinguish based
on the sort of the argument, which is suboptimal. *)
first [ apply (const_intro_impl _ _ _ H); clear H
| revert H; apply forall_elim']
| |- ?C _ => trans (True C)%I;
first (apply equiv_entails_sym, left_id, _; reflexivity);
apply impl_elim_l'
| |- ?C _ => apply impl_entails
end.
(** This starts on a goal of the form ∀ ..., ?0... → ?1 ⊑ ?2.
......@@ -215,8 +205,8 @@ Ltac u_revert_all :=
applies [tac] on the goal (now of the form _ ⊑ _), and then reverts the
Coq assumption so that we end up with the same shape as where we started,
but with an additional assumption ★-ed to the context *)
Ltac u_löb tac :=
u_revert_all;
Ltac löb tac :=
revert_all;
(* Add a box *)
etrans; last (eapply always_elim; reflexivity);
(* We now have a goal for the form True ⊑ P, with the "original" conclusion
......@@ -233,7 +223,7 @@ Ltac u_löb tac :=
| |- _ ( _ _) => apply impl_intro_l, const_elim_l;
let H := fresh in intro H; go; revert H
(* This is the "bottom" of the goal, where we see the impl introduced
by u_revert_all as well as the ▷ from löb_strong and the □ we added. *)
by uPred_revert_all as well as the ▷ from löb_strong and the □ we added. *)
| |- ?R (?L _) => apply impl_intro_l;
trans (L R)%I;
first (eapply equiv_entails, always_and_sep_r, _; reflexivity);
......
......@@ -79,7 +79,7 @@ Proof.
do 4 (rewrite big_sepS_insert; last set_solver).
rewrite !fn_lookup_insert fn_lookup_insert_ne // !fn_lookup_insert.
rewrite 3!assoc. apply sep_mono.
- rewrite saved_prop_agree. u_strip_later.
- rewrite saved_prop_agree. strip_later.
apply wand_intro_l. rewrite [(_ (_ - Π★{set _} _))%I]comm !assoc wand_elim_r.
rewrite (big_sepS_delete _ I i) //.
rewrite [(_ Π★{set _} _)%I]comm [(_ Π★{set _} _)%I]comm -!assoc.
......@@ -114,8 +114,7 @@ Proof.
rewrite [( _ _)%I]comm -!assoc. eapply wand_apply_l.
{ by rewrite <-later_wand, <-later_intro. }
{ by rewrite later_sep. }
u_strip_later.
apply: (eq_rewrite R Q (λ x, x)%I); eauto with I.
strip_later. apply: (eq_rewrite R Q (λ x, x)%I); eauto with I.
Qed.
(** Actual proofs *)
......@@ -179,7 +178,7 @@ Proof.
apply const_elim_sep_l=>Hs. destruct p; last done.
rewrite {1}/barrier_inv =>/={Hs}. rewrite later_sep.
eapply wp_store with (v' := '0); eauto with I ndisj.
u_strip_later. cancel [l '0]%I.
strip_later. cancel [l '0]%I.
apply wand_intro_l. rewrite -(exist_intro (State High I)).
rewrite -(exist_intro ). rewrite const_equiv /=; last by eauto using signal_step.
rewrite left_id -later_intro {2}/barrier_inv -!assoc. apply sep_mono_r.
......@@ -210,7 +209,7 @@ Proof.
apply const_elim_sep_l=>Hs.
rewrite {1}/barrier_inv =>/=. rewrite later_sep.
eapply wp_load; eauto with I ndisj.
rewrite -!assoc. apply sep_mono_r. u_strip_later.
rewrite -!assoc. apply sep_mono_r. strip_later.
apply wand_intro_l. destruct p.
{ (* a Low state. The comparison fails, and we recurse. *)
rewrite -(exist_intro (State Low I)) -(exist_intro {[ Change i ]}).
......@@ -240,8 +239,7 @@ Proof.
apply wand_intro_l. rewrite [(heap_ctx _ _)%I]sep_elim_r.
rewrite [(sts_own _ _ _ _)%I]sep_elim_r [(sts_ctx _ _ _ _)%I]sep_elim_r.
rewrite !assoc [(_ saved_prop_own i Q)%I]comm !assoc saved_prop_agree.
wp_op>; last done. intros _. u_strip_later.
wp_if.
wp_op; [|done]=> _. wp_if.
eapply wand_apply_r; [done..|]. eapply wand_apply_r; [done..|].
apply: (eq_rewrite Q' Q (λ x, x)%I); last by eauto with I.
rewrite eq_sym. eauto with I.
......
......@@ -12,7 +12,7 @@ Ltac wp_strip_later :=
| |- _ _ => apply later_intro
| |- _ _ => reflexivity
end
in revert_intros ltac:(first [ u_strip_later | etrans; [|go] ] ).
in intros_revert ltac:(first [ strip_later | etrans; [|go] ] ).
Ltac wp_bind K :=
lazymatch eval hnf in K with
| [] => idtac
......@@ -29,10 +29,10 @@ Ltac wp_finish :=
try (eapply pvs_intro;
match goal with |- _ wp _ _ _ => simpl | _ => fail end)
| _ => idtac
end in simpl; revert_intros go.
end in simpl; intros_revert go.
Tactic Notation "wp_rec" ">" :=
u_löb ltac:((* Find the redex and apply wp_rec *)
löb ltac:((* Find the redex and apply wp_rec *)
idtac; (* <https://coq.inria.fr/bugs/show_bug.cgi?id=4584> *)
lazymatch goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
......
......@@ -228,7 +228,6 @@ Ltac setoid_subst :=
| H : @equiv ?A ?e _ ?x |- _ => symmetry in H; setoid_subst_aux (@equiv A e) x
end.
(** f_equiv solves goals of the form "f _ = f _", for any relation and any
number of arguments, by looking for appropriate "Proper" instances.
If it cannot solve an equality, it will leave that to the user. *)
......@@ -306,6 +305,13 @@ Ltac solve_proper :=
end;
solve [ f_equiv ].
(** The tactic [intros_revert tac] introduces all foralls/arrows, performs tac,
and then reverts them. *)
Ltac intros_revert tac :=
lazymatch goal with
| |- _, _ => let H := fresh in intro H; intros_revert tac; revert H
| |- _ => tac
end.
(** Given a tactic [tac2] generating a list of terms, [iter tac1 tac2]
runs [tac x] for each element [x] until [tac x] succeeds. If it does not
......
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