From d9f00379cf7b5ac5dc5bfbbd3dbd03f200017430 Mon Sep 17 00:00:00 2001
From: Lionel Rieg <lionel.rieg@univ-grenoble-alpes.fr>
Date: Wed, 12 May 2021 00:04:58 +0200
Subject: [PATCH] New model file NoByzantine.v

---
 CaseStudies/Convergence/Algorithm_noB.v       | 11 ++-----
 .../Exploration/ImpossibilityKDividesN.v      | 28 ++++++----------
 CaseStudies/Exploration/Tower.v               | 27 +++++-----------
 CaseStudies/Gathering/Impossibility.v         | 18 ++++-------
 CaseStudies/Gathering/InR/Algorithm.v         | 21 ++++--------
 CaseStudies/Gathering/InR/Impossibility.v     | 19 +++++------
 CaseStudies/Gathering/InR2/Algorithm.v        | 17 +++-------
 .../Gathering/InR2/FSyncFlexNoMultAlgorithm.v | 18 +++--------
 CaseStudies/Gathering/InR2/Peleg.v            | 17 +++-------
 CaseStudies/Gathering/InR2/Viglietta.v        | 14 +++-----
 Models/NoByzantine.v                          | 32 +++++++++++++++++++
 _CoqProject                                   |  1 +
 12 files changed, 95 insertions(+), 128 deletions(-)
 create mode 100644 Models/NoByzantine.v

diff --git a/CaseStudies/Convergence/Algorithm_noB.v b/CaseStudies/Convergence/Algorithm_noB.v
index e7fc035d..d814c44f 100644
--- a/CaseStudies/Convergence/Algorithm_noB.v
+++ b/CaseStudies/Convergence/Algorithm_noB.v
@@ -28,6 +28,7 @@ Require Import Pactole.Setting.
 Require Import Pactole.Spaces.R2.
 Require Import Pactole.Observations.SetObservation.
 Require Import Pactole.Models.Rigid.
+Require Import Pactole.Models.NoByzantine.
 Require Import Pactole.Models.Similarity.
 Set Implicit Arguments.
 Close Scope R_scope.
@@ -43,6 +44,8 @@ Variable n : nat.
 Hypothesis n_non_0 : n <> 0%nat.
 
 Instance MyRobots : Names := Robots n 0.
+Instance NoByz : NoByzantine.
+Proof. now split. Qed.
 
 (* BUG?: To help finding correct instances, loops otherwise! *)
 Instance Loc : Location := {| location := R2 |}.
@@ -99,14 +102,6 @@ Qed.
 
 Hint Resolve obs_non_empty : core.
 
-(** There is no byzantine robot so to prove anything about an ident
-    we just need to consider good robots.*)
-Lemma no_byz : forall P, (forall g, P (Good g)) -> forall id, P id.
-Proof using n_non_0.
-intros P Hg [g | b].
-+ apply Hg.
-+ destruct b. lia.
-Qed.
 
 (** ** Properties of executions  *)
 
diff --git a/CaseStudies/Exploration/ImpossibilityKDividesN.v b/CaseStudies/Exploration/ImpossibilityKDividesN.v
index fb692954..90400cc2 100644
--- a/CaseStudies/Exploration/ImpossibilityKDividesN.v
+++ b/CaseStudies/Exploration/ImpossibilityKDividesN.v
@@ -15,6 +15,7 @@ Require Import Lia.
 Require Import Decidable.
 Require Import Equalities.
 Require Import List Setoid SetoidList Compare_dec Morphisms.
+Require Import Pactole.Models.NoByzantine.
 Require Import Pactole.CaseStudies.Exploration.Definitions.
 
 
@@ -33,32 +34,23 @@ Instance Robots : Names := Robots kG 0.
 
 (** Assumptions on the number of robots: it is non zero, less than and divides the ring size. *)
 Hypothesis kdn : (ring_size mod kG = 0)%nat.
