Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
I
Iris
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
0
Issues
0
List
Boards
Labels
Service Desk
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Rodolphe Lepigre
Iris
Commits
cec53bd4
Verified
Commit
cec53bd4
authored
Jun 14, 2019
by
Paolo G. Giarrusso
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
tactic>tactic3 for remaining tactics
parent
c9418149
Changes
3
Hide whitespace changes
Inline
Sidebyside
Showing
3 changed files
with
34 additions
and
34 deletions
+34
34
tests/proofmode.ref
tests/proofmode.ref
+18
18
tests/proofmode_iris.ref
tests/proofmode_iris.ref
+6
6
theories/proofmode/ltac_tactics.v
theories/proofmode/ltac_tactics.v
+10
10
No files found.
tests/proofmode.ref
View file @
cec53bd4
...
...
@@ 443,8 +443,8 @@ Tactic failure: iModIntro: spatial context is nonempty.
: string
The command has indeed failed with message:
In nested Ltac calls to "iDestruct (open_constr) as (constr)",
"iDestructCore (open_constr) as (constr) (tactic)" and
"iDestructCore (open_constr) as (constr) (tactic)", last call failed.
"iDestructCore (open_constr) as (constr) (tactic
3
)" and
"iDestructCore (open_constr) as (constr) (tactic
3
)", last call failed.
Tactic failure: iDestruct: "HQ" not found.
"iIntros_dup_name"
: string
...
...
@@ 553,14 +553,14 @@ Tactic failure: iStartProof: not a BI assertion.
: string
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
"iPoseProofCoreLem (constr) as (constr) before_tc (tactic)" and
"iPoseProofCore (open_constr) as (constr) (constr) (tactic
3
)",
"iPoseProofCoreLem (constr) as (constr) before_tc (tactic
3
)" and
"<iris.proofmode.ltac_tactics.iIntoEmpValid>", last call failed.
Tactic failure: iPoseProof: not a BI assertion.
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
"iPoseProofCoreLem (constr) as (constr) before_tc (tactic)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic
3
)",
"iPoseProofCoreLem (constr) as (constr) before_tc (tactic
3
)",
"tac" (bound to spec_tac ltac:(()); [ ..  tac Htmp ]),
"tac" (bound to spec_tac ltac:(()); [ ..  tac Htmp ]),
"tac" (bound to fun H => iDestructHyp H as pat),
...
...
@@ 573,15 +573,15 @@ Tactic failure: iRename: "H" not fresh.
: string
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)" and
"iPoseProofCore (open_constr) as (constr) (constr) (tactic
3
)" and
"iPoseProofCoreHyp (constr) as (constr)", last call failed.
Tactic failure: iPoseProof: "Hx" not found.
"iPoseProof_not_found_fail2"
: string
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
"iPoseProofCoreLem (constr) as (constr) before_tc (tactic)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic
3
)",
"iPoseProofCoreLem (constr) as (constr) before_tc (tactic
3
)",
"tac" (bound to spec_tac ltac:(()); [ ..  tac Htmp ]),
"tac" (bound to spec_tac ltac:(()); [ ..  tac Htmp ]),
"spec_tac" (bound to
...
...
@@ 616,9 +616,9 @@ Tactic failure: iElaborateSelPat: "H" not found.
: string
The command has indeed failed with message:
In nested Ltac calls to "iDestruct (open_constr) as (constr)",
"iDestructCore (open_constr) as (constr) (tactic)",
"iDestructCore (open_constr) as (constr) (tactic)",
"iDestructCore (open_constr) as (constr) (tactic)",
"iDestructCore (open_constr) as (constr) (tactic
3
)",
"iDestructCore (open_constr) as (constr) (tactic
3
)",
"iDestructCore (open_constr) as (constr) (tactic
3
)",
"tac" (bound to fun H => iDestructHyp H as pat),
"iDestructHyp (constr) as (constr)",
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>" and
...
...
@@ 627,9 +627,9 @@ Tactic failure: iDestruct: "{HP}"
should contain exactly one proper introduction pattern.
The command has indeed failed with message:
In nested Ltac calls to "iDestruct (open_constr) as (constr)",
"iDestructCore (open_constr) as (constr) (tactic)",
"iDestructCore (open_constr) as (constr) (tactic)",
"iDestructCore (open_constr) as (constr) (tactic)",
"iDestructCore (open_constr) as (constr) (tactic
3
)",
"iDestructCore (open_constr) as (constr) (tactic
3
)",
"iDestructCore (open_constr) as (constr) (tactic
3
)",
"tac" (bound to fun H => iDestructHyp H as pat),
"iDestructHyp (constr) as (constr)",
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>" and
...
...
@@ 648,7 +648,7 @@ Tactic failure: iOrDestruct: "H1" or "H'" not fresh.
: string
The command has indeed failed with message:
In nested Ltac calls to "iApply (open_constr)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic
3
)",
"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
failed.
Tactic failure: iApply: cannot apply P.
...
...
@@ 656,7 +656,7 @@ Tactic failure: iApply: cannot apply P.
: string
The command has indeed failed with message:
In nested Ltac calls to "iApply (open_constr)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic
3
)",
"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
failed.
Tactic failure: iApply: Q
...
...
@@ 665,7 +665,7 @@ not absorbing and the remaining hypotheses not affine.
: string
The command has indeed failed with message:
In nested Ltac calls to "iApply (open_constr)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic
3
)",
"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
failed.
Tactic failure: iApply: Q
...
...
tests/proofmode_iris.ref
View file @
cec53bd4
...
...
@@ 111,20 +111,20 @@
: string
The command has indeed failed with message:
In nested Ltac calls to "iInv (constr) as (constr)",
"iInvCore (constr) in (tactic)" and
"iInvCore (constr) with (constr) as (open_constr) in (tactic)", last call
"iInvCore (constr) in (tactic
3
)" and
"iInvCore (constr) with (constr) as (open_constr) in (tactic
3
)", last call
failed.
Tactic failure: iInv: selector 34 is not of the right type .
The command has indeed failed with message:
In nested Ltac calls to "iInv (constr) as (constr)",
"iInvCore (constr) in (tactic)" and
"iInvCore (constr) with (constr) as (open_constr) in (tactic)", last call
"iInvCore (constr) in (tactic
3
)" and
"iInvCore (constr) with (constr) as (open_constr) in (tactic
3
)", last call
failed.
Tactic failure: iInv: invariant nroot not found.
The command has indeed failed with message:
In nested Ltac calls to "iInv (constr) as (constr)",
"iInvCore (constr) in (tactic)" and
"iInvCore (constr) with (constr) as (open_constr) in (tactic)", last call
"iInvCore (constr) in (tactic
3
)" and
"iInvCore (constr) with (constr) as (open_constr) in (tactic
3
)", last call
failed.
Tactic failure: iInv: invariant "H2" not found.
"test_iInv"
...
...
theories/proofmode/ltac_tactics.v
View file @
cec53bd4
...
...
@@ 726,7 +726,7 @@ Tactic Notation "iPoseProofCoreHyp" constr(H) "as" constr(Hnew) :=
end
.
Tactic
Notation
"iPoseProofCoreLem"
constr(lem) "as" constr(Hnew) "before_tc" tactic(tac) :=
constr
(
lem
)
"as"
constr
(
Hnew
)
"before_tc"
tactic
3
(
tac
)
:
=
eapply
tac_pose_proof
with
Hnew
_;
(* (j:=H) *)
[
iIntoEmpValid
lem

pm_reduce
;
...
...
@@ 1015,7 +1015,7 @@ Both variants of [lazy_tc] are used in other tactics that build on top of
because it may be not possible to eliminate logical connectives before all
type class constraints have been resolved. *)
Tactic
Notation
"iPoseProofCore"
open_constr
(
lem
)
"as" constr(p) constr(lazy_tc) tactic(tac) :=
"as"
constr
(
p
)
constr
(
lazy_tc
)
tactic
3
(
tac
)
:
=
iStartProof
;
let
Htmp
:
=
iFresh
in
let
t
:
=
lazymatch
lem
with
ITrm
?t
?xs
?pat
=>
t

