Select Git revision
WithMultiplicity.v
WithMultiplicity.v 10.53 KiB
(**************************************************************************)
(* Mechanised Framework for Local Interactions & Distributed Algorithms *)
(* T. Balabonski, P. Courtieu, L. Rieg, X. Urbain *)
(* PACTOLE project *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence. *)
(* *)
(**************************************************************************)
(**************************************************************************)
(** Mechanised Framework for Local Interactions & Distributed Algorithms
T. Balabonski, P. Courtieu, L. Rieg, X. Urbain
PACTOLE project
This file is distributed under the terms of the CeCILL-C licence.
*)
(**************************************************************************)
Require Import Lia PeanoNat.
Require Import SetoidList.
Require Export Pactole.CaseStudies.Gathering.Definitions.
Require Export Pactole.Observations.MultisetObservation.
Close Scope R_scope.
Close Scope VectorSpace_scope.
Set Implicit Arguments.
Typeclasses eauto := (bfs) 5.
(* Require Even. *)
(** Gathering Definitions specific to a setting with multiplicities, i.e. a multiset observation. *)
Section MultisetGathering.
(** Here, we restrict the state to only contain the location. *)
Context `{Location}.
(* TODO: add the existence of a similarity here *)
#[export]Instance Info : State location := OnlyLocation (fun _ => True).
Context {VS : RealVectorSpace location}.
Context {RMS : RealMetricSpace location}.
Context `{Names}.
Context `{robot_choice}.
Context `{update_choice}.
Context `{inactive_choice}.
Context {UpdFun : update_function _ _ _}.
Context {InaFun : inactive_function _}.
#[export] Existing Instance multiset_observation.
Notation "!! config" :=
(@obs_from_config location _ _ _ multiset_observation config origin : observation) (at level 10).
Lemma no_info : forall x y, get_location x == get_location y -> x == y.
Proof using . now intros. Qed.
(** When all robots are on two towers of the same height, there is no solution to the gathering problem.
Therefore, we define these configurations as [invalid]. *)
Definition invalid (config : configuration) :=
Nat.Even nG /\ nG >=2 /\ exists pt1 pt2 : location, pt1 =/= pt2
/\ (!! config)[pt1] = Nat.div2 nG /\ (!! config)[pt2] = Nat.div2 nG.
Global Instance invalid_compat : Proper (equiv ==> iff) invalid.
Proof using .
intros ? ? Heq. split; intros [HnG [Hle [pt1 [pt2 [Hneq Hpt]]]]];
repeat split; trivial; exists pt1, pt2; split; trivial; now rewrite Heq in *.
Qed.
(** [ValidsolGathering r d] means that any possible (infinite)
execution, generated by demon [d] and robogram [r] and any intial configuration not [invalid], will *eventually* be [Gather]ed.
This is the statement used for the correctness proof of the algorithms. *)
Definition ValidSolGathering (r : robogram) (d : demon) :=
forall config : configuration, ~invalid config -> WillGather (execute r d config).
(** ** Generic properties **)
(* We need to unfold [obs_is_ok] for rewriting *)
Definition obs_from_config_spec : forall (config : configuration) (pt : location),
(!! config)[pt] = countA_occ _ equiv_dec pt (List.map get_location (config_list config))
:= fun config => obs_from_config_spec config origin.
Lemma obs_non_nil : 2 <= nG -> forall config,
!! config =/= MMultisetInterface.empty.
Proof using .
simpl obs_from_config. intros HnG config Heq.
assert (Hlgth:= config_list_length config).
assert (Hl : config_list config = nil).
{ apply List.map_eq_nil with _ get_location.
rewrite <- make_multiset_empty.
now intro; rewrite Heq. }
rewrite Hl in Hlgth.
simpl in *.
lia.
Qed.
Lemma invalid_size : nB = 0 ->
forall config : configuration, invalid config -> size (!! config) = 2.
Proof using .
intros HnB config [Heven [HsizeG [pt1 [pt2 [Hdiff [Hpt1 Hpt2]]]]]].
rewrite <- (@cardinal_total_sub_eq _ _ _ _ _ (add pt2 (Nat.div2 nG) (singleton pt1 (Nat.div2 nG)))).
+ rewrite size_add.
destruct (In_dec pt2 (singleton pt1 (Nat.div2 nG))) as [Hin | Hin].
- exfalso. rewrite In_singleton in Hin.
destruct Hin. now contradiction Hdiff.
- rewrite size_singleton; trivial; [].
apply Exp_prop.div2_not_R0. apply HsizeG.
- apply Exp_prop.div2_not_R0. apply HsizeG.
+ intro pt. destruct (pt =?= pt2) as [Heq2 | Heq2], (pt =?= pt1) as [Heq1 | Heq1].
- rewrite Heq1, Heq2 in *. now contradiction Hdiff.
- rewrite add_spec, singleton_spec.
do 2 destruct_match; try contradiction; [].
simpl.
rewrite Heq2.
now apply Nat.eq_le_incl.
- rewrite add_other, singleton_spec; auto; [].
destruct_match; try contradiction; [].
rewrite Heq1.
now apply Nat.eq_le_incl.
- rewrite add_other, singleton_spec; auto; [].
destruct_match; try contradiction; [].
auto with arith.
+ rewrite cardinal_add, cardinal_singleton, cardinal_obs_from_config.
rewrite HnB, Nat.add_0_r. now apply even_div2.
Qed.
Lemma invalid_strengthen : nB = 0 -> forall config, invalid config ->
{ pt1 : location & { pt2 : location | pt1 =/= pt2 & !! config == add pt1 (Nat.div2 nG) (singleton pt2 (Nat.div2 nG)) } }.
Proof using .
intros HnB config Hconfig.
(* Because we want a computational goal and the hypothesis is not,
we first destruct the support to get the elements and only then
prove that they are the same as the one given in [invalid]. *)
assert (Hlen := invalid_size HnB Hconfig). rewrite size_spec in Hlen.
destruct (support (!! config)) as [| pt1 [| pt2 [| ? ?]]] eqn:Hsupp; try discriminate; [].
(* Transforming sig2 into sig to have only one goal after instanciating pt1 and pt2 *)
cut {pt1 : location & {pt2 : location
| pt1 =/= pt2 /\ obs_from_config config origin == add pt1 (Nat.div2 nG) (singleton pt2 (Nat.div2 nG))}}.
{ intros [? [? [? ?]]]. eauto. }
exists pt1, pt2.destruct Hconfig as [Heven [Hge2 [pt1' [pt2' [Hdiff [Hpt1' Hpt2']]]]]].
(* Both couples of points are the same *)
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 Hpt1'.
destruct nG as [| [| nG]]; simpl; solve [ auto with arith | lia]. }
assert (Hin2 : InA equiv pt2' (pt1 :: pt2 :: nil)).
{ rewrite <- Hsupp, support_spec. unfold In. rewrite Hpt2'.
destruct nG as [| [| nG]]; simpl; solve [ auto with arith | lia]. }
rewrite 2 InA_cons, InA_nil in Hin1, Hin2. clear -Hin1 Hin2 Hdiff.
decompose [or] Hin1; decompose [or] Hin2; tauto || contradiction Hdiff; etransitivity; eauto. }
split.
+ intro. apply Hdiff.
decompose [and or] Hcase; repeat (etransitivity; eauto; symmetry).
+ symmetry. apply cardinal_total_sub_eq.
- intro pt. rewrite add_spec, singleton_spec.
repeat destruct_match;
destruct Hcase as [[Heq1 Heq2] | [Heq1 Heq2]];
rewrite Heq1 in *; rewrite Heq2 in *;
try match goal with H : pt == _ |- _ => rewrite H in *; clear H end;
rewrite ?Hpt1', ?Hpt2'; lia || now contradiction Hdiff.
- rewrite cardinal_add, cardinal_singleton, cardinal_obs_from_config, even_div2; auto; lia.
Qed.
Lemma invalid_same_location : nB = 0 -> forall config pt1 pt2 pt3, invalid config ->
In pt1 (!! config) -> In pt2 (!! config) -> In pt3 (!! config) ->
pt1 =/= pt3 -> pt2 =/= pt3 -> pt1 == pt2.
Proof using .
intros HnB config pt1 pt2 pt3 Hinvalid Hin1 Hin2 Hin3 Hdiff13 Hdiff23.
destruct (invalid_strengthen HnB Hinvalid) as [pta [ptb Hdiff Hobs]].
rewrite Hobs, add_In, In_singleton in Hin1, Hin2, Hin3.
destruct Hin1 as [[] | []], Hin2 as [[] | []], Hin3 as [[] | []];
solve [ etransitivity; eauto
| contradiction Hdiff13; etransitivity; eauto
| contradiction Hdiff23; etransitivity; eauto ].
Qed.
Arguments invalid_same_location _ config {pt1} {pt2} pt3 _ _ _ _ _.
Lemma invalid_dec : nB = 0 -> forall config, {invalid config} + {~invalid config}.
Proof using .
intros HnB config.
destruct (size (!! config)) as [| [| [| n]]] eqn:Hsize;
try (right; intro Habs; apply invalid_size in Habs; lia); [].
rewrite size_elements in Hsize.
destruct (elements (!! config)) as [| [pt1 n1] [| [pt2 n2] [| ? ?]]] eqn:Helem;
try discriminate; [].
destruct (n1 =?= n2) as [Hn | Hn].
* left.
assert (2 * n1 = nG).
{ assert (Hcardinal := cardinal_obs_from_config config origin).
rewrite cardinal_fold_elements, Helem in Hcardinal. simpl in Hcardinal.
rewrite <- Hn, HnB in Hcardinal. lia. }
assert (n1 = Nat.div2 nG). { rewrite <- (Exp_prop.div2_double n1). now f_equal. }
split; [| split].
+ now exists n1.
+ cut (0 < n1); try lia; [].
assert (Hin : InA eq_pair (pt1, n1) (elements (!! config))).
{ rewrite Helem. now left. }
rewrite elements_spec in Hin. simpl in Hin. lia.
+ exists pt1, pt2.
hnf in Hn. subst n1 n2.
repeat split.
- assert (Hnodup := elements_NoDupA (!! config)).
rewrite Helem in Hnodup. inv Hnodup. rewrite InA_cons, InA_nil in *.
unfold eq_elt in *. simpl in *. tauto.
- change pt1 with (fst (pt1, Nat.div2 nG)). change (Nat.div2 nG) with (snd (pt1, Nat.div2 nG)) at 2.
eapply proj1. rewrite <- elements_spec.
rewrite Helem. now left.
- change pt2 with (fst (pt2, Nat.div2 nG)). change (Nat.div2 nG) with (snd (pt2, Nat.div2 nG)) at 2.
eapply proj1. rewrite <- elements_spec. rewrite Helem. now right; left.
* right.
intro Hvalid. contradiction Hn.
assert (Hhalf : 0 < Nat.div2 nG).
{ destruct Hvalid as [_ [Hle _]]. destruct nG as [| [| ?]]; simpl; solve [ auto with arith | lia]. }
destruct (invalid_strengthen HnB Hvalid) as [pt1' [pt2' Hdiff Hobs]].
assert (Hperm : PermutationA eq_pair ((pt1, n1) :: (pt2, n2) :: nil)
((pt1', Nat.div2 nG) :: (pt2', Nat.div2 nG) :: nil)).
{ rewrite <- Helem, Hobs. rewrite elements_add, elements_singleton; auto; [].
cbn [removeA]. rewrite singleton_other; trivial; [].
constructor.
+ split; simpl; reflexivity || lia.
+ destruct_match.
- contradiction Hdiff. hnf in * |-; simpl in *. auto.
- reflexivity. }
rewrite PermutationA_2 in Hperm; autoclass; [].
clear -Hperm. destruct Hperm as [[[] []] | [[] []]]; compute in *; congruence.
Qed.
End MultisetGathering.