diff --git a/CaseStudies/Gathering/InR2/Weber/Weber_point.v b/CaseStudies/Gathering/InR2/Weber/Weber_point.v index 683e21372b4cba61e03727330a0d5bd03c200c99..a268413a98f2c3456ffe23544b0bc62d0e96423c 100644 --- a/CaseStudies/Gathering/InR2/Weber/Weber_point.v +++ b/CaseStudies/Gathering/InR2/Weber/Weber_point.v @@ -2652,6 +2652,354 @@ Proof. constructor;auto. Qed. +Lemma weber_nonunique_segment_l L ps x w: + ps <> nil -> + aligned_on L ps -> + Weber ps w -> + Weber ps x -> + (L ^P x < L ^P w)%R -> + (0 < ^R (L^on x ps))%R -> + (0 < ^R (L^on w ps))%R -> + forall m, + line_contains L m + -> (L ^P x < L ^P m)%R + -> (L ^P m < L ^P w)%R + -> Weber ps m /\ ((^R (L ^on) m ps) = 0)%R. +Proof. + intros h_nonnil h_aligned_on h_weber_w h_weber_x h_proj' h_x_gt0 h_w_gt0 + m h_contain_m h_ltxm h_lt_mw. + alias (^R (L ^left) m ps) as leftm after h_nonnil. + alias (^R (L ^right) m ps) as rightm after h_nonnil. + alias (^R (L ^on) m ps) as onm after h_nonnil. + alias (^R (L ^left) w ps) as leftw after h_nonnil. + alias (^R (L ^right) w ps) as rightw after h_nonnil. + alias (^R (L ^on) w ps) as onw after h_nonnil. + alias (^R (L ^left) x ps) as leftx after h_nonnil. + alias (^R (L ^right) x ps) as rightx after h_nonnil. + alias (^R (L ^on) x ps) as onx after h_nonnil. + assert (0<=leftw)%R as h_lwpos by (unremember; apply pos_INR). + assert (0<=leftx)%R as h_lxpos by (unremember; apply pos_INR). + assert (0<=rightw)%R as h_rwpos by (unremember; apply pos_INR). + assert (0<=rightx)%R as h_rxpos by (unremember; apply pos_INR). + assert (0<=leftm)%R as h_lmpos by (unremember; apply pos_INR). + assert (0<=rightm)%R as h_rmpos by (unremember; apply pos_INR). + assert (0<=onm)%R as onmpos by (unremember; apply pos_INR). + + specialize (weber_aligned h_nonnil h_aligned_on h_weber_w) as ha_align_w. + specialize (weber_aligned h_nonnil h_aligned_on h_weber_x) as ha_align_x. + assert ((aligned_on L (w::ps))) as h_align_wps. + { apply aligned_on_cons_iff;split;auto. } + assert ((aligned_on L (x::ps))) as h_align_xps. + { apply aligned_on_cons_iff;split;auto. } + assert (x=/=w) as h_neqxw. + { intros abs. + rewrite abs in h_proj'. + lra. } + assert (L^P x <> L^P w) as h_proj. + { intro abs. + apply (f_equal (line_proj_inv L)) in abs. + rewrite <- ha_align_w, <-ha_align_x in h_neqxw. + contradiction. } + assert (line_dir L =/= 0%VS) as h_dir_nonnull. + { apply line_dir_nonnul with x w;auto. } + dup h_weber_x. + apply (@weber_aligned_spec_weak L ps x h_dir_nonnull h_align_xps) in h_weber_x'. + reremember in h_weber_x'. + assert (leftx + onx + rightx = leftw + onw + rightw)%R as h_eq_xw. + { transitivity (^R ps). + - rewrite (line_left_on_right_partition L x ps). + repeat rewrite app_length. + repeat rewrite plus_INR. + reremember;lra. + - rewrite (line_left_on_right_partition L w ps). + repeat rewrite app_length. + repeat rewrite plus_INR. + reremember;lra. } + + assert (leftw + onw + rightw = leftm + onm + rightm)%R. + { transitivity (^R ps). + - rewrite (line_left_on_right_partition L w ps). + repeat rewrite app_length. + repeat rewrite plus_INR. + reremember;lra. + - rewrite (line_left_on_right_partition L m ps). + repeat rewrite app_length. + repeat rewrite plus_INR. + reremember;lra. } + assert (leftx + onm <= leftw)%R. + { subst leftx leftw onm. + transitivity ((^R (L ^left) m ps) + (^R (L ^on) m ps))%R. + - apply Rplus_le_compat_r. + apply left_weaker. + assumption. + - apply Rge_le. + apply left_lt;lra. } + assert (rightw + onm <= rightx)%R. + { subst rightw rightx onm. + transitivity ((^R (L ^right) m ps) + (^R (L ^on) m ps))%R. + - apply Rplus_le_compat_r. + apply right_weaker. + assumption. + - apply Rge_le. + apply right_lt;lra. } + assert (rightm >= rightw + onw)%R. + { subst rightm rightw onw. + apply right_lt;lra. } + assert (leftm >= leftx + onx)%R. + { subst leftm onx leftx. + apply left_lt;lra. } + assert (~Rabs(leftx - rightx) < onx)%R as h_lt_balancex. + { intro abs. + unremember in abs. + apply <- weber_aligned_spec in abs;auto; reremember;auto. + red in abs. + destruct abs as [ _ h_uniq]. + apply h_neqxw;auto. + symmetry;auto. } + assert (~Rabs(leftw - rightw) < onw)%R as h_lt_balancew. + { intro abs. + unremember in abs. + apply <- weber_aligned_spec in abs;auto; reremember;auto. + red in abs. + destruct abs as [ _ h_uniq]. + apply h_neqxw;auto. } + assert (Rabs (leftx - rightx) = onx)%R as h_equilib_x by lra. + dup h_weber_w. + apply (@weber_aligned_spec_weak L ps w h_dir_nonnull h_align_wps) in h_weber_w'. + reremember in h_weber_w'. + assert (Rabs (leftw - rightw) = onw)%R as h_equilib_w by lra. + + rewrite Rabs_left1 in h_equilib_x. + 2:{ destruct (Rle_lt_dec leftx rightx);try lra. + exfalso. + rewrite Rabs_right in h_equilib_w; try lra. } + rewrite Rabs_right in h_equilib_w; try lra. + split;[|lra]. + apply (@weber_aligned_spec_weak L);auto; auto. + - apply aligned_on_cons_iff;auto. + - reremember. + apply Rabs_le;lra. +Qed. + +Lemma weber_nonunique_segment L ps x w: + ps <> nil -> + aligned_on L ps -> + Weber ps w -> + Weber ps x -> + (L ^P x <> L ^P w)%R -> + (0 < ^R (L^on x ps))%R -> + (0 < ^R (L^on w ps))%R -> + forall m, + line_contains L m (* FIXME: should not be needed *) + -> strict_segment x w m + -> Weber ps m /\ ((^R (L ^on) m ps) = 0)%R. +Proof. + intros h_nonnil h_aligned_on h_weber_w h_weber_x h_diff_xw h_x_gt0 h_w_gt0 m h_contains_m h_strict_seg. + specialize (weber_aligned h_nonnil h_aligned_on h_weber_w) as ha_align_w. + specialize (weber_aligned h_nonnil h_aligned_on h_weber_x) as ha_align_x. + dup h_strict_seg. + rewrite (strict_segment_line L x w m) in h_strict_seg';auto. + destruct h_strict_seg as [h_seg _]. + destruct h_strict_seg' as [h_ineq | h_ineq]. + - destruct h_ineq as [h_lt_xm h_lt_mw]. + assert (((L ^P) x < (L ^P) w)%R) as h_lt_xw by lra. + apply (weber_nonunique_segment_l h_nonnil h_aligned_on h_weber_w h_weber_x h_lt_xw + h_x_gt0 h_w_gt0 h_contains_m h_lt_xm h_lt_mw). + - destruct h_ineq as [h_lt_wm h_lt_mx]. + assert (((L ^P) w < (L ^P) x)%R) as h_lt_wx by lra. + apply (weber_nonunique_segment_l h_nonnil h_aligned_on h_weber_x h_weber_w h_lt_wx + h_w_gt0 h_x_gt0 h_contains_m h_lt_wm h_lt_mx). +Qed. + +(* +Lemma foo (x y m: R2): segment x y (middle x y) . +Proof. + remember (x::y::nil) as ps. + remember (line_calc ps) as L. + assert (ps <> nil) as h_nonnil. + { now intro abs;subst. } + assert (aligned ps) as h_align_ps. + { unremember. + apply aligned_spec. + exists (y-x)%VS. + intros p H. + apply InA_singleton in H. + rewrite H. + exists 1%R. + rewrite mul_1. + symmetry. + apply add_sub. } + assert (line_contains L x) as h_line_x. + { apply aligned_on_InA_contains with (ps:=ps);auto. + + unremember. + auto. + + unremember. + unremember in h_align_ps. + apply line_calc_spec;auto. } + assert (line_contains L y) as h_line_y. + { apply aligned_on_InA_contains with (ps:=ps);auto. + + unremember. + auto. + + unremember. + unremember in h_align_ps. + apply line_calc_spec;auto. } + + dup h_align_ps. + rewrite (line_calc_spec ps) in h_align_ps'. + reremember in h_align_ps'. + specialize (line_iP_min_InA L ps h_nonnil h_align_ps') as h_min. + specialize (line_iP_max_InA L ps h_nonnil h_align_ps') as h_max. + + apply (line_min_max_spec L (middle x y::ps)). + { intro abs. + discriminate. } + 3:{ auto. } + - admit. + - red. + specialize (line_middle L (middle x y :: ps)) as h_mid. + + + assert (((L ^min) ps) = (L^P) x /\ (L ^max) ps = (L ^P) y \/ ((L ^min) ps) = ((L^P) y) /\ (L ^max) ps = (L ^P) x). + { rewrite Heqps in h_min at 2. + rewrite Heqps in h_max at 2. + rewrite InA_cons in h_min,h_max. + rewrite InA_cons in h_min,h_max. + rewrite InA_nil in h_min,h_max. + + assert (InA equiv x ps) as h_in_x. + { unremember; auto. } + assert (InA equiv y ps) as h_in_y. + { unremember; auto. } + + specialize (line_bounds L ps x h_in_x) as h_inx. + specialize (line_bounds L ps y h_in_y) as h_iny. + + destruct h_min as [h_min | [h_min | abs]]; try contradiction; + destruct h_max as [h_max | [h_max | abs]]; try contradiction. + - assert ((L ^-P) ((L ^min) ps) = x) as h_min' by auto. + assert ((L ^-P) ((L ^max) ps) = x) as h_max' by auto. + rewrite <- h_max' in h_inx. + rewrite line_P_iP_max in h_inx. + assert ((L ^P) x = (L ^P) y). + { subst x. + + lra. } + left. + +. + + specialize (line_min_le_max L ps) as h_minmax. + admit. } + destruct H as [ [h_min_x h_max_y] | [h_min_y h_max_x]]. + - rewrite h_min_x,h_max_y in h_mid. + red. + exists (1/2)%R. + split; try lra. + assert ((1 - 1 / 2 = 1/2)%R). + { lra. } + rewrite H. + transitivity (1 / 2 * (x + y))%VS. + 2:{ apply mul_distr_add. } + reflexivity. + - rewrite h_min_y,h_max_x in h_mid. + red. + exists (1/2)%R. + split; try lra. + assert ((1 - 1 / 2 = 1/2)%R). + { lra. } + rewrite H. + transitivity (1 / 2 * (x + y))%VS. + 2:{ apply mul_distr_add. } + reflexivity. + + + + +Lemma foo (x y m: R2): segment x y (middle x y) . +Proof. + remember (x::y::nil) as ps. + remember (line_calc ps) as L. + assert (aligned ps). + { unremember. + apply aligned_spec. + exists (y-x)%VS. + intros p H. + apply InA_singleton in H. + rewrite H. + exists 1%R. + rewrite mul_1. + symmetry. + apply add_sub. } + assert (line_contains L x). + { apply aligned_on_InA_contains with (ps:=ps);auto. + + unremember. + auto. + + unremember. + unremember in H. + apply line_calc_spec;auto. } + assert (line_contains L y). + { apply aligned_on_InA_contains with (ps:=ps);auto. + + unremember. + auto. + + unremember. + unremember in H. + apply line_calc_spec;auto. } + assert (line_contains L (middle x y)). + { apply line_contains_middle;auto. } + + apply (segment_line L);auto. + destruct (Rle_dec ((L ^P) x) ( (L ^P) y));[left|right]. + - split. + + cbn. + unremember. + cbn. + destruct (equiv_dec x y);cbn. + * simpl. + repeat rewrite Rmult_0_r. + lra. + * repeat rewrite Rmult_plus_distr_r. + repeat rewrite Rmult_plus_distr_l. + repeat rewrite Rmult_plus_distr_r. + remember (fst x) as a. + remember (fst y) as b. + remember (snd x) as d. + remember (snd y) as e. + repeat rewrite Ropp_mult_distr_r_reverse. + repeat rewrite Ropp_mult_distr_l_reverse. + repeat rewrite Ropp_involutive. + repeat rewrite Ropp_mult_distr_l_reverse. + assert (a * b + - (a * a) + (- (a * b) + a * a) = 0)%R as h_simpl_1. + { lra. } + assert (d * e + - (d * d) + (- (d * e) + d * d) = 0)%R as h_simpl_2. + { lra. } + rewrite h_simpl_1, h_simpl_2. + setoid_rewrite Rplus_comm at 8. + setoid_rewrite Rplus_assoc at 3. + setoid_rewrite Rplus_comm at 6. + setoid_rewrite Rplus_assoc at 3. + setoid_rewrite <- Rplus_assoc at 3. + assert ((1 / 2 * a * b) + - (1 / 2 * b * a) = 0)%R as h_simpl_3 . + { admit. + } + setoid_rewrite h_simpl_3. + + assert ((- (1 / 2 * a * a) + 1 / 2 * b * b) + (- (a * b) + a * a) == 1/2 * ((a + -b)* (a+ -b)))%R. + { setoid_rewrite Rmult_plus_distr_r. + repeat setoid_rewrite Rmult_plus_distr_l. + (* setoid_rewrite Rmult_plus_distr_l. *) + (* setoid_rewrite Rmult_plus_distr_r. *) + admit. } + admit. + + admit. + - admit. +Admitted. + +Lemma bar (x y m: R2): x<>y -> strict_segment x y (middle x y) . +Proof. + +Admitted. +*) + (* When there are an odd number of points, the weber point is always unique. *) Lemma weber_odd_unique ps w : Nat.Odd (length ps) -> Weber ps w -> OnlyWeber ps w. @@ -2673,7 +3021,8 @@ Proof. 2:{ apply weber_Naligned_unique;auto. } split;auto. intros x h_weber_x. - destruct (equiv_dec x w);auto. + move x at top. + destruct (equiv_dec x w) as [ | h_neqxw ];auto. exfalso. alias (line_calc ps) as L after h_weber_w. assert (aligned_on L ps) as h_aligned_on. @@ -2681,55 +3030,264 @@ Proof. now apply line_calc_spec. } specialize (weber_aligned h_nonnil h_aligned_on h_weber_w) as ha_align_w. specialize (weber_aligned h_nonnil h_aligned_on h_weber_x) as ha_align_x. - assert ((aligned_on L (w::ps))). - { apply aligned_on_cons_iff;split;auto. } - assert ((aligned_on L (x::ps))). - { apply aligned_on_cons_iff;split;auto. } assert (line_dir L =/= 0%VS) as h_dir_nonnull. { apply line_dir_nonnul with x w;auto. } + assert (L^P x <> L^P w) as h_proj. + { intro abs. + apply (f_equal (line_proj_inv L)) in abs. + rewrite <- ha_align_w, <-ha_align_x in h_neqxw. + contradiction. } + alias (^R (L ^left) w ps) as leftw after h_Odd_ps. + alias (^R (L ^right) w ps) as rightw after h_Odd_ps. + alias (^R (L ^on) w ps) as onw after h_Odd_ps. + alias (^R (L ^left) x ps) as leftx after h_Odd_ps. + alias (^R (L ^right) x ps) as rightx after h_Odd_ps. + alias (^R (L ^on) x ps) as onx after h_Odd_ps. +(* + assert (exists pt, Weber ps pt /\ ((^R (L ^on) pt ps) = 0)%R) as h_ex_pt. + { specialize (Rdichotomy _ _ h_proj) as [h_proj' | h_proj'];clear h_proj. + - destruct (equiv_dec onw 0)%R as [? | h_w_neq0]. + { exists w;subst onw;auto. } + destruct (equiv_dec onx 0)%R as [? | h_x_neq0]. + { exists x;subst onx;auto. } + assert (0 < onx)%R as h_x_gt0. + { assert (onx <> 0 /\ onx >= 0)%R;try split;try lra. + - assumption. + - unremember. + apply Rle_ge , pos_INR. } + assert (0 < onw)%R as h_w_gt0. + { assert (onw <> 0 /\ onw >= 0)%R;try split;try lra. + - assumption. + - unremember. + apply Rle_ge , pos_INR. } + clear h_w_neq0 h_x_neq0. + assert ((L ^P) x <> (L ^P) w)%R as h_diff_xw by lra. + specialize (weber_nonunique_segment h_nonnil h_aligned_on h_weber_w h_weber_x h_diff_xw) as h. + reremember in h. + specialize (h h_x_gt0 h_w_gt0). + exists (middle x w). + assert (line_contains L (middle x w)). + { apply line_contains_middle;auto. } + apply h;auto. + apply bar;auto. + - + +*) + assert ((aligned_on L (w::ps))) as h_align_wps. + { apply aligned_on_cons_iff;split;auto. } + assert ((aligned_on L (x::ps))) as h_align_xps. + { apply aligned_on_cons_iff;split;auto. } + (* assert (line_dir L =/= 0%VS) as h_dir_nonnull. *) + (* { apply line_dir_nonnul with x w;auto. } *) dup h_weber_w. rewrite -> (@weber_aligned_spec_weak L) in h_weber_w';auto. - assert (exists pt, Weber ps pt /\ ((^R (L ^on) pt ps) = 0)%R). - { destruct (equiv_dec (^R (L ^on) w ps) 0)%R. - - exists w;auto. - - destruct (equiv_dec (^R (L ^on) x ps) 0)%R. - + exists x;auto. - + assert (forall m, - (L ^P x < L ^P m)%R - -> (L ^P m < L ^P w)%R - -> Weber ps m /\ ((^R (L ^on) m ps) = 0)%R). - { intros m H1 H2. - alias (^R (L ^left) w ps) as leftw after h_Odd_ps. - alias (^R (L ^right) w ps) as rightw after h_Odd_ps. - alias (^R (L ^on) w ps) as onw after h_Odd_ps. - alias (^R (L ^left) x ps) as leftx after h_Odd_ps. - alias (^R (L ^right) x ps) as rightx after h_Odd_ps. - alias (^R (L ^on) x ps) as onx after h_Odd_ps. - alias (^R (L ^left) m ps) as leftm after h_Odd_ps. - alias (^R (L ^right) m ps) as rightm after h_Odd_ps. - alias (^R (L ^on) m ps) as onm after h_Odd_ps. - assert(leftx - rightx = onx)%R by admit. - assert (rightw - leftw = onw)%R by admit. - assert (leftx + onx + rightx = leftw + onw + rightw)%R by admit. - assert (leftw + onw + rightw = leftm + onm + rightm)%R by admit. - assert (rightm >= rightx + onx)%R by admit. - assert (leftm >= onw + leftw)%R by admit. - assert(0 <= onm)%R by admit. - assert (leftm - rightm <= onm)%R. - { lra. } - assert (onm = 0)%R. - lra. - split; try lra. - apply (@weber_aligned_spec_weak L);auto; try lra. - - admit. - - reremember. - admit. } - exists (middle w x). - destruct (H1 (middle w x));auto. - { admit. } - { admit. } - } - destruct H1 as [pt [hpt1 hpt2]]. + reremember in h_weber_w'. + assert (0<=leftw)%R as h_lwpos by (unremember; apply pos_INR). + assert (0<=leftx)%R as h_lxpos by (unremember; apply pos_INR). + assert (0<=rightw)%R as h_rwpos by (unremember; apply pos_INR). + assert (0<=rightx)%R as h_rxpos by (unremember; apply pos_INR). + dup h_weber_x. + apply (@weber_aligned_spec_weak L ps x h_dir_nonnull h_align_xps) in h_weber_x'. + reremember in h_weber_x'. + assert (~Rabs(leftx - rightx) < onx)%R as h_lt_balancex. + { intro abs. + unremember in abs. + apply <- weber_aligned_spec in abs;auto; reremember;auto. + red in abs. + destruct abs as [ _ h_uniq]. + apply h_neqxw;auto. + symmetry;auto. } + assert (~Rabs(leftw - rightw) < onw)%R as h_lt_balancew. + { intro abs. + unremember in abs. + apply <- weber_aligned_spec in abs;auto; reremember;auto. + red in abs. + destruct abs as [ _ h_uniq]. + apply h_neqxw;auto. } + assert (Rabs (leftx - rightx) = onx)%R as h_equilib_x by lra. + assert (Rabs (leftw - rightw) = onw)%R as h_equilib_w by lra. + clear h_weber_w' h_weber_x' h_lt_balancex h_lt_balancew. + assert (exists pt, Weber ps pt /\ ((^R (L ^on) pt ps) = 0)%R) as h_ex_pt. + { specialize (Rdichotomy _ _ h_proj) as [h_proj' | h_proj'];clear h_proj. + - destruct (equiv_dec onw 0)%R as [? | h_w_neq0]. + { exists w;subst onw;auto. } + destruct (equiv_dec onx 0)%R as [? | h_x_neq0]. + { exists x;subst onx;auto. } + assert (0 < onx)%R as h_x_gt0. + { assert (onx <> 0 /\ onx >= 0)%R;try split;try lra. + - assumption. + - unremember. + apply Rle_ge , pos_INR. } + assert (0 < onw)%R as h_w_gt0. + { assert (onw <> 0 /\ onw >= 0)%R;try split;try lra. + - assumption. + - unremember. + apply Rle_ge , pos_INR. } + clear h_w_neq0 h_x_neq0. + assert (forall m, + line_contains L m + -> (L ^P x < L ^P m)%R + -> (L ^P m < L ^P w)%R + -> Weber ps m /\ ((^R (L ^on) m ps) = 0)%R) as h_segment_weber. + { intros m h_contain_m h_ltxm h_lt_mw. + alias (^R (L ^left) m ps) as leftm after h_Odd_ps. + alias (^R (L ^right) m ps) as rightm after h_Odd_ps. + alias (^R (L ^on) m ps) as onm after h_Odd_ps. + assert (0<=leftm)%R as h_lmpos by (unremember; apply pos_INR). + assert (0<=rightm)%R as h_rmpos by (unremember; apply pos_INR). + assert (0<=onm)%R as onmpos by (unremember; apply pos_INR). + assert (leftx + onx + rightx = leftw + onw + rightw)%R as h_eq_xw. + { transitivity (^R ps). + - rewrite (line_left_on_right_partition L x ps). + repeat rewrite app_length. + repeat rewrite plus_INR. + reremember;lra. + - rewrite (line_left_on_right_partition L w ps). + repeat rewrite app_length. + repeat rewrite plus_INR. + reremember;lra. } + + assert (leftw + onw + rightw = leftm + onm + rightm)%R. + { transitivity (^R ps). + - rewrite (line_left_on_right_partition L w ps). + repeat rewrite app_length. + repeat rewrite plus_INR. + reremember;lra. + - rewrite (line_left_on_right_partition L m ps). + repeat rewrite app_length. + repeat rewrite plus_INR. + reremember;lra. } + assert (leftx + onm <= leftw)%R. + { subst leftx leftw onm. + transitivity ((^R (L ^left) m ps) + (^R (L ^on) m ps))%R. + - apply Rplus_le_compat_r. + apply left_weaker. + assumption. + - apply Rge_le. + apply left_lt;lra. } + assert (rightw + onm <= rightx)%R. + { subst rightw rightx onm. + transitivity ((^R (L ^right) m ps) + (^R (L ^on) m ps))%R. + - apply Rplus_le_compat_r. + apply right_weaker. + assumption. + - apply Rge_le. + apply right_lt;lra. } + assert (rightm >= rightw + onw)%R. + { subst rightm rightw onw. + apply right_lt;lra. } + assert (leftm >= leftx + onx)%R. + { subst leftm onx leftx. + apply left_lt;lra. } + rewrite Rabs_left1 in h_equilib_x. + all:swap 1 2. + { destruct (Rle_lt_dec leftx rightx);try lra. + exfalso. + rewrite Rabs_right in h_equilib_w; try lra. } + rewrite Rabs_right in h_equilib_w; try lra. + split;[|lra]. + apply (@weber_aligned_spec_weak L);auto; auto. + - apply aligned_on_cons_iff;auto. + - reremember. + apply Rabs_le;lra. } + exists (L^-P ((L^P x + L^P w) * 1/2))%R. + apply h_segment_weber;auto. + + apply line_contains_proj_inv;auto. + + rewrite line_P_iP;auto. + lra. + + rewrite line_P_iP;auto. + lra. + - destruct (equiv_dec onw 0)%R as [? | h_w_neq0]. + { exists w;subst onw;auto. } + destruct (equiv_dec onx 0)%R as [? | h_x_neq0]. + { exists x;subst onx;auto. } + assert (0 < onx)%R as h_x_gt0. + { assert (onx <> 0 /\ onx >= 0)%R;try split;try lra. + - assumption. + - unremember. + apply Rle_ge , pos_INR. } + assert (0 < onw)%R as h_w_gt0. + { assert (onw <> 0 /\ onw >= 0)%R;try split;try lra. + - assumption. + - unremember. + apply Rle_ge , pos_INR. } + clear h_w_neq0 h_x_neq0. + assert (forall m, + line_contains L m + -> (L ^P w < L ^P m)%R + -> (L ^P m < L ^P x)%R + -> Weber ps m /\ ((^R (L ^on) m ps) = 0)%R) as h_segment_weber. + { intros m h_contain_m h_ltwm h_lt_mx. + alias (^R (L ^left) m ps) as leftm after h_Odd_ps. + alias (^R (L ^right) m ps) as rightm after h_Odd_ps. + alias (^R (L ^on) m ps) as onm after h_Odd_ps. + assert (0<=leftm)%R as h_lmpos by (unremember; apply pos_INR). + assert (0<=rightm)%R as h_rmpos by (unremember; apply pos_INR). + assert (0<=onm)%R as onmpos by (unremember; apply pos_INR). + assert (leftx + onx + rightx = leftw + onw + rightw)%R as h_eq_xw. + { transitivity (^R ps). + - rewrite (line_left_on_right_partition L x ps). + repeat rewrite app_length. + repeat rewrite plus_INR. + reremember;lra. + - rewrite (line_left_on_right_partition L w ps). + repeat rewrite app_length. + repeat rewrite plus_INR. + reremember;lra. } + + assert (leftw + onw + rightw = leftm + onm + rightm)%R. + { transitivity (^R ps). + - rewrite (line_left_on_right_partition L w ps). + repeat rewrite app_length. + repeat rewrite plus_INR. + reremember;lra. + - rewrite (line_left_on_right_partition L m ps). + repeat rewrite app_length. + repeat rewrite plus_INR. + reremember;lra. } + assert (leftw + onm <= leftx)%R. + { subst leftx leftw onm. + transitivity ((^R (L ^left) m ps) + (^R (L ^on) m ps))%R. + - apply Rplus_le_compat_r. + apply left_weaker. + assumption. + - apply Rge_le. + apply left_lt;lra. } + assert (rightx + onm <= rightw)%R. + { subst rightw rightx onm. + transitivity ((^R (L ^right) m ps) + (^R (L ^on) m ps))%R. + - apply Rplus_le_compat_r. + apply right_weaker. + assumption. + - apply Rge_le. + apply right_lt;lra. } + assert (rightm >= rightx + onx)%R. + { subst rightm rightx onx. + apply right_lt;lra. } + assert (leftm >= leftw + onw)%R. + { subst leftm onw leftw. + apply left_lt;lra. } + + + rewrite Rabs_left1 in h_equilib_w. + all:swap 1 2. + { destruct (Rle_lt_dec leftw rightw);try lra. + exfalso. + rewrite Rabs_right in h_equilib_x; try lra. } + rewrite Rabs_right in h_equilib_x; try lra. + split;[|lra]. + apply (@weber_aligned_spec_weak L);auto; auto. + - apply aligned_on_cons_iff;auto. + - reremember. + apply Rabs_le;lra. } + exists (L^-P ((L^P x + L^P w) * 1/2))%R. + apply h_segment_weber;auto. + + apply line_contains_proj_inv;auto. + + rewrite line_P_iP;auto. + lra. + + rewrite line_P_iP;auto. + lra. } + destruct h_ex_pt as [pt [hpt1 hpt2]]. rewrite -> (@weber_aligned_spec_weak L) in hpt1;auto. 2:{ specialize (weber_aligned h_nonnil h_aligned_on hpt1) as ha_align_pt. apply aligned_on_cons_iff;split;auto. } @@ -2739,17 +3297,56 @@ Proof. assert (Nat.Even (length ps)). { eapply left_right_balanced_even with (w := pt) (L:=L);try lra. } + apply Nat.Even_Odd_False with (Rlength ps);auto. +Qed. + + +Lemma line_contains_def (L: @line R2) w: + line_contains L w -> + L^-P (L ^P w) = w. +Proof. + intros h_contain. + apply h_contain. +Qed. -Admitted. + +Lemma weber_same L ps w: + ps <> nil -> + aligned_on L ps -> + Weber ps w -> + forall w', + line_contains L w' -> + (L^on w' ps = L^on w ps)%R -> + (L^left w' ps = L^left w ps)%R -> + (L^right w' ps = L^right w ps)%R -> + Weber ps w'. +Proof. + intros H H0 H1 w' H2 H3 H4 H5. + destruct (equiv_dec w w'). + { now rewrite <- e. } + assert (line_dir L =/= 0%VS) as h_dir_nonnull. + { apply line_dir_nonnul with w w';auto. + apply (@weber_aligned L ps) ;auto. } + apply (@weber_aligned_spec_weak L);auto. + { apply aligned_on_cons_iff;auto. } + rewrite H3,H4,H5. + apply (@weber_aligned_spec_weak L);auto. + { apply aligned_on_cons_iff;split;auto. + apply (@weber_aligned L ps) ;auto. } +Qed. Lemma weber_segment_InA ps w1 w2 : (forall w, Weber ps w <-> segment w1 w2 w) -> InA equiv w1 ps /\ InA equiv w2 ps. Proof. - (* Proof sketch: suppose w1 is not occupied, then there is a point - close to w1 but outside the segment that is also a weber point +(* Proof sketch: suppose w1 is not occupied, then there is a point + close to w1 but outside the segment that is also a weber point (since left, right and on would be the same). This would be a contradiction. *) + + intros h_forall. + + Admitted. (*