diff --git a/CaseStudies/Gathering/InR2/Weber/Weber_point.v b/CaseStudies/Gathering/InR2/Weber/Weber_point.v
index 230b491673ce88ba0251cf04d1a0ffe148431712..110df8cd0b804242f419c8fcf207069838a9525d 100644
--- a/CaseStudies/Gathering/InR2/Weber/Weber_point.v
+++ b/CaseStudies/Gathering/InR2/Weber/Weber_point.v
@@ -2466,7 +2466,6 @@ Proof.
eapply hwebeq;eauto.
Qed.
-Require Import LibHyps.LibHyps.
Lemma right_lt: forall {T : Type} {S0 : Setoid T} {EQ0 : EqDec S0} {VS : RealVectorSpace T} {H : EuclideanSpace T}
(L : line) (ps : list T) (w w' : T),
((L ^P) w' < (L ^P) w)%R ->
@@ -2599,6 +2598,111 @@ Proof.
lra.
Qed.
+Lemma INR_add_le: forall x y r: nat,
+ x + y < r ->
+ (((INR x) + (INR y) + 1 <= INR r)%R) .
+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.
+Qed.
+
+Lemma INR_add_le': forall x y r: nat,
+ ((INR x) + (INR y) < INR r)%R ->
+ (((INR x) + (INR y) + 1 <= INR r)%R) .
+Proof.
+ intros x y r h_Rlt.
+ apply INR_add_le.
+ rewrite <- plus_INR in h_Rlt;auto.
+ now apply INR_lt.
+Qed.
+
+Lemma INR_minus_le: forall x y r: nat,
+ y <= x ->
+ x - y < r ->
+ (((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.
+Qed.
+
+Lemma INR_minus_le': forall x y r: nat,
+ y <= x ->
+ ((INR x) - (INR y) < INR r)%R ->
+ (((INR x) - (INR y) + 1 <= INR r)%R) .
+Proof.
+ intros x y r h_le h_Rlt.
+ apply INR_minus_le;auto.
+ rewrite <- minus_INR in h_Rlt;auto.
+ 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 *)
@@ -2609,9 +2713,12 @@ Lemma weber_aligned_spec_right_bigger_2 L ps w :
OnlyWeber ps w.
Proof.
intros h_neq_ps_nil h_line_dir h_align h_left_right h_Rlt_Rabs.
- (* assert ( ((^R (L ^left) w ps) - (^R (L ^right) w ps) + 1 <= 0)%R) as h_left_right'. *)
- (* { admit. } *)
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.
+
apply Rlt_le in h_Rlt_Rabs as h_Rle_Rabs.
apply <- h_weak in h_Rle_Rabs.
clear h_weak.
@@ -2631,13 +2738,15 @@ Proof.
rewrite hrabs_eq in *.
clear hrabs_eq.
rewrite Ropp_minus_distr' in h_Rlt_Rabs.
- remember (^R (L ^left) x ps) as leftx in *.
- remember (^R (L ^right) x ps) as rightx in *.
- remember (^R (L ^on) x ps) as onx in *.
- remember (^R (L ^left) w ps) as leftw in *.
- remember (^R (L ^right) w ps) as rightw in *.
- remember (^R (L ^on) w ps) as onw in *.
-
+ 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. }
+ clear h_Rlt_Rabs.
+ move x before w.
+ 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.
@@ -2646,10 +2755,8 @@ Proof.
apply (f_equal INR) in h2.
repeat rewrite app_length in h2.
repeat rewrite plus_INR in h2.
-
- rewrite <- Heqrightx,<- Heqleftx, <- Heqleftw, <-Heqrightw, <- Heqonx, <- Heqonw 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.
@@ -2657,90 +2764,36 @@ Proof.
rewrite <- h_align_x in c.
contradiction. }
specialize (Rdichotomy _ _ h_proj) as [h_proj' | h_proj'].
- - assert (rightx >= rightw + onw )%R.
- { rewrite Heqrightx , Heqonw , Heqrightw.
+ - assert (rightx >= rightw + onw )%R as h_le_rightxw.
+ { unremember.
now apply right_lt. }
- assert (onx + leftx <= leftw)%R.
- { lra. }
- clear H0.
- assert (onx >= 0)%R.
+ assert (onx >= 0)%R as h_onx_pos.
{ rewrite Heqonx.
apply Rle_ge.
apply pos_INR. }
- assert ((rightx - leftx) <= onx)%R.
+ assert ((rightx - leftx) <= onx)%R as h_balance.
{ rewrite Rabs_left1 in h_rabs.
- lra.
- lra. }
- clear c.
- clear h_proj'.
- clear h_proj.
lra.
-
- - /g.
- assert (onw > 0)%R by lra.
- assert (leftx >= leftw + onw )%R.
- { rewrite Heqleftx, Heqleftw, Heqonw.
+ - assert (onw > 0)%R by lra.
+ assert (leftx >= leftw + onw )%R.
+ { unremember.
now apply left_lt. }
assert (rightx <= rightw)%R.
- { rewrite Heqrightx, Heqrightw.
+ { unremember.
now apply right_weaker. }
- assert (leftx > rightx)%R by lra.
- assert (leftx - rightx <= onx)%R.
- { rewrite Rabs_pos_eq in h_rabs;lra. }
- clear h_rabs.
-
- assert (onw >=0)%R.
- { rewrite Heqonw.
- apply Rle_ge.
- apply pos_INR. }
- assert (onx >=0)%R.
- { rewrite Heqonx.
- apply Rle_ge.
- apply pos_INR. }
- assert (leftw >=0)%R.
- { rewrite Heqleftw.
- apply Rle_ge.
- apply pos_INR. }
- assert (leftx >=0)%R.
- { rewrite Heqleftx.
- apply Rle_ge.
- apply pos_INR. }
- assert (rightw >=0)%R.
- { rewrite Heqrightw.
- apply Rle_ge.
- apply pos_INR. }
- assert (rightx >=0)%R.
- { rewrite Heqrightx.
- apply Rle_ge.
- apply pos_INR. }
+ 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.
clear h_proj.
assert (rightx + onx <= rightw)%R by lra.
-
- assert (rightw - leftw + 1 <= onw)%R.
- { (* hideously going back and forth from R to nat. *)
- rewrite Heqrightw, Heqleftw, Heqonw.
- rewrite <- minus_INR.
- 2:lra.
- change (IZR (Zpos xH)) with (INR 1).
- rewrite <- plus_INR.
- apply le_INR.
- apply not_gt.
- intro abs.
- apply le_INR in abs.
- change (S (Rlength ((L ^on) w ps)))
- with (1+(Rlength ((L ^on) w ps))) in abs.
- repeat rewrite plus_INR in abs.
- rewrite minus_INR in abs.
- 2: lra.
- change (INR 1) with (IZR (Zpos xH)) in abs.
- rewrite <- Heqrightw, <- Heqleftw, <- Heqonw in abs.
- lra. }
-
- clear h_left_right.
- clear h_Rlt_Rabs.
- lra.
+ 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 ->
@@ -2748,8 +2801,28 @@ Lemma weber_aligned_spec_left_bigger_2 L ps w :
((^R (L^right w ps)) - (^R (L^left w ps)) < 0)%R ->
(Rabs ((^R (L^left w ps)) - (^R (L^right w ps))) < ^R (L^on w ps))%R ->
OnlyWeber ps w.
-Proof.
-Admitted.
+Proof.
+ intros h_neq_ps_nil h_line_dir h_align h_left_right h_Rlt_Rabs.
+ specialize (@weber_aligned_spec_right_bigger_2 (line_reverse L) ps w h_neq_ps_nil) as h.
+ apply h;clear h.
+ - intro abs.
+ apply h_line_dir.
+ clear h_line_dir.
+ cbn in abs.
+ inversion abs.
+ rewrite H0 in H1.
+ destruct L;cbn in H0, H1.
+ cbn.
+ apply pair_eqE;simpl.
+ split;lra.
+ - now apply aligned_on_reverse in h_align.
+ - rewrite line_reverse_left, line_reverse_right.
+ assumption.
+ - rewrite line_reverse_left, line_reverse_right, line_reverse_on.
+ rewrite Rabs_minus_sym.
+ assumption.
+Qed.
+
Lemma weber_aligned_spec_on_2 L ps w :
ps <> nil -> (* Seems necessary *)
line_dir L =/= 0%VS ->