Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
I
iriscoq
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
0
Issues
0
List
Boards
Labels
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
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
Joshua Yanovski
iriscoq
Commits
0495154c
Commit
0495154c
authored
Apr 04, 2017
by
JacquesHenri Jourdan
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Upred : explain why things are how they are.
parent
8f3ebec4
Changes
1
Hide whitespace changes
Inline
Sidebyside
Showing
1 changed file
with
19 additions
and
0 deletions
+19
0
theories/base_logic/upred.v
theories/base_logic/upred.v
+19
0
No files found.
theories/base_logic/upred.v
View file @
0495154c
...
...
@@ 8,7 +8,26 @@ Set Default Proof Using "Type".
Record
uPred
(
M
:
ucmraT
)
:
Type
:=
IProp
{
uPred_holds
:>
nat
→
M
→
Prop
;
(
*
[
uPred_mono
]
is
used
to
prove
non

expansiveness
(
guaranteed
by
[
uPred_ne
]).
Therefore
,
it
is
important
that
we
do
not
restrict
it
to
only
valid
elements
.
*
)
uPred_mono
n
x1
x2
:
uPred_holds
n
x1
→
x1
≼
{
n
}
x2
→
uPred_holds
n
x2
;
(
*
We
have
to
restrict
this
to
hold
only
for
valid
elements
,
otherwise
this
condition
is
no
longer
limit
preserving
,
and
uPred
does
no
longer
form
a
COFE
(
i
.
e
.,
[
uPred_compl
]
breaks
).
This
is
because
the
distance
and
equivalence
on
this
cofe
ignores
the
truth
valid
on
invalid
elements
.
This
,
in
turns
,
is
required
by
the
fact
that
entailment
has
to
ignore
invalid
elements
,
which
is
itself
essential
for
proving
[
ownM_valid
].
We
could
,
actually
,
make
the
following
condition
true
even
for
invalid
elements
:
we
have
proved
that
uPred
is
isomorphic
to
a
sub

COFE
of
the
COFE
of
predicates
that
are
monotonous
both
with
respect
to
the
step
index
and
with
respect
to
x
.
However
,
that
would
essentially
require
changing
(
by
making
more
complicated
)
the
model
of
many
connectives
of
the
logic
,
which
we
don
'
t
want
.
*
)
uPred_closed
n1
n2
x
:
uPred_holds
n1
x
→
n2
≤
n1
→
✓
{
n2
}
x
→
uPred_holds
n2
x
}
.
Arguments
uPred_holds
{
_
}
_
_
_
:
simpl
never
.
...
...
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