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
Lennard Gäher
Iris
Commits
4b059555
Commit
4b059555
authored
Dec 20, 2018
by
Robbert Krebbers
Browse files
The unbounded fractional camera.
parent
0e078666
Changes
3
Hide whitespace changes
Inline
Side-by-side
_CoqProject
View file @
4b059555
...
...
@@ -26,6 +26,7 @@ theories/algebra/gmultiset.v
theories/algebra/coPset.v
theories/algebra/deprecated.v
theories/algebra/proofmode_classes.v
theories/algebra/ufrac.v
theories/bi/notation.v
theories/bi/interface.v
theories/bi/derived_connectives.v
...
...
theories/algebra/frac.v
View file @
4b059555
(** This file provides a version of the fractional camera whose elements are
in the internal (0,1] of the rational numbers.
Notice that this camera could in principle be obtained by restricting the
validity of the unbounded fractional camera [ufrac]. *)
From
Coq
.
QArith
Require
Import
Qcanon
.
From
iris
.
algebra
Require
Export
cmra
.
From
iris
.
algebra
Require
Import
proofmode_classes
.
Set
Default
Proof
Using
"Type"
.
(** Since the standard (0,1] fractional camera is used more often, we define
[frac] through a [Notation] instead of a [Definition]. That way, Coq infers the
[frac] camera by default when using the [Qp] type. *)
Notation
frac
:
=
Qp
(
only
parsing
).
Section
frac
.
...
...
theories/algebra/ufrac.v
0 → 100644
View file @
4b059555
(** This file provides a "bounded" version of the fractional camera whose
elements are in the interval (0,..) instead of (0,1]. *)
From
Coq
.
QArith
Require
Import
Qcanon
.
From
iris
.
algebra
Require
Export
cmra
.
From
iris
.
algebra
Require
Import
proofmode_classes
.
Set
Default
Proof
Using
"Type"
.
(** Since the standard (0,1] fractional camera [frac] is used more often, we
define [ufrac] through a [Definition] instead of a [Notation]. That way, Coq
infers the [frac] camera by default when using the [Qp] type. *)
Definition
ufrac
:
=
Qp
.
Section
ufrac
.
Canonical
Structure
ufracC
:
=
leibnizC
ufrac
.
Instance
ufrac_valid
:
Valid
ufrac
:
=
λ
x
,
True
.
Instance
ufrac_pcore
:
PCore
ufrac
:
=
λ
_
,
None
.
Instance
ufrac_op
:
Op
ufrac
:
=
λ
x
y
,
(
x
+
y
)%
Qp
.
Lemma
ufrac_included
(
x
y
:
ufrac
)
:
x
≼
y
↔
(
x
<
y
)%
Qc
.
Proof
.
by
rewrite
Qp_lt_sum
.
Qed
.
Corollary
ufrac_included_weak
(
x
y
:
ufrac
)
:
x
≼
y
→
(
x
≤
y
)%
Qc
.
Proof
.
intros
?%
ufrac_included
.
auto
using
Qclt_le_weak
.
Qed
.
Definition
ufrac_ra_mixin
:
RAMixin
ufrac
.
Proof
.
split
;
try
apply
_;
try
done
.
Qed
.
Canonical
Structure
ufracR
:
=
discreteR
ufrac
ufrac_ra_mixin
.
Global
Instance
ufrac_cmra_discrete
:
CmraDiscrete
ufracR
.
Proof
.
apply
discrete_cmra_discrete
.
Qed
.
End
ufrac
.
Global
Instance
ufrac_cancelable
(
q
:
ufrac
)
:
Cancelable
q
.
Proof
.
intros
?????.
by
apply
Qp_eq
,
(
inj
(
Qcplus
q
)),
(
Qp_eq
(
q
+
y
)
(
q
+
z
))%
Qp
.
Qed
.
Global
Instance
ufrac_id_free
(
q
:
ufrac
)
:
IdFree
q
.
Proof
.
intros
[
q0
Hq0
]
?
EQ
%
Qp_eq
.
rewrite
-{
1
}(
Qcplus_0_r
q
)
in
EQ
.
eapply
Qclt_not_eq
;
first
done
.
by
apply
(
inj
(
Qcplus
q
)).
Qed
.
Lemma
ufrac_op'
(
q
p
:
ufrac
)
:
(
p
⋅
q
)
=
(
p
+
q
)%
Qp
.
Proof
.
done
.
Qed
.
Global
Instance
is_op_ufrac
(
q
:
ufrac
)
:
IsOp'
q
(
q
/
2
)%
Qp
(
q
/
2
)%
Qp
.
Proof
.
by
rewrite
/
IsOp'
/
IsOp
ufrac_op'
Qp_div_2
.
Qed
.
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