diff --git a/CaseStudies/Exploration/ImpossibilityKDividesN.v b/CaseStudies/Exploration/ImpossibilityKDividesN.v
index f1f0459012f9e4bca3d29b77e27936813c3b963e..91351b25a2a5c36aa044454b9b4229c8613984eb 100644
--- a/CaseStudies/Exploration/ImpossibilityKDividesN.v
+++ b/CaseStudies/Exploration/ImpossibilityKDividesN.v
@@ -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 :
diff --git a/CaseStudies/Exploration/Tower.v b/CaseStudies/Exploration/Tower.v
index 4106e6ffd94ea0bc4348126b7a5182ad4d2197d8..e1c1639f3600d98c62e23a200005f131bb5bf693 100644
--- a/CaseStudies/Exploration/Tower.v
+++ b/CaseStudies/Exploration/Tower.v
@@ -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).
diff --git a/Core/Formalism.v b/Core/Formalism.v
index 0fd593ce5a81f9c277bcc8b72be6eefdd5eadc32..1575dcb9855dfeea76c51c0170583f3adbe308f8 100644
--- a/Core/Formalism.v
+++ b/Core/Formalism.v
@@ -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 :=
diff --git a/Models/RingSSync.v b/Models/RingSSync.v
index b382c0279d47fa659d830ba262c752c636d31187..1b4f6c01399d25cfc7971a80a0cd729a09c3faf2 100644
--- a/Models/RingSSync.v
+++ b/Models/RingSSync.v
@@ -1,14 +1,14 @@
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) }.
diff --git a/Spaces/Ring.v b/Spaces/Ring.v
index 46d346f432c478736007f2ffe63916d5c77c1132..47c9e0add06b25f994f4f98f1df17e9de6f02fa1 100644
--- a/Spaces/Ring.v
+++ b/Spaces/Ring.v
@@ -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.
diff --git a/Util/Fin.v b/Util/Fin.v
index 3b57f1f4b8a7f7eccf9888742958763edf41a672..920a71f8e664cee4db246e48b4e03e773743967f 100644
--- a/Util/Fin.v
+++ b/Util/Fin.v
@@ -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 .