Skip to content
Snippets Groups Projects
Commit 3204ac5a authored by Sébastien Bouchard's avatar Sébastien Bouchard
Browse files

RingSpec seems required + some lemmas and simplifications

parent 707fed38
No related branches found
No related tags found
No related merge requests found
......@@ -8,7 +8,7 @@
(**************************************************************************)
Require Import Utf8 Arith SetoidList.
From Pactole Require Import Util.Stream Util.Fin Models.NoByzantine
From Pactole Require Import Util.Stream Models.NoByzantine
Models.RingSSync CaseStudies.Exploration.ExplorationDefs.
Set Implicit Arguments.
......@@ -17,11 +17,10 @@ Typeclasses eauto := (bfs).
Section Exploration.
(** Given an abitrary ring *)
Variable n : nat.
Context {RR : RingSpec}.
(** There are kG good robots and no byzantine ones. *)
Variable k : nat.
Instance Robots : Names := Robots (S k) 0.
Instance Loc : Location := @Loc n.
(** Assumptions on the number of robots: it strictly divides the ring size. *)
Hypothesis kdn : (S (S (S n)) mod (S k) = 0).
......@@ -86,8 +85,8 @@ Qed.
(** Translating [ref_config] by multiples of [S (S (S n)) / (S k)]
does not change its observation. *)
Lemma obs_trans_ref_config : forall g,
!! (map_config (Ring.trans (create_ref_config g)) ref_config) == !! ref_config.
Lemma obs_asbf_ref_config : forall g,
!! (map_config (asbf (create_ref_config g)⁻¹) ref_config) == !! ref_config.
Proof using kdn.
unfold obs_from_config, MultisetObservation.multiset_observation,
MultisetObservation.make_multiset. intro g. f_equiv.
......@@ -104,22 +103,22 @@ Proof using kdn.
split; intros [id [Hpt _]]; revert Hpt; apply (no_byz id); clear id; intros g' Hpt.
+ pose (id' := subf g' g). change (fin (S k)) with G in id'.
exists (Good id'). split. 2:{ rewrite InA_Leibniz. apply In_names. }
rewrite <- Hpt. cbn-[trans create_ref_config]. split. 2: reflexivity.
rewrite <- Hpt. cbn-[subf create_ref_config]. split. 2: reflexivity.
unfold create_ref_config, Datatypes.id, id'. apply fin2nat_inj.
cbn-[subm subf Nat.div Nat.modulo]. rewrite subm_mod, subf2nat, subm2nat,
mod2fin2nat, Nat.add_mod_idemp_l, 2 (Nat.mod_small (_ * _)).
rewrite local_subproof1 at 3 5. rewrite <- Nat.mul_sub_distr_r,
<- Nat.mul_add_distr_r, Nat.mul_mod_distr_r, Nat.mul_cancel_r.
reflexivity. 2,6: apply Nat.neq_succ_0. 1,2: apply local_subproof2.
all: apply local_subproof3. apply fin_lt. apply mod2fin_lt.
rewrite 2 subf2nat, 3 mod2fin2nat, Nat.add_mod_idemp_l,
2 (Nat.mod_small (_ * _)). rewrite local_subproof1 at 3 5.
rewrite <- Nat.mul_sub_distr_r, <- Nat.mul_add_distr_r,
Nat.mul_mod_distr_r. reflexivity. 1,5: apply Nat.neq_succ_0.
apply local_subproof2. all: apply local_subproof3. apply fin_lt.
apply mod2fin_lt.
+ pose (id' := addf g' g). change (fin (S k)) with G in id'.
exists (Good id'). split. 2:{ rewrite InA_Leibniz. apply In_names. }
rewrite <- Hpt. cbn-[subm addf Nat.modulo Nat.div]. split. 2: reflexivity.
unfold create_ref_config, id'. apply fin2nat_inj. rewrite subm_mod,
subm2nat, 2 mod2fin2nat, Nat.add_mod_idemp_l, 2 (Nat.mod_small (_ * _)).
rewrite <- Hpt. cbn. split. 2: reflexivity. unfold create_ref_config, id'.
apply fin2nat_inj. rewrite subf2nat, 3 mod2fin2nat, addf2nat,
Nat.add_mod_idemp_l, 2 (Nat.mod_small (_ * _)).
rewrite local_subproof1 at 2 4. rewrite <- Nat.mul_sub_distr_r,
<- Nat.mul_add_distr_r, Nat.mul_mod_distr_r. apply Nat.mul_cancel_r.
all: cycle 1. rewrite addf2nat, Nat.add_mod_idemp_l, <- Nat.add_assoc,
all: cycle 1. rewrite Nat.add_mod_idemp_l, <- Nat.add_assoc,
le_plus_minus_r, <- Nat.add_mod_idemp_r, Nat.mod_same, Nat.add_0_r.
apply Nat.mod_small. 4: apply Nat.lt_le_incl.
2,3,5,6,10: apply Nat.neq_succ_0. 3,6: apply local_subproof2.
......@@ -150,7 +149,7 @@ Proof using . coinduction Hcoind. apply FSYNC_one. Qed.
(** As all robots see the same observation, we take for instance the one at location [origin]. *)
Definition move := pgm r (!! ref_config).
Definition target := @move_along n fin0 move.
Definition target := move_along fin0 move.
(** Acceptable starting configurations contain no tower,
that is, all robots are at different locations. *)
......@@ -172,9 +171,8 @@ Hypothesis Hmove : move == SelfLoop.
Lemma round_id : round r da ref_config == ref_config.
Proof using Hmove kdn.
rewrite FSYNC_round_simplify; try (now split); []. apply no_byz_eq. intro g.
cbn-[trans equiv map_config Nat.modulo Nat.div create_ref_config].
erewrite obs_from_config_ignore_snd, obs_trans_ref_config, Hmove,
move_along_0. apply Bijection.retraction_section.
cbn-[BijectionInverse equiv]. erewrite obs_from_config_ignore_snd,
obs_asbf_ref_config, Hmove, move_along_0. apply Bijection.retraction_section.
Qed.
Lemma NeverVisited_ref_config : e, e == execute r bad_demon ref_config
......@@ -213,7 +211,7 @@ End NoMove.
(** *** Equality of configurations up to translation **)
(** Translating a configuration. *)
Definition f_config config m : configuration := map_config ((trans m)⁻¹) config.
Definition f_config config m : configuration := map_config (asbm m) config.
Instance f_config_compat : Proper (equiv ==> equiv ==> equiv) f_config.
Proof using .
......@@ -255,12 +253,11 @@ Lemma f_config_modulo : ∀ config m,
f_config config (m mod (S (S (S n)))) == f_config config m.
Proof using . intros * id. apply addm_mod. Qed.
Lemma trans_f_config : (config : configuration) (id1 id2 : ident) (m : nat),
trans (fin2nat (config id1)) (config id2)
== trans (f_config config m id1) (f_config config m id2).
Lemma asbf_f_config : (config : configuration) (id1 id2 : ident) (m : nat),
asbf (config id1)⁻¹ (config id2)
== asbf (f_config config m id1)⁻¹ (f_config config m id2).
Proof using .
intros. unfold f_config. cbn-[addm subm equiv]. rewrite 2 subm_subf,
2 mod2finK, 2addm_addf, <- subfA, addfVKV. reflexivity.
intros. unfold f_config. cbn-[equiv]. symmetry. apply subf_addm_addm.
Qed.
(** Two configurations are equivalent if they are equal up to a global translation. *)
......@@ -314,12 +311,12 @@ Qed.
hence the same answer from the robogram. *)
Lemma config1_obs_equiv : config1 config2, equiv_config config1 config2
-> g, !! (map_config (trans (config1 (Good g))) config1)
== !! (map_config (trans (config2 (Good g))) config2).
-> g, !! (map_config (asbf (config1 (Good g))⁻¹) config1)
== !! (map_config (asbf (config2 (Good g))⁻¹) config2).
Proof using k_inf_n kdn.
intros config1 config2 [offset Hequiv] g. f_equiv.
unfold equiv_config_m in Hequiv. rewrite Hequiv.
intros id. cbn[map_config]. apply trans_f_config.
intros id. cbn[map_config]. apply asbf_f_config.
Qed.
Theorem equiv_config_m_round : m config1 config2,
......@@ -328,12 +325,12 @@ Theorem equiv_config_m_round : ∀ m config1 config2,
Proof using k_inf_n kdn.
unfold equiv_config_m. intros * Hequiv. unfold f_config.
rewrite 2 (FSYNC_round_simplify r _ FSYNC_one). intros id. apply (no_byz id).
clear id. intro g. cbn-[trans equiv Bijection.BijectionInverse].
setoid_rewrite <- config1_obs_equiv. 2,3: reflexivity. rewrite Hequiv,
2 move_along_trans. unfold f_config, map_config. cbn-[addm subm move_along].
rewrite 2 submVKV, addm_move_along. apply move_along_compat. reflexivity.
apply (pgm_compat r), obs_from_config_compat. 2: reflexivity. intros id.
rewrite 2 addm_addf, 2 subm_subf, 2 mod2finK, <- subfA, addfVKV. reflexivity.
clear id. intro g. cbn-[equiv BijectionInverse].
setoid_rewrite <- config1_obs_equiv. 2,3: reflexivity. rewrite Hequiv.
cbn-[f_config equiv]. rewrite <- 2 subf_move_along'.
unfold f_config, map_config. cbn. rewrite 2 subfVKV, addm_move_along.
apply move_along_compat. reflexivity. apply (pgm_compat r),
obs_from_config_compat. 2: reflexivity. intros id. apply subf_addm_addm.
Qed.
Corollary equiv_config_round : config1 config2, equiv_config config1 config2
......@@ -454,10 +451,9 @@ Hypothesis Hmove : move =/= SelfLoop.
Lemma round_simplify : round r da ref_config == f_config ref_config target.
Proof using k_inf_n kdn.
rewrite (FSYNC_round_simplify _ _ FSYNC_one). apply no_byz_eq. intro g.
cbn-[trans equiv ref_config Nat.modulo]. rewrite obs_from_config_ignore_snd,
move_along_trans, (proj1 (Bijection.Inversion _ _ _)) by reflexivity.
setoid_rewrite obs_trans_ref_config. cbn-[Nat.modulo].
symmetry. apply addm_mod.
cbn-[BijectionInverse mod2fin equiv]. rewrite obs_from_config_ignore_snd,
obs_asbf_ref_config. cbn-[mod2fin equiv]. unfold target. rewrite subff,
2 move_along0_, addfC, addm_addf, mod2finK. reflexivity.
Qed.
Corollary round_ref_config :
......
......@@ -28,11 +28,10 @@ Typeclasses eauto := (bfs).
Section Tower.
(** Given an abitrary ring *)
Variable n : nat.
Context {RR : RingSpec}.
(** There are S k good robots and no byzantine ones. *)
Variable k : nat.
Instance Robots : Names := Robots (S k) 0.
Instance Loc : Location := @Loc n.
(** Assumptions on the number of robots: it is non zero and strictly divides the ring size. *)
Hypothesis kdn : (S (S (S n)) mod (S k) = 0).
......
......@@ -608,7 +608,7 @@ Definition da_with_all_activated da := {|
choose_inactive_compat := da.(choose_inactive_compat) |}.
Lemma da_with_all_activated_FSYNC_da : forall da, FSYNC_da (da_with_all_activated da).
Proof. now intros da id. Qed.
Proof using . now intros da id. Qed.
(** An unfair demon activates at least one activable robot if such a robot exists. *)
Definition unfair_da r da config :=
......
Require Import Utf8.
From Pactole Require Export Setting Spaces.Ring Spaces.Isomorphism
From Pactole Require Export Setting Util.Fin Util.Bijection Spaces.Ring
Observations.MultisetObservation.
Set Implicit Arguments.
Section RingSSync.
Context {n : nat} {Robots : Names}.
Context {RR : RingSpec} {Robots : Names}.
Instance Loc : Location := make_Location (@ring_node n).
Global Instance Loc : Location := make_Location ring_node.
Global Instance St : State location := OnlyLocation (fun _ => True).
......@@ -20,17 +20,17 @@ Global Instance RC : robot_choice direction :=
(** Demon's frame choice:
we move back the robot to the origin with a translation
and we can choose the orientation of the ring. *)
Global Instance FC : frame_choice (nat * bool) := {
Global Instance FC : frame_choice (location * bool) := {
frame_choice_bijection :=
λ nb, if snd nb then comp (trans (fst nb)) (sym (fst nb))
else trans (fst nb);
λ nb, if snd nb then comp (asbf (fst nb)⁻¹) (symbf (fst nb))
else asbf (fst nb)⁻¹;
frame_choice_Setoid := eq_setoid _ }.
Global Existing Instance NoChoice.
Global Existing Instance NoChoiceIna.
Global Existing Instance NoChoiceInaFun.
Global Instance UpdFun : update_function direction (nat * bool) unit := {
Global Instance UpdFun : update_function direction (location * bool) unit := {
update := λ config g _ dir _, move_along (config (Good g)) dir;
update_compat := ltac:(repeat intro; subst; now apply move_along_compat) }.
......
......@@ -12,9 +12,14 @@ Require Import Utf8 Lia Psatz SetoidDec Rbase.
From Pactole Require Import Util.Coqlib Util.Bijection Spaces.Graph
Spaces.Isomorphism Models.NoByzantine Util.Fin.
(** ** A ring **)
(** What we need to define a ring. *)
Class RingSpec := { n : nat }.
Section Ring.
Context {n : nat}.
Context {RR : RingSpec}.
Definition ring_node := finite_node (S (S (S n))).
Inductive direction := Forward | Backward | SelfLoop.
......@@ -184,10 +189,10 @@ Proof using .
Qed.
Lemma subf_move_along' : (v1 v2 : ring_node) (d : direction),
subf (move_along v1 d) v2 = addm (subf v1 v2) (dir2nat d).
subf (move_along v1 d) v2 = move_along (subf v1 v2) d.
Proof using .
intros. rewrite <- oppf_subf, subf_move_along, oppf_subm, subfA, addfC,
<- addf_subf, addm_addf. reflexivity.
<- addf_subf, addf_addm, dir2mod2fin. reflexivity.
Qed.
(* returns the ''opposite'' direction *)
......@@ -253,7 +258,7 @@ Lemma move_along_dir2nat_diff : ∀ (v1 v2 : ring_node) (d : direction),
Proof using .
intros. split; intros H.
- rewrite move_alongE, H, diffE, addm_addf, mod2finK. apply subfVK.
- subst. rewrite diffE, subf_move_along', subff, addm_addf, add0f.
- subst. rewrite diffE, subf_move_along', subff, move_along0_.
symmetry. apply dir2mod2fin.
Qed.
......
......@@ -558,6 +558,14 @@ Proof using .
intros. rewrite 3 subfE, <- addfA, oppf_addf, subfE. reflexivity.
Qed.
Lemma subf_addf_addf : f1 f2 f3 : fin (S n),
subf (addf f1 f3) (addf f2 f3) = subf f1 f2.
Proof using . intros. rewrite <- subfA, addfVKV. reflexivity. Qed.
Lemma subf_addm_addm : (f1 f2 : fin (S n)) (m : nat),
subf (addm f1 m) (addm f2 m) = subf f1 f2.
Proof using . intros. rewrite 2 addm_addf. apply subf_addf_addf. Qed.
Lemma subm_comp : (f : fin (S n)) (m2 m1 : nat),
subm (subm f m1) m2 = subm f (m1 + m2).
Proof using .
......
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