Commit edcdbc1d authored by Robbert Krebbers's avatar Robbert Krebbers

Try to start proofmode for all introduction tactics.

I also renamed `iProof` into `iStartProof`, as it is supposed to be
something internal, and not a substitute of Coq's `Proof` command (as
originally intended).
parent 47360b63
...@@ -77,6 +77,7 @@ Qed. ...@@ -77,6 +77,7 @@ Qed.
End heap. End heap.
Tactic Notation "wp_apply" open_constr(lem) := Tactic Notation "wp_apply" open_constr(lem) :=
iStartProof;
lazymatch goal with lazymatch goal with
| |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => | |- _ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
wp_bind_core K; iApply lem; try iNext) wp_bind_core K; iApply lem; try iNext)
...@@ -84,6 +85,7 @@ Tactic Notation "wp_apply" open_constr(lem) := ...@@ -84,6 +85,7 @@ Tactic Notation "wp_apply" open_constr(lem) :=
end. end.
Tactic Notation "wp_alloc" ident(l) "as" constr(H) := Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
iStartProof;
lazymatch goal with lazymatch goal with
| |- _ wp ?E ?e ?Q => | |- _ wp ?E ?e ?Q =>
first first
...@@ -105,6 +107,7 @@ Tactic Notation "wp_alloc" ident(l) := ...@@ -105,6 +107,7 @@ Tactic Notation "wp_alloc" ident(l) :=
let H := iFresh in wp_alloc l as H. let H := iFresh in wp_alloc l as H.
Tactic Notation "wp_load" := Tactic Notation "wp_load" :=
iStartProof;
lazymatch goal with lazymatch goal with
| |- _ wp ?E ?e ?Q => | |- _ wp ?E ?e ?Q =>
first first
...@@ -120,6 +123,7 @@ Tactic Notation "wp_load" := ...@@ -120,6 +123,7 @@ Tactic Notation "wp_load" :=
end. end.
Tactic Notation "wp_store" := Tactic Notation "wp_store" :=
iStartProof;
lazymatch goal with lazymatch goal with
| |- _ wp ?E ?e ?Q => | |- _ wp ?E ?e ?Q =>
first first
...@@ -138,6 +142,7 @@ Tactic Notation "wp_store" := ...@@ -138,6 +142,7 @@ Tactic Notation "wp_store" :=
end. end.
Tactic Notation "wp_cas_fail" := Tactic Notation "wp_cas_fail" :=
iStartProof;
lazymatch goal with lazymatch goal with
| |- _ wp ?E ?e ?Q => | |- _ wp ?E ?e ?Q =>
first first
...@@ -158,6 +163,7 @@ Tactic Notation "wp_cas_fail" := ...@@ -158,6 +163,7 @@ Tactic Notation "wp_cas_fail" :=
end. end.
Tactic Notation "wp_cas_suc" := Tactic Notation "wp_cas_suc" :=
iStartProof;
lazymatch goal with lazymatch goal with
| |- _ wp ?E ?e ?Q => | |- _ wp ?E ?e ?Q =>
first first
......
...@@ -42,16 +42,17 @@ Tactic Notation "iMatchHyp" tactic1(tac) := ...@@ -42,16 +42,17 @@ Tactic Notation "iMatchHyp" tactic1(tac) :=
end. end.
(** * Start a proof *) (** * Start a proof *)
Tactic Notation "iProof" := Ltac iStartProof :=
lazymatch goal with lazymatch goal with
| |- of_envs _ _ => fail "iProof: already in Iris proofmode" | |- of_envs _ _ => idtac
| |- ?P => | |- ?P =>
match eval hnf in P with lazymatch eval hnf in P with
(* need to use the unfolded version of [uPred_valid] due to the hnf *) (* need to use the unfolded version of [uPred_valid] due to the hnf *)
| True _ => apply tac_adequate | True _ => apply tac_adequate
| _ _ => apply uPred.wand_entails, tac_adequate | _ _ => apply uPred.wand_entails, tac_adequate
(* need to use the unfolded version of [⊣⊢] due to the hnf *) (* need to use the unfolded version of [⊣⊢] due to the hnf *)
| uPred_equiv' _ _ => apply uPred.iff_equiv, tac_adequate | uPred_equiv' _ _ => apply uPred.iff_equiv, tac_adequate
| _ => fail "iStartProof: not a uPred"
end end
end. end.
...@@ -389,6 +390,7 @@ Tactic Notation "iIntoValid" open_constr(t) := ...@@ -389,6 +390,7 @@ Tactic Notation "iIntoValid" open_constr(t) :=
Tactic Notation "iPoseProofCore" open_constr(lem) "as" constr(p) tactic(tac) := Tactic Notation "iPoseProofCore" open_constr(lem) "as" constr(p) tactic(tac) :=
let pose_trm t tac := let pose_trm t tac :=
let Htmp := iFresh in let Htmp := iFresh in
iStartProof;
lazymatch type of t with lazymatch type of t with
| string => | string =>
eapply tac_pose_proof_hyp with _ _ t _ Htmp _; eapply tac_pose_proof_hyp with _ _ t _ Htmp _;
...@@ -506,10 +508,12 @@ Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4) ...@@ -506,10 +508,12 @@ Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
(** * Disjunction *) (** * Disjunction *)
Tactic Notation "iLeft" := Tactic Notation "iLeft" :=
iStartProof;
eapply tac_or_l; eapply tac_or_l;
[let P := match goal with |- FromOr ?P _ _ => P end in [let P := match goal with |- FromOr ?P _ _ => P end in
apply _ || fail "iLeft:" P "not a disjunction"|]. apply _ || fail "iLeft:" P "not a disjunction"|].
Tactic Notation "iRight" := Tactic Notation "iRight" :=
iStartProof;
eapply tac_or_r; eapply tac_or_r;
[let P := match goal with |- FromOr ?P _ _ => P end in [let P := match goal with |- FromOr ?P _ _ => P end in
apply _ || fail "iRight:" P "not a disjunction"|]. apply _ || fail "iRight:" P "not a disjunction"|].
...@@ -524,7 +528,7 @@ Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) := ...@@ -524,7 +528,7 @@ Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
(** * Conjunction and separating conjunction *) (** * Conjunction and separating conjunction *)
Tactic Notation "iSplit" := Tactic Notation "iSplit" :=
try iProof; iStartProof;
lazymatch goal with lazymatch goal with
| |- _ _ => | |- _ _ =>
eapply tac_and_split; eapply tac_and_split;
...@@ -533,6 +537,7 @@ Tactic Notation "iSplit" := ...@@ -533,6 +537,7 @@ Tactic Notation "iSplit" :=
end. end.
Tactic Notation "iSplitL" constr(Hs) := Tactic Notation "iSplitL" constr(Hs) :=
iStartProof;
let Hs := words Hs in let Hs := words Hs in
eapply tac_sep_split with _ _ false Hs _ _; (* (js:=Hs) *) eapply tac_sep_split with _ _ false Hs _ _; (* (js:=Hs) *)
[let P := match goal with |- FromSep ?P _ _ => P end in [let P := match goal with |- FromSep ?P _ _ => P end in
...@@ -540,6 +545,7 @@ Tactic Notation "iSplitL" constr(Hs) := ...@@ -540,6 +545,7 @@ Tactic Notation "iSplitL" constr(Hs) :=
|env_cbv; reflexivity || fail "iSplitL: hypotheses" Hs |env_cbv; reflexivity || fail "iSplitL: hypotheses" Hs
"not found in the context"| |]. "not found in the context"| |].
Tactic Notation "iSplitR" constr(Hs) := Tactic Notation "iSplitR" constr(Hs) :=
iStartProof;
let Hs := words Hs in let Hs := words Hs in
eapply tac_sep_split with _ _ true Hs _ _; (* (js:=Hs) *) eapply tac_sep_split with _ _ true Hs _ _; (* (js:=Hs) *)
[let P := match goal with |- FromSep ?P _ _ => P end in [let P := match goal with |- FromSep ?P _ _ => P end in
...@@ -575,6 +581,7 @@ Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(H) := ...@@ -575,6 +581,7 @@ Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(H) :=
(** * Existential *) (** * Existential *)
Tactic Notation "iExists" uconstr(x1) := Tactic Notation "iExists" uconstr(x1) :=
iStartProof;
eapply tac_exist; eapply tac_exist;
[let P := match goal with |- FromExist ?P _ => P end in [let P := match goal with |- FromExist ?P _ => P end in
apply _ || fail "iExists:" P "not an existential" apply _ || fail "iExists:" P "not an existential"
...@@ -614,11 +621,13 @@ Local Tactic Notation "iExistDestruct" constr(H) ...@@ -614,11 +621,13 @@ Local Tactic Notation "iExistDestruct" constr(H)
(** * Always *) (** * Always *)
Tactic Notation "iAlways":= Tactic Notation "iAlways":=
iStartProof;
apply tac_always_intro; apply tac_always_intro;
[reflexivity || fail "iAlways: spatial context non-empty"|]. [reflexivity || fail "iAlways: spatial context non-empty"|].
(** * Later *) (** * Later *)
Tactic Notation "iNext" open_constr(n) := Tactic Notation "iNext" open_constr(n) :=
iStartProof;
let P := match goal with |- _ ?P => P end in let P := match goal with |- _ ?P => P end in
try lazymatch n with 0 => fail 1 "iNext: cannot strip 0 laters" end; try lazymatch n with 0 => fail 1 "iNext: cannot strip 0 laters" end;
eapply (tac_next _ _ n); eapply (tac_next _ _ n);
...@@ -632,6 +641,7 @@ Tactic Notation "iNext":= iNext _. ...@@ -632,6 +641,7 @@ Tactic Notation "iNext":= iNext _.
(** * Update modality *) (** * Update modality *)
Tactic Notation "iModIntro" := Tactic Notation "iModIntro" :=
iStartProof;
eapply tac_modal_intro; eapply tac_modal_intro;
[let P := match goal with |- IntoModal _ ?P => P end in [let P := match goal with |- IntoModal _ ?P => P end in
apply _ || fail "iModIntro:" P "not a modality"|]. apply _ || fail "iModIntro:" P "not a modality"|].
...@@ -775,11 +785,11 @@ Tactic Notation "iIntros" constr(pat) := ...@@ -775,11 +785,11 @@ Tactic Notation "iIntros" constr(pat) :=
| ?pat :: ?pats => | ?pat :: ?pats =>
let H := iFresh in iIntro H; iDestructHyp H as pat; go pats let H := iFresh in iIntro H; iDestructHyp H as pat; go pats
end end
in let pats := intro_pat.parse pat in try iProof; go pats. in let pats := intro_pat.parse pat in iStartProof; go pats.
Tactic Notation "iIntros" := iIntros [IAll]. Tactic Notation "iIntros" := iIntros [IAll].
Tactic Notation "iIntros" "(" simple_intropattern(x1) ")" := Tactic Notation "iIntros" "(" simple_intropattern(x1) ")" :=
try iProof; iIntro ( x1 ). try iStartProof; iIntro ( x1 ).
Tactic Notation "iIntros" "(" simple_intropattern(x1) Tactic Notation "iIntros" "(" simple_intropattern(x1)
simple_intropattern(x2) ")" := simple_intropattern(x2) ")" :=
iIntros ( x1 ); iIntro ( x2 ). iIntros ( x1 ); iIntro ( x2 ).
...@@ -908,7 +918,7 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) := ...@@ -908,7 +918,7 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
| 0 => fail "iDestruct: cannot introduce" n "hypotheses" | 0 => fail "iDestruct: cannot introduce" n "hypotheses"
| 1 => repeat iIntroForall; let H := iFresh in iIntro H; tac H | 1 => repeat iIntroForall; let H := iFresh in iIntro H; tac H
| S ?n' => repeat iIntroForall; let H := iFresh in iIntro H; go n' | S ?n' => repeat iIntroForall; let H := iFresh in iIntro H; go n'
end in intros; try iProof; go n in end in intros; iStartProof; go n in
lazymatch type of lem with lazymatch type of lem with
| nat => intro_destruct lem | nat => intro_destruct lem
| Z => (* to make it work in Z_scope. We should just be able to bind | Z => (* to make it work in Z_scope. We should just be able to bind
...@@ -1039,6 +1049,7 @@ Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH) ...@@ -1039,6 +1049,7 @@ Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
(** * Löb Induction *) (** * Löb Induction *)
Tactic Notation "iLöbCore" "as" constr (IH) := Tactic Notation "iLöbCore" "as" constr (IH) :=
iStartProof;
eapply tac_löb with _ IH; eapply tac_löb with _ IH;
[reflexivity || fail "iLöb: persistent context not empty" [reflexivity || fail "iLöb: persistent context not empty"
|env_cbv; reflexivity || fail "iLöb:" IH "not fresh"|]. |env_cbv; reflexivity || fail "iLöb:" IH "not fresh"|].
...@@ -1105,6 +1116,7 @@ Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2) ...@@ -1105,6 +1116,7 @@ Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
(** * Assert *) (** * Assert *)
Tactic Notation "iAssertCore" open_constr(Q) "with" constr(Hs) "as" tactic(tac) := Tactic Notation "iAssertCore" open_constr(Q) "with" constr(Hs) "as" tactic(tac) :=
iStartProof;
let H := iFresh in let H := iFresh in
let Hs := spec_pat.parse Hs in let Hs := spec_pat.parse Hs in
lazymatch Hs with lazymatch Hs with
......
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