Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Rodolphe Lepigre
Iris
Commits
e224e891
Commit
e224e891
authored
Oct 25, 2016
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Rename uPred_eq into uPred_internal_eq.
parent
260b7508
Changes
10
Hide whitespace changes
Inline
Side-by-side
Showing
10 changed files
with
49 additions
and
46 deletions
+49
-46
base_logic/base_logic.v
base_logic/base_logic.v
+1
-1
base_logic/derived.v
base_logic/derived.v
+16
-15
base_logic/primitive.v
base_logic/primitive.v
+14
-18
program_logic/boxes.v
program_logic/boxes.v
+3
-2
program_logic/iprop.v
program_logic/iprop.v
+1
-1
program_logic/saved_prop.v
program_logic/saved_prop.v
+1
-1
proofmode/class_instances.v
proofmode/class_instances.v
+5
-2
proofmode/coq_tactics.v
proofmode/coq_tactics.v
+6
-4
proofmode/tactics.v
proofmode/tactics.v
+1
-1
tests/proofmode.v
tests/proofmode.v
+1
-1
No files found.
base_logic/base_logic.v
View file @
e224e891
...
...
@@ -14,4 +14,4 @@ Hint Resolve and_intro and_elim_l' and_elim_r' : I.
Hint
Resolve
always_mono
:
I
.
Hint
Resolve
sep_elim_l'
sep_elim_r'
sep_mono
:
I
.
Hint
Immediate
True_intro
False_elim
:
I
.
Hint
Immediate
iff_refl
eq_refl'
:
I
.
Hint
Immediate
iff_refl
internal_
eq_refl'
:
I
.
base_logic/derived.v
View file @
e224e891
...
...
@@ -241,13 +241,13 @@ Proof.
-
apply
exist_elim
=>
x
.
eauto
using
pure_mono
.
Qed
.
Lemma
eq_refl'
{
A
:
cofeT
}
(
a
:
A
)
P
:
P
⊢
a
≡
a
.
Proof
.
rewrite
(
True_intro
P
).
apply
eq_refl
.
Qed
.
Hint
Resolve
eq_refl'
.
Lemma
equiv_eq
{
A
:
cofeT
}
P
(
a
b
:
A
)
:
a
≡
b
→
P
⊢
a
≡
b
.
Lemma
internal_
eq_refl'
{
A
:
cofeT
}
(
a
:
A
)
P
:
P
⊢
a
≡
a
.
Proof
.
rewrite
(
True_intro
P
).
apply
internal_
eq_refl
.
Qed
.
Hint
Resolve
internal_
eq_refl'
.
Lemma
equiv_
internal_
eq
{
A
:
cofeT
}
P
(
a
b
:
A
)
:
a
≡
b
→
P
⊢
a
≡
b
.
Proof
.
by
intros
->.
Qed
.
Lemma
eq_sym
{
A
:
cofeT
}
(
a
b
:
A
)
:
a
≡
b
⊢
b
≡
a
.
Proof
.
apply
(
eq_rewrite
a
b
(
λ
b
,
b
≡
a
)%
I
)
;
auto
.
solve_proper
.
Qed
.
Lemma
internal_
eq_sym
{
A
:
cofeT
}
(
a
b
:
A
)
:
a
≡
b
⊢
b
≡
a
.
Proof
.
apply
(
internal_
eq_rewrite
a
b
(
λ
b
,
b
≡
a
)%
I
)
;
auto
.
solve_proper
.
Qed
.
Lemma
pure_alt
φ
:
■
φ
⊣
⊢
∃
_
:
φ
,
True
.
Proof
.
...
...
@@ -280,9 +280,10 @@ Proof.
Qed
.
Lemma
equiv_iff
P
Q
:
(
P
⊣
⊢
Q
)
→
True
⊢
P
↔
Q
.
Proof
.
intros
->
;
apply
iff_refl
.
Qed
.
Lemma
eq_iff
P
Q
:
P
≡
Q
⊢
P
↔
Q
.
Lemma
internal_
eq_iff
P
Q
:
P
≡
Q
⊢
P
↔
Q
.
Proof
.
apply
(
eq_rewrite
P
Q
(
λ
Q
,
P
↔
Q
))%
I
;
first
solve_proper
;
auto
using
iff_refl
.
apply
(
internal_eq_rewrite
P
Q
(
λ
Q
,
P
↔
Q
))%
I
;
first
solve_proper
;
auto
using
iff_refl
.
Qed
.
(* Derived BI Stuff *)
...
...
@@ -445,12 +446,12 @@ Proof.
apply
impl_intro_l
;
rewrite
-
always_and
.
apply
always_mono
,
impl_elim
with
P
;
auto
.
Qed
.
Lemma
always_eq
{
A
:
cofeT
}
(
a
b
:
A
)
:
□
(
a
≡
b
)
⊣
⊢
a
≡
b
.
Lemma
always_
internal_
eq
{
A
:
cofeT
}
(
a
b
:
A
)
:
□
(
a
≡
b
)
⊣
⊢
a
≡
b
.
Proof
.
apply
(
anti_symm
(
⊢
))
;
auto
using
always_elim
.
apply
(
eq_rewrite
a
b
(
λ
b
,
□
(
a
≡
b
))%
I
)
;
auto
.
apply
(
internal_
eq_rewrite
a
b
(
λ
b
,
□
(
a
≡
b
))%
I
)
;
auto
.
{
intros
n
;
solve_proper
.
}
rewrite
-(
eq_refl
a
)
always_pure
;
auto
.
rewrite
-(
internal_
eq_refl
a
)
always_pure
;
auto
.
Qed
.
Lemma
always_and_sep
P
Q
:
□
(
P
∧
Q
)
⊣
⊢
□
(
P
★
Q
).
...
...
@@ -692,8 +693,8 @@ Global Instance ownM_timeless (a : M) : Timeless a → TimelessP (uPred_ownM a).
Proof
.
intros
?.
rewrite
/
TimelessP
later_ownM
.
apply
exist_elim
=>
b
.
rewrite
(
timelessP
(
a
≡
b
))
(
except_0_intro
(
uPred_ownM
b
))
-
except_0_and
.
apply
except_0_mono
.
rewrite
eq_sym
.
apply
(
eq_rewrite
b
a
(
uPred_ownM
))
;
first
apply
_;
auto
.
apply
except_0_mono
.
rewrite
internal_
eq_sym
.
apply
(
internal_
eq_rewrite
b
a
(
uPred_ownM
))
;
first
apply
_;
auto
.
Qed
.
(* Persistence *)
...
...
@@ -716,9 +717,9 @@ Proof. by intros; rewrite /PersistentP always_forall; apply forall_mono. Qed.
Global
Instance
exist_persistent
{
A
}
(
Ψ
:
A
→
uPred
M
)
:
(
∀
x
,
PersistentP
(
Ψ
x
))
→
PersistentP
(
∃
x
,
Ψ
x
).
Proof
.
by
intros
;
rewrite
/
PersistentP
always_exist
;
apply
exist_mono
.
Qed
.
Global
Instance
eq_persistent
{
A
:
cofeT
}
(
a
b
:
A
)
:
Global
Instance
internal_
eq_persistent
{
A
:
cofeT
}
(
a
b
:
A
)
:
PersistentP
(
a
≡
b
:
uPred
M
)%
I
.
Proof
.
by
intros
;
rewrite
/
PersistentP
always_eq
.
Qed
.
Proof
.
by
intros
;
rewrite
/
PersistentP
always_
internal_
eq
.
Qed
.
Global
Instance
cmra_valid_persistent
{
A
:
cmraT
}
(
a
:
A
)
:
PersistentP
(
✓
a
:
uPred
M
)%
I
.
Proof
.
by
intros
;
rewrite
/
PersistentP
always_cmra_valid
.
Qed
.
...
...
base_logic/primitive.v
View file @
e224e891
...
...
@@ -58,12 +58,13 @@ Definition uPred_exist_aux : { x | x = @uPred_exist_def }. by eexists. Qed.
Definition
uPred_exist
{
M
A
}
:
=
proj1_sig
uPred_exist_aux
M
A
.
Definition
uPred_exist_eq
:
@
uPred_exist
=
@
uPred_exist_def
:
=
proj2_sig
uPred_exist_aux
.
Program
Definition
uPred_eq_def
{
M
}
{
A
:
cofeT
}
(
a1
a2
:
A
)
:
uPred
M
:
=
Program
Definition
uPred_
internal_
eq_def
{
M
}
{
A
:
cofeT
}
(
a1
a2
:
A
)
:
uPred
M
:
=
{|
uPred_holds
n
x
:
=
a1
≡
{
n
}
≡
a2
|}.
Solve
Obligations
with
naive_solver
eauto
2
using
(
dist_le
(
A
:
=
A
)).
Definition
uPred_eq_aux
:
{
x
|
x
=
@
uPred_eq_def
}.
by
eexists
.
Qed
.
Definition
uPred_eq
{
M
A
}
:
=
proj1_sig
uPred_eq_aux
M
A
.
Definition
uPred_eq_eq
:
@
uPred_eq
=
@
uPred_eq_def
:
=
proj2_sig
uPred_eq_aux
.
Definition
uPred_internal_eq_aux
:
{
x
|
x
=
@
uPred_internal_eq_def
}.
by
eexists
.
Qed
.
Definition
uPred_internal_eq
{
M
A
}
:
=
proj1_sig
uPred_internal_eq_aux
M
A
.
Definition
uPred_internal_eq_eq
:
@
uPred_internal_eq
=
@
uPred_internal_eq_def
:
=
proj2_sig
uPred_internal_eq_aux
.
Program
Definition
uPred_sep_def
{
M
}
(
P
Q
:
uPred
M
)
:
uPred
M
:
=
{|
uPred_holds
n
x
:
=
∃
x1
x2
,
x
≡
{
n
}
≡
x1
⋅
x2
∧
P
n
x1
∧
Q
n
x2
|}.
...
...
@@ -177,7 +178,7 @@ Notation "□ P" := (uPred_always P)
(
at
level
20
,
right
associativity
)
:
uPred_scope
.
Notation
"▷ P"
:
=
(
uPred_later
P
)
(
at
level
20
,
right
associativity
)
:
uPred_scope
.
Infix
"≡"
:
=
uPred_eq
:
uPred_scope
.
Infix
"≡"
:
=
uPred_
internal_
eq
:
uPred_scope
.
Notation
"✓ x"
:
=
(
uPred_cmra_valid
x
)
(
at
level
20
)
:
uPred_scope
.
Notation
"|==> Q"
:
=
(
uPred_bupd
Q
)
(
at
level
99
,
Q
at
level
200
,
format
"|==> Q"
)
:
uPred_scope
.
...
...
@@ -189,7 +190,7 @@ Notation "P ==★ Q" := (P -★ |==> Q)%I
Module
uPred_primitive
.
Definition
unseal
:
=
(
uPred_pure_eq
,
uPred_and_eq
,
uPred_or_eq
,
uPred_impl_eq
,
uPred_forall_eq
,
uPred_exist_eq
,
uPred_eq_eq
,
uPred_sep_eq
,
uPred_wand_eq
,
uPred_always_eq
,
uPred_exist_eq
,
uPred_
internal_
eq_eq
,
uPred_sep_eq
,
uPred_wand_eq
,
uPred_always_eq
,
uPred_later_eq
,
uPred_ownM_eq
,
uPred_cmra_valid_eq
,
uPred_bupd_eq
).
Ltac
unseal
:
=
rewrite
!
unseal
/=.
...
...
@@ -245,15 +246,15 @@ Proof.
Qed
.
Global
Instance
wand_proper
:
Proper
((
⊣
⊢
)
==>
(
⊣
⊢
)
==>
(
⊣
⊢
))
(@
uPred_wand
M
)
:
=
ne_proper_2
_
.
Global
Instance
eq_ne
(
A
:
cofeT
)
n
:
Proper
(
dist
n
==>
dist
n
==>
dist
n
)
(@
uPred_eq
M
A
).
Global
Instance
internal_
eq_ne
(
A
:
cofeT
)
n
:
Proper
(
dist
n
==>
dist
n
==>
dist
n
)
(@
uPred_
internal_
eq
M
A
).
Proof
.
intros
x
x'
Hx
y
y'
Hy
;
split
=>
n'
z
;
unseal
;
split
;
intros
;
simpl
in
*.
-
by
rewrite
-(
dist_le
_
_
_
_
Hx
)
-?(
dist_le
_
_
_
_
Hy
)
;
auto
.
-
by
rewrite
(
dist_le
_
_
_
_
Hx
)
?(
dist_le
_
_
_
_
Hy
)
;
auto
.
Qed
.
Global
Instance
eq_proper
(
A
:
cofeT
)
:
Proper
((
≡
)
==>
(
≡
)
==>
(
⊣
⊢
))
(@
uPred_eq
M
A
)
:
=
ne_proper_2
_
.
Global
Instance
internal_
eq_proper
(
A
:
cofeT
)
:
Proper
((
≡
)
==>
(
≡
)
==>
(
⊣
⊢
))
(@
uPred_
internal_
eq
M
A
)
:
=
ne_proper_2
_
.
Global
Instance
forall_ne
A
n
:
Proper
(
pointwise_relation
_
(
dist
n
)
==>
dist
n
)
(@
uPred_forall
M
A
).
Proof
.
...
...
@@ -355,21 +356,16 @@ Proof. unseal; split=> n x ??; by exists a. Qed.
Lemma
exist_elim
{
A
}
(
Φ
:
A
→
uPred
M
)
Q
:
(
∀
a
,
Φ
a
⊢
Q
)
→
(
∃
a
,
Φ
a
)
⊢
Q
.
Proof
.
unseal
;
intros
H
ΦΨ
;
split
=>
n
x
?
[
a
?]
;
by
apply
H
ΦΨ
with
a
.
Qed
.
Lemma
eq_refl
{
A
:
cofeT
}
(
a
:
A
)
:
True
⊢
a
≡
a
.
Lemma
internal_
eq_refl
{
A
:
cofeT
}
(
a
:
A
)
:
True
⊢
a
≡
a
.
Proof
.
unseal
;
by
split
=>
n
x
??
;
simpl
.
Qed
.
Lemma
eq_rewrite
{
A
:
cofeT
}
a
b
(
Ψ
:
A
→
uPred
M
)
P
Lemma
internal_
eq_rewrite
{
A
:
cofeT
}
a
b
(
Ψ
:
A
→
uPred
M
)
P
{
H
Ψ
:
∀
n
,
Proper
(
dist
n
==>
dist
n
)
Ψ
}
:
(
P
⊢
a
≡
b
)
→
(
P
⊢
Ψ
a
)
→
P
⊢
Ψ
b
.
Proof
.
unseal
;
intros
Hab
Ha
;
split
=>
n
x
??.
apply
H
Ψ
with
n
a
;
auto
.
-
by
symmetry
;
apply
Hab
with
x
.
-
by
apply
Ha
.
Qed
.
Lemma
eq_equiv
{
A
:
cofeT
}
(
a
b
:
A
)
:
(
True
⊢
a
≡
b
)
→
a
≡
b
.
Proof
.
unseal
=>
Hab
;
apply
equiv_dist
;
intros
n
;
apply
Hab
with
∅
;
last
done
.
apply
cmra_valid_validN
,
ucmra_unit_valid
.
Qed
.
Lemma
eq_rewrite_contractive
{
A
:
cofeT
}
a
b
(
Ψ
:
A
→
uPred
M
)
P
Lemma
internal_eq_rewrite_contractive
{
A
:
cofeT
}
a
b
(
Ψ
:
A
→
uPred
M
)
P
{
H
Ψ
:
Contractive
Ψ
}
:
(
P
⊢
▷
(
a
≡
b
))
→
(
P
⊢
Ψ
a
)
→
P
⊢
Ψ
b
.
Proof
.
unseal
;
intros
Hab
Ha
;
split
=>
n
x
??.
apply
H
Ψ
with
n
a
;
auto
.
...
...
program_logic/boxes.v
View file @
e224e891
...
...
@@ -165,7 +165,8 @@ Lemma box_fill_all f P Q : box N f P ★ ▷ P ={N}=★ box N (const true <$> f)
Proof
.
iIntros
"[H HP]"
;
iDestruct
"H"
as
(
Φ
)
"[#HeqP Hf]"
.
iExists
Φ
;
iSplitR
;
first
by
rewrite
big_sepM_fmap
.
rewrite
eq_iff
later_iff
big_sepM_later
;
iDestruct
(
"HeqP"
with
"HP"
)
as
"HP"
.
rewrite
internal_eq_iff
later_iff
big_sepM_later
.
iDestruct
(
"HeqP"
with
"HP"
)
as
"HP"
.
iCombine
"Hf"
"HP"
as
"Hf"
.
rewrite
big_sepM_fmap
;
iApply
(
fupd_big_sepM
_
_
f
).
iApply
(
big_sepM_impl
_
_
f
)
;
iFrame
"Hf"
.
...
...
@@ -192,7 +193,7 @@ Proof.
iMod
(
"Hclose"
with
"[Hγ]"
)
;
first
(
iNext
;
iExists
false
;
iFrame
;
eauto
).
by
iApply
"HΦ"
.
}
iModIntro
;
iSplitL
"HΦ"
.
-
rewrite
eq_iff
later_iff
big_sepM_later
.
by
iApply
"HeqP"
.
-
rewrite
internal_
eq_iff
later_iff
big_sepM_later
.
by
iApply
"HeqP"
.
-
iExists
Φ
;
iSplit
;
by
rewrite
big_sepM_fmap
.
Qed
.
End
box
.
...
...
program_logic/iprop.v
View file @
e224e891
...
...
@@ -151,6 +151,6 @@ Lemma iProp_unfold_equivI {Σ} (P Q : iProp Σ) :
iProp_unfold
P
≡
iProp_unfold
Q
⊢
(
P
≡
Q
:
iProp
Σ
).
Proof
.
rewrite
-{
2
}(
iProp_fold_unfold
P
)
-{
2
}(
iProp_fold_unfold
Q
).
eapply
(
uPred
.
eq_rewrite
_
_
(
λ
z
,
eapply
(
uPred
.
internal_
eq_rewrite
_
_
(
λ
z
,
iProp_fold
(
iProp_unfold
P
)
≡
iProp_fold
z
))%
I
;
auto
with
I
;
solve_proper
.
Qed
.
program_logic/saved_prop.v
View file @
e224e891
...
...
@@ -42,7 +42,7 @@ Section saved_prop.
{
intros
z
.
rewrite
/
G1
/
G2
-
cFunctor_compose
-{
2
}[
z
]
cFunctor_id
.
apply
(
ne_proper
(
cFunctor_map
F
))
;
split
=>?
;
apply
iProp_fold_unfold
.
}
rewrite
-{
2
}[
x
]
help
-{
2
}[
y
]
help
.
apply
later_mono
.
apply
(
eq_rewrite
(
G1
x
)
(
G1
y
)
(
λ
z
,
G2
(
G1
x
)
≡
G2
z
))%
I
;
apply
(
internal_
eq_rewrite
(
G1
x
)
(
G1
y
)
(
λ
z
,
G2
(
G1
x
)
≡
G2
z
))%
I
;
first
solve_proper
;
auto
with
I
.
Qed
.
End
saved_prop
.
proofmode/class_instances.v
View file @
e224e891
...
...
@@ -33,8 +33,11 @@ Proof. by rewrite /IntoPure discrete_valid. Qed.
(* FromPure *)
Global
Instance
from_pure_pure
φ
:
@
FromPure
M
(
■
φ
)
φ
.
Proof
.
done
.
Qed
.
Global
Instance
from_pure_eq
{
A
:
cofeT
}
(
a
b
:
A
)
:
@
FromPure
M
(
a
≡
b
)
(
a
≡
b
).
Proof
.
rewrite
/
FromPure
.
eapply
pure_elim
;
[
done
|]=>
->.
apply
eq_refl'
.
Qed
.
Global
Instance
from_pure_internal_eq
{
A
:
cofeT
}
(
a
b
:
A
)
:
@
FromPure
M
(
a
≡
b
)
(
a
≡
b
).
Proof
.
rewrite
/
FromPure
.
eapply
pure_elim
;
[
done
|]=>
->.
apply
internal_eq_refl'
.
Qed
.
Global
Instance
from_pure_cmra_valid
{
A
:
cmraT
}
(
a
:
A
)
:
@
FromPure
M
(
✓
a
)
(
✓
a
).
Proof
.
...
...
proofmode/coq_tactics.v
View file @
e224e891
...
...
@@ -653,9 +653,9 @@ Lemma tac_rewrite Δ i p Pxy (lr : bool) Q :
(
∀
n
,
Proper
(
dist
n
==>
dist
n
)
Φ
)
→
(
Δ
⊢
Φ
(
if
lr
then
x
else
y
))
→
Δ
⊢
Q
.
Proof
.
intros
?
A
x
y
?
HPxy
->
?
;
apply
eq_rewrite
;
auto
.
intros
?
A
x
y
?
HPxy
->
?
;
apply
internal_
eq_rewrite
;
auto
.
rewrite
{
1
}
envs_lookup_sound'
//
;
rewrite
sep_elim_l
HPxy
.
destruct
lr
;
auto
using
eq_sym
.
destruct
lr
;
auto
using
internal_
eq_sym
.
Qed
.
Lemma
tac_rewrite_in
Δ
i
p
Pxy
j
q
P
(
lr
:
bool
)
Q
:
...
...
@@ -673,8 +673,10 @@ Proof.
rewrite
sep_elim_l
HPxy
always_and_sep_r
.
rewrite
(
envs_simple_replace_sound
_
_
j
)
//
;
simpl
.
rewrite
HP
right_id
-
assoc
;
apply
wand_elim_r'
.
destruct
lr
.
-
apply
(
eq_rewrite
x
y
(
λ
y
,
□
?q
Φ
y
-
★
Δ
'
)%
I
)
;
eauto
with
I
.
solve_proper
.
-
apply
(
eq_rewrite
y
x
(
λ
y
,
□
?q
Φ
y
-
★
Δ
'
)%
I
)
;
eauto
using
eq_sym
with
I
.
-
apply
(
internal_eq_rewrite
x
y
(
λ
y
,
□
?q
Φ
y
-
★
Δ
'
)%
I
)
;
eauto
with
I
.
solve_proper
.
-
apply
(
internal_eq_rewrite
y
x
(
λ
y
,
□
?q
Φ
y
-
★
Δ
'
)%
I
)
;
eauto
using
internal_eq_sym
with
I
.
solve_proper
.
Qed
.
...
...
proofmode/tactics.v
View file @
e224e891
...
...
@@ -1200,7 +1200,7 @@ Tactic Notation "iMod" open_constr(lem) "as" "%" simple_intropattern(pat) :=
Hint
Extern
0
(
of_envs
_
⊢
_
)
=>
by
iPureIntro
.
Hint
Extern
0
(
of_envs
_
⊢
_
)
=>
iAssumption
.
Hint
Extern
0
(
of_envs
_
⊢
_
)
=>
progress
iIntros
.
Hint
Resolve
uPred
.
eq_refl'
.
(* Maybe make an [iReflexivity] tactic *)
Hint
Resolve
uPred
.
internal_
eq_refl'
.
(* Maybe make an [iReflexivity] tactic *)
(* We should be able to write [Hint Extern 1 (of_envs _ ⊢ (_ ★ _)%I) => ...],
but then [eauto] mysteriously fails. See bug 4762 *)
...
...
tests/proofmode.v
View file @
e224e891
...
...
@@ -67,7 +67,7 @@ Lemma demo_5 (M : ucmraT) (x y : M) (P : uPred M) :
(
∀
z
,
P
→
z
≡
y
)
⊢
(
P
-
★
(
x
,
x
)
≡
(
y
,
x
)).
Proof
.
iIntros
"H1 H2"
.
iRewrite
(
uPred
.
eq_sym
x
x
with
"[#]"
)
;
first
done
.
iRewrite
(
uPred
.
internal_
eq_sym
x
x
with
"[#]"
)
;
first
done
.
iRewrite
-(
"H1"
$!
_
with
"[-]"
)
;
first
done
.
done
.
Qed
.
...
...
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