Merge branch 'coq-8.16' of https://gitlab.liris.cnrs.fr/xurbain/pactole-dev 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,6 +123,8 @@ unfold names in Heq. repeat rewrite ?map_app, map_map in Heq. apply eqlistA_app_
 + now do 2 rewrite map_length.
 Qed.
 
+Section Robots.
+
 (** 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.
@@ -147,3 +149,43 @@ Proof using .
 Defined.
 
 Global Opaque G B.
+(* TODO: discuss this
+Section NM.
+
+Variables n m: nat.
+
+Notation GRob := (@G (Robots n m)).
+Notation BRob := (@B (Robots n m)).
+
+Lemma GRob_Robots : GRob = fin n.
+Proof using . reflexivity. Qed.
+
+Lemma BRob_Robots : BRob = fin m.
+Proof using . reflexivity. Qed.
+
+Lemma GRob_Robots_eq_iff : forall g1 g2 : GRob, g1 = g2 :> GRob <-> g1 = g2 :> fin n.
+Proof using . reflexivity. Qed.
+
+Lemma BRob_Robots_eq_iff : forall b1 b2 : BRob, b1 = b2 :> BRob <-> b1 = b2 :> fin m.
+Proof using . reflexivity. Qed.
+
+Definition good0 : GRob := fin0.
+
+Definition byz0 : BRob := fin0.
+
+Lemma all_good0 : forall g : GRob, n = 1 -> g = good0.
+Proof using . intros * H. rewrite GRob_Robots_eq_iff. apply all_fin0, H. Qed.
+
+Lemma all_good_eq : forall g1 g2 : GRob, n = 1 -> g1 = g2.
+Proof using ltc_l_n. intros * H. rewrite GRob_Robots_eq_iff. apply all_eq, H. Qed.
+
+Lemma all_byz0 : forall b : BRob, m = 1 -> b = byz0.
+Proof using . intros * H. rewrite BRob_Robots_eq_iff. apply all_fin0, H. Qed.
+
+Lemma all_byz_eq : forall b1 b2 : BRob, m = 1 -> b1 = b2.
+Proof using ltc_l_m. intros * H. rewrite BRob_Robots_eq_iff. apply all_eq, H. Qed.
+End NM.
+
+*)
+
+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;