Merge remote-tracking branch 'origin/prod' into coq-8.16

.gitlab-ci.yml

@@ -5,7 +5,8 @@ stages:
   stage: build
   image: coqorg/${CI_JOB_NAME}
   before_script:
-    - if [ -n "${COMPILER_EDGE}" ]; then opam switch ${COMPILER_EDGE} && eval $(opam env); fi
+    - if [ -n "${COMPILER_EDGE}" ]; then opam switch ${COMPILER_EDGE}; fi
+    - eval $(opam env)
     - opam update -y
     - opam config list
     - opam repo list

Core/Identifiers.v

@@ -123,10 +123,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;
@@ -145,5 +149,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.

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.

Util/Fin.v

@@ -1632,6 +1632,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
@@ -1725,4 +1728,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.

Util/ListComplements.v

@@ -54,6 +54,15 @@ intros x l Hin. induction l.
 - destruct Hin. subst. now left. right. auto.
 Qed. *)
 
+Lemma all_eq : forall (l : list A) (a1 : A), In a1 l ->length l = 1
+  -> forall a2 : A, In a2 l -> a2 = a1.
+Proof using .
+  intros * Hi1 H * Hi2. destruct l as [|h t].
+  rewrite (proj2 (length_zero_iff_nil _)) in H by reflexivity. discriminate H.
+  destruct t as [|h1 t]. cbn in Hi1, Hi2. destruct Hi1, Hi2. subst. reflexivity.
+  1-3: contradiction. exfalso. eapply Nat.neq_succ_0, eq_add_S, H.
+Qed.
+
 Lemma InA_Leibniz : forall (x : A) l, InA Logic.eq x l <-> In x l.
 Proof using .
 intros x l. split; intro Hl; induction l; inversion_clear Hl;