diff --git a/Core/Identifiers.v b/Core/Identifiers.v index 2f485ec5b2244f722fb1039f8c9a160bb7e682dd..7b13ef900acc61a5ee97f16c91472dfe01982e63 100644 --- a/Core/Identifiers.v +++ b/Core/Identifiers.v @@ -116,10 +116,14 @@ unfold names in Heq. repeat rewrite ?map_app, map_map in Heq. apply eqlistA_app_ + now do 2 rewrite map_length. Qed. +Section Robots. + +Context (n m : nat) {ln lm : nat} {ltc_l_n : ln <c n} {ltc_l_m : lm <c m}. + (** Given a number of correct and Byzantine robots, we can build canonical names. It is not declared as a global instance to avoid creating spurious settings. *) -Definition Robots (n m : nat) : Names. -Proof using . +Definition Robots : Names. +Proof using n m. refine {| nG := n; nB := m; @@ -138,5 +142,37 @@ Proof using . + intros ? ?. apply enum_eq. + intros ? ?. apply enum_eq. Defined. - Global Opaque G B. + +Notation G := (@G Robots). +Notation B := (@B Robots). + +Lemma G_Robots : G = fin n. +Proof using . reflexivity. Qed. + +Lemma B_Robots : B = fin m. +Proof using . reflexivity. Qed. + +Lemma G_Robots_eq_iff : ∀ g1 g2 : G, g1 = g2 :> G <-> g1 = g2 :> fin n. +Proof using . reflexivity. Qed. + +Lemma B_Robots_eq_iff : ∀ b1 b2 : B, b1 = b2 :> B <-> b1 = b2 :> fin m. +Proof using . reflexivity. Qed. + +Definition good0 : G := fin0. + +Definition byz0 : B := fin0. + +Lemma all_good0 : ∀ g : G, n = 1 -> g = good0. +Proof using . intros * H. rewrite G_Robots_eq_iff. apply all_fin0, H. Qed. + +Lemma all_good_eq : ∀ g1 g2 : G, n = 1 -> g1 = g2. +Proof using ltc_l_n. intros * H. rewrite G_Robots_eq_iff. apply all_eq, H. Qed. + +Lemma all_byz0 : ∀ b : B, m = 1 -> b = byz0. +Proof using . intros * H. rewrite B_Robots_eq_iff. apply all_fin0, H. Qed. + +Lemma all_byz_eq : ∀ b1 b2 : B, m = 1 -> b1 = b2. +Proof using ltc_l_m. intros * H. rewrite B_Robots_eq_iff. apply all_eq, H. Qed. + +End Robots. diff --git a/Spaces/Ring.v b/Spaces/Ring.v index 894c1163b577aec279b2fdce14cf59149912f422..b9368aa0dac8d4f1b963c4cc691c3767a990cbd2 100644 --- a/Spaces/Ring.v +++ b/Spaces/Ring.v @@ -538,6 +538,9 @@ Proof using . specialize (H v2). rewrite (asbfE v1), (asbfE v2) in H. apply H. Qed. +Lemma transs : ∀ v : fin n, trans v v = fin0. +Proof using . intros. rewrite transvE. apply asbfVf. Qed. + Definition sym (v : fin n) : isomorphism Ring. Proof using . refine {| @@ -575,4 +578,7 @@ Lemma move_along_sym : ∀ (v1 v2 : fin n) (d : direction), move_along (sym v1 v2) d = sym v1 (move_along v2 (swap_direction d)). Proof using . intros. rewrite symvE, (sybfE v1). apply move_along_symf. Qed. +Lemma symm : ∀ v : fin n, sym v v = v. +Proof using . intros. rewrite symvE. apply sybff. Qed. + End Ring. diff --git a/Util/Fin.v b/Util/Fin.v index c1fcbaafb9eaf54b01764dcea07579b90c8966a5..24eec458b76b9041cc74a83d5878d9a90031326d 100644 --- a/Util/Fin.v +++ b/Util/Fin.v @@ -1603,6 +1603,9 @@ Proof using . intros * f3. rewrite compE, 3 asbfVE, asbfE, addf_subf. apply subf_subf. Qed. +Lemma asbfVf : ∀ f : fin u, (asbf f)â»Â¹ f = fin0. +Proof using . intros. rewrite asbfVE. apply subff. Qed. + (* * * The bijection on fin u whose section is sucf @@ -1696,4 +1699,7 @@ Proof using . intros c f. rewrite sybfE, sybfVE. reflexivity. Qed. Lemma sybfK : ∀ c : fin u, sybf c ∘ sybf c == id. Proof using . intros c f. rewrite compE, sybfE. apply symfK. Qed. +Lemma sybff : ∀ c : fin u, sybf c c = c. +Proof using . intros. rewrite sybfE. apply symff. Qed. + End mod2fin.