Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
C
coq-pactole
Manage
Activity
Members
Labels
Plan
Issues
0
Issue boards
Milestones
Wiki
Code
Merge requests
0
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Model registry
Operate
Environments
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pactole
coq-pactole
Commits
28f42262
Commit
28f42262
authored
5 years ago
by
Lionel Rieg
Browse files
Options
Downloads
Patches
Plain Diff
Coquilles dans les commentaires
parent
a8ca8e48
No related branches found
No related tags found
No related merge requests found
Changes
4
Hide whitespace changes
Inline
Side-by-side
Showing
4 changed files
Models/ContinuousGraph.v
+5
-4
5 additions, 4 deletions
Models/ContinuousGraph.v
Models/GraphEquivalence.v
+0
-8
0 additions, 8 deletions
Models/GraphEquivalence.v
Models/RigidFlexibleEquivalence.v
+1
-1
1 addition, 1 deletion
Models/RigidFlexibleEquivalence.v
Spaces/Graph.v
+1
-1
1 addition, 1 deletion
Spaces/Graph.v
with
7 additions
and
14 deletions
Models/ContinuousGraph.v
+
5
−
4
View file @
28f42262
...
@@ -305,7 +305,8 @@ Proof. intro. simpl. repeat (split; try reflexivity). Qed.
...
@@ -305,7 +305,8 @@ Proof. intro. simpl. repeat (split; try reflexivity). Qed.
(
**
**
On
configurations
*
)
(
**
**
On
configurations
*
)
(
**
The
precondition
for
liftable
changes
of
frame
is
that
they
must
come
from
isomorphisms
.
*
)
(
**
The
precondition
for
liftable
changes
of
frame
is
that
they
must
come
from
isomorphisms
(
which
must
not
change
the
thresholds
).
*
)
Global
Instance
InfoV
:
@
State
LocationV
stateV
.
Global
Instance
InfoV
:
@
State
LocationV
stateV
.
simple
refine
{|
simple
refine
{|
get_location
:=
fun
state
=>
fst
(
proj1_sig
state
);
get_location
:=
fun
state
=>
fst
(
proj1_sig
state
);
...
@@ -436,7 +437,7 @@ Defined.
...
@@ -436,7 +437,7 @@ Defined.
Notation
configV
:=
(
@
configuration
_
stateV
_
_
).
Notation
configV
:=
(
@
configuration
_
stateV
_
_
).
Notation
configG
:=
(
@
configuration
_
stateG
_
_
).
Notation
configG
:=
(
@
configuration
_
stateG
_
_
).
(
*
RMK
:
we
cannot
use
map_config
as
the
Location
instance
is
not
the
same
.
*
)
(
*
RMK
:
we
cannot
use
[
map_config
]
here
as
the
Location
instance
is
not
the
same
.
*
)
Definition
config_V2G
(
config
:
configV
)
:
configG
:=
fun
id
=>
state_V2G
(
config
id
).
Definition
config_V2G
(
config
:
configV
)
:
configG
:=
fun
id
=>
state_V2G
(
config
id
).
Global
Instance
config_V2G_compat
:
Proper
(
equiv
==>
equiv
)
config_V2G
.
Global
Instance
config_V2G_compat
:
Proper
(
equiv
==>
equiv
)
config_V2G
.
...
@@ -450,7 +451,7 @@ Proof. intros ? ? Hconfig id. unfold config_G2V. f_equiv. apply Hconfig. Qed.
...
@@ -450,7 +451,7 @@ Proof. intros ? ? Hconfig id. unfold config_G2V. f_equiv. apply Hconfig. Qed.
Lemma
config_V2G2V
:
forall
config
:
configV
,
config_G2V
(
config_V2G
config
)
==
config
.
Lemma
config_V2G2V
:
forall
config
:
configV
,
config_G2V
(
config_V2G
config
)
==
config
.
Proof
.
intros
.
unfold
config_G2V
,
config_V2G
.
now
repeat
try
(
split
;
simpl
).
Qed
.
Proof
.
intros
.
unfold
config_G2V
,
config_V2G
.
now
repeat
try
(
split
;
simpl
).
Qed
.
(
**
The
observation
for
continuous
setting
is
almost
the
same
as
for
the
discrete
one
:
(
**
The
observation
for
the
continuous
setting
is
almost
the
same
as
for
the
discrete
one
:
we
simply
project
robots
on
edges
either
to
the
source
or
target
of
the
edge
we
simply
project
robots
on
edges
either
to
the
source
or
target
of
the
edge
depending
on
where
they
are
located
compared
to
the
threshold
of
the
edge
;
depending
on
where
they
are
located
compared
to
the
threshold
of
the
edge
;
and
add
the
current
location
.
*
)
and
add
the
current
location
.
*
)
...
@@ -501,7 +502,7 @@ intros iso Hstable x. unfold stable_threshold in *. simpl in *.
...
@@ -501,7 +502,7 @@ intros iso Hstable x. unfold stable_threshold in *. simpl in *.
now
rewrite
<-
(
Hstable
x
),
Bijection
.
retraction_section
.
now
rewrite
<-
(
Hstable
x
),
Bijection
.
retraction_section
.
Qed
.
Qed
.
(
**
G
raph
isomorphisms
not
changing
thresholds
as
a
frame
choice
*
)
(
**
Frame
choice
:
g
raph
isomorphisms
not
changing
thresholds
*
)
Global
Instance
FrameChoiceIsomorphismV
:
@
frame_choice
LocationV
(
sig
stable_threshold
)
:=
{|
Global
Instance
FrameChoiceIsomorphismV
:
@
frame_choice
LocationV
(
sig
stable_threshold
)
:=
{|
frame_choice_bijection
:=
fun
f
=>
@
iso_V
locV
E
G
(
proj1_sig
f
);
frame_choice_bijection
:=
fun
f
=>
@
iso_V
locV
E
G
(
proj1_sig
f
);
frame_choice_Setoid
:=
sig_Setoid
(
@
isomorphism_Setoid
locV
E
G
);
frame_choice_Setoid
:=
sig_Setoid
(
@
isomorphism_Setoid
locV
E
G
);
...
...
This diff is collapsed.
Click to expand it.
Models/GraphEquivalence.v
+
0
−
8
View file @
28f42262
...
@@ -156,14 +156,6 @@ Proof.
...
@@ -156,14 +156,6 @@ Proof.
+
intros
config1
config2
Hconfig
gg
g
?
pt1
pt2
Hpt
.
+
intros
config1
config2
Hconfig
gg
g
?
pt1
pt2
Hpt
.
f_equiv
;
try
apply
Hpt
;
[].
f_equiv
;
try
apply
Hpt
;
[].
f_equiv
.
now
apply
(
choose_update_compat
da
);
f_equiv
.
f_equiv
.
now
apply
(
choose_update_compat
da
);
f_equiv
.
(
*
destruct
(
Hconfig
(
Good
g
))
as
[
Hptg
[[
Hsrc
Htgt
]
Hthd
]],
(
proj1_sig
(
config1
(
Good
g
)))
as
[
ptg1
e1
],
(
proj1_sig
(
config2
(
Good
g
)))
as
[
ptg2
e2
].
simpl
in
Hptg
,
Hsrc
,
Htgt
,
Hthd
.
destruct
(
ptg1
=?=
tgt
e1
),
(
ptg2
=?=
tgt
e2
),
(
ptg1
=?=
src
e1
),
(
ptg2
=?=
src
e2
);
solve
[
reflexivity
|
rewrite
Hptg
,
Hsrc
,
Htgt
in
*
;
contradiction
|
now
rewrite
Hthd
,
Hconfig
,
Hpt
].
*
)
+
intros
config1
config2
Hconfig
id1
id2
Hid
.
simpl
in
Hid
.
subst
id1
.
+
intros
config1
config2
Hconfig
id1
id2
Hid
.
simpl
in
Hid
.
subst
id1
.
assert
(
Hpt
:=
Hconfig
id2
).
assert
(
Hpt
:=
Hconfig
id2
).
destruct
Hpt
as
[
Hpt
[[
Hsrc
Htgt
]
Hthd
]],
destruct
Hpt
as
[
Hpt
[[
Hsrc
Htgt
]
Hthd
]],
...
...
This diff is collapsed.
Click to expand it.
Models/RigidFlexibleEquivalence.v
+
1
−
1
View file @
28f42262
...
@@ -59,7 +59,7 @@ Context (Rigid : Rigid.RigidSetting).
...
@@ -59,7 +59,7 @@ Context (Rigid : Rigid.RigidSetting).
Notation
rigid_da
:=
(
@
demonic_action
_
_
_
_
location
(
similarity
location
)
Trigid
_
_
_
).
Notation
rigid_da
:=
(
@
demonic_action
_
_
_
_
location
(
similarity
location
)
Trigid
_
_
_
).
Notation
rigid_demon
:=
(
@
demon
_
_
_
_
location
(
similarity
location
)
Trigid
_
_
_
).
Notation
rigid_demon
:=
(
@
demon
_
_
_
_
location
(
similarity
location
)
Trigid
_
_
_
).
(
**
**
Characterization
of
flexible
demons
that
act
s
rigidly
**
)
(
**
**
Characterization
of
flexible
demons
that
act
rigidly
**
)
(
**
A
flexible
choice
is
rigid
if
its
[
move_ratio
]
is
1.
*
)
(
**
A
flexible
choice
is
rigid
if
its
[
move_ratio
]
is
1.
*
)
Definition
is_rigid
choice
:=
Flexible
.
move_ratio
choice
==
ratio_1
.
Definition
is_rigid
choice
:=
Flexible
.
move_ratio
choice
==
ratio_1
.
...
...
This diff is collapsed.
Click to expand it.
Spaces/Graph.v
+
1
−
1
View file @
28f42262
...
@@ -23,7 +23,7 @@ Class Graph (V E : Type) := {
...
@@ -23,7 +23,7 @@ Class Graph (V E : Type) := {
src
:
E
->
V
;
(
*
source
and
target
of
an
edge
*
)
src
:
E
->
V
;
(
*
source
and
target
of
an
edge
*
)
tgt
:
E
->
V
;
tgt
:
E
->
V
;
threshold
:
E
->
R
;
threshold
:
E
->
R
;
(
*
TODO
:
use
[
strict_ratio
]
instead
?
*
)
threshold_pos
:
forall
e
,
(
0
<
threshold
e
<
1
)
%
R
;
threshold_pos
:
forall
e
,
(
0
<
threshold
e
<
1
)
%
R
;
src_compat
:>
Proper
(
equiv
==>
equiv
)
src
;
src_compat
:>
Proper
(
equiv
==>
equiv
)
src
;
tgt_compat
:>
Proper
(
equiv
==>
equiv
)
tgt
;
tgt_compat
:>
Proper
(
equiv
==>
equiv
)
tgt
;
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
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!
Save comment
Cancel
Please
register
or
sign in
to comment