Skip to content
Snippets Groups Projects
Commit dc3672c2 authored by Pierre Courtieu's avatar Pierre Courtieu
Browse files

WIP on last proofs about WB point.

parent d371c464
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
CaseStudies/Gathering/InR2/Weber/Gather_flex_async.v
+ 238
− 161
View file @ dc3672c2
This diff is collapsed.
CaseStudies/Gathering/InR2/Weber/Line.v
+ 239
− 0
View file @ dc3672c2
......@@ -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.
......
CaseStudies/Gathering/InR2/Weber/Weber_point.v
+ 654
− 2
View file @ dc3672c2
This diff is collapsed.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment