Commit b39f5a52 authored by Ralf Jung's avatar Ralf Jung

Proof mode error messages: Print hypothesis name without [INamed]

parent 4d9e16ec
...@@ -37,11 +37,11 @@ No applicable tactic. ...@@ -37,11 +37,11 @@ No applicable tactic.
The command has indeed failed with message: The command has indeed failed with message:
In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
"iElaborateSelPat_go", last call failed. "iElaborateSelPat_go", last call failed.
Tactic failure: iElaborateSelPat: (INamed "HQ") not found. Tactic failure: iElaborateSelPat: "HQ" not found.
The command has indeed failed with message: The command has indeed failed with message:
In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
"iElaborateSelPat_go", last call failed. "iElaborateSelPat_go", last call failed.
Tactic failure: iElaborateSelPat: (INamed "HQ") not found. Tactic failure: iElaborateSelPat: "HQ" not found.
The command has indeed failed with message: The command has indeed failed with message:
In nested Ltac calls to "iSpecialize (open_constr)", In nested Ltac calls to "iSpecialize (open_constr)",
"iSpecializeCore (open_constr) as (constr)", "iSpecializeCore (open_constr) as (constr)",
...@@ -192,7 +192,11 @@ The command has indeed failed with message: ...@@ -192,7 +192,11 @@ The command has indeed failed with message:
In nested Ltac calls to "iDestruct (open_constr) as (constr)", In nested Ltac calls to "iDestruct (open_constr) as (constr)",
"iDestructCore (open_constr) as (constr) (tactic)" and "iDestructCore (open_constr) as (constr) (tactic)" and
"iDestructCore (open_constr) as (constr) (tactic)", last call failed. "iDestructCore (open_constr) as (constr) (tactic)", last call failed.
Tactic failure: iDestruct: (INamed "HQ") not found. Tactic failure: iDestruct: "HQ" not found.
The command has indeed failed with message:
In nested Ltac calls to "iIntros (constr)", "iIntros_go" and
"iIntro (constr)", last call failed.
Tactic failure: iIntro: "HP" not fresh.
The command has indeed failed with message: The command has indeed failed with message:
In nested Ltac calls to "iIntros ( (intropattern) )", In nested Ltac calls to "iIntros ( (intropattern) )",
"iIntro ( (intropattern) )" and "intros x", last call failed. "iIntro ( (intropattern) )" and "intros x", last call failed.
...@@ -203,3 +207,6 @@ Tactic failure: iSplitL: hypotheses ["HPx"] not found. ...@@ -203,3 +207,6 @@ Tactic failure: iSplitL: hypotheses ["HPx"] not found.
The command has indeed failed with message: The command has indeed failed with message:
Ltac call to "iSplitL (constr)" failed. Ltac call to "iSplitL (constr)" failed.
Tactic failure: iSplitL: hypotheses ["HPx"] not found. Tactic failure: iSplitL: hypotheses ["HPx"] not found.
The command has indeed failed with message:
Ltac call to "iExact (constr)" failed.
Tactic failure: iExact: "HQ" not found.
...@@ -561,9 +561,12 @@ Lemma iDestruct_bad_name P : ...@@ -561,9 +561,12 @@ Lemma iDestruct_bad_name P :
P - P. P - P.
Proof. iIntros "HP". Fail iDestruct "HQ" as "HP". Abort. Proof. iIntros "HP". Fail iDestruct "HQ" as "HP". Abort.
Lemma iIntros_dup_name P : Lemma iIntros_dup_name P Q :
P - x y : (), P. P - Q - x y : (), P.
Proof. iIntros "HP" (x). Fail iIntros (x). Abort. Proof.
iIntros "HP". Fail iIntros "HP".
iIntros "HQ" (x). Fail iIntros (x).
Abort.
Lemma iSplit_one_of_many P : Lemma iSplit_one_of_many P :
P - P - P P. P - P - P P.
...@@ -571,4 +574,10 @@ Proof. ...@@ -571,4 +574,10 @@ Proof.
iIntros "HP1 HP2". Fail iSplitL "HP1 HPx". Fail iSplitL "HPx HP1". iIntros "HP1 HP2". Fail iSplitL "HP1 HPx". Fail iSplitL "HPx HP1".
Abort. Abort.
Lemma iExact_not_found P :
P - P.
Proof.
iIntros "HP". Fail iExact "HQ".
Abort.
End error_tests. End error_tests.
...@@ -30,6 +30,13 @@ and iInv. *) ...@@ -30,6 +30,13 @@ and iInv. *)
Ltac iSolveSideCondition := Ltac iSolveSideCondition :=
split_and?; try solve [ fast_done | solve_ndisj ]. split_and?; try solve [ fast_done | solve_ndisj ].
(** Used for printing [string]s and [ident]s. *)
Ltac pretty_ident H :=
lazymatch H with
| INamed ?H => H
| ?H => H
end.
(** * Misc *) (** * Misc *)
Ltac iMissingHyps Hs := Ltac iMissingHyps Hs :=
...@@ -148,7 +155,9 @@ Ltac iElaborateSelPat_go pat Δ Hs := ...@@ -148,7 +155,9 @@ Ltac iElaborateSelPat_go pat Δ Hs :=
| SelIdent ?H :: ?pat => | SelIdent ?H :: ?pat =>
lazymatch pm_eval (envs_lookup_delete false H Δ) with lazymatch pm_eval (envs_lookup_delete false H Δ) with
| Some (?p,_,?Δ') => iElaborateSelPat_go pat Δ' (ESelIdent p H :: Hs) | Some (?p,_,?Δ') => iElaborateSelPat_go pat Δ' (ESelIdent p H :: Hs)
| None => fail "iElaborateSelPat:" H "not found" | None =>
let H := pretty_ident H in
fail "iElaborateSelPat:" H "not found"
end end
end. end.
Ltac iElaborateSelPat pat := Ltac iElaborateSelPat pat :=
...@@ -159,7 +168,9 @@ Ltac iElaborateSelPat pat := ...@@ -159,7 +168,9 @@ Ltac iElaborateSelPat pat :=
Local Ltac iClearHyp H := Local Ltac iClearHyp H :=
eapply tac_clear with _ H _ _; (* (i:=H) *) eapply tac_clear with _ H _ _; (* (i:=H) *)
[pm_reflexivity || fail "iClear:" H "not found" [pm_reflexivity ||
let H := pretty_ident H in
fail "iClear:" H "not found"
|pm_reduce; iSolveTC || |pm_reduce; iSolveTC ||
let P := match goal with |- TCOr (Affine ?P) _ => P end in let P := match goal with |- TCOr (Affine ?P) _ => P end in
fail "iClear:" H ":" P "not affine and the goal not absorbing" fail "iClear:" H ":" P "not affine and the goal not absorbing"
...@@ -180,7 +191,8 @@ Tactic Notation "iClear" "(" ident_list(xs) ")" constr(Hs) := ...@@ -180,7 +191,8 @@ Tactic Notation "iClear" "(" ident_list(xs) ")" constr(Hs) :=
(** * Assumptions *) (** * Assumptions *)
Tactic Notation "iExact" constr(H) := Tactic Notation "iExact" constr(H) :=
eapply tac_assumption with _ H _ _; (* (i:=H) *) eapply tac_assumption with _ H _ _; (* (i:=H) *)
[pm_reflexivity || fail "iExact:" H "not found" [pm_reflexivity ||
fail "iExact:" H "not found"
|iSolveTC || |iSolveTC ||
let P := match goal with |- FromAssumption _ ?P _ => P end in let P := match goal with |- FromAssumption _ ?P _ => P end in
fail "iExact:" H ":" P "does not match goal" fail "iExact:" H ":" P "does not match goal"
...@@ -232,7 +244,9 @@ Tactic Notation "iExFalso" := apply tac_ex_falso. ...@@ -232,7 +244,9 @@ Tactic Notation "iExFalso" := apply tac_ex_falso.
(** * Making hypotheses persistent or pure *) (** * Making hypotheses persistent or pure *)
Local Tactic Notation "iPersistent" constr(H) := Local Tactic Notation "iPersistent" constr(H) :=
eapply tac_persistent with _ H _ _ _; (* (i:=H) *) eapply tac_persistent with _ H _ _ _; (* (i:=H) *)
[pm_reflexivity || fail "iPersistent:" H "not found" [pm_reflexivity ||
let H := pretty_ident H in
fail "iPersistent:" H "not found"
|iSolveTC || |iSolveTC ||
let P := match goal with |- IntoPersistent _ ?P _ => P end in let P := match goal with |- IntoPersistent _ ?P _ => P end in
fail "iPersistent:" P "not persistent" fail "iPersistent:" P "not persistent"
...@@ -243,7 +257,9 @@ Local Tactic Notation "iPersistent" constr(H) := ...@@ -243,7 +257,9 @@ Local Tactic Notation "iPersistent" constr(H) :=
Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) := Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
eapply tac_pure with _ H _ _ _; (* (i:=H1) *) eapply tac_pure with _ H _ _ _; (* (i:=H1) *)
[pm_reflexivity || fail "iPure:" H "not found" [pm_reflexivity ||
let H := pretty_ident H in
fail "iPure:" H "not found"
|iSolveTC || |iSolveTC ||
let P := match goal with |- IntoPure ?P _ => P end in let P := match goal with |- IntoPure ?P _ => P end in
fail "iPure:" P "not pure" fail "iPure:" P "not pure"
...@@ -285,7 +301,9 @@ Local Ltac iFramePure t := ...@@ -285,7 +301,9 @@ Local Ltac iFramePure t :=
Local Ltac iFrameHyp H := Local Ltac iFrameHyp H :=
iStartProof; iStartProof;
eapply tac_frame with _ H _ _ _; eapply tac_frame with _ H _ _ _;
[pm_reflexivity || fail "iFrame:" H "not found" [pm_reflexivity ||
let H := pretty_ident H in
fail "iFrame:" H "not found"
|iSolveTC || |iSolveTC ||
let R := match goal with |- Frame _ ?R _ _ => R end in let R := match goal with |- Frame _ ?R _ _ => R end in
fail "iFrame: cannot frame" R fail "iFrame: cannot frame" R
...@@ -395,13 +413,17 @@ Local Tactic Notation "iIntro" constr(H) := ...@@ -395,13 +413,17 @@ Local Tactic Notation "iIntro" constr(H) :=
let P := lazymatch goal with |- Persistent ?P => P end in let P := lazymatch goal with |- Persistent ?P => P end in
fail 1 "iIntro: introducing non-persistent" H ":" P fail 1 "iIntro: introducing non-persistent" H ":" P
"into non-empty spatial context" "into non-empty spatial context"
|pm_reflexivity || fail 1 "iIntro:" H "not fresh" |pm_reflexivity ||
let H := pretty_ident H in
fail 1 "iIntro:" H "not fresh"
|iSolveTC |iSolveTC
|] |]
| (* (_ -∗ _) *) | (* (_ -∗ _) *)
eapply tac_wand_intro with _ H _ _; (* (i:=H) *) eapply tac_wand_intro with _ H _ _; (* (i:=H) *)
[iSolveTC [iSolveTC
| pm_reflexivity || fail 1 "iIntro:" H "not fresh" | pm_reflexivity ||
let H := pretty_ident H in
fail 1 "iIntro:" H "not fresh"
|] |]
| fail "iIntro: nothing to introduce" ]. | fail "iIntro: nothing to introduce" ].
...@@ -414,7 +436,9 @@ Local Tactic Notation "iIntro" "#" constr(H) := ...@@ -414,7 +436,9 @@ Local Tactic Notation "iIntro" "#" constr(H) :=
|iSolveTC || |iSolveTC ||
let P := match goal with |- IntoPersistent _ ?P _ => P end in let P := match goal with |- IntoPersistent _ ?P _ => P end in
fail 1 "iIntro:" P "not persistent" fail 1 "iIntro:" P "not persistent"
|pm_reflexivity || fail 1 "iIntro:" H "not fresh" |pm_reflexivity ||
let H := pretty_ident H in
fail 1 "iIntro:" H "not fresh"
|] |]
| (* (?P -∗ _) *) | (* (?P -∗ _) *)
eapply tac_wand_intro_persistent with _ H _ _ _; (* (i:=H) *) eapply tac_wand_intro_persistent with _ H _ _ _; (* (i:=H) *)
...@@ -425,7 +449,9 @@ Local Tactic Notation "iIntro" "#" constr(H) := ...@@ -425,7 +449,9 @@ Local Tactic Notation "iIntro" "#" constr(H) :=
|iSolveTC || |iSolveTC ||
let P := match goal with |- TCOr (Affine ?P) _ => P end in let P := match goal with |- TCOr (Affine ?P) _ => P end in
fail 1 "iIntro:" P "not affine and the goal not absorbing" fail 1 "iIntro:" P "not affine and the goal not absorbing"
|pm_reflexivity || fail 1 "iIntro:" H "not fresh" |pm_reflexivity ||
let H := pretty_ident H in
fail 1 "iIntro:" H "not fresh"
|] |]
| fail "iIntro: nothing to introduce" ]. | fail "iIntro: nothing to introduce" ].
...@@ -488,7 +514,9 @@ Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) := ...@@ -488,7 +514,9 @@ Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
| hnil => idtac | hnil => idtac
| hcons ?x ?xs => | hcons ?x ?xs =>
notypeclasses refine (tac_forall_specialize _ _ H _ _ _ _ _ _ _); notypeclasses refine (tac_forall_specialize _ _ H _ _ _ _ _ _ _);
[pm_reflexivity || fail "iSpecialize:" H "not found" [pm_reflexivity ||
let H := pretty_ident H in
fail "iSpecialize:" H "not found"
|iSolveTC || |iSolveTC ||
let P := match goal with |- IntoForall ?P _ => P end in let P := match goal with |- IntoForall ?P _ => P end in
fail "iSpecialize: cannot instantiate" P "with" x fail "iSpecialize: cannot instantiate" P "with" x
...@@ -519,8 +547,12 @@ Ltac iSpecializePat_go H1 pats := ...@@ -519,8 +547,12 @@ Ltac iSpecializePat_go H1 pats :=
iSpecializePat_go H1 pats iSpecializePat_go H1 pats
| SIdent ?H2 :: ?pats => | SIdent ?H2 :: ?pats =>
notypeclasses refine (tac_specialize _ _ _ H2 _ H1 _ _ _ _ _ _ _ _ _ _); notypeclasses refine (tac_specialize _ _ _ H2 _ H1 _ _ _ _ _ _ _ _ _ _);
[pm_reflexivity || fail "iSpecialize:" H2 "not found" [pm_reflexivity ||
|pm_reflexivity || fail "iSpecialize:" H1 "not found" let H2 := pretty_ident H2 in
fail "iSpecialize:" H2 "not found"
|pm_reflexivity ||
let H1 := pretty_ident H1 in
fail "iSpecialize:" H1 "not found"
|iSolveTC || |iSolveTC ||
let P := match goal with |- IntoWand _ _ ?P ?Q _ => P end in let P := match goal with |- IntoWand _ _ ?P ?Q _ => P end in
let Q := match goal with |- IntoWand _ _ ?P ?Q _ => Q end in let Q := match goal with |- IntoWand _ _ ?P ?Q _ => Q end in
...@@ -528,7 +560,9 @@ Ltac iSpecializePat_go H1 pats := ...@@ -528,7 +560,9 @@ Ltac iSpecializePat_go H1 pats :=
|pm_reflexivity|iSpecializePat_go H1 pats] |pm_reflexivity|iSpecializePat_go H1 pats]
| SPureGoal ?d :: ?pats => | SPureGoal ?d :: ?pats =>
notypeclasses refine (tac_specialize_assert_pure _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _); notypeclasses refine (tac_specialize_assert_pure _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
[pm_reflexivity || fail "iSpecialize:" H1 "not found" [pm_reflexivity ||
let H1 := pretty_ident H1 in
fail "iSpecialize:" H1 "not found"
|solve_to_wand H1 |solve_to_wand H1
|iSolveTC || |iSolveTC ||
let Q := match goal with |- FromPure _ ?Q _ => Q end in let Q := match goal with |- FromPure _ ?Q _ => Q end in
...@@ -538,7 +572,9 @@ Ltac iSpecializePat_go H1 pats := ...@@ -538,7 +572,9 @@ Ltac iSpecializePat_go H1 pats :=
|iSpecializePat_go H1 pats] |iSpecializePat_go H1 pats]
| SGoal (SpecGoal GPersistent false ?Hs_frame [] ?d) :: ?pats => | SGoal (SpecGoal GPersistent false ?Hs_frame [] ?d) :: ?pats =>
notypeclasses refine (tac_specialize_assert_persistent _ _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _ _); notypeclasses refine (tac_specialize_assert_persistent _ _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _ _);
[pm_reflexivity || fail "iSpecialize:" H1 "not found" [pm_reflexivity ||
let H1 := pretty_ident H1 in
fail "iSpecialize:" H1 "not found"
|solve_to_wand H1 |solve_to_wand H1
|iSolveTC || |iSolveTC ||
let Q := match goal with |- Persistent ?Q => Q end in let Q := match goal with |- Persistent ?Q => Q end in
...@@ -552,7 +588,9 @@ Ltac iSpecializePat_go H1 pats := ...@@ -552,7 +588,9 @@ Ltac iSpecializePat_go H1 pats :=
| SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs ?d) :: ?pats => | SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs ?d) :: ?pats =>
let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
notypeclasses refine (tac_specialize_assert _ _ _ _ H1 _ lr Hs' _ _ _ _ _ _ _ _ _ _ _); notypeclasses refine (tac_specialize_assert _ _ _ _ H1 _ lr Hs' _ _ _ _ _ _ _ _ _ _ _);
[pm_reflexivity || fail "iSpecialize:" H1 "not found" [pm_reflexivity ||
let H1 := pretty_ident H1 in
fail "iSpecialize:" H1 "not found"
|solve_to_wand H1 |solve_to_wand H1
|lazymatch m with |lazymatch m with
| GSpatial => notypeclasses refine (add_modal_id _ _) | GSpatial => notypeclasses refine (add_modal_id _ _)
...@@ -565,7 +603,9 @@ Ltac iSpecializePat_go H1 pats := ...@@ -565,7 +603,9 @@ Ltac iSpecializePat_go H1 pats :=
|iSpecializePat_go H1 pats] |iSpecializePat_go H1 pats]
| SAutoFrame GPersistent :: ?pats => | SAutoFrame GPersistent :: ?pats =>
notypeclasses refine (tac_specialize_assert_persistent _ _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _ _); notypeclasses refine (tac_specialize_assert_persistent _ _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _ _);
[pm_reflexivity || fail "iSpecialize:" H1 "not found" [pm_reflexivity ||
let H1 := pretty_ident H1 in
fail "iSpecialize:" H1 "not found"
|solve_to_wand H1 |solve_to_wand H1
|iSolveTC || |iSolveTC ||
let Q := match goal with |- Persistent ?Q => Q end in let Q := match goal with |- Persistent ?Q => Q end in
...@@ -575,7 +615,9 @@ Ltac iSpecializePat_go H1 pats := ...@@ -575,7 +615,9 @@ Ltac iSpecializePat_go H1 pats :=
|iSpecializePat_go H1 pats] |iSpecializePat_go H1 pats]
| SAutoFrame ?m :: ?pats => | SAutoFrame ?m :: ?pats =>
notypeclasses refine (tac_specialize_frame _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _); notypeclasses refine (tac_specialize_frame _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
[pm_reflexivity || fail "iSpecialize:" H1 "not found" [pm_reflexivity ||
let H1 := pretty_ident H1 in
fail "iSpecialize:" H1 "not found"
|solve_to_wand H1 |solve_to_wand H1
|lazymatch m with |lazymatch m with
| GSpatial => notypeclasses refine (add_modal_id _ _) | GSpatial => notypeclasses refine (add_modal_id _ _)
...@@ -625,7 +667,9 @@ Tactic Notation "iSpecializeCore" open_constr(H) ...@@ -625,7 +667,9 @@ Tactic Notation "iSpecializeCore" open_constr(H)
| true => | true =>
(* FIXME: do something reasonable when the BI is not affine *) (* FIXME: do something reasonable when the BI is not affine *)
notypeclasses refine (tac_specialize_persistent_helper _ _ H _ _ _ _ _ _ _ _ _ _ _); notypeclasses refine (tac_specialize_persistent_helper _ _ H _ _ _ _ _ _ _ _ _ _ _);
[pm_reflexivity || fail "iSpecialize:" H "not found" [pm_reflexivity ||
let H := pretty_ident H in
fail "iSpecialize:" H "not found"
|iSpecializePat H pat; |iSpecializePat H pat;
[.. [..
|refine (tac_specialize_persistent_helper_done _ H _ _ _); |refine (tac_specialize_persistent_helper_done _ H _ _ _);
...@@ -732,13 +776,19 @@ Tactic Notation "iPoseProofCore" open_constr(lem) ...@@ -732,13 +776,19 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
lazymatch type of t with lazymatch type of t with
| ident => | ident =>
eapply tac_pose_proof_hyp with _ _ t _ Htmp _; eapply tac_pose_proof_hyp with _ _ t _ Htmp _;
[pm_reflexivity || fail "iPoseProof:" t "not found" [pm_reflexivity ||
|pm_reflexivity || fail "iPoseProof:" Htmp "not fresh" let t := pretty_ident t in
fail "iPoseProof:" t "not found"
|pm_reflexivity ||
let Htmp := pretty_ident Htmp in
fail "iPoseProof:" Htmp "not fresh"
|goal_tac ()] |goal_tac ()]
| _ => | _ =>
eapply tac_pose_proof with _ Htmp _; (* (j:=H) *) eapply tac_pose_proof with _ Htmp _; (* (j:=H) *)
[iIntoEmpValid t [iIntoEmpValid t
|pm_reflexivity || fail "iPoseProof:" Htmp "not fresh" |pm_reflexivity ||
let Htmp := pretty_ident Htmp in
fail "iPoseProof:" Htmp "not fresh"
|goal_tac ()] |goal_tac ()]
end; end;
try iSolveTC in try iSolveTC in
...@@ -788,7 +838,9 @@ Tactic Notation "iRevert" constr(Hs) := ...@@ -788,7 +838,9 @@ Tactic Notation "iRevert" constr(Hs) :=
go Hs go Hs
| ESelIdent _ ?H :: ?Hs => | ESelIdent _ ?H :: ?Hs =>
eapply tac_revert with _ H _ _; (* (i:=H2) *) eapply tac_revert with _ H _ _; (* (i:=H2) *)
[pm_reflexivity || fail "iRevert:" H "not found" [pm_reflexivity ||
let H := pretty_ident H in
fail "iRevert:" H "not found"
|pm_reduce; go Hs] |pm_reduce; go Hs]
end in end in
let Hs := iElaborateSelPat Hs in iStartProof; go Hs. let Hs := iElaborateSelPat Hs in iStartProof; go Hs.
...@@ -854,12 +906,18 @@ Tactic Notation "iRight" := ...@@ -854,12 +906,18 @@ Tactic Notation "iRight" :=
Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) := 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) *) eapply tac_or_destruct with _ _ H _ H1 H2 _ _ _; (* (i:=H) (j1:=H1) (j2:=H2) *)
[pm_reflexivity || fail "iOrDestruct:" H "not found" [pm_reflexivity ||
let H := pretty_ident H in
fail "iOrDestruct:" H "not found"
|iSolveTC || |iSolveTC ||
let P := match goal with |- IntoOr ?P _ _ => P end in let P := match goal with |- IntoOr ?P _ _ => P end in
fail "iOrDestruct: cannot destruct" P fail "iOrDestruct: cannot destruct" P
|pm_reflexivity || fail "iOrDestruct:" H1 "not fresh" |pm_reflexivity ||
|pm_reflexivity || fail "iOrDestruct:" H2 "not fresh" let H1 := pretty_ident H1 in
fail "iOrDestruct:" H1 "not fresh"
|pm_reflexivity ||
let H2 := pretty_ident H2 in
fail "iOrDestruct:" H2 "not fresh"
| |]. | |].
(** * Conjunction and separating conjunction *) (** * Conjunction and separating conjunction *)
...@@ -901,7 +959,9 @@ Tactic Notation "iSplitR" := iSplitL "". ...@@ -901,7 +959,9 @@ Tactic Notation "iSplitR" := iSplitL "".
Local Tactic Notation "iAndDestruct" constr(H) "as" constr(H1) constr(H2) := 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 || fail "iAndDestruct:" H "not found" [pm_reflexivity ||
let H := pretty_ident H in
fail "iAndDestruct:" H "not found"
|pm_reduce; iSolveTC || |pm_reduce; iSolveTC ||
let P := let P :=
lazymatch goal with lazymatch goal with
...@@ -909,7 +969,10 @@ Local Tactic Notation "iAndDestruct" constr(H) "as" constr(H1) constr(H2) := ...@@ -909,7 +969,10 @@ Local Tactic Notation "iAndDestruct" constr(H) "as" constr(H1) constr(H2) :=
| |- IntoAnd _ ?P _ _ => P | |- IntoAnd _ ?P _ _ => P
end in end in
fail "iAndDestruct: cannot destruct" P fail "iAndDestruct: cannot destruct" P
|pm_reflexivity || fail "iAndDestruct:" H1 "or" H2 " not fresh"|]. |pm_reflexivity ||
let H1 := pretty_ident H1 in
let H2 := pretty_ident H2 in
fail "iAndDestruct:" H1 "or" H2 " not fresh"|].
Local Tactic Notation "iAndDestructChoice" constr(H) "as" constr(d) constr(H') := 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' _ _ _;
...@@ -917,7 +980,9 @@ Local Tactic Notation "iAndDestructChoice" constr(H) "as" constr(d) constr(H') : ...@@ -917,7 +980,9 @@ Local Tactic Notation "iAndDestructChoice" constr(H) "as" constr(d) constr(H') :
|pm_reduce; iSolveTC || |pm_reduce; iSolveTC ||
let P := match goal with |- TCOr (IntoAnd _ ?P _ _) _ => P end in let P := match goal with |- TCOr (IntoAnd _ ?P _ _) _ => P end in
fail "iAndDestructChoice: cannot destruct" P fail "iAndDestructChoice: cannot destruct" P
|pm_reflexivity || fail "iAndDestructChoice:" H' " not fresh"|]. |pm_reflexivity ||
let H' := pretty_ident H' in
fail "iAndDestructChoice:" H' " not fresh"|].
(** * Existential *) (** * Existential *)
Tactic Notation "iExists" uconstr(x1) := Tactic Notation "iExists" uconstr(x1) :=
...@@ -952,13 +1017,17 @@ Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) "," ...@@ -952,13 +1017,17 @@ Tactic Notation "iExists" uconstr(x1) "," uconstr(x2) "," uconstr(x3) ","
Local Tactic Notation "iExistDestruct" constr(H) Local Tactic Notation "iExistDestruct" constr(H)
"as" simple_intropattern(x) constr(Hx) := "as" simple_intropattern(x) constr(Hx) :=
eapply tac_exist_destruct with H _ Hx _ _; (* (i:=H) (j:=Hx) *) eapply tac_exist_destruct with H _ Hx _ _; (* (i:=H) (j:=Hx) *)
[pm_reflexivity || fail "iExistDestruct:" H "not found" [pm_reflexivity ||
let H := pretty_ident H in
fail "iExistDestruct:" H "not found"
|iSolveTC || |iSolveTC ||
let P := match goal with |- IntoExist ?P _ => P end in let P := match goal with |- IntoExist ?P _ => P end in
fail "iExistDestruct: cannot destruct" P|]; fail "iExistDestruct: cannot destruct" P|];
let y := fresh in let y := fresh in
intros y; eexists; split; intros y; eexists; split;
[pm_reflexivity || fail "iExistDestruct:" Hx "not fresh" [pm_reflexivity ||
let Hx := pretty_ident Hx in
fail "iExistDestruct:" Hx "not fresh"
|revert y; intros x]. |revert y; intros x].
(** * Modality introduction *) (** * Modality introduction *)
...@@ -1086,15 +1155,16 @@ Tactic Notation "iCombine" constr(Hs) "as" constr(pat) := ...@@ -1086,15 +1155,16 @@ Tactic Notation "iCombine" constr(Hs) "as" constr(pat) :=
let Hs := iMissingHyps Hs in let Hs := iMissingHyps Hs in
fail "iCombine: hypotheses" Hs "not found" fail "iCombine: hypotheses" Hs "not found"
|iSolveTC |iSolveTC
|pm_reflexivity || fail "iCombine:" H "not fresh" |pm_reflexivity ||
let H := pretty_ident H in
fail "iCombine:" H "not fresh"
|iDestructHyp H as pat]. |iDestructHyp H as pat].
Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(pat) := Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(pat) :=
iCombine [H1;H2] as pat. iCombine [H1;H2] as pat.
(** * Introduction tactic *) (** * Introduction tactic *)
Tactic Notation "iIntros" constr(pat) := Ltac iIntros_go pats startproof :=
let rec go pats startproof :=
lazymatch pats with lazymatch pats with
| [] => | [] =>
lazymatch startproof with lazymatch startproof with
...@@ -1102,28 +1172,29 @@ Tactic Notation "iIntros" constr(pat) := ...@@ -1102,28 +1172,29 @@ Tactic Notation "iIntros" constr(pat) :=
| false => idtac | false => idtac
end end
(* Optimizations to avoid generating fresh names *) (* Optimizations to avoid generating fresh names *)
| IPureElim :: ?pats => iIntro (?); go pats startproof | IPureElim :: ?pats => iIntro (?); iIntros_go pats startproof
| IAlwaysElim (IIdent ?H) :: ?pats => iIntro #H; go pats false | IAlwaysElim (IIdent ?H) :: ?pats => iIntro #H; iIntros_go pats false
| IDrop :: ?pats