diff --git a/CaseStudies/Gathering/InR2/Weber/Weber_point.v b/CaseStudies/Gathering/InR2/Weber/Weber_point.v
index 110df8cd0b804242f419c8fcf207069838a9525d..f3e9f05fbe0186c2b55d0608e253cf10fce5996a 100644
--- a/CaseStudies/Gathering/InR2/Weber/Weber_point.v
+++ b/CaseStudies/Gathering/InR2/Weber/Weber_point.v
@@ -2722,7 +2722,7 @@ Proof.
apply Rlt_le in h_Rlt_Rabs as h_Rle_Rabs.
apply <- h_weak in h_Rle_Rabs.
clear h_weak.
- split;auto.
+ split;[now auto|].
intros x h_weber.
destruct (equiv_dec x w);auto.
exfalso.
@@ -2822,7 +2822,7 @@ Proof.
rewrite Rabs_minus_sym.
assumption.
Qed.
-
+
Lemma weber_aligned_spec_on_2 L ps w :
ps <> nil -> (* Seems necessary *)
line_dir L =/= 0%VS ->
@@ -2831,7 +2831,76 @@ Lemma weber_aligned_spec_on_2 L ps w :
(0 < ^R (L^on w ps))%R ->
OnlyWeber ps w.
Proof.
-Admitted.
+ intros h_neq_ps_nil h_line_dir h_align h_left_right h_Rlt_onw.
+ specialize (weber_aligned_spec_weak h_line_dir h_align) as h_weak.
+ alias (^R (L ^left) w ps) as leftw after h_neq_ps_nil.
+ alias (^R (L ^right) w ps) as rightw after h_neq_ps_nil.
+ alias (^R (L ^on) w ps) as onw after h_neq_ps_nil.
+ split.
+ { apply h_weak.
+ rewrite Rabs_minus_sym.
+ rewrite h_left_right.
+ rewrite Rabs_R0.
+ lra. }
+ clear h_weak.
+ intros x h_weber.
+ move x before w.
+ destruct (equiv_dec x w);auto.
+ exfalso.
+ apply aligned_on_cons_iff in h_align as h.
+ destruct h as [h_line h_align_ps].
+ assert (aligned_on L (x::ps)) as h_align_ps'.
+ { apply aligned_on_cons_iff.
+ split;auto.
+ eapply weber_aligned;eauto. }
+ specialize (weber_aligned h_neq_ps_nil h_align_ps h_weber) as h_align_x.
+ specialize (weber_aligned_spec_weak_right h_line_dir h_neq_ps_nil h_align_ps h_weber) as h_rabs.
+ alias (^R (L ^left) x ps) as leftx after h_neq_ps_nil.
+ alias (^R (L ^right) x ps) as rightx after h_neq_ps_nil.
+ alias (^R (L ^on) x ps) as onx after h_neq_ps_nil.
+ assert (onx+leftx+rightx = onw+leftw+rightw)%R as h_eq_partition.
+ { specialize (line_left_on_right_partition L x ps) as h1.
+ specialize (line_left_on_right_partition L w ps) as h2.
+ rewrite h1 in h2 at 1.
+ apply PermutationA_length in h2.
+ apply (f_equal INR) in h2.
+ repeat rewrite app_length in h2.
+ repeat rewrite plus_INR in h2.
+ reremember in h2.
+ lra. }
+ assert (L^P x <> L^P w) as h_proj.
+ { intro abs.
+ apply (f_equal (line_proj_inv L)) in abs.
+ rewrite <- h_line in c.
+ rewrite <- h_align_x in c.
+ contradiction. }
+ specialize (Rdichotomy _ _ h_proj) as [h_proj' | h_proj']; clear h_proj.
+ - assert (rightx >= rightw + onw )%R as h_le_rightxw.
+ { unremember.
+ now apply right_lt. }
+ assert (onx >= 0)%R as h_onx_pos.
+ { rewrite Heqonx.
+ apply Rle_ge.
+ apply pos_INR. }
+ assert ((rightx - leftx) <= onx)%R as h_balance.
+ { rewrite Rabs_left1 in h_rabs.
+ - lra.
+ - lra. }
+ lra.
+ - assert (onw > 0)%R by lra.
+ assert (leftx >= leftw + onw )%R.
+ { unremember.
+ now apply left_lt. }
+ assert (rightx <= rightw)%R.
+ { unremember.
+ now apply right_weaker. }
+ assert (leftx > rightx)%R by lra.
+ assert (leftx - rightx <= onx)%R as h_balance.
+ { rewrite Rabs_pos_eq in h_rabs;lra. }
+ clear h_rabs.
+ assert (rightx + onx <= rightw)%R by lra.
+ lra.
+Qed.
Lemma weber_aligned_spec L ps w :
ps <> nil -> (* Seems necessary *)
@@ -2864,387 +2933,78 @@ Proof.
lra. }
Qed.
-(*
- specialize (weber_aligned_spec_weak Hlinedir Halign) as h_weak.
- destruct
- (Rcase_abs ((^R (L ^left) w ps)
- - (^R (L ^right) w ps))%R) as [h_abs| h_abs].
- - apply weber_aligned_spec_right;auto.
- - specialize (@weber_aligned_spec_right (line_reverse L) ps) as hrev.
-
-
- split.
- - intros H.
- destruct H.
- apply h_weak in H.
- destruct (Rle_lt_or_eq_dec _ _ H) as [hlt | h_exact];clear H.
- + auto.
- + exfalso.
- (* WLOG suppose right has more points than left. Thus there
- is at least one point in ps at the right of w. Let us take the closest one p.
- hypothesis (left w - right w = on w) implies that the point w' = (w+p)/2 is such that:
- (left w' - right w' = 0 = on w') because left w' = left w + on w, and right w' = right w.
- so by 1st order spec w' is a weber point distinct from w, which contradict OnlyWeber w. *)
- (* First get rid of the Rabs ,by distinguishing the two cases *)
- destruct
- (Rcase_abs ((^R (L ^left) w ps)
- - (^R (L ^right) w ps))%R) as [h_abs| h_abs];
- [ rewrite (Rabs_left _ h_abs) in h_exact |
- rewrite (Rabs_right _ h_abs) in h_exact].
- *
- remember (L^-P (L^min (L^right w ps))) as w'.
- assert(InA equiv w' ((L ^right) w ps)).
- { subst w'.
- apply line_iP_min_InA.
- - rewrite <- length_zero_iff_nil.
-
- assert (0 <= (INR (length (line_left L w ps))))%R.
- { apply pos_INR. }
- assert (INR (length (line_right L w ps)) > 0)%R as h_lgth.
- { lra. }
- intro abs.
- rewrite abs in h_lgth.
- cbn in h_lgth.
- lra.
- - eapply aligned_on_inclA with (ps':=ps).
- + apply line_right_inclA.
- + rewrite aligned_on_cons_iff in Halign.
- apply Halign. }
- assert(Weber ps w').
- { specialize (bipartition_min L ((L ^right) w ps)) as h.
- apply PermutationA_length in h.
- rewrite app_length in h.
- (* apply (f_equal INR) in h. *)
- (* rewrite plus_INR in h. *)
- (* rewrite <- Heqw' in h. *)
- rewrite <- Heqw' in h.
-
- specialize (line_left_on_right_partition L w ps) as h_w.
- specialize (line_left_on_right_partition L w' ps) as h_w'.
- rewrite h_w' in h_w at 1.
- clear h_w'.
- apply PermutationA_length in h_w.
- rewrite 4 app_length in h_w.
- rewrite weber_aligned_spec_weak with (L:=L);auto.
- 2:{ rewrite aligned_on_cons_iff in *|-*.
- split.
- - subst w'.
- apply line_contains_proj_inv.
- assumption.
- - apply Halign. }
-
- assert ((L ^P) w < (L ^P) w')%R.
- { subst w'.
- rewrite line_P_iP_min.
- (* TODO: have a lemma *)
- assert(InA equiv (L^-P ((L ^min) ((L ^right) w ps)))
- ((L ^right) w ps)).
- { admit. }
- unfold line_right in H1 at 2.
- apply filter_InA in H1.
- 2:{ repeat intro.
- f_equal.
- now rewrite H3. }
- rewrite Rltb_true in H1.
- rewrite line_P_iP_min in H1.
- apply H1.
- }
- rewrite <- aggravate_right in h;auto.
- rewrite <- aggravate_on in h;auto.
- rewrite <- h in h_w.
- apply (f_equal INR) in h, h_w.
- rewrite plus_INR in h,h_w.
- rewrite plus_INR in h_w.
- rewrite plus_INR in h_w.
- (* rewrite <- Heqw' in h. *)
- assert (((^R (L ^left) w' ps) - (^R (L ^right) w' ps)) = (^R (L ^on) w' ps))%R.
- { lra. }
- assert (0 <= (^R (L ^on) w' ps))%R.
- { apply pos_INR. }
- rewrite Rabs_pos_eq;
- lra. }
- assert (abs:w'<>w).
- { specialize (line_right_spec L w w' ps) as h.
- rewrite h in H.
- intro abs.
- rewrite abs in H.
- lra. }
- apply abs.
- now apply H0.
- * remember (L^-P (L^min (L^right w ps))) as w'.
- assert(InA equiv w' ((L ^right) w ps)).
- { subst w'.
- apply line_iP_min_InA.
- - rewrite <- length_zero_iff_nil.
-
- assert (0 <= (INR (length (line_left L w ps))))%R.
- { apply pos_INR. }
- assert (INR (length (line_right L w ps)) > 0)%R as h_lgth.
- { lra. }
- intro abs.
- rewrite abs in h_lgth.
- cbn in h_lgth.
- lra.
- - eapply aligned_on_inclA with (ps':=ps).
- + apply line_right_inclA.
- + rewrite aligned_on_cons_iff in Halign.
- apply Halign. }
- assert(Weber ps w').
- { specialize (bipartition_min L ((L ^right) w ps)) as h.
- apply PermutationA_length in h.
- rewrite app_length in h.
- (* apply (f_equal INR) in h. *)
- (* rewrite plus_INR in h. *)
- (* rewrite <- Heqw' in h. *)
- rewrite <- Heqw' in h.
-
- specialize (line_left_on_right_partition L w ps) as h_w.
- specialize (line_left_on_right_partition L w' ps) as h_w'.
- rewrite h_w' in h_w at 1.
- clear h_w'.
- apply PermutationA_length in h_w.
- rewrite 4 app_length in h_w.
- rewrite weber_aligned_spec_weak with (L:=L);auto.
- 2:{ rewrite aligned_on_cons_iff in *|-*.
- split.
- - subst w'.
- apply line_contains_proj_inv.
- assumption.
- - apply Halign. }
-
- assert ((L ^P) w < (L ^P) w')%R.
- { subst w'.
- rewrite line_P_iP_min.
- (* TODO: have a lemma *)
- assert(InA equiv (L^-P ((L ^min) ((L ^right) w ps)))
- ((L ^right) w ps)).
- { admit. }
- unfold line_right in H1 at 2.
- apply filter_InA in H1.
- 2:{ repeat intro.
- f_equal.
- now rewrite H3. }
- rewrite Rltb_true in H1.
- rewrite line_P_iP_min in H1.
- apply H1.
- }
- rewrite <- aggravate_right in h;auto.
- rewrite <- aggravate_on in h;auto.
- rewrite <- h in h_w.
- apply (f_equal INR) in h, h_w.
- rewrite plus_INR in h,h_w.
- rewrite plus_INR in h_w.
- rewrite plus_INR in h_w.
- (* rewrite <- Heqw' in h. *)
- assert (((^R (L ^left) w' ps) - (^R (L ^right) w' ps)) = (^R (L ^on) w' ps))%R.
- { lra. }
- assert (0 <= (^R (L ^on) w' ps))%R.
- { apply pos_INR. }
- rewrite Rabs_pos_eq;
- lra. }
- assert (abs:w'<>w).
- { specialize (line_right_spec L w w' ps) as h.
- rewrite h in H.
- intro abs.
- rewrite abs in H.
- lra. }
- apply abs.
- now apply H0.
-
-
- *
- *
-
-
-line_left_on_right_partition
-
-
- specialize (@shift_right L w ps Hpsnonnil Hlinedir Halign) as h.
- decompose [sig and] h; clear h.
- rename x into w'.
- apply H5.
- symmetry.
- apply H0.
- apply <- (@weber_aligned_spec_weak L ps w');auto.
- -- rewrite H2.
- rewrite H1.
- rewrite H3.
- cbn .
- rewrite app_length.
- rewrite plus_INR.
- rewrite <- h_exact.
- match goal with
- |- (Rabs ?e <= _)%R => assert ((e = 0)%R)
- end.
- { lra. }
- rewrite H4.
- apply Req_le,Rabs_R0.
- -- rewrite -> (aligned_on_cons_iff _ _ _) in H.
- destruct H.
- apply (aligned_on_cons_iff _ _ _).
- split;auto.
- rewrite -> (aligned_on_cons_iff _ _ _) in Halign.
- apply Halign.
- * specialize (@shift_left L w ps Hpsnonnil Hlinedir Halign) as h.
- decompose [sig and] h; clear h.
- rename x into w'.
- apply H5.
- symmetry.
- apply H0.
- apply <- (@weber_aligned_spec_weak L ps w');auto.
- -- rewrite H2.
- rewrite H1.
- rewrite H3.
- cbn .
- rewrite app_length.
- rewrite plus_INR.
- rewrite <- h_exact.
- match goal with
- |- (Rabs ?e <= _)%R => assert ((e = 0)%R)
- end.
- { lra. }
- rewrite H4.
- apply Req_le,Rabs_R0.
- -- rewrite -> (aligned_on_cons_iff _ _ _) in H.
- destruct H.
- apply (aligned_on_cons_iff _ _ _).
- split;auto.
- rewrite -> (aligned_on_cons_iff _ _ _) in Halign.
- apply Halign.
- -
-
-
-
-
- assert ((^R (L ^right) w ps) - (^R (L ^left) w ps) = (^R (L ^on) w ps))%R.
- { lra. }
-
- rewrite app_length.
- rewrite plus_INR.
- rewrite <- H4.
- rewrite Rplus_minus.
-
- .
- rewrite Rabs_right.
- .
- assert ((Rlength ((L ^left) w ps) + Rlength ((L ^on) w ps)) >= 0).
-
-
- destruct (Rle_lt_dec (^R (L ^left) w ps) (^R (L ^right) w ps)) as [h_le | h_lt].
- destruct (Rle_lt_or_eq_dec _ _ h_le) as [h_lt | h_eq].
- * (* Strictly less points on the left than on the right *)
- specialize h_exact as h_exact_keep.
- rewrite Rabs_left in h_exact.
- assert ((^R (L ^right) w ps) - (^R (L ^left) w ps) = (^R (L ^on) w ps))%R as h_delta.
- { lra. }
- clear h_le h_exact.
- specialize (shift_right Hpsnonnil Hlinedir Halign) as h.
- decompose [and sig] h. clear h.
-
-
- pose (pt := L^-P (line_min L ((L ^right) w ps))%VS).
- pose (w' := middle w pt).
- assert(w =/= w').
- { admit. }
- assert (Weber ps w').
- { apply weber_aligned_spec_weak with (L:=L);auto.
- - apply aligned_on_cons_iff.
- split.
- + apply line_contains_middle.
- * apply Halign.
- intuition.
- * admit. (* by construction of pt? *)
- + rewrite aligned_on_cons_iff in Halign.
- apply Halign.
- -
- intuition.
- intros x H1.
-
- }
- { intro abs.
- apply middle_diff with (ptx:=w)(pty:=pt).
- all:cycle 1.
- - fold w'.
- rewrite abs.
- intuition.
- - admit. (* w' was built for that from the fact pt is L-min w ps *)
-
- specialize middle_diff with (ptx:=w)(pty:=pt) as hmid.
- intro abs.
- apply hmid.
- 2:rewrite abs.
- }
- assert ((^R (L^on w' ps)) == 0)%R.
- {
-
-
-
- rewrite (line_on_length_aligned L _ _ Halign) in e.
-
-
-
- all:swap 1 2.
- - intros Hdelta.
- assert (Weber ps w) as HWeberw.
- { eapply weber_aligned_spec_weak;eauto.
- lra. }
- specialize weber_first_order with (w:=w) (ps:=ps) as hfuw.
-
- red.
- split;auto.
- intros x HWeberx.
- move x at top.
- assert (aligned_on L ps) as Halignps. { eapply aligned_on_cons_iff;eauto. }
- (* assert (aligned_on L (x::ps)) as Halignxps. { } *)
- specialize @weber_aligned with (1:=Hpsnonnil) (3:=HWeberx)(2:=Halignps) as HalignX.
- specialize @weber_aligned with (1:=Hpsnonnil) (3:=HWeberw)(2:=Halignps) as HalignW.
- assert (aligned_on L (x::ps)) as Halignxps.
- { eapply aligned_on_cons_iff; eauto. }
- specialize weber_aligned_spec_weak with (1:=Hlinedir) (2:=Halignxps) as [hx1 _].
- specialize (hx1 HWeberx).
- move hx1 after HWeberw.
- destruct (Rtotal_order (L^P w) (L^P x)) as [Hpw | [Hpw | Hpw]].
- all:swap 2 1.
- + (* x and w are indeed equal *)
- red in HalignX, HalignW.
- rewrite <- Hpw in HalignX.
- transitivity ((L ^-P) ((L ^P) w));auto.
- + (* x is on the right of w. let us see which side of w wins *)
- unfold Rabs in Hdelta.
- destruct (Rcase_abs (INR (Rlength ((L ^left) w ps)) - INR (Rlength ((L ^right) w ps))))
- as [hleftwins|hleftloses].
- all:swap 1 2.
- * (* left of w wins over right *)
- (* then left also wins for x, since it is even more on the right *)
- unfold Rabs in hx1.
- destruct (Rcase_abs (INR (Rlength ((L ^left) x ps)) - INR (Rlength ((L ^right) x ps)))).
- { (* absurd case: w < x so left x >= left w *)
- exfalso.
- unfold line_left,line_right in r.
- assert ().
- }
- specialize weber_aligned_spec_weak with (1:=Hlinedir) (2:=Halign) as hiff.
-
-
-
- assert (InA equiv x ((L ^left) w ps)).
- unfold Rabs in Hdelta.
- destruct (Rcase_abs (INR (Rlength ((L ^left) w ps)) - INR (Rlength ((L ^right) w ps))))
- as [hcase|hcase].
- all:swap 1 2.
- + (* left of w wins over right *)
- (* then left also wins *)
- destruct
- specialize weber_aligned_spec_weak with (1:=Hlinedir) (2:=Halign) as hiff.
-
-
- - admit.
-
-Qed.
-*)
Lemma weber_majority ps w :
countA_occ equiv R2_EqDec w ps > (Nat.div2 (length ps + 1)) -> OnlyWeber ps w.
-Proof. Admitted.
+Proof.
+ intros h_count.
+ assert (Weber ps w) as h_weberw.
+ { apply weber_majority_weak.
+ lia. }
+ destruct (aligned_dec ps) as [h_align | h_nalign].
+ 2:{ apply weber_Naligned_unique;auto. }
+ alias (line_calc ps) as L after h_count.
+ assert (aligned_on L ps) as h_aligned_on.
+ { unremember.
+ now apply line_calc_spec. }
+ assert (ps <>nil) as h_nonnil.
+ { intro abs.
+ rewrite <- length_zero_iff_nil in abs.
+ specialize (countA_occ_length_le equiv R2_EqDec ps w) as h.
+ lia. }
+ destruct (equiv_dec (line_dir L) 0%VS) as [h_eq0 | h_neq0].
+ { assert (forall x : R2, {w == x} + {~ w == x}) as h_dec.
+ { intros x.
+ destruct (R2dec_bool w x) eqn:heq.
+ - rewrite R2dec_bool_true_iff in heq.
+ now left.
+ - rewrite R2dec_bool_false_iff in heq.
+ now right. }
+ edestruct (Forall_dec (equiv w) h_dec ps) as [h_forall | h_nforall].
+ - assert (exists ps', PermutationA equiv ps (w::ps')).
+ { apply PermutationA_split;auto.
+ assert (countA_occ equiv R2_EqDec w ps > 0) by lia.
+ rewrite <- countA_occ_pos;eauto. }
+ destruct H.
+ rewrite H in h_forall.
+ apply weber_gathered in h_forall.
+ rewrite H.
+ assumption.
+ - exfalso.
+ apply neg_Forall_Exists_neg in h_nforall;auto.
+ apply Exists_exists in h_nforall.
+ destruct h_nforall as [e [h_in_e h_neq_e]].
+ assert (InA equiv e ps).
+ { now apply InA_Leibniz. }
+ assert (line_contains L w) as h_contains_w.
+ { apply weber_aligned with ps;auto. }
+ assert (line_contains L e) as h_contains_e.
+ { apply aligned_on_InA_contains with ps;auto. }
+ specialize (line_dir_nonnul L w e h_neq_e h_contains_w h_contains_e) as h.
+ now apply h. }
+ specialize (line_left_on_right_partition L w ps) as h_partition.
+ apply PermutationA_length in h_partition.
+ repeat rewrite app_length in h_partition.
+ assert (aligned_on L (w :: ps)) as h_alignwps.
+ { apply aligned_on_cons_iff.
+ split;auto.
+ apply weber_aligned with ps;auto. }
+ specialize (line_on_length_aligned L w ps h_alignwps) as h_on_countA.
+ assert (Rlength ((L ^left) w ps) + Rlength ((L ^right) w ps) < Nat.div2 (Rlength ps + 1)).
+ { specialize (div2_sum_p1_ge (Rlength ps)) as h_le.
+ lia. }
+ apply weber_aligned_spec with (L:=L);auto.
+ - assert (0 <= (^R (L ^left) w ps) < (^R (L ^on) w ps))%R.
+ { split.
+ - apply pos_INR.
+ - apply lt_INR.
+ lia. }
+ assert (0 <= (^R (L ^right) w ps) < (^R (L ^on) w ps))%R.
+ { split.
+ - apply pos_INR.
+ - apply lt_INR.
+ lia. }
+ apply Rabs_def1;lra.
+Qed.
(* When there are an odd number of points, the weber point is always unique. *)
Lemma weber_odd_unique ps w :