Last admits for Weber point.

CaseStudies/Gathering/InR2/Weber/Line.v

@@ -1046,21 +1046,6 @@ Lemma line_right_spec L x y ps :
   InA equiv y (L^right x ps) <-> (InA equiv y ps /\ (L^P y > L^P x)%R).
 Proof. unfold line_right. now rewrite filter_InA, Rltb_true ; [|intros ? ? ->]. Qed.
 
-Lemma line_left_diff L a ps:
-    ((L ^left) a ps) <> nil ->
-    aligned_on L ps ->
-    (L ^-P) ((L ^max) ((L ^left) a ps)) <> a.
-Proof.
-  intros h_left h_align.
-  intro abs.
-  assert (aligned_on L ((L ^left) a ps)) as h_align'.
-  { eapply aligned_on_inclA with ps;auto.
-    apply line_left_inclA. }
-  specialize (line_iP_max_InA L _ h_left h_align') as h.
-  rewrite abs in h.
-  rewrite line_left_spec in h.
-  lra.
-Qed.
 
 Lemma line_left_on_right_partition L x ps : 
   PermutationA equiv ps (L^left x ps ++ L^on x ps ++ L^right x ps).
@@ -1155,6 +1140,52 @@ Proof.
     lra.
 Qed.
 
+Lemma line_left_diff L a ps:
+    ((L ^left) a ps) <> nil ->
+    aligned_on L ps ->
+    (L ^-P) ((L ^max) ((L ^left) a ps)) =/= a.
+Proof.
+  intros h_left h_align.
+  intro abs.
+  assert (aligned_on L ((L ^left) a ps)) as h_align'.
+  { eapply aligned_on_inclA with ps;auto.
+    apply line_left_inclA. }
+  specialize (line_iP_max_InA L _ h_left h_align') as h.
+  rewrite abs in h.
+  rewrite line_left_spec in h.
+  lra.
+Qed.
+
+
+Lemma eqlistA_nil_eq: forall [A : Type] (eqA : A -> A -> Prop) l, eqlistA eqA l nil <-> l = nil.
+Proof.
+  intros A eqA l.
+  split.  
+  - induction l;intros;auto.
+    inversion H0.
+  - intro h.
+    subst.
+    apply eqlistA_nil.
+Qed.
+
+
+Lemma line_right_diff L a ps:
+    ((L ^right) a ps) <> nil ->
+    aligned_on L ps ->
+    (L ^-P) ((L ^min) ((L ^right) a ps)) =/= a.
+Proof.
+  intros h_right h_align.
+  rewrite <- line_reverse_iP_max.
+
+  rewrite <- line_reverse_left.
+  apply line_left_diff;auto.
+  - intro abs.
+    rewrite <- eqlistA_nil_eq with (eqA:=equiv) in abs .
+    rewrite line_reverse_left in abs.
+    rewrite eqlistA_nil_eq in abs.
+    contradiction.
+  - now apply -> aligned_on_reverse.
+Qed.
   
 Lemma bipartition_min: forall L ps,
     PermutationA equiv ps
@@ -1286,36 +1317,30 @@ Proof.
   apply PermutationA_app_inv_l with (2:=h2).
   typeclasses eauto.
 Qed.
-(*
-Lemma aggravate_left': forall L ps w w',
-    ((L^P w') < (L^P w))%R
-    -> L^right w' (L^left w ps) = nil
-    -> L^on w' ps = nil
-    -> PermutationA equiv (L^left w ps) (L^left w' ps).
+
+
+Lemma aggravate_left' : forall L ps w w',
+    ((L ^P) w < (L ^P) w')%R ->
+    (L ^left) w' ((L ^right) w ps) = nil ->
+    (L ^on) w ps = nil ->
+    PermutationA equiv ((L ^left) w' ps) ((L ^left) w ps).
 Proof.
-  intros L ps w w' H0 H1 H2.
-  specialize (line_left_on_right_partition L w' ps) as h1.
-  specialize (line_left_on_right_partition L w ps) as h2.
-  rewrite H2 in h1.
-  rewrite app_nil_l in h1.
-  assert (PermutationA equiv ((L ^right) w ps ++ (L ^on) w ps) ((L ^right) w' ps)).
-  { specialize (line_left_on_right_partition L w ((L ^right) w' ps)) as h3.
-    rewrite H2 in h3.
-    rewrite app_nil_r in h3.
-    rewrite <- aggravate_left in h3;auto.
-    rewrite <- aggravate_on_left in h3;auto.
-    rewrite h3.
-    reflexivity.
-  }
-  rewrite <- H3 in h2.
-  rewrite app_assoc in h1.
-  rewrite h1 in h2 at 1.
-  symmetry.
-  apply PermutationA_app_inv_l with (2:=h2).
-  typeclasses eauto.
+  intros L ps w w' H0 H1 H2. 
+  remember (line_reverse L) as L'.
+  
+  repeat rewrite <- line_reverse_right.
+  apply aggravate_right'.
+  - repeat rewrite line_reverse_proj.
+    lra.
+  - apply PermutationA_nil with equiv;auto.
+    + typeclasses eauto.
+    + setoid_rewrite line_reverse_left.
+      setoid_rewrite line_reverse_right.
+      now rewrite H1.
+  - apply eqlistA_nil_eq with equiv.
+    rewrite <- H2.
+    apply line_reverse_on.
 Qed.
-*)
-
 
 Lemma line_on_length_aligned L x ps : 
   aligned_on L (x :: ps) ->