Commit 2539f335 authored by Robbert Krebbers's avatar Robbert Krebbers

Move iIntro tactics arround.

parent 99fd8e5b
Pipeline #573 passed with stage
......@@ -97,46 +97,6 @@ Tactic Notation "iAssumption" :=
(** * False *)
Tactic Notation "iExFalso" := apply tac_ex_falso.
(** * Pure introduction *)
Local Tactic Notation "iIntro" "{" simple_intropattern(x) "}" :=
lazymatch goal with
| |- _ ( _, _) => apply tac_forall_intro; intros x
| |- _ (?P _) =>
eapply tac_impl_intro_pure;
[apply _ || fail "iIntro:" P "not pure"|]; intros x
| |- _ (?P - _) =>
eapply tac_wand_intro_pure;
[apply _ || fail "iIntro:" P "not pure"|]; intros x
| |- _ => intros x
end.
(** * Introduction *)
Local Tactic Notation "iIntro" constr(H) :=
lazymatch goal with
| |- _ (?Q _) =>
eapply tac_impl_intro with _ H; (* (i:=H) *)
[reflexivity || fail "iIntro: introducing " H ":" Q
"into non-empty spatial context"
|env_cbv; reflexivity || fail "iIntro:" H "not fresh"|]
| |- _ (_ - _) =>
eapply tac_wand_intro with _ H; (* (i:=H) *)
[env_cbv; reflexivity || fail "iIntro:" H "not fresh"|]
| _ => fail "iIntro: nothing to introduce"
end.
Local Tactic Notation "iIntro" "#" constr(H) :=
lazymatch goal with
| |- _ (?P _) =>
eapply tac_impl_intro_persistent with _ H _; (* (i:=H) *)
[apply _ || fail "iIntro: " P " not persistent"
|env_cbv; reflexivity || fail "iIntro:" H "not fresh"|]
| |- _ (?P - _) =>
eapply tac_wand_intro_persistent with _ H _; (* (i:=H) *)
[apply _ || fail "iIntro: " P " not persistent"
|env_cbv; reflexivity || fail "iIntro:" H "not fresh"|]
| _ => fail "iIntro: nothing to introduce"
end.
(** * Making hypotheses persistent or pure *)
Local Tactic Notation "iPersistent" constr(H) :=
eapply tac_persistent with _ H _ _ _; (* (i:=H) *)
......@@ -685,6 +645,44 @@ Tactic Notation "iNext":=
apply _ || fail "iNext:" P "does not contain laters"|].
(** * Introduction tactic *)
Local Tactic Notation "iIntro" "{" simple_intropattern(x) "}" :=
lazymatch goal with
| |- _ ( _, _) => apply tac_forall_intro; intros x
| |- _ (?P _) =>
eapply tac_impl_intro_pure;
[apply _ || fail "iIntro:" P "not pure"|]; intros x
| |- _ (?P - _) =>
eapply tac_wand_intro_pure;
[apply _ || fail "iIntro:" P "not pure"|]; intros x
| |- _ => intros x
end.
Local Tactic Notation "iIntro" constr(H) :=
lazymatch goal with
| |- _ (?Q _) =>
eapply tac_impl_intro with _ H; (* (i:=H) *)
[reflexivity || fail "iIntro: introducing " H ":" Q
"into non-empty spatial context"
|env_cbv; reflexivity || fail "iIntro:" H "not fresh"|]
| |- _ (_ - _) =>
eapply tac_wand_intro with _ H; (* (i:=H) *)
[env_cbv; reflexivity || fail "iIntro:" H "not fresh"|]
| _ => fail "iIntro: nothing to introduce"
end.
Local Tactic Notation "iIntro" "#" constr(H) :=
lazymatch goal with
| |- _ (?P _) =>
eapply tac_impl_intro_persistent with _ H _; (* (i:=H) *)
[apply _ || fail "iIntro: " P " not persistent"
|env_cbv; reflexivity || fail "iIntro:" H "not fresh"|]
| |- _ (?P - _) =>
eapply tac_wand_intro_persistent with _ H _; (* (i:=H) *)
[apply _ || fail "iIntro: " P " not persistent"
|env_cbv; reflexivity || fail "iIntro:" H "not fresh"|]
| _ => fail "iIntro: nothing to introduce"
end.
Tactic Notation "iIntros" constr(pat) :=
let rec go pats :=
lazymatch pats 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