Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
I
Iris
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
0
Issues
0
List
Boards
Labels
Service Desk
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
George Pirlea
Iris
Commits
4a36be37
Commit
4a36be37
authored
Jan 05, 2017
by
Ralf Jung
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
apply feedback; fix compilation with coq 8.5
parent
af7b6da1
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
18 additions
and
15 deletions
+18
-15
theories/algebra/ofe.v
theories/algebra/ofe.v
+18
-15
No files found.
theories/algebra/ofe.v
View file @
4a36be37
...
@@ -956,22 +956,25 @@ Proof.
...
@@ -956,22 +956,25 @@ Proof.
Qed
.
Qed
.
(** Sigma *)
(** Sigma *)
Class
LimitPreserving
{
A
:
ofeT
}
`
{!
Cofe
A
}
(
P
:
A
→
Prop
)
:
Prop
:
=
limit_preserving
:
∀
c
:
chain
A
,
(
∀
n
,
P
(
c
n
))
→
P
(
compl
c
).
Section
sigma
.
Section
sigma
.
Context
{
A
:
ofeT
}
{
f
:
A
→
Prop
}.
Context
{
A
:
ofeT
}
{
P
:
A
→
Prop
}.
(* TODO: Find a better place for this Equiv instance. It also
(* TODO: Find a better place for this Equiv instance. It also
should not depend on A being an OFE. *)
should not depend on A being an OFE. *)
Instance
sig_equiv
:
Equiv
(
sig
f
)
:
=
Instance
sig_equiv
:
Equiv
(
sig
P
)
:
=
λ
x1
x2
,
(
proj1_sig
x1
)
≡
(
proj1_sig
x2
).
λ
x1
x2
,
(
proj1_sig
x1
)
≡
(
proj1_sig
x2
).
Instance
sig_dist
:
Dist
(
sig
f
)
:
=
Instance
sig_dist
:
Dist
(
sig
P
)
:
=
λ
n
x1
x2
,
(
proj1_sig
x1
)
≡
{
n
}
≡
(
proj1_sig
x2
).
λ
n
x1
x2
,
(
proj1_sig
x1
)
≡
{
n
}
≡
(
proj1_sig
x2
).
Global
Lemma
exist_ne
:
Lemma
exist_ne
:
∀
n
x1
x2
,
x1
≡
{
n
}
≡
x2
→
∀
n
x1
x2
,
x1
≡
{
n
}
≡
x2
→
∀
(
H1
:
f
x1
)
(
H2
:
f
x2
),
(
exist
f
x1
H1
)
≡
{
n
}
≡
(
exist
f
x2
H2
).
∀
(
H1
:
P
x1
)
(
H2
:
P
x2
),
(
exist
P
x1
H1
)
≡
{
n
}
≡
(
exist
P
x2
H2
).
Proof
.
intros
n
??
Hx
??.
exact
Hx
.
Qed
.
Proof
.
intros
n
??
Hx
??.
exact
Hx
.
Qed
.
Global
Instance
proj1_sig_ne
:
Proper
(
dist
n
==>
dist
n
)
(@
proj1_sig
_
f
).
Global
Instance
proj1_sig_ne
:
Proper
(
dist
n
==>
dist
n
)
(@
proj1_sig
_
P
).
Proof
.
intros
n
[]
[]
?.
done
.
Qed
.
Proof
.
intros
n
[]
[]
?.
done
.
Qed
.
Definition
sig_ofe_mixin
:
OfeMixin
(
sig
f
).
Definition
sig_ofe_mixin
:
OfeMixin
(
sig
P
).
Proof
.
Proof
.
split
.
split
.
-
intros
x
y
.
unfold
dist
,
sig_dist
,
equiv
,
sig_equiv
.
-
intros
x
y
.
unfold
dist
,
sig_dist
,
equiv
,
sig_equiv
.
...
@@ -979,24 +982,24 @@ Section sigma.
...
@@ -979,24 +982,24 @@ Section sigma.
-
unfold
dist
,
sig_dist
.
intros
n
.
-
unfold
dist
,
sig_dist
.
intros
n
.
split
;
[
intros
[]
|
intros
[]
[]
|
intros
[]
[]
[]]
;
simpl
;
try
done
.
split
;
[
intros
[]
|
intros
[]
[]
|
intros
[]
[]
[]]
;
simpl
;
try
done
.
intros
.
by
etrans
.
intros
.
by
etrans
.
-
intros
n
[
]
[].
unfold
dist
,
sig_dist
.
apply
dist_S
.
-
intros
n
[
??]
[??].
unfold
dist
,
sig_dist
.
simpl
.
apply
dist_S
.
Qed
.
Qed
.
Canonical
Structure
sigC
:
ofeT
:
=
OfeT
(
sig
f
)
sig_ofe_mixin
.
Canonical
Structure
sigC
:
ofeT
:
=
OfeT
(
sig
P
)
sig_ofe_mixin
.
Global
Class
LimitPreserving
`
{
Cofe
A
}
:
Prop
:
=
(* FIXME: WTF, it seems that within these braces {...} the ofe argument of LimitPreserving
limit_preserving
:
∀
c
:
chain
A
,
(
∀
n
,
f
(
c
n
))
→
f
(
compl
c
).
suddenyl becomes explicit...? *)
Program
Definition
sig_compl
`
{
LimitPreserving
}
:
Compl
sigC
:
=
Program
Definition
sig_compl
`
{
LimitPreserving
_
P
}
:
Compl
sigC
:
=
λ
c
,
exist
f
(
compl
(
chain_map
proj1_sig
c
))
_
.
λ
c
,
exist
P
(
compl
(
chain_map
proj1_sig
c
))
_
.
Next
Obligation
.
Next
Obligation
.
intros
?
Hlim
c
.
apply
Hlim
.
move
=>
n
/=.
destruct
(
c
n
).
done
.
intros
?
Hlim
c
.
apply
Hlim
.
move
=>
n
/=.
destruct
(
c
n
).
done
.
Qed
.
Qed
.
Program
Definition
sig_cofe
`
{
LimitPreserving
}
:
Cofe
sigC
:
=
Program
Definition
sig_cofe
`
{
LimitPreserving
_
P
}
:
Cofe
sigC
:
=
{|
compl
:
=
sig_compl
|}.
{|
compl
:
=
sig_compl
|}.
Next
Obligation
.
Next
Obligation
.
intros
?
Hlim
n
c
.
apply
(
conv_compl
n
(
chain_map
proj1_sig
c
)).
intros
?
Hlim
n
c
.
apply
(
conv_compl
n
(
chain_map
proj1_sig
c
)).
Qed
.
Qed
.
Global
Instance
sig_timeless
(
x
:
sig
f
)
:
Global
Instance
sig_timeless
(
x
:
sig
P
)
:
Timeless
(
proj1_sig
x
)
→
Timeless
x
.
Timeless
(
proj1_sig
x
)
→
Timeless
x
.
Proof
.
intros
?
y
.
destruct
x
,
y
.
unfold
dist
,
sig_dist
,
equiv
,
sig_equiv
.
apply
(
timeless
_
).
Qed
.
Proof
.
intros
?
y
.
destruct
x
,
y
.
unfold
dist
,
sig_dist
,
equiv
,
sig_equiv
.
apply
(
timeless
_
).
Qed
.
Global
Instance
sig_discrete_cofe
:
Discrete
A
→
Discrete
sigC
.
Global
Instance
sig_discrete_cofe
:
Discrete
A
→
Discrete
sigC
.
...
...
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