Skip to content
Snippets Groups Projects
Commit ffbc0ddf authored by Sébastien Bouchard's avatar Sébastien Bouchard
Browse files

Merge branch 'master' into prod

# Conflicts:
#	CaseStudies/Exploration/Definitions.v
parents 5fe74db2 fab40648
No related branches found
No related tags found
No related merge requests found
...@@ -22,6 +22,12 @@ Definition is_visited (l : location) (c : configuration) : Prop := ...@@ -22,6 +22,12 @@ Definition is_visited (l : location) (c : configuration) : Prop :=
Definition Will_be_visited (l : location) (e : execution) : Prop := Definition Will_be_visited (l : location) (e : execution) : Prop :=
eventually (instant (is_visited l)) e. eventually (instant (is_visited l)) e.
Definition simple_exploration (e : execution) :=
forall pt, Will_be_visited pt e.
Definition perpetual_exploration (e : execution) :=
Stream.forever simple_exploration e.
(** Eventually, all robots stop moving. *) (** Eventually, all robots stop moving. *)
Definition Stall (e : execution) := hd e == (hd (tl e)). Definition Stall (e : execution) := hd e == (hd (tl e)).
...@@ -34,7 +40,7 @@ Definition Will_stop (e : execution) : Prop := ...@@ -34,7 +40,7 @@ Definition Will_stop (e : execution) : Prop :=
(** [ExplorationStop e] means that after a finite time, every node of the space has been (** [ExplorationStop e] means that after a finite time, every node of the space has been
visited, and after that time, all robots will stay at the same place forever. *) visited, and after that time, all robots will stay at the same place forever. *)
Definition ExplorationStop (e : execution) := Definition ExplorationStop (e : execution) :=
(forall l, Will_be_visited l e) /\ Will_stop e. simple_exploration e /\ Will_stop e.
Global Instance is_visited_compat : Global Instance is_visited_compat :
Proper (equiv ==> equiv ==> iff) is_visited. Proper (equiv ==> equiv ==> iff) is_visited.
...@@ -52,6 +58,16 @@ Proof using . ...@@ -52,6 +58,16 @@ Proof using .
- rewrite He, Hl. exact H. - rewrite He, Hl. exact H.
Qed. Qed.
Global Instance simple_exploration_compat :
Proper (equiv ==> iff) simple_exploration.
Proof using .
intros e1 e2 He. unfold simple_exploration. now setoid_rewrite He.
Qed.
Global Instance perpetual_exploration_compat :
Proper (equiv ==> iff) perpetual_exploration.
Proof using . apply Stream.forever_compat, simple_exploration_compat. Qed.
Global Instance Stall_compat : Proper (equiv ==> iff) Stall. Global Instance Stall_compat : Proper (equiv ==> iff) Stall.
Proof using . Proof using .
intros e1 e2 He. unfold Stall. split; intros H. intros e1 e2 He. unfold Stall. split; intros H.
...@@ -85,5 +101,4 @@ Proof using . ...@@ -85,5 +101,4 @@ Proof using .
+ rewrite He. exact Hs. + rewrite He. exact Hs.
Qed. Qed.
End ExplorationDefs. End ExplorationDefs.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment