Commit 0e078666 authored by Robbert Krebbers's avatar Robbert Krebbers

A bit of refactoring of the `iIntro` tactics.

- More consistent indentation.
- Mark new subgoals as comments.
parent 332f5c45
...@@ -400,21 +400,28 @@ Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" := ...@@ -400,21 +400,28 @@ Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" :=
want to unfold x and start the proof mode. Instead, we want to want to unfold x and start the proof mode. Instead, we want to
use intros. So [iStartProof] has to be called only if [intros] use intros. So [iStartProof] has to be called only if [intros]
fails *) fails *)
intros x || (* We use [_ || _] instead of [first [..|..]] so that the error in the second
(iStartProof; branch propagates upwards. *)
lazymatch goal with (
| |- envs_entails _ _ => (* introduction at the meta level *)
eapply tac_forall_intro; intros x
[iSolveTC || ) || (
let P := match goal with |- FromForall ?P _ => P end in (* introduction in the logic *)
fail "iIntro: cannot turn" P "into a universal quantifier" iStartProof;
|pm_prettify; intros x] lazymatch goal with
end). | |- envs_entails _ _ =>
eapply tac_forall_intro;
[iSolveTC ||
let P := match goal with |- FromForall ?P _ => P end in
fail "iIntro: cannot turn" P "into a universal quantifier"
|pm_prettify; intros x
(* subgoal *)]
end).
Local Tactic Notation "iIntro" constr(H) := Local Tactic Notation "iIntro" constr(H) :=
iStartProof; iStartProof;
first first
[ (* (?Q → _) *) [(* (?Q → _) *)
eapply tac_impl_intro with _ H _ _ _; (* (i:=H) *) eapply tac_impl_intro with _ H _ _ _; (* (i:=H) *)
[iSolveTC [iSolveTC
|pm_reduce; iSolveTC || |pm_reduce; iSolveTC ||
...@@ -425,58 +432,62 @@ Local Tactic Notation "iIntro" constr(H) := ...@@ -425,58 +432,62 @@ Local Tactic Notation "iIntro" constr(H) :=
let H := pretty_ident H in let H := pretty_ident H in
fail 1 "iIntro:" H "not fresh" fail 1 "iIntro:" H "not fresh"
|iSolveTC |iSolveTC
|] |(* subgoal *)]
| (* (_ -∗ _) *) |(* (_ -∗ _) *)
eapply tac_wand_intro with _ H _ _; (* (i:=H) *) eapply tac_wand_intro with _ H _ _; (* (i:=H) *)
[iSolveTC [iSolveTC
| pm_reflexivity || | pm_reflexivity ||
let H := pretty_ident H in let H := pretty_ident H in
fail 1 "iIntro:" H "not fresh" fail 1 "iIntro:" H "not fresh"
|] |(* subgoal *)]
| fail "iIntro: nothing to introduce" ]. | fail 1 "iIntro: nothing to introduce" ].
Local Tactic Notation "iIntro" "#" constr(H) := Local Tactic Notation "iIntro" "#" constr(H) :=
iStartProof; iStartProof;
first first
[ (* (?P → _) *) [(* (?P → _) *)
eapply tac_impl_intro_persistent with _ H _ _ _; (* (i:=H) *) eapply tac_impl_intro_persistent with _ H _ _ _; (* (i:=H) *)
[iSolveTC [iSolveTC
|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 || |pm_reflexivity ||
let H := pretty_ident H in let H := pretty_ident H in
fail 1 "iIntro:" H "not fresh" fail 1 "iIntro:" H "not fresh"
|] |(* subgoal *)]
| (* (?P -∗ _) *) |(* (?P -∗ _) *)
eapply tac_wand_intro_persistent with _ H _ _ _; (* (i:=H) *) eapply tac_wand_intro_persistent with _ H _ _ _; (* (i:=H) *)
[ iSolveTC [iSolveTC
| 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"
|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 || |pm_reflexivity ||
let H := pretty_ident H in let H := pretty_ident H in
fail 1 "iIntro:" H "not fresh" fail 1 "iIntro:" H "not fresh"
|] |(* subgoal *)]
| fail "iIntro: nothing to introduce" ]. |fail 1 "iIntro: nothing to introduce"].
Local Tactic Notation "iIntro" "_" := Local Tactic Notation "iIntro" "_" :=
iStartProof;
first first
[ (* (?Q → _) *) [(* (?Q → _) *)
iStartProof; eapply tac_impl_intro_drop; eapply tac_impl_intro_drop;
[ iSolveTC | ] [iSolveTC
| (* (_ -∗ _) *) |(* subgoal *)]
iStartProof; eapply tac_wand_intro_drop; |(* (_ -∗ _) *)
[ iSolveTC eapply tac_wand_intro_drop;
| iSolveTC || [iSolveTC
let P := match goal with |- TCOr (Affine ?P) _ => P end in |iSolveTC ||
fail 1 "iIntro:" P "not affine and the goal not absorbing" let P := match goal with |- TCOr (Affine ?P) _ => P end in
|] fail 1 "iIntro:" P "not affine and the goal not absorbing"
| (* (∀ _, _) *) iIntro (_) |(* subgoal *)]
| fail 1 "iIntro: nothing to introduce" ]. |(* (∀ _, _) *)
iIntro (_)
(* subgoal *)
|fail 1 "iIntro: nothing to introduce"].
Local Tactic Notation "iIntroForall" := Local Tactic Notation "iIntroForall" :=
lazymatch goal with lazymatch goal 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