Commit b5ce30bf authored by Robbert Krebbers's avatar Robbert Krebbers

Merge commit '59fbe96b' into gen_proofmode

parents 307d0084 59fbe96b
......@@ -5,6 +5,10 @@ Coq development, but not every API-breaking change is listed. Changes marked
## Iris master
Changes in and extensions of the theory:
* [#] Weakestpre for total program correctness.
Changes in Coq:
* Rename `timelessP` -> `timeless` (projection of the `Timeless` class)
......
......@@ -150,11 +150,22 @@ Induction
variables `x1 ... xn`, the hypotheses given by the selection pattern `selpat`,
and the spatial context.
Rewriting
---------
Rewriting / simplification
--------------------------
- `iRewrite pm_trm` / `iRewrite pm_trm in "H"` : rewrite using an internal
equality in the proof mode goal / hypothesis `H`.
- `iEval (tac)` / `iEval (tac) in H` : performs a tactic `tac` on the proof mode
goal / hypothesis `H`. The tactic `tac` should be a reduction or rewriting
tactic like `simpl`, `cbv`, `lazy`, `rewrite` or `setoid_rewrite`. The `iEval`
tactic is implemented by running `tac` on `?evar ⊢ P` / `P ⊢ ?evar` where `P`
is the proof goal / hypothesis `H`. After running `tac`, `?evar` is unified
with the resulting `P`, which in turn becomes the new proof mode goal /
hypothesis `H`.
Note that parentheses around `tac` are needed.
- `iSimpl` / `iSimpl in H` : performs `simpl` on the proof mode goal /
hypothesis `H`. This is a shorthand for `iEval (simpl)`.
- `iRewrite pm_trm` : rewrite an equality in the conclusion.
- `iRewrite pm_trm in "H"` : rewrite an equality in the hypothesis `H`.
Iris
----
......
......@@ -208,7 +208,7 @@ Lemma box_fill E f P :
Proof.
iIntros (?) "H HP"; iDestruct "H" as (Φ) "[#HeqP Hf]".
iExists Φ; iSplitR; first by rewrite big_opM_fmap.
rewrite internal_eq_iff later_iff big_sepM_later.
iEval (rewrite internal_eq_iff later_iff big_sepM_later) in "HeqP".
iDestruct ("HeqP" with "HP") as "HP".
iCombine "Hf" "HP" as "Hf".
rewrite -big_opM_opM big_opM_fmap; iApply (fupd_big_sepM _ _ f).
......
......@@ -6,18 +6,19 @@ Set Default Proof Using "Type".
Import uPred.
Lemma tac_wp_expr_eval `{heapG Σ} Δ s E Φ e e' :
e = e'
( (e'':=e'), e = e'')
envs_entails Δ (WP e' @ s; E {{ Φ }}) envs_entails Δ (WP e @ s; E {{ Φ }}).
Proof. by intros ->. Qed.
Lemma tac_twp_expr_eval `{heapG Σ} Δ s E Φ e e' :
e = e'
( (e'':=e'), e = e'')
envs_entails Δ (WP e' @ s; E [{ Φ }]) envs_entails Δ (WP e @ s; E [{ Φ }]).
Proof. by intros ->. Qed.
Tactic Notation "wp_expr_eval" tactic(t) :=
iStartProof;
try (first [eapply tac_wp_expr_eval|eapply tac_twp_expr_eval];
[t; reflexivity|]).
[let x := fresh in intros x; t; unfold x; reflexivity
|]).
Ltac wp_expr_simpl := wp_expr_eval simpl.
Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.
......
......@@ -128,7 +128,7 @@ Lemma wptp_result s n e1 t1 v2 t2 σ1 σ2 φ :
Proof.
intros. rewrite wptp_steps // laterN_later. apply: bupd_iter_laterN_mono.
iDestruct 1 as (e2 t2' ?) "((Hw & HE & _) & H & _)"; simplify_eq.
iDestruct (wp_value_inv with "H") as "H". rewrite uPred_fupd_eq.
iDestruct (wp_value_inv' with "H") as "H". rewrite uPred_fupd_eq.
iMod ("H" with "[Hw HE]") as ">(_ & _ & $)"; iFrame; auto.
Qed.
......
......@@ -222,7 +222,7 @@ Qed.
Lemma twp_value' s E Φ v : Φ v - WP of_val v @ s; E [{ Φ }].
Proof. iIntros "HΦ". rewrite twp_unfold /twp_pre to_of_val. auto. Qed.
Lemma twp_value_inv s E Φ v : WP of_val v @ s; E [{ Φ }] ={E}= Φ v.
Lemma twp_value_inv' s E Φ v : WP of_val v @ s; E [{ Φ }] ={E}= Φ v.
Proof. by rewrite twp_unfold /twp_pre to_of_val. Qed.
Lemma twp_strong_mono s1 s2 E1 E2 e Φ Ψ :
......@@ -267,7 +267,7 @@ Proof.
+ iMod ("H" with "[$]") as "[H _]". iDestruct "H" as %(? & ? & ? & ?).
by edestruct (atomic _ _ _ _ Hstep).
- destruct (atomic _ _ _ _ Hstep) as [v <-%of_to_val].
iMod (twp_value_inv with "H") as ">H". iFrame "Hphy". by iApply twp_value'.
iMod (twp_value_inv' with "H") as ">H". iFrame "Hphy". by iApply twp_value'.
Qed.
Lemma twp_bind K `{!LanguageCtx K} s E e Φ :
......@@ -348,6 +348,8 @@ Lemma twp_value_fupd' s E Φ v : (|={E}=> Φ v) -∗ WP of_val v @ s; E [{ Φ }]
Proof. intros. by rewrite -twp_fupd -twp_value'. Qed.
Lemma twp_value_fupd s E Φ e v `{!IntoVal e v} : (|={E}=> Φ v) - WP e @ s; E [{ Φ }].
Proof. intros. rewrite -twp_fupd -twp_value //. Qed.
Lemma twp_value_inv s E Φ e v `{!IntoVal e v} : WP e @ s; E [{ Φ }] ={E}= Φ v.
Proof. intros; rewrite -(of_to_val e v) //; by apply twp_value_inv'. Qed.
Lemma twp_frame_l s E e Φ R : R WP e @ s; E [{ Φ }] - WP e @ s; E [{ v, R Φ v }].
Proof. iIntros "[? H]". iApply (twp_strong_mono with "H"); auto with iFrame. Qed.
......
......@@ -207,7 +207,7 @@ Qed.
Lemma wp_value' s E Φ v : Φ v WP of_val v @ s; E {{ Φ }}.
Proof. iIntros "HΦ". rewrite wp_unfold /wp_pre to_of_val. auto. Qed.
Lemma wp_value_inv s E Φ v : WP of_val v @ s; E {{ Φ }} ={E}= Φ v.
Lemma wp_value_inv' s E Φ v : WP of_val v @ s; E {{ Φ }} ={E}= Φ v.
Proof. by rewrite wp_unfold /wp_pre to_of_val. Qed.
Lemma wp_strong_mono s1 s2 E1 E2 e Φ Ψ :
......@@ -251,7 +251,7 @@ Proof.
+ iMod ("H" with "[$]") as "[H _]". iDestruct "H" as %(? & ? & ? & ?).
by edestruct (atomic _ _ _ _ Hstep).
- destruct (atomic _ _ _ _ Hstep) as [v <-%of_to_val].
iMod (wp_value_inv with "H") as ">H". iFrame "Hphy". by iApply wp_value'.
iMod (wp_value_inv' with "H") as ">H". iFrame "Hphy". by iApply wp_value'.
Qed.
Lemma wp_step_fupd s E1 E2 e P Φ :
......@@ -321,6 +321,8 @@ Proof. intros. by rewrite -wp_fupd -wp_value'. Qed.
Lemma wp_value_fupd s E Φ e v `{!IntoVal e v} :
(|={E}=> Φ v) WP e @ s; E {{ Φ }}.
Proof. intros. rewrite -wp_fupd -wp_value //. Qed.
Lemma wp_value_inv s E Φ e v `{!IntoVal e v} : WP e @ s; E {{ Φ }} ={E}= Φ v.
Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value_inv'. Qed.
Lemma wp_frame_l s E e Φ R : R WP e @ s; E {{ Φ }} WP e @ s; E {{ v, R Φ v }}.
Proof. iIntros "[? H]". iApply (wp_strong_mono with "H"); auto with iFrame. Qed.
......
......@@ -460,9 +460,22 @@ Qed.
(** * Basic rules *)
Lemma tac_eval Δ Q Q' :
Q = Q'
( (Q'':=Q'), Q'' Q) (* We introduce [Q''] as a let binding so that
tactics like `reflexivity` as called by [rewrite //] do not eagerly unify
it with [Q]. See [test_iEval] in [tests/proofmode]. *)
envs_entails Δ Q' envs_entails Δ Q.
Proof. by intros ->. Qed.
Proof. by intros <-. Qed.
Lemma tac_eval_in Δ Δ' i p P P' Q :
envs_lookup i Δ = Some (p, P)
( (P'':=P'), P P')
envs_simple_replace i p (Esnoc Enil i P') Δ = Some Δ'
envs_entails Δ' Q envs_entails Δ Q.
Proof.
rewrite envs_entails_eq /=. intros ? HP ? <-.
rewrite envs_simple_replace_singleton_sound //; simpl.
by rewrite HP wand_elim_r.
Qed.
Class AffineEnv (Γ : env PROP) := affine_env : Forall Affine Γ.
Global Instance affine_env_nil : AffineEnv Enil.
......
......@@ -87,9 +87,29 @@ Tactic Notation "iStartProof" uconstr(PROP) :=
(** * Simplification *)
Tactic Notation "iEval" tactic(t) :=
iStartProof; try (eapply tac_eval; [t; reflexivity|]).
iStartProof;
eapply tac_eval;
[let x := fresh in intros x; t; unfold x; reflexivity
|].
Tactic Notation "iEval" tactic(t) "in" constr(H) :=
iStartProof;
eapply tac_eval_in with _ H _ _ _;
[env_reflexivity || fail "iEval:" H "not found"
|let x := fresh in intros x; t; unfold x; reflexivity
|env_reflexivity
|].
Tactic Notation "iSimpl" := iEval simpl.
Tactic Notation "iSimpl" "in" constr(H) := iEval simpl in H.
(* It would be nice to also have an `iSsrRewrite`, however, for this we need to
pass arguments to Ssreflect's `rewrite` like `/= foo /bar` in Ltac, see:
https://sympa.inria.fr/sympa/arc/coq-club/2018-01/msg00000.html
PMP told me (= Robbert) in person that this is not possible today, but may be
possible in Ltac2. *)
(** * Context manipulation *)
Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
......
......@@ -314,4 +314,10 @@ Lemma test_assert_pure (φ : Prop) P :
φ P P ⌜φ⌝.
Proof. iIntros (Hφ). iAssert ⌜φ⌝%I with "[%]" as "$"; auto. Qed.
Lemma test_iEval x y : (y + x)%nat = 1 - S (x + y) = 2%nat : PROP.
Proof.
iIntros (H).
iEval (rewrite (Nat.add_comm x y) // H).
done.
Qed.
End tests.
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