From 6b86c7c3e270afc131d31a14fefea6a6c47a297d Mon Sep 17 00:00:00 2001
From: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
Date: Fri, 28 Feb 2025 15:46:52 +0100
Subject: [PATCH] Removing calls to libhyps and a few cleaning.

---
 CaseStudies/Gathering/Impossibility.v         |  5 +-
 .../Gathering/InR2/Weber/Gather_flex_async.v  | 88 ++++++++++++-------
 Util/ListComplements.v                        | 10 +++
 Util/SetoidDefs.v                             |  5 ++
 4 files changed, 74 insertions(+), 34 deletions(-)

diff --git a/CaseStudies/Gathering/Impossibility.v b/CaseStudies/Gathering/Impossibility.v
index ac16573c..9d9be381 100644
--- a/CaseStudies/Gathering/Impossibility.v
+++ b/CaseStudies/Gathering/Impossibility.v
@@ -91,8 +91,8 @@ Instance InaFun : inactive_function unit := {
 
 (* Trying to avoid notation problem with implicit arguments *)
 Notation "s [ x ]" := (multiplicity x s) (at level 2, no associativity, format "s [ x ]").
-Notation obs_from_config := (@obs_from_config _ _ _ _ multiset_observation).
-Notation "!! config" := (obs_from_config config origin) (at level 10).
+(* Notation obs_from_confi := (@obs_from_config _ _ _ _ multiset_observation). *)
+Notation "!! config" := (@obs_from_config _ _ _ _ multiset_observation config origin) (at level 10).
 
 (* FIXME: why is this instance not taken from Similarity from Definition *)
 Instance Frame : frame_choice (similarity location) := FrameChoiceSimilarity.
@@ -121,7 +121,6 @@ simpl. destruct n as [| [| ?]].
 - simpl. solve [ auto with arith | lia].
 Qed.
 
-(* We need to unfold [obs_is_ok] for rewriting *)
 Definition obs_from_config_spec : forall config (pt : location),
   (!! config)[pt] = countA_occ _ equiv_dec pt (List.map get_location (config_list config))
   := WithMultiplicity.obs_from_config_spec.
diff --git a/CaseStudies/Gathering/InR2/Weber/Gather_flex_async.v b/CaseStudies/Gathering/InR2/Weber/Gather_flex_async.v
index 7882e3c0..5cdf0a2e 100644
--- a/CaseStudies/Gathering/InR2/Weber/Gather_flex_async.v
+++ b/CaseStudies/Gathering/InR2/Weber/Gather_flex_async.v
@@ -154,22 +154,21 @@ Local Existing Instances dist_sum_compat R2_VS R2_ES.
  * (even when the weber point is not unique).
  * This is a very strong assumption : such a function may not exist in closed form, 
  * and the Weber point can only be approximated. *)
