Commit 25d8d958 authored by Robbert's avatar Robbert

Merge branch 'isimpl_many' into 'master'

Allow multiple arguments in `iEval .. in` and `iSimpl in`.

Closes #238

See merge request iris/iris!237
parents cdc564bf a7fe86a3
......@@ -152,16 +152,19 @@ Rewriting / simplification
equality in the proof mode goal / hypothesis `H`.
- `iRewrite -pm_trm` / `iRewrite -pm_trm in "H"` : rewrite in reverse direction
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)`.
- `iEval (tac)` / `iEval (tac) in "selpat"` : performs a tactic `tac`
on the proof mode goal / hypotheses given by the selection pattern
`selpat`. Using `%` as part of the selection pattern is unsupported.
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 / a hypothesis given by `selpat`. After
running `tac`, `?evar` is unified with the resulting `P`, which in
turn becomes the new proof mode goal / a hypothesis given by
`selpat`. Note that parentheses around `tac` are needed.
- `iSimpl` / `iSimpl in "selpat"` : performs `simpl` on the proof mode
goal / hypotheses given by the selection pattern `selpat`. This is a
shorthand for `iEval (simpl)`.
Iris
......
......@@ -101,6 +101,27 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
--------------------------------------∗
⌜S (S (S x)) = y⌝
1 subgoal
PROP : sbi
x, y, z : nat
============================
"H1" : ⌜S (S (S x)) = y⌝
"H2" : ⌜S y = z⌝
--------------------------------------∗
⌜S (S (S x)) = y⌝
1 subgoal
PROP : sbi
x, y, z : nat
============================
"H1" : ⌜S (S (S x)) = y⌝
--------------------------------------□
"H2" : ⌜(1 + y)%nat = z⌝
--------------------------------------∗
⌜S (S (S x)) = y⌝
"test_iFrame_later_1"
: string
1 subgoal
......
......@@ -473,6 +473,16 @@ Check "test_iSimpl_in".
Lemma test_iSimpl_in x y : (3 + x)%nat = y - S (S (S x)) = y : PROP.
Proof. iIntros "H". iSimpl in "H". Show. done. Qed.
Lemma test_iSimpl_in_2 x y z :
(3 + x)%nat = y - (1 + y)%nat = z -
S (S (S x)) = y : PROP.
Proof. iIntros "H1 H2". iSimpl in "H1 H2". Show. done. Qed.
Lemma test_iSimpl_in3 x y z :
(3 + x)%nat = y - (1 + y)%nat = z -
S (S (S x)) = y : PROP.
Proof. iIntros "#H1 H2". iSimpl in "#". Show. done. Qed.
Lemma test_iIntros_pure_neg : ( ¬False : PROP)%I.
Proof. by iIntros (?). Qed.
......
......@@ -107,32 +107,6 @@ Ltac iFresh :=
constr:(IAnon n)
end.
(** * Simplification *)
Tactic Notation "iEval" tactic(t) :=
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 _ _ _;
[pm_reflexivity || fail "iEval:" H "not found"
|let x := fresh in intros x; t; unfold x; reflexivity
|pm_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 with the current
Ltac, but it may be possible in Ltac2. *)
(** * Context manipulation *)
Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
eapply tac_rename with _ H1 H2 _ _; (* (i:=H1) (j:=H2) *)
......@@ -143,9 +117,12 @@ Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
let H2 := pretty_ident H2 in
fail "iRename:" H2 "not fresh"|].
(** Elaborated selection patterns, unlike the type [sel_pat], contains
only specific identifiers, and no wildcards like `#` (with the
exception of the pure selection pattern `%`) *)
Inductive esel_pat :=
| ESelPure
| ESelIdent : bool ident esel_pat.
| ESelIdent : (* whether the ident is intuitionistic *) bool ident esel_pat.
Local Ltac iElaborateSelPat_go pat Δ Hs :=
lazymatch pat with
......@@ -167,6 +144,8 @@ Local Ltac iElaborateSelPat_go pat Δ Hs :=
fail "iElaborateSelPat:" H "not found"
end
end.
(** Converts a selection pattern (given as a string) to a list of
elaborated selection patterns. *)
Ltac iElaborateSelPat pat :=
lazymatch goal with
| |- envs_entails ?Δ _ =>
......@@ -196,6 +175,39 @@ Tactic Notation "iClear" constr(Hs) :=
Tactic Notation "iClear" "(" ident_list(xs) ")" constr(Hs) :=
iClear Hs; clear xs.
(** ** Simplification *)
Tactic Notation "iEval" tactic(t) :=
iStartProof;
eapply tac_eval;
[let x := fresh in intros x; t; unfold x; reflexivity
|].
Local Ltac iEval_go t Hs :=
lazymatch Hs with
| [] => idtac
| ESelPure :: ?Hs => fail "iEval: %: unsupported selection pattern"
| ESelIdent _ ?H :: ?Hs =>
eapply tac_eval_in with _ H _ _ _;
[pm_reflexivity || let H := pretty_ident H in fail "iEval:" H "not found"
|let x := fresh in intros x; t; unfold x; reflexivity
|pm_reflexivity
|iEval_go t Hs]
end.
Tactic Notation "iEval" tactic(t) "in" constr(Hs) :=
iStartProof; let Hs := iElaborateSelPat Hs in iEval_go t Hs.
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 with the current
Ltac, but it may be possible in Ltac2. *)
(** * Assumptions *)
Tactic Notation "iExact" constr(H) :=
eapply tac_assumption with _ H _ _; (* (i:=H) *)
......
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