_
=>
lem
end
in
...
...
@@ 1710,7 +1710,7 @@ Instance copy_destruct_affinely {PROP : bi} (P : PROP) :
Instance
copy_destruct_persistently
{
PROP
:
bi
}
(
P
:
PROP
)
:
CopyDestruct
P
→
CopyDestruct
(<
pers
>
P
)
:
=
{}.
Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
Tactic
Notation
"iDestructCore"
open_constr
(
lem
)
"as"
constr
(
p
)
tactic
3
(
tac
)
:
=
let
ident
:
=
lazymatch
type
of
lem
with

ident
=>
constr
:
(
Some
lem
)
...
...
@@ 1869,7 +1869,7 @@ result in the following actions:
 Introduce the spatial hypotheses and intuitionistic hypotheses involving [x]
 Introduce the proofmode hypotheses [Hs]
*)
Tactic Notation "iInductionCore" tactic(tac) "as" constr(IH) :=
Tactic
Notation
"iInductionCore"
tactic
3
(
tac
)
"as"
constr
(
IH
)
:
=
let
rec
fix_ihs
rev_tac
:
=
lazymatch
goal
with

H
:
context
[
envs_entails
_
_
]

_
=>
...
...
@@ 2144,7 +2144,7 @@ Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
Boolean or an introduction pattern, which will be coerced into [true] if it
only contains `#` or `%` patterns at the toplevel, and [false] otherwise. *)
Tactic
Notation
"iAssertCore"
open_constr
(
Q
)
"with" constr(Hs) "as" constr(p) tactic(tac) :=
"with"
constr
(
Hs
)
"as"
constr
(
p
)
tactic
3
(
tac
)
:
=
iStartProof
;
let
pats
:
=
spec_pat
.
parse
Hs
in
lazymatch
pats
with
...
...
@@ 2156,7 +2156,7 @@ Tactic Notation "iAssertCore" open_constr(Q)
[
pm_reduce
;
iSpecializeCore
H
with
hnil
pats
as
p
;
[..
tac
H
]].
Tactic Notation "iAssertCore" open_constr(Q) "as" constr(p) tactic(tac) :=
Tactic
Notation
"iAssertCore"
open_constr
(
Q
)
"as"
constr
(
p
)
tactic
3
(
tac
)
:
=
let
p
:
=
intro_pat_intuitionistic
p
in
lazymatch
p
with