-Axiom weber_calc : list R2 -> R2.
-Axiom weber_calc_correct : forall ps, Weber ps (weber_calc ps).
+(* Axiom weber_calc : list R2 -> R2. *)
+(* Axiom weber_calc_correct : forall ps, Weber ps (weber_calc ps). *)
  (* We also suppose this function doesn't depend on the order of the points. 
  * This is probably not necessary (we can show that it holds when the points aren't colinear) 
  * but simplifies the proof a bit. *)
-Axiom weber_calc_compat : Proper (PermutationA equiv ==> equiv) weber_calc.
-Local Existing Instance weber_calc_compat.
+(* Axiom weber_calc_compat : Proper (PermutationA equiv ==> equiv) weber_calc. *)
+(* Local Existing Instance weber_calc_compat. *)
 
 (* We then build a function that calculates the weber segment of a set of points. *)
-Definition weber_calc_seg : list R2 -> R2 * R2. Admitted.
+Axiom weber_calc_seg : list R2 -> R2 * R2. 
 
-Lemma weber_calc_seg_correct : forall ps,
+Axiom weber_calc_seg_correct : forall ps,
     ps <> [] -> forall w,
     let '(w1, w2) := weber_calc_seg ps in 
     Weber ps w <-> segment w1 w2 w.
-Proof. Admitted.
 Lemma weber_calc_seg_correct_1 : forall ps w1 w2,
     ps <> [] ->
     weber_calc_seg ps = (w1, w2) -> 
@@ -181,8 +180,7 @@ Proof.
   apply h.
 Qed.
 
-Lemma weber_calc_seg_compat : Proper (PermutationA equiv ==> perm_pairA equiv) weber_calc_seg.
-Proof. Admitted.
+Axiom weber_calc_seg_compat : Proper (PermutationA equiv ==> perm_pairA equiv) weber_calc_seg.
 
 Local Existing Instance weber_calc_seg_compat.
 
@@ -324,7 +322,7 @@ Definition flex_da_prop da :=
     get_location (config id) == get_dest (config id) \/ 
     (delta <= dist (get_start (config id)) (get_location (config id)))%R.
 
-(* We are in a flexible and semi-synchronous setting. *)
+(* When a robot perfoms a look-compute, it is reset to ration 0. *)
 Local Instance UpdateF : update_function location (similarity location) unit.
 simple refine {| 
   update config g _ target _ := (get_location (config (Good g)), target, ratio_0)
@@ -362,7 +360,7 @@ Definition pos_list (config : configuration) : list location :=
 
 Lemma pos_list_length config : length (pos_list config) = n.
 Proof using . 
-unfold pos_list. rewrite map_length, config_list_length.
+unfold pos_list. rewrite length_map, config_list_length.
 cbn. now rewrite Nat.add_0_r.
 Qed.
 
@@ -462,26 +460,27 @@ Proof using Type.
     - exists 0%R;lra. }
   rewrite <- (pos_list_length config).
   unfold pos_list.
-  rewrite map_length.
+  rewrite length_map.
   unfold config_list, names.
   rewrite app_length.
   rewrite app_length.
-  rewrite map_length.
-  rewrite map_length.
+  rewrite length_map.
+  rewrite length_map.
   unfold Gpos, Bpos.
-  rewrite map_length.
-  rewrite map_length.
+  rewrite length_map.
+  rewrite length_map.
   reflexivity.
 Qed.
 
 
 Lemma n_nG: n = nG.
-Proof using lt_0n.
+Proof using n.
   rewrite n_nGnB.
   rewrite nB_eq_0.
-  lia.
+  apply Nat.add_0_r.
 Qed.
 
+
 (* I can't use the [invalid] definition from the file WithMultiplicity
  * because it relies on a state that contains only a location.
  * Notice that when [n] is even, [n/2] is the same as [(n+1)/2].
@@ -497,6 +496,33 @@ Proof using .
 intros c1 c2 Hc. unfold invalid. setoid_rewrite Hc. reflexivity.
 Qed.
 
+
+
+(*
+Require Pactole.CaseStudies.Gathering.Impossibility.
+
+(* Lemma build_similarity : forall [pt1 pt2 pt3 pt4 : R2], pt1 =/= pt2 -> pt3 =/= pt4 -> similarity R2. *)
+
+
+Lemma invalid_equivalent:
+  forall c, invalid c <-> WithMultiplicity.invalid c.
+
+Proof.
+  
+Qed.
+
+Definition gather_impossible:
+  Nat.Even n ->
+  forall (r : robogram) (config : configuration),
+    WithMultiplicity.invalid config ->
+    exists d : demon,
+      Fair d /\ ~ WillGather (execute r d config) :=
+  fun heven => (@Pactole.CaseStudies.Gathering.Impossibility.noGathering_Fair
+                  n heven (not_eq_sym (Nat.lt_neq _ _ lt_0n)) _ _ _
+                  build_similarity build_similarity_compat build_similarity_eq1
+                  build_similarity_eq2 build_similarity_inverse).
+*)
+
 (*
 Ltac rename_depth ::= constr:(2).
 *)
@@ -541,6 +567,7 @@ Proof using Type.
     eapply Nat.nle_succ_diag_l;eauto.
 Qed.
 
+
 (* The support of a multiset, but elements are repeated 
  * a number of times equal to their multiplicity. 
  * This is needed to convert an observation from multiset to list format, 
@@ -924,10 +951,8 @@ Lemma elements_subset: forall (o:multiset location) l l',
 Proof using Type.
   intros o l l' hnodup hperm.
   foldR2.
-  
   specialize @from_elements_append with (l1:=l) (l2:=l') as h_all_equiv.
   specialize (h_all_equiv _ _ _ _).
-
   specialize (@union_subset_l _ _ _ _ _ (from_elements l) (from_elements l')) as h_subunion.
   transitivity (union (from_elements l) (from_elements l'));auto.
   specialize (@from_elements_elements _ _ _ _ _ o) as h'''.
@@ -1421,29 +1446,31 @@ Definition gatherW_pgm (obs : observation) : location :=
     else
       let '(w1, w2) := weber_calc_seg (multi_support obs) in
       let L := line_calc (multi_support obs) in 
-      let r1 := L^-P (L^min (multi_support obs)) in 
-      let r2 := L^-P (L^max (multi_support obs)) in
+      let m :=
+        let r1 := L^-P (L^min (multi_support obs)) in 
+        let r2 := L^-P (L^max (multi_support obs)) in        
+        middle r1 r2 in
       (* phase 1 : move to the unique weber point *)   
       if w1 =?= w2 then w1 else 
         (* From now on [n] is even and the robots are aligned 
          * (since the weber point isn't unique). *)
-        (* TODO: add the check that the position is not bivalent,
-    otherwise gatherW_pgm is not compatible with equality on
-    observations. *)
-        (* FIXED: change n with cardinal obs, for respectfulness *)
+        (* We use cardinal obs instead of n, for respectfulness. We
+           also use the fact that robot_with_mult is applied to
+           multi_support obs which always return the same list (not a
+           permutation). *)
         match robot_with_mult (Nat.div2 (cardinal obs +1)) (multi_support obs) with
         | Some t =>
             (* phase 2 : safe move to [t] *)
             if existsb (strict_segment_decb 0%VS t) (multi_support obs) 
             then 0%VS else t
         | None =>
-            if segment_decb w1 w2 (middle r1 r2) then 
+            if segment_decb w1 w2 m then 
               (* phase 3 : robots on [w1] or [w2] move to the middle *)
-              if (w1 ==b 0%VS) || (w2 ==b 0%VS) then middle r1 r2 else 0%VS
-            else if segment_decb (middle r1 r2) w1 w2 then 
+              if (w1 ==b 0%VS) || (w2 ==b 0%VS) then m else 0%VS
+            else if segment_decb m w1 w2 then 
                    (* phase 4 : robots on [w1] move to [w2] *)
                    if w1 ==b 0%VS then w2 else 0%VS 
-                 else if segment_decb (middle r1 r2) w2 w1 then
+                 else if segment_decb m w2 w1 then
                         (* also phase 4 : robots on [w2] move to [w1] *)
                         if w2 ==b 0%VS then w1 else 0%VS
                       else 
@@ -5235,5 +5262,4 @@ case (inv_initial Hvalid Hstay) as [Hinv1 | [Hinv2 | [Hinv3 | Hinv4]]].
 + destruct Hinv3 as [L [w1 [w2 Hinv3]]]. eapply phase3_correct ; eauto.
 + destruct Hinv4 as [L [w1 [w2 Hinv4]]]. eapply phase4_correct ; eauto.
 Qed.  
-
 End Gathering.
diff --git a/Util/ListComplements.v b/Util/ListComplements.v
index 6edbe17c..9bd172c4 100644
--- a/Util/ListComplements.v
+++ b/Util/ListComplements.v
@@ -1463,6 +1463,8 @@ Section CountA.
 Context (A : Type).
 Context (eqA : relation A).
 Context (HeqA : Equivalence eqA).
+(* Context [eqA : relation A].
+   Context {HeqA : Equivalence eqA}. *)
 Hypothesis eq_dec : forall x y : A, {eqA x y} + {~eqA x y}.
 
 Fixpoint countA_occ (x : A) l :=
@@ -1495,6 +1497,7 @@ intros a b Hab l. induction l as [| x l]; intros [| x' l'] Hl.
   - contradiction Hx. now rewrite Hxy, Hab.
 Qed.
 
+
 Lemma countA_occ_alls_in : forall x n, countA_occ x (alls x n) = n.
 Proof using HeqA.
 intros x n. induction n; simpl; trivial.
@@ -1637,6 +1640,13 @@ Qed.
 
 End CountA.
 
+(* Global Instance countA_occ_compat_setoid A {S:Setoid A} {D:EqDec S}:  *)
+(*   Proper (@equiv _ S ==> PermutationA equiv ==> eq) (countA_occ D). *)
+(* Proof using . *)
+(*   apply countA_occ_compat. *)
+(*   autoclass. *)
+(* Qed. *)
+
 Lemma countA_occ_map {A B} (eqA : relation A) (eqB : relation B) Aeq_dec Beq_dec :
   forall (f : A -> B), Proper (eqA ==> eqB) f -> injective eqA eqB f ->
   forall x l, countA_occ eqB Beq_dec (f x) (map f l) = countA_occ eqA Aeq_dec x l.
diff --git a/Util/SetoidDefs.v b/Util/SetoidDefs.v
index 7308e14c..2a6d5ab9 100644
--- a/Util/SetoidDefs.v
+++ b/Util/SetoidDefs.v
@@ -50,6 +50,11 @@ Lemma equiv_dec_refl {T U} {S : Setoid T} {E : EqDec S} :
   forall (e : T) (A B : U), (if equiv_dec e e then A else B) = A.
 Proof using . intros. destruct_match; intuition auto with *. Qed.
 
+Lemma equiv_dec_other {T U : Type} {S : Setoid T} {E : EqDec S}:
+  forall (e e': T) (A B : U), e=/= e' -> (if equiv_dec e e' then A else B) = B.
+Proof using . intros. destruct_match; intuition auto with *. Qed.
+
+
 (** **  Setoid Definitions  **)
 
 Instance fun_Setoid A B `(Setoid B) : Setoid (A -> B) | 4.
-- 
GitLab