Skip to content

GitLab

Commit 8cea92ec authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'ci/joe/compact_ipm_simple' into 'master' 

Simple changes to make proof mode terms more compact

See merge request iris/iris!248
parents c9984c7f ded831d3
Expand all Hide whitespace changes
Inline Side-by-side
tests/proofmode.ref
View file @ 8cea92ec
......@@ -456,7 +456,7 @@ The command has indeed failed with message:
In nested Ltac calls to "iIntros ( (intropattern) )",
"iIntro ( (intropattern) )" and "intros x", last call failed.
x is already used.
"iSplit_one_of_many"
"iSplitL_one_of_many"
: string
The command has indeed failed with message:
Ltac call to "iSplitL (constr)" failed.
......@@ -464,6 +464,39 @@ Tactic failure: iSplitL: hypotheses ["HPx"] not found.
The command has indeed failed with message:
Ltac call to "iSplitL (constr)" failed.
Tactic failure: iSplitL: hypotheses ["HPx"] not found.
"iSplitR_one_of_many"
: string
The command has indeed failed with message:
Ltac call to "iSplitR (constr)" failed.
Tactic failure: iSplitR: hypotheses ["HPx"] not found.
The command has indeed failed with message:
Ltac call to "iSplitR (constr)" failed.
Tactic failure: iSplitR: hypotheses ["HPx"] not found.
"iCombine_fail"
: string
The command has indeed failed with message:
Ltac call to "iCombine (constr) as (constr)" failed.
Tactic failure: iCombine: hypotheses ["HP3"] not found.
"iSpecialize_bad_name1_fail"
: string
The command has indeed failed with message:
In nested Ltac calls to "iSpecialize (open_constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
failed.
Tactic failure: iSpecialize: "H" not found.
"iSpecialize_bad_name2_fail"
: string
The command has indeed failed with message:
In nested Ltac calls to "iSpecialize (open_constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
failed.
Tactic failure: iSpecialize: "H" not found.
"iExact_fail"
: string
The command has indeed failed with message:
......@@ -519,12 +552,30 @@ In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
"iPoseProofCoreLem (constr) as (constr) before_tc (tactic)",
"tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]),
"tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]),
"tac" (bound to fun H => iDestructHyp H as pat),
"iDestructHyp (constr) as (constr)",
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>",
"<iris.proofmode.ltac_tactics.iDestructHypGo>" and
"iRename (constr) into (constr)", last call failed.
Tactic failure: iRename: "H" not fresh.
"iPoseProof_not_found_fail"
: string
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)" and
"iPoseProofCoreHyp (constr) as (constr)", last call failed.
Tactic failure: iPoseProof: "Hx" not found.
"iPoseProofCoreHyp_not_found_fail"
: string
The command has indeed failed with message:
Ltac call to "iPoseProofCoreHyp (constr) as (constr)" failed.
Tactic failure: iPoseProof: "Hx" not found.
"iPoseProofCoreHyp_not_fresh_fail"
: string
The command has indeed failed with message:
Ltac call to "iPoseProofCoreHyp (constr) as (constr)" failed.
Tactic failure: iPoseProof: "H1" not fresh.
"iRevert_fail"
: string
The command has indeed failed with message:
......@@ -555,6 +606,14 @@ In nested Ltac calls to "iDestruct (open_constr) as (constr)",
"<iris.proofmode.ltac_tactics.iDestructHypGo>", last call failed.
Tactic failure: iDestruct: (IList [[IClear (sel_patterns.SelIdent "HP")]])
invalid.
"iOrDestruct_fail"
: string
The command has indeed failed with message:
Ltac call to "iOrDestruct (constr) as (constr) (constr)" failed.
Tactic failure: iOrDestruct: "H'" or "H2" not fresh.
The command has indeed failed with message:
Ltac call to "iOrDestruct (constr) as (constr) (constr)" failed.
Tactic failure: iOrDestruct: "H1" or "H'" not fresh.
"iApply_fail"
: string
The command has indeed failed with message:
......
tests/proofmode.v
View file @ 8cea92ec
......@@ -777,13 +777,41 @@ Proof.
iIntros "HQ" (x). Fail iIntros (x).
Abort.
Check "iSplit_one_of_many".
Lemma iSplit_one_of_many P :
Check "iSplitL_one_of_many".
Lemma iSplitL_one_of_many P :
P -∗ P -∗ P ∗ P.
Proof.
iIntros "HP1 HP2". Fail iSplitL "HP1 HPx". Fail iSplitL "HPx HP1".
Abort.
Check "iSplitR_one_of_many".
Lemma iSplitR_one_of_many P :
P -∗ P -∗ P ∗ P.
Proof.
iIntros "HP1 HP2". Fail iSplitR "HP1 HPx". Fail iSplitR "HPx HP1".
Abort.
Check "iCombine_fail".
Lemma iCombine_fail P:
P -∗ P -∗ P ∗ P.
Proof.
iIntros "HP1 HP2". Fail iCombine "HP1 HP3" as "HP".
Abort.
Check "iSpecialize_bad_name1_fail".
Lemma iSpecialize_bad_name1_fail P Q:
(P -∗ Q) -∗ P -∗ Q.
Proof.
iIntros "HW HP". Fail iSpecialize ("H" with "HP").
Abort.
Check "iSpecialize_bad_name2_fail".
Lemma iSpecialize_bad_name2_fail P Q:
(P -∗ Q) -∗ P -∗ Q.
Proof.
iIntros "HW HP". Fail iSpecialize ("HW" with "H").
Abort.
Check "iExact_fail".
Lemma iExact_fail P Q :
<affine> P -∗ Q -∗ <affine> P.
......@@ -811,6 +839,24 @@ Proof.
iIntros "H". Fail iPoseProof bi.and_intro as "H".
Abort.
Check "iPoseProof_not_found_fail".
Lemma iPoseProof_not_found_fail P : P -∗ P.
Proof.
iIntros "H". Fail iPoseProof "Hx" as "H1".
Abort.
Check "iPoseProofCoreHyp_not_found_fail".
Lemma iPoseProofCoreHyp_not_found_fail P : P -∗ P -∗ P.
Proof.
iIntros "H". Fail iPoseProofCoreHyp "Hx" as "H1".
Abort.
Check "iPoseProofCoreHyp_not_fresh_fail".
Lemma iPoseProofCoreHyp_not_fresh_fail P : P -∗ P -∗ P.
Proof.
iIntros "H0 H1". Fail iPoseProofCoreHyp "H0" as "H1".
Abort.
Check "iRevert_fail".
Lemma iRevert_fail P : P -∗ P.
Proof. Fail iRevert "H". Abort.
......@@ -819,6 +865,12 @@ Check "iDestruct_fail".
Lemma iDestruct_fail P : P -∗ <absorb> P.
Proof. iIntros "HP". Fail iDestruct "HP" as "{HP}". Fail iDestruct "HP" as "[{HP}]". Abort.
Check "iOrDestruct_fail".
Lemma iOrDestruct_fail P : (P ∨ P) -∗ P -∗ P.
Proof.
iIntros "H H'". Fail iOrDestruct "H" as "H'" "H2". Fail iOrDestruct "H" as "H1" "H'".
Abort.
Check "iApply_fail".
Lemma iApply_fail P Q : P -∗ Q.
Proof. iIntros "HP". Fail iApply "HP". Abort.
......
theories/proofmode/coq_tactics.v
View file @ 8cea92ec
This diff is collapsed.
theories/proofmode/ltac_tactics.v
View file @ 8cea92ec
......@@ -39,15 +39,20 @@ Ltac pretty_ident H :=
(** * Misc *)
Ltac iMissingHyps Hs :=
let Δ :=
lazymatch goal with
| |- envs_entails ?Δ _ => Δ
| |- context[ envs_split _ _ ?Δ ] => Δ
end in
Ltac iGetCtx :=
lazymatch goal with
| |- envs_entails ?Δ _ => Δ
| |- context[ envs_split _ _ ?Δ ] => Δ
end.
Ltac iMissingHypsCore Δ Hs :=
let Hhyps := pm_eval (envs_dom Δ) in
eval vm_compute in (list_difference Hs Hhyps).
Ltac iMissingHyps Hs :=
let Δ := iGetCtx in
iMissingHypsCore Δ Hs.
Ltac iTypeOf H :=
let Δ := match goal with |- envs_entails ?Δ _ => Δ end in
pm_eval (envs_lookup H Δ).
......@@ -119,13 +124,17 @@ Ltac iFresh :=
(** * Context manipulation *)
Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
eapply tac_rename with _ H1 H2 _ _; (* (i:=H1) (j:=H2) *)
eapply tac_rename with H1 H2 _ _; (* (i:=H1) (j:=H2) *)
[pm_reflexivity ||
let H1 := pretty_ident H1 in
fail "iRename:" H1 "not found"
|pm_reflexivity ||
let H2 := pretty_ident H2 in
fail "iRename:" H2 "not fresh"|].
|pm_reduce;
lazymatch goal with
| |- False =>
let H2 := pretty_ident H2 in
fail "iRename:" H2 "not fresh"
| _ => idtac (* subgoal *)
end].
(** Elaborated selection patterns, unlike the type [sel_pat], contains
only specific identifiers, and no wildcards like `#` (with the
......@@ -197,11 +206,10 @@ Local Ltac iEval_go t Hs :=
| [] => idtac
| ESelPure :: ?Hs => fail "iEval: %: unsupported selection pattern"
| ESelIdent _ ?H :: ?Hs =>
eapply tac_eval_in with _ H _ _ _;
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]
|pm_reduce; iEval_go t Hs]
end.
Tactic Notation "iEval" tactic(t) "in" constr(Hs) :=
......@@ -276,7 +284,7 @@ Tactic Notation "iExFalso" := apply tac_ex_falso.
(** * Making hypotheses intuitionistic or pure *)
Local Tactic Notation "iIntuitionistic" constr(H) :=
eapply tac_intuitionistic with _ H _ _ _; (* (i:=H) *)
eapply tac_intuitionistic with H _ _ _; (* (i:=H) *)
[pm_reflexivity ||
let H := pretty_ident H in
fail "iIntuitionistic:" H "not found"
......@@ -286,7 +294,7 @@ Local Tactic Notation "iIntuitionistic" constr(H) :=
|pm_reduce; iSolveTC ||
let P := match goal with |- TCOr (Affine ?P) _ => P end in
fail "iIntuitionistic:" P "not affine and the goal not absorbing"
|pm_reflexivity|].
|pm_reduce].
Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
eapply tac_pure with _ H _ _ _; (* (i:=H1) *)
......@@ -448,41 +456,51 @@ Local Tactic Notation "iIntro" constr(H) :=
iStartProof;
first
[(* (?Q → _) *)
eapply tac_impl_intro with _ H _ _ _; (* (i:=H) *)
eapply tac_impl_intro with H _ _ _; (* (i:=H) *)
[iSolveTC
|pm_reduce; iSolveTC ||
let P := lazymatch goal with |- Persistent ?P => P end in
fail 1 "iIntro: introducing non-persistent" H ":" P
"into non-empty spatial context"
|pm_reflexivity ||
let H := pretty_ident H in
fail 1 "iIntro:" H "not fresh"
|iSolveTC
|(* subgoal *)]
|pm_reduce;
let H := pretty_ident H in
lazymatch goal with
| |- False =>
let H := pretty_ident H in
fail 1 "iIntro:" H "not fresh"
| _ => idtac (* subgoal *)
end]
|(* (_ -∗ _) *)
eapply tac_wand_intro with _ H _ _; (* (i:=H) *)
eapply tac_wand_intro with H _ _; (* (i:=H) *)
[iSolveTC
| pm_reflexivity ||
let H := pretty_ident H in
fail 1 "iIntro:" H "not fresh"
|(* subgoal *)]
| pm_reduce;
lazymatch goal with
| |- False =>
let H := pretty_ident H in
fail 1 "iIntro:" H "not fresh"
| _ => idtac (* subgoal *)
end]
| fail 1 "iIntro: nothing to introduce" ].
Local Tactic Notation "iIntro" "#" constr(H) :=
iStartProof;
first
[(* (?P → _) *)
eapply tac_impl_intro_intuitionistic with _ H _ _ _; (* (i:=H) *)
eapply tac_impl_intro_intuitionistic with H _ _ _; (* (i:=H) *)
[iSolveTC
|iSolveTC ||
let P := match goal with |- IntoPersistent _ ?P _ => P end in
fail 1 "iIntro:" P "not persistent"
|pm_reflexivity ||
let H := pretty_ident H in
fail 1 "iIntro:" H "not fresh"
|(* subgoal *)]
|pm_reduce;
lazymatch goal with
| |- False =>
let H := pretty_ident H in
fail 1 "iIntro:" H "not fresh"
| _ => idtac (* subgoal *)
end]
|(* (?P -∗ _) *)
eapply tac_wand_intro_intuitionistic with _ H _ _ _; (* (i:=H) *)
eapply tac_wand_intro_intuitionistic with H _ _ _; (* (i:=H) *)
[iSolveTC
|iSolveTC ||
let P := match goal with |- IntoPersistent _ ?P _ => P end in
......@@ -490,10 +508,13 @@ Local Tactic Notation "iIntro" "#" constr(H) :=
|iSolveTC ||
let P := match goal with |- TCOr (Affine ?P) _ => P end in
fail 1 "iIntro:" P "not affine and the goal not absorbing"
|pm_reflexivity ||
let H := pretty_ident H in
fail 1 "iIntro:" H "not fresh"
|(* subgoal *)]
|pm_reduce;
lazymatch goal with
| |- False =>
let H := pretty_ident H in
fail 1 "iIntro:" H "not fresh"
| _ => idtac (* subgoal *)
end]
|fail 1 "iIntro: nothing to introduce"].
Local Tactic Notation "iIntro" constr(H) "as" constr(p) :=
......@@ -686,23 +707,34 @@ Local Ltac iIntoEmpValid t :=
|exact t]].
Tactic Notation "iPoseProofCoreHyp" constr(H) "as" constr(Hnew) :=
eapply tac_pose_proof_hyp with _ _ H _ Hnew _;
[pm_reflexivity ||
let H := pretty_ident H in
fail "iPoseProof:" H "not found"
|pm_reflexivity ||
let Htmp := pretty_ident Hnew in
fail "iPoseProof:" Hnew "not fresh"
|].
let Δ := iGetCtx in
eapply tac_pose_proof_hyp with H Hnew;
pm_reduce;
lazymatch goal with
| |- False =>
let lookup := pm_eval (envs_lookup_delete false H Δ) in
lazymatch lookup with
| None =>
let H := pretty_ident H in
fail "iPoseProof:" H "not found"
| _ =>
let Hnew := pretty_ident Hnew in
fail "iPoseProof:" Hnew "not fresh"
end
| _ => idtac
end.
Tactic Notation "iPoseProofCoreLem"
constr(lem) "as" constr(Hnew) "before_tc" tactic(tac) :=
eapply tac_pose_proof with _ Hnew _; (* (j:=H) *)
eapply tac_pose_proof with Hnew _; (* (j:=H) *)
[iIntoEmpValid lem
|pm_reflexivity ||
let Htmp := pretty_ident Hnew in
fail "iPoseProof:" Hnew "not fresh"
|tac];
|pm_reduce;
lazymatch goal with
| |- False =>
let Hnew := pretty_ident Hnew in
fail "iPoseProof:" Hnew "not fresh"
| _ => tac
end];
(* Solve all remaining TC premises generated by [iIntoEmpValid] *)
try iSolveTC.
......@@ -715,7 +747,7 @@ Local Ltac iSpecializeArgs_go H xs :=
lazymatch xs with
| hnil => idtac
| hcons ?x ?xs =>
notypeclasses refine (tac_forall_specialize _ _ H _ _ _ _ _ _ _);
notypeclasses refine (tac_forall_specialize _ H _ _ _ _ _ _ _);
[pm_reflexivity ||
let H := pretty_ident H in
fail "iSpecialize:" H "not found"
......@@ -724,8 +756,8 @@ Local Ltac iSpecializeArgs_go H xs :=
fail "iSpecialize: cannot instantiate" P "with" x
|lazymatch goal with (* Force [A] in [ex_intro] to deal with coercions. *)
| |- ∃ _ : ?A, _ =>
notypeclasses refine (@ex_intro A _ x (conj _ _))
end; [shelve..|pm_reflexivity|iSpecializeArgs_go H xs]]
notypeclasses refine (@ex_intro A _ x _)
end; [shelve..|pm_reduce; iSpecializeArgs_go H xs]]
end.
Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
iSpecializeArgs_go H xs.
......@@ -791,7 +823,7 @@ Ltac iSpecializePat_go H1 pats :=
fail "iSpecialize: cannot instantiate" P "with" Q
|pm_reflexivity|iSpecializePat_go H1 pats]]
| SPureGoal ?d :: ?pats =>
notypeclasses refine (tac_specialize_assert_pure _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _ _);
notypeclasses refine (tac_specialize_assert_pure _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
[pm_reflexivity ||
let H1 := pretty_ident H1 in
fail "iSpecialize:" H1 "not found"
......@@ -799,9 +831,9 @@ Ltac iSpecializePat_go H1 pats :=
|iSolveTC ||
let Q := match goal with |- FromPure _ ?Q _ => Q end in
fail "iSpecialize:" Q "not pure"
|pm_reflexivity
|solve_done d (*goal*)
|iSpecializePat_go H1 pats]
|pm_reduce;
iSpecializePat_go H1 pats]
| SGoal (SpecGoal GIntuitionistic false ?Hs_frame [] ?d) :: ?pats =>
notypeclasses refine (tac_specialize_assert_intuitionistic _ _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _ _);
[pm_reflexivity ||
......@@ -1063,22 +1095,22 @@ Tactic Notation "iRight" :=
fail "iRight:" P "not a disjunction"
|(* subgoal *)].
Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
eapply tac_or_destruct with _ _ H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
eapply tac_or_destruct with H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
[pm_reflexivity ||
let H := pretty_ident H in
fail "iOrDestruct:" H "not found"
|iSolveTC ||
let P := match goal with |- IntoOr ?P _ _ => P end in
fail "iOrDestruct: cannot destruct" P
|pm_reflexivity ||
let H1 := pretty_ident H1 in
fail "iOrDestruct:" H1 "not fresh"
|pm_reflexivity ||
let H2 := pretty_ident H2 in
fail "iOrDestruct:" H2 "not fresh"
|(* subgoal 1 *)
|(* subgoal 2 *)].
| pm_reduce;
lazymatch goal with
| |- False =>
let H1 := pretty_ident H1 in
let H2 := pretty_ident H2 in
fail "iOrDestruct:" H1 "or" H2 "not fresh"
| _ => split
end].
(** * Conjunction and separating conjunction *)
Tactic Notation "iSplit" :=
......@@ -1094,35 +1126,39 @@ Tactic Notation "iSplitL" constr(Hs) :=
iStartProof;
let Hs := words Hs in
let Hs := eval vm_compute in (INamed <$> Hs) in
eapply tac_sep_split with _ _ Left Hs _ _; (* (js:=Hs) *)
let Δ := iGetCtx in
eapply tac_sep_split with Left Hs _ _; (* (js:=Hs) *)
[iSolveTC ||
let P := match goal with |- FromSep _ ?P _ _ => P end in
fail "iSplitL:" P "not a separating conjunction"
|pm_reflexivity ||
let Hs := iMissingHyps Hs in
fail "iSplitL: hypotheses" Hs "not found"
|(* subgoal 1 *)
|(* subgoal 2 *)].
|pm_reduce;
lazymatch goal with
| |- False => let Hs := iMissingHypsCore Δ Hs in
fail "iSplitL: hypotheses" Hs "not found"
| _ => split; [(* subgoal 1 *)|(* subgoal 2 *)]
end].
Tactic Notation "iSplitR" constr(Hs) :=
iStartProof;
let Hs := words Hs in
let Hs := eval vm_compute in (INamed <$> Hs) in
eapply tac_sep_split with _ _ Right Hs _ _; (* (js:=Hs) *)
let Δ := iGetCtx in
eapply tac_sep_split with Right Hs _ _; (* (js:=Hs) *)
[iSolveTC ||
let P := match goal with |- FromSep _ ?P _ _ => P end in
fail "iSplitR:" P "not a separating conjunction"
|pm_reflexivity ||
let Hs := iMissingHyps Hs in
fail "iSplitR: hypotheses" Hs "not found"
|(* subgoal 1 *)
|(* subgoal 2 *)].
|pm_reduce;
lazymatch goal with
| |- False => let Hs := iMissingHypsCore Δ Hs in
fail "iSplitR: hypotheses" Hs "not found"
| _ => split; [(* subgoal 1 *)|(* subgoal 2 *)]
end].
Tactic Notation "iSplitL" := iSplitR "".
Tactic Notation "iSplitR" := iSplitL "".
Local Tactic Notation "iAndDestruct" constr(H) "as" constr(H1) constr(H2) :=
eapply tac_and_destruct with _ H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
eapply tac_and_destruct with H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
[pm_reflexivity ||
let H := pretty_ident H in
fail "iAndDestruct:" H "not found"
......@@ -1133,22 +1169,28 @@ Local Tactic Notation "iAndDestruct" constr(H) "as" constr(H1) constr(H2) :=
| |- IntoAnd _ ?P _ _ => P
end in
fail "iAndDestruct: cannot destruct" P
|pm_reflexivity ||
let H1 := pretty_ident H1 in
let H2 := pretty_ident H2 in
fail "iAndDestruct:" H1 "or" H2 "not fresh"
|(* subgoal *)].
|pm_reduce;
lazymatch goal with
| |- False =>
let H1 := pretty_ident H1 in
let H2 := pretty_ident H2 in
fail "iAndDestruct:" H1 "or" H2 "not fresh"
| _ => idtac (* subgoal *)
end].
Local Tactic Notation "iAndDestructChoice" constr(H) "as" constr(d) constr(H') :=
eapply tac_and_destruct_choice with _ H _ d H' _ _ _;
eapply tac_and_destruct_choice with H _ d H' _ _ _;
[pm_reflexivity || fail "iAndDestructChoice:" H "not found"
|pm_reduce; iSolveTC ||
let P := match goal with |- TCOr (IntoAnd _ ?P _ _) _ => P end in
fail "iAndDestructChoice: cannot destruct" P
|pm_reflexivity ||
let H' := pretty_ident H' in
fail "iAndDestructChoice:" H' "not fresh"
|(* subgoal *)].
|pm_reduce;
lazymatch goal with
| |- False =>
let H' := pretty_ident H' in
fail "iAndDestructChoice:" H' "not fresh"
| _ => idtac (* subgoal *)
end].
(** * Existential *)
Tactic Notation "iExists" uconstr(x1) :=
......@@ -1190,13 +1232,14 @@ Local Tactic Notation "iExistDestruct" constr(H)
|iSolveTC ||
let P := match goal with |- IntoExist ?P _ => P end in
fail "iExistDestruct: cannot destruct" P|];
let y := fresh in
intros y; eexists; split;
[pm_reflexivity ||
let Hx := pretty_ident Hx in
fail "iExistDestruct:" Hx "not fresh"
|revert y; intros x
(* subgoal *)].
let y := fresh in
intros y; pm_reduce;
match goal with
| |- False =>
let Hx := pretty_ident Hx in
fail "iExistDestruct:" Hx "not fresh"
| _ => revert y; intros x (* subgoal *)
end.
(** * Modality introduction *)
Tactic Notation "iModIntro" uconstr(sel) :=
......@@ -1229,15 +1272,14 @@ Tactic Notation "iNext" := iModIntro (▷^_ _)%I.
(** * Update modality *)
Tactic Notation "iModCore" constr(H) :=
eapply tac_modal_elim with _ H _ _ _ _ _ _;
eapply tac_modal_elim with H _ _ _ _ _ _;
[pm_reflexivity || fail "iMod:" H "not found"
|iSolveTC ||
let P := match goal with |- ElimModal _ _ _ ?P _ _ _ => P end in