true
=>
iAssertCore
Q
with
"[#]"
as
p
tac
...
...
@@ 2314,7 +2314,7 @@ Tactic Notation "iAssumptionInv" constr(N) :=
(* The argument [select] is the namespace [N] or hypothesis name ["H"] of the
invariant. *)
Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" open_constr(Hclose) "in" tactic(tac) :=
Tactic
Notation
"iInvCore"
constr
(
select
)
"with"
constr
(
pats
)
"as"
open_constr
(
Hclose
)
"in"
tactic
3
(
tac
)
:
=
iStartProof
;
let
pats
:
=
spec_pat
.
parse
pats
in
lazymatch
pats
with
...
...
@@ 2361,13 +2361,13 @@ Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" open_constr(H
)].
(* Without closing view shift *)
Tactic Notation "iInvCore" constr(N) "with" constr(pats) "in" tactic(tac) :=
Tactic
Notation
"iInvCore"
constr
(
N
)
"with"
constr
(
pats
)
"in"
tactic
3
(
tac
)
:
=
iInvCore
N
with
pats
as
(@
None
string
)
in
ltac
:
(
tac
).
(* Without pattern *)
Tactic Notation "iInvCore" constr(N) "as" constr(Hclose) "in" tactic(tac) :=
Tactic
Notation
"iInvCore"
constr
(
N
)
"as"
constr
(
Hclose
)
"in"
tactic
3
(
tac
)
:
=
iInvCore
N
with
"[$]"
as
Hclose
in
ltac
:
(
tac
).
(* Without both *)
Tactic Notation "iInvCore" constr(N) "in" tactic(tac) :=
Tactic
Notation
"iInvCore"
constr
(
N
)
"in"
tactic
3
(
tac
)
:
=
iInvCore
N
with
"[$]"
as
(@
None
string
)
in
ltac
:
(
tac
).
(* With everything *)
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment