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

Fix of other proofs about Weber point.

parent 0631003b
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
CaseStudies/Gathering/InR2/Weber/Align_flex_async.v
+ 86
− 11
View file @ 466d47b2
...@@ -39,7 +39,7 @@ Require Import FunInd. ...@@ -39,7 +39,7 @@ Require Import FunInd.
Require Import FMapFacts. Require Import FMapFacts.
(* Helping typeclass resolution avoid infinite loops. *) (* Helping typeclass resolution avoid infinite loops. *)
Typeclasses eauto := (bfs). (* Typeclasses eauto := (bfs). *)
(* Pactole basic definitions *) (* Pactole basic definitions *)
Require Export Pactole.Setting. Require Export Pactole.Setting.
...@@ -62,6 +62,7 @@ Require Import Pactole.CaseStudies.Gathering.InR2.Weber.Weber_point. ...@@ -62,6 +62,7 @@ Require Import Pactole.CaseStudies.Gathering.InR2.Weber.Weber_point.
(* User defined *) (* User defined *)
Import Permutation. Import Permutation.
Import Datatypes. Import Datatypes.
Import ListNotations.
Set Implicit Arguments. Set Implicit Arguments.
...@@ -70,7 +71,7 @@ Close Scope VectorSpace_scope. ...@@ -70,7 +71,7 @@ Close Scope VectorSpace_scope.
Section Alignment. Section Alignment.
Local Existing Instances dist_sum_compat. Local Existing Instances dist_sum_compat R2_VS R2_ES.
(* We assume the existence of a function that calculates a weber point of a collection (* We assume the existence of a function that calculates a weber point of a collection
* (even when the weber point is not unique). * (even when the weber point is not unique).
...@@ -328,10 +329,17 @@ Proof using . ...@@ -328,10 +329,17 @@ Proof using .
intros H. destruct f as [f Pf]. intros H. destruct f as [f Pf].
change (lift (existT precondition f Pf) (config id)) with (map_config (lift (existT precondition f Pf)) config id). change (lift (existT precondition f Pf) (config id)) with (map_config (lift (existT precondition f Pf)) config id).
rewrite multi_support_config. unfold pos_list. rewrite config_list_map, map_map. rewrite multi_support_config. unfold pos_list. rewrite config_list_map, map_map.
+ apply eqlistA_PermutationA. f_equiv. intros [[s d] r] [[s' d'] r'] Hsdr. inv Hsdr. apply eqlistA_PermutationA. (* f_equiv. *)
cbn -[equiv straight_path]. destruct Pf as [sim Hsim]. rewrite <-Hsim. apply straight_path_similarity. apply (@map_extensionalityA_compat _ _ equiv equiv _).
+ intros [[s d] r] [[s' d'] r'] [[Hs Hd] Hr]. cbn -[equiv] in H, Hs, Hd, Hr |- *. - intros [[s d] r] [[s' d'] r'] Hsdr.
repeat split ; cbn -[equiv] ; auto. inversion Hsdr.
cbn in H0,H1.
destruct H0.
rewrite <- Subset.subset_eq in H1.
subst.
cbn -[equiv straight_path]. destruct Pf as [sim Hsim]. rewrite <-Hsim.
apply straight_path_similarity.
- reflexivity.
Qed. Qed.
Lemma lift_update_swap da config1 config2 g target : Lemma lift_update_swap da config1 config2 g target :
...@@ -456,7 +464,7 @@ split ; intros H1 id ; specialize (H1 id) ; specialize (H id) ; ...@@ -456,7 +464,7 @@ split ; intros H1 id ; specialize (H1 id) ; specialize (H id) ;
+ left. now rewrite Hs, Hd. + left. now rewrite Hs, Hd.
+ right. now rewrite Hd, Hp. + right. now rewrite Hd, Hp.
Qed. Qed.
Lemma config_stay_impl_config_stg config : Lemma config_stay_impl_config_stg config :
config_stay config -> forall p, config_stay_or_go config p. config_stay config -> forall p, config_stay_or_go config p.
Proof using . Proof using .
...@@ -464,8 +472,63 @@ unfold config_stay, config_stay_or_go. intros Hstay p i. specialize (Hstay i). ...@@ -464,8 +472,63 @@ unfold config_stay, config_stay_or_go. intros Hstay p i. specialize (Hstay i).
destruct (config i) as [[start dest] _]. now left. destruct (config i) as [[start dest] _]. now left.
Qed. Qed.
(* Typeclasses eauto := (bfs). *)
(* 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')) <->
exists id, (x == c id /\ x' == c' id)%VS.
Proof using lt_0n.
pose (id0 :=(Fin.Fin lt_0n)).
pose (g0 :=(Good id0)).
pose (default :=(c g0)).
pose (default' :=(c' g0)).
split.
+ intros Hin.
specialize @config_list_InA_combine_same_lgth2 with (1:=Hin)(dfA:=default)(dfB:=default') as h.
destruct h as [i [Hn [Hx Hx']]].
rewrite config_list_spec in Hx,Hx'.
unfold default in Hx,Hx'.
unfold default' in Hx'.
rewrite map_nth in Hx .
rewrite map_nth in Hx' .
exists (nth i names g0);auto.
+ intros [[g|b] [Hx Hx']] ; [|byz_exfalso].
rewrite Hx,Hx'.
rewrite config_list_spec.
rewrite config_list_spec.
rewrite combine_map.
apply InA_alt.
exists (c (Good g),c' (Good g)).
split;auto.
apply in_map_iff.
exists (Good g,Good g);split;auto.
apply in_combine_id;split;auto.
unfold names.
apply in_app_iff.
left.
apply in_map_iff.
exists g;split;auto.
apply In_Gnames.
Qed.
Lemma config_list_In_combine x x' c c' :
List.In (x, x') (combine (config_list c) (config_list c')) <->
exists id, x == c id /\ x' == c' id.
Proof using lt_0n.
rewrite <- In_InA_is_leibniz with (eqA:=equiv).
- apply config_list_InA_combine.
- intros x0 y.
cbn.
split;[ intros [[[h0 h1] h2] [[h3 h4] h5]]| intro h].
+ destruct x0 as [[[u1 u2] t] [[v1 v2] w]]; destruct y as [[[u1' u2'] t'] [[v1' v2'] w']];cbn in *.
rewrite <- Subset.subset_eq in h2, h5.
subst;auto.
+ now subst.
Qed.
(* This would have been much more pleasant to do with mathcomp's tuples. *) (* This would have been much more pleasant to do with mathcomp's tuples. *)
Lemma config_list_InA_combine x x' c c' : (*Lemma config_list_InA_combine x x' c c' :
InA equiv (x, x') (combine (config_list c) (config_list c')) <-> InA equiv (x, x') (combine (config_list c) (config_list c')) <->
exists id, x == c id /\ x' == c' id. exists id, x == c id /\ x' == c' id.
Proof using lt_0n. Proof using lt_0n.
...@@ -502,7 +565,7 @@ split. ...@@ -502,7 +565,7 @@ split.
rewrite H. apply nth_InA ; autoclass. rewrite combine_length. repeat rewrite config_list_length. rewrite H. apply nth_InA ; autoclass. rewrite combine_length. repeat rewrite config_list_length.
rewrite Nat.min_id. cbn. destruct g. cbn. lia. rewrite Nat.min_id. cbn. destruct g. cbn. lia.
Qed. Qed.
*)
Lemma pos_list_InA_combine x x' c c' : Lemma pos_list_InA_combine x x' c c' :
InA equiv (x, x') (combine (pos_list c) (pos_list c')) <-> InA equiv (x, x') (combine (pos_list c) (pos_list c')) <->
exists id, x == get_location (c id) /\ x' == get_location (c' id). exists id, x == get_location (c id) /\ x' == get_location (c' id).
...@@ -532,11 +595,13 @@ unfold pos_list. rewrite (@InA_map_iff _ _ equiv equiv) ; autoclass. ...@@ -532,11 +595,13 @@ unfold pos_list. rewrite (@InA_map_iff _ _ equiv equiv) ; autoclass.
+ foldR2. apply get_location_compat. + foldR2. apply get_location_compat.
Qed. Qed.
Typeclasses eauto := (bfs).
(* A technical lemma used to prove the fact that the configuration always (* A technical lemma used to prove the fact that the configuration always
* contracts towards the weber point. *) * contracts towards the weber point. *)
Lemma segment_progress a b r1 r2 : Lemma segment_progress a b r1 r2 :
segment b (straight_path a b r1) (straight_path a b (add_ratio r1 r2)). segment b (straight_path a b r1) (straight_path a b (add_ratio r1 r2)).
Proof using . Proof using .
Typeclasses eauto := (dfs).
assert (Hr1 := ratio_bounds r1). assert (Hr1 := ratio_bounds r1).
assert (Hr2 := ratio_bounds r2). assert (Hr2 := ratio_bounds r2).
unfold add_ratio. case (Rle_dec R1 (r1 + r2)) as [Hle | HNle]. unfold add_ratio. case (Rle_dec R1 (r1 + r2)) as [Hle | HNle].
...@@ -692,7 +757,9 @@ Definition is_looping (robot : info) : bool := ...@@ -692,7 +757,9 @@ Definition is_looping (robot : info) : bool :=
if get_start robot =?= get_destination robot then true else false. if get_start robot =?= get_destination robot then true else false.
Local Instance is_looping_compat : Proper (equiv ==> eq) is_looping. Local Instance is_looping_compat : Proper (equiv ==> eq) is_looping.
Proof using . intros [[? ?] ?] [[? ?] ?] [[H1 H2] _]. cbn -[equiv] in *. now rewrite H1, H2. Qed. Proof using . intros [[? ?] ?] [[? ?] ?] [[H1 H2] _]. cbn -[equiv] in *.
cbn in H1,H2.
now rewrite H1, H2. Qed.
Lemma is_looping_ratio start dest r1 r2 : Lemma is_looping_ratio start dest r1 r2 :
is_looping (start, dest, r1) = is_looping (start, dest, r2). is_looping (start, dest, r1) = is_looping (start, dest, r2).
...@@ -977,6 +1044,7 @@ Lemma Rplus_le_compat3_3 x y z x' y' z' eps : ...@@ -977,6 +1044,7 @@ Lemma Rplus_le_compat3_3 x y z x' y' z' eps :
(x <= x')%R -> (y <= y')%R -> (z <= z' - eps)%R -> (x + y + z <= x' + y' + z' - eps)%R. (x <= x')%R -> (y <= y')%R -> (z <= z' - eps)%R -> (x + y + z <= x' + y' + z' - eps)%R.
Proof using . lra. Qed. Proof using . lra. Qed.
Typeclasses eauto := (dfs) 5.
(* If a robot that is not [looping on the weber point] is activated, (* If a robot that is not [looping on the weber point] is activated,
* the measure strictly decreases. *) * the measure strictly decreases. *)
Lemma round_decreases_measure_strong config da w : Lemma round_decreases_measure_strong config da w :
...@@ -1017,7 +1085,10 @@ case (Sumbool.sumbool_of_bool (is_looping (config id))) as [Hloop | HNloop]. ...@@ -1017,7 +1085,10 @@ case (Sumbool.sumbool_of_bool (is_looping (config id))) as [Hloop | HNloop].
destruct (config id) as [[s d] ri]. revert HNon Hloop. unfold is_on, is_looping. destruct (config id) as [[s d] ri]. revert HNon Hloop. unfold is_on, is_looping.
case ifP_sumbool ; case ifP_sumbool ; try discriminate. case ifP_sumbool ; case ifP_sumbool ; try discriminate.
cbn -[equiv straight_path]. intros ->. now rewrite straight_path_same. cbn -[equiv straight_path]. intros ->. now rewrite straight_path_same.
++intros [? ?] [? ?] [H1 H2]. unfold f. rewrite H1, H2. reflexivity. ++intros [? ?] [? ?] [H1 H2]. unfold f.
cbn -[equiv] in H1,H2.
foldR2.
rewrite H1, H2. reflexivity.
++intros [? ?] [? ?]. split ; auto. ++intros [? ?] [? ?]. split ; auto.
+ unfold is_looping in HNloop. destruct (config id) as [[s d] r] eqn:Econfig. simpl in HNloop. + unfold is_looping in HNloop. destruct (config id) as [[s d] r] eqn:Econfig. simpl in HNloop.
case (s =?= d) as [Hsd | Hsd] ; [exfalso ; revert HNloop ; destruct_match ; intuition |]. case (s =?= d) as [Hsd | Hsd] ; [exfalso ; revert HNloop ; destruct_match ; intuition |].
...@@ -1072,9 +1143,12 @@ Inductive FirstActivNLW w : demon -> configuration -> Prop := ...@@ -1072,9 +1143,12 @@ Inductive FirstActivNLW w : demon -> configuration -> Prop :=
FirstActivNLW w (Stream.tl d) (round gatherW (Stream.hd d) config) -> FirstActivNLW w (Stream.tl d) (round gatherW (Stream.hd d) config) ->
FirstActivNLW w d config. FirstActivNLW w d config.
Typeclasses eauto := (bfs).
Lemma gathered_aligned ps x : Lemma gathered_aligned ps x :
Forall (fun y => y == x) ps -> aligned ps. Forall (fun y => y == x) ps -> aligned ps.
Proof using. Proof using.
Typeclasses eauto := (dfs) 7.
rewrite Forall_forall. intros Hgathered. rewrite Forall_forall. intros Hgathered.
exists (Build_line x 0%VS). intros y Hin. unfold line_contains. exists (Build_line x 0%VS). intros y Hin. unfold line_contains.
rewrite line_proj_spec, line_proj_inv_spec. cbn -[equiv RealVectorSpace.add opp mul inner_product]. rewrite line_proj_spec, line_proj_inv_spec. cbn -[equiv RealVectorSpace.add opp mul inner_product].
...@@ -1147,6 +1221,7 @@ Qed. ...@@ -1147,6 +1221,7 @@ Qed.
Definition lt_config eps c c' := Definition lt_config eps c c' :=
(0 <= measure c <= measure c' - eps)%R. (0 <= measure c <= measure c' - eps)%R.
Typeclasses eauto := (dfs) 5.
Local Instance lt_config_compat : Proper (equiv ==> equiv ==> equiv ==> iff) lt_config. Local Instance lt_config_compat : Proper (equiv ==> equiv ==> equiv ==> iff) lt_config.
Proof using . intros e e' He c1 c1' Hc1 c2 c2' Hc2. unfold lt_config. now rewrite He, Hc1, Hc2. Qed. Proof using . intros e e' He c1 c1' Hc1 c2 c2' Hc2. unfold lt_config. now rewrite He, Hc1, Hc2. Qed.
......
CaseStudies/Gathering/InR2/Weber/Align_flex_ssync.v
+ 61
− 31
View file @ 466d47b2
...@@ -39,7 +39,7 @@ Require Import FunInd. ...@@ -39,7 +39,7 @@ Require Import FunInd.
Require Import FMapFacts. Require Import FMapFacts.
(* Helping typeclass resolution avoid infinite loops. *) (* Helping typeclass resolution avoid infinite loops. *)
Typeclasses eauto := (bfs). (* Typeclasses eauto := (bfs). *)
(* Pactole basic definitions *) (* Pactole basic definitions *)
Require Export Pactole.Setting. Require Export Pactole.Setting.
...@@ -60,6 +60,7 @@ Require Import Pactole.CaseStudies.Gathering.InR2.Weber.Weber_point. ...@@ -60,6 +60,7 @@ Require Import Pactole.CaseStudies.Gathering.InR2.Weber.Weber_point.
(* User defined *) (* User defined *)
Import Permutation. Import Permutation.
Import Datatypes. Import Datatypes.
Import ListNotations.
Set Implicit Arguments. Set Implicit Arguments.
...@@ -68,7 +69,7 @@ Close Scope VectorSpace_scope. ...@@ -68,7 +69,7 @@ Close Scope VectorSpace_scope.
Section Alignment. Section Alignment.
Local Existing Instances dist_sum_compat. Local Existing Instances dist_sum_compat R2_VS R2_ES.
(* We assume the existence of a function that calculates a weber point of a collection (* We assume the existence of a function that calculates a weber point of a collection
* (even when the weber point is not unique). * (even when the weber point is not unique).
...@@ -225,6 +226,7 @@ pattern s. apply MMultisetFacts.ind. ...@@ -225,6 +226,7 @@ pattern s. apply MMultisetFacts.ind.
Qed. Qed.
(* This is the main result about multi_support. *) (* This is the main result about multi_support. *)
Typeclasses eauto := (bfs).
Lemma multi_support_config config id : Lemma multi_support_config config id :
PermutationA equiv PermutationA equiv
(multi_support (obs_from_config config (config id))) (multi_support (obs_from_config config (config id)))
...@@ -241,6 +243,7 @@ Corollary multi_support_map f config id : ...@@ -241,6 +243,7 @@ Corollary multi_support_map f config id :
(multi_support (obs_from_config (map_config (lift f) config) (lift f (config id)))) (multi_support (obs_from_config (map_config (lift f) config) (lift f (config id))))
(List.map (projT1 f) (config_list config)). (List.map (projT1 f) (config_list config)).
Proof using . Proof using .
Typeclasses eauto := (dfs).
intros H. destruct f as [f Pf]. cbn -[equiv config_list multi_support]. intros H. destruct f as [f Pf]. cbn -[equiv config_list multi_support].
change (f (config id)) with (map_config f config id). change (f (config id)) with (map_config f config id).
now rewrite multi_support_config, config_list_map. now rewrite multi_support_config, config_list_map.
...@@ -375,39 +378,55 @@ cofix Hind. intros config d Hsim Halign. constructor. ...@@ -375,39 +378,55 @@ cofix Hind. intros config d Hsim Halign. constructor.
Qed. Qed.
(* This would have been much more pleasant to do with mathcomp's tuples. *) (* 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')) <->
exists id, (x == c id /\ x' == c' id)%VS.
Proof using lt_0n.
pose (id0 :=(Fin.Fin lt_0n)).
pose (g0 :=(Good id0)).
pose (default :=(c g0)).
pose (default' :=(c' g0)).
split.
+ intros Hin.
specialize @config_list_InA_combine_same_lgth2 with (1:=Hin)(dfA:=default)(dfB:=default') as h.
destruct h as [i [Hn [Hx Hx']]].
rewrite config_list_spec in Hx,Hx'.
unfold default in Hx,Hx'.
unfold default' in Hx'.
rewrite map_nth in Hx .
rewrite map_nth in Hx' .
exists (nth i names g0);auto.
+ intros [[g|b] [Hx Hx']] ; [|byz_exfalso].
rewrite Hx,Hx'.
rewrite config_list_spec.
rewrite config_list_spec.
rewrite combine_map.
apply InA_alt.
exists (c (Good g),c' (Good g)).
split;auto.
apply in_map_iff.
exists (Good g,Good g);split;auto.
apply in_combine_id;split;auto.
unfold names.
apply in_app_iff.
left.
apply in_map_iff.
exists g;split;auto.
apply In_Gnames.
Qed.
Lemma config_list_In_combine x x' c c' : Lemma config_list_In_combine x x' c c' :
List.In (x, x') (combine (config_list c) (config_list c')) <-> List.In (x, x') (combine (config_list c) (config_list c')) <->
exists id, x == c id /\ x' == c' id. exists id, x == c id /\ x' == c' id.
Proof using lt_0n. Proof using lt_0n.
assert (g0 : G). rewrite <- In_InA_is_leibniz with (eqA:=equiv).
{ change G with (fin n). apply (exist _ 0). lia. } - apply config_list_InA_combine.
split. - cbn.
+ intros Hin. apply (@In_nth (location * location) _ _ (c (Good g0), c' (Good g0))) in Hin. split;[ intros [h1 h2]| intro h].
destruct Hin as [i [Hi Hi']]. + destruct x0; destruct y;cbn in *;subst;auto.
rewrite combine_nth in Hi' by now repeat rewrite config_list_length. inv Hi'. + now subst.
assert (i < n) as Hin.
{
eapply Nat.lt_le_trans ; [exact Hi|]. rewrite combine_length.
repeat rewrite config_list_length. rewrite Nat.min_id. cbn. lia.
}
pose (g := exist (fun x => x < n) i Hin).
change (fin n) with G in *. exists (Good g) ;
split ; rewrite config_list_spec, map_nth ; f_equiv ; unfold names ;
rewrite app_nth1, map_nth by (now rewrite map_length, Gnames_length) ;
f_equiv ; cbn ; change G with (fin n) ; apply nth_enum.
+ intros [[g|b] [Hx Hx']].
- assert ((x, x') = nth (proj1_sig g) (combine (config_list c) (config_list c')) (c (Good g0), c' (Good g0))) as H.
{
rewrite combine_nth by now repeat rewrite config_list_length.
destruct g as [g Hg].
repeat rewrite config_list_spec, map_nth. rewrite Hx, Hx'. unfold names.
repeat rewrite app_nth1, map_nth by now rewrite map_length, Gnames_length.
repeat f_equal ; cbn ; change G with (fin n) ; erewrite nth_enum ; reflexivity.
}
rewrite H. apply nth_In. rewrite combine_length. repeat rewrite config_list_length.
rewrite Nat.min_id. cbn. destruct g. cbn. lia.
- exfalso. assert (Hbyz := In_Bnames b). apply list_in_length_n0 in Hbyz. rewrite Bnames_length in Hbyz. auto.
Qed. Qed.
(* This measure counts how many robots aren't on the weber point. *) (* This measure counts how many robots aren't on the weber point. *)
...@@ -587,9 +606,11 @@ destruct (round gatherW da config i =?= weber_calc (config_list config)) as [Hre ...@@ -587,9 +606,11 @@ destruct (round gatherW da config i =?= weber_calc (config_list config)) as [Hre
* exfalso. apply Hi. rewrite Hround. destruct_match ; intuition. * exfalso. apply Hi. rewrite Hround. destruct_match ; intuition.
Qed. Qed.
Typeclasses eauto := (bfs).
Lemma gathered_aligned ps x : Lemma gathered_aligned ps x :
(Forall (fun y => y == x) ps) -> aligned ps. (Forall (fun y => y == x) ps) -> aligned ps.
Proof using . Proof using .
Typeclasses eauto := (dfs).
rewrite Forall_forall. intros Hgathered. rewrite Forall_forall. intros Hgathered.
exists (Build_line x 0%VS). intros y Hin. unfold line_contains. exists (Build_line x 0%VS). intros y Hin. unfold line_contains.
rewrite line_proj_spec, line_proj_inv_spec. cbn -[equiv RealVectorSpace.add opp mul inner_product]. rewrite line_proj_spec, line_proj_inv_spec. cbn -[equiv RealVectorSpace.add opp mul inner_product].
...@@ -666,7 +687,16 @@ Definition lt_config eps c c' := ...@@ -666,7 +687,16 @@ Definition lt_config eps c c' :=
(0 <= measure c <= measure c' - eps)%R. (0 <= measure c <= measure c' - eps)%R.
Local Instance lt_config_compat : Proper (equiv ==> equiv ==> equiv ==> iff) lt_config. Local Instance lt_config_compat : Proper (equiv ==> equiv ==> equiv ==> iff) lt_config.
Proof using . intros e e' He c1 c1' Hc1 c2 c2' Hc2. unfold lt_config. now rewrite He, Hc1, Hc2. Qed. Proof using .
intros ? ? H1 ? ? H2 ? ? H3.
unfold lt_config.
rewrite H1.
rewrite H2 at 1.
rewrite H3 at 1.
rewrite H2.
reflexivity.
Qed.
(* We proove this using the well-foundedness of lt on nat. *) (* We proove this using the well-foundedness of lt on nat. *)
Lemma lt_config_wf eps : (eps > 0)%R -> well_founded (lt_config eps). Lemma lt_config_wf eps : (eps > 0)%R -> well_founded (lt_config eps).
......
CaseStudies/Gathering/InR2/Weber/Align_rigid_ssync.v
+ 86
− 35
View file @ 466d47b2
...@@ -37,9 +37,9 @@ Require Import Psatz. ...@@ -37,9 +37,9 @@ Require Import Psatz.
Require Import Inverse_Image. Require Import Inverse_Image.
Require Import FunInd. Require Import FunInd.
Require Import FMapFacts. Require Import FMapFacts.
Require Import Pactole.Util.ListComplements.
(* Helping typeclass resolution avoid infinite loops. *) (* Helping typeclass resolution avoid infinite loops. *)
Typeclasses eauto := (bfs). (* Typeclasses eauto := (bfs). *)
(* Pactole basic definitions *) (* Pactole basic definitions *)
Require Export Pactole.Setting. Require Export Pactole.Setting.
...@@ -61,6 +61,7 @@ Require Import Pactole.CaseStudies.Gathering.InR2.Weber.Weber_point. ...@@ -61,6 +61,7 @@ Require Import Pactole.CaseStudies.Gathering.InR2.Weber.Weber_point.
(* User defined *) (* User defined *)
Import Permutation. Import Permutation.
Import Datatypes. Import Datatypes.
Import ListNotations.
Set Implicit Arguments. Set Implicit Arguments.
Close Scope R_scope. Close Scope R_scope.
...@@ -69,6 +70,7 @@ Close Scope VectorSpace_scope. ...@@ -69,6 +70,7 @@ Close Scope VectorSpace_scope.
Section Alignment. Section Alignment.
Local Existing Instances dist_sum_compat R2_VS R2_ES.
(* We assume the existence of a function that calculates a weber point of a collection (* We assume the existence of a function that calculates a weber point of a collection
* (even when the weber point is not unique). * (even when the weber point is not unique).
...@@ -86,12 +88,43 @@ Local Existing Instance weber_calc_compat. ...@@ -86,12 +88,43 @@ Local Existing Instance weber_calc_compat.
Variables n : nat. Variables n : nat.
Hypothesis lt_0n : 0 < n. Hypothesis lt_0n : 0 < n.
(* There are no byzantine robots. *) (* There are no byzantine robots. *)
Local Instance N : Names := Robots n 0. Local Instance N : Names := Robots n 0.
Local Instance NoByz : NoByzantine. Local Instance NoByz : NoByzantine.
Proof using . now split. Qed. Proof using . now split. Qed.
Lemma list_in_length_n0 {A : Type} x (l : list A) : List.In x l -> length l <> 0.
Proof using . intros Hin. induction l as [|y l IH] ; cbn ; auto. Qed.
Lemma byz_impl_false : B -> False.
Proof using .
intros b. assert (Hbyz := In_Bnames b).
apply list_in_length_n0 in Hbyz.
rewrite Bnames_length in Hbyz.
cbn in Hbyz. intuition.
Qed.
(* Use this tactic to solve any goal
* provided there is a byzantine robot as a hypothesis. *)
Ltac byz_exfalso :=
match goal with
| b : ?B |- _ => exfalso ; apply (byz_impl_false b)
end.
(* Since all robots are good robots, we can define a function
* from identifiers to good identifiers. *)
Definition unpack_good (id : ident) : G :=
match id with
| Good g => g
| Byz _ => ltac:(byz_exfalso)
end.
Lemma good_unpack_good id : Good (unpack_good id) == id.
Proof using . unfold unpack_good. destruct_match ; [auto | byz_exfalso]. Qed.
Lemma unpack_good_good g : unpack_good (Good g) = g.
Proof using . reflexivity. Qed.
(* The robots are in the plane (R^2). *) (* The robots are in the plane (R^2). *)
Local Instance Loc : Location := make_Location R2. Local Instance Loc : Location := make_Location R2.
Local Instance LocVS : RealVectorSpace location := R2_VS. Local Instance LocVS : RealVectorSpace location := R2_VS.
...@@ -189,6 +222,7 @@ pattern s. apply MMultisetFacts.ind. ...@@ -189,6 +222,7 @@ pattern s. apply MMultisetFacts.ind.
+ now reflexivity. + now reflexivity.
Qed. Qed.
Typeclasses eauto := (bfs).
(* This is the main result about multi_support. *) (* This is the main result about multi_support. *)
Lemma multi_support_config config id : Lemma multi_support_config config id :
PermutationA equiv PermutationA equiv
...@@ -208,6 +242,7 @@ Corollary multi_support_map f config id : ...@@ -208,6 +242,7 @@ Corollary multi_support_map f config id :
Proof using . Proof using .
intros H. destruct f as [f Pf]. cbn -[equiv config_list multi_support]. intros H. destruct f as [f Pf]. cbn -[equiv config_list multi_support].
change (f (config id)) with (map_config f config id). change (f (config id)) with (map_config f config id).
Typeclasses eauto := (dfs).
now rewrite multi_support_config, config_list_map. now rewrite multi_support_config, config_list_map.
Qed. Qed.
...@@ -281,42 +316,54 @@ Qed. ...@@ -281,42 +316,54 @@ Qed.
Lemma sub_lt_sub (i j k : nat) : j < i <= k -> k - i < k - j. Lemma sub_lt_sub (i j k : nat) : j < i <= k -> k - i < k - j.
Proof using lt_0n. lia. Qed. Proof using lt_0n. lia. Qed.
Lemma list_in_length_n0 {A : Type} x (l : list A) : List.In x l -> length l <> 0.
Proof using . intros Hin. induction l as [|y l IH] ; cbn ; auto. Qed.
(* This would have been much more pleasant to do with mathcomp's tuples. *) (* 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')) <->
exists id, (x == c id /\ x' == c' id)%VS.
Proof using lt_0n.
pose (id0 :=(Fin.Fin lt_0n)).
pose (g0 :=(Good id0)).
pose (default :=(c g0)).
pose (default' :=(c' g0)).
split.
+ intros Hin.
specialize @config_list_InA_combine_same_lgth2 with (1:=Hin)(dfA:=default)(dfB:=default') as h.
destruct h as [i [Hn [Hx Hx']]].
rewrite config_list_spec in Hx,Hx'.
unfold default in Hx,Hx'.
unfold default' in Hx'.
rewrite map_nth in Hx .
rewrite map_nth in Hx' .
exists (nth i names g0);auto.
+ intros [[g|b] [Hx Hx']] ; [|byz_exfalso].
rewrite Hx,Hx'.
rewrite config_list_spec.
rewrite config_list_spec.
rewrite combine_map.
apply InA_alt.
exists (c (Good g),c' (Good g)).
split;auto.
apply in_map_iff.
exists (Good g,Good g);split;auto.
apply in_combine_id;split;auto.
unfold names.
apply in_app_iff.
left.
apply in_map_iff.
exists g;split;auto.
apply In_Gnames.
Qed.
Lemma config_list_In_combine x x' c c' : Lemma config_list_In_combine x x' c c' :
List.In (x, x') (combine (config_list c) (config_list c')) <-> List.In (x, x') (combine (config_list c) (config_list c')) <->
exists id, x == c id /\ x' == c' id. exists id, x == c id /\ x' == c' id.
Proof using lt_0n. Proof using lt_0n.
assert (g0 : G). rewrite <- In_InA_is_leibniz with (eqA:=equiv).
{ change G with (fin n). apply (exist _ 0). lia. } - apply config_list_InA_combine.
split. - cbn.
+ intros Hin. apply (@In_nth (location * location) _ _ (c (Good g0), c' (Good g0))) in Hin. split;[ intros [h1 h2]| intro h].
destruct Hin as [i [Hi Hi']]. + destruct x0; destruct y;cbn in *;subst;auto.
rewrite combine_nth in Hi' by now repeat rewrite config_list_length. inv Hi'. + now subst.
assert (i < n) as Hin.
{
eapply Nat.lt_le_trans ; [exact Hi|]. rewrite combine_length.
repeat rewrite config_list_length. rewrite Nat.min_id. cbn. lia.
}
pose (g := exist (fun x => x < n) i Hin).
change (fin n) with G in *. exists (Good g) ;
split ; rewrite config_list_spec, map_nth ; f_equiv ; unfold names ;
rewrite app_nth1, map_nth by (now rewrite map_length, Gnames_length) ;
f_equiv ; cbn ; change G with (fin n) ; apply nth_enum.
+ intros [[g|b] [Hx Hx']].
- assert ((x, x') = nth (proj1_sig g) (combine (config_list c) (config_list c')) (c (Good g0), c' (Good g0))) as H.
{
rewrite combine_nth by now repeat rewrite config_list_length.
destruct g as [g Hg].
repeat rewrite config_list_spec, map_nth. rewrite Hx, Hx'. unfold names.
repeat rewrite app_nth1, map_nth by now rewrite map_length, Gnames_length.
repeat f_equal ; cbn ; change G with (fin n) ; erewrite nth_enum ; reflexivity.
}
rewrite H. apply nth_In. rewrite combine_length. repeat rewrite config_list_length.
rewrite Nat.min_id. cbn. destruct g. cbn. lia.
- exfalso. assert (Hbyz := In_Bnames b). apply list_in_length_n0 in Hbyz. rewrite Bnames_length in Hbyz. auto.
Qed. Qed.
(* This measure strictly decreases whenever a robot moves. *) (* This measure strictly decreases whenever a robot moves. *)
...@@ -338,7 +385,8 @@ Lemma round_preserves_weber config da w : ...@@ -338,7 +385,8 @@ Lemma round_preserves_weber config da w :
Proof using lt_0n. Proof using lt_0n.
intros Hsim Hweb. apply weber_contract with (config_list config) ; auto. intros Hsim Hweb. apply weber_contract with (config_list config) ; auto.
unfold contract. rewrite Forall2_Forall, Forall_forall by now repeat rewrite config_list_length. unfold contract. rewrite Forall2_Forall, Forall_forall by now repeat rewrite config_list_length.
intros [x x']. rewrite config_list_In_combine. intros [x x'].
rewrite config_list_In_combine.
intros [id [Hx Hx']]. revert Hx'. rewrite round_simplify by auto. intros [id [Hx Hx']]. revert Hx'. rewrite round_simplify by auto.
repeat destruct_match ; intros Hx' ; rewrite Hx, Hx' ; try apply segment_end. repeat destruct_match ; intros Hx' ; rewrite Hx, Hx' ; try apply segment_end.
assert (w == weber_calc (config_list config)) as Hw. assert (w == weber_calc (config_list config)) as Hw.
...@@ -375,9 +423,12 @@ unfold measure. apply sub_lt_sub. split. ...@@ -375,9 +423,12 @@ unfold measure. apply sub_lt_sub. split.
rewrite config_list_length. cbn ; lia. rewrite config_list_length. cbn ; lia.
Qed. Qed.
Typeclasses eauto := (bfs).
Lemma gathered_aligned ps x : Lemma gathered_aligned ps x :
(Forall (fun y => y == x) ps) -> aligned ps. (Forall (fun y => y == x) ps) -> aligned ps.
Proof using . Proof using .
Typeclasses eauto := (dfs).
rewrite Forall_forall. intros Hgathered. rewrite Forall_forall. intros Hgathered.
exists (Build_line x 0%VS). intros y Hin. unfold line_contains. exists (Build_line x 0%VS). intros y Hin. unfold line_contains.
rewrite line_proj_spec, line_proj_inv_spec. cbn -[equiv RealVectorSpace.add opp mul inner_product]. rewrite line_proj_spec, line_proj_inv_spec. cbn -[equiv RealVectorSpace.add opp mul inner_product].
......
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