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

Merg with master

parents 2c38510a 66d83a75
No related branches found
No related tags found
No related merge requests found
Showing
with 14799 additions and 6 deletions
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
Require Import Pactole.CaseStudies.Gathering.InR2.Weber.Gather_flex_async.
Print Assumptions gather_correct.
This diff is collapsed.
(**************************************************************************)
(** Mechanised Framework for Local Interactions & Distributed Algorithms
T. Balabonski, P. Courtieu, L. Rieg, X. Urbain
PACTOLE project
This file is distributed under the terms of the CeCILL-C licence *)
(**************************************************************************)
(**************************************************************************)
(* Author : Mathis Bouverot-Dupuis (June 2022).
* This file gives some properties of segments in a euclidean space.
* A vector space is not enough to have the decidability of being in a segment. *)
(**************************************************************************)
Require Import Bool.
Require Import Lia Field.
Require Import Rbase Rbasic_fun R_sqrt Rtrigo_def.
Require Import List.
Require Import SetoidList.
Require Import Relations.
Require Import RelationPairs.
Require Import Morphisms.
Require Import Psatz.
Require Import Inverse_Image.
Require Import FunInd.
Require Import FMapFacts.
Require Import SetoidDec.
(* Helping typeclass resolution avoid infinite loops. *)
(* Typeclasses eauto := (bfs). *)
Require Import Pactole.Spaces.EuclideanSpace.
Require Import Pactole.Util.SetoidDefs.
Require Import Pactole.Util.Coqlib.
Require Import Pactole.Util.Ratio.
Require Import Pactole.Util.Bijection.
Require Import Pactole.Spaces.Similarity.
Require Import Pactole.CaseStudies.Gathering.InR2.Weber.Utils.
Section Segment.
Context {T : Type} `{EuclideanSpace T}.
Implicit Types (a b c x y z : T).
(* [segment a b] represents the set of points that are in the segment
* [a, b], endpoints INCLUDED. *)
Definition segment a b : T -> Prop := fun x =>
exists t : R, (0 <= t <= 1)%R /\ (x == t * a + (1 - t) * b)%VS.
Global Instance segment_compat : Proper (equiv ==> equiv ==> equiv ==> iff) segment.
Proof using .
intros ? ? H1 ? ? H2 ? ? H3. unfold segment.
setoid_rewrite H1. setoid_rewrite H2. setoid_rewrite H3. reflexivity.
Qed.
Lemma segment_sym a b x : segment a b x <-> segment b a x.
Proof.
revert a b x.
cut (forall a b x, segment a b x -> segment b a x).
{ intros H1. split ; apply H1. }
intros a b x. unfold segment. intros [t [Ht Hx]].
exists (1 - t)%R. split ; [lra|].
assert (H1 : ((1 - (1 - t)) == t)%R).
{ unfold Rminus. now rewrite Ropp_plus_distr, Ropp_involutive, <-Rplus_assoc, Rplus_opp_r, Rplus_0_l. }
rewrite H1, RealVectorSpace.add_comm. exact Hx.
Qed.
Lemma segment_start a b : segment a b a.
Proof.
unfold segment. exists 1%R. split ; [lra|].
now rewrite mul_1, Rminus_eq_0, mul_0, add_origin_r.
Qed.
Lemma segment_end a b : segment a b b.
Proof.
unfold segment. exists 0%R. split ; [lra|].
now rewrite mul_0, Rminus_0_r, mul_1, add_origin_l.
Qed.
Lemma segment_same a x : segment a a x <-> x == a.
Proof.
split ; [|intros -> ; apply segment_start].
intros [t [Ht Hx]]. revert Hx. unfold Rminus.
now rewrite <-add_morph, mul_1, minus_morph, add_sub.
Qed.
Lemma segment_straight_path a b (r : ratio) : segment a b (straight_path a b r).
Proof.
rewrite segment_sym. unfold segment. exists r. split.
+ apply ratio_bounds.
+ cbn -[equiv RealVectorSpace.add mul opp].
rewrite mul_distr_add, 2 (RealVectorSpace.add_comm (r * b)), RealVectorSpace.add_assoc.
apply add_compat ; auto. unfold Rminus. rewrite <-add_morph, mul_1.
apply add_compat ; auto. now rewrite minus_morph, mul_opp.
Qed.
(* This lemma is the reason why we need a euclidean space (a vector space is not enough). *)
Lemma segment_dec a b x : {segment a b x} + {~segment a b x}.
Proof.
case (a =?= b) as [Hab | Hab].
+ case (x =?= a) as [Hxa | Hxa].
- left. rewrite Hxa, Hab. apply segment_start.
- right. rewrite Hab in *. rewrite segment_same. intuition.
+ assert (H1 : forall t, x == t * b + (1 - t) * a <-> x - a == t * (b - a)).
{
intros t. unfold Rminus. rewrite <-add_morph, mul_1, minus_morph.
rewrite mul_distr_add, mul_opp, (add_comm a), add_assoc.
split ; [intros -> | intros H1].
+ now rewrite <-add_assoc, add_opp, add_origin_r.
+ apply (add_reg_r (-a)). now rewrite <-add_assoc, add_opp, add_origin_r.
}
pose (t := (inner_product (x - a) (b - a) / (inner_product (b - a) (b - a)))%R).
case (x =?= t * b + (1 - t) * a) as [Hx | Hx].
- case (Rle_dec 0%R t) as [Ht0 | Ht0].
* case (Rle_dec t 1%R) as [Ht1 | Ht1].
++left. rewrite segment_sym. exists t. split ; intuition.
++right. rewrite segment_sym. intros [s [Hs Hx']].
rewrite H1 in Hx, Hx'.
assert (Hst : t == s).
{ rewrite Hx' in Hx. apply mul_reg_r in Hx ; auto.
unfold complement. rewrite (sub_origin b a). intuition. }
rewrite <-Hst in Hs. intuition.
* right. rewrite segment_sym. intros [s [Hs Hx']].
rewrite H1 in Hx, Hx'.
assert (Hst : t == s).
{ rewrite Hx' in Hx. apply mul_reg_r in Hx ; auto.
unfold complement. rewrite (sub_origin b a). intuition. }
rewrite <-Hst in Hs. intuition.
- right. rewrite segment_sym. intros [s [Hs Hx']].
assert (Hst : s == t).
{
rewrite H1 in Hx'.
apply inner_product_compat in Hx'. specialize (Hx' (b - a) (b - a) ltac:(auto)).
rewrite inner_product_mul_l in Hx'.
apply (Rmult_eq_compat_r (Rinv (inner_product (b - a) (b - a)))) in Hx'.
rewrite Rmult_assoc, Rinv_r, Rmult_1_r in Hx'.
+ rewrite <-Hx'. reflexivity.
+ rewrite <-squared_norm_product.
rewrite <-Rsqr_0, <-square_norm_equiv ; try lra.
rewrite norm_defined, sub_origin. intuition.
}
rewrite Hst in Hx'. intuition.
Qed.
Definition segment_decb a b x := if segment_dec a b x then true else false.
Lemma segment_decb_true a b x :
segment_decb a b x = true <-> segment a b x.
Proof. unfold segment_decb. case ifP_sumbool ; intuition. Qed.
Lemma segment_decb_false a b x :
segment_decb a b x = false <-> ~segment a b x.
Proof. unfold segment_decb. case ifP_sumbool ; intuition. Qed.
Lemma segment_incl_iff a b a' b' :
(forall x, segment a b x -> segment a' b' x) <-> segment a' b' a /\ segment a' b' b.
Proof.
split.
+ intros Hincl. split ; apply Hincl ; [apply segment_start | apply segment_end].
+ intros [[ta [Hta Ha]] [tb [Htb Hb]]] x [t [Ht Hx]].
exists (t * ta + (1 - t) * tb)%R. split ; [nra|].
rewrite Hx, Ha, Hb. unfold Rminus.
repeat rewrite mul_distr_add. repeat rewrite mul_morph.
assert (Hrewrite : forall x1 x2 x3 x4 : T, x1 + x2 + (x3 + x4) == (x1 + x3) + (x2 + x4)).
{ intros x1 x2 x3 x4. rewrite <-add_assoc, (add_assoc x2).
rewrite (add_comm x2). now repeat rewrite add_assoc. }
rewrite Hrewrite. clear Hrewrite. apply add_compat.
- rewrite add_morph. reflexivity.
- rewrite add_morph. apply mul_compat ; auto ; []. nra.
Qed.
Lemma segment_eq_weak a b a' b' :
(forall x, segment a b x <-> segment a' b' x) -> a == a' \/ a == b'.
Proof.
intros Heq.
assert (Hincl : forall x, segment a b x -> segment a' b' x). { apply Heq. }
assert (Hincl' : forall x, segment a' b' x -> segment a b x). { apply Heq. }
apply segment_incl_iff in Hincl. apply segment_incl_iff in Hincl'.
destruct Hincl as [[ta [Hta Ha]] [tb [Htb Hb]]].
destruct Hincl' as [[ta' [Hta' Ha']] [tb' [Htb' Hb']]].
assert (Ha2 := Ha). rewrite Ha', Hb' in Ha. repeat rewrite mul_distr_add in Ha. repeat rewrite mul_morph in Ha.
assert (Hrewrite : forall x1 x2 x3 x4, x1 + x2 + (x3 + x4) == (x1 + x3) + (x2 + x4)).
{ intros x1 x2 x3 x4. rewrite <-add_assoc, (add_assoc x2).
rewrite (add_comm x2). now repeat rewrite add_assoc. }
rewrite Hrewrite in Ha. clear Hrewrite. rewrite 2 add_morph in Ha.
pose (t := (ta * ta' + (1 - ta) * tb')%R).
assert (Ht1 : (ta * (1 - ta') + (1 - ta) * (1 - tb') = 1 - t)%R).
{ unfold t. nra. }
fold t in Ha. rewrite Ht1 in Ha. apply (add_compat _ _ (reflexivity (-a))) in Ha.
rewrite (add_comm (-a)), add_opp, add_assoc, <-(mul_1 (-a)), mul_opp, <-minus_morph, add_morph in Ha.
unfold Rminus in Ha. rewrite <-(Ropp_involutive t) in Ha at 1.
rewrite <-Ropp_plus_distr, minus_morph, <-mul_opp, <-mul_distr_add, add_comm in Ha.
symmetry in Ha. rewrite mul_eq0_iff, sub_origin in Ha.
case Ha as [Ht | Eab].
+ assert (Ht' : t = 1%R). { cbn in Ht. lra. } clear Ht.
unfold t in Ht'.
case (ta =?= 0%R) as [Hta0 | Hta0].
- right. now rewrite Ha2, Hta0, mul_0, add_origin_l, Rminus_0_r, mul_1.
- case (ta =?= 1%R) as [Hta1 | Hta1].
* left. now rewrite Ha2, Hta1, mul_1, Rminus_eq_0, mul_0, add_origin_r.
* cbn in Hta0, Hta1. assert (Hta0' : ta' = 1%R). { nra. }
left. now rewrite Ha', Hta0', mul_1, Rminus_eq_0, mul_0, add_origin_r.
+ left. setoid_rewrite Eab in Heq. setoid_rewrite segment_same in Heq.
symmetry. rewrite Heq. apply segment_start.
Qed.
Lemma segment_eq_iff a b a' b' :
(forall x, segment a b x <-> segment a' b' x) <-> perm_pairA equiv (a, b) (a', b').
Proof.
split.
+ intros Heq. case (a =?= b) as [Eab | NEab].
- setoid_rewrite Eab in Heq. setoid_rewrite segment_same in Heq.
left. split.
* rewrite Eab. symmetry. rewrite Heq. apply segment_start.
* symmetry. rewrite Heq. apply segment_end.
- destruct (segment_eq_weak _ _ _ _ Heq) as [Haa' | Hab'] ; [left | right].
* split ; [now auto|].
setoid_rewrite segment_sym in Heq.
destruct (segment_eq_weak _ _ _ _ Heq) as [Hbb' | Hba'] ; [auto | exfalso].
apply NEab. now rewrite Haa', Hba'.
* split ; [now auto|].
setoid_rewrite segment_sym in Heq.
destruct (segment_eq_weak _ _ _ _ Heq) as [Hbb' | Hba'] ; [exfalso | auto].
apply NEab. now rewrite Hab', Hbb'.
+ intros [[Ha Hb] | [Ha Hb]] x ; rewrite Ha, Hb ; [|rewrite segment_sym] ; reflexivity.
Qed.
Lemma segment_decb_eq_iff a b x a' b' x' :
segment_decb a b x = segment_decb a' b' x' <->
(segment a b x <-> segment a' b' x').
Proof. unfold segment_decb. case ifP_sumbool ; case ifP_sumbool ; intuition. Qed.
Lemma segment_decb_sym a b x :
segment_decb a b x = segment_decb b a x.
Proof. unfold segment_decb. case ifP_sumbool ; case ifP_sumbool ; rewrite segment_sym ; intuition. Qed.
End Segment.
Section StrictSegment.
Context {T : Type} `{EuclideanSpace T}.
Implicit Types (a b c x y z : T).
(* [strict_segment a b] represents the set of points that are in the segment
* [a, b], endpoints EXCLUDED. *)
Definition strict_segment a b : T -> Prop := fun x =>
segment a b x /\ x =/= a /\ x =/= b.
Global Instance strict_segment_compat : Proper (equiv ==> equiv ==> equiv ==> iff) strict_segment.
Proof using .
intros ? ? H1 ? ? H2 ? ? H3. unfold strict_segment. now rewrite H1, H2, H3.
Qed.
Lemma strict_segment_sym a b x : strict_segment a b x <-> strict_segment b a x.
Proof. unfold strict_segment. rewrite segment_sym. intuition. Qed.
Lemma strict_segment_incl a b x :
strict_segment a b x -> segment a b x.
Proof. unfold strict_segment. intuition. Qed.
Lemma segment_spec_strict a b x :
segment a b x <-> strict_segment a b x \/ x == a \/ x == b.
Proof.
split.
+ case (x =?= a) ; [tauto|]. case (x =?= b) ; [tauto|].
unfold strict_segment. left. intuition.
+ intros [? |[-> | ->]].
- now apply strict_segment_incl.
- now apply segment_start.
- now apply segment_end.
Qed.
Lemma strict_segment_dec a b x :
{strict_segment a b x} + {~strict_segment a b x}.
Proof.
unfold strict_segment.
case (x =?= a) as [Hxa | Hxa] ; [intuition|].
case (x =?= b) as [Hxb | Hxb] ; [intuition|].
case (segment_dec a b x) as [Hseg | Hseg] ; intuition.
Qed.
Definition strict_segment_decb a b x := if strict_segment_dec a b x then true else false.
Lemma strict_segment_decb_eq_iff a b x a' b' x' :
strict_segment_decb a b x = strict_segment_decb a' b' x' <->
(strict_segment a b x <-> strict_segment a' b' x').
Proof. unfold strict_segment_decb. case ifP_sumbool ; case ifP_sumbool ; intuition. Qed.
Lemma strict_segment_decb_sym a b x :
strict_segment_decb a b x = strict_segment_decb b a x.
Proof. unfold strict_segment_decb. case ifP_sumbool ; case ifP_sumbool ; rewrite strict_segment_sym ; intuition. Qed.
Lemma strict_segment_decb_true a b x :
strict_segment_decb a b x = true <-> strict_segment a b x.
Proof. unfold strict_segment_decb. case ifP_sumbool ; intuition. Qed.
Lemma strict_segment_decb_false a b x :
strict_segment_decb a b x = false <-> ~strict_segment a b x.
Proof. unfold strict_segment_decb. case ifP_sumbool ; intuition. Qed.
End StrictSegment.
Require Import Pactole.Spaces.R2.
(* Some results for similarities are only available in R². *)
Section SegmentsInR2.
Local Existing Instances R2_VS R2_ES.
Implicit Types (sim : similarity R2) (a b x : R2).
Lemma R2segment_similarity_weak sim a b x :
segment a b x -> segment (sim a) (sim b) (sim x).
Proof.
intros [t [Ht Hx]]. exists t. split ; auto ; []. rewrite Hx.
rewrite sim_add, 2 sim_mul. repeat rewrite <-add_assoc. f_equiv.
assert (Hrewrite : (1 - (1 - t))%R = t). { lra. }
rewrite Hrewrite. clear Hrewrite.
rewrite add_comm, <-add_assoc. setoid_rewrite <-(add_origin_r ((1 - t) * sim b)%VS) at 2.
f_equiv. unfold Rminus. rewrite <-add_morph, mul_1, minus_morph.
rewrite <-add_assoc, (add_assoc (-sim 0)%VS), (add_comm (-sim 0)%VS).
rewrite add_opp, add_origin_l, add_opp. reflexivity.
Qed.
Lemma R2segment_similarity sim a b x :
segment a b x <-> segment (sim a) (sim b) (sim x).
Proof.
split.
+ now apply R2segment_similarity_weak.
+ intros Hseg. apply (R2segment_similarity_weak (inverse sim)) in Hseg.
cbn in Hseg. repeat rewrite retraction_section in Hseg. exact Hseg.
Qed.
Lemma R2strict_segment_similarity sim a b x :
strict_segment a b x <-> strict_segment (sim a) (sim b) (sim x).
Proof.
unfold strict_segment. rewrite (R2segment_similarity sim).
assert (Hsim : forall x1 x2, x1 =/= x2 <-> sim x1 =/= sim x2).
{ intros x1 x2. cbn. split.
+ intros NEx Esim. apply (f_equal (retraction sim)) in Esim.
rewrite 2 retraction_section in Esim. intuition.
+ intros NEsim Ex. apply NEsim. now f_equal. }
rewrite (Hsim x a), (Hsim x b). reflexivity.
Qed.
End SegmentsInR2.
This diff is collapsed.
This diff is collapsed.
......@@ -20,6 +20,17 @@ Require Import Pactole.Util.Enum.
Set Implicit Arguments.
(* Lemma nth_enum i m d : *)
(* forall Him : i < m, nth i (enum m) d = exist (fun x => x < m) i Him. *)
(* Proof using . *)
(* intros Him. apply eq_proj1, Nat.le_antisymm ; cbn. *)
(* + apply lt_n_Sm_le, firstn_enum_spec. rewrite <-(firstn_skipn (S i)) at 1. *)
(* rewrite app_nth1 ; [apply nth_In|] ; rewrite firstn_length_le ; try rewrite enum_length ; lia. *)
(* + apply skipn_enum_spec. rewrite <-(firstn_skipn i) at 1. *)
(* rewrite app_nth2 ; [apply nth_In|] ; rewrite firstn_length_le by (rewrite enum_length ; lia) ; auto. *)
(* rewrite Nat.sub_diag, skipn_length, enum_length. lia. *)
(* Qed. *)
(** ** Byzantine Robots *)
(** We have finitely many robots. Some are good, others are Byzantine.
......
(**************************************************************************)
(**************************************************************************)
(* Mechanised Framework for Local Interactions & Distributed Algorithms *)
(* C. Auger, P. Courtieu, L. Rieg, X. Urbain , R. Pelle *)
(* PACTOLE project *)
......@@ -175,6 +175,7 @@ Proof using .
* f_equiv.
rewrite Hconfig.
now setoid_rewrite Hpt.
(* subst. do 3 (f_equiv; auto; []). now rewrite Hpt. *)
+ intros config1 config2 Hconfig id1 id2 Hid. simpl in Hid. subst id1.
destruct (Cconfig id2) as [v1 e1 p1 | e1 p1]; cbn -[ratio_0];
now do 3 f_equiv; rewrite Hconfig.
......
......@@ -13,7 +13,7 @@ Require Import Lia.
Require Import SetoidList.
Require Import SetoidDec.
Require Import Pactole.Util.FMaps.FMapList.
Require Import Pactole.Util.MMultiset.MMultisetWMap.
Require Pactole.Util.MMultiset.MMultisetWMap.
Require Export Pactole.Util.MMultiset.MMultisetInterface.
Require Export Pactole.Util.MMultiset.MMultisetFacts.
Require Export Pactole.Util.MMultiset.MMultisetExtraOps.
......@@ -33,9 +33,8 @@ Context {loc : Type}.
Context `{EqDec loc}.
Existing Instance multiplicity_compat.
Existing Instance FMOps_WMap.
Existing Instance MakeFMultisetsFacts.
Existing Instance MMultisetWMap.FMOps_WMap.
Existing Instance MMultisetWMap.MakeFMultisetsFacts.
(** ** Building multisets from lists **)
......
......@@ -4,7 +4,7 @@ Require Import Pactole.Models.ContinuousGraph.
Require Import Pactole.Models.Rigid.
Require Import Pactole.Models.RigidFlexibleEquivalence_Assumptions.
Require Import Pactole.Models.DiscreteGraph.
Require Import Pactole.Models.GraphEquivalence.
(*Require Import Pactole.Models.GraphEquivalence.*)
Require Import Pactole.Models.Flexible.
Require Import Pactole.Models.Similarity.
Require Import Pactole.Spaces.Isomorphism.
......
This diff is collapsed.
Paper/img/contraction_lemma.drawio.png

18 KiB

Paper/img/measure_decrease_not_on_A.drawio.png

4.62 KiB

Paper/img/measure_decrease_not_on_B.drawio.png

4.49 KiB

Paper/img/measure_decrease_on_A.drawio.png

3.06 KiB

Paper/img/measure_decrease_on_B.drawio.png

3.17 KiB

Paper/img/phase_transition_diagram.drawio.png

22.8 KiB

0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment