Commit 82bd1095 authored by Robbert Krebbers's avatar Robbert Krebbers

Up to 15 binders for `iRevert`, `iRevertIntros`, `iInduction` and `iLöb`!

This commit made me cry...
parent 61da8709
......@@ -648,6 +648,10 @@ Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
ident(x5) ident(x6) ident(x7) ident(x8) ident(x9) ident(x10)
ident(x11) ident(x12) ident(x13) ident(x14) ")" :=
iForallRevert x14; iRevert ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
ident(x5) ident(x6) ident(x7) ident(x8) ident(x9) ident(x10)
ident(x11) ident(x12) ident(x13) ident(x14) ident(x15) ")" :=
iForallRevert x15; iRevert ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ).
Tactic Notation "iRevert" "(" ident(x1) ")" constr(Hs) :=
iRevert Hs; iRevert ( x1 ).
......@@ -693,6 +697,10 @@ Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
ident(x5) ident(x6) ident(x7) ident(x8) ident(x9) ident(x10)
ident(x11) ident(x12) ident(x13) ident(x14) ")" constr(Hs) :=
iRevert Hs; iRevert ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ).
Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
ident(x5) ident(x6) ident(x7) ident(x8) ident(x9) ident(x10)
ident(x11) ident(x12) ident(x13) ident(x14) ident(x15) ")" constr(Hs) :=
iRevert Hs; iRevert ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ).
(** * The specialize and pose proof tactics *)
Record iTrm {X As S} :=
......@@ -1512,6 +1520,13 @@ Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
simple_intropattern(x9) simple_intropattern(x10) simple_intropattern(x11)
simple_intropattern(x12) simple_intropattern(x13) simple_intropattern(x14) ")" :=
iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ); iIntro ( x14 ).
Tactic Notation "iIntros" "(" 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) simple_intropattern(x11)
simple_intropattern(x12) simple_intropattern(x13) simple_intropattern(x14)
simple_intropattern(x15) ")" :=
iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ); iIntro ( x15 ).
Tactic Notation "iIntros" "(" simple_intropattern(x1) ")" constr(p) :=
iIntros ( x1 ); iIntros p.
......@@ -1576,6 +1591,13 @@ Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
simple_intropattern(x12) simple_intropattern(x13) simple_intropattern(x14)
")" constr(p) :=
iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ); iIntros p.
Tactic Notation "iIntros" "(" 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) simple_intropattern(x11)
simple_intropattern(x12) simple_intropattern(x13) simple_intropattern(x14)
simple_intropattern(x15) ")" constr(p) :=
iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ); iIntros p.
Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1) ")" :=
iIntros p; iIntros ( x1 ).
......@@ -1640,6 +1662,13 @@ Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1)
simple_intropattern(x11) simple_intropattern(x12) simple_intropattern(x13)
simple_intropattern(x14) ")" :=
iIntros p; iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ).
Tactic Notation "iIntros" constr(p) "(" 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)
simple_intropattern(x11) simple_intropattern(x12) simple_intropattern(x13)
simple_intropattern(x14) simple_intropattern(x15) ")" :=
iIntros p; iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ).
Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1) ")" constr(p2) :=
iIntros p; iIntros ( x1 ); iIntros p2.
......@@ -1708,6 +1737,13 @@ Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1)
simple_intropattern(x11) simple_intropattern(x12) simple_intropattern(x13)
simple_intropattern(x14) ")" constr(p2) :=
iIntros p; iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ); iIntros p2.
Tactic Notation "iIntros" constr(p) "(" 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)
simple_intropattern(x11) simple_intropattern(x12) simple_intropattern(x13)
simple_intropattern(x14) simple_intropattern(x15) ")" constr(p2) :=
iIntros p; iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x15 ); iIntros p2.
(* Used for generalization in iInduction and iLöb *)
Tactic Notation "iRevertIntros" constr(Hs) "with" tactic3(tac) :=
......@@ -1775,6 +1811,11 @@ Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
ident(x12) ident(x13) ident(x14) ")" constr(Hs) "with" tactic3(tac):=
iRevertIntros Hs with (iRevert (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14);
tac; iIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)).
Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
ident(x5) ident(x6) ident(x7) ident(x8) ident(x9) ident(x10) ident(x11)
ident(x12) ident(x13) ident(x14) ident(x15) ")" constr(Hs) "with" tactic3(tac):=
iRevertIntros Hs with (iRevert (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x14);
tac; iIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)).
Tactic Notation "iRevertIntros" "with" tactic3(tac) :=
iRevertIntros "" with tac.
......@@ -1823,6 +1864,10 @@ Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
ident(x5) ident(x6) ident(x7) ident(x8) ident(x9) ident(x10) ident(x11)
ident(x12) ident(x13) ident(x14) ")" "with" tactic3(tac):=
iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) "" with tac.
Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
ident(x5) ident(x6) ident(x7) ident(x8) ident(x9) ident(x10) ident(x11)
ident(x12) ident(x13) ident(x14) ident(x15) ")" "with" tactic3(tac):=
iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) "" with tac.
(** * Destruct tactic *)
Class CopyDestruct {PROP : bi} (P : PROP).
......@@ -2114,6 +2159,13 @@ Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
iInductionRevert x "" with
(iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) "" with
(iInductionCore (induction x as pat) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ident(x6)
ident(x7) ident(x8) ident (x9) ident(x10) ident(x11) ident(x12) ident(x13)
ident(x14) ident(x15) ")" :=
iInductionRevert x "" with
(iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) "" with
(iInductionCore (induction x as pat) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" constr(Hs) :=
......@@ -2195,6 +2247,13 @@ Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
iInductionRevert x Hs with
(iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) "" with
(iInductionCore (induction x as pat) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"forall" "(" ident(x1) ident(x2) ident(x3) ident(x4) ident(x5) ident(x6)
ident(x7) ident(x8) ident (x9) ident(x10) ident(x11) ident(x12) ident(x13)
ident(x14) ident(x15) ")" constr(Hs) :=
iInductionRevert x Hs with
(iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) "" with
(iInductionCore (induction x as pat) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"using" uconstr(u) :=
......@@ -2279,6 +2338,13 @@ Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
iInductionRevert x "" with
(iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) "" with
(iInductionCore (induction x as pat using u) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"using" uconstr(u) "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4)
ident(x5) ident(x6) ident(x7) ident(x8) ident (x9) ident(x10) ident(x11)
ident(x12) ident(x13) ident(x14) ident(x15) ")" :=
iInductionRevert x "" with
(iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) "" with
(iInductionCore (induction x as pat using u) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"using" uconstr(u) "forall" constr(Hs) :=
......@@ -2362,6 +2428,13 @@ Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
iInductionRevert x Hs with
(iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) "" with
(iInductionCore (induction x as pat using u) as IH)).
Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
"using" uconstr(u) "forall" "(" ident(x1) ident(x2) ident(x3) ident(x4)
ident(x5) ident(x6) ident(x7) ident(x8) ident (x9) ident(x10) ident(x11)
ident(x12) ident(x13) ident(x14) ident(x15) ")" constr(Hs) :=
iInductionRevert x Hs with
(iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) "" with
(iInductionCore (induction x as pat using u) as IH)).
(** * Löb Induction *)
Tactic Notation "iLöbCore" "as" constr (IH) :=
......@@ -2437,6 +2510,11 @@ Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
ident(x10) ident(x11) ident(x12) ident(x13) ident(x14) ")" :=
iLöbRevert "" with
(iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) "" with (iLöbCore as IH)).
Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
ident(x3) ident(x4) ident(x5) ident(x6) ident(x7) ident(x8) ident(x9)
ident(x10) ident(x11) ident(x12) ident(x13) ident(x14) ident(x15) ")" :=
iLöbRevert "" with
(iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) "" with (iLöbCore as IH)).
Tactic Notation "iLöb" "as" constr (IH) "forall" constr(Hs) :=
iLöbRevert Hs with (iLöbCore as IH).
......@@ -2492,6 +2570,11 @@ Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
ident(x10) ident(x11) ident(x12) ident(x13) ident(x14) ")" constr(Hs) :=
iLöbRevert Hs with
(iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14) "" with (iLöbCore as IH)).
Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
ident(x3) ident(x4) ident(x5) ident(x6) ident(x7) ident(x8) ident(x9)
ident(x10) ident(x11) ident(x12) ident(x13) ident(x14) ident(x15) ")" constr(Hs) :=
iLöbRevert Hs with
(iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) "" with (iLöbCore as IH)).
(** * Assert *)
(* The argument [p] denotes whether [Q] is persistent. It can either be a
......
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