replace seq_subst by an implementation based on map

math-comp · Oct 30, 2024 · ef307d3 · ef307d3
1 parent 21f975d
commit ef307d3
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 13 deletions.
diff --git a/theories/cells_alg.v b/theories/cells_alg.v
@@ -3768,7 +3768,7 @@ Lemma connect_limits_seq_subst (l : seq cell) c c' :
   connect_limits l -> connect_limits (seq_subst l c c').
 Proof.
 move=> ll rr; elim: l => [ | a [ | b l] Ih] /=; first by [].
-  by case: ifP.
+  by [].
 move=> /[dup] conn /andP[ab conn'].
 have conn0 : path (fun c1 c2 => right_limit c1 == left_limit c2) a (b :: l).
    by exact: conn.
@@ -3826,7 +3826,7 @@ case: ecg => [[oc [pcc [ocP1 [hP [cP [ocin conn]]]]]] | ].
     rewrite connect_limits_rcons; last by apply/eqP/rcons_neq0.
     move=> /andP[] cP cc.
     rewrite connect_limits_rcons; last first.
-      by case: (pcc')=> /= [ | ? ?]; case: ifP.
+      by case: (pcc')=> /= [ | ? ?].
     apply/andP; split; last first.
       rewrite -cats1 seq_subst_cat /=.
       move: cc; rewrite last_rcons=> /eqP <-.

diff --git a/theories/math_comp_complements.v b/theories/math_comp_complements.v
@@ -10,12 +10,8 @@ Import Order.TTheory GRing.Theory Num.Theory Num.ExtraDef Num.
 
 Open Scope ring_scope.
 
-Fixpoint seq_subst {A : eqType}(l : seq A) (b c : A) : seq A :=
-  match l with
-  | nil => nil
-  | a :: tl =>
-    if a == b then (c :: seq_subst tl b c) else (a :: seq_subst tl b c)
-  end.
+Definition seq_subst {A : eqType} (l : seq A) (b c : A) : seq A :=
+  map [eta id with b |-> c] l.
 
 Lemma mem_seq_subst {A : eqType} (l : seq A) b c x :
   x \in (seq_subst l b c) -> (x \in l) || (x == c).
@@ -25,16 +21,21 @@ rewrite /=.
 by case: ifP => [] ?; rewrite !inE=> /orP[ | /Ih /orP[] ] ->; rewrite ?orbT.
 Qed.
 
+Lemma map_nilp {A B : Type} (f : A -> B) (l : seq A) :
+  nilp [seq f x | x <- l] = nilp l.
+Proof. by case: l. Qed.
+
+Lemma map_eq0 {A B : eqType} (f : A -> B) (l : seq A) :
+  ([seq f x | x <- l] == [::]) = (l == [::]).
+Proof. by case: l. Qed.
+
 Lemma seq_subst_eq0  {A : eqType} (l : seq A) b c :
   (seq_subst l b c == [::]) = (l == [::]).
-Proof. by case : l => [ | a l] //=; case: ifP. Qed.
+Proof. exact: map_eq0. Qed.
 
 Lemma seq_subst_cat {A : eqType} (l1 l2 : seq A) b c :
   seq_subst (l1 ++ l2) b c = seq_subst l1 b c ++ seq_subst l2 b c.
-Proof.
-elim: l1 => [ // | a l1 Ih] /=.
-by case: ifP=> [ab | anb]; rewrite Ih.
-Qed.
+Proof. exact: map_cat. Qed.
 
 Lemma last_in_not_nil (A : eqType) (e : A) (s : seq A) :
 s != [::] -> last e s \in s.