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
Iris
Fairis
Commits
0b56a3e3
Commit
0b56a3e3
authored
Jan 30, 2016
by
Ralf Jung
Browse files
show that we can implement the predecessor function
parent
e486d0dd
Changes
2
Hide whitespace changes
Inline
Side-by-side
barrier/lifting.v
View file @
0b56a3e3
...
...
@@ -259,14 +259,14 @@ Proof.
Qed
.
Lemma
wp_le_false
n1
n2
E
Q
:
n1
>
n2
→
~
(
n1
≤
n2
)
→
▷
Q
LitFalseV
⊑
wp
(
Σ
:=
Σ
)
E
(
Le
(
LitNat
n1
)
(
LitNat
n2
))
Q
.
Proof
.
intros
Hle
.
etransitivity
;
last
eapply
wp_lift_pure_step
with
(
φ
:=
λ
e
'
,
e
'
=
LitFalse
);
last
first
.
-
intros
?
?
?
?
Hstep
.
inversion_clear
Hstep
;
last
done
.
exfalso
.
eapply
le_not_gt
with
(
n
:=
n1
);
eassumption
.
-
intros
?
.
do
3
eexists
.
econstructor
;
done
.
exfalso
.
omega
.
-
intros
?
.
do
3
eexists
.
econstructor
;
omega
.
-
reflexivity
.
-
apply
later_mono
,
forall_intro
=>
e2
.
apply
impl_intro_l
.
apply
const_elim_l
=>->
.
...
...
barrier/tests.v
View file @
0b56a3e3
...
...
@@ -93,9 +93,29 @@ Module LiftingTests.
eapply
impl_elim
;
first
by
eapply
and_elim_l
.
apply
and_intro
.
+
apply
const_intro
;
omega
.
+
by
rewrite
!
and_elim_r
.
-
rewrite
-
wp_le_false
;
last
by
omega
.
rewrite
-
wp_case_inr
//
-!later_intro -wp_value' //.
-
rewrite
-
wp_le_false
/=
// -wp_case_inr //
.
rewrite
-!
later_intro
-
wp_value
'
//.
rewrite
and_elim_r
.
apply
const_elim_l
=>
Hle
.
assert
(
Heq
:
n1
=
pred
n2
)
by
omega
.
by
subst
n1
=>{
Hle
Hgt
}
.
assert
(
Heq
:
n1
=
pred
n2
)
by
omega
.
by
subst
n1
.
Qed
.
Definition
Pred
:=
Lam
(
If
(
Le
(
Var
0
)
(
LitNat
0
))
(
LitNat
0
)
(
App
(
FindPred
(
Var
0
))
(
LitNat
0
))
).
Lemma
Pred_spec
n
E
Q
:
▷
Q
(
LitNatV
$
pred
n
)
⊑
wp
(
Σ
:=
Σ
)
E
(
App
Pred
(
LitNat
n
))
Q
.
Proof
.
rewrite
-
wp_lam
//. asimpl.
rewrite
-
(
wp_bind
_
_
(
CaseCtx
EmptyCtx
_
_
)).
assert
(
Decision
(
n
≤
0
))
as
Hn
by
apply
_.
destruct
Hn
as
[
Hle
|
Hgt
].
-
rewrite
-
wp_le_true
/=
//. rewrite -wp_case_inl //.
apply
later_mono
.
rewrite
-!
later_intro
-
wp_value
'
//.
assert
(
Heq
:
n
=
0
)
by
omega
.
by
subst
n
.
-
rewrite
-
wp_le_false
/=
// -wp_case_inr //.
apply
later_mono
.
rewrite
-!
later_intro
-
FindPred_spec
.
apply
and_intro
.
+
by
apply
const_intro
;
omega
.
+
done
.
Qed
.
End
LiftingTests
.
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