From c312c678ac8af99d5c632285cbff5e1b55325478 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Thu, 5 Nov 2020 21:45:23 +0900 Subject: Apply suggestions from code review Co-authored-by: Cyril Cohen --- mathcomp/ssreflect/path.v | 2 +- mathcomp/ssreflect/seq.v | 4 +--- 2 files changed, 2 insertions(+), 4 deletions(-) (limited to 'mathcomp') diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index 04caf36..350e066 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -227,7 +227,7 @@ Proof. by move=> Pxs; rewrite filter_mask; exact: path_mask_in. Qed. Lemma cycle_mask_in m s : all P s -> cycle leT s -> cycle leT (mask m s). Proof. case: (resize_mask m s) => {m} m sizeE ->. -elim: m s sizeE => [|[]m ih] [|x s] //= [sizeE] /andP [Px Ps]. +elim: m s sizeE => [|[] m ih] [|x s] //= [sizeE] /andP[Px Ps]. - rewrite -!cats1 -(mask_cat [:: true] [:: x]) //. by apply: path_mask_in; rewrite /= all_cat /= Px Ps. - move=> xsx; apply: ih => // {sizeE}; case: s xsx Ps => //= y s. diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 57cee21..18e7dac 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -1923,9 +1923,7 @@ Lemma mask_cat m1 m2 s1 s2 : Proof. by move: m1 s1; apply: seq_ind2 => // -[] m1 x1 s1 /= _ ->. Qed. Lemma all_mask a m s : all a s -> all a (mask m s). -Proof. -by elim: m s => [|[] m IHm] [|x s] //= /andP [? /IHm ->]; rewrite ?andbT. -Qed. +Proof. by elim: s m => [|x s IHs] [|[] m]//= /andP[ax /IHs->]; rewrite ?ax. Qed. Lemma has_mask_cons a b m x s : has a (mask (b :: m) (x :: s)) = b && a x || has a (mask m s). -- cgit v1.2.3