Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Rodolphe Lepigre
Iris
Commits
589e1fed
Commit
589e1fed
authored
Sep 07, 2019
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Add `iStopProof` tactic.
This commit closes issue
#265
.
parent
01db4f64
Changes
4
Show whitespace changes
Inline
Side-by-side
Showing
4 changed files
with
43 additions
and
10 deletions
+43
-10
theories/proofmode/coq_tactics.v
theories/proofmode/coq_tactics.v
+16
-2
theories/proofmode/environments.v
theories/proofmode/environments.v
+17
-5
theories/proofmode/ltac_tactics.v
theories/proofmode/ltac_tactics.v
+8
-2
theories/proofmode/reduction.v
theories/proofmode/reduction.v
+2
-1
No files found.
theories/proofmode/coq_tactics.v
View file @
589e1fed
...
...
@@ -12,14 +12,28 @@ Implicit Types Γ : env PROP.
Implicit
Types
Δ
:
envs
PROP
.
Implicit
Types
P
Q
:
PROP
.
(** *
Adequacy
*)
Lemma
tac_
adequate
P
:
envs_entails
(
Envs
Enil
Enil
1
)
P
→
P
.
(** *
Starting and stopping the proof mode
*)
Lemma
tac_
start
P
:
envs_entails
(
Envs
Enil
Enil
1
)
P
→
bi_emp_valid
P
.
Proof
.
rewrite
envs_entails_eq
!
of_envs_eq
/=.
rewrite
intuitionistically_True_emp
left_id
=><-.
apply
and_intro
=>
//.
apply
pure_intro
;
repeat
constructor
.
Qed
.
Lemma
tac_stop
Δ
P
:
(
match
env_intuitionistic
Δ
,
env_spatial
Δ
with
|
Enil
,
Γ
s
=>
env_to_prop
Γ
s
|
Γ
p
,
Enil
=>
□
env_to_prop_and
Γ
p
|
Γ
p
,
Γ
s
=>
□
env_to_prop_and
Γ
p
∗
env_to_prop
Γ
s
end
%
I
⊢
P
)
→
envs_entails
Δ
P
.
Proof
.
rewrite
envs_entails_eq
!
of_envs_eq
.
intros
<-.
rewrite
and_elim_r
-
env_to_prop_and_sound
-
env_to_prop_sound
.
destruct
(
env_intuitionistic
Δ
),
(
env_spatial
Δ
)
;
by
rewrite
/=
?intuitionistically_True_emp
?left_id
?right_id
.
Qed
.
(** * Basic rules *)
Lemma
tac_eval
Δ
Q
Q'
:
(
∀
(
Q''
:
=
Q'
),
Q''
⊢
Q
)
→
(* We introduce [Q''] as a let binding so that
...
...
theories/proofmode/environments.v
View file @
589e1fed
...
...
@@ -364,11 +364,15 @@ Definition envs_split {PROP} (d : direction)
''
(
Δ
1
,
Δ
2
)
←
envs_split_go
js
Δ
(
envs_clear_spatial
Δ
)
;
if
d
is
Right
then
Some
(
Δ
1
,
Δ
2
)
else
Some
(
Δ
2
,
Δ
1
).
Fixpoint
env_to_prop_go
{
PROP
:
bi
}
(
acc
:
PROP
)
(
Γ
:
env
PROP
)
:
PROP
:
=
match
Γ
with
Enil
=>
acc
|
Esnoc
Γ
_
P
=>
env_to_prop_go
(
P
∗
acc
)%
I
Γ
end
.
Definition
env_to_prop
{
PROP
:
bi
}
(
Γ
:
env
PROP
)
:
PROP
:
=
let
fix
aux
Γ
acc
:
=
match
Γ
with
Enil
=>
acc
|
Esnoc
Γ
_
P
=>
aux
Γ
(
P
∗
acc
)%
I
end
in
match
Γ
with
Enil
=>
emp
%
I
|
Esnoc
Γ
_
P
=>
aux
Γ
P
end
.
match
Γ
with
Enil
=>
emp
%
I
|
Esnoc
Γ
_
P
=>
env_to_prop_go
P
Γ
end
.
Fixpoint
env_to_prop_and_go
{
PROP
:
bi
}
(
acc
:
PROP
)
(
Γ
:
env
PROP
)
:
PROP
:
=
match
Γ
with
Enil
=>
acc
|
Esnoc
Γ
_
P
=>
env_to_prop_and_go
(
P
∧
acc
)%
I
Γ
end
.
Definition
env_to_prop_and
{
PROP
:
bi
}
(
Γ
:
env
PROP
)
:
PROP
:
=
match
Γ
with
Enil
=>
True
%
I
|
Esnoc
Γ
_
P
=>
env_to_prop_and_go
P
Γ
end
.
Section
envs
.
Context
{
PROP
:
bi
}.
...
...
@@ -767,7 +771,15 @@ Qed.
Lemma
env_to_prop_sound
Γ
:
env_to_prop
Γ
⊣
⊢
[
∗
]
Γ
.
Proof
.
destruct
Γ
as
[|
Γ
?
P
]
;
simpl
;
first
done
.
destruct
Γ
as
[|
Γ
i
P
]
;
simpl
;
first
done
.
revert
P
.
induction
Γ
as
[|
Γ
IH
?
Q
]=>
P
;
simpl
.
-
by
rewrite
right_id
.
-
rewrite
/=
IH
(
comm
_
Q
_
)
assoc
.
done
.
Qed
.
Lemma
env_to_prop_and_sound
Γ
:
env_to_prop_and
Γ
⊣
⊢
[
∧
]
Γ
.
Proof
.
destruct
Γ
as
[|
Γ
i
P
]
;
simpl
;
first
done
.
revert
P
.
induction
Γ
as
[|
Γ
IH
?
Q
]=>
P
;
simpl
.
-
by
rewrite
right_id
.
-
rewrite
/=
IH
(
comm
_
Q
_
)
assoc
.
done
.
...
...
theories/proofmode/ltac_tactics.v
View file @
589e1fed
...
...
@@ -71,7 +71,7 @@ Tactic Notation "iStartProof" :=
| |- envs_entails _ _ => idtac
| |- ?φ => notypeclasses refine (as_emp_valid_2 φ _ _);
[iSolveTC || fail "iStartProof: not a BI assertion"
|
apply
tac_
adequate
]
|apply tac_
start
]
end.
(* Same as above, with 2 differences :
...
...
@@ -92,7 +92,13 @@ Tactic Notation "iStartProof" uconstr(PROP) :=
to find the corresponding bi. *)
| |- ?φ => notypeclasses refine ((λ P : PROP, @as_emp_valid_2 φ _ P) _ _ _);
[iSolveTC || fail "iStartProof: not a BI assertion"
|
apply
tac_adequate
]
|apply tac_start]
end.
Tactic Notation "iStopProof" :=
lazymatch goal with
| |- envs_entails _ _ => apply tac_stop; pm_reduce
| |- _ => fail "iStopProof: proofmode not started"
end.
(** * Generate a fresh identifier *)
...
...
theories/proofmode/reduction.v
View file @
589e1fed
...
...
@@ -13,7 +13,8 @@ Declare Reduction pm_eval := cbv [
envs_lookup
envs_lookup_delete
envs_delete
envs_snoc
envs_app
envs_simple_replace
envs_replace
envs_split
envs_clear_spatial
envs_clear_intuitionistic
envs_incr_counter
envs_split_go
envs_split
env_to_prop
envs_split_go
envs_split
env_to_prop_go
env_to_prop
env_to_prop_and_go
env_to_prop_and
(* PM option combinators *)
pm_option_bind
pm_from_option
pm_option_fun
].
...
...
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