Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
Iris
Commits
e14e9ec2
Commit
e14e9ec2
authored
Dec 07, 2017
by
Jacques-Henri Jourdan
Browse files
Merge uPred_mono and uPred_closed.
parent
cbb493e7
Changes
3
Hide whitespace changes
Inline
Side-by-side
theories/base_logic/double_negation.v
View file @
e14e9ec2
...
...
@@ -30,11 +30,11 @@ Import uPred.
Lemma
laterN_big
n
a
x
φ
:
✓
{
n
}
x
→
a
≤
n
→
(
▷
^
a
⌜φ⌝
)%
I
n
x
→
φ
.
Proof
.
induction
2
as
[|
??
IHle
].
-
induction
a
;
repeat
(
rewrite
//=
||
uPred
.
unseal
).
-
induction
a
;
repeat
(
rewrite
//=
||
uPred
.
unseal
).
intros
Hlater
.
apply
IHa
;
auto
using
cmra_validN_S
.
move
:
Hlater
;
repeat
(
rewrite
//=
||
uPred
.
unseal
).
move
:
Hlater
;
repeat
(
rewrite
//=
||
uPred
.
unseal
).
-
intros
.
apply
IHle
;
auto
using
cmra_validN_S
.
eapply
uPred_
closed
;
eauto
using
cmra_validN_S
.
eapply
uPred_
mono
;
eauto
using
cmra_validN_S
.
Qed
.
Lemma
laterN_small
n
a
x
φ
:
✓
{
n
}
x
→
n
<
a
→
(
▷
^
a
⌜φ⌝
)%
I
n
x
.
...
...
@@ -46,15 +46,15 @@ Proof.
-
induction
n
as
[|
n
IHn
]
;
[|
move
:
IHle
]
;
repeat
(
rewrite
//=
||
uPred
.
unseal
).
red
;
rewrite
//=.
intros
.
eapply
(
uPred_
closed
_
_
(
S
n
))
;
eauto
using
cmra_validN_S
.
eapply
(
uPred_
mono
_
_
(
S
n
))
;
eauto
using
cmra_validN_S
.
Qed
.
(* It is easy to show that most of the basic properties of bupd that
are used throughout Iris hold for nnupd.
are used throughout Iris hold for nnupd.
In fact, the first three properties that follow hold for any
modality of the form (- -∗ Q) -∗ Q for arbitrary Q. The situation
here is slightly different, because nnupd is of the form
here is slightly different, because nnupd is of the form
∀ n, (- -∗ (Q n)) -∗ (Q n), but the proofs carry over straightforwardly.
*)
...
...
@@ -77,8 +77,8 @@ Proof.
Qed
.
Lemma
nnupd_ownM_updateP
x
(
Φ
:
M
→
Prop
)
:
x
~~>
:
Φ
→
uPred_ownM
x
=
n
=>
∃
y
,
⌜Φ
y
⌝
∧
uPred_ownM
y
.
Proof
.
intros
Hbupd
.
split
.
rewrite
/
uPred_nnupd
.
repeat
uPred
.
unseal
.
Proof
.
intros
Hbupd
.
split
.
rewrite
/
uPred_nnupd
.
repeat
uPred
.
unseal
.
intros
n
y
?
Hown
a
.
red
;
rewrite
//=
=>
n'
yf
??.
inversion
Hown
as
(
x'
&
Hequiv
).
...
...
@@ -87,18 +87,18 @@ Proof.
case
(
decide
(
a
≤
n'
)).
-
intros
Hle
Hwand
.
exfalso
.
eapply
laterN_big
;
last
(
uPred
.
unseal
;
eapply
(
Hwand
n'
(
y'
⋅
x'
)))
;
eauto
.
*
rewrite
comm
-
assoc
.
done
.
*
rewrite
comm
-
assoc
.
done
.
*
e
exists
.
split
;
eapply
uPred_mono
;
red
;
rewrite
//=
;
eauto
.
-
intros
;
assert
(
n'
<
a
).
omega
.
*
rewrite
comm
-
assoc
.
done
.
*
rewrite
comm
-
assoc
.
done
.
*
exists
y'
.
split
=>//.
by
exists
x'
.
-
intros
;
assert
(
n'
<
a
).
omega
.
move
:
laterN_small
.
uPred
.
unseal
.
naive_solver
.
Qed
.
(* However, the transitivity property seems to be much harder to
prove. This is surprising, because transitivity does hold for
prove. This is surprising, because transitivity does hold for
modalities of the form (- -∗ Q) -∗ Q. What goes wrong when we quantify
now over n?
now over n?
*)
Remark
nnupd_trans
P
:
(|=
n
=>
|=
n
=>
P
)
⊢
(|=
n
=>
P
).
...
...
@@ -111,7 +111,7 @@ Proof.
(* Oops -- the exponents of the later modality don't match up! *)
Abort
.
(* Instead, we will need to prove this in the model. We start by showing that
(* Instead, we will need to prove this in the model. We start by showing that
nnupd is the limit of a the following sequence:
(- -∗ False) - ∗ False,
...
...
@@ -121,12 +121,12 @@ Abort.
Then, it is easy enough to show that each of the uPreds in this sequence
is transitive. It turns out that this implies that nnupd is transitive. *)
(* The definition of the sequence above: *)
Fixpoint
uPred_nnupd_k
{
M
}
k
(
P
:
uPred
M
)
:
uPred
M
:
=
((
P
-
∗
▷
^
k
False
)
-
∗
▷
^
k
False
)
∧
match
k
with
match
k
with
O
=>
True
|
S
k'
=>
uPred_nnupd_k
k'
P
end
.
...
...
@@ -138,11 +138,11 @@ Notation "|=n=>_ k Q" := (uPred_nnupd_k k Q)
(* One direction of the limiting process is easy -- nnupd implies nnupd_k for each k *)
Lemma
nnupd_trunc1
k
P
:
(|=
n
=>
P
)
⊢
|=
n
=>
_k
P
.
Proof
.
induction
k
.
-
rewrite
/
uPred_nnupd_k
/
uPred_nnupd
.
induction
k
.
-
rewrite
/
uPred_nnupd_k
/
uPred_nnupd
.
rewrite
(
forall_elim
0
)
//=
right_id
//.
-
simpl
.
apply
and_intro
;
auto
.
rewrite
/
uPred_nnupd
.
rewrite
/
uPred_nnupd
.
rewrite
(
forall_elim
(
S
k
))
//=.
Qed
.
...
...
@@ -190,10 +190,10 @@ Lemma nnupd_nnupd_k_dist k P: (|=n=> P)%I ≡{k}≡ (|=n=>_k P)%I.
***
intros
.
exfalso
.
assert
(
n
≤
k'
).
omega
.
assert
(
n
=
S
k
∨
n
<
S
k
)
as
[->|]
by
omega
.
****
eapply
laterN_big
;
eauto
;
unseal
.
eapply
HnnP
;
eauto
.
****
move
:
nnupd_k_elim
.
unseal
.
intros
Hnnupdk
.
****
move
:
nnupd_k_elim
.
unseal
.
intros
Hnnupdk
.
eapply
laterN_big
;
eauto
.
unseal
.
eapply
(
Hnnupdk
n
k
)
;
first
omega
;
eauto
.
exists
x
,
x'
.
split_and
!
;
eauto
.
eapply
uPred_
closed
;
eauto
.
exists
x
,
x'
.
split_and
!
;
eauto
.
eapply
uPred_
mono
;
eauto
.
**
intros
HP
.
eapply
IHk
;
auto
.
move
:
HP
.
unseal
.
intros
(?&?)
;
naive_solver
.
Qed
.
...
...
@@ -203,13 +203,13 @@ Lemma nnupd_k_intro k P: P ⊢ (|=n=>_k P).
Proof
.
induction
k
;
rewrite
//=
?right_id
.
-
apply
wand_intro_l
.
apply
wand_elim_l
.
-
apply
and_intro
;
auto
.
-
apply
and_intro
;
auto
.
apply
wand_intro_l
.
apply
wand_elim_l
.
Qed
.
Lemma
nnupd_k_mono
k
P
Q
:
(
P
⊢
Q
)
→
(|=
n
=>
_k
P
)
⊢
(|=
n
=>
_k
Q
).
Proof
.
induction
k
;
rewrite
//=
?right_id
=>
HPQ
.
induction
k
;
rewrite
//=
?right_id
=>
HPQ
.
-
do
2
(
apply
wand_mono
;
auto
).
-
apply
and_mono
;
auto
;
do
2
(
apply
wand_mono
;
auto
).
Qed
.
...
...
@@ -227,7 +227,7 @@ Lemma nnupd_k_trans k P: (|=n=>_k |=n=>_k P) ⊢ (|=n=>_k P).
Proof
.
revert
P
.
induction
k
;
intros
P
.
-
rewrite
//=
?right_id
.
apply
wand_intro_l
.
-
rewrite
//=
?right_id
.
apply
wand_intro_l
.
rewrite
{
1
}(
nnupd_k_intro
0
(
P
-
∗
False
)%
I
)
//=
?right_id
.
apply
wand_elim_r
.
-
rewrite
{
2
}(
nnupd_k_unfold
k
P
).
apply
and_intro
.
...
...
@@ -262,8 +262,8 @@ Proof.
case
(
decide
(
a
≤
n'
)).
-
intros
Hle
Hwand
.
exfalso
.
eapply
laterN_big
;
last
(
uPred
.
unseal
;
eapply
(
Hwand
n'
x'
))
;
eauto
.
*
rewrite
comm
.
done
.
*
rewrite
comm
.
done
.
*
rewrite
comm
.
done
.
*
rewrite
comm
.
done
.
-
intros
;
assert
(
n'
<
a
).
omega
.
move
:
laterN_small
.
uPred
.
unseal
.
naive_solver
.
...
...
@@ -299,23 +299,23 @@ End classical.
Lemma
nnupd_dne
φ
:
(|=
n
=>
⌜
¬¬
φ
→
φ⌝
:
uPred
M
)%
I
.
Proof
.
rewrite
/
uPred_nnupd
.
apply
forall_intro
=>
n
.
apply
wand_intro_l
.
rewrite
?right_id
.
apply
wand_intro_l
.
rewrite
?right_id
.
assert
(
∀
φ
,
¬¬¬¬
φ
→
¬¬
φ
)
by
naive_solver
.
assert
(
Hdne
:
¬¬
(
¬¬
φ
→
φ
))
by
naive_solver
.
split
.
unseal
.
intros
n'
??
Hupd
.
case
(
decide
(
n'
<
n
)).
-
intros
.
move
:
laterN_small
.
unseal
.
naive_solver
.
-
intros
.
assert
(
n
≤
n'
).
omega
.
-
intros
.
assert
(
n
≤
n'
).
omega
.
exfalso
.
specialize
(
Hupd
n'
ε
).
eapply
Hdne
.
intros
Hfal
.
eapply
laterN_big
;
eauto
.
eapply
laterN_big
;
eauto
.
unseal
.
rewrite
right_id
in
Hupd
*
;
naive_solver
.
Qed
.
(* Nevertheless, we can prove a weaker form of adequacy (which is equvialent to adequacy
under classical axioms) directly without passing through the proofs for bupd: *)
Lemma
adequacy_helper1
P
n
k
x
:
✓
{
S
n
+
k
}
x
→
¬¬
(
Nat
.
iter
(
S
n
)
(
λ
P
,
|=
n
=>
▷
P
)%
I
P
(
S
n
+
k
)
x
)
✓
{
S
n
+
k
}
x
→
¬¬
(
Nat
.
iter
(
S
n
)
(
λ
P
,
|=
n
=>
▷
P
)%
I
P
(
S
n
+
k
)
x
)
→
¬¬
(
∃
x'
,
✓
{
n
+
k
}
(
x'
)
∧
Nat
.
iter
n
(
λ
P
,
|=
n
=>
▷
P
)%
I
P
(
n
+
k
)
(
x'
)).
Proof
.
revert
k
P
x
.
induction
n
.
...
...
@@ -325,12 +325,12 @@ Proof.
specialize
(
Hf3
(
S
k
)
(
S
k
)
ε
).
rewrite
right_id
in
Hf3
*.
unseal
.
intros
Hf3
.
eapply
Hf3
;
eauto
.
intros
???
Hx'
.
rewrite
left_id
in
Hx'
*=>
Hx'
.
unseal
.
unseal
.
assert
(
n'
<
S
k
∨
n'
=
S
k
)
as
[|]
by
omega
.
*
intros
.
move
:
(
laterN_small
n'
(
S
k
)
x'
False
).
rewrite
//=.
unseal
.
intros
Hsmall
.
eapply
Hsmall
;
eauto
.
*
subst
.
intros
.
exfalso
.
eapply
Hf2
.
exists
x'
.
split
;
eauto
using
cmra_validN_S
.
-
intros
k
P
x
Hx
.
rewrite
?Nat_iter_S_r
.
-
intros
k
P
x
Hx
.
rewrite
?Nat_iter_S_r
.
replace
(
S
(
S
n
)
+
k
)
with
(
S
n
+
(
S
k
))
by
omega
.
replace
(
S
n
+
k
)
with
(
n
+
(
S
k
))
by
omega
.
intros
.
eapply
IHn
.
replace
(
S
n
+
S
k
)
with
(
S
(
S
n
)
+
k
)
by
omega
.
eauto
.
...
...
@@ -338,7 +338,7 @@ Proof.
Qed
.
Lemma
adequacy_helper2
P
n
k
x
:
✓
{
S
n
+
k
}
x
→
¬¬
(
Nat
.
iter
(
S
n
)
(
λ
P
,
|=
n
=>
▷
P
)%
I
P
(
S
n
+
k
)
x
)
✓
{
S
n
+
k
}
x
→
¬¬
(
Nat
.
iter
(
S
n
)
(
λ
P
,
|=
n
=>
▷
P
)%
I
P
(
S
n
+
k
)
x
)
→
¬¬
(
∃
x'
,
✓
{
k
}
(
x'
)
∧
Nat
.
iter
0
(
λ
P
,
|=
n
=>
▷
P
)%
I
P
k
(
x'
)).
Proof
.
revert
x
.
induction
n
.
...
...
theories/base_logic/primitive.v
View file @
e14e9ec2
...
...
@@ -35,11 +35,10 @@ Program Definition uPred_impl_def {M} (P Q : uPred M) : uPred M :=
{|
uPred_holds
n
x
:
=
∀
n'
x'
,
x
≼
x'
→
n'
≤
n
→
✓
{
n'
}
x'
→
P
n'
x'
→
Q
n'
x'
|}.
Next
Obligation
.
intros
M
P
Q
n1
x1
x1'
HPQ
[
x2
Hx1'
]
n2
x3
[
x4
Hx3
]
?
;
simpl
in
*.
intros
M
P
Q
n1
n1'
x1
x1'
HPQ
[
x2
Hx1'
]
Hn1
n2
x3
[
x4
Hx3
]
?
;
simpl
in
*.
rewrite
Hx3
(
dist_le
_
_
_
_
Hx1'
)
;
auto
.
intros
??.
eapply
HPQ
;
auto
.
exists
(
x2
⋅
x4
)
;
by
rewrite
assoc
.
Qed
.
Next
Obligation
.
intros
M
P
Q
[|
n1
]
[|
n2
]
x
;
auto
with
lia
.
Qed
.
Definition
uPred_impl_aux
:
seal
(@
uPred_impl_def
).
by
eexists
.
Qed
.
Definition
uPred_impl
{
M
}
:
=
unseal
uPred_impl_aux
M
.
Definition
uPred_impl_eq
:
...
...
@@ -71,14 +70,9 @@ Definition uPred_internal_eq_eq:
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
|}.
Next
Obligation
.
intros
M
P
Q
n
x
y
(
x1
&
x2
&
Hx
&?&?)
[
z
Hy
].
intros
M
P
Q
n
1
n2
x
y
(
x1
&
x2
&
Hx
&?&?)
[
z
Hy
]
Hn
.
exists
x1
,
(
x2
⋅
z
)
;
split_and
?
;
eauto
using
uPred_mono
,
cmra_includedN_l
.
by
rewrite
Hy
Hx
assoc
.
Qed
.
Next
Obligation
.
intros
M
P
Q
n1
n2
x
(
x1
&
x2
&
Hx
&?&?)
?.
exists
x1
,
x2
;
ofe_subst
;
split_and
!
;
eauto
using
dist_le
,
uPred_closed
,
cmra_validN_op_l
,
cmra_validN_op_r
.
eapply
dist_le
,
Hn
.
by
rewrite
Hy
Hx
assoc
.
Qed
.
Definition
uPred_sep_aux
:
seal
(@
uPred_sep_def
).
by
eexists
.
Qed
.
Definition
uPred_sep
{
M
}
:
=
unseal
uPred_sep_aux
M
.
...
...
@@ -88,11 +82,10 @@ Program Definition uPred_wand_def {M} (P Q : uPred M) : uPred M :=
{|
uPred_holds
n
x
:
=
∀
n'
x'
,
n'
≤
n
→
✓
{
n'
}
(
x
⋅
x'
)
→
P
n'
x'
→
Q
n'
(
x
⋅
x'
)
|}.
Next
Obligation
.
intros
M
P
Q
n
x1
x1'
HPQ
?
n3
x3
???
;
simpl
in
*.
apply
uPred_mono
with
(
x1
⋅
x3
)
;
intros
M
P
Q
n
1
n1'
x1
x1'
HPQ
?
Hn
n3
x3
???
;
simpl
in
*.
e
apply
uPred_mono
with
n3
(
x1
⋅
x3
)
;
eauto
using
cmra_validN_includedN
,
cmra_monoN_r
,
cmra_includedN_le
.
Qed
.
Next
Obligation
.
naive_solver
.
Qed
.
Definition
uPred_wand_aux
:
seal
(@
uPred_wand_def
).
by
eexists
.
Qed
.
Definition
uPred_wand
{
M
}
:
=
unseal
uPred_wand_aux
M
.
Definition
uPred_wand_eq
:
...
...
@@ -103,7 +96,7 @@ Definition uPred_wand_eq :
because Iris is afine. The following is easier to work with. *)
Program
Definition
uPred_plainly_def
{
M
}
(
P
:
uPred
M
)
:
uPred
M
:
=
{|
uPred_holds
n
x
:
=
P
n
ε
|}.
Solve
Obligations
with
naive_solver
eauto
using
uPred_
closed
,
ucmra_unit_validN
.
Solve
Obligations
with
naive_solver
eauto
using
uPred_
mono
,
ucmra_unit_validN
.
Definition
uPred_plainly_aux
:
seal
(@
uPred_plainly_def
).
by
eexists
.
Qed
.
Definition
uPred_plainly
{
M
}
:
=
unseal
uPred_plainly_aux
M
.
Definition
uPred_plainly_eq
:
...
...
@@ -114,7 +107,6 @@ Program Definition uPred_persistently_def {M} (P : uPred M) : uPred M :=
Next
Obligation
.
intros
M
;
naive_solver
eauto
using
uPred_mono
,
@
cmra_core_monoN
.
Qed
.
Next
Obligation
.
naive_solver
eauto
using
uPred_closed
,
@
cmra_core_validN
.
Qed
.
Definition
uPred_persistently_aux
:
seal
(@
uPred_persistently_def
).
by
eexists
.
Qed
.
Definition
uPred_persistently
{
M
}
:
=
unseal
uPred_persistently_aux
M
.
Definition
uPred_persistently_eq
:
...
...
@@ -123,10 +115,7 @@ Definition uPred_persistently_eq :
Program
Definition
uPred_later_def
{
M
}
(
P
:
uPred
M
)
:
uPred
M
:
=
{|
uPred_holds
n
x
:
=
match
n
return
_
with
0
=>
True
|
S
n'
=>
P
n'
x
end
|}.
Next
Obligation
.
intros
M
P
[|
n
]
x1
x2
;
eauto
using
uPred_mono
,
cmra_includedN_S
.
Qed
.
Next
Obligation
.
intros
M
P
[|
n1
]
[|
n2
]
x
;
eauto
using
uPred_closed
,
cmra_validN_S
with
lia
.
intros
M
P
[|
n1
]
[|
n2
]
x1
x2
;
eauto
using
uPred_mono
,
cmra_includedN_S
with
lia
.
Qed
.
Definition
uPred_later_aux
:
seal
(@
uPred_later_def
).
by
eexists
.
Qed
.
Definition
uPred_later
{
M
}
:
=
unseal
uPred_later_aux
M
.
...
...
@@ -136,10 +125,9 @@ Definition uPred_later_eq :
Program
Definition
uPred_ownM_def
{
M
:
ucmraT
}
(
a
:
M
)
:
uPred
M
:
=
{|
uPred_holds
n
x
:
=
a
≼
{
n
}
x
|}.
Next
Obligation
.
intros
M
a
n
x1
x
[
a'
Hx1
]
[
x2
->]
.
exists
(
a'
⋅
x2
).
by
rewrite
(
assoc
op
)
Hx1
.
intros
M
a
n
1
n2
x1
x
[
a'
Hx1
]
[
x2
Hx
]
Hn
.
eapply
cmra_includedN_le
=>//
.
exists
(
a'
⋅
x2
).
by
rewrite
Hx
(
assoc
op
)
Hx1
.
Qed
.
Next
Obligation
.
naive_solver
eauto
using
cmra_includedN_le
.
Qed
.
Definition
uPred_ownM_aux
:
seal
(@
uPred_ownM_def
).
by
eexists
.
Qed
.
Definition
uPred_ownM
{
M
}
:
=
unseal
uPred_ownM_aux
M
.
Definition
uPred_ownM_eq
:
...
...
@@ -157,13 +145,12 @@ Program Definition uPred_bupd_def {M} (Q : uPred M) : uPred M :=
{|
uPred_holds
n
x
:
=
∀
k
yf
,
k
≤
n
→
✓
{
k
}
(
x
⋅
yf
)
→
∃
x'
,
✓
{
k
}
(
x'
⋅
yf
)
∧
Q
k
x'
|}.
Next
Obligation
.
intros
M
Q
n
x1
x2
HQ
[
x3
Hx
]
k
yf
Hk
.
intros
M
Q
n
1
n2
x1
x2
HQ
[
x3
Hx
]
Hn
k
yf
Hk
.
rewrite
(
dist_le
_
_
_
_
Hx
)
;
last
lia
.
intros
Hxy
.
destruct
(
HQ
k
(
x3
⋅
yf
))
as
(
x'
&?&?)
;
[
auto
|
by
rewrite
assoc
|].
exists
(
x'
⋅
x3
)
;
split
;
first
by
rewrite
-
assoc
.
apply
uPred_mono
with
x'
;
eauto
using
cmra_includedN_l
.
eauto
using
uPred_mono
,
cmra_includedN_l
.
Qed
.
Next
Obligation
.
naive_solver
.
Qed
.
Definition
uPred_bupd_aux
:
seal
(@
uPred_bupd_def
).
by
eexists
.
Qed
.
Definition
uPred_bupd
{
M
}
:
=
unseal
uPred_bupd_aux
M
.
Definition
uPred_bupd_eq
:
@
uPred_bupd
=
@
uPred_bupd_def
:
=
seal_eq
uPred_bupd_aux
.
...
...
@@ -380,7 +367,7 @@ Proof. intros HP HQ; unseal; split=> n x ? [?|?]. by apply HP. by apply HQ. Qed.
Lemma
impl_intro_r
P
Q
R
:
(
P
∧
Q
⊢
R
)
→
P
⊢
Q
→
R
.
Proof
.
unseal
;
intros
HQ
;
split
=>
n
x
??
n'
x'
????.
apply
HQ
;
naive_solver
eauto
using
uPred_mono
,
uPred_closed
,
cmra_included_includedN
.
naive_solver
eauto
using
uPred_mono
,
cmra_included_includedN
.
Qed
.
Lemma
impl_elim
P
Q
R
:
(
P
⊢
Q
→
R
)
→
(
P
⊢
Q
)
→
P
⊢
R
.
Proof
.
by
unseal
;
intros
HP
HP'
;
split
=>
n
x
??
;
apply
HP
with
n
x
,
HP'
.
Qed
.
...
...
@@ -432,7 +419,7 @@ Lemma wand_intro_r P Q R : (P ∗ Q ⊢ R) → P ⊢ Q -∗ R.
Proof
.
unseal
=>
HPQR
;
split
=>
n
x
??
n'
x'
???
;
apply
HPQR
;
auto
.
exists
x
,
x'
;
split_and
?
;
auto
.
eapply
uPred_
closed
with
n
;
eauto
using
cmra_validN_op_l
.
eapply
uPred_
mono
with
n
x
;
eauto
using
cmra_validN_op_l
.
Qed
.
Lemma
wand_elim_l'
P
Q
R
:
(
P
⊢
Q
-
∗
R
)
→
P
∗
Q
⊢
R
.
Proof
.
...
...
@@ -486,14 +473,14 @@ Qed.
Lemma
persistently_impl_plainly
P
Q
:
(
■
P
→
□
Q
)
⊢
□
(
■
P
→
Q
).
Proof
.
unseal
;
split
=>
/=
n
x
?
HPQ
n'
x'
????.
eapply
uPred_mono
with
(
core
x
)
,
cmra_included_includedN
;
auto
.
eapply
uPred_mono
with
n'
(
core
x
)
=>//
;
[|
by
apply
cmra_included_includedN
]
.
apply
(
HPQ
n'
x
)
;
eauto
using
cmra_validN_le
.
Qed
.
Lemma
plainly_impl_plainly
P
Q
:
(
■
P
→
■
Q
)
⊢
■
(
■
P
→
Q
).
Proof
.
unseal
;
split
=>
/=
n
x
?
HPQ
n'
x'
????.
eapply
uPred_mono
with
ε
,
cmra_included_includedN
;
auto
.
eapply
uPred_mono
with
n'
ε
=>//
;
[|
by
apply
cmra_included_includedN
]
.
apply
(
HPQ
n'
x
)
;
eauto
using
cmra_validN_le
.
Qed
.
...
...
@@ -505,7 +492,7 @@ Qed.
Lemma
l
ö
b
P
:
(
▷
P
→
P
)
⊢
P
.
Proof
.
unseal
;
split
=>
n
x
?
HP
;
induction
n
as
[|
n
IH
]
;
[
by
apply
HP
|].
apply
HP
,
IH
,
uPred_
closed
with
(
S
n
)
;
eauto
using
cmra_validN_S
.
apply
HP
,
IH
,
uPred_
mono
with
(
S
n
)
x
;
eauto
using
cmra_validN_S
.
Qed
.
Lemma
later_forall_2
{
A
}
(
Φ
:
A
→
uPred
M
)
:
(
∀
a
,
▷
Φ
a
)
⊢
▷
∀
a
,
Φ
a
.
Proof
.
unseal
;
by
split
=>
-[|
n
]
x
.
Qed
.
...
...
@@ -526,8 +513,7 @@ Qed.
Lemma
later_false_excluded_middle
P
:
▷
P
⊢
▷
False
∨
(
▷
False
→
P
).
Proof
.
unseal
;
split
=>
-[|
n
]
x
?
/=
HP
;
[
by
left
|
right
].
intros
[|
n'
]
x'
????
;
[|
done
].
eauto
using
uPred_closed
,
uPred_mono
,
cmra_included_includedN
.
intros
[|
n'
]
x'
????
;
eauto
using
uPred_mono
,
cmra_included_includedN
.
Qed
.
Lemma
persistently_later
P
:
□
▷
P
⊣
⊢
▷
□
P
.
Proof
.
by
unseal
.
Qed
.
...
...
@@ -577,7 +563,7 @@ Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed.
Lemma
bupd_intro
P
:
P
==
∗
P
.
Proof
.
unseal
.
split
=>
n
x
?
HP
k
yf
?
;
exists
x
;
split
;
first
done
.
apply
uPred_
closed
with
n
;
eauto
using
cmra_validN_op_l
.
apply
uPred_
mono
with
n
x
;
eauto
using
cmra_validN_op_l
.
Qed
.
Lemma
bupd_mono
P
Q
:
(
P
⊢
Q
)
→
(|==>
P
)
==
∗
Q
.
Proof
.
...
...
@@ -593,8 +579,7 @@ Proof.
destruct
(
HP
k
(
x2
⋅
yf
))
as
(
x'
&?&?)
;
eauto
.
{
by
rewrite
assoc
-(
dist_le
_
_
_
_
Hx
)
;
last
lia
.
}
exists
(
x'
⋅
x2
)
;
split
;
first
by
rewrite
-
assoc
.
exists
x'
,
x2
;
split_and
?
;
auto
.
apply
uPred_closed
with
n
;
eauto
3
using
cmra_validN_op_l
,
cmra_validN_op_r
.
exists
x'
,
x2
.
eauto
using
uPred_mono
,
cmra_validN_op_l
,
cmra_validN_op_r
.
Qed
.
Lemma
bupd_ownM_updateP
x
(
Φ
:
M
→
Prop
)
:
x
~~>
:
Φ
→
uPred_ownM
x
==
∗
∃
y
,
⌜Φ
y
⌝
∧
uPred_ownM
y
.
...
...
theories/base_logic/upred.v
View file @
e14e9ec2
...
...
@@ -9,9 +9,8 @@ Set Default Proof Using "Type".
Record
uPred
(
M
:
ucmraT
)
:
Type
:
=
IProp
{
uPred_holds
:
>
nat
→
M
→
Prop
;
uPred_mono
n
x1
x2
:
uPred_holds
n
x1
→
x1
≼
{
n
}
x2
→
uPred_holds
n
x2
;
uPred_closed
n1
n2
x
:
uPred_holds
n1
x
→
n2
≤
n1
→
uPred_holds
n2
x
uPred_mono
n1
n2
x1
x2
:
uPred_holds
n1
x1
→
x1
≼
{
n1
}
x2
→
n2
≤
n1
→
uPred_holds
n2
x2
}.
Arguments
uPred_holds
{
_
}
_
_
_
:
simpl
never
.
Add
Printing
Constructor
uPred
.
...
...
@@ -81,18 +80,15 @@ Section cofe.
Program
Definition
uPred_compl
:
Compl
uPredC
:
=
λ
c
,
{|
uPred_holds
n
x
:
=
∀
n'
,
n'
≤
n
→
✓
{
n'
}
x
→
c
n'
n'
x
|}.
Next
Obligation
.
move
=>
/=
c
n
x1
x2
Hx1
Hx12
n'
Hn'n
Hv
.
eapply
uPred_mono
.
by
eapply
Hx1
,
cmra_validN_includedN
,
cmra_includedN_le
.
by
eapply
cmra_includedN_le
.
Qed
.
Next
Obligation
.
move
=>
/=
c
n1
n2
x
Hc
Hn12
n3
Hn23
Hv
.
apply
Hc
.
lia
.
done
.
move
=>
/=
c
n1
n2
x1
x2
HP
Hx12
Hn12
n3
Hn23
Hv
.
eapply
uPred_mono
.
eapply
HP
,
cmra_validN_includedN
,
cmra_includedN_le
=>//
;
lia
.
eapply
cmra_includedN_le
=>//
;
lia
.
done
.
Qed
.
Global
Program
Instance
uPred_cofe
:
Cofe
uPredC
:
=
{|
compl
:
=
uPred_compl
|}.
Next
Obligation
.
intros
n
c
;
split
=>
i
x
Hin
Hv
.
etrans
;
[|
by
symmetry
;
apply
(
chain_cauchy
c
i
n
)].
split
=>
H
;
[
by
apply
H
|].
repeat
intro
.
apply
(
chain_cauchy
c
n'
i
)=>//.
by
eapply
uPred_
closed
.
repeat
intro
.
apply
(
chain_cauchy
c
n'
i
)=>//.
by
eapply
uPred_
mono
.
Qed
.
End
cofe
.
Arguments
uPredC
:
clear
implicits
.
...
...
@@ -107,8 +103,7 @@ Proof. by intros x1 x2 Hx; apply uPred_ne, equiv_dist. Qed.
Lemma
uPred_holds_ne
{
M
}
(
P
Q
:
uPred
M
)
n1
n2
x
:
P
≡
{
n2
}
≡
Q
→
n2
≤
n1
→
✓
{
n2
}
x
→
Q
n1
x
→
P
n2
x
.
Proof
.
intros
[
Hne
]
???.
eapply
Hne
;
try
done
.
eapply
uPred_closed
;
eauto
using
cmra_validN_le
.
intros
[
Hne
]
???.
eapply
Hne
;
try
done
.
eauto
using
uPred_mono
,
cmra_validN_le
.
Qed
.
(** functor *)
...
...
@@ -116,7 +111,6 @@ Program Definition uPred_map {M1 M2 : ucmraT} (f : M2 -n> M1)
`
{!
CmraMorphism
f
}
(
P
:
uPred
M1
)
:
uPred
M2
:
=
{|
uPred_holds
n
x
:
=
P
n
(
f
x
)
|}.
Next
Obligation
.
naive_solver
eauto
using
uPred_mono
,
cmra_morphism_monotoneN
.
Qed
.
Next
Obligation
.
naive_solver
eauto
using
uPred_closed
,
cmra_morphism_validN
.
Qed
.
Instance
uPred_map_ne
{
M1
M2
:
ucmraT
}
(
f
:
M2
-
n
>
M1
)
`
{!
CmraMorphism
f
}
n
:
Proper
(
dist
n
==>
dist
n
)
(
uPred_map
f
).
...
...
@@ -174,7 +168,7 @@ Inductive uPred_entails {M} (P Q : uPred M) : Prop :=
Hint
Extern
0
(
uPred_entails
_
_
)
=>
reflexivity
.
Instance
uPred_entails_rewrite_relation
M
:
RewriteRelation
(@
uPred_entails
M
).
Hint
Resolve
uPred_mono
uPred_closed
:
uPred_def
.
Hint
Resolve
uPred_mono
:
uPred_def
.
(** Notations *)
Notation
"P ⊢ Q"
:
=
(
uPred_entails
P
%
I
Q
%
I
)
...
...
Write
Preview
Supports
Markdown
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