Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Marianna Rapoport
iris-coq
Commits
fba57127
Commit
fba57127
authored
Jul 05, 2016
by
Robbert Krebbers
Browse files
Rename fallthrough (instances) into default.
parent
79d0d5fd
Changes
4
Hide whitespace changes
Inline
Side-by-side
prelude/collections.v
View file @
fba57127
...
...
@@ -140,7 +140,7 @@ Hint Mode SetUnfold + - : typeclass_instances.
Class
SetUnfoldSimpl
(
P
Q
:
Prop
)
:
=
{
set_unfold_simpl
:
SetUnfold
P
Q
}.
Hint
Extern
0
(
SetUnfoldSimpl
_
_
)
=>
csimpl
;
constructor
:
typeclass_instances
.
Instance
set_unfold_fa
l
lt
hrough
P
:
SetUnfold
P
P
|
1000
.
done
.
Qed
.
Instance
set_unfold_
de
fa
u
lt
P
:
SetUnfold
P
P
|
1000
.
done
.
Qed
.
Definition
set_unfold_1
`
{
SetUnfold
P
Q
}
:
P
→
Q
:
=
proj1
(
set_unfold
P
Q
).
Definition
set_unfold_2
`
{
SetUnfold
P
Q
}
:
Q
→
P
:
=
proj2
(
set_unfold
P
Q
).
...
...
proofmode/classes.v
View file @
fba57127
...
...
@@ -52,7 +52,7 @@ Global Arguments into_later _ _ {_}.
Class
FromLater
(
P
Q
:
uPred
M
)
:
=
from_later
:
▷
Q
⊢
P
.
Global
Arguments
from_later
_
_
{
_
}.
Global
Instance
into_later_fa
l
lt
hrough
P
:
IntoLater
P
P
|
1000
.
Global
Instance
into_later_
de
fa
u
lt
P
:
IntoLater
P
P
|
1000
.
Proof
.
apply
later_intro
.
Qed
.
Global
Instance
into_later_later
P
:
IntoLater
(
▷
P
)
P
.
Proof
.
done
.
Qed
.
...
...
@@ -222,7 +222,7 @@ Global Instance make_sep_true_l P : MakeSep True P P.
Proof
.
by
rewrite
/
MakeSep
left_id
.
Qed
.
Global
Instance
make_sep_true_r
P
:
MakeSep
P
True
P
.
Proof
.
by
rewrite
/
MakeSep
right_id
.
Qed
.
Global
Instance
make_sep_fa
l
lt
hrough
P
Q
:
MakeSep
P
Q
(
P
★
Q
)
|
100
.
Global
Instance
make_sep_
de
fa
u
lt
P
Q
:
MakeSep
P
Q
(
P
★
Q
)
|
100
.
Proof
.
done
.
Qed
.
Global
Instance
frame_sep_l
R
P1
P2
Q
Q'
:
Frame
R
P1
Q
→
MakeSep
Q
P2
Q'
→
Frame
R
(
P1
★
P2
)
Q'
|
9
.
...
...
@@ -236,7 +236,7 @@ Global Instance make_and_true_l P : MakeAnd True P P.
Proof
.
by
rewrite
/
MakeAnd
left_id
.
Qed
.
Global
Instance
make_and_true_r
P
:
MakeAnd
P
True
P
.
Proof
.
by
rewrite
/
MakeAnd
right_id
.
Qed
.
Global
Instance
make_and_fa
l
lt
hrough
P
Q
:
MakeSep
P
Q
(
P
★
Q
)
|
100
.
Global
Instance
make_and_
de
fa
u
lt
P
Q
:
MakeSep
P
Q
(
P
★
Q
)
|
100
.
Proof
.
done
.
Qed
.
Global
Instance
frame_and_l
R
P1
P2
Q
Q'
:
Frame
R
P1
Q
→
MakeAnd
Q
P2
Q'
→
Frame
R
(
P1
∧
P2
)
Q'
|
9
.
...
...
@@ -250,7 +250,7 @@ Global Instance make_or_true_l P : MakeOr True P True.
Proof
.
by
rewrite
/
MakeOr
left_absorb
.
Qed
.
Global
Instance
make_or_true_r
P
:
MakeOr
P
True
True
.
Proof
.
by
rewrite
/
MakeOr
right_absorb
.
Qed
.
Global
Instance
make_or_fa
l
lt
hrough
P
Q
:
MakeOr
P
Q
(
P
∨
Q
)
|
100
.
Global
Instance
make_or_
de
fa
u
lt
P
Q
:
MakeOr
P
Q
(
P
∨
Q
)
|
100
.
Proof
.
done
.
Qed
.
Global
Instance
frame_or
R
P1
P2
Q1
Q2
Q
:
Frame
R
P1
Q1
→
Frame
R
P2
Q2
→
MakeOr
Q1
Q2
Q
→
Frame
R
(
P1
∨
P2
)
Q
.
...
...
@@ -259,7 +259,7 @@ Proof. rewrite /Frame /MakeOr => <- <- <-. by rewrite -sep_or_l. Qed.
Class
MakeLater
(
P
lP
:
uPred
M
)
:
=
make_later
:
▷
P
⊣
⊢
lP
.
Global
Instance
make_later_true
:
MakeLater
True
True
.
Proof
.
by
rewrite
/
MakeLater
later_True
.
Qed
.
Global
Instance
make_later_fa
l
lt
hrough
P
:
MakeLater
P
(
▷
P
)
|
100
.
Global
Instance
make_later_
de
fa
u
lt
P
:
MakeLater
P
(
▷
P
)
|
100
.
Proof
.
done
.
Qed
.
Global
Instance
frame_later
R
P
Q
Q'
:
...
...
proofmode/coq_tactics.v
View file @
fba57127
...
...
@@ -453,7 +453,7 @@ Qed.
Class
IntoAssert
(
P
:
uPred
M
)
(
Q
:
uPred
M
)
(
R
:
uPred
M
)
:
=
into_assert
:
R
★
(
P
-
★
Q
)
⊢
Q
.
Global
Arguments
into_assert
_
_
_
{
_
}.
Lemma
into_assert_fa
l
lt
hrough
P
Q
:
IntoAssert
P
Q
P
.
Lemma
into_assert_
de
fa
u
lt
P
Q
:
IntoAssert
P
Q
P
.
Proof
.
by
rewrite
/
IntoAssert
wand_elim_r
.
Qed
.
Lemma
tac_specialize_assert
Δ
Δ
'
Δ
1
Δ
2
'
j
q
lr
js
R
P1
P2
P1'
Q
:
...
...
proofmode/tactics.v
View file @
fba57127
...
...
@@ -194,7 +194,7 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
[
env_cbv
;
reflexivity
||
fail
"iSpecialize:"
H1
"not found"
|
solve_to_wand
H1
|
match
k
with
|
GoalStd
=>
apply
into_assert_fa
l
lt
hrough
|
GoalStd
=>
apply
into_assert_
de
fa
u
lt
|
GoalPvs
=>
apply
_
||
fail
"iSpecialize: cannot generate pvs goal"
end
|
env_cbv
;
reflexivity
||
fail
"iSpecialize:"
Hs
"not found"
...
...
@@ -752,7 +752,7 @@ Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
|
[
SGoal
?k
?lr
?Hs
]
=>
eapply
tac_assert
with
_
_
_
lr
Hs
H
Q
_;
(* (js:=Hs) (j:=H) (P:=Q) *)
[
match
k
with
|
GoalStd
=>
apply
into_assert_fa
l
lt
hrough
|
GoalStd
=>
apply
into_assert_
de
fa
u
lt
|
GoalPvs
=>
apply
_
||
fail
"iAssert: cannot generate pvs goal"
end
|
env_cbv
;
reflexivity
||
fail
"iAssert:"
Hs
"not found"
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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