Commit e5c102c3 authored by Robbert Krebbers's avatar Robbert Krebbers

Version of iPoseProof with intro pattern.

parent 7dec931b
...@@ -39,8 +39,10 @@ Context management ...@@ -39,8 +39,10 @@ Context management
implications/wands of a hypothesis whose conclusion is persistent. In this implications/wands of a hypothesis whose conclusion is persistent. In this
case, all hypotheses can be used for proving the premises, as well as for case, all hypotheses can be used for proving the premises, as well as for
the resulting goal. the resulting goal.
- `iPoseProof pm_trm as "H"` : put `pm_trm` into the context as a new hypothesis - `iPoseProof pm_trm as (x1 ... xn) "ipat"` : put `pm_trm` into the context and
`H`. eliminates it. This tactic is essentially the same as `iDestruct` with the
difference that when `pm_trm` is a non-univerisally quantified spatial
hypothesis, it will not throw the hypothesis away.
- `iAssert P with "spat" as "ipat"` : generates a new subgoal `P` and adds the - `iAssert P with "spat" as "ipat"` : generates a new subgoal `P` and adds the
hypothesis `P` to the current goal. The specialization pattern `spat` hypothesis `P` to the current goal. The specialization pattern `spat`
specifies which hypotheses will be consumed by proving `P`. The introduction specifies which hypotheses will be consumed by proving `P`. The introduction
......
...@@ -554,9 +554,6 @@ Tactic Notation "iPoseProofCore" open_constr(lem) ...@@ -554,9 +554,6 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
| false => go spec_tac; last (tac Htmp) | false => go spec_tac; last (tac Htmp)
end. end.
Tactic Notation "iPoseProof" open_constr(lem) "as" constr(H) :=
iPoseProofCore lem as false false (fun Htmp => iRename Htmp into H).
(** * Apply *) (** * Apply *)
Tactic Notation "iApply" open_constr(lem) := Tactic Notation "iApply" open_constr(lem) :=
let rec go H := first let rec go H := first
...@@ -1172,6 +1169,40 @@ Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1) ...@@ -1172,6 +1169,40 @@ Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
Tactic Notation "iDestruct" open_constr(lem) "as" "%" simple_intropattern(pat) := Tactic Notation "iDestruct" open_constr(lem) "as" "%" simple_intropattern(pat) :=
iDestructCore lem as true (fun H => iPure H as pat). iDestructCore lem as true (fun H => iPure H as pat).
Tactic Notation "iPoseProof" open_constr(lem) "as" constr(pat) :=
iPoseProofCore lem as pat false (fun H => iDestructHyp H as pat).
Tactic Notation "iPoseProof" open_constr(lem) "as" "(" simple_intropattern(x1) ")"
constr(pat) :=
iPoseProofCore lem as pat false (fun H => iDestructHyp H as ( x1 ) pat).
Tactic Notation "iPoseProof" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) ")" constr(pat) :=
iPoseProofCore lem as pat false (fun H => iDestructHyp H as ( x1 x2 ) pat).
Tactic Notation "iPoseProof" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
iPoseProofCore lem as pat false (fun H => iDestructHyp H as ( x1 x2 x3 ) pat).
Tactic Notation "iPoseProof" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
constr(pat) :=
iPoseProofCore lem as pat false (fun H => iDestructHyp H as ( x1 x2 x3 x4 ) pat).
Tactic Notation "iPoseProof" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) ")" constr(pat) :=
iPoseProofCore lem as pat false (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 ) 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) ")" constr(pat) :=
iPoseProofCore lem as pat false (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) 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) ")"
constr(pat) :=
iPoseProofCore lem as pat false (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) 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) ")" constr(pat) :=
iPoseProofCore lem as pat false (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
(** * Induction *) (** * Induction *)
Tactic Notation "iInductionCore" constr(x) Tactic Notation "iInductionCore" constr(x)
"as" simple_intropattern(pat) constr(IH) := "as" simple_intropattern(pat) constr(IH) :=
......
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