From a264ffa5a06f689e68dacc99cf18af817557c2a2 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
Date: Thu, 7 Nov 2024 17:06:23 +0100
Subject: [PATCH] WIP.
---
.../Gathering/InR2/Weber/Weber_point.v | 597 +++++-------------
Util/ListComplements.v | 3 +-
Util/NumberComplements.v | 61 ++
Util/Preliminary.v | 83 +++
4 files changed, 311 insertions(+), 433 deletions(-)
diff --git a/CaseStudies/Gathering/InR2/Weber/Weber_point.v b/CaseStudies/Gathering/InR2/Weber/Weber_point.v
index f3e9f05f..683e2137 100644
--- a/CaseStudies/Gathering/InR2/Weber/Weber_point.v
+++ b/CaseStudies/Gathering/InR2/Weber/Weber_point.v
@@ -1740,7 +1740,7 @@ assert (Hineq : (norm (list_sumVS (map (u w) ps)) + INR (countA_occ equiv R2_EqD
* rewrite S_INR. lra.
}
transitivity (INR (Nat.div2 (length ps + 1))) ; [| now apply le_INR].
-eapply Rplus_le_reg_r ; rewrite Hineq. Search INR Rle le.
+eapply Rplus_le_reg_r ; rewrite Hineq.
rewrite <-(Rplus_le_compat_l (INR (Nat.div2 (length ps + 1))) _ _ (le_INR _ _ Hcount)).
rewrite <-plus_INR. apply le_INR. apply div2_sum_p1_ge.
Qed.
@@ -1799,358 +1799,7 @@ Qed.
(* Notation "L '^lftof' x '^in' ps" := (INR (Rlength (line_left L x ps))) (at level 100, no associativity). *)
-Notation "'^R' x" := (INR (Rlength x)) (at level 180, no associativity).
-
-(* Definition lefts L x (ps:list R2) := (INR (Rlength (line_left L x ps))). *)
-Definition rights L x (ps:list R2) := (INR (Rlength (line_right L x ps))).
-(* Definition ons L x (ps:list R2) := (INR (Rlength (line_on L x ps))). *)
-(*
-(* We can always find a point w' strictly on the right of w but close
- enough so that there is not point of ps between w and w', including
- w' itself. Thus the left of w' is exactly left w + on w and right w
- = right w'.
-
-------------------p1---p2-----------w----w'---p3----p4-----------
- p5
- p6
-
-In this case: take e.g. w' = the middle of [w;p3] *)
-Lemma shift_right: forall L w (ps: list R2),
- ps <> nil -> (* Seems necessary *)
- line_dir L =/= 0%VS ->
- aligned_on L (w :: ps) ->
- { w' | aligned_on L (w' :: w :: ps) /\
- L^on w' ps = nil
- /\ PermutationA equiv (L^left w' ps) (L^left w ps ++ L^on w ps)
- /\ L^right w' ps= L^right w ps
- /\ w =/=w' }.
-Proof.
- intros L w ps h_ps_nonil h_lineOK h_align.
- assert (line_contains L w) as h_line_w.
- { apply aligned_on_cons_iff in h_align.
- now destruct h_align. }
- assert (forall w' : R2, ((L ^P) w <= (L^P) w')%R ->
- inclA equiv ((L ^right) w' ps) ((L ^right) w ps))
- as h_right_incl.
- { now apply line_right_inclA_3. }
- assert (forall w' : R2, ((L ^P) w' <= (L^P) w)%R ->
- inclA equiv ((L ^left) w' ps) ((L ^left) w ps))
- as h_left_incl.
- { now apply line_left_inclA_3. }
- specialize (@line_left_on_right_partition _ _ _ _ _ L w ps) as h_split.
- specialize (@line_right_inclA_4 _ _ _ _ _ L w ps) as h_right.
-
- (* TODO: first see if there is something in ps on the right of w. *)
- destruct ((L ^right) w ps) eqn:heq_lright.
- - exists ((L^-P)((L^P) w + 1))%R.
- remember ((L^-P)((L^P) w + 1))%R as w'.
- specialize (@line_left_on_right_partition _ _ _ _ _ L w' ps) as h_split'.
- assert ((L ^P) w < (L ^P) w')%R as h_lt_w_w'.
- { subst w'.
- rewrite line_P_iP;try auto.
- lra. }
- assert ((L ^P) w <= (L ^P) w')%R as h_le_w_w' by lra.
- specialize h_right_incl with (1:=h_le_w_w').
- specialize h_right with (1:=h_lt_w_w').
- assert (line_contains L w').
- { subst.
- lazy beta delta [line_contains].
- rewrite line_P_iP;auto. }
- assert ((L ^on) w' ps = nil) as h_lon_w'_nil.
- { specialize inclA_nil with (2:=h_right).
- intros H0.
- apply H0.
- typeclasses eauto. }
- assert (h_right_w'_nil : (L ^right) w' ps = nil).
- { apply inclA_nil with (2:=h_right_incl).
- typeclasses eauto. }
- assert (PermutationA equiv ((L ^right) w ps) ((L ^right) w' ps)) as h_right_w_w'.
- { rewrite heq_lright.
- apply inclA_nil in h_right_incl.
- rewrite h_right_incl.
- - constructor.
- - typeclasses eauto. }
- repeat split.
- + rewrite -> aligned_on_cons_iff.
- split;auto.
- + assumption.
- + (* rewrite <- heq_lright in h_split. *)
- (* rewrite H0 in h_split. *)
- setoid_rewrite app_nil_end.
- rewrite app_nil_end at 1.
-
- setoid_rewrite <- h_lon_w'_nil at 1.
- setoid_rewrite <- heq_lright at 1 2.
- rewrite h_right_w_w' at 1.
- setoid_rewrite app_assoc_reverse.
- transitivity ps.
- * now symmetry.
- * now rewrite heq_lright.
- + rewrite heq_lright in h_right_w_w'.
- apply PermutationA_nil with (2:=h_right_w_w').
- typeclasses eauto.
- + rewrite Heqw'.
- intro abs.
- assert ((L ^P) w == (L ^P) ((L ^-P) ((L ^P) w + 1))) as h_abs.
- { now rewrite <- abs. }
- setoid_rewrite line_P_iP in h_abs.
- cbn -[line_proj] in h_abs.
- * lra.
- * assumption.
- - rewrite <- heq_lright in *.
- assert ((L ^right) w ps <> nil).
- { symmetry.
- rewrite heq_lright.
- apply nil_cons. }
- remember (L^-P (((line_min L ((L ^right) w ps)) - (L^P w)) / 2)) as w'.
- exists w'.
-
- repeat split.
- + rewrite -> aligned_on_cons_iff.
- split.
- * subst w'.
- now apply line_contains_proj_inv.
- * assumption.
- + eapply (Preliminary.PermutationA_nil setoid_equiv).
- Print Instances Proper.
- rewrite h_split.
- rewrite 2 line_on_app.
- assert ((L ^on) w' ((L ^left) w ps) = nil).
- { }
- assert ((L ^on) w' ((L ^on) w ps) = nil).
- { admit. }
- assert ((L ^on) w' ((L ^right) w ps) = nil).
- { admit. }
- app_eq_nil
- subst w'.
- red.
- rewrite line_P_iP.
- reflexivity.
- *
- remember (middle w (L^-P (line_min L ((L ^right) w ps))%VS)) as w'.
- exists w'.
- specialize (@line_left_on_right_partition _ _ _ _ _ L w' ps) as h_split'.
- assert (line_contains L w').
- { subst.
- apply line_contains_middle;auto.
- lazy beta delta [line_contains].
- rewrite line_P_iP;auto. }
-
- repeat split.
- + rewrite -> aligned_on_cons_iff.
- split;auto.
- +
-
- destruct ((L ^on) w' ps) eqn:heq_lonw' ;auto.
- assert ((L ^P) w < (L ^P) r0)%R.
- { admit. }
- assert ((L ^P) r0 < ((L ^min) ((L ^right) w ps)))%R.
- { admit. }
-
-
-
-
- assert ((L ^P) w < (L ^P)((L ^-P) ((L ^min) ((L ^right) w ps))))%R as h_lt_w_w'.
- { rewrite line_P_iP;auto.
- specialize (@line_min_spec_nonnil _ _ _ _ _ L ps) with (1:=h_ps_nonil) as h_lmin_ps.
- specialize (@line_min_spec_nonnil _ _ _ _ _ L) with (1:=H) as h_lmin_ps2.
- apply Rgt_lt.
- specialize (@line_right_spec _ _ _ _ _ L w ((L ^-P) ((L ^min) ((L ^right) w ps))) ps) as h.
- destruct h as [h1 h2].
-
- rewrite h_lmin_ps2.
-
- }
- assert ((L ^P) w < (L ^P) w')%R as h_lt_w_w'.
- { subst w'.
- specialize (line_bounds L ps) as h_line_bounds.
-
- rewrite line_P_iP;try auto.
- lra. }
- assert ((L ^P) w <= (L ^P) w')%R as h_le_w_w' by lra.
- specialize h_right_incl with (1:=h_le_w_w').
- specialize h_right with (1:=h_lt_w_w').
- assert (line_contains L w').
- { subst.
- lazy beta delta [line_contains].
- rewrite line_P_iP;auto. }
- assert ((L ^on) w' ps = nil) as h_lon_w'_nil.
- { specialize inclA_nil with (2:=h_right).
- intros H0.
- apply H0.
- typeclasses eauto. }
- assert (h_right_w'_nil : (L ^right) w' ps = nil).
- { apply inclA_nil with (2:=h_right_incl).
- typeclasses eauto. }
- assert (PermutationA equiv ((L ^right) w ps) ((L ^right) w' ps)) as h_right_w_w'.
- { rewrite heq_lright.
- apply inclA_nil in h_right_incl.
- rewrite h_right_incl.
- - constructor.
- - typeclasses eauto. }
- repeat split.
- + rewrite -> aligned_on_cons_iff.
- split;auto.
- + assumption.
- + (* rewrite <- heq_lright in h_split. *)
- (* rewrite H0 in h_split. *)
- setoid_rewrite app_nil_end.
- rewrite app_nil_end at 1.
-
- setoid_rewrite <- h_lon_w'_nil at 1.
- setoid_rewrite <- heq_lright at 1 2.
- rewrite h_right_w_w' at 1.
- setoid_rewrite app_assoc_reverse.
- transitivity ps.
- * now symmetry.
- * now rewrite heq_lright.
- + rewrite heq_lright in h_right_w_w'.
- apply PermutationA_nil with (2:=h_right_w_w').
- typeclasses eauto.
- + rewrite Heqw'.
- intro abs.
- assert ((L ^P) w == (L ^P) ((L ^-P) ((L ^P) w + 1))) as h_abs.
- { now rewrite <- abs. }
- setoid_rewrite line_P_iP in h_abs.
- cbn -[line_proj] in h_abs.
- * lra.
- * assumption.
-
-
- assert (line_contains L w').
- { subst.
- apply line_contains_middle.
- - apply aligned_on_cons_iff in h_align.
- destruct h_align.
- assumption.
- - unfold line_contains.
- rewrite line_P_iP_min.
- reflexivity. }
-
- specialize (@line_left_on_right_partition _ _ _ _ _ L w' ps) as h_split'.
- (* Only if there is something in ps on the left of w. *)
- exists w'.
- repeat split.
- + rewrite -> aligned_on_cons_iff.
- split;auto.
- +
- enough (not (exists x, InA equiv x ps /\ (L ^P) x = (L ^P) w')).
- { destruct ((L ^on) w' ps) eqn:heq_lon ; try auto.
- exfalso.
- assert (InA equiv r0 ((L ^on) w' ps)).
- { rewrite heq_lon.
- constructor 1;auto. }
- apply H1.
- exists r0.
- split.
- - apply line_on_spec in H2.
- destruct H2;auto.
- - apply line_on_spec in H2.
- destruct H2;auto. }
-
- intro abs.
- destruct abs.
- rewrite <- (line_on_spec L) in H1.
- destruct abs as [w'' [h_InA_w'' h_eq_w'']].
-
-
- (* Only if there is something in ps on the left of w. *)
- exists (middle w (L^-P (line_min L ((L ^right) w ps))%VS)).
- remember (middle w (L^-P (line_min L ((L ^right) w ps))%VS)) as w'.
- unfold middle in Heqw'.
-
- assert ((L ^P) w < (L ^P) w')%R as h_left_nil.
- { admit. }
- assert (line_contains L w').
- { subst.
- apply line_contains_middle.
- - apply aligned_on_cons_iff in h_align.
- destruct h_align.
- assumption.
- - unfold line_contains.
- rewrite line_P_iP_min.
- reflexivity. }
- assert (line_contains L w).
- { apply aligned_on_cons_iff in h_align.
- destruct h_align.
- assumption. }
- specialize (@line_left_on_right_partition _ _ _ _ _ L w' ps) as h_split'.
-
-
- repeat split.
- - rewrite -> aligned_on_cons_iff.
- split;auto.
- -
- Set Nested Proofs Allowed.
- enough (PermutationA equiv ((L ^on) w' ps) (nil:list R2)).
- { apply Preliminary.PermutationA_nil with (2:= H1);auto. }
- rewrite line_on_perm_compat.
- 4: apply h_split.
- 2: reflexivity.
- 2:reflexivity.
- rewrite line_on_app.
- rewrite line_on_app.
- assert ((L ^on) w' ((L ^left) w ps) = nil).
- { unfold line_on.
- rewrite -> (@filter_nilA _ equiv);try typeclasses eauto.
- intros x H1.
- apply eqb_false_iff.
- intros abs.
- apply line_left_spec in H1.
- destruct H1.
- unfold equiv, R_Setoid, eq_setoid in abs.
- change ((L ^P) w' = (L ^P) x)%R in abs.
- lra. }
-
- line_left_spec.
-
-
- apply eqlistA_PermutationA.
- rewrite eqlistA_app.
- 4:assumption.
- rewrite eqlistA_app.
-
- apply app_eq_nil.
-
- rewrite h_split'.
- rewrite line_on_app.
-
-
-
-
-
-apply aligned_on_cons_iff in h_align as h_align2.
- destruct h_align2 as [h1 h2].
- apply aligned_on_cons_iff ; split.
- + rewrite Heqw'.
- apply line_contains_middle.
- * assumption.
- * admit. (* shoudl be trivial, unless L^min is by default *)
- + assumption.
- -
-
- admit.
-
-Admitted.
-
-
-(* Symmetrical for going on the left of w. *)
-Lemma shift_left: forall L w (ps: list R2),
- ps <> nil -> (* Seems necessary *)
- line_dir L =/= 0%VS ->
- aligned_on L (w :: ps) ->
- { w' | aligned_on L (w' :: w :: ps) /\
- L^on w' ps = nil
- /\ PermutationA equiv (L^right w' ps) (L^right w ps ++ L^on w ps)
- /\ L^left w' ps= L^left w ps
- /\ w =/=w' }.
-Proof.
- intros L w ps h_ps_nonil h_lineOK h_align.
- admit.
-
-Admitted.
-
-*)
+Notation "'^R' x" := (INR (length x)) (at level 180, no associativity).
Lemma weber_aligned_sufficient L ps w :
ps <> nil -> (* Seems necessary *)
@@ -2337,7 +1986,7 @@ Proof.
intros A l H.
destruct (Nat.eq_decidable (length l) 0).
- now apply length_0.
- - assert (0 < Rlength l).
+ - assert (0 < length l).
{ lia. }
apply (lt_0_INR (length l)) in H1.
exfalso.
@@ -2432,7 +2081,7 @@ Proof.
now apply h_incl. }
apply (@InA_nth _ equiv 0%VS w' ((L ^on) w' ps)) in H0.
destruct H0 as [n [y [h1 h2]]].
- assert (0 < Rlength ((L ^on) w' ps)) by lia.
+ assert (0 < length ((L ^on) w' ps)) by lia.
apply lt_INR in H0.
cbn in H0.
lra. }
@@ -2604,11 +2253,7 @@ Lemma INR_add_le: forall x y r: nat,
Proof.
intros x y r h_Rlt.
rewrite <- plus_INR.
- (* 1%R is actually a notation for (IZR 1%Z). *)
- change (IZR (Zpos xH)) with (INR 1).
- rewrite <- plus_INR.
- apply le_INR.
- lia.
+ now apply NumberComplements.INR_add_le.
Qed.
Lemma INR_add_le': forall x y r: nat,
@@ -2627,14 +2272,8 @@ Lemma INR_minus_le: forall x y r: nat,
(((INR x) - (INR y) + 1 <= INR r)%R) .
Proof.
intros x y r h_le h_Rlt.
- (* hideously going back and forth from R to nat. *)
- rewrite <- minus_INR;[|apply INR_le].
- 2:{ now apply le_INR. }
- (* 1%R is actually a notation for (IZR 1%Z). *)
- change (IZR (Zpos xH)) with (INR 1).
- rewrite <- plus_INR.
- apply le_INR.
- lia.
+ rewrite <- minus_INR;auto.
+ now apply NumberComplements.INR_add_le.
Qed.
Lemma INR_minus_le': forall x y r: nat,
@@ -2648,62 +2287,6 @@ Proof.
now apply INR_lt.
Qed.
-(* Dealing with hyps generated by "remember" *)
-Ltac reremember_in h :=
- repeat match goal with
- H: ?X = _ |- _ => (* (INR (length _)) *)
- is_var X;
- rewrite <- H in h
- end.
-
-Ltac reremember_ :=
- repeat match goal with
- H: ?X = _ |- _ =>
- is_var X;
- rewrite <- H
- end.
-
-Ltac unremember_in h :=
- repeat match goal with
- H: ?X = _ |- _ =>
- is_var X;
- rewrite H in h
- end.
-
-Ltac unremember_ :=
- repeat match goal with
- H: ?X = _ |- _ =>
- is_var X;
- rewrite H
- end.
-
-Ltac remember_move_all t name ath :=
- remember t as name in *;
- match goal with
- H: name = t |- _ =>
- move H after ath;
- move name at top
- end.
-
-Ltac remember_move_in t name inlh ath :=
- remember t as name in inlh ;
- match goal with
- H: name = t |- _ =>
- move H after ath;
- move name at top
- end.
-
-Tactic Notation "alias" constr(t) "as" ident(name) "after" hyp(h) :=
- remember_move_all t name h.
-
-Tactic Notation "alias" constr(t) "as" ident(name) "in" hyp_list(lh) "after" hyp(h) :=
- remember_move_in t name lh h.
-
-Tactic Notation "unremember" := unremember_.
-Tactic Notation "unremember" "in" hyp(h) := unremember_in h.
-Tactic Notation "reremember" := reremember_.
-Tactic Notation "reremember" "in" hyp(h) := reremember_in h.
-
Lemma weber_aligned_spec_right_bigger_2 L ps w :
ps <> nil -> (* Seems necessary *)
line_dir L =/= 0%VS ->
@@ -2740,8 +2323,14 @@ Proof.
rewrite Ropp_minus_distr' in h_Rlt_Rabs.
assert (((^R (L ^right) w ps) - (^R (L ^left) w ps) + 1 <= (^R (L ^on) w ps))%R)
as h_weber_strong.
- { apply INR_minus_le';try lra.
- apply INR_le;lra. }
+ { rewrite <- minus_INR.
+ - apply INR_add_le_INR.
+ rewrite minus_INR.
+ + reremember.
+ assumption.
+ + reremember.
+ apply INR_le;lra.
+ - apply INR_le;lra. }
clear h_Rlt_Rabs.
move x before w.
alias (^R (L ^left) x ps) as leftx after h_neq_ps_nil.
@@ -2792,8 +2381,6 @@ Proof.
lra.
Qed.
-(* Require Import LibHyps.LibHyps. *)
-
Lemma weber_aligned_spec_left_bigger_2 L ps w :
ps <> nil -> (* Seems necessary *)
line_dir L =/= 0%VS ->
@@ -2989,8 +2576,8 @@ Proof.
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.
+ assert (length ((L ^left) w ps) + length ((L ^right) w ps) < Nat.div2 (length ps + 1)).
+ { specialize (div2_sum_p1_ge (length 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.
@@ -3006,6 +2593,65 @@ Proof.
apply Rabs_def1;lra.
Qed.
+Ltac duplic h name :=
+ set (name := h);
+ clearbody name;
+ move name before h.
+
+Ltac duplic_autoname h :=
+ let name := fresh h "'" in
+ duplic h name.
+
+Tactic Notation "dup" hyp(h) := duplic_autoname h.
+Tactic Notation "dup" hyp(h) "as" ident(name) := duplic h name.
+
+
+Lemma left_right_balanced_even ps (w:R2) L:
+ (Rabs ((^R (L ^left) w ps) - (^R (L ^right) w ps)) = 0)%R ->
+ (^R (L ^on) w ps) = 0%R ->
+ Nat.Even (length ps).
+Proof.
+ intros h_eq0 h_on_0.
+ assert (((^R (L ^left) w ps) = (^R (L ^right) w ps))) as h_left_right.
+ { destruct (Rle_lt_dec (^R (L ^left) w ps) (^R (L ^right) w ps))%R as [h | h].
+ - rewrite Rabs_left1 in h_eq0;try lra.
+ - rewrite Rabs_pos_eq in h_eq0;try lra. }
+ 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.
+ apply (f_equal INR) in h_partition.
+ repeat rewrite plus_INR in h_partition.
+ rewrite h_on_0, h_left_right in h_partition.
+ assert ((^R ps) = (2 * (^R (L ^right) w ps))%R) by lra.
+ change 2%R with (INR 2%nat) in H.
+ rewrite <- mult_INR in H.
+ apply INR_injection in H.
+ rewrite H.
+ eexists ;eauto.
+Qed.
+
+Lemma middle_diff_l: forall x y:R2, x<>y -> middle x y <> x.
+Proof.
+ intros x y H.
+ specialize (middle_diff H) as h.
+ intro abs.
+ rewrite abs in h.
+ apply h.
+ constructor;auto.
+Qed.
+
+Lemma middle_diff_r: forall x y:R2, x<>y -> middle x y <> y.
+Proof.
+ intros x y H.
+ specialize (middle_diff H) as h.
+ intro abs.
+ rewrite abs in h.
+ apply h.
+ constructor 2.
+ constructor;auto.
+Qed.
+
(* 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.
@@ -3016,12 +2662,101 @@ Proof.
* 2. Show that there is a weber point on the segment [w1, w2]
* that is not in ps (i.e. with multiplicity 0).
* 3. Using weber_aligned_spec show that n is even. *)
+ intros h_Odd_ps h_weber_w.
+ assert (ps<>nil) as h_nonnil.
+ { intro abs.
+ rewrite abs in h_Odd_ps.
+ cbn in h_Odd_ps.
+ inversion h_Odd_ps.
+ lia. }
+ destruct (aligned_dec ps) as [h_align | h_nalign].
+ 2:{ apply weber_Naligned_unique;auto. }
+ split;auto.
+ intros x h_weber_x.
+ destruct (equiv_dec x w);auto.
+ exfalso.
+ alias (line_calc ps) as L after h_weber_w.
+ assert (aligned_on L ps) as h_aligned_on.
+ { unremember.
+ 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. }
+ 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]].
+ 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. }
+ assert (Rabs ((^R (L ^left) pt ps) - (^R (L ^right) pt ps)) >= 0)%R.
+ { apply Rle_ge.
+ apply Rabs_pos. }
+
+ assert (Nat.Even (length ps)).
+ { eapply left_right_balanced_even with (w := pt) (L:=L);try lra. }
+
Admitted.
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. Admitted.
+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
+ (since left, right and on would be the same). This would be a
+ contradiction. *)
+Admitted.
+(*
+Lemma weber_segment_InA' ps w1 w2 :
+ (forall w, Weber ps w <-> segment w1 w2 w)
+ <-> InA equiv w1 ps /\ InA equiv w2 ps /\ Weber ps w1 /\ Weber ps w2.
+Proof. Admitted.
+*)
End WeberPoint.
diff --git a/Util/ListComplements.v b/Util/ListComplements.v
index 0f0ef68a..98ed93b3 100644
--- a/Util/ListComplements.v
+++ b/Util/ListComplements.v
@@ -30,6 +30,7 @@ Require Import Psatz.
Require Import SetoidDec.
Require Import Pactole.Util.Preliminary.
Require Import Pactole.Util.NumberComplements.
+Require Import Arith.
Set Implicit Arguments.
@@ -939,8 +940,6 @@ intro l1. induction l1 as [| e l1]; intro l2.
Defined.
-Require Import Arith.
-
Lemma nth_firstn2: forall (l : list A) k n df, k < n -> nth k l df = List.nth k (firstn n l) df.
Proof.
intros l k n df H.
diff --git a/Util/NumberComplements.v b/Util/NumberComplements.v
index 76d8f79d..a453654d 100644
--- a/Util/NumberComplements.v
+++ b/Util/NumberComplements.v
@@ -612,3 +612,64 @@ Proof using ltc_ll_ul ltc_lr_ur.
Qed.
End lt_pred_mul_ul_ur.
+
+
+Lemma INR_injection: forall n1 n2,
+ INR n1 = INR n2 ->
+ n1 = n2.
+Proof.
+ induction n1 using nat_ind2;intros.
+ - destruct n2;auto.
+ destruct n2.
+ + exfalso.
+ cbn in H.
+ lra.
+ + exfalso.
+ repeat rewrite S_INR in H.
+ assert (INR n2 >= 0)%R.
+ { apply Rle_ge, pos_INR. }
+ cbn in H.
+ lra.
+ - destruct n2.
+ + exfalso.
+ cbn in H.
+ lra.
+ + destruct n2;auto.
+ repeat rewrite S_INR in H.
+ assert (INR n2 >= 0)%R.
+ { apply Rle_ge, pos_INR. }
+ cbn in H.
+ lra.
+ - assert (INR n1 >= 0)%R.
+ { apply Rle_ge, pos_INR. }
+ repeat rewrite S_INR in H.
+ destruct n2.
+ { exfalso.
+ cbn in H.
+ lra. }
+ destruct n2.
+ + exfalso.
+ cbn in H.
+ lra.
+ + rewrite (IHn1 n2);auto.
+ repeat rewrite S_INR in H.
+ lra.
+Qed.
+
+Lemma INR_add_le: forall x y: nat, x < y -> (((INR x) + 1 <= (INR y))%R).
+Proof.
+ intros x y h_Rlt.
+ change (IZR (Zpos xH)) with (INR 1).
+ rewrite <- plus_INR.
+ apply le_INR.
+ lia.
+Qed.
+
+Lemma INR_add_le_INR: forall x y : nat,
+ ((INR x) < (INR y))%R ->
+ (((INR x) + 1 <= (INR y))%R) .
+Proof.
+ intros x y h_Rlt.
+ apply INR_add_le.
+ now apply INR_lt.
+Qed.
diff --git a/Util/Preliminary.v b/Util/Preliminary.v
index 58551d1e..4182c099 100644
--- a/Util/Preliminary.v
+++ b/Util/Preliminary.v
@@ -72,6 +72,89 @@ Ltac revert_all :=
| |- ?B => repeat revert_one B
end.
+
+(* Dealing with hyps generated by "remember" *)
+Ltac reremember_in h :=
+ repeat match goal with
+ H: ?X = _ |- _ =>
+ is_var X;
+ rewrite <- H in h
+ end.
+
+Ltac reremember_ :=
+ repeat match goal with
+ H: ?X = _ |- _ =>
+ is_var X;
+ rewrite <- H
+ end.
+
+Ltac unremember_in h :=
+ repeat match goal with
+ H: ?X = _ |- _ =>
+ is_var X;
+ rewrite H in h
+ end.
+
+Ltac unremember_ :=
+ repeat match goal with
+ H: ?X = _ |- _ =>
+ is_var X;
+ rewrite H
+ end.
+
+Ltac remember_all_move_after t name ath :=
+ remember t as name in *;
+ match goal with
+ H: name = t |- _ =>
+ move H after ath;
+ move name at top
+ end.
+
+Ltac remember_all_move_before t name ath :=
+ remember t as name in *;
+ match goal with
+ H: name = t |- _ =>
+ move H before ath;
+ move name at top
+ end.
+
+Ltac remember_in_move_after t name inlh ath :=
+ remember t as name in inlh ;
+ match goal with
+ H: name = t |- _ =>
+ move H after ath;
+ move name at top
+ end.
+
+Ltac remember_in_move_before t name inlh ath :=
+ remember t as name in inlh ;
+ match goal with
+ H: name = t |- _ =>
+ move H before ath;
+ move name at top
+ end.
+
+(* alias is like remember but allows to move around the var and hyp
+ created . *)
+Tactic Notation "alias" constr(t) "as" ident(name) "after" hyp(h) :=
+ remember_all_move_after t name h.
+Tactic Notation "alias" constr(t) "as" ident(name) "before" hyp(h) :=
+ remember_all_move_before t name h.
+
+Tactic Notation "alias" constr(t) "as" ident(name) "in" hyp_list(lh) "after" hyp(h) :=
+ remember_in_move_after t name lh h.
+Tactic Notation "alias" constr(t) "as" ident(name) "in" hyp_list(lh) "before" hyp(h) :=
+ remember_in_move_before t name lh h.
+
+(* unremember is equivalent to applying subst to all hyps of the form
+id = term (not the symmetric though, as would subst so). *)
+Tactic Notation "unremember" := unremember_.
+Tactic Notation "unremember" "in" hyp(h) := unremember_in h.
+(* reremember tries to identify new occurrences of remembered
+ expressions and replace them by the name. *)
+Tactic Notation "reremember" := reremember_.
+Tactic Notation "reremember" "in" hyp(h) := reremember_in h.
+
Definition injective {A B : Type} (eqA : relation A) (eqB : relation B) (f : A -> B) : Prop :=
forall x y, eqB (f x) (f y) -> eqA x y.
--
GitLab