diff --git a/CaseStudies/Gathering/InR2/Weber/Gather_flex_async.v b/CaseStudies/Gathering/InR2/Weber/Gather_flex_async.v
index 0019291001c339689c85ac27ae0fc866984a7a9c..c2706e185911063287d2a1a9f76ca6e4379d827a 100644
--- a/CaseStudies/Gathering/InR2/Weber/Gather_flex_async.v
+++ b/CaseStudies/Gathering/InR2/Weber/Gather_flex_async.v
@@ -37,7 +37,7 @@ Require Import Psatz.
Require Import Inverse_Image.
Require Import FunInd.
Require Import FMapFacts.
-Require Import LibHyps.LibHyps.
+(* Require Import LibHyps.LibHyps. *)
Require Import Pactole.Util.ListComplements.
(* Helping typeclass resolution avoid infinite loops. *)
(* This does not seem to help much *)
@@ -68,10 +68,10 @@ Require Import Pactole.CaseStudies.Gathering.InR2.Weber.Weber_point.
(* User defined *)
Import Permutation.
Import Datatypes.
-
+Import ListNotations.
+(*
Section LibHyps_stuff.
Local Open Scope autonaming_scope.
-Import ListNotations.
(* Define the naming scheme as new tactic pattern matching on a type
th, and the depth n of the recursive naming analysis. Here we state
@@ -86,7 +86,7 @@ Ltac rename_hyp_2 n th :=
(* Then overwrite the customization hook of the naming tactic *)
Ltac rename_hyp ::= rename_hyp_2.
-Section LibHyps_stuff.
+End LibHyps_stuff.*)
Set Implicit Arguments.
@@ -308,6 +308,14 @@ unfold pos_list. rewrite map_length, config_list_length.
cbn. now rewrite Nat.add_0_r.
Qed.
+Lemma pos_list_non_nil config : (pos_list config) <> [].
+Proof using lt_0n.
+ intro abs.
+ apply length_zero_iff_nil in abs.
+ rewrite pos_list_length in abs.
+ lia.
+Qed.
+
(* This would have been much more pleasant to do with mathcomp's tuples. *)
Lemma config_list_InA_combine x x' (c c':configuration) :
InA equiv (x, x') (combine (config_list c) (config_list c')) <->
@@ -421,7 +429,9 @@ Proof using .
intros c1 c2 Hc. unfold invalid. setoid_rewrite Hc. reflexivity.
Qed.
+(*
Ltac rename_depth ::= constr:(2).
+*)
#[local] Definition info0: info := (0%VS, 0%VS, ratio_0).
(* I could have included this in the definition of invalid.
* I prefered to use [(n+1)/2] instead of [n/2] and thus have
@@ -942,6 +952,7 @@ Proof.
typeclasses eauto.
Qed.
+(*
Ltac rename_hyp_3 n th :=
match th with
| nil => name(`_nil`)
@@ -961,7 +972,7 @@ Ltac rename_hyp_3 n th :=
(* Then overwrite the customization hook of the naming tactic *)
Ltac rename_hyp ::= rename_hyp_3.
Ltac rename_depth ::= constr:(3).
-
+*)
Lemma support_mult_pos:
forall {elt : Type} {S0 : Setoid elt} {H : EqDec S0} {Ops : FMOps elt H}
@@ -970,14 +981,16 @@ Lemma support_mult_pos:
InA equiv x (support ms) <-> ms[x]>0.
Proof.
clear lt_0n.
- intros/g.
- split;intros/n.
- { apply support_spec in h_InA_x_support_ms_.
- destruct (eq_0_lt_dec (ms[x]))/ng.
+ intros.
+ split.
+ { intros h_InA_x_support_ms_ .
+ apply support_spec in h_InA_x_support_ms_.
+ destruct (eq_0_lt_dec (ms[x])) as [h_eq_mult_x_ms_0_|?].
- apply not_In in h_eq_mult_x_ms_0_.
contradiction.
- lia. }
- { destruct (InA_dec H x (support ms)) /ng.
+ { intros h_gt_mult_x_ms_0_ .
+ destruct (InA_dec H x (support ms)) as [|h_not_InA_x_support_].
- assumption.
- exfalso.
rewrite support_spec in h_not_InA_x_support_.
@@ -993,7 +1006,7 @@ Lemma remove_all_cardinal_plus:
forall (x : elt) (m : multiset elt), cardinal (remove_all x m) + m[x] = cardinal m.
Proof.
clear lt_0n delta_g0 delta n.
- intros /ng.
+ intros elt S0 H Ops h_FMultisetsOn_Ops_ x m .
assert (m[x] <= cardinal m).
{ apply cardinal_lower. }
specialize remove_all_cardinal with (x:=x)(m:=m) as h.
@@ -1009,16 +1022,18 @@ Lemma obs_invalid_doubleton1:
-> forall z, z =/= x -> z =/= y -> o[z]=0.
Proof.
clear lt_0n.
- intros/gn.
- specialize remove_all_cardinal_plus with (x:=x)(m:=o) as ?/n.
- specialize remove_all_cardinal_plus with (x:=y)(m:=(remove_all x o)) as ?/n.
+ intros elt S0 H Ops h_FMultisetsOn_Ops_ o x y h_nequiv_x_y_ h_ge_add_mult_mult_card_o_ z h_nequiv_z_x_ h_nequiv_z_y_ .
+ specialize remove_all_cardinal_plus with (x:=x)(m:=o).
+ intro h_eq_add_card_mult_card_o_ .
+ specialize remove_all_cardinal_plus with (x:=y)(m:=(remove_all x o)).
+ intro h_eq_add_card_mult_card_remAll_ .
foldR2.
rewrite remove_all_other with (x:=x)(y:=y)(m:=o) in h_eq_add_card_mult_card_remAll_.
2:{ symmetry;assumption. }
rewrite <- h_eq_add_card_mult_card_remAll_ in h_eq_add_card_mult_card_o_.
- assert (cardinal (remove_all y (remove_all x o)) = 0)/n.
+ assert (cardinal (remove_all y (remove_all x o)) = 0) as h_eq_card_remAll_0_.
{ lia. }
- assert (o[z] = (remove_all y (remove_all x o))[z])/n.
+ assert (o[z] = (remove_all y (remove_all x o))[z]) as h_eq_mult_z_o_mult_z_remAll_.
{ rewrite remove_all_other;auto.
rewrite remove_all_other;auto. }
rewrite h_eq_mult_z_o_mult_z_remAll_.
@@ -1038,28 +1053,31 @@ Lemma obs_invalid_doubleton2:
-> PermutationA equiv (support o) (x::y::nil).
Proof.
clear lt_0n delta_g0 delta n.
- intros/gn.
- specialize (obs_invalid_doubleton1 _ h_nequiv_x_y_ h_ge_add_mult_mult_card_o_) as ?/n.
+ intros elt S0 H Ops h_FMultisetsOn_Ops_ o x y h_nequiv_x_y_ h_gt_mult_x_o_0_ h_gt_mult_y_o_0_ h_ge_add_mult_mult_card_o_ .
+ specialize (obs_invalid_doubleton1 _ h_nequiv_x_y_ h_ge_add_mult_mult_card_o_).
+ intro h_all_eq_mult_0_ .
- specialize support_mult_pos with (x:=x)(ms:=o) as [? ?]/n.
+ specialize support_mult_pos with (x:=x)(ms:=o).
+ intros [h_impl_gt_mult_0_ h_impl_InA_x_support_].
specialize h_impl_InA_x_support_ with (1:=h_gt_mult_x_o_0_).
- specialize support_mult_pos with (x:=y)(ms:=o) as [? ?]/n.
+ specialize support_mult_pos with (x:=y)(ms:=o).
+ intros [h_impl_gt_mult_0_0 h_impl_InA_y_support_].
specialize h_impl_InA_y_support_ with (1:=h_gt_mult_y_o_0_).
specialize (@PermutationA_split _ equiv _ x (support o) h_impl_InA_x_support_) as h_permut.
- destruct h_permut as [l' hl']/g.
+ destruct h_permut as [l' hl'].
transitivity (x :: l');auto.
constructor 2;auto.
- assert (InA equiv y l') /n.
+ assert (InA equiv y l') as h_InA_y_l'_.
{ rewrite hl' in h_impl_InA_y_support_.
- inversion h_impl_InA_y_support_/sng.
- - exfalso. symmetry in h_equiv_y_x_. contradiction.
+ inversion h_impl_InA_y_support_.
+ - exfalso. symmetry in h_nequiv_x_y_. contradiction.
- assumption. }
specialize (@PermutationA_split _ equiv _ y l' h_InA_y_l'_) as h_permut.
- destruct h_permut as [l'' hl'']/g.
+ destruct h_permut as [l'' hl''].
transitivity (y :: l'').
{ assumption. }
constructor 2;auto.
@@ -1068,7 +1086,7 @@ Proof.
- reflexivity.
- absurd (o[e]=0).
all:cycle 1.
- + assert (NoDupA equiv (e :: x :: y :: l'')) /n.
+ + assert (NoDupA equiv (e :: x :: y :: l'')) as h_NodupA_cons_e_x_.
{ eapply PermutationA_preserves_NoDupA with (lâ‚ := (x :: e :: y :: l''));try typeclasses eauto.
constructor 3.
eapply PermutationA_preserves_NoDupA with (lâ‚ := (x :: y :: e :: l''));try typeclasses eauto.
@@ -1076,7 +1094,7 @@ Proof.
constructor 3.
apply PermutationA_preserves_NoDupA with (2:=hl');try typeclasses eauto.
eapply support_NoDupA. }
- inversion h_NodupA_cons_e_x_/sng.
+ inversion h_NodupA_cons_e_x_ as [ | x0 l h_not_InA_e_cons_ h_NodupA_cons_x_y_ [h_eq_x0_e_ h_eq_l_cons_x_y_] ].
apply h_all_eq_mult_0_.
* intro abs.
apply h_not_InA_e_cons_.
@@ -1103,8 +1121,9 @@ Lemma support_div2_split:
-> o[x] + o[y] >= cardinal o.
Proof.
clear lt_0n delta_g0 delta n.
- intros/sng.
- specialize div2_sum_p1_ge with (n:=cardinal o) as ?/n.
+ intros elt S0 H Ops h_FMultisetsOn_Ops_ o x y h_eq_mult_x_o_div2_add_ h_eq_mult_y_o_div2_add_ .
+ specialize div2_sum_p1_ge with (n:=cardinal o).
+ intro h_le_card_o_add_div2_div2_.
rewrite <- h_eq_mult_x_o_div2_add_ in h_le_card_o_add_div2_div2_ at 1.
rewrite <- h_eq_mult_x_o_div2_add_ in h_le_card_o_add_div2_div2_ at 1.
lia.
@@ -1121,20 +1140,22 @@ Proof.
intros h.
unfold invalid_obs in h.
destruct h as [x [y h]].
- decompose [and] h; clear h /n.
- specialize @obs_invalid_doubleton1 with (o:=o) (2:=h_nequiv_x_y_) as ?/n.
+ (* decompose [and] h; clear h /n. *)
+ destruct h as [h_nequiv_x_y_ [h_neq_card_o_0_ [h_eq_mult_x_o_div2_add_ h_eq_mult_y_o_div2_add_]]].
+ specialize @obs_invalid_doubleton1 with (o:=o) (2:=h_nequiv_x_y_).
+ intro h_impl_eq_mult_0_.
specialize (h_impl_eq_mult_0_ _).
- assert(o[x] + o[y] >= cardinal o)/n.
+ assert(o[x] + o[y] >= cardinal o) as h_ge_add_mult_mult_card_o_.
{ apply support_div2_split;auto. }
specialize h_impl_eq_mult_0_ with (1:=h_ge_add_mult_mult_card_o_).
- specialize @obs_invalid_doubleton2 with (o:=o) (2:=h_nequiv_x_y_) as ?/n.
+ specialize @obs_invalid_doubleton2 with (o:=o) (2:=h_nequiv_x_y_).
+ intro h_impl_PermutA_support_cons_.
assert (h_div2_pos: 0 < Nat.div2 (cardinal o + 1)) by (apply card_div2;eauto).
- assert (o[x] > 0) by lia /n.
- assert (o[y] > 0) by lia /n.
+ assert (o[x] > 0) as h_gt_mult_x_o_0_ by lia .
+ assert (o[y] > 0) as h_gt_mult_y_o_0_ by lia.
specialize (h_impl_PermutA_support_cons_ _ h_gt_mult_x_o_0_ h_gt_mult_y_o_0_).
-
exists x, y.
repeat split;auto.
Qed.
@@ -1158,10 +1179,15 @@ Proof.
right.
intro abs.
rewrite heq in *.
- specialize obs_invalid_doubleton with (1:=abs) as ?/n.
+ specialize obs_invalid_doubleton with (1:=abs).
+ intros h_ex_and_PermutA_and_.
rewrite support_empty in h_ex_and_PermutA_and_.
- decompose [ex and] h_ex_and_PermutA_and_ /gn.
- assert (length (@nil location) = length (x::x0::nil))/n.
+ destruct h_ex_and_PermutA_and_
+ as [ x [ x0 [ h_PermutA_nil_cons_x_x0_ [
+ h_eq_mult_x_empty_div2_add_
+ [ h_eq_mult_x0_empty_div2_add_ h_all_eq_mult_0_]]]]].
+
+ assert (length (@nil location) = length (x::x0::nil)) as h_eq_length_nil_length_cons_ .
{ rewrite h_PermutA_nil_cons_x_x0_ at 1;auto. }
cbn in h_eq_length_nil_length_cons_.
discriminate h_eq_length_nil_length_cons_. }
@@ -1175,10 +1201,13 @@ Proof.
destruct l as [ | b l'].
{ right.
intro abs.
- specialize obs_invalid_doubleton with (1:=abs) as ?/n.
+ specialize obs_invalid_doubleton with (1:=abs).
+ intro h_ex_and_PermutA_and_ .
rewrite heq in *.
- decompose [ex and] h_ex_and_PermutA_and_ /gn.
- assert (length (a::nil) = length (x::x0::nil))/n.
+ destruct h_ex_and_PermutA_and_
+ as [x [ x0 [ h_PermutA_cons_a_cons_x_x0_
+ [ h_eq_mult_x_o_div2_add_ [ h_eq_mult_x0_o_div2_add_ h_all_eq_mult_0_]]]]].
+ assert (length (a::nil) = length (x::x0::nil)) as h_eq_length_cons_length_cons_.
{ rewrite h_PermutA_cons_a_cons_x_x0_;auto. }
cbn in h_eq_length_cons_length_cons_.
discriminate h_eq_length_cons_length_cons_. }
@@ -1186,10 +1215,14 @@ Proof.
all:swap 1 2.
{ right.
intro abs.
- specialize obs_invalid_doubleton with (1:=abs) as ?/n.
+ specialize obs_invalid_doubleton with (1:=abs).
+ intro h_ex_and_PermutA_and_ .
rewrite heq in *.
- decompose [ex and] h_ex_and_PermutA_and_ /gn.
- assert (length (a::b::c::l'') = length (x::x0::nil))/n.
+ destruct h_ex_and_PermutA_and_
+ as [x [ x0 [ h_PermutA_cons_a_b_cons_x_x0_
+ [ h_eq_mult_x_o_div2_add_
+ [ h_eq_mult_x0_o_div2_add_ h_all_eq_mult_0_]]]]].
+ assert (length (a::b::c::l'') = length (x::x0::nil)) as h_eq_length_cons_length_cons_.
{ rewrite h_PermutA_cons_a_b_cons_x_x0_;auto. }
cbn in h_eq_length_cons_length_cons_.
discriminate h_eq_length_cons_length_cons_. }
@@ -1202,18 +1235,18 @@ Proof.
rewrite Nat.add_0_r in h_card.
destruct (Nat.eq_dec (o[a]) (o[b])).
- left.
- assert (Nat.Even (cardinal o)) as ?/n.
+ assert (Nat.Even (cardinal o)) as h_Even_card_o_ .
{ rewrite e in h_card.
replace (o[b] + o[b]) with (2 * o[b]) in h_card;[|lia].
red.
eauto. }
- assert (cardinal o = (2 * (Nat.div2 (cardinal o + 1)))) /n.
- { specialize even_div2 with (1:=h_Even_card_o_) as ?/n.
+ assert (cardinal o = (2 * (Nat.div2 (cardinal o + 1)))).
+ { specialize even_div2 with (1:=h_Even_card_o_) as h_eq_add_div2_div2_card_o_ .
rewrite <- even_div2_p1 in h_eq_add_div2_div2_card_o_;auto.
lia. }
- assert (o[a] = (Nat.div2 (cardinal o + 1))) /n.
+ assert (o[a] = (Nat.div2 (cardinal o + 1))) as h_eq_mult_a_o_div2_add_.
{ lia. }
- assert (o[b] = (Nat.div2 (cardinal o + 1))) /n.
+ assert (o[b] = (Nat.div2 (cardinal o + 1))) as h_eq_mult_b_o_div2_add_.
{ lia. }
red. exists a, b;repeat (split;auto).
+ apply NoDupA_2fst with (l:=nil).
@@ -1234,18 +1267,20 @@ Proof.
apply cardinal_lower.
- right.
intro h_abs.
- specialize obs_invalid_doubleton with (1:=h_abs) as ?/n.
-
-
+ specialize obs_invalid_doubleton with (1:=h_abs) as h_ex_and_PermutA_and_ .
rewrite heq in *.
- decompose [ex and] h_ex_and_PermutA_and_ /gn; clear h_ex_and_PermutA_and_.
-
- assert (support o = [x ;x0] \/ support o = [x0 ;x]) /n.
+ destruct h_ex_and_PermutA_and_
+ as [ x [ x0
+ [ h_PermutA_cons_a_b_cons_x_x0_
+ [ h_eq_mult_x_o_div2_add_
+ [ h_eq_mult_x0_o_div2_add_ h_all_eq_mult_0_]]]]].
+ assert (support o = [x ;x0] \/ support o = [x0 ;x]) as h_or_eq_support_cons_eq_support_cons_.
{ rewrite heq.
- specialize (@PermutationA_2 _ equiv _ a b x x0) as ?/n.
- destruct h_iff_PermutA_cons_cons_or_and_and_; intros /n.
+ specialize (@PermutationA_2 _ equiv _ a b x x0) as h_iff_PermutA_cons_cons_or_and_and_.
+ destruct h_iff_PermutA_cons_cons_or_and_and_ as [ h_impl_or_and_and_ ]; intros.
specialize h_impl_or_and_and_ with (1:=h_PermutA_cons_a_b_cons_x_x0_).
- decompose [and or] h_impl_or_and_and_ /n .
+ (* decompose [and or] h_impl_or_and_and_ /n . *)
+ destruct h_impl_or_and_and_ as [ [ h_equiv_a_x_ h_equiv_b_x0_ ] | [ h_equiv_a_x0_ h_equiv_b_x_] ].
- left.
cbn in h_equiv_a_x_,h_equiv_b_x0_.
rewrite h_equiv_a_x_,h_equiv_b_x0_.
@@ -1254,18 +1289,19 @@ Proof.
cbn in h_equiv_a_x0_,h_equiv_b_x_.
rewrite h_equiv_a_x0_,h_equiv_b_x_.
reflexivity. }
- destruct h_or_eq_support_cons_eq_support_cons_ /n.
+ destruct h_or_eq_support_cons_eq_support_cons_
+ as [h_eq_support_o_cons_x_x0_ | h_eq_support_o_cons_x0_x_ ].
+ rewrite heq in h_eq_support_o_cons_x_x0_.
- inversion h_eq_support_o_cons_x_x0_/sng.
+ inversion h_eq_support_o_cons_x_x0_;subst.
rewrite <- h_eq_mult_x0_o_div2_add_ in h_eq_mult_x_o_div2_add_.
contradiction.
+ rewrite heq in h_eq_support_o_cons_x0_x_.
- inversion h_eq_support_o_cons_x0_x_/sng.
+ inversion h_eq_support_o_cons_x0_x_;subst.
rewrite <- h_eq_mult_x_o_div2_add_ in h_eq_mult_x0_o_div2_add_.
contradiction.
Defined.
-Ltac rename_depth ::= constr:(2).
+(* Ltac rename_depth ::= constr:(2). *)
(* Local Instance gatherW_pgm_compat : Proper (@equiv _ observation_Setoid ==> ???) obs_invalid_dec. *)
@@ -1275,10 +1311,10 @@ Lemma obs_invalid_dec_compat_left: forall o o': observation,
obs_invalid_dec o = left h ->
exists h', obs_invalid_dec o' = left h'.
Proof.
- intros/n.
- destruct (obs_invalid_dec o') eqn:?/n;eauto.
+ intros o o' h_equiv_o_o'_ h_invalid_obs_o_ h_eq_obs_invalid_dec_left_ .
+ destruct (obs_invalid_dec o') as [h_invalid_obs_o'_ | h_not_invalid_obs_ ] eqn:h_eq_obs_invalid_dec_ ;eauto.
foldR2.
- clear h_eq_obs_invalid_dec_left_ h_eq_obs_invalid_dec_right_.
+ clear h_eq_obs_invalid_dec_left_ h_eq_obs_invalid_dec_.
setoid_rewrite h_equiv_o_o'_ in h_invalid_obs_o_.
contradiction.
Qed.
@@ -1290,10 +1326,10 @@ Lemma obs_invalid_dec_compat_right: forall o o': observation,
obs_invalid_dec o = right h ->
exists h', obs_invalid_dec o' = right h'.
Proof.
- intros/n.
- destruct (obs_invalid_dec o') eqn:?/n;eauto.
+ intros o o' h_equiv_o_o'_ h_not_invalid_obs_ h_eq_obs_invalid_dec_right_ .
+ destruct (obs_invalid_dec o') eqn:h_eq_obs_invalid_dec_;eauto.
foldR2.
- clear h_eq_obs_invalid_dec_left_ h_eq_obs_invalid_dec_right_.
+ clear h_eq_obs_invalid_dec_ h_eq_obs_invalid_dec_right_.
setoid_rewrite h_equiv_o_o'_ in h_not_invalid_obs_.
contradiction.
Qed.
@@ -1407,6 +1443,38 @@ rewrite multi_support_config. unfold pos_list. rewrite config_list_map, map_map.
(* repeat split ; cbn -[equiv] ; auto. *)
Qed.
+Lemma multi_support_non_nil f config :
+ Proper (equiv ==> equiv) (projT1 f) ->
+ multi_support (!! (map_config (lift f) config)) <> [].
+Proof using lt_0n.
+ intros h' abs.
+ specialize (@multi_support_map f config h').
+ intros H.
+ rewrite abs in H.
+ symmetry in H.
+ apply Preliminary.PermutationA_nil in H.
+ apply map_eq_nil in H.
+ eelim pos_list_non_nil.
+ - eassumption.
+ - typeclasses eauto.
+Qed.
+
+Lemma multi_support_non_nil2 (config : configuration):
+ multi_support (!! config) <> [].
+Proof.
+ intro abs.
+ specialize (@multi_support_config config) as h.
+ foldR2.
+ rewrite abs in h.
+ apply pos_list_non_nil with config.
+ foldR2.
+ eapply Preliminary.PermutationA_nil.
+ 2:{ symmetry.
+ eapply h. }
+ typeclasses eauto.
+Qed.
+
+
Corollary multiplicity_countA config x :
(!! config)[x] = countA_occ equiv R2_EqDec x (pos_list config).
Proof using . now rewrite <-multi_support_config, multi_support_countA. Qed.
@@ -1424,14 +1492,14 @@ Proof using.
rewrite <- (pos_list_length config).
remember (pos_list config) as l.
symmetry in h_neq.
- specialize (@countA_occ_removeA_other _ _ _ location_EqDec y x l h_neq) as ?/n.
+ specialize (@countA_occ_removeA_other _ _ _ location_EqDec y x l h_neq) as h_eq_countA_occ_countA_occ_ .
foldR2.
rewrite <- h_eq_countA_occ_countA_occ_.
assert (countA_occ equiv location_EqDec y l <= length (removeA (eqA:=equiv) location_EqDec x l)).
{ rewrite <- h_eq_countA_occ_countA_occ_.
apply countA_occ_length_le. }
assert (length (removeA (eqA:=equiv) location_EqDec x l) + countA_occ equiv location_EqDec x l = length l).
- { specialize (@PermutationA_count_split _ _ _ location_EqDec x l) as ?/n.
+ { specialize (@PermutationA_count_split _ _ _ location_EqDec x l) as h_PermutA_l_app_ .
rewrite h_PermutA_l_app_ at 3.
rewrite app_length.
rewrite alls_length.
@@ -1446,38 +1514,38 @@ Lemma multiplicity_sum3_bound x y z config :
(!!config)[x] + (!!config)[y] + (!!config)[z] <= n.
Proof using .
clear lt_0n delta_g0.
- intros /n.
+ intros h_nequiv_x_y_ h_nequiv_y_z_ h_nequiv_x_z_ .
fold info0.
repeat rewrite multiplicity_countA.
remember (pos_list config) as l.
symmetry in h_nequiv_x_y_.
- specialize (@countA_occ_removeA_other _ _ _ location_EqDec y x l h_nequiv_x_y_) as ?/n.
+ specialize (@countA_occ_removeA_other _ _ _ location_EqDec y x l h_nequiv_x_y_) as h_eq_countA_occ_countA_occ_ .
foldR2.
rewrite <- h_eq_countA_occ_countA_occ_.
symmetry in h_nequiv_x_z_.
- specialize (@countA_occ_removeA_other _ _ _ location_EqDec z x l h_nequiv_x_z_) as ?/n.
+ specialize (@countA_occ_removeA_other _ _ _ location_EqDec z x l h_nequiv_x_z_) as h_eq_countA_occ_countA_occ_0 .
foldR2.
rewrite <- h_eq_countA_occ_countA_occ_0.
symmetry in h_nequiv_y_z_.
- specialize (@countA_occ_removeA_other _ _ _ location_EqDec z y (removeA (eqA:=equiv) location_EqDec x l) h_nequiv_y_z_) as ?/n.
+ specialize (@countA_occ_removeA_other _ _ _ location_EqDec z y (removeA (eqA:=equiv) location_EqDec x l) h_nequiv_y_z_) as h_eq_countA_occ_countA_occ_1 .
foldR2.
rewrite <- h_eq_countA_occ_countA_occ_1.
remember (removeA (eqA:=equiv) location_EqDec x l) as l_nox.
remember (removeA (eqA:=equiv) location_EqDec y l_nox) as l_noxy.
- assert (countA_occ equiv location_EqDec y l <= length l_nox) as ?/n.
+ assert (countA_occ equiv location_EqDec y l <= length l_nox) as h_le_countA_occ_length_ .
{ rewrite <- h_eq_countA_occ_countA_occ_.
apply countA_occ_length_le. }
- assert (countA_occ equiv location_EqDec z l_nox <= length l_noxy) as ?/n.
+ assert (countA_occ equiv location_EqDec z l_nox <= length l_noxy) as h_le_countA_occ_length_0 .
{ rewrite <- h_eq_countA_occ_countA_occ_1.
apply countA_occ_length_le. }
- assert (length (removeA (eqA:=equiv) location_EqDec x l) + countA_occ equiv location_EqDec x l = length l) as ?/n.
- { specialize (@PermutationA_count_split _ _ _ location_EqDec x l) as ?/n.
+ assert (length (removeA (eqA:=equiv) location_EqDec x l) + countA_occ equiv location_EqDec x l = length l) as h_eq_add_length_ .
+ { specialize (@PermutationA_count_split _ _ _ location_EqDec x l) as h_PermutA_l_app_ .
rewrite h_PermutA_l_app_ at 3.
rewrite app_length.
rewrite alls_length.
lia. }
- assert (length (removeA (eqA:=equiv) location_EqDec y l_nox) + countA_occ equiv location_EqDec y l_nox = length l_nox) as ?/n.
- { specialize (@PermutationA_count_split _ _ _ location_EqDec y l_nox) as ?/n.
+ assert (length (removeA (eqA:=equiv) location_EqDec y l_nox) + countA_occ equiv location_EqDec y l_nox = length l_nox) as h_eq_add_length_0 .
+ { specialize (@PermutationA_count_split _ _ _ location_EqDec y l_nox) as h_PermutA_l_nox_app_ .
rewrite h_PermutA_l_nox_app_ at 3.
rewrite app_length.
rewrite alls_length.
@@ -1485,7 +1553,7 @@ Proof using .
remember (countA_occ equiv location_EqDec x l) as h_l.
remember (countA_occ equiv location_EqDec y l_nox) as h_l_nox.
remember (countA_occ equiv location_EqDec z l_noxy) as h_l_noxy.
- specialize (n_cardinal config info0) as ?/n.
+ specialize (n_cardinal config info0) as h_eq_card_n_ .
rewrite <- (pos_list_length config).
rewrite <- Heql in *.
subst.
@@ -1607,7 +1675,7 @@ Proof using Type.
(multi_support o) == find (fun x : R2 => countA_occ equiv R2_EqDec x ps ==b Nat.div2 (cardinal o + 1))
(multi_support o)).
{ apply find_compat.
- - intros x y ?/n.
+ - intros x y h_equiv_x_y_ .
rewrite h_equiv_x_y_.
foldR2.
specialize countA_occ_compat with (eqA:=@eq (@location Loc)) as h.
@@ -1654,11 +1722,7 @@ Proof using Type.
* unfold multi_support in hinr.
apply in_flat_map_Exists in hinr.
apply Exists_exists in hinr.
- decompose [ex and] hinr /n.
-
-
-
-
+ destruct hinr as [ x [h_In_x_elements_ h_In_r_] ].
symmetry.
apply Nat.lt_neq.
apply Nat.lt_le_trans with (size o).
@@ -1691,7 +1755,7 @@ Proof.
foldR2.
- specialize (from_elements_elements o) as ?/n.
+ specialize (from_elements_elements o) as h_equiv_from_elements_o_ .
foldR2.
rewrite <- h_equiv_from_elements_o_ at 2.
rewrite cardinal_from_elements.
@@ -1699,25 +1763,27 @@ Proof.
unfold multi_support.
rewrite flat_map_concat_map.
-
- assert (forall l k, fold_left (fun (x : nat) (_ : elt) => S x) (concat (List.map (fun '(x, mx) => alls x mx) l)) k =
- fold_left (fun (acc : nat) (xn : elt * nat) => snd xn + acc) l k).
- { induction l;simpl;intros/sng;auto.
- destruct a.
- cbn.
- rewrite fold_left_app.
- assert ((fold_left (fun (x : nat) (_ : elt) => S x) (alls e n0) k) = n0 + k) /n.
- { assert (forall l k, (fold_left (fun (x : nat) (_ : elt) => S x) l k) = length l + k) /n.
- { induction l0;simpl;auto.
- intros k0.
- rewrite IHl0.
- lia. }
- rewrite h_all_eq_0.
- rewrite alls_length.
- reflexivity.
- }
- rewrite h_eq_fold_left_add_.
- apply h_all_eq_.
+ assert (forall l k,
+ fold_left (fun (x : nat) (_ : elt) => S x) (concat (List.map (fun '(x, mx) => alls x mx) l)) k =
+ fold_left (fun (acc : nat) (xn : elt * nat) => snd xn + acc) l k).
+ { induction l as [ | a l h_all_eq_ ].
+ - simpl;intros;auto.
+ - simpl;intros.
+ destruct a.
+ cbn.
+ rewrite fold_left_app.
+ assert ((fold_left (fun (x : nat) (_ : elt) => S x) (alls e n0) k) = n0 + k) as h_eq_fold_left_add_.
+ { assert (forall l k, (fold_left (fun (x : nat) (_ : elt) => S x) l k) = length l + k) as h_all_eq_0.
+ { induction l0;simpl;auto.
+ intros k0.
+ rewrite IHl0.
+ lia. }
+ rewrite h_all_eq_0.
+ rewrite alls_length.
+ reflexivity.
+ }
+ rewrite h_eq_fold_left_add_.
+ apply h_all_eq_.
}
apply H0.
Qed.
@@ -1726,7 +1792,7 @@ Qed.
Local Instance gatherW_pgm_compat : Proper (@equiv _ observation_Setoid ==> @equiv _ location_Setoid) gatherW_pgm.
Proof using lt_0n.
clear delta_g0.
- intros ? ? H/g.
+ intros x y H .
unfold observation,multiset_observation in x.
specialize @multi_support_compat as hsupp.
@@ -1747,33 +1813,36 @@ Proof using lt_0n.
clear h' h_eq_obs_inv.
foldR2.
- assert (length (multi_support x) == length (multi_support y)) /n.
+ assert (length (multi_support x) == length (multi_support y)) as h_equiv_length_length_ .
{ rewrite hsupp.
reflexivity. }
foldR2.
rewrite <- h_equiv_length_length_.
- destruct (length (multi_support x) =?= 0)eqn:? /n.
+ destruct (length (multi_support x) =?= 0) as [ h_equiv_length_0_ | h_nequiv_length_0_ ] eqn:h_eq_equiv_dec.
{ reflexivity. }
- clear h_eq_equiv_dec_right_.
+ clear h_eq_equiv_dec.
- assert (multi_support x <> []) /n.
+ assert (multi_support x <> []) as h_neq_multi_support_nil_ .
{ intro abs.
rewrite abs in h_nequiv_length_0_.
cbn in h_nequiv_length_0_.
now apply h_nequiv_length_0_. }
foldR2.
- destruct (weber_calc_seg (multi_support x)) eqn: hcalcx/g.
- destruct (weber_calc_seg (multi_support y)) eqn: hcalcy/g.
+ destruct (weber_calc_seg (multi_support x)) eqn: hcalcx.
+ destruct (weber_calc_seg (multi_support y)) eqn: hcalcy.
foldR2.
red in h.
- destruct (r =?= r0);destruct (r1 =?= r2)/n.
- { decompose [or and] h /n;clear h.
+ destruct (r =?= r0) as [h_equiv_r_r0_ | h_nequiv_r_r0_];
+ destruct (r1 =?= r2) as [ h_equiv_r1_r2_ | h_nequiv_r1_r2_ ].
+
+
+ { decompose [or and] h ;clear h.
+ assumption.
+ now rewrite h_equiv_r_r0_. }
{ exfalso.
- decompose [or and] h /n;clear h.
+ destruct h as [ [h_equiv_r_r1_ h_equiv_r0_r2_] | [h_equiv_r_r2_ h_equiv_r0_r1_]].
+ rewrite <- h_equiv_r_r0_ in h_equiv_r0_r2_.
rewrite h_equiv_r_r1_ in h_equiv_r0_r2_.
contradiction.
@@ -1782,7 +1851,7 @@ Proof using lt_0n.
rewrite h_equiv_r_r2_ in h_equiv_r0_r1_.
contradiction. }
{ exfalso.
- decompose [or and] h /n;clear h.
+ destruct h as [[h_equiv_r_r1_ h_equiv_r0_r2_] | [h_equiv_r_r2_ h_equiv_r0_r1_]].
+ symmetry in h_equiv_r0_r2_.
rewrite <- h_equiv_r1_r2_ in h_equiv_r0_r2_.
rewrite <- h_equiv_r_r1_ in h_equiv_r0_r2_.
@@ -1793,48 +1862,50 @@ Proof using lt_0n.
contradiction. }
(* From here the Weber segment is not a single point, therefore:
- all points are aligned. *)
- assert (cardinal x = cardinal y) /n.
+ assert (cardinal x = cardinal y) as h_eq_card_card_ .
{ rewrite <- multi_set_length_cardinal.
rewrite <- multi_set_length_cardinal.
eapply Preliminary.PermutationA_length;eauto;try typeclasses eauto. }
rewrite <- h_eq_card_card_.
- specialize robot_with_mult_unique_obs with (1:=n0) (2:=hsupp) as?/n.
+ specialize robot_with_mult_unique_obs with (1:=n0) (2:=hsupp)
+ as h_equiv_robot_with_mult_robot_with_mult_ .
cbn -[robot_with_mult cardinal multi_support] in h_equiv_robot_with_mult_robot_with_mult_.
apply opt_eq_leibnitz in h_equiv_robot_with_mult_robot_with_mult_.
foldR2.
rewrite <- h_equiv_robot_with_mult_robot_with_mult_.
- destruct (robot_with_mult (Nat.div2 (cardinal x + 1)) (multi_support x)) eqn:?/ng.
+ destruct (robot_with_mult (Nat.div2 (cardinal x + 1)) (multi_support x))
+ as [l | h_eq_robot_with_mult_None_] eqn:h_eq_robot_with_mult_l_ .
{ cbn -[multi_support].
now rewrite hsupp. }
- remember (line_calc (multi_support x)) as Lx/g.
- remember (line_calc (multi_support y)) as Ly/g.
+ remember (line_calc (multi_support x)) as Lx.
+ remember (line_calc (multi_support y)) as Ly.
lazy zeta.
- (remember ((Lx ^-P) ((Lx ^min) (multi_support x))) as r3)/g.
- remember ((Lx ^-P) ((Lx ^max) (multi_support x))) as r4 /g.
- remember ((Ly ^-P) ((Ly ^min) (multi_support y))) as r3' /g.
- remember ((Ly ^-P) ((Ly ^max) (multi_support y))) as r4' /g.
+ (remember ((Lx ^-P) ((Lx ^min) (multi_support x))) as r3).
+ remember ((Lx ^-P) ((Lx ^max) (multi_support x))) as r4.
+ remember ((Ly ^-P) ((Ly ^min) (multi_support y))) as r3'.
+ remember ((Ly ^-P) ((Ly ^max) (multi_support y))) as r4'.
assert (aligned (multi_support x)).
- { assert (Weber (multi_support x) r) as ? /n.
+ { assert (Weber (multi_support x) r) as h_Weber_multi_support_r_ .
{ specialize weber_calc_seg_correct with (ps:=(multi_support x))(w:=r)(1:=h_neq_multi_support_nil_)
as h_webercalc.
rewrite hcalcx in h_webercalc.
apply h_webercalc.
apply segment_start. }
- assert (Weber (multi_support x) r0) as ? /n.
+ assert (Weber (multi_support x) r0) as h_Weber_multi_support_r0_ .
{ specialize weber_calc_seg_correct with (ps:=(multi_support x))(w:=r0)(1:=h_neq_multi_support_nil_)
as h_webercalc.
rewrite hcalcx in h_webercalc.
apply h_webercalc.
apply segment_end. }
- destruct (aligned_dec (multi_support x)); auto/n.
+ destruct (aligned_dec (multi_support x)); auto.
exfalso.
- assert (OnlyWeber (multi_support x) r) as ? /n.
+ assert (OnlyWeber (multi_support x) r) as h_OnlyWeber_multi_support_r_ .
{ eapply weber_Naligned_unique;eauto. }
red in h_OnlyWeber_multi_support_r_.
- decompose [and] h_OnlyWeber_multi_support_r_; clear h_OnlyWeber_multi_support_r_ /n.
+ destruct h_OnlyWeber_multi_support_r_ as [ h_Weber_multi_support_r_0 h_all_equiv_ ].
specialize h_all_equiv_ with (x:=r0) (1:=h_Weber_multi_support_r0_).
symmetry in h_all_equiv_.
contradiction. }
@@ -1842,15 +1913,15 @@ Proof using lt_0n.
{ now rewrite <- hsupp. }
specialize @line_endpoints_invariant with (ps := multi_support x) (L1:=Lx)(L2:=Ly)
- as ? /n.
+ as h_all_perm_pairA_ .
specialize h_all_perm_pairA_ with (1:=h_neq_multi_support_nil_).
- assert (aligned_on Lx (multi_support x))/n.
+ assert (aligned_on Lx (multi_support x)) as h_aligned_on_Lx_multi_support_ .
{ rewrite HeqLx.
rewrite <- line_calc_spec.
eassumption. }
specialize h_all_perm_pairA_ with (1:=h_aligned_on_Lx_multi_support_).
- assert (aligned_on Ly (multi_support x))/n.
+ assert (aligned_on Ly (multi_support x)) as h_aligned_on_Ly_multi_support_ .
{ rewrite hsupp.
rewrite HeqLy.
rewrite <- line_calc_spec.
@@ -1866,9 +1937,9 @@ Proof using lt_0n.
rewrite <- Heqr4' in h_all_perm_pairA_.
- assert ((middle r3 r4) = (middle r3' r4')) /n.
+ assert ((middle r3 r4) = (middle r3' r4')) as h_eq_middle_middle_ .
{ red in h_all_perm_pairA_.
- decompose [or and] h_all_perm_pairA_ /n ; clear h_all_perm_pairA_.
+ destruct h_all_perm_pairA_ as [[h_equiv_r3_r3'_ h_equiv_r4_r4'_] | [ h_equiv_r3_r4'_ h_equiv_r4_r3'_ ]].
- rewrite h_equiv_r3_r3'_,h_equiv_r4_r4'_.
reflexivity.
- rewrite <- h_equiv_r3_r4'_, h_equiv_r4_r3'_.
@@ -1876,17 +1947,17 @@ Proof using lt_0n.
foldR2.
rewrite <- h_eq_middle_middle_.
- assert (segment_decb r r0 (middle r3 r4) == segment_decb r1 r2 (middle r3 r4)) /n.
+ assert (segment_decb r r0 (middle r3 r4) == segment_decb r1 r2 (middle r3 r4)) as h_equiv_segment_decb_segment_decb_ .
{
- decompose [and or ] h /n.
+ destruct h as [[ h_equiv_r_r1_ h_equiv_r0_r2_ ] | [h_equiv_r_r2_ h_equiv_r0_r1_ ]].
+ rewrite <- h_equiv_r_r1_,h_equiv_r0_r2_.
reflexivity.
+ rewrite <- h_equiv_r_r2_,h_equiv_r0_r1_.
apply segment_decb_sym. }
rewrite h_equiv_segment_decb_segment_decb_.
- destruct (segment_decb r1 r2 (middle r3 r4)) eqn:? /n.
- { decompose [and or ] h /n.
+ destruct (segment_decb r1 r2 (middle r3 r4)) eqn:h_eq_segment_decb.
+ { destruct h as[[h_equiv_r_r1_ h_equiv_r0_r2_]|[h_equiv_r_r2_ h_equiv_r0_r1_]].
- rewrite <- h_equiv_r_r1_,h_equiv_r0_r2_.
reflexivity.
- rewrite <- h_equiv_r_r2_,h_equiv_r0_r1_.
@@ -1896,7 +1967,7 @@ Proof using lt_0n.
(* TODO: lemma *)
assert (forall {T : Type} {S0 : Setoid T} {EQ0 : EqDec S0} {VS : RealVectorSpace T} (a b x : T), ~ segment a b x -> ~ strict_segment a b x) as not_strict_segment_not_seg.
- { intros /n.
+ { intros.
intro abs.
apply strict_segment_incl in abs.
contradiction. }
@@ -1913,16 +1984,16 @@ Proof using lt_0n.
-> p =/= b
-> ~segment p a b
) as h_lemma2.
- { intros /gn.
+ { intros a b p h_segment_a_b_p_ h_nequiv_p_b_ .
rewrite segment_dist_sum in h_segment_a_b_p_.
intro abs.
rewrite segment_dist_sum in abs.
rewrite dist_sym in abs at 1.
rewrite (dist_sym a b) in abs.
rewrite abs in h_segment_a_b_p_.
- assert (0 <= dist a b)%R by now apply dist_nonneg /n.
- assert (0 <= dist p b)%R by now apply dist_nonneg /n.
- assert (dist p b = 0)%R /n.
+ assert (0 <= dist a b)%R by now apply dist_nonneg.
+ assert (0 <= dist p b)%R by now apply dist_nonneg.
+ assert (dist p b = 0)%R as h_eq_dist_IZR_.
{ foldR2.
remember (dist p b) as x1.
remember (dist a b) as x2.
@@ -1937,8 +2008,8 @@ Proof using lt_0n.
line_contains L b ->
line_contains L p ->
(strict_segment p a b \/ strict_segment p b a) \/ segment a b p) as h_lemma.
- { intros/ng.
- specialize segment_line with (L:=L) as ?/n.
+ { intros T S0 EQ0 VS ES a b p L h_nequiv_a_b_ h_line_contains_L_a_ h_line_contains_L_b_ h_line_contains_L_p_ .
+ specialize segment_line with (L:=L) as h_all_iff_ .
specialize h_all_iff_ with (1:=h_line_contains_L_a_) (2:=h_line_contains_L_b_) (3:=h_line_contains_L_p_) as h_abp.
specialize h_all_iff_ with (2:=h_line_contains_L_a_) (3:=h_line_contains_L_b_) (1:=h_line_contains_L_p_) as h_pab.
specialize h_all_iff_ with (3:=h_line_contains_L_a_) (2:=h_line_contains_L_b_) (1:=h_line_contains_L_p_) as h_pba.
@@ -1972,16 +2043,17 @@ Proof using lt_0n.
lra. }
specialize (@h_lemma _ _ _ LocVS LocES) with (L:=Lx)(p := (@middle _ _ _ LocVS r3 r4)) (a:=r) (b:=r0) (1:=h_nequiv_r_r0_).
- destruct (h_lemma) as [[ ? | ? ] | ?] /n.
+ destruct (h_lemma) as [[ h_strict_segment_middle_r_r0_ | h_strict_segment_middle_r0_r_] | h_segment_r_r0_middle_ ].
all:cycle 3.
- red in h_strict_segment_middle_r_r0_.
- decompose [and] h_strict_segment_middle_r_r0_ /n.
+ destruct h_strict_segment_middle_r_r0_ as [ h_segment_middle_r_r0_ [h_nequiv_r0_middle_ h_nequiv_r0_r_ ]] .
+ (* decompose [and] h_strict_segment_middle_r_r0_ /n h_segment_middle_r_r0_ h_nequiv_r0_middle_ h_nequiv_r0_r_ . *)
specialize h_lemma2 with (1:=h_segment_middle_r_r0_) (2:=h_nequiv_r0_r_).
rewrite segment_sym in h_lemma2.
apply segment_decb_true in h_segment_middle_r_r0_.
apply segment_decb_false in h_lemma2.
foldR2.
- decompose [and or] h/n.
+ destruct h as [[h_equiv_r_r1_ h_equiv_r0_r2_]|[h_equiv_r_r2_ h_equiv_r0_r1_]].
+ repeat rewrite <- h_equiv_r_r1_.
repeat rewrite <-h_equiv_r0_r2_.
rewrite h_segment_middle_r_r0_.
@@ -1993,13 +2065,13 @@ Proof using lt_0n.
rewrite h_lemma2.
reflexivity.
- red in h_strict_segment_middle_r0_r_.
- decompose [and] h_strict_segment_middle_r0_r_ /n.
+ destruct h_strict_segment_middle_r0_r_ as [ h_segment_middle_r0_r_ [ h_nequiv_r_middle_ h_nequiv_r_r0_0 ]] .
specialize h_lemma2 with (1:=h_segment_middle_r0_r_)(2:=h_nequiv_r_r0_0).
rewrite segment_sym in h_lemma2.
apply segment_decb_true in h_segment_middle_r0_r_.
apply segment_decb_false in h_lemma2.
foldR2.
- decompose [and or] h/n.
+ destruct h as [[h_equiv_r_r1_ h_equiv_r0_r2_]|[h_equiv_r_r2_ h_equiv_r0_r1_]].
+ repeat rewrite <- h_equiv_r_r1_.
repeat rewrite <-h_equiv_r0_r2_.
rewrite h_segment_middle_r0_r_.
@@ -2011,7 +2083,7 @@ Proof using lt_0n.
rewrite h_lemma2.
reflexivity.
- specialize h_lemma2 with (1:=h_segment_r_r0_middle_).
- assert (middle r3 r4 =/= r0)/n.
+ assert (middle r3 r4 =/= r0) as h_nequiv_middle_r0_ .
{ foldR2.
apply segment_decb_false in h_equiv_segment_decb_segment_decb_.
intro abs.
@@ -2022,13 +2094,12 @@ Proof using lt_0n.
apply segment_decb_true in h_segment_r_r0_middle_.
apply segment_decb_false in h_lemma2.
foldR2.
- decompose [and or] h/n.
+ destruct h as [ [h_equiv_r_r1_ h_equiv_r0_r2_] | [h_equiv_r_r2_ h_equiv_r0_r1_] ].
+ repeat rewrite <- h_equiv_r_r1_.
repeat rewrite <-h_equiv_r0_r2_.
rewrite h_lemma2.
reflexivity.
- +
- repeat rewrite <- h_equiv_r0_r1_.
+ + repeat rewrite <- h_equiv_r0_r1_.
repeat rewrite <-h_equiv_r_r2_.
rewrite h_lemma2.
reflexivity.
@@ -2121,16 +2192,22 @@ cbn -[segment_decb strict_segment_decb middle robot_with_mult Nat.div sim
config_list get_location multi_support equiv_dec line_proj line_proj_inv] ; repeat split ; [].
apply (Similarity.injective sim). rewrite Bijection.section_retraction. foldR2.
-assert (Hw := weber_calc_seg_correct (pos_list config)).
+
+specialize weber_calc_seg_correct with (1:=(pos_list_non_nil config)) as Hw.
destruct (weber_calc_seg (pos_list config)) as [w1 w2].
-assert (Hw' := weber_calc_seg_correct (multi_support obs)).
+foldR2.
+assert (Hw' := @weber_calc_seg_correct (multi_support obs)).
destruct (weber_calc_seg (multi_support obs)) as [w1' w2'].
assert (Hw_perm : perm_pairA equiv (sim w1, sim w2) (w1', w2')).
{
apply segment_eq_iff. intros x. rewrite <-(Bijection.section_retraction sim x).
- rewrite <-R2segment_similarity, <-Hw, <-Hw'.
+ rewrite <-R2segment_similarity.
+ rewrite <-Hw.
+ foldR2.
+ rewrite <-Hw'.
change obs with (!! (map_config (lift f) config)). rewrite multi_support_map by auto.
cbn [projT1 f]. fold sim. now rewrite <-weber_similarity.
+ apply multi_support_non_nil2.
}
clear Hw'.
diff --git a/CaseStudies/Gathering/InR2/Weber/Line.v b/CaseStudies/Gathering/InR2/Weber/Line.v
index 8359b089eded1379325f30fe1d9de6dbab45ea4e..6b2a93a4f1a550869f4fb3d4a9c30dc3dba81456 100644
--- a/CaseStudies/Gathering/InR2/Weber/Line.v
+++ b/CaseStudies/Gathering/InR2/Weber/Line.v
@@ -194,6 +194,14 @@ Qed.
Definition line_contains L x : Prop := L^-P (L^P x) == x.
+Lemma line_contains_proj_inv: forall L (t:R),
+ line_dir L =/= 0 -> line_contains L (L^-P t).
+Proof.
+ intros L t h.
+ red.
+ rewrite line_P_iP;auto.
+Qed.
+
Global Instance line_contains_compat :
Proper (equiv ==> equiv ==> iff) line_contains.
Proof. intros ? ? H1 ? ? H2. unfold line_contains. now rewrite H1, H2. Qed.
@@ -765,6 +773,22 @@ Proof.
intros ? ? H1 ? ? H2 ? ? H3. unfold line_on. f_equiv ; [|exact H3].
intros ? ? H4. now rewrite H1, H2, H4.
Qed.
+
+Global Instance line_on_perm_compat :
+ Proper (equiv ==> equiv ==> PermutationA equiv ==> PermutationA equiv) line_on.
+Proof.
+intros ? ? H1 ? ? H2 ? ? H3. unfold line_on.
+rewrite filter_extensionalityA_compat.
+- apply filter_PermutationA_compat.
+ + repeat intro.
+ rewrite H0.
+ reflexivity.
+ + eassumption.
+- repeat intro.
+ rewrite H2,H0,H1.
+ reflexivity.
+- reflexivity.
+Qed.
Notation "L '^left'" := (line_left L).
Notation "L '^right'" := (line_right L).
@@ -777,6 +801,181 @@ Proof. unfold line_right. apply filter_inclA. intros ? ? Heq. now rewrite Heq. Q
Lemma line_on_inclA L x ps : inclA equiv (L^on x ps) ps.
Proof. unfold line_on. apply filter_inclA. intros ? ? Heq. now rewrite Heq. Qed.
+Lemma line_left_inclA_2 L a ps b:
+ InA equiv b (L^left a ps) ->
+ inclA equiv (L^left b ps) (L^left a ps).
+Proof.
+ intros H0.
+ lazy beta delta [inclA line_left].
+ intros x H1.
+ apply filter_InA in H1,H0.
+ destruct H1 as [H2 H3].
+ destruct H0 as [H1 H4 ].
+ eapply filter_InA.
+ - repeat intro.
+ now rewrite H0.
+ - split;auto.
+ apply Rltb_true in H3,H4.
+ apply Rltb_true.
+ lra.
+ - repeat intro.
+ now rewrite H3.
+ - repeat intro.
+ now rewrite H3.
+Qed.
+
+Lemma line_right_lt L a ps b:
+ InA equiv b (L^right a ps) ->
+ inclA equiv (L^right b ps) (L^right a ps).
+Proof.
+ intros H0.
+ lazy beta delta [inclA line_right].
+ intros x H1.
+ apply filter_InA in H1,H0.
+ destruct H1 as [H2 H3].
+ destruct H0 as [H1 H4 ].
+ eapply filter_InA.
+ - repeat intro.
+ now rewrite H0.
+ - split;auto.
+ apply Rltb_true in H3,H4.
+ apply Rltb_true.
+ lra.
+ - repeat intro.
+ now rewrite H3.
+ - repeat intro.
+ now rewrite H3.
+Qed.
+
+Lemma line_on_inclA_2 L a ps b:
+ InA equiv b (L^on a ps) ->
+ inclA equiv (L^on b ps) (L^on a ps).
+Proof.
+ intros H0.
+ lazy beta delta [inclA line_on].
+ intros x H1.
+ apply filter_InA in H1,H0.
+ destruct H1 as [H2 H3].
+ destruct H0 as [H1 H4 ].
+ eapply filter_InA.
+ - repeat intro.
+ now rewrite H0.
+ - split;auto.
+ rewrite eqb_true_iff.
+ rewrite eqb_true_iff in H3.
+ transitivity ((L ^P) b);auto.
+ now apply eqb_true_iff.
+ - repeat intro.
+ now rewrite H3.
+ - repeat intro.
+ now rewrite H3.
+Qed.
+
+Lemma line_left_inclA_3 L a ps b:
+ ((L^P) b <= (L^P) a)%R ->
+ inclA equiv (L^left b ps) (L^left a ps).
+Proof.
+ intros H0.
+ lazy beta delta [inclA line_left].
+ intros x H1.
+ apply filter_InA in H1.
+ 2:{ repeat intro.
+ now rewrite H3. }
+ destruct H1 as [H2 H3].
+ eapply filter_InA.
+ { repeat intro.
+ now rewrite H1. }
+ split;auto.
+ apply Rltb_true in H3.
+ apply Rltb_true.
+ lra.
+Qed.
+
+Lemma line_right_inclA_3 L a ps b:
+ ((L^P) a <= (L^P) b)%R ->
+ inclA equiv (L^right b ps) (L^right a ps).
+Proof.
+ intros H0.
+ lazy beta delta [inclA line_right].
+ intros x H1.
+ apply filter_InA in H1.
+ 2:{ repeat intro.
+ now rewrite H3. }
+ destruct H1 as [H2 H3].
+ eapply filter_InA.
+ { repeat intro.
+ now rewrite H1. }
+ split;auto.
+ apply Rltb_true in H3.
+ apply Rltb_true.
+ lra.
+Qed.
+
+Lemma line_on_inclA_3 L a ps b:
+ ((L^P) a == (L^P) b)%R ->
+ inclA equiv (L^on b ps) (L^on a ps).
+Proof.
+ intros H0.
+ lazy beta delta [inclA line_on].
+ intros x H1.
+ apply filter_InA in H1.
+ 2:{ repeat intro.
+ now rewrite H3. }
+ destruct H1 as [H2 H3].
+ eapply filter_InA.
+ { repeat intro.
+ now rewrite H1. }
+ split;auto.
+ rewrite eqb_true_iff.
+ rewrite eqb_true_iff in H3.
+ transitivity ((L ^P) b);auto.
+Qed.
+
+
+Lemma line_right_inclA_4 L a ps b:
+ ((L^P) a < (L^P) b)%R ->
+ inclA equiv (L^on b ps) (L^right a ps).
+Proof.
+ intros H0.
+ lazy beta delta [inclA line_right].
+ intros x H1.
+ apply filter_InA in H1.
+ 2:{ repeat intro.
+ now rewrite H3. }
+ destruct H1 as [H2 H3].
+ eapply filter_InA.
+ { repeat intro.
+ now rewrite H1. }
+ split;auto.
+ apply eqb_true_iff in H3.
+ apply Rltb_true.
+ cbn in H3.
+ lra.
+Qed.
+
+Lemma line_left_inclA_4 L a ps b:
+ ((L^P) b < (L^P) a)%R ->
+ inclA equiv (L^on b ps) (L^left a ps).
+Proof.
+ intros H0.
+ lazy beta delta [inclA line_left].
+ intros x H1.
+ apply filter_InA in H1.
+ 2:{ repeat intro.
+ now rewrite H3. }
+ destruct H1 as [H2 H3].
+ eapply filter_InA.
+ { repeat intro.
+ now rewrite H1. }
+ split;auto.
+ apply eqb_true_iff in H3.
+ apply Rltb_true.
+ cbn in H3.
+ lra.
+Qed.
+
+
+
Lemma line_left_spec L x y ps :
InA equiv y (L^left x ps) <-> (InA equiv y ps /\ (L^P y < L^P x)%R).
Proof. unfold line_left. now rewrite filter_InA, Rltb_true ; [|intros ? ? ->]. Qed.
@@ -820,6 +1019,46 @@ unfold line_right. rewrite line_P_iP_max, (@filter_nilA _ equiv) ; [| autoclass
intros x Hin. rewrite Rltb_false. apply Rle_not_lt. now apply line_bounds.
Qed.
+Lemma bipartition_min: forall L ps,
+ PermutationA equiv ps
+ ((L ^on) (L^-P (L^min ps)) ps ++ (L ^right) (L^-P (L^min ps)) ps).
+Proof.
+ intros L ps.
+ rewrite line_left_on_right_partition with (L:=L) (x:=(L^-P (L ^min ps))) at 1.
+ rewrite line_left_iP_min.
+ reflexivity.
+Qed.
+
+Lemma aggravate_right: forall L ps w w',
+ ((L^P w) < (L^P w'))%R
+ -> L^right w' ps = L^right w' (L^right w ps).
+Proof.
+ symmetry.
+ unfold line_right.
+ rewrite filter_comm.
+ rewrite filter_weakened;auto.
+ intros x H1 H2.
+ rewrite Rltb_true in *|- *.
+ etransitivity;eauto.
+Qed.
+
+Lemma aggravate_on: forall L ps w w',
+ ((L^P w) < (L^P w'))%R
+ -> L^on w' ps = L^on w' (L^right w ps).
+Proof.
+ intros L ps w w' H0.
+ unfold line_on, line_right.
+ rewrite <- filter_andb.
+ apply filter_extensionality_compat;auto.
+ repeat intro.
+ subst y.
+ destruct ((L ^P) w' ==b (L ^P) x) eqn:heq;cbn;auto.
+ symmetry.
+ rewrite eqb_true_iff in heq.
+ rewrite Rltb_true.
+ now rewrite <- heq.
+Qed.
+
Lemma line_on_length_aligned L x ps :
aligned_on L (x :: ps) ->
length (L^on x ps) = countA_occ equiv EQ0 x ps.
diff --git a/CaseStudies/Gathering/InR2/Weber/Weber_point.v b/CaseStudies/Gathering/InR2/Weber/Weber_point.v
index c8c78f6932bdbdfdc643236f1c810bdfca858db3..b28ce7b071b7701902cf82eeb8f006364e122c6c 100644
--- a/CaseStudies/Gathering/InR2/Weber/Weber_point.v
+++ b/CaseStudies/Gathering/InR2/Weber/Weber_point.v
@@ -54,6 +54,9 @@ Require Export Pactole.CaseStudies.Gathering.InR2.Weber.Line.
Set Implicit Arguments.
+Global Arguments inclA_nil [A] {eqA} {_} l _.
+
+
Close Scope R_scope.
Close Scope VectorSpace_scope.
@@ -1757,12 +1760,661 @@ rewrite <-(line_on_length_aligned L _ _ Halign).
f_equiv. rewrite <-Rabs_Ropp. f_equiv. lra.
Qed.
+Lemma line_on_app: forall (L: line) (l l':list R2) x,
+ PermutationA equiv ((L ^on) x (l++l')) (((L ^on) x l) ++ ((L ^on) x l')) .
+Proof.
+ intros L l l' x.
+ unfold line_on.
+ rewrite filter_app.
+ reflexivity.
+Qed.
+Lemma line_on_perm_compat: forall {T : Type} {S0 : Setoid T} {EQ0 : EqDec S0} {VS : RealVectorSpace T}
+ {H : EuclideanSpace T},
+ Proper (equiv ==> equiv ==> PermutationA equiv ==> PermutationA equiv) line_on.
+Proof.
+ repeat intro.
+ unfold line_on.
+ rewrite H2.
+ rewrite (filter_ext (fun y2 : T => (x ^P) x0 ==b (x ^P) y2) (fun y2 : T => (y ^P) y0 ==b (y ^P) y2)).
+ { reflexivity. }
+ intros a.
+ rewrite H1.
+ rewrite H0.
+ reflexivity.
+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.
+
+*)
Lemma weber_aligned_spec L ps w :
+ ps <> nil -> (* Seems necessary *)
line_dir L =/= 0%VS ->
aligned_on L (w :: ps) ->
OnlyWeber ps w <->
- (Rabs (INR (length (L^left w ps)) - INR (length (L^right w ps))) < INR (length (L^on w ps)))%R.
-Proof. Admitted.
+ (Rabs ((^R (L^left w ps)) - (^R (L^right w ps))) < ^R (L^on w ps))%R.
+ (* (Rabs (INR (length (L^left w ps)) - INR (length (L^right w ps))) < INR (length (L^on w ps)))%R. *)
+Proof.
+ intros Hpsnonnil Hlinedir Halign.
+ specialize (weber_aligned_spec_weak Hlinedir Halign) as h_weak.
+ 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. }
+
+ rewrite <- aggravate_right in h.
+ rewrite <- aggravate_on in h.
+ lia.
+
+
+ assert( (Rlength ((L ^left) w' ps)) = (Rlength ((L ^left) w ps)) + (Rlength ((L ^on) w ps))).
+ { rewrite h in h_w.
+
+
+
+ lra. admit. }
+ lra.
+
+ rewrite Rabs_pos_eq.
+ { lra.
+ }
+ assert (abs:w'<>w).
+ { specialize (line_right_spec L w w' ps) as h.
+ rewrite h in H1.
+ intro abs.
+ rewrite abs in H1.
+ 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.