diff --git a/CaseStudies/Gathering/InR2/Algorithm_withLight.v b/CaseStudies/Gathering/InR2/Algorithm_withLight.v
index 924ef899c4a0860bc58509f8185878d884628470..d88ced1fd6c64c7105cd44f1c297dc2257cf4162 100644
--- a/CaseStudies/Gathering/InR2/Algorithm_withLight.v
+++ b/CaseStudies/Gathering/InR2/Algorithm_withLight.v
@@ -164,7 +164,7 @@ refine {|
Defined.
-(* We are in a rigid formalism with no other info than the location, so the demon makes no choice. *)
+(* We are in a rigid formalism with no other info than the location and color, so the demon makes no choice. *)
Instance Loc : Location := make_Location R2.
Instance VS : RealVectorSpace location := R2_VS.
Instance ES : EuclideanSpace location := R2_ES.
@@ -172,7 +172,6 @@ Instance RobotChoice : robot_choice (location*L) :=
{ robot_choice_Setoid := prod_Setoid location_Setoid L_Setoid }.
Instance ActiveChoice : update_choice unit := NoChoice.
Instance InactiveChoice : inactive_choice unit := { inactive_choice_EqDec := unit_eqdec }.
-(* Instance Info : State location := OnlyLocation (fun _ => True). *)
(* true = white, false = black *)
Instance St : State (location*L) := @WithMultiplicityLight.St _ Lght.
@@ -884,7 +883,6 @@ Local Existing Instance multiset_observation.
Typeclasses eauto := (bfs).
(** The target in the triangle case. *)
-(* TODO: replace [isobarycenter_3_pts] with the general [isobarycenter]. *)
Definition target_triangle (pt1 pt2 pt3 : location) : location :=
let typ := classify_triangle pt1 pt2 pt3 in
match typ with
@@ -1102,14 +1100,13 @@ rewrite <- support_spec, Hin. now right; left.
Qed.
(** The robogram solving the gathering problem in R². *)
-(* Note: If gatherR2_pgm is adapted to this model it should already return a location * L *)
Definition gatherR2_pgmLight (obs : observation) : location * L :=
if bivalent_obs obs
then let other_loc := find_other_loc (fst obs) origin in
if color_bivalent_obs obs
then if observer_lght (snd obs)
then (middle origin other_loc, false)
- else (origin, true) (* was: (other_loc, true) *)
+ else (origin, true)
else let maj_black := find_max_black obs origin other_loc in
(maj_black, observer_lght (snd obs))
else (gatherR2_old_pgm (fst obs), observer_lght (snd obs)).
@@ -1510,7 +1507,7 @@ Qed.
- 4''] Dirty scalene triangle: # robots not on SECT
- 5] Clean generic case (|SEC| ≥ 4): # robots not on target
- 6] Dirty Generic case (|SEC| ≥ 4): # robots not on SECT
- - 7] Bivalent case: no need, durect jump to Majority tower of Gathered
+ - 7] Bivalent case: no need, direct jump to Majority tower of Gathered
- 8] Color bivalent case: # black robots
*)
@@ -3704,36 +3701,6 @@ contradiction.
Qed.
-Lemma forall_ident pred: Forall pred names <-> forall id:ident, pred id.
-Proof using .
- split.
- - intros H id.
- eapply Forall_forall in H;eauto.
- apply In_names.
- - intros H.
- apply Forall_forall.
- intros x H0.
- apply H;auto.
-Qed.
-
-Lemma exists_ident pred: List.Exists pred names <-> exists id:ident, pred id.
-Proof using .
- split.
- - intros H.
- eapply Exists_exists in H;eauto.
- destruct H as [x [hx hx']].
- exists x.
- assumption.
- - intros H.
- destruct H as [x predx].
- apply Exists_exists.
- exists x.
- split.
- + apply In_names.
- + assumption.
-Qed.
-
-
Lemma Exists_decidable :
forall [A : Type] (P : A -> Prop),
(forall x : A, P x \/ ~ P x)
@@ -3804,7 +3771,7 @@ Lemma sub_cb_nb_precondition_wholecolmove_dec id1:
get_location (config id) == get_location (config id1) ->
is_moving gatherR2 da config id).
Proof using .
- rewrite <- forall_ident.
+ rewrite <- Forall_ident.
match goal with
|- Forall ?pred _ \/ _ => destruct (Forall_decidable pred (dec1 id1) names)
end.
@@ -3822,7 +3789,7 @@ Lemma dec3 x:
is_moving gatherR2 da config id) /\ is_moving gatherR2 da config id2).
Proof using .
red.
- rewrite <- exists_ident.
+ rewrite <- Exists_ident.
apply Exists_decidable.
intros x0.
apply Decidable.dec_and.
@@ -3830,7 +3797,7 @@ Proof using .
destruct ((get_location (config x0) =?= get_location (config x)));intuition.
- apply Decidable.dec_and.
+ red.
- rewrite <- forall_ident.
+ rewrite <- Forall_ident.
apply Forall_decidable.
apply dec1.
+ apply is_moving_dec.
@@ -3841,7 +3808,7 @@ Lemma cb_nb_precondition_wholecolmove_dec:
cb_nb_precondition_wholecolmove \/ ~ cb_nb_precondition_wholecolmove .
Proof using .
unfold cb_nb_precondition_wholecolmove.
- setoid_rewrite <- exists_ident.
+ setoid_rewrite <- Exists_ident.
apply Exists_decidable.
intro x.
apply dec3.
@@ -4029,8 +3996,8 @@ destruct (active da) as [| id l] eqn:Hactive.
2:{ red. apply sub_cb_nb_precondition_wholecolmove_dec. }
destruct H.
- left.
- rewrite <- exists_ident.
- rewrite <- forall_ident in H.
+ rewrite <- Exists_ident.
+ rewrite <- Forall_ident in H.
rewrite <- Exists_Forall_neg in H.
+ revert H.
apply Exists_impl.
@@ -4066,7 +4033,7 @@ destruct (active da) as [| id l] eqn:Hactive.
\/ get_location (config id2) == get_location (config id1))).
{ intros id0 id2.
specialize (h_cb_nb_wm id0 id2).
- rewrite <-exists_ident in h_cb_nb_wm.
+ rewrite <-Exists_ident in h_cb_nb_wm.
destruct (Exists_decidable ((fun id : ident =>
get_location (config id) == get_location (config id0) /\ ~ is_moving gatherR2 da config id))) with (l:=names).
{ intros id'.
@@ -4074,16 +4041,16 @@ destruct (active da) as [| id l] eqn:Hactive.
- apply get_location_dec.
- apply Decidable.dec_not.
destruct (is_moving_dec gatherR2 da config id'); now left + right. }
- + left; apply exists_ident;auto.
+ + left; apply Exists_ident;auto.
+ destruct h_cb_nb_wm as [h | [h | h]].
* contradiction.
* right.
split.
- -- rewrite <- exists_ident;auto.
+ -- rewrite <- Exists_ident;auto.
-- now left.
* right.
split.
- -- rewrite <- exists_ident;auto.
+ -- rewrite <- Exists_ident;auto.
-- now right. }
intros id1.
@@ -4260,7 +4227,7 @@ destruct (active da) as [| id l] eqn:Hactive.
\/ ~(exists id'', get_location (config id'') = get_location (config id_move)
/\ ~ is_moving gatherR2 da config id''))
as [[id'' [h_id''_loc h_id''_move]]| h].
- { setoid_rewrite <- exists_ident.
+ { setoid_rewrite <- Exists_ident.
apply Exists_decidable.
intros x.
apply Decidable.dec_and.
@@ -4273,7 +4240,7 @@ destruct (active da) as [| id l] eqn:Hactive.
assumption.
* now apply stationary_moving.
* now apply stationary_moving.
- + rewrite <- exists_ident in h.
+ + rewrite <- Exists_ident in h.
rewrite <- Forall_Exists_neg in h.
changeR2.
assert (Forall (fun x : ident =>
@@ -4414,7 +4381,7 @@ destruct (active da) as [| id l] eqn:Hactive.
\/ ~(exists id'', get_location (config id'') = get_location (config id_move)
/\ ~ is_moving gatherR2 da config id''))
as [[id'' [h_id''_loc h_id''_move]]| h].
- { setoid_rewrite <- exists_ident.
+ { setoid_rewrite <- Exists_ident.
apply Exists_decidable.
intros x.
apply Decidable.dec_and.
@@ -4427,7 +4394,7 @@ destruct (active da) as [| id l] eqn:Hactive.
assumption.
* now apply stationary_moving.
* now apply stationary_moving.
- + rewrite <- exists_ident in h.
+ + rewrite <- Exists_ident in h.
rewrite <- Forall_Exists_neg in h.
changeR2.
assert (Forall (fun x : ident =>
@@ -4496,7 +4463,7 @@ destruct (active da) as [| id l] eqn:Hactive.
/\ get_location (config id_counterexample) = get_location (config id')) as [id_counter [h_counter1 h_counter2]].
{ apply Decidable.dec_not_not.
{ red.
- setoid_rewrite <- exists_ident.
+ setoid_rewrite <- Exists_ident.
apply Exists_decidable.
intros x.
apply Decidable.dec_and.
@@ -7096,6 +7063,75 @@ destruct (gathered_at_dec config (get_location (config (Good g1)))) as [Hmove |
Qed.
+(* *********** UNFAIR DEMON ************** *)
+
+(* Unfairness in terms of gathering: someone always moves if robots
+ are not gathered (and position is valid). *)
+Definition unfair_da_gathering r da config :=
+ (forall pt, ~gathered_at pt config) ->
+ changing r da config <> nil.
+
+Definition unfair_gathering r d config :=
+ Stream.forever2 (Stream.instant2 (unfair_da_gathering r)) d (execute r d config).
+
+(* We link this definition to the usual notion of unfairness:
+ if a robot can move, then some robot moves. *)
+
+Definition sim_da_with_all_activated da : similarity_da.
+Proof using .
+exists (da_with_all_activated da).
+apply (proj2_sig da).
+Defined.
+
+Lemma unfair_da_gather_impl: forall da config,
+ unfair_da gatherR2 (proj_sim_da da) config ->
+ unfair_da_gathering gatherR2 da config.
+Proof using .
+unfold unfair_da, unfair_da_gathering.
+intros da config Hunfair Hgather.
+apply Hunfair.
+destruct (OneMustChange (Good g1) (Hgather (get_location (config (Good g1)))))
+ as [gmove Hgmove].
+assert (Hall : List.In gmove (active (proj_sim_da (sim_da_with_all_activated da)))).
+{ unfold active. simpl. rewrite List.filter_In. auto using In_names. }
+specialize (Hgmove (sim_da_with_all_activated da)
+ (FSYNC_SSYNC_da (da_with_all_activated_FSYNC_da da)) Hall).
+rewrite changing_spec in Hgmove.
+intro Habs. apply no_changing_same_config in Habs. apply Hgmove, Habs.
+Qed.
+
+Lemma unfair_gather_impl : forall d config,
+ unfair gatherR2 (similarity_demon2demon d) config ->
+ unfair_gathering gatherR2 d config.
+Proof using .
+coinduction cfsd.
++ destruct H. clear -H. simpl in *. now apply unfair_da_gather_impl.
++ now destruct H.
+Qed.
+
+(* Final theorem for unfair demons. *)
+Theorem unfair_Gathering_in_R2 : forall (d : similarity_demon) config,
+ SSYNC (d : demon) ->
+ unfair gatherR2 (d : demon) config ->
+ WillGather (execute gatherR2 d config).
+Proof using .
+intros d config Hssync Hunfair'.
+assert (Hunfair : unfair_gathering gatherR2 d config) by now apply unfair_gather_impl.
+clear Hunfair'.
+revert d Hssync Hunfair. pattern config.
+apply (well_founded_ind wf_lt_config). clear config.
+intros config Hind d Hssync Hunfair.
+(* Are we already gathered? *)
+destruct (gathered_at_dec config (get_location (config (Good g1)))) as [Hmove | Hmove].
++ (* If so, not much to do *)
+ apply Stream.Now. exists (get_location (config (Good g1))). now apply gathered_at_OK.
++ (* Otherwise, by assumption on the demon, a robot should move
+ so we can use our well-founded induction hypothesis. *)
+ destruct Hunfair as [Hactive Hunfair], Hssync. hnf in Hactive.
+ apply Stream.Later, Hind; trivial; try (now apply never_bivalent); [].
+ apply round_lt_config; trivial; [].
+ apply Hactive; trivial; []. intros pt Habs. apply Hmove. eapply gathered_precise, Habs.
+Qed.
End GatheringInR2.
(* We prefer calling this from another file, see Algorithm_withLight_ASsumptions.v. *)
diff --git a/CaseStudies/Gathering/InR2/Algorithm_withLight_Assumptions.v b/CaseStudies/Gathering/InR2/Algorithm_withLight_Assumptions.v
index fb7e777e87409836d2e01111551e21e2689a4ae6..ae1cefaf8348e8a000416d087013a51a9affe287 100644
--- a/CaseStudies/Gathering/InR2/Algorithm_withLight_Assumptions.v
+++ b/CaseStudies/Gathering/InR2/Algorithm_withLight_Assumptions.v
@@ -1,2 +1,3 @@
Require Pactole.CaseStudies.Gathering.InR2.Algorithm_withLight.
Print Assumptions InR2.Algorithm_withLight.Gathering_in_R2.
+Print Assumptions InR2.Algorithm_withLight.unfair_Gathering_in_R2.
diff --git a/CaseStudies/Gathering/WithMultiplicityLight.v b/CaseStudies/Gathering/WithMultiplicityLight.v
index 09ea4ea62b35f4a321bf102855c280c0ebaf3811..e003a4a98dafcb47db8889d7458ee0a1bea58e03 100644
--- a/CaseStudies/Gathering/WithMultiplicityLight.v
+++ b/CaseStudies/Gathering/WithMultiplicityLight.v
@@ -46,9 +46,8 @@ Class Lights := {
Section MultisetGathering.
-(** Here, we restrict the state to only contain the location. *)
+(** Here, the state contain the location and the color. *)
Context `{Loc:Location}.
-(* TODO: add the existence of a similarity here *)
Context {Lght : Lights}.
Local Instance St : State (location*L) := AddInfo L (OnlyLocation (fun _ => True)).
@@ -1183,18 +1182,14 @@ specialize (@obs_from_config_fst st config (fst (!!! (config, st))) (snd (!!! (c
assert (Hcase : pt1' == pt1 /\ pt2' == pt2 \/ pt1' == pt2 /\ pt2' == pt1).
{ assert (Hin1 : InA equiv pt1' (pt1 :: pt2 :: nil)).
{ rewrite <- Hsupp, support_spec. unfold In.
- rewrite hfst.
- rewrite Hpt1'.
- destruct (nG+nB) as [| [| nG]] eqn:heqnB ; simpl; try lia.
- set (d := (Nat.div2 nG)).
- lia. }
+ rewrite hfst, Hpt1'.
+ destruct (nG+nB) as [| [| nG]] eqn:heqnB ; simpl;
+ lia || (set (d := (Nat.div2 nG)); lia). }
assert (Hin2 : InA equiv pt2' (pt1 :: pt2 :: nil)).
{ rewrite <- Hsupp, support_spec. unfold In.
- rewrite hfst.
- rewrite Hpt2'.
- destruct (nG+nB) as [| [| nG]] eqn:heqnB; simpl; try lia.
- set (d := (Nat.div2 nG)).
- lia. }
+ rewrite hfst, Hpt2'.
+ destruct (nG+nB) as [| [| nG]] eqn:heqnB; simpl;
+ lia || (set (d := (Nat.div2 nG)); lia). }
rewrite 2 InA_cons, InA_nil in Hin1, Hin2. clear -Hin1 Hin2 Hdiff.
decompose [or] Hin1; decompose [or] Hin2; tauto || elim Hdiff; etransitivity; eauto. }
split.
diff --git a/Core/Formalism.v b/Core/Formalism.v
index 10159f49916154701b9b9c439ad679e4dc0e385c..c3ff4b95fea717649423670796d4cedbd367b991 100644
--- a/Core/Formalism.v
+++ b/Core/Formalism.v
@@ -794,9 +794,9 @@ Proof using . now intros da id. Qed.
(** An unfair demon activates at least one activable robot if such a robot exists. *)
Definition unfair_da r da config :=
- (* If assuming all robots are activated, a robot can move *)
+ (* If assuming all robots are activated, a robot can evolve *)
changing r (da_with_all_activated da) config <> nil ->
- (* then at least a robot moves *)
+ (* then at least a robot evolves *)
changing r da config <> nil.
Definition unfair r d config :=
diff --git a/Core/Identifiers.v b/Core/Identifiers.v
index d6a61b02be35b598c7ca4a47e95addcf00234b1b..6e0f1691f0338358c34ebdc91cc640819065f45f 100644
--- a/Core/Identifiers.v
+++ b/Core/Identifiers.v
@@ -70,6 +70,16 @@ intro r. cbn. unfold names. rewrite in_app_iff. destruct r as [g | b].
- right. apply in_map, In_Bnames.
Qed.
+Corollary Forall_ident `{Names} : forall P, Forall P names <-> forall id, P id.
+Proof using . intro P. rewrite Forall_forall. generalize In_names. intuition. Qed.
+
+Corollary Exists_ident `{Names} : forall P, List.Exists P names <-> exists id, P id.
+Proof using .
+intro P.
+rewrite Exists_exists.
+split; intro Hex; decompose [ex and] Hex; eauto using In_names.
+Qed.
+
Lemma names_NoDup `{Names} : NoDup names.
Proof using .
unfold names. rewrite <- NoDupA_Leibniz. apply (NoDupA_app _).
diff --git a/Observations/MultisetObservation.v b/Observations/MultisetObservation.v
index 73b74e3f98ef4f6530de357a6a6fab4ac5c51305..8e9f7718eabed16205d72177676c3b432824db91 100644
--- a/Observations/MultisetObservation.v
+++ b/Observations/MultisetObservation.v
@@ -241,7 +241,7 @@ Qed.
Lemma obs_from_config_on_loc : forall config st pt,
(obs_from_config config st)[pt] = length (on_loc pt config).
-Proof.
+Proof using .
intros config st pt.
unfold obs_from_config, on_loc. cbn.
rewrite config_list_spec, map_map.
@@ -254,11 +254,11 @@ Qed.
Lemma In_occupied : forall config st pt,
In pt (obs_from_config config st) <-> InA equiv pt (occupied config).
-Proof. intros. now rewrite occupied_spec, obs_from_config_In. Qed.
+Proof using . intros. now rewrite occupied_spec, obs_from_config_In. Qed.
Lemma support_occupied : forall config st,
PermutationA equiv (support (obs_from_config config st)) (occupied config).
-Proof.
+Proof using .
intros. apply NoDupA_equivlistA_PermutationA.
+ autoclass.
+ apply support_NoDupA.
diff --git a/Util/ListComplements.v b/Util/ListComplements.v
index 3bd8d16287945e05154b008300e689b8334013ec..4783c9573bb166489c28f0e935c856839fbb66e6 100644
--- a/Util/ListComplements.v
+++ b/Util/ListComplements.v
@@ -2066,7 +2066,7 @@ Qed.
Global Instance removeA_dups_compat : forall eqA_dec,
Proper (PermutationA eqA ==> PermutationA eqA) (removeA_dups eqA_dec).
-Proof.
+Proof using HeqA.
intros eqA_dec l1 l2 Hperm.
apply NoDupA_equivlistA_PermutationA; trivial; try apply removeA_dups_spec; [].
transitivity l1.