Skip to content
Snippets Groups Projects
Commit 25b98a82 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'iInv_more_args' into 'master' 

Allow up to 10 introduction patterns for iInv.

See merge request iris/iris!252
parents 76dd21ac d23e8b0a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/proofmode/ltac_tactics.v
+ 228
− 0
View file @ 25b98a82
......@@ -1356,6 +1356,17 @@ Tactic Notation "iDestructHyp" constr(H) "as" "(" simple_intropattern(x1)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) ")" constr(pat) :=
iExistDestruct H as x1 H; iDestructHyp H as ( x2 x3 x4 x5 x6 x7 x8 ) pat.
Tactic Notation "iDestructHyp" constr(H) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) simple_intropattern(x9) ")" constr(pat) :=
iExistDestruct H as x1 H; iDestructHyp H as ( x2 x3 x4 x5 x6 x7 x8 x9 ) pat.
Tactic Notation "iDestructHyp" constr(H) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) simple_intropattern(x9) simple_intropattern(x10) ")"
constr(pat) :=
iExistDestruct H as x1 H; iDestructHyp H as ( x2 x3 x4 x5 x6 x7 x8 x9 x10 ) pat.
(** * Combinining hypotheses *)
Tactic Notation "iCombine" constr(Hs) "as" constr(pat) :=
......@@ -1776,6 +1787,17 @@ Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) ")" constr(pat) :=
iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) simple_intropattern(x9) ")" constr(pat) :=
iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 x9 ) pat).
Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) simple_intropattern(x9) simple_intropattern(x10) ")"
constr(pat) :=
iDestructCore lem as pat (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ) pat).
Tactic Notation "iDestruct" open_constr(lem) "as" "%" simple_intropattern(pat) :=
iDestructCore lem as true (fun H => iPure H as pat).
......@@ -1813,6 +1835,17 @@ Tactic Notation "iPoseProof" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) ")" constr(pat) :=
iPoseProofCore lem as pat false (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
Tactic Notation "iPoseProof" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) simple_intropattern(x9) ")" constr(pat) :=
iPoseProofCore lem as pat false (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 x9 ) pat).
Tactic Notation "iPoseProof" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) simple_intropattern(x9) simple_intropattern(x10) ")"
constr(pat) :=
iPoseProofCore lem as pat false (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ) pat).
(** * Induction *)
(* An invocation of [iInduction (x) as pat IH forall (x1...xn) Hs] will
......@@ -2347,6 +2380,41 @@ Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
constr(pat) constr(Hclose) :=
iInvCore N with Hs as (Some Hclose) in (fun x H => iDestructHyp H as (x1 x2 x3 x4) pat).
Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) ")" constr(pat) constr(Hclose) :=
iInvCore N with Hs as (Some Hclose) in (fun x H =>
iDestructHyp H as (x1 x2 x3 x4 x5) pat).
Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) constr(Hclose) :=
iInvCore N with Hs as (Some Hclose) in (fun x H =>
iDestructHyp H as (x1 x2 x3 x4 x5 x6) pat).
Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
constr(pat) constr(Hclose) :=
iInvCore N with Hs as (Some Hclose) in (fun x H =>
iDestructHyp H as (x1 x2 x3 x4 x5 x6 x7) pat).
Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) ")" constr(pat) constr(Hclose) :=
iInvCore N with Hs as (Some Hclose) in (fun x H =>
iDestructHyp H as (x1 x2 x3 x4 x5 x6 x7 x8) pat).
Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) simple_intropattern(x9) ")" constr(pat) constr(Hclose) :=
iInvCore N with Hs as (Some Hclose) in (fun x H =>
iDestructHyp H as (x1 x2 x3 x4 x5 x6 x7 x8 x9) pat).
Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) simple_intropattern(x9) simple_intropattern(x10) ")"
constr(pat) constr(Hclose) :=
iInvCore N with Hs as (Some Hclose) in (fun x H =>
iDestructHyp H as (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) pat).
(* Without closing view shift *)
Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" constr(pat) :=
......@@ -2385,6 +2453,59 @@ Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(
| unit => destruct x as []; iDestructHyp H as (x1 x2 x3 x4) pat
| _ => revert x; intros x1; iDestructHyp H as ( x2 x3 x4) pat
end).
Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) ")" constr(pat) :=
iInvCore N with Hs in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as (x1 x2 x3 x4 x5) pat
| _ => revert x; intros x1; iDestructHyp H as ( x2 x3 x4 x5) pat
end).
Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
iInvCore N with Hs in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as (x1 x2 x3 x4 x5 x6) pat
| _ => revert x; intros x1; iDestructHyp H as ( x2 x3 x4 x5 x6) pat
end).
Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
constr(pat) :=
iInvCore N with Hs in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as (x1 x2 x3 x4 x5 x6 x7) pat
| _ => revert x; intros x1; iDestructHyp H as ( x2 x3 x4 x5 x6 x7) pat
end).
Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) ")" constr(pat) :=
iInvCore N with Hs in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as (x1 x2 x3 x4 x5 x6 x7 x8) pat
| _ => revert x; intros x1; iDestructHyp H as ( x2 x3 x4 x5 x6 x7 x8) pat
end).
Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) simple_intropattern(x9) ")" constr(pat) :=
iInvCore N with Hs in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as (x1 x2 x3 x4 x5 x6 x7 x8 x9) pat
| _ => revert x; intros x1; iDestructHyp H as ( x2 x3 x4 x5 x6 x7 x8 x9) pat
end).
Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) simple_intropattern(x9) simple_intropattern(x10) ")"
constr(pat) :=
iInvCore N with Hs in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) pat
| _ => revert x; intros x1; iDestructHyp H as ( x2 x3 x4 x5 x6 x7 x8 x9 x10) pat
end).
(* Without pattern *)
Tactic Notation "iInv" constr(N) "as" constr(pat) constr(Hclose) :=
......@@ -2423,6 +2544,60 @@ Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
| unit => destruct x as []; iDestructHyp H as (x1 x2 x3 x4) pat
| _ => revert x; intros x1; iDestructHyp H as ( x2 x3 x4) pat
end).
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) ")"
constr(pat) constr(Hclose) :=
iInvCore N as (Some Hclose) in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as (x1 x2 x3 x4 x5) pat
| _ => revert x; intros x1; iDestructHyp H as ( x2 x3 x4 x5) pat
end).
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) constr(Hclose) :=
iInvCore N as (Some Hclose) in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as (x1 x2 x3 x4 x5 x6) pat
| _ => revert x; intros x1; iDestructHyp H as ( x2 x3 x4 x5 x6) pat
end).
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
constr(pat) constr(Hclose) :=
iInvCore N as (Some Hclose) in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as (x1 x2 x3 x4 x5 x6 x7) pat
| _ => revert x; intros x1; iDestructHyp H as ( x2 x3 x4 x5 x6 x7) pat
end).
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) ")" constr(pat) constr(Hclose) :=
iInvCore N as (Some Hclose) in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as (x1 x2 x3 x4 x5 x6 x7 x8) pat
| _ => revert x; intros x1; iDestructHyp H as ( x2 x3 x4 x5 x6 x7 x8) pat
end).
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) simple_intropattern(x9) ")" constr(pat) constr(Hclose) :=
iInvCore N as (Some Hclose) in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as (x1 x2 x3 x4 x5 x6 x7 x8 x9) pat
| _ => revert x; intros x1; iDestructHyp H as ( x2 x3 x4 x5 x6 x7 x8 x9) pat
end).
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) simple_intropattern(x9) simple_intropattern(x10) ")"
constr(pat) constr(Hclose) :=
iInvCore N as (Some Hclose) in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) pat
| _ => revert x; intros x1; iDestructHyp H as ( x2 x3 x4 x5 x6 x7 x8 x9 x10) pat
end).
(* Without both *)
Tactic Notation "iInv" constr(N) "as" constr(pat) :=
......@@ -2460,6 +2635,59 @@ Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
| unit => destruct x as []; iDestructHyp H as (x1 x2 x3 x4) pat
| _ => revert x; intros x1; iDestructHyp H as ( x2 x3 x4) pat
end).
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) ")" constr(pat) :=
iInvCore N in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as (x1 x2 x3 x4 x5) pat
| _ => revert x; intros x1; iDestructHyp H as ( x2 x3 x4 x5) pat
end).
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
iInvCore N in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as (x1 x2 x3 x4 x5 x6) pat
| _ => revert x; intros x1; iDestructHyp H as ( x2 x3 x4 x5 x6) pat
end).
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
constr(pat) :=
iInvCore N in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as (x1 x2 x3 x4 x5 x6 x7) pat
| _ => revert x; intros x1; iDestructHyp H as ( x2 x3 x4 x5 x6 x7) pat
end).
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) ")" constr(pat) :=
iInvCore N in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as (x1 x2 x3 x4 x5 x6 x7 x8) pat
| _ => revert x; intros x1; iDestructHyp H as ( x2 x3 x4 x5 x6 x7 x8) pat
end).
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) simple_intropattern(x9) ")" constr(pat) :=
iInvCore N in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as (x1 x2 x3 x4 x5 x6 x7 x8 x9) pat
| _ => revert x; intros x1; iDestructHyp H as ( x2 x3 x4 x5 x6 x7 x8 x9) pat
end).
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) simple_intropattern(x9) simple_intropattern(x10) ")"
constr(pat) :=
iInvCore N in
(fun x H => lazymatch type of x with
| unit => destruct x as []; iDestructHyp H as (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) pat
| _ => revert x; intros x1; iDestructHyp H as ( x2 x3 x4 x5 x6 x7 x8 x9 x10) pat
end).
(** Miscellaneous *)
Tactic Notation "iAccu" :=
......
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