-(* This version triggers an "out of memory" error in the Program Definition of [da]!
+(* (* FIXME: This version triggers an "out of memory" error in the Program Definition of [da]! *)
 Hypothesis k_bounds : (1 < kG < ring_size)%nat.
 Definition k_sup_1 : (1 < kG)%nat := proj1 k_bounds.
 Definition k_inf_n : (kG < ring_size)%nat := proj2 k_bounds. *)
 Hypothesis k_sup_1 : (1 < kG)%nat.
 Hypothesis k_inf_n : (kG < ring_size)%nat.
 
-(** There is no byzantine robot so we can simplify properties
-    about identifiers and configurations. *)
-Lemma no_byz : forall (id : ident) P, (forall g, P (Good g)) -> P id.
-Proof using k_inf_n k_sup_1 kdn.
-intros [g | b] P HP.
-+ apply HP.
-+ destruct b. lia.
-Qed.
+
+Instance NoByz : NoByzantine.
+Proof using . now split. Qed.
 
 (** A dummy state used for (inexistant) byzantine robots. *)
 Definition origin : location := of_Z 0.
-Definition dummy_val : location := origin. (* could be anything *)
+Definition dummy_loc : location := origin. (* could be anything *)
 
 Notation "!! config" := (obs_from_config config origin) (at level 0).
 
-Lemma no_byz_eq : forall config1 config2 : configuration,
-  (forall g, config1 (Good g) == config2 (Good g)) -> config1 == config2.
-Proof using k_inf_n k_sup_1 kdn. intros config1 config2 Heq id. apply (no_byz id). intro g. apply Heq. Qed.
-
 
 (** Let us consider an arbirary robogram. *)
 Variable r : robogram.
@@ -80,12 +72,12 @@ Definition create_ref_config (g : G) : location :=
 Definition ref_config : configuration :=
   fun id => match id with
               | Good g => create_ref_config g
-              | Byz b => dummy_val
+              | Byz b => dummy_loc
             end.
 
 Lemma ref_config_injective :
   Util.Preliminary.injective eq equiv (fun id => get_location (ref_config id)).
-Proof using k_inf_n k_sup_1 kdn.
+Proof using k_sup_1 k_inf_n kdn.
 intros id1 id2.
 assert (ring_size / kG <> 0)%nat by (rewrite Nat.div_small_iff; lia).
 apply (no_byz id2), (no_byz id1). clear id1 id2.
@@ -106,7 +98,7 @@ Qed.
 (**  Translating [ref_config] by multiples of [ring_size / kG] does not change its observation. *)
 Lemma obs_trans_ref_config : forall g,
   !! (map_config (Ring.trans (to_Z (create_ref_config g))) ref_config) == !! ref_config.
-Proof using k_inf_n k_sup_1 kdn.
+Proof using k_sup_1 k_inf_n kdn.
 unfold obs_from_config,
        MultisetObservation.multiset_observation, MultisetObservation.make_multiset.
 intro g. apply MMultisetFacts.from_elements_compat. (* FIXME: [f_equiv] works but is too long *)
@@ -170,7 +162,7 @@ Qed.
 (** The demon activate all robots and shifts their view to be on 0. *)
 Program Definition da : demonic_action := {|
   activate := fun id => true;
-  relocate_byz := fun _ _ => dummy_val;
+  relocate_byz := fun _ _ => dummy_loc;
   change_frame := fun config g => (to_Z (config (Good g)), false);
   choose_update := fun _ _ _ => tt;
   choose_inactive := fun _ _ => tt |}.
diff --git a/CaseStudies/Exploration/Tower.v b/CaseStudies/Exploration/Tower.v
index 332c2446..fc378f5f 100644
--- a/CaseStudies/Exploration/Tower.v
+++ b/CaseStudies/Exploration/Tower.v
@@ -23,6 +23,7 @@ Require Import Decidable.
 Require Import Setoid Equalities Morphisms.
 Require Import Compare_dec FinFun.
 Require Import ZArith Arith_base Arith.Div2 Lia Psatz.
+Require Import Pactole.Models.NoByzantine.
 Require Import Pactole.CaseStudies.Exploration.Definitions.
 
 
@@ -41,28 +42,16 @@ Instance Robots : Names := Robots kG 0.
 (** Assumptions on the number of robots: it is non zero and strictly divides the ring size. *)
 Hypothesis kdn : (ring_size mod kG = 0)%nat.
 Hypothesis k_inf_n : (kG < ring_size)%nat.
-(*Hypothesis k_sup_1 : (1 < kG)%nat.*)
 
-(** There is no byzantine robot so we can simplify properties about identifiers and configurations. *)
-(* TODO: put properties with no byz into a file Models/NoByzantine.v *)
-Lemma no_byz : forall (id : ident) P, (forall g, P (Good g)) -> P id.
-Proof using k_inf_n (*k_sup_1*) kdn.
-intros [g | b] P HP.
-+ apply HP.
-+ destruct b. lia.
-Qed.
+(** There is no byzantine robot. *)
+Instance NoByz : NoByzantine.
+Proof using . now split. Qed.
 
-(** A dummy state used for (inexistant) byzantine robots. *)
 Definition origin : location := of_Z 0.
-Definition dummy_val : location := origin. (* could be anything *)
 
 Notation "!! config" := (@obs_from_config _ _ _ _ multiset_observation config origin) (at level 0).
 Notation execute := (execute (UpdFun := UpdFun)).
 
-Lemma no_byz_eq : forall config1 config2 : configuration,
-  (forall g, config1 (Good g) == config2 (Good g)) -> config1 == config2.
-Proof using k_inf_n (*k_sup_1*) kdn. intros config1 config2 Heq id. apply (no_byz id). intro g. apply Heq. Qed.
-
 (** In order to prove that at least one position is occupied, we define the list of positions. *)
 Definition Vlist := Identifiers.enum ring_size.
 
@@ -74,7 +63,7 @@ Proof using . apply enum_length. Qed.
 
 (** As there is strictly less robots than location, there is an empty location. *)
 Lemma ConfigExistsEmpty : forall config, ¬ (∀ pt, In pt (!! config)).
-Proof using k_inf_n (*k_sup_1*) kdn.
+Proof using k_inf_n kdn.
 generalize k_inf_n; intros Hkin config Hall.
 assert (Hsize : size (!! config) < ring_size).
 { apply le_lt_trans with (cardinal (!! config)).
@@ -114,7 +103,7 @@ Theorem no_stop_on_starting_config : forall r d config,
   Explore_and_Stop r ->
   Valid_starting_config config ->
   ~Stopped (execute r d config).
-Proof using k_inf_n (*k_sup_1*) kdn.
+Proof using k_inf_n kdn.
 intros r d config.
 generalize (@reflexivity execution equiv _ (execute r d config)).
 generalize (execute r d config) at -2.
@@ -145,7 +134,7 @@ Lemma tower_on_final_config : forall r d config,
   Explore_and_Stop r ->
   Stopped (execute r d config) ->
   exists loc, ((!! config)[loc] > 1)%nat.
-Proof using k_inf_n (*k_sup_1*) kdn.
+Proof using k_inf_n kdn.
 intros r d config Hfair Hsol Hstop.
 assert (Hequiv := @no_stop_on_starting_config r d config Hfair Hsol).
 assert (Hvalid : ~Valid_starting_config config) by tauto.
@@ -197,7 +186,7 @@ Lemma no_exploration_k_inf_2 : forall r d config,
   Explore_and_Stop r ->
   Valid_starting_config config ->
   (kG > 1)%nat.
-Proof using k_inf_n (*k_sup_1*) kdn.
+Proof using k_inf_n kdn.
 intros r d config Hfair Hsol Hvalid.
 assert (Hexr := exec_stopped r).
 assert (Htower := tower_on_final_config).
diff --git a/CaseStudies/Gathering/Impossibility.v b/CaseStudies/Gathering/Impossibility.v
index eab81935..d1a8d363 100644
--- a/CaseStudies/Gathering/Impossibility.v
+++ b/CaseStudies/Gathering/Impossibility.v
@@ -30,6 +30,7 @@ Require Import Pactole.CaseStudies.Gathering.Definitions.
 Require Pactole.CaseStudies.Gathering.WithMultiplicity.
 Import Pactole.Observations.MultisetObservation.
 Require Import Pactole.Models.Rigid.
+Require Import Pactole.Models.NoByzantine.
 Set Implicit Arguments.
 Close Scope R_scope.
 Close Scope VectorSpace_scope.
@@ -45,6 +46,8 @@ Section ImpossibilityProof.
 (** There are n good robots and no byzantine ones. *)
 Variable n : nat.
 Instance MyRobots : Names := Robots n 0.
+Instance NoByz : NoByzantine.
+Proof using . now split. Qed.
 
 (** We assume that the number of robots is even and non-null. *)
 Hypothesis even_nG : Nat.Even n.
@@ -100,6 +103,10 @@ Instance Frame : frame_choice (similarity location) := FrameChoiceSimilarity.
 Implicit Type config : configuration.
 Implicit Type da : demonic_action.
 
+Lemma no_byz_eq : forall config1 config2 : configuration,
+  (forall g, get_location (config1 (Good g)) == get_location (config2 (Good g))) ->
+  config1 == config2.
+Proof using . intros. apply no_byz_eq. intro. now apply WithMultiplicity.no_info. Qed.
 
 Lemma nG_ge_2 : 2 <= nG.
 Proof using even_nG nG_non_0.
@@ -122,17 +129,6 @@ Definition obs_from_config_spec : forall config (pt : location),
   (!! config)[pt] = countA_occ _ equiv_dec pt (List.map get_location (config_list config))
   := WithMultiplicity.obs_from_config_spec.
 
-Lemma no_byz : forall (id : ident) P, (forall g, P (Good g)) -> P id.
-Proof using nG_non_0.
-intros [g | b] P HP.
-+ apply HP.
-+ destruct b. lia.
-Qed.
-
-Lemma no_byz_eq : forall config1 config2,
-  (forall g, get_location (config1 (Good g)) == get_location (config2 (Good g))) -> config1 == config2.
-Proof using nG_non_0. intros config1 config2 Heq id. apply (no_byz id), Heq. Qed.
-
 Definition mk_info : location -> location := id.
 Arguments mk_info _%VectorSpace_scope.
 Lemma mk_info_get_location : forall pt, get_location (mk_info pt) == pt.
diff --git a/CaseStudies/Gathering/InR/Algorithm.v b/CaseStudies/Gathering/InR/Algorithm.v
index a715536b..96b5f0f1 100644
--- a/CaseStudies/Gathering/InR/Algorithm.v
+++ b/CaseStudies/Gathering/InR/Algorithm.v
@@ -40,6 +40,8 @@ Require Import Pactole.Observations.MultisetObservation.
 Require Import Pactole.Models.Similarity.
 (* Specific to rigidity *)
 Require Export Pactole.Models.Rigid.
+(* Specific to settings without Byzantine robots *)
+Require Export Pactole.Models.NoByzantine.
 
 (* User defined *)
 Import Permutation.
@@ -59,6 +61,8 @@ Variable n : nat.
 Hypothesis size_G : n >= 2.
 (** We assume that we have at least two good robots and no byzantine one. *)
 Instance MyRobots : Names := Robots n 0.
+Instance NoByz : NoByzantine.
+Proof using . now split. Qed.
 
 (* (* BUG?: To help finding correct instances, loops otherwise! *)
 Existing Instance R_Setoid.
@@ -106,21 +110,10 @@ intros sim x y. destruct (similarity_in_R_case sim) as [Hsim | Hsim];
 repeat rewrite Hsim; cbn in *; field.
 Qed.
 
-Lemma no_byz : forall P (config : configuration), (forall g, P (config (Good g))) -> forall id, P (config id).
-Proof using size_G.
-intros P config Hconfig [g | b].
-+ apply Hconfig.
-+ destruct b. lia.
-Qed.
-
 Lemma no_byz_eq : forall config1 config2 : configuration,
   (forall g, get_location (config1 (Good g)) == get_location (config2 (Good g))) ->
   config1 == config2.
-Proof using size_G.
-intros config1 config2 Heq id. apply WithMultiplicity.no_info. destruct id as [g | b].
-+ apply Heq.
-+ destruct b. lia.
-Qed.
+Proof using . intros. apply no_byz_eq. intro. now apply WithMultiplicity.no_info. Qed.
 
 
 (** Spectra can never be empty as the number of robots is non null. *)
@@ -1448,7 +1441,7 @@ Lemma gathered_precise : forall config pt,
 Proof using size_G.
 intros config pt Hgather id id'. transitivity pt.
 - apply Hgather.
-- symmetry. apply no_byz. apply Hgather.
+- symmetry. apply (no_byz id), Hgather.
 Qed.
 
 Corollary not_gathered_generalize : forall config id,
@@ -1565,7 +1558,7 @@ intros da Hda config pt Hgather. rewrite (round_simplify_Majority).
     induction names as [| id l].
     + reflexivity.
     + simpl. destruct_match.
-      - elim Hdiff. simpl in *. subst. apply no_byz. intro g. apply Hgather.
+      - elim Hdiff. simpl in *. subst. apply (no_byz id), Hgather.
       - apply IHl. }
   rewrite H0. specialize (Hgather g1). rewrite <- Hgather. apply pos_in_config.
 Qed.
diff --git a/CaseStudies/Gathering/InR/Impossibility.v b/CaseStudies/Gathering/InR/Impossibility.v
index 52cdcbfe..751914ec 100644
--- a/CaseStudies/Gathering/InR/Impossibility.v
+++ b/CaseStudies/Gathering/InR/Impossibility.v
@@ -28,6 +28,7 @@ Require Import Pactole.Setting.
 Require Import FMapFacts.
 Require Import Pactole.Spaces.R.
 Require Import Pactole.Models.Rigid.
+Require Import Pactole.Models.NoByzantine.
 Require Import Pactole.CaseStudies.Gathering.WithMultiplicity.
 Set Implicit Arguments.
 Close Scope R_scope.
@@ -40,6 +41,8 @@ Section ImpossibilityProof.
 (** There are n good robots and no byzantine ones. *)
 Variable n : nat.
 Instance MyRobots : Names := Robots n 0.
+Instance NoByz : NoByzantine.
+Proof using . now split. Qed.
 
 (** We assume that the number of robots is even and non-null. *)
 Hypothesis even_nG : Nat.Even n.
@@ -74,6 +77,11 @@ Notation "!! config" := (obs_from_config config origin) (at level 10).
 Implicit Type config : configuration.
 Implicit Type da : demonic_action.
 
+Lemma no_byz_eq : forall config1 config2 : configuration,
+  (forall g, get_location (config1 (Good g)) == get_location (config2 (Good g))) ->
+  config1 == config2.
+Proof using . intros. apply no_byz_eq. intro. now apply WithMultiplicity.no_info. Qed.
+
 Lemma nG_ge_2 : 2 <= nG.
 Proof using even_nG nG_non_0.
 assert (Heven := even_nG). assert (H0 := nG_non_0).
@@ -95,17 +103,6 @@ Definition obs_from_config_spec : forall config (pt : location),
   (!! config)[pt] = countA_occ _ equiv_dec pt (List.map get_location (config_list config))
   := obs_from_config_spec.
 
-Lemma no_byz : forall (id : ident) P, (forall g, P (Good g)) -> P id.
-Proof using nG_non_0.
-intros [g | b] P HP.
-+ apply HP.
-+ destruct b. lia.
-Qed.
-
-Lemma no_byz_eq : forall config1 config2,
-  (forall g, get_location (config1 (Good g)) == get_location (config2 (Good g))) -> config1 == config2.
-Proof using nG_non_0. intros config1 config2 Heq id. apply (no_byz id), Heq. Qed.
-
 Definition mk_info : location -> location := id.
 Lemma mk_info_get_location : forall pt, get_location (mk_info pt) == pt.
 Proof using . reflexivity. Qed.
diff --git a/CaseStudies/Gathering/InR2/Algorithm.v b/CaseStudies/Gathering/InR2/Algorithm.v
index 8cdd7dd9..6923ff9d 100644
--- a/CaseStudies/Gathering/InR2/Algorithm.v
+++ b/CaseStudies/Gathering/InR2/Algorithm.v
@@ -43,6 +43,8 @@ Require Import Pactole.CaseStudies.Gathering.Definitions.
 Require Import Pactole.Observations.MultisetObservation.
 (* Specific to rigidity *)
 Require Import Pactole.Models.Rigid.
+(* Specific to settings with no Byzantine robots *)
+Require Import Pactole.Models.NoByzantine.
 
 (* User defined *)
 Import Permutation.
@@ -71,6 +73,8 @@ Hypothesis size_G : (3 <= n)%nat.
 
 (** There are n good robots and no byzantine ones. *)
 Instance MyRobots : Names := Robots n 0.
+Instance NoByz : NoByzantine.
+Proof using . now split. Qed.
 
 (* Existing Instance R2_Setoid.
 Existing Instance R2_EqDec.
@@ -126,21 +130,10 @@ intro. rewrite config_list_spec, map_cst.
 rewrite names_length. simpl. now rewrite plus_0_r.
 Qed.
 
-Lemma no_byz : forall P, (forall g, P (Good g)) -> forall id, P id.
-Proof using size_G.
-intros P Hg [g | b].
-+ apply Hg.
-+ destruct b. lia.
-Qed.
-
 Lemma no_byz_eq : forall config1 config2 : configuration,
   (forall g, get_location (config1 (Good g)) == get_location (config2 (Good g))) ->
   config1 == config2.
-Proof using size_G.
-intros config1 config2 Heq id. apply WithMultiplicity.no_info. destruct id as [g | b].
-+ apply Heq.
-+ destruct b. lia.
-Qed.
+Proof using . intros. apply no_byz_eq. intro. now apply WithMultiplicity.no_info. Qed.
 
 Lemma map_sim_support : forall (f : Bijection.bijection location) (s : observation),
   PermutationA (@equiv location _) (support (map f s)) (List.map f (support s)).
diff --git a/CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v b/CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v
index 5f53f44a..2146fc56 100644
--- a/CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v
+++ b/CaseStudies/Gathering/InR2/FSyncFlexNoMultAlgorithm.v
@@ -22,6 +22,7 @@ Require Import Psatz.
 Require Import Inverse_Image.
 Require Import Pactole.Setting.
 Require Import Pactole.Models.Flexible.
+Require Import Pactole.Models.NoByzantine.
 Require Import Pactole.Observations.SetObservation.
 Require Import Pactole.Spaces.R2.
 Require Import Pactole.CaseStudies.Gathering.Definitions.
@@ -46,6 +47,8 @@ Hypothesis size_G : (2 <= n)%nat.
 
 (** There are n good robots and no byzantine ones. *)
 Instance MyRobots : Names := Robots n 0.
+Instance NoByz : NoByzantine.
+Proof using . now split. Qed.
 
 Instance Loc : Location := make_Location R2.
 Local Existing Instance R2_VS.
@@ -117,21 +120,10 @@ Coercion paths_in_R2 : location >-> path_R2.
 Instance paths_in_R2_compat : Proper (@equiv _ location_Setoid ==> equiv) paths_in_R2.
 Proof using . intros pt1 pt2 Heq. now rewrite Heq. Qed.
 
-Lemma no_byz : forall P, (forall g, P (Good g)) -> forall id, P id.
-Proof using size_G.
-intros P Hconfig [g | b].
-+ apply Hconfig.
-+ destruct b. lia.
-Qed.
-
 Lemma no_byz_eq : forall config1 config2 : configuration,
   (forall g, get_location (config1 (Good g)) == get_location (config2 (Good g))) ->
   config1 == config2.
-Proof using size_G.
-intros config1 config2 Heq id. apply no_info. destruct id as [g | b].
-+ apply Heq.
-+ destruct b. lia.
-Qed.
+Proof using . intros ? ? Heq. apply no_byz_eq. intro. apply Heq. Qed.
 
 Lemma config_list_alls : forall pt, config_list (fun _ => pt) = alls pt nG.
 Proof using .
@@ -664,7 +656,7 @@ Lemma gathered_precise : forall config pt,
 Proof using size_G.
 intros config pt Hgather id id'. transitivity pt.
 - apply Hgather.
-- symmetry. revert id. apply no_byz, Hgather.
+- symmetry. apply (no_byz id), Hgather.
 Qed.
 (*
 Corollary not_gathered_generalize : forall config id,
diff --git a/CaseStudies/Gathering/InR2/Peleg.v b/CaseStudies/Gathering/InR2/Peleg.v
index 50d1db25..80d03a76 100644
--- a/CaseStudies/Gathering/InR2/Peleg.v
+++ b/CaseStudies/Gathering/InR2/Peleg.v
@@ -22,6 +22,7 @@ Require Import Psatz.
 Require Import Inverse_Image.
 Require Import Pactole.Setting.
 Require Import Pactole.Models.Flexible.
+Require Import Pactole.Models.NoByzantine.
 Require Import Pactole.Observations.MultisetObservation.
 Require Import Pactole.Spaces.R2.
 Require Import Pactole.CaseStudies.Gathering.WithMultiplicity.
@@ -48,6 +49,8 @@ Hypothesis size_G : (2 <= n)%nat.
 
 (** There are n good robots and no byzantine ones. *)
 Instance MyRobots : Names := Robots n 0.
+Instance NoByz : NoByzantine.
+Proof using . now split. Qed.
 
 Instance Loc : Location := make_Location R2.
 Instance Loc_VS : @RealVectorSpace location location_Setoid location_EqDec := R2_VS.
@@ -113,21 +116,11 @@ Coercion paths_in_R2 : location >-> path_R2.
 Instance paths_in_R2_compat : Proper (@equiv _ location_Setoid ==> equiv) paths_in_R2.
 Proof using . intros pt1 pt2 Heq. now rewrite Heq. Qed.
 
-Lemma no_byz : forall P, (forall g, P (Good g)) -> forall id, P id.
-Proof using size_G.
-intros P Hconfig [g | b].
-+ apply Hconfig.
-+ destruct b. lia.
-Qed.
 
 Lemma no_byz_eq : forall config1 config2 : configuration,
   (forall g, get_location (config1 (Good g)) == get_location (config2 (Good g))) ->
   config1 == config2.
-Proof using size_G.
-intros config1 config2 Heq id. apply no_info. destruct id as [g | b].
-+ apply Heq.
-+ destruct b. lia.
-Qed.
+Proof using . intros. apply no_byz_eq. intro. now apply WithMultiplicity.no_info. Qed.
 
 Lemma config_list_alls : forall pt, config_list (fun _ => pt) = alls pt nG.
 Proof using .
@@ -703,7 +696,7 @@ Lemma gathered_precise : forall config pt,
 Proof using size_G.
 intros config pt Hgather id id'. transitivity pt.
 - apply Hgather.
-- symmetry. revert id. apply no_byz, Hgather.
+- symmetry. apply (no_byz id), Hgather.
 Qed.
 (*
 Corollary not_gathered_generalize : forall config id,
diff --git a/CaseStudies/Gathering/InR2/Viglietta.v b/CaseStudies/Gathering/InR2/Viglietta.v
index 543279d6..08580216 100644
--- a/CaseStudies/Gathering/InR2/Viglietta.v
+++ b/CaseStudies/Gathering/InR2/Viglietta.v
@@ -14,6 +14,7 @@ Require Import Pactole.Setting.
 Require Import Pactole.Spaces.R.
 Require Import Pactole.Spaces.R2.
 Require Import Pactole.Models.Similarity.
+Require Import Pactole.Models.NoByzantine.
 Require Import Pactole.CaseStudies.Gathering.Definitions.
 
 (* Helping typeclass resolution avoid infinite loops. *)
@@ -27,8 +28,10 @@ Local Existing Instance R2.R2_ES.
 
 Section RDV.
 
-(** There are only 2 robots: r0 and r1. *)
+(** There are only 2 robots: r0 and r1, and neither is Byzantine. *)
 Instance N : Names := Robots 2 0.
+Instance NoByz : NoByzantine.
+Proof using . now split. Qed.
 
 Notation lt2 := (fun x => x < 2)%nat.
 Definition lt02 : (0 < 2)%nat := ltac:(abstract lia).
@@ -60,15 +63,6 @@ Definition info := (location * light)%type.
 Instance St : State info := AddInfo light
    (OnlyLocation (fun f => sigT (fun sim : similarity location => Bijection.section sim == f))).
 
-(** Since there are none, we can ignore Byzantine robots. *)
-Lemma no_byz_eq : forall config1 config2 : configuration,
-  (forall g, config1 (Good g) == config2 (Good g)) -> config1 == config2.
-Proof using .
-intros config1 config2 Heq id. destruct id as [g | b].
-+ apply Heq.
-+ destruct b. exfalso. lia.
-Qed.
-
 (** The robot have access to the full state of all robots, that is, their locations and lights. *)
 Instance Obs : @Observation info Loc St N.
 simple refine {| observation := info * info;   (* self & other robot's state *)
diff --git a/Models/NoByzantine.v b/Models/NoByzantine.v
new file mode 100644
index 00000000..977fbbc9
--- /dev/null
+++ b/Models/NoByzantine.v
@@ -0,0 +1,32 @@
+Require Import SetoidClass.
+Require Import Pactole.Core.Identifiers.
+Require Import Pactole.Core.State.
+Require Import Pactole.Core.Configuration.
+
+(** To use these results, just provide an instance of the [NoByzantine] class. *)
+
+Section NoByzantine.
+
+Context `{Names}.
+Context `{St : State}.
+
+Class NoByzantine := { nB_eq_0 : nB = 0 }.
+
+Context {NoByz : NoByzantine}.
+(** There is no byzantine robot so we can simplify properties
+    about identifiers and configurations. *)
+Lemma no_byz : forall (id : ident) P, (forall g, P (Good g)) -> P id.
+Proof using NoByz.
+intros [g | b] P HP.
++ apply HP.
++ assert (Hnil : Bnames = nil) by now rewrite <- List.length_zero_iff_nil, Bnames_length, nB_eq_0.
+  elim (@List.in_nil _ b). rewrite <- Hnil. apply In_Bnames.
+Qed.
+
+Lemma no_byz_eq : forall config1 config2 : configuration,
+  (forall g, config1 (Good g) == config2 (Good g)) -> config1 == config2.
+Proof using NoByz.
+intros config1 config2 Heq id. apply (no_byz id). intro g. apply Heq.
+Qed.
+
+End NoByzantine.
diff --git a/_CoqProject b/_CoqProject
index 98b63e82..34d77e30 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -44,6 +44,7 @@ Core/Formalism.v
 Setting.v
 
 ## Models
+Models/NoByzantine.v
 Models/Flexible.v
 Models/Rigid.v
 Models/RigidFlexibleEquivalence.v
-- 
GitLab