Results for fold 1 Results for lemma nth_default: s n : size s <= n -> nth s n = x0 SUCCESS! Proof Found in EFSM: elim : s n => [|x s IHs] [|n] //=. rewrite /= ?eqxx // ltnS => lt_i_s. auto. Tactics applied: 912 Original Proof: [by elim: s n => [|x s IHs] [|n]; try exact (IHs n).] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 3 sec Number of successful tactic applications: 44 Number of failed tactic applications: 868 Results for lemma take_cons: x s : take n0 (x :: s) = if n0 is n.+1 then x :: (take n s) else [::] SUCCESS! Proof Found in EFSM: elim : s => // x s IHs. Tactics applied: 6 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 1 Number of failed tactic applications: 5 Results for lemma mask_cat: m1 s1 : size m1 = size s1 -> forall m2 s2, mask (m1 ++ m2) (s1 ++ s2) = mask m1 s1 ++ mask m2 s2 FAILURE! Tactics applied: 10000 Original Proof: [move=> Hm1 m2 s2; elim: m1 s1 Hm1 => [|b1 m1 IHm] [|x1 s1] //= [Hm1]. by rewrite (IHm _ Hm1); case b1.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 327 Number of failed tactic applications: 9674 Results for lemma rev_cons: x s : rev (x :: s) = rcons (rev s) x FAILURE! Tactics applied: 374 Original Proof: [by rewrite -cats1 -catrevE.] Proof search time: 0 min, 2 sec Number of successful tactic applications: 3 Number of failed tactic applications: 371 Results for lemma rcons_cons: x s z : rcons (x :: s) z = x :: rcons s z SUCCESS! Proof Found in EFSM: elim : s => // x s IHs. Tactics applied: 6 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 1 Number of failed tactic applications: 5 Results for lemma hasPn: s : reflect (forall x, x \in s -> ~~ a x) (~~ has a s) FAILURE! Tactics applied: 10000 Original Proof: [apply: (iffP idP) => not_a_s => [x s_x|]. by apply: contra not_a_s => a_x; apply/hasP; exists x. by apply/hasP=> [[x s_x]]; apply/negP; exact: not_a_s.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 428 Number of failed tactic applications: 9573 Results for lemma drop_rcons: s : n0 <= size s -> forall x, drop n0 (rcons s x) = rcons (drop n0 s) x FAILURE! Tactics applied: 10000 Original Proof: [by elim: s n0 => [|y s IHs] [|n]; try exact (IHs n).] Proof search time: 0 min, 14 sec Number of successful tactic applications: 191 Number of failed tactic applications: 9810 Results for lemma index_size: x s : index x s <= size s SUCCESS! Proof Found in EFSM: elim : s => //= y s IHs; rewrite eq_sym. case : eqP => // ->. Tactics applied: 633 Original Proof: [by rewrite /index find_size.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 2 sec Number of successful tactic applications: 28 Number of failed tactic applications: 605 Results for lemma sub0seq: s : subseq [::] s SUCCESS! Proof Found in EFSM: elim : s => // x s IHs. Tactics applied: 6 Original Proof: [by case: s.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 1 Number of failed tactic applications: 5 Results for lemma all_filterP: s : reflect (filter s = s) (all s) FAILURE! Tactics applied: 10000 Original Proof: [apply: (iffP idP) => [| <-]; last exact: filter_all. by elim: s => //= x s IHs /andP[-> Hs]; rewrite IHs.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 300 Number of failed tactic applications: 9701 Results for lemma size_map: s : size (map s) = size s SUCCESS! Proof Found in EFSM: by elim: s => //= x s ->. Tactics applied: 150 Original Proof: [by elim: s => //= x s ->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 14 Number of failed tactic applications: 136 Results for lemma size0nil: s : size s = 0 -> s = [::] SUCCESS! Proof Found in EFSM: elim : s => // x s IHs. Tactics applied: 6 Original Proof: [by case: s.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 1 Number of failed tactic applications: 5 Results for lemma size_cat: s1 s2 : size (s1 ++ s2) = size s1 + size s2 SUCCESS! Proof Found in EFSM: by elim: s1 => //= x s1 ->. Tactics applied: 183 Original Proof: [by elim: s1 => //= x s1 ->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 6 Number of failed tactic applications: 177 Results for lemma has_filter: a s : has a s = (filter a s != [::]) SUCCESS! Proof Found in EFSM: elim : s => //= x s; case : (a x) => _ //=. Tactics applied: 381 Original Proof: [by rewrite has_count count_filter; case (filter a s).] Shorter Proof Found? no Proof reused from all_count proof search time: 0 min, 2 sec Number of successful tactic applications: 27 Number of failed tactic applications: 354 Results for lemma size_mkseq: f n : size (mkseq f n) = n FAILURE! Tactics applied: 10000 Original Proof: [by rewrite size_map size_iota.] Proof search time: 0 min, 30 sec Number of successful tactic applications: 998 Number of failed tactic applications: 9003 Results for lemma allpairs_uniq: R (f : S -> T -> R) s t : uniq s -> uniq t -> {in [seq (x, y) | x <- s, y <- t] &, injective (prod_curry f)} -> uniq (allpairs f s t) FAILURE! Tactics applied: 10000 Original Proof: [move=> Us Ut inj_f; have: all (mem s) s by exact/allP. elim: {-2}s Us => //= x s1 IHs /andP[s1'x Us1] /andP[sx1 ss1]. rewrite cat_uniq {}IHs // andbT map_inj_in_uniq ?Ut // => [|y1 y2 *]. apply/hasPn=> _ /allpairsP[z [s1z tz ->]]; apply/mapP=> [[y ty Dy]]. suffices [Dz1 _]: (z.1, z.2) = (x, y) by rewrite -Dz1 s1z in s1'x. apply: inj_f => //; apply/allpairsP; last by exists (x, y). by have:= allP ss1 _ s1z; exists z. suffices: (x, y1) = (x, y2) by case. by apply: inj_f => //; apply/allpairsP; [exists (x, y1) | exists (x, y2)].] Proof search time: 0 min, 21 sec Number of successful tactic applications: 415 Number of failed tactic applications: 9586 Results for lemma size_drop: s : size (drop n0 s) = size s - n0 FAILURE! Tactics applied: 10000 Original Proof: [by elim: s n0 => [|x s IHs] [|n]; try exact (IHs n).] Proof search time: 0 min, 18 sec Number of successful tactic applications: 750 Number of failed tactic applications: 9251 Results for lemma eq_in_has: s : {in s, a1 =1 a2} -> has a1 s = has a2 s FAILURE! Tactics applied: 10000 Original Proof: [by move/eq_in_filter=> eq_a12; rewrite !has_filter eq_a12.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 306 Number of failed tactic applications: 9695 Results for lemma cats0: s : s ++ [::] = s SUCCESS! Proof Found in EFSM: by elim: s => //= x s ->. Tactics applied: 150 Original Proof: [by elim: s => //= x s ->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 12 Number of failed tactic applications: 138 Results for lemma nth_rcons: s x n : nth (rcons s x) n = if n < size s then nth s n else if n == size s then x else x0 FAILURE! Tactics applied: 10000 Original Proof: [by elim: s n => [|y s IHs] [|n] //=; rewrite ?nth_nil ?IHs.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1375 Number of failed tactic applications: 8626 Results for lemma cat_nseq: n x s : nseq n x ++ s = ncons n x s SUCCESS! Proof Found in EFSM: by elim: n => //= n ->. Tactics applied: 133 Original Proof: [by elim: n => //= n ->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 3 Number of failed tactic applications: 130 Results for lemma before_find: s i : i < find s -> a (nth s i) = false FAILURE! Tactics applied: 10000 Original Proof: [by elim: s i => //= x s IHs; case Hx: (a x) => [|] // [|i] //; exact: (IHs i).] Proof search time: 0 min, 18 sec Number of successful tactic applications: 675 Number of failed tactic applications: 9326 Results for lemma mask1: b x : mask [:: b] [:: x] = nseq b x SUCCESS! Proof Found in EFSM: by case: b. Tactics applied: 110 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 1 Number of failed tactic applications: 109 Results for lemma eq_in_map: (T1 : eqType) T2 (f1 f2 : T1 -> T2) (s : seq T1) : {in s, f1 =1 f2} <-> map f1 s = map f2 s FAILURE! Tactics applied: 10000 Original Proof: [elim: s => //= x s IHs; split=> [eqf12 | [f12x /IHs eqf12]]; last first. by move=> y /predU1P[-> | /eqf12]. rewrite eqf12 ?mem_head //; congr (_ :: _). by apply/IHs=> y s_y; rewrite eqf12 // mem_behead.] Proof search time: 0 min, 32 sec Number of successful tactic applications: 253 Number of failed tactic applications: 9748 Results for lemma rotr1_rcons: x s : rotr 1 (rcons s x) = x :: s FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -rot1_cons rotK.] Proof search time: 0 min, 39 sec Number of successful tactic applications: 816 Number of failed tactic applications: 9185 Results for lemma mem_allpairs: R (f : S -> T -> R) s1 t1 s2 t2 : s1 =i s2 -> t1 =i t2 -> allpairs f s1 t1 =i allpairs f s2 t2 FAILURE! Tactics applied: 10000 Original Proof: [move=> eq_s eq_t z. by apply/allpairsP/allpairsP=> [] [p fpz]; exists p; rewrite eq_s eq_t in fpz *.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 325 Number of failed tactic applications: 9676 Results for lemma nth_ncons: m x s n : nth (ncons m x s) n = if n < m then x else nth s (n - m) FAILURE! Tactics applied: 3504 Original Proof: [by elim: m n => [|m IHm] [|n] //=; exact: IHm.] Proof search time: 0 min, 8 sec Number of successful tactic applications: 28 Number of failed tactic applications: 3476 Results for lemma find_size: s : find s <= size s SUCCESS! Proof Found in EFSM: elim : s => //= x s; case : (a x) => _ //=. Tactics applied: 381 Original Proof: [by elim: s => //= x s IHs; case (a x).] Shorter Proof Found? no Proof reused from all_count proof search time: 0 min, 2 sec Number of successful tactic applications: 26 Number of failed tactic applications: 355 Results for lemma rot_size: s : rot (size s) s = s FAILURE! Tactics applied: 10000 Original Proof: [exact: rot_oversize.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 988 Number of failed tactic applications: 9013 Results for lemma rev_rotr: s : rev (rotr n0 s) = rot n0 (rev s) FAILURE! Tactics applied: 10000 Original Proof: [apply: canRL rotrK _; rewrite {1}/rotr size_rev size_rotr /rotr {2}/rot rev_cat. set m := size s - n0; rewrite -{1}(@size_takel m _ _ (leq_subr _ _)). by rewrite -size_rev rot_size_cat -rev_cat cat_take_drop.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1105 Number of failed tactic applications: 8896 Results for lemma pmap_sub_uniq: s : uniq s -> uniq (pmap insT s) FAILURE! Tactics applied: 10000 Original Proof: [exact: (pmap_uniq (insubK _)).] Proof search time: 0 min, 19 sec Number of successful tactic applications: 502 Number of failed tactic applications: 9499 Results for lemma perm_eq_uniq: s1 s2 : perm_eq s1 s2 -> uniq s1 = uniq s2 FAILURE! Tactics applied: 10000 Original Proof: [move=> eq_s12; apply: perm_uniq; [exact: perm_eq_mem | exact: perm_eq_size].] Proof search time: 0 min, 17 sec Number of successful tactic applications: 306 Number of failed tactic applications: 9695 Results for lemma size_subseq_leqif: s1 s2 : subseq s1 s2 -> size s1 <= size s2 ?= iff (s1 == s2) FAILURE! Tactics applied: 10000 Original Proof: [move=> sub12; split; first exact: size_subseq. apply/idP/eqP=> [|-> //]; case/subseqP: sub12 => m sz_m ->{s1}. rewrite size_mask -sz_m // -all_count -(eq_all eqb_id). by move/(@all_pred1P _ true)->; rewrite sz_m mask_true.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 1208 Number of failed tactic applications: 8793 Results for lemma foldl_cat: z s1 s2 : foldl z (s1 ++ s2) = foldl (foldl z s1) s2 FAILURE! Tactics applied: 960 Original Proof: [by rewrite -(revK (s1 ++ s2)) foldl_rev rev_cat foldr_cat -!foldl_rev !revK.] Proof search time: 0 min, 2 sec Number of successful tactic applications: 7 Number of failed tactic applications: 953 Results for lemma nth_set_nth: s n y : nth (set_nth s n y) =1 [eta nth s with n |-> y] FAILURE! Tactics applied: 10000 Original Proof: [elim: s n => [|x s IHs] [|n] [|m] //=; rewrite ?nth_nil ?IHs // nth_ncons eqSS. case: ltngtP => // [lt_nm | ->]; last by rewrite subnn. by rewrite nth_default // subn_gt0.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 282 Number of failed tactic applications: 9719 Results for lemma zip_cat: s1 s2 t1 t2 : size s1 = size t1 -> zip (s1 ++ s2) (t1 ++ t2) = zip s1 t1 ++ zip s2 t2 FAILURE! Tactics applied: 10000 Original Proof: [by move/eqP; elim: s1 t1 => [|x s IHs] [|y t] //= /IHs->.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 161 Number of failed tactic applications: 9840 Results for lemma nth_nil: n : nth [::] n = x0 SUCCESS! Proof Found in EFSM: by case: n. Tactics applied: 116 Original Proof: [by case: n.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 1 Number of failed tactic applications: 115 Results for lemma sub_all: s : all a1 s -> all a2 s SUCCESS! Proof Found in EFSM: elim : s => //= x s IHs /andP[not_sfx /IHs->]; rewrite andbT. auto. Tactics applied: 1228 Original Proof: [by rewrite !all_count !eqn_leq !count_size => /leq_trans-> //; exact: sub_count.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 3 sec Number of successful tactic applications: 61 Number of failed tactic applications: 1167 Results for lemma nth_zip: x y s t i : size s = size t -> nth (x, y) (zip s t) i = (nth x s i, nth y t i) FAILURE! Tactics applied: 10000 Original Proof: [by move/eqP; elim: i s t => [|i IHi] [|y1 s1] [|y2 t] //= /IHi->.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 373 Number of failed tactic applications: 9628 Results for lemma allpairs_catr: R (f : S -> T -> R) s t1 t2 : allpairs f s (t1 ++ t2) =i allpairs f s t1 ++ allpairs f s t2 FAILURE! Tactics applied: 10000 Original Proof: [move=> z; rewrite mem_cat. apply/allpairsP/orP=> [[p [sP1]]|]. by rewrite mem_cat; case/orP; [left | right]; apply/allpairsP; exists p. by case=> /allpairsP[p [sp1 sp2 ->]]; exists p; rewrite mem_cat sp2 ?orbT.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 448 Number of failed tactic applications: 9553 Results for lemma subseq_refl: s : subseq s s SUCCESS! Proof Found in EFSM: elim : s => // x s IHs. rewrite /= ?eqxx // ltnS => lt_i_s. Tactics applied: 322 Original Proof: [by elim: s => //= x s IHs; rewrite eqxx.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 sec Number of successful tactic applications: 17 Number of failed tactic applications: 305 Results for lemma drop_size: s : drop (size s) s = [::] SUCCESS! Proof Found in EFSM: elim : s => // x s IHs. Tactics applied: 6 Original Proof: [by rewrite drop_oversize // leqnn.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 1 Number of failed tactic applications: 5 Results for lemma allP: s : reflect (forall x, x \in s -> a x) (all a s) FAILURE! Tactics applied: 10000 Original Proof: [elim: s => [|x s IHs]; first by left. rewrite /= andbC; case: IHs => IHs /=. apply: (iffP idP) => [Hx y|]; last by apply; exact: mem_head. by case/predU1P=> [->|Hy]; auto. by right=> H; case IHs => y Hy; apply H; exact: mem_behead.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 446 Number of failed tactic applications: 9555 Results for lemma size_belast: x s : size (belast x s) = size s FAILURE! Tactics applied: 10000 Original Proof: [by elim: s x => [|y s IHs] x //=; rewrite IHs.] Proof search time: 0 min, 31 sec Number of successful tactic applications: 1095 Number of failed tactic applications: 8906 Results for lemma map_comp: (f1 : T2 -> T3) (f2 : T1 -> T2) s : map (f1 \o f2) s = map f1 (map f2 s) SUCCESS! Proof Found in EFSM: by elim: s => //= x s ->. Tactics applied: 150 Original Proof: [by elim: s => //= x s ->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 11 Number of failed tactic applications: 139 Results for lemma size2_zip: s t : size t <= size s -> size (zip s t) = size t FAILURE! Tactics applied: 10000 Original Proof: [by elim: s t => [|x s IHs] [|y t] //= Hs; rewrite IHs.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 724 Number of failed tactic applications: 9277 Results for lemma unzip2_zip: s t : size t <= size s -> unzip2 (zip s t) = t FAILURE! Tactics applied: 10000 Original Proof: [by elim: s t => [|x s IHs] [|y t] //= le_t_s; rewrite IHs.] Proof search time: 0 min, 15 sec Number of successful tactic applications: 163 Number of failed tactic applications: 9838 Results for lemma has_rotr: a s : has a (rotr n0 s) = has a s SUCCESS! Proof Found in EFSM: by rewrite has_cat orbC -has_cat cat_take_drop. Tactics applied: 266 Original Proof: [by rewrite has_rot.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 14 Number of failed tactic applications: 252 Results for lemma all_map: a s : all a (map s) = all (preim f a) s SUCCESS! Proof Found in EFSM: by elim: s => //= x s ->. Tactics applied: 150 Original Proof: [by elim: s => //= x s ->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 14 Number of failed tactic applications: 136 Results for lemma size_rot: s : size (rot n0 s) = size s FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -{2}[s]cat_take_drop /rot !size_cat addnC.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 750 Number of failed tactic applications: 9251 Results for lemma mem_subseq: s1 s2 : subseq s1 s2 -> {subset s1 <= s2} FAILURE! Tactics applied: 10000 Original Proof: [by case/subseqP=> m _ -> x; exact: mem_mask.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1351 Number of failed tactic applications: 8650 Results for lemma mem_undup: s : undup s =i s FAILURE! Tactics applied: 10000 Original Proof: [move=> x; elim: s => //= y s IHs. by case Hy: (y \in s); rewrite in_cons IHs //; case: eqP => // ->.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 376 Number of failed tactic applications: 9625 Results for lemma perm_eqrP: s1 s2 : reflect (perm_eqr s1 s2) (perm_eq s1 s2) FAILURE! Tactics applied: 10000 Original Proof: [apply: (iffP idP) => [/perm_eqlP eq12 s3| <- //]. by rewrite !(perm_eq_sym s3) eq12.] Proof search time: 0 min, 32 sec Number of successful tactic applications: 953 Number of failed tactic applications: 9048 Results for lemma eq_has_r: s1 s2 : s1 =i s2 -> has^~ s1 =1 has^~ s2 FAILURE! Tactics applied: 10000 Original Proof: [move=> Es12 a; apply/(hasP a s1)/(hasP a s2) => [] [x Hx Hax]; by exists x; rewrite // ?Es12 // -Es12.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 353 Number of failed tactic applications: 9648 Results for lemma has_nil: : has [::] = false SUCCESS! Proof Found in EFSM: by []. Tactics applied: 97 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 3 Number of failed tactic applications: 94 Results for lemma map_inj_in_uniq: s : {in s &, injective f} -> uniq (map f s) = uniq s FAILURE! Tactics applied: 10000 Original Proof: [elim: s => //= x s IHs //= injf; congr (~~ _ && _). apply/mapP/idP=> [[y sy /injf] | ]; last by exists x. by rewrite mem_head mem_behead // => ->. apply: IHs => y z sy sz; apply: injf => //; exact: predU1r.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 319 Number of failed tactic applications: 9682 Results for lemma rot_add_mod: m n s : n <= size s -> m <= size s -> rot m (rot n s) = rot (if m + n <= size s then m + n else m + n - size s) s FAILURE! Tactics applied: 10000 Original Proof: [move=> Hn Hm; case: leqP => [/rot_addn // | /ltnW Hmn]; symmetry. by rewrite -{2}(rotK n s) /rotr -rot_addn size_rot addnBA ?subnK ?addnK.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 537 Number of failed tactic applications: 9464 Results for lemma rot_oversize: n s : size s <= n -> rot n s = s FAILURE! Tactics applied: 10000 Original Proof: [by move=> le_s_n; rewrite /rot take_oversize ?drop_oversize.] Proof search time: 0 min, 14 sec Number of successful tactic applications: 331 Number of failed tactic applications: 9670 Results for lemma rotrK: : cancel (@rotr T n0) (rot n0) FAILURE! Tactics applied: 10000 Original Proof: [move=> s; have [lt_n0s | ge_n0s] := ltnP n0 (size s). by rewrite -{1}(subKn (ltnW lt_n0s)) -{1}[size s]size_rotr; exact: rotK. by rewrite -{2}(rot_oversize ge_n0s) /rotr (eqnP ge_n0s) rot0.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 333 Number of failed tactic applications: 9668 Results for lemma perm_eq_iotaP: {s t : seq T} x0 (It := iota 0 (size t)) : reflect (exists2 Is, perm_eq Is It & s = map (nth x0 t) Is) (perm_eq s t) FAILURE! Tactics applied: 1288 Original Proof: [apply: (iffP idP) => [Est | [Is eqIst ->]]; last first. by rewrite -{2}[t](mkseq_nth x0) perm_map. elim: t => [|x t IHt] in s It Est *. by rewrite (perm_eq_small _ Est) //; exists [::]. have /rot_to[k s1 Ds]: x \in s by rewrite (perm_eq_mem Est) mem_head. have [|Is1 eqIst1 Ds1] := IHt s1; first by rewrite -(perm_cons x) -Ds perm_rot. exists (rotr k (0 :: map succn Is1)). by rewrite perm_rot /It /= perm_cons (iota_addl 1) perm_map. by rewrite map_rotr /= -map_comp -(@eq_map _ _ (nth x0 t)) // -Ds1 -Ds rotK.] Proof search time: 0 min, 3 sec Number of successful tactic applications: 13 Number of failed tactic applications: 1275 Results for lemma mem_nth: s n : n < size s -> nth s n \in s FAILURE! Tactics applied: 10000 Original Proof: [by elim: s n => [|x s IHs] // [_|n sz_s]; rewrite ?mem_head // mem_behead ?IHs.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 651 Number of failed tactic applications: 9350 Results for lemma size_flatten: ss : size (flatten ss) = sumn (shape ss) FAILURE! Tactics applied: 10000 Original Proof: [by elim: ss => //= s ss <-; rewrite size_cat.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 998 Number of failed tactic applications: 9003 Results for lemma perm_eq_refl: s : perm_eq s s SUCCESS! Proof Found in EFSM: case : s => [|x s]; apply /perm_eqP=> a; constructor. Tactics applied: 1935 Original Proof: [exact/perm_eqP.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 4 sec Number of successful tactic applications: 109 Number of failed tactic applications: 1826 Results for lemma zip_rcons: s1 s2 z1 z2 : size s1 = size s2 -> zip (rcons s1 z1) (rcons s2 z2) = rcons (zip s1 s2) (z1, z2) FAILURE! Tactics applied: 10000 Original Proof: [by move=> eq_sz; rewrite -!cats1 zip_cat //= eq_sz.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 256 Number of failed tactic applications: 9745 Results for lemma rotr_size_cat: s1 s2 : rotr (size s2) (s1 ++ s2) = s2 ++ s1 FAILURE! Tactics applied: 10000 Original Proof: [by rewrite /rotr size_cat addnK rot_size_cat.] Proof search time: 0 min, 40 sec Number of successful tactic applications: 1005 Number of failed tactic applications: 8996 Results for lemma mem_rev: s : rev s =i s FAILURE! Tactics applied: 10000 Original Proof: [by move=> y; elim: s => // x s IHs; rewrite rev_cons /= mem_rcons in_cons IHs.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 357 Number of failed tactic applications: 9644 Results for lemma filter_rcons: s x : filter (rcons s x) = if a x then rcons (filter s) x else filter s FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -!cats1 filter_cat /=; case (a x); rewrite /= ?cats0.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 366 Number of failed tactic applications: 9635 Results for lemma mkseq_uniq: (f : nat -> T) n : injective f -> uniq (mkseq f n) FAILURE! Tactics applied: 10000 Original Proof: [by move/map_inj_uniq->; apply: iota_uniq.] Proof search time: 0 min, 32 sec Number of successful tactic applications: 1518 Number of failed tactic applications: 8483 Results for lemma can2_mem_pmap: : pcancel g f -> forall s u, (u \in pmap f s) = (g u \in s) FAILURE! Tactics applied: 10000 Original Proof: [by move=> gK s u; rewrite -(mem_map (pcan_inj gK)) pmap_filter // mem_filter gK.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 513 Number of failed tactic applications: 9488 Results for lemma all_nil: : all [::] = true SUCCESS! Proof Found in EFSM: by []. Tactics applied: 97 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 3 Number of failed tactic applications: 94 Results for lemma filter_id: s : filter (filter s) = filter s FAILURE! Tactics applied: 10000 Original Proof: [by apply/all_filterP; exact: filter_all.] Proof search time: 0 min, 15 sec Number of successful tactic applications: 427 Number of failed tactic applications: 9574 Results for lemma take_nth: n s : n < size s -> take n.+1 s = rcons (take n s) (nth s n) FAILURE! Tactics applied: 10000 Original Proof: [by elim: s n => [|x s IHs] //= [|n] Hn /=; rewrite ?take0 -?IHs.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 615 Number of failed tactic applications: 9386 Results for lemma reshapeKl: sh s : size s >= sumn sh -> shape (reshape sh s) = sh FAILURE! Tactics applied: 10000 Original Proof: [elim: sh s => [[]|n sh IHsh] //= s sz_s. rewrite size_takel; last exact: leq_trans (leq_addr _ _) sz_s. by rewrite IHsh // -(leq_add2l n) size_drop -maxnE leq_max sz_s orbT.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 291 Number of failed tactic applications: 9710 Results for lemma last_rcons: x s z : last x (rcons s z) = z SUCCESS! Proof Found in EFSM: by elim: s x => //= y s IHs x; Tactics applied: 178 Original Proof: [by rewrite -cats1 last_cat.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 5 Number of failed tactic applications: 173 Results for lemma suffix_subseq: s1 s2 : subseq s2 (s1 ++ s2) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -{1}[s2]cat0s cat_subseq ?sub0seq.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1631 Number of failed tactic applications: 8370 Results for lemma subseq_trans: : transitive subseq FAILURE! Tactics applied: 10000 Original Proof: [move=> _ _ s /subseqP[m2 _ ->] /subseqP[m1 _ ->]. elim: s => [|x s IHs] in m2 m1 *; first by rewrite !mask0. case: m1 => [|[] m1]; first by rewrite mask0. case: m2 => [|[] m2] //; first by rewrite /= eqxx IHs. case/subseqP: (IHs m2 m1) => m sz_m def_s; apply/subseqP. by exists (false :: m); rewrite //= sz_m. case/subseqP: (IHs m2 m1) => m sz_m def_s; apply/subseqP. by exists (false :: m); rewrite //= sz_m.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 918 Number of failed tactic applications: 9083 Results for lemma perm_rotr: n s : perm_eql (rotr n s) s FAILURE! Tactics applied: 10000 Original Proof: [exact: perm_rot.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 594 Number of failed tactic applications: 9407 Results for lemma natnseq0P: s : reflect (s = nseq (size s) 0) (sumn s == 0) FAILURE! Tactics applied: 10000 Original Proof: [apply: (iffP idP) => [|->]; last by rewrite sumn_nseq. by elim: s => //= x s IHs; rewrite addn_eq0 => /andP[/eqP-> /IHs <-].] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1112 Number of failed tactic applications: 8889 Results for lemma nth_index_map: s x0 x : {in s &, injective f} -> x \in s -> nth x0 s (index (f x) (map f s)) = x FAILURE! Tactics applied: 10000 Original Proof: [elim: s => //= y s IHs inj_f s_x; rewrite (inj_in_eq inj_f) ?mem_head //. move: s_x; rewrite inE eq_sym; case: eqP => [-> | _] //=; apply: IHs. by apply: sub_in2 inj_f => z; exact: predU1r.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 290 Number of failed tactic applications: 9711 Results for lemma index_head: x s : index x (x :: s) = 0 SUCCESS! Proof Found in EFSM: elim : s => [|y s IHs] //=. rewrite /= ?eqxx // ltnS => lt_i_s. case : eqP => // ->. Tactics applied: 533 Original Proof: [by rewrite /= eqxx.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 2 sec Number of successful tactic applications: 18 Number of failed tactic applications: 515 Results for lemma mem_seq4: x y1 y2 y3 y4 : (x \in [:: y1; y2; y3; y4]) = xpred4 y1 y2 y3 y4 x SUCCESS! Proof Found in EFSM: by rewrite !inE. Tactics applied: 241 Original Proof: [by rewrite !inE.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 4 Number of failed tactic applications: 237 Results for lemma hasP: s : reflect (exists2 x, x \in s & a x) (has a s) FAILURE! Tactics applied: 1328 Original Proof: [elim: s => [|y s IHs] /=; first by right; case. case ay: (a y); first by left; exists y; rewrite ?mem_head. apply: (iffP IHs) => [] [x ysx ax]; exists x => //; first exact: mem_behead. by case: (predU1P ysx) ax => [->|//]; rewrite ay.] Proof search time: 0 min, 3 sec Number of successful tactic applications: 14 Number of failed tactic applications: 1314 Results for lemma mem_behead: s : {subset behead s <= s} FAILURE! Tactics applied: 10000 Original Proof: [by case: s => // y s x; exact: predU1r.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 363 Number of failed tactic applications: 9638 Results for lemma take_size: s : take (size s) s = s SUCCESS! Proof Found in EFSM: by elim: s => //= x s ->. Tactics applied: 150 Original Proof: [by rewrite take_oversize // leqnn.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 12 Number of failed tactic applications: 138 Results for lemma uniq_catCA: s1 s2 s3 : uniq (s1 ++ s2 ++ s3) = uniq (s2 ++ s1 ++ s3) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite !catA -!(uniq_catC s3) !(cat_uniq s3) uniq_catC !has_cat orbC.] Proof search time: 0 min, 32 sec Number of successful tactic applications: 1449 Number of failed tactic applications: 8552 Results for lemma has_pred0: s : has pred0 s = false SUCCESS! Proof Found in EFSM: elim : s => // x s IHs. Tactics applied: 6 Original Proof: [by rewrite has_count count_pred0.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 1 Number of failed tactic applications: 5 Results for lemma cat0s: s : [::] ++ s = s SUCCESS! Proof Found in EFSM: elim : s => // x s IHs. Tactics applied: 6 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 1 Number of failed tactic applications: 5 Results for lemma mask_true: s n : size s <= n -> mask (nseq n true) s = s FAILURE! Tactics applied: 10000 Original Proof: [by elim: s n => [|x s IHs] [|n] //= Hn; congr (_ :: _); apply: IHs.] Proof search time: 0 min, 15 sec Number of successful tactic applications: 227 Number of failed tactic applications: 9774 Results for lemma mem_rcons: s y : rcons s y =i y :: s FAILURE! Tactics applied: 10000 Original Proof: [by move=> x; rewrite -cats1 /= mem_cat mem_seq1 orbC in_cons.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 339 Number of failed tactic applications: 9662 Results for lemma index_cat: x s1 s2 : index x (s1 ++ s2) = if x \in s1 then index x s1 else size s1 + index x s2 FAILURE! Tactics applied: 10000 Original Proof: [by rewrite /index find_cat has_pred1.] Proof search time: 0 min, 31 sec Number of successful tactic applications: 1441 Number of failed tactic applications: 8560 Results for lemma nth_mkseq: f n i : i < n -> nth x0 (mkseq f n) i = f i FAILURE! Tactics applied: 686 Original Proof: [by move=> Hi; rewrite (nth_map 0) ?nth_iota ?size_iota.] Proof search time: 0 min, 2 sec Number of successful tactic applications: 12 Number of failed tactic applications: 674 Results for lemma rot_rotr: m n s : rot m (rotr n s) = rotr n (rot m s) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite {2}/rotr size_rot rot_rot.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 735 Number of failed tactic applications: 9266 Results for lemma perm_eq_sym: : symmetric perm_eq FAILURE! Tactics applied: 10000 Original Proof: [by move=> s1 s2; apply/perm_eqP/perm_eqP=> ? ?.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 372 Number of failed tactic applications: 9629 Results for lemma rem_id: s : x \notin s -> rem s = s FAILURE! Tactics applied: 10000 Original Proof: [by elim: s => //= y s IHs /norP[neq_yx /IHs->]; rewrite eq_sym (negbTE neq_yx).] Proof search time: 0 min, 22 sec Number of successful tactic applications: 344 Number of failed tactic applications: 9657 Results for lemma constantP: s : reflect (exists x, s = nseq (size s) x) (constant s) FAILURE! Tactics applied: 1332 Original Proof: [apply: (iffP idP) => [| [x ->]]; last exact: constant_nseq. case: s => [|x s] /=; first by exists x0. by move/all_pred1P=> def_s; exists x; rewrite -def_s.] Proof search time: 0 min, 3 sec Number of successful tactic applications: 16 Number of failed tactic applications: 1316 Results for lemma size_subseq: s1 s2 : subseq s1 s2 -> size s1 <= size s2 FAILURE! Tactics applied: 10000 Original Proof: [by case/subseqP=> m sz_m ->; rewrite size_mask -sz_m ?count_size.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 1343 Number of failed tactic applications: 8658 Results for lemma rotr_uniq: (s : seq T') : uniq (rotr n0 s) = uniq s FAILURE! Tactics applied: 10000 Original Proof: [by rewrite rot_uniq.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 769 Number of failed tactic applications: 9232 Results for lemma inj_map: : injective f -> injective map FAILURE! Tactics applied: 10000 Original Proof: [by move=> injf; elim=> [|y1 s1 IHs] [|y2 s2] //= [/injf-> /IHs->].] Proof search time: 0 min, 17 sec Number of successful tactic applications: 357 Number of failed tactic applications: 9644 Results for lemma rot_uniq: s : uniq (rot n0 s) = uniq s FAILURE! Tactics applied: 10000 Original Proof: [by rewrite /rot uniq_catC cat_take_drop.] Proof search time: 0 min, 27 sec Number of successful tactic applications: 756 Number of failed tactic applications: 9245 Results for lemma subseq_filter: s1 s2 a : subseq s1 (filter a s2) = all a s1 && subseq s1 s2 FAILURE! Tactics applied: 10000 Original Proof: [elim: s2 s1 => [|x s2 IHs] [|y s1] //=; rewrite ?andbF ?sub0seq //. by case a_x: (a x); rewrite /= !IHs /=; case: eqP => // ->; rewrite a_x.] Proof search time: 0 min, 33 sec Number of successful tactic applications: 1246 Number of failed tactic applications: 8755 Results for lemma map_rcons: s x : map (rcons s x) = rcons (map s) (f x) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -!cats1 map_cat.] Proof search time: 0 min, 42 sec Number of successful tactic applications: 816 Number of failed tactic applications: 9185 Results for lemma rem_filter: s : uniq s -> rem s = filter (predC1 x) s FAILURE! Tactics applied: 10000 Original Proof: [elim: s => //= y s IHs /andP[not_s_y /IHs->]. by case: eqP => //= <-; apply/esym/all_filterP; rewrite all_predC has_pred1.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 367 Number of failed tactic applications: 9634 Results for lemma drop_behead: : drop n0 =1 iter n0 behead FAILURE! Tactics applied: 10000 Original Proof: [by elim: n0 => [|n IHn] [|x s] //; rewrite iterSr -IHn.] Proof search time: 0 min, 15 sec Number of successful tactic applications: 261 Number of failed tactic applications: 9740 Results for lemma rev_zip: s1 s2 : size s1 = size s2 -> rev (zip s1 s2) = zip (rev s1) (rev s2) FAILURE! Tactics applied: 10000 Original Proof: [elim: s1 s2 => [|x s1 IHs] [|y s2] //= [eq_sz]. by rewrite !rev_cons zip_rcons ?IHs ?size_rev.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 250 Number of failed tactic applications: 9751 Results for lemma sub_has: s : has a1 s -> has a2 s FAILURE! Tactics applied: 10000 Original Proof: [by rewrite !has_find; exact: leq_ltn_trans (sub_find s).] Proof search time: 0 min, 14 sec Number of successful tactic applications: 449 Number of failed tactic applications: 9552 Results for lemma cat_uniq: s1 s2 : uniq (s1 ++ s2) = [&& uniq s1, ~~ has (mem s1) s2 & uniq s2] FAILURE! Tactics applied: 10000 Original Proof: [elim: s1 => [|x s1 IHs]; first by rewrite /= has_pred0. by rewrite has_sym /= mem_cat !negb_or has_sym IHs -!andbA; do !bool_congr.] Proof search time: 0 min, 49 sec Number of successful tactic applications: 1102 Number of failed tactic applications: 8899 Results for lemma mem_take: s x : x \in take n0 s -> x \in s FAILURE! Tactics applied: 10000 Original Proof: [by move=> s0x; rewrite -(cat_take_drop n0 s) mem_cat /= s0x.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 351 Number of failed tactic applications: 9650 Results for lemma find_cat: s1 s2 : find (s1 ++ s2) = if has s1 then find s1 else size s1 + find s2 FAILURE! Tactics applied: 10000 Original Proof: [by elim: s1 => //= x s1 IHs; case: (a x) => //; rewrite IHs (fun_if succn).] Proof search time: 0 min, 23 sec Number of successful tactic applications: 942 Number of failed tactic applications: 9059 Results for lemma iota_uniq: m n : uniq (iota m n) FAILURE! Tactics applied: 10000 Original Proof: [by elim: n m => //= n IHn m; rewrite mem_iota ltnn /=.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 1444 Number of failed tactic applications: 8557 Results for lemma mkseq_nth: s : mkseq (nth x0 s) (size s) = s FAILURE! Tactics applied: 10000 Original Proof: [by apply: (@eq_from_nth _ x0); rewrite size_mkseq // => i Hi; rewrite nth_mkseq.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 306 Number of failed tactic applications: 9695 Results for lemma map_id_in: (T : eqType) f (s : seq T) : {in s, f =1 id} -> map f s = s FAILURE! Tactics applied: 10000 Original Proof: [by move/eq_in_map->; apply: map_id.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 338 Number of failed tactic applications: 9663 Results for lemma map_mask: m s : map (mask m s) = mask m (map s) FAILURE! Tactics applied: 10000 Original Proof: [by elim: m s => [|[|] m IHm] [|x p] //=; rewrite IHm.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 473 Number of failed tactic applications: 9528 Results for lemma perm_catAC: s1 s2 s3 : perm_eql ((s1 ++ s2) ++ s3) ((s1 ++ s3) ++ s2) FAILURE! Tactics applied: 10000 Original Proof: [by apply/perm_eqlP; rewrite -!catA perm_cat2l perm_catC.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 400 Number of failed tactic applications: 9601 Results for lemma nconsK: n x : cancel (ncons n x) (drop n) FAILURE! Tactics applied: 10000 Original Proof: [by elim: n => //; case.] Proof search time: 0 min, 15 sec Number of successful tactic applications: 232 Number of failed tactic applications: 9769 Results for lemma has_count: s : has s = (0 < count s) SUCCESS! Proof Found in EFSM: elim : s => //= x s; case : (a x) => _ //=. Tactics applied: 375 Original Proof: [by elim: s => //= x s ->; case (a x).] Shorter Proof Found? no Proof reused from all_count proof search time: 0 min, 2 sec Number of successful tactic applications: 24 Number of failed tactic applications: 351 Results for lemma subseqP: s1 s2 : reflect (exists2 m, size m = size s2 & s1 = mask m s2) (subseq s1 s2) FAILURE! Tactics applied: 350 Original Proof: [elim: s2 s1 => [|y s2 IHs2] [|x s1]. - by left; exists [::]. - by right; do 2!case. - by left; exists (nseq (size s2).+1 false); rewrite ?size_nseq //= mask_false. apply: {IHs2}(iffP (IHs2 _)) => [] [m sz_m def_s1]. by exists ((x == y) :: m); rewrite /= ?sz_m // -def_s1; case: eqP => // ->. case: eqP => [_ | ne_xy]; last first. by case: m def_s1 sz_m => [//|[m []//|m]] -> [<-]; exists m. pose i := index true m; have def_m_i: take i m = nseq (size (take i m)) false. apply/all_pred1P; apply/(all_nthP true) => j. rewrite size_take ltnNge geq_min negb_or -ltnNge; case/andP=> lt_j_i _. rewrite nth_take //= -negb_add addbF -addbT -negb_eqb. by rewrite [_ == _](before_find _ lt_j_i). have lt_i_m: i < size m. rewrite ltnNge; apply/negP=> le_m_i; rewrite take_oversize // in def_m_i. by rewrite def_m_i mask_false in def_s1. rewrite size_take lt_i_m in def_m_i. exists (take i m ++ drop i.+1 m). rewrite size_cat size_take size_drop lt_i_m. by rewrite sz_m in lt_i_m *; rewrite subnKC. rewrite {s1 def_s1}[s1](congr1 behead def_s1). rewrite -[s2](cat_take_drop i) -{1}[m](cat_take_drop i) {}def_m_i -cat_cons. have sz_i_s2: size (take i s2) = i by apply: size_takel; rewrite sz_m in lt_i_m. rewrite lastI cat_rcons !mask_cat ?size_nseq ?size_belast ?mask_false //=. by rewrite (drop_nth true) // nth_index -?index_mem.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 2 Number of failed tactic applications: 348 Results for lemma mem_mask: x m s : x \in mask m s -> x \in s FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -!has_pred1 => /has_mask.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 371 Number of failed tactic applications: 9630 Results for lemma mem_last: x s : last x s \in x :: s FAILURE! Tactics applied: 10000 Original Proof: [by rewrite lastI mem_rcons mem_head.] Proof search time: 0 min, 39 sec Number of successful tactic applications: 733 Number of failed tactic applications: 9268 Results for lemma mem_rem: s : {subset rem s <= s} FAILURE! Tactics applied: 10000 Original Proof: [exact: mem_subseq (rem_subseq s).] Proof search time: 0 min, 22 sec Number of successful tactic applications: 348 Number of failed tactic applications: 9653 Results for lemma cat_subseq: s1 s2 s3 s4 : subseq s1 s3 -> subseq s2 s4 -> subseq (s1 ++ s2) (s3 ++ s4) FAILURE! Tactics applied: 10000 Original Proof: [case/subseqP=> m1 sz_m1 ->; case/subseqP=> m2 sz_m2 ->; apply/subseqP. by exists (m1 ++ m2); rewrite ?size_cat ?mask_cat ?sz_m1 ?sz_m2.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 359 Number of failed tactic applications: 9642 Results for lemma mask_rot: m s : size m = size s -> mask (rot n0 m) (rot n0 s) = rot (count id (take n0 m)) (mask m s) FAILURE! Tactics applied: 10000 Original Proof: [move=> Hs. have Hsn0: size (take n0 m) = size (take n0 s) by rewrite !size_take Hs. rewrite -(size_mask Hsn0) {1 2}/rot mask_cat ?size_drop ?Hs //. rewrite -{4}(cat_take_drop n0 m) -{4}(cat_take_drop n0 s) mask_cat //. by rewrite rot_size_cat.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 162 Number of failed tactic applications: 9839 Results for lemma scanl_cat: x s1 s2 : scanl x (s1 ++ s2) = scanl x s1 ++ scanl (foldl g x s1) s2 FAILURE! Tactics applied: 10000 Original Proof: [by elim: s1 x => //= y s1 IHs1 x; rewrite IHs1.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 215 Number of failed tactic applications: 9786 Results for lemma map_take: s : map (take n0 s) = take n0 (map s) FAILURE! Tactics applied: 10000 Original Proof: [by elim: n0 s => [|n IHn] [|x s] //=; rewrite IHn.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 974 Number of failed tactic applications: 9027 Results for lemma map_rotr: s : map (rotr n0 s) = rotr n0 (map s) FAILURE! Tactics applied: 10000 Original Proof: [by apply: canRL (@rotK n0 T2) _; rewrite -map_rot rotrK.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 975 Number of failed tactic applications: 9026 Results for lemma filter_pred0: s : filter pred0 s = [::] SUCCESS! Proof Found in EFSM: elim : s => // x s IHs. Tactics applied: 6 Original Proof: [by elim: s.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 1 Number of failed tactic applications: 5 Results for lemma allPn: s : reflect (exists2 x, x \in s & ~~ a x) (~~ all a s) FAILURE! Tactics applied: 1370 Original Proof: [elim: s => [|x s IHs]; first by right=> [[x Hx _]]. rewrite /= andbC negb_and; case: IHs => IHs /=. by left; case: IHs => y Hy Hay; exists y; first exact: mem_behead. apply: (iffP idP) => [|[y]]; first by exists x; rewrite ?mem_head. by case/predU1P=> [-> // | s_y not_a_y]; case: IHs; exists y.] Proof search time: 0 min, 3 sec Number of successful tactic applications: 15 Number of failed tactic applications: 1355 Results for lemma eq_count: a1 a2 : a1 =1 a2 -> count a1 =1 count a2 FAILURE! Tactics applied: 10000 Original Proof: [by move=> Ea s; rewrite !count_filter (eq_filter Ea).] Proof search time: 0 min, 19 sec Number of successful tactic applications: 466 Number of failed tactic applications: 9535 Results for lemma nth_cat: s1 s2 n : nth (s1 ++ s2) n = if n < size s1 then nth s1 n else nth s2 (n - size s1) FAILURE! Tactics applied: 347 Original Proof: [by elim: s1 n => [|x s1 IHs] [|n]; try exact (IHs n).] Proof search time: 0 min, 1 sec Number of successful tactic applications: 2 Number of failed tactic applications: 345 Results for lemma size_nseq: n x : size (nseq n x) = n SUCCESS! Proof Found in EFSM: by elim: n => //= n ->. Tactics applied: 133 Original Proof: [by rewrite size_ncons addn0.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 3 Number of failed tactic applications: 130 Results for lemma drop1: : drop 1 =1 behead SUCCESS! Proof Found in EFSM: move => s; rewrite -(cat0s s). elim : s => //= y s IHs; rewrite drop0. constructor. Tactics applied: 6599 Original Proof: [by case=> [|x [|y s]].] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 10 sec Number of successful tactic applications: 359 Number of failed tactic applications: 6240 Results for lemma has_sym: s1 s2 : has (mem s1) s2 = has (mem s2) s1 FAILURE! Tactics applied: 10000 Original Proof: [by apply/(hasP _ s2)/(hasP _ s1) => [] [x]; exists x.] Proof search time: 0 min, 55 sec Number of successful tactic applications: 1077 Number of failed tactic applications: 8924 Results for lemma has_predC: a s : has (predC a) s = ~~ all a s SUCCESS! Proof Found in EFSM: elim : s => //= x s; case : (a x) => _ //=. Tactics applied: 381 Original Proof: [by elim: s => //= x s ->; case (a x).] Shorter Proof Found? no Proof reused from all_count proof search time: 0 min, 2 sec Number of successful tactic applications: 24 Number of failed tactic applications: 357 Results for lemma sub_count: s : count a1 s <= count a2 s FAILURE! Tactics applied: 10000 Original Proof: [by elim: s => //= x s; apply: leq_add; case a1x: (a1 x); rewrite // s12.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 642 Number of failed tactic applications: 9359 Results for lemma sub_find: s : find a2 s <= find a1 s FAILURE! Tactics applied: 10000 Original Proof: [by elim: s => //= x s IHs; case: ifP => // /(contraFF (@s12 x))->.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 639 Number of failed tactic applications: 9362 Results for lemma uniq_perm_eq: s1 s2 : uniq s1 -> uniq s2 -> s1 =i s2 -> perm_eq s1 s2 FAILURE! Tactics applied: 10000 Original Proof: [move=> Us1 Us2 eq12; apply/allP=> x _; apply/eqP. by rewrite !count_uniq_mem ?eq12.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 226 Number of failed tactic applications: 9775 Results for lemma all_pred1P: x s : reflect (s = nseq (size s) x) (all (pred1 x) s) FAILURE! Tactics applied: 368 Original Proof: [elim: s => [|y s IHs] /=; first by left. case: eqP => [->{y} | ne_xy]; last by right=> [] [? _]; case ne_xy. by apply: (iffP IHs) => [<- //| []].] Proof search time: 0 min, 1 sec Number of successful tactic applications: 2 Number of failed tactic applications: 366 Results for lemma take_size_cat: n s1 s2 : size s1 = n -> take n (s1 ++ s2) = s1 FAILURE! Tactics applied: 10000 Original Proof: [by move <-; elim: s1 => [|x s1 IHs]; rewrite ?take0 //= IHs.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 323 Number of failed tactic applications: 9678 Results for lemma catrev_catr: s t u : catrev s (t ++ u) = catrev s t ++ u FAILURE! Tactics applied: 10000 Original Proof: [by elim: s t => //= x s IHs t; rewrite -IHs.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 290 Number of failed tactic applications: 9711 Results for lemma filter_predT: s : filter predT s = s SUCCESS! Proof Found in EFSM: by elim: s => //= x s ->. Tactics applied: 150 Original Proof: [by elim: s => //= x s ->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 12 Number of failed tactic applications: 138 Results for lemma in_nil: x : (x \in [::]) = false SUCCESS! Proof Found in EFSM: by []. Tactics applied: 97 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 3 Number of failed tactic applications: 94 Results for lemma has_predT: s : has predT s = (0 < size s) SUCCESS! Proof Found in EFSM: elim : s => // x s IHs. Tactics applied: 6 Original Proof: [by rewrite has_count count_predT.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 1 Number of failed tactic applications: 5 Results for lemma map_pK: : pcancel g f -> cancel (map g) pmap FAILURE! Tactics applied: 10000 Original Proof: [by move=> gK; elim=> //= x s ->; rewrite gK.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 355 Number of failed tactic applications: 9646 Results for lemma map_subseq: s1 s2 : subseq s1 s2 -> subseq (map f s1) (map f s2) FAILURE! Tactics applied: 10000 Original Proof: [case/subseqP=> m sz_m ->; apply/subseqP. by exists m; rewrite ?size_map ?map_mask.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 1689 Number of failed tactic applications: 8312 Results for lemma flattenK: ss : reshape (shape ss) (flatten ss) = ss FAILURE! Tactics applied: 302 Original Proof: [by elim: ss => //= s ss IHss; rewrite take_size_cat ?drop_size_cat ?IHss.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 0 Number of failed tactic applications: 302 Results for lemma scanlK: : (forall x, cancel (g x) (f x)) -> forall x, cancel (scanl x) (pairmap x) FAILURE! Tactics applied: 10000 Original Proof: [by move=> Hfg x s; elim: s x => //= y s IHs x; rewrite Hfg IHs.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 351 Number of failed tactic applications: 9650 Results for lemma all_pred0: s : all pred0 s = (size s == 0) SUCCESS! Proof Found in EFSM: elim : s => // x s IHs. Tactics applied: 6 Original Proof: [by rewrite all_count count_pred0 eq_sym.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 1 Number of failed tactic applications: 5 Results for lemma size_mask: m s : size m = size s -> size (mask m s) = count id m FAILURE! Tactics applied: 10000 Original Proof: [by elim: m s => [|b m IHm] [|x s] //= [Hs]; case: b; rewrite /= IHm.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 423 Number of failed tactic applications: 9578 Results for lemma has_find: s : has s = (find s < size s) SUCCESS! Proof Found in EFSM: elim : s => //= x s; case : (a x) => _ //=. Tactics applied: 381 Original Proof: [by elim: s => //= x s IHs; case (a x); rewrite ?leqnn.] Shorter Proof Found? yes Proof reused from all_count proof search time: 0 min, 2 sec Number of successful tactic applications: 24 Number of failed tactic applications: 357 Results for lemma eq_has: a1 a2 : a1 =1 a2 -> has a1 =1 has a2 FAILURE! Tactics applied: 10000 Original Proof: [by move=> Ea s; rewrite !has_count (eq_count Ea).] Proof search time: 0 min, 16 sec Number of successful tactic applications: 452 Number of failed tactic applications: 9549 Results for lemma perm_to_subseq: s1 s2 : subseq s1 s2 -> {s3 | perm_eq s2 (s1 ++ s3)} FAILURE! Tactics applied: 2014 Original Proof: [elim Ds2: s2 s1 => [|y s2' IHs] [|x s1] //=; try by exists s2; rewrite Ds2. case: eqP => [-> | _] /IHs[s3 perm_s2] {IHs}. by exists s3; rewrite perm_cons. by exists (rcons s3 y); rewrite -cat_cons -perm_rcons -!cats1 catA perm_cat2r.] Proof search time: 0 min, 3 sec Number of successful tactic applications: 24 Number of failed tactic applications: 1990 Results for lemma count_predUI: a1 a2 s : count (predU a1 a2) s + count (predI a1 a2) s = count a1 s + count a2 s FAILURE! Tactics applied: 10000 Original Proof: [elim: s => //= x s IHs; rewrite /= addnCA -addnA IHs addnA addnC. by rewrite -!addnA; do 2 nat_congr; case (a1 x); case (a2 x).] Proof search time: 0 min, 20 sec Number of successful tactic applications: 747 Number of failed tactic applications: 9254 Results for lemma mem_belast: s y : {subset belast y s <= y :: s} FAILURE! Tactics applied: 10000 Original Proof: [by move=> x ys'x; rewrite lastI mem_rcons mem_behead.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 340 Number of failed tactic applications: 9661 Results for lemma size_rem: s : x \in s -> size (rem s) = (size s).-1 FAILURE! Tactics applied: 10000 Original Proof: [by move/perm_to_rem/perm_eq_size->.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 512 Number of failed tactic applications: 9489 Results for lemma rot0: s : rot 0 s = s FAILURE! Tactics applied: 10000 Original Proof: [by rewrite /rot drop0 take0 cats0.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 1133 Number of failed tactic applications: 8868 Results for lemma mem_mask_rot: m s : size m = size s -> mask (rot n0 m) (rot n0 s) =i mask m s FAILURE! Tactics applied: 10000 Original Proof: [by move=> Hm x; rewrite mask_rot // mem_rot.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 249 Number of failed tactic applications: 9752 Results for lemma perm_to_rem: s : x \in s -> perm_eq s (x :: rem s) FAILURE! Tactics applied: 10000 Original Proof: [elim: s => // y s IHs; rewrite inE /= eq_sym perm_eq_sym. case: eqP => [-> // | _ /IHs]. by rewrite (perm_catCA [:: x] [:: y]) perm_cons perm_eq_sym.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 436 Number of failed tactic applications: 9565 Results for lemma mapK: (f1 : T1 -> T2) (f2 : T2 -> T1) : cancel f1 f2 -> cancel (map f1) (map f2) FAILURE! Tactics applied: 10000 Original Proof: [by move=> eq_f12; elim=> //= x s ->; rewrite eq_f12.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 374 Number of failed tactic applications: 9627 Results for lemma foldl_rev: z s : foldl z (rev s) = foldr (fun x z => f z x) z s FAILURE! Tactics applied: 10000 Original Proof: [elim/last_ind: s z => [|s x IHs] z //=. by rewrite rev_rcons -cats1 foldr_cat -IHs.] Proof search time: 0 min, 15 sec Number of successful tactic applications: 131 Number of failed tactic applications: 9870 Results for lemma subseq0: s : subseq s [::] = (s == [::]) SUCCESS! Proof Found in EFSM: elim : s => // x s IHs. Tactics applied: 6 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 1 Number of failed tactic applications: 5 Results for lemma pmap_uniq: s : uniq s -> uniq (pmap f s) FAILURE! Tactics applied: 10000 Original Proof: [by move/(filter_uniq [eta f]); rewrite -(pmap_filter fK); exact: map_uniq.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 505 Number of failed tactic applications: 9496 Results for lemma size_scanl: x s : size (scanl x s) = size s FAILURE! Tactics applied: 10000 Original Proof: [by elim: s x => //= y s IHs x; rewrite IHs.] Proof search time: 0 min, 34 sec Number of successful tactic applications: 994 Number of failed tactic applications: 9007 Results for lemma nth_behead: s n : nth (behead s) n = nth s n.+1 SUCCESS! Proof Found in EFSM: elim : s n => [|x s IHs] [|n] //=. Tactics applied: 27 Original Proof: [by case: s n => [|x s] [|n].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 4 Number of failed tactic applications: 23 Results for lemma rot_to: s x : x \in s -> rot_to_spec s x FAILURE! Tactics applied: 10000 Original Proof: [move=> s_x; pose i := index x s; exists i (drop i.+1 s ++ take i s). rewrite -cat_cons {}/i; congr cat; elim: s s_x => //= y s IHs. by rewrite eq_sym in_cons; case: eqP => // -> _; rewrite drop0.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 178 Number of failed tactic applications: 9823 Results for lemma filter_undup: p s : filter p (undup s) = undup (filter p s) FAILURE! Tactics applied: 10000 Original Proof: [elim: s => //= x s IHs; rewrite (fun_if undup) fun_if /= mem_filter /=. by rewrite (fun_if (filter p)) /= IHs; case: ifP => -> //=; exact: if_same.] Proof search time: 0 min, 28 sec Number of successful tactic applications: 683 Number of failed tactic applications: 9318 Results for lemma filter_map: a s : filter a (map s) = map (filter (preim f a) s) FAILURE! Tactics applied: 10000 Original Proof: [by elim: s => //= x s IHs; rewrite (fun_if map) /= IHs.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 975 Number of failed tactic applications: 9026 Results for lemma map_cat: s1 s2 : map (s1 ++ s2) = map s1 ++ map s2 SUCCESS! Proof Found in EFSM: by elim: s1 => //= x s1 ->. Tactics applied: 183 Original Proof: [by elim: s1 => [|x s1 IHs] //=; rewrite IHs.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 4 Number of failed tactic applications: 179 Results for lemma allpairs_cat: s1 s2 t : allpairs (s1 ++ s2) t = allpairs s1 t ++ allpairs s2 t FAILURE! Tactics applied: 10000 Original Proof: [by elim: s1 => //= x s1 ->; rewrite catA.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 233 Number of failed tactic applications: 9768 Results for lemma has_pred1: x s : has (pred1 x) s = (x \in s) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -(eq_has (mem_seq1^~ x)) (has_sym [:: x]) /= orbF.] Proof search time: 0 min, 35 sec Number of successful tactic applications: 408 Number of failed tactic applications: 9593 Results for lemma in_cons: y s x : (x \in y :: s) = (x == y) || (x \in s) SUCCESS! Proof Found in EFSM: elim : s => // x s IHs. Tactics applied: 6 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 1 Number of failed tactic applications: 5 Results for lemma ltn_size_undup: s : (size (undup s) < size s) = ~~ uniq s FAILURE! Tactics applied: 10000 Original Proof: [by elim: s => //= x s IHs; case Hx: (x \in s); rewrite //= ltnS size_undup.] Proof search time: 0 min, 27 sec Number of successful tactic applications: 588 Number of failed tactic applications: 9413 Results for lemma size_behead: s : size (behead s) = (size s).-1 SUCCESS! Proof Found in EFSM: elim : s => // x s IHs. Tactics applied: 6 Original Proof: [by case: s.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 1 Number of failed tactic applications: 5 Results for lemma last_map: s x : last (f x) (map s) = f (last x s) SUCCESS! Proof Found in EFSM: by elim: s x => //= y s IHs x; Tactics applied: 178 Original Proof: [by elim: s x => /=.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 5 Number of failed tactic applications: 173 Results for lemma catrevE: s t : catrev s t = rev s ++ t FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -catrev_catr.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 290 Number of failed tactic applications: 9711 Results for lemma mapP: s y : reflect (exists2 x, x \in s & y = f x) (y \in map f s) FAILURE! Tactics applied: 1304 Original Proof: [elim: s => [|x s IHs]; first by right; case. rewrite /= in_cons eq_sym; case Hxy: (f x == y). by left; exists x; [rewrite mem_head | rewrite (eqP Hxy)]. apply: (iffP IHs) => [[x' Hx' ->]|[x' Hx' Dy]]. by exists x'; first exact: predU1r. by move: Dy Hxy => ->; case/predU1P: Hx' => [->|]; [rewrite eqxx | exists x'].] Proof search time: 0 min, 3 sec Number of successful tactic applications: 13 Number of failed tactic applications: 1291 Results for lemma all_predI: a1 a2 s : all (predI a1 a2) s = all a1 s && all a2 s FAILURE! Tactics applied: 10000 Original Proof: [apply: (can_inj negbK); rewrite negb_and -!has_predC -has_predU. by apply: eq_has => x; rewrite /= negb_and.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 817 Number of failed tactic applications: 9184 Results for lemma allpairsP: R (f : S -> T -> R) s t z : reflect (exists p, [/\ p.1 \in s, p.2 \in t & z = f p.1 p.2]) (z \in allpairs f s t) FAILURE! Tactics applied: 1286 Original Proof: [elim: s => [|x s IHs /=]; first by right=> [[p []]]. rewrite mem_cat; have [fxt_z | not_fxt_z] := altP mapP. by left; have [y t_y ->] := fxt_z; exists (x, y); rewrite mem_head. apply: (iffP IHs) => [] [[x' y] /= [s_x' t_y def_z]]; exists (x', y). by rewrite !inE predU1r. by have [def_x' | //] := predU1P s_x'; rewrite def_z def_x' map_f in not_fxt_z.] Proof search time: 0 min, 3 sec Number of successful tactic applications: 13 Number of failed tactic applications: 1273 Results for lemma sumn_cat: s1 s2 : sumn (s1 ++ s2) = sumn s1 + sumn s2 FAILURE! Tactics applied: 10000 Original Proof: [by elim: s1 => //= x s1 ->; rewrite addnA.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 991 Number of failed tactic applications: 9010 Results for lemma perm_rcons: x s : perm_eql (rcons s x) (x :: s) FAILURE! Tactics applied: 10000 Original Proof: [by move=> /= s2; rewrite -cats1 perm_catC.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 548 Number of failed tactic applications: 9453 Results for lemma nthP: (T : eqType) (s : seq T) x x0 : reflect (exists2 i, i < size s & nth x0 s i = x) (x \in s) FAILURE! Tactics applied: 326 Original Proof: [apply: (iffP idP) => [|[n Hn <-]]; last by apply mem_nth. by exists (index x s); [rewrite index_mem | apply nth_index].] Proof search time: 0 min, 1 sec Number of successful tactic applications: 1 Number of failed tactic applications: 325 Results for lemma undup_uniq: s : uniq (undup s) FAILURE! Tactics applied: 10000 Original Proof: [by elim: s => //= x s IHs; case s_x: (x \in s); rewrite //= mem_undup s_x.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 748 Number of failed tactic applications: 9253 Results for lemma nth_incr_nth: v i j : nth 0 (incr_nth v i) j = (i == j) + nth 0 v j FAILURE! Tactics applied: 10000 Original Proof: [elim: v i j => [|n v IHv] [|i] [|j] //=; rewrite ?eqSS ?addn0 //; try by case j. elim: i j => [|i IHv] [|j] //=; rewrite ?eqSS //; by case j.] Proof search time: 0 min, 27 sec Number of successful tactic applications: 650 Number of failed tactic applications: 9351 Results for lemma sub1seq: x s : subseq [:: x] s = (x \in s) FAILURE! Tactics applied: 10000 Original Proof: [by elim: s => //= y s; rewrite inE; case: (x == y); rewrite ?sub0seq.] Proof search time: 0 min, 31 sec Number of successful tactic applications: 371 Number of failed tactic applications: 9630 Results for lemma belast_map: s x : belast (f x) (map s) = map (belast x s) FAILURE! Tactics applied: 10000 Original Proof: [by elim: s x => //= y s IHs x; rewrite IHs.] Proof search time: 0 min, 41 sec Number of successful tactic applications: 816 Number of failed tactic applications: 9185 Results for lemma eqseq_cons: x1 x2 s1 s2 : (x1 :: s1 == x2 :: s2) = (x1 == x2) && (s1 == s2) SUCCESS! Proof Found in EFSM: elim : s1 n0 => [|x s1 IHs] [|n] //=. Tactics applied: 28 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 1 Number of failed tactic applications: 27 Results for lemma mem_seq3: x y1 y2 y3 : (x \in [:: y1; y2; y3]) = xpred3 y1 y2 y3 x SUCCESS! Proof Found in EFSM: by rewrite !inE. Tactics applied: 241 Original Proof: [by rewrite !inE.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 4 Number of failed tactic applications: 237 Results for lemma filter_pred1_uniq: s x : uniq s -> x \in s -> filter (pred1 x) s = [:: x] FAILURE! Tactics applied: 10000 Original Proof: [move=> uniq_s s_x; rewrite (all_pred1P _ _ (filter_all _ _)). by rewrite -count_filter count_uniq_mem ?s_x.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 255 Number of failed tactic applications: 9746 Results for lemma all_pred1_nseq: x y n : all (pred1 x) (nseq n y) = (n == 0) || (x == y) FAILURE! Tactics applied: 10000 Original Proof: [case: n => //= n; rewrite eq_sym; apply: andb_idr => /eqP->{x}. by elim: n => //= n ->; rewrite eqxx.] Proof search time: 0 min, 34 sec Number of successful tactic applications: 742 Number of failed tactic applications: 9259 Results for lemma map_of_seq: (T1 : eqType) T2 (s : seq T1) (fs : seq T2) (y0 : T2) : {f | uniq s -> size fs = size s -> map f s = fs} FAILURE! Tactics applied: 1286 Original Proof: [exists (fun x => nth y0 fs (index x s)) => uAs eq_sz. apply/esym/(@eq_from_nth _ y0); rewrite ?size_map eq_sz // => i ltis. have x0 : T1 by [case: (s) ltis]; by rewrite (nth_map x0) // index_uniq.] Proof search time: 0 min, 3 sec Number of successful tactic applications: 12 Number of failed tactic applications: 1274 Results for lemma mem_mask_cons: x b m y s : (x \in mask (b :: m) (y :: s)) = b && (x == y) || (x \in mask m s) SUCCESS! Proof Found in EFSM: by case: b. Tactics applied: 110 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 5 Number of failed tactic applications: 105 Results for lemma mem_map: s x : (f x \in map f s) = (x \in s) FAILURE! Tactics applied: 10000 Original Proof: [by apply/mapP/idP=> [[y Hy /Hf->] //|]; exists x.] Proof search time: 0 min, 44 sec Number of successful tactic applications: 1132 Number of failed tactic applications: 8869 Results for lemma size_take: s : size (take n0 s) = if n0 < size s then n0 else size s FAILURE! Tactics applied: 10000 Original Proof: [have [le_sn | lt_ns] := leqP (size s) n0; first by rewrite take_oversize. by rewrite size_takel // ltnW.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 729 Number of failed tactic applications: 9272 Results for lemma subseq_uniq: s1 s2 : subseq s1 s2 -> uniq s2 -> uniq s1 FAILURE! Tactics applied: 10000 Original Proof: [by case/subseqP=> m _ -> Us2; exact: mask_uniq.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 1679 Number of failed tactic applications: 8322 Results for lemma perm_eq_trans: : transitive perm_eq FAILURE! Tactics applied: 10000 Original Proof: [move=> s2 s1 s3; move/perm_eqP=> eq12; move/perm_eqP=> eq23. by apply/perm_eqP=> a; rewrite eq12.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 941 Number of failed tactic applications: 9060 Results for lemma nth_scanl: s n : n < size s -> forall x, nth x1 (scanl x s) n = foldl g x (take n.+1 s) FAILURE! Tactics applied: 10000 Original Proof: [by elim: s n => [|y s IHs] [|n] Hn x //=; rewrite ?take0 ?IHs.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 258 Number of failed tactic applications: 9743 Results for lemma eqseqE: : eqseq = eq_op SUCCESS! Proof Found in EFSM: by []. Tactics applied: 97 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 1 Number of failed tactic applications: 96 Results for lemma rotr_rotr: m n s : rotr m (rotr n s) = rotr n (rotr m s) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite /rotr !size_rot rot_rot.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 725 Number of failed tactic applications: 9276 Results for lemma size_pmap: s : size (pmap s) = count [eta f] s SUCCESS! Proof Found in EFSM: apply /eqP; elim : s => //= x s IHs. rewrite -(cat0s s). case fx: (f x) => //= [u] <-; Tactics applied: 2403 Original Proof: [by elim: s => //= x s <-; case: (f _).] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 5 sec Number of successful tactic applications: 82 Number of failed tactic applications: 2321 Results for fold 2 Results for lemma has_seq1: x : has [:: x] = a x SUCCESS! Proof Found in EFSM: apply : (can_inj negbK); rewrite /= ?cats0. case : (a x) => //; Tactics applied: 3950 Original Proof: [exact: orbF.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 7 sec Number of successful tactic applications: 142 Number of failed tactic applications: 3808 Results for lemma prefix_subseq: s1 s2 : subseq s1 (s1 ++ s2) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -{1}[s1]cats0 cat_subseq ?sub0seq.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1288 Number of failed tactic applications: 8713 Results for lemma eq_in_find: s : {in s, a1 =1 a2} -> find a1 s = find a2 s FAILURE! Tactics applied: 10000 Original Proof: [elim: s => //= x s IHs eq_a12; rewrite eq_a12 ?mem_head // IHs // => y s'y. by rewrite eq_a12 // mem_behead.] Proof search time: 0 min, 36 sec Number of successful tactic applications: 2636 Number of failed tactic applications: 7365 Results for lemma map_cons: x s : map (x :: s) = f x :: map s SUCCESS! Proof Found in EFSM: elim : s => // y s IHs; Tactics applied: 9 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 8 Results for lemma count_size: s : count s <= size s FAILURE! Tactics applied: 10000 Original Proof: [by elim: s => //= x s; case: (a x); last exact: leqW.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 2385 Number of failed tactic applications: 7616 Results for lemma uniq_size_uniq: s1 s2 : uniq s1 -> s1 =i s2 -> uniq s2 = (size s2 == size s1) FAILURE! Tactics applied: 10000 Original Proof: [move=> Us1 eqs12; apply/idP/idP=> [Us2 | /eqP eq_sz12]. by rewrite eqn_leq !uniq_leq_size // => y; rewrite eqs12. by apply: (leq_size_uniq Us1) => [y|]; rewrite (eqs12, eq_sz12).] Proof search time: 0 min, 25 sec Number of successful tactic applications: 1263 Number of failed tactic applications: 8738 Results for lemma mem_iota: m n i : (i \in iota m n) = (m <= i) && (i < m + n) FAILURE! Tactics applied: 10000 Original Proof: [elim: n m => [|n IHn] /= m; first by rewrite addn0 ltnNge andbN. rewrite -addSnnS leq_eqVlt in_cons eq_sym. by case: eqP => [->|_]; [rewrite leq_addr | exact: IHn].] Proof search time: 0 min, 16 sec Number of successful tactic applications: 259 Number of failed tactic applications: 9742 Results for lemma nth_pairmap: s n : n < size s -> forall x, nth x2 (pairmap x s) n = f (nth x1 (x :: s) n) (nth x1 s n) FAILURE! Tactics applied: 10000 Original Proof: [by elim: s n => [|y s IHs] [|n] //= Hn x; apply: IHs.] Proof search time: 0 min, 27 sec Number of successful tactic applications: 1694 Number of failed tactic applications: 8307 Results for lemma size_pairmap: x s : size (pairmap x s) = size s FAILURE! Tactics applied: 10000 Original Proof: [by elim: s x => //= y s IHs x; rewrite IHs.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 2585 Number of failed tactic applications: 7416 Results for lemma eq_from_nth: s1 s2 : size s1 = size s2 -> (forall i, i < size s1 -> nth s1 i = nth s2 i) -> s1 = s2 FAILURE! Tactics applied: 10000 Original Proof: [elim: s1 s2 => [|x1 s1 IHs1] [|x2 s2] //= [eq_sz] eq_s12. rewrite [x1](eq_s12 0) // (IHs1 s2) // => i; exact: (eq_s12 i.+1).] Proof search time: 0 min, 19 sec Number of successful tactic applications: 1164 Number of failed tactic applications: 8837 Results for lemma all_predT: s : all predT s SUCCESS! Proof Found in EFSM: elim : s => // y s IHs; Tactics applied: 9 Original Proof: [by rewrite all_count count_predT.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 8 Results for lemma catA: s1 s2 s3 : s1 ++ s2 ++ s3 = (s1 ++ s2) ++ s3 SUCCESS! Proof Found in EFSM: by elim: s1 => //= x s1 ->. Tactics applied: 169 Original Proof: [by elim: s1 => //= x s1 ->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 8 Number of failed tactic applications: 161 Results for lemma filter_subseq: a s : subseq (filter a s) s FAILURE! Tactics applied: 10000 Original Proof: [by apply/subseqP; exists (map a s); rewrite ?size_map ?filter_mask.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 2061 Number of failed tactic applications: 7940 Results for lemma perm_rot: n s : perm_eql (rot n s) s FAILURE! Tactics applied: 10000 Original Proof: [by move=> /= s2; rewrite perm_catC cat_take_drop.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 2698 Number of failed tactic applications: 7303 Results for lemma mem_seq2: x y1 y2 : (x \in [:: y1; y2]) = xpred2 y1 y2 x SUCCESS! Proof Found in EFSM: by rewrite !inE. Tactics applied: 237 Original Proof: [by rewrite !inE.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 234 Results for lemma foldr_map: s : foldr f z0 (map h s) = foldr (fun x z => f (h x) z) z0 s SUCCESS! Proof Found in EFSM: by elim: s => //= x s ->. Tactics applied: 128 Original Proof: [by elim: s => //= x s ->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 11 Number of failed tactic applications: 117 Results for lemma undup_id: s : uniq s -> undup s = s FAILURE! Tactics applied: 10000 Original Proof: [by elim: s => //= x s IHs /andP[/negbTE-> /IHs->].] Proof search time: 0 min, 31 sec Number of successful tactic applications: 2319 Number of failed tactic applications: 7682 Results for lemma nth0: s : nth s 0 = head s SUCCESS! Proof Found in EFSM: elim : s => // y s IHs; Tactics applied: 9 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 8 Results for lemma perm_eq_small: s1 s2 : size s2 <= 1 -> perm_eq s1 s2 -> s1 = s2 FAILURE! Tactics applied: 10000 Original Proof: [move=> s2_le1 eqs12; move/perm_eq_size: eqs12 s2_le1 (perm_eq_mem eqs12). by case: s2 s1 => [|x []] // [|y []] // _ _ /(_ x); rewrite !inE eqxx => /eqP->.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 1247 Number of failed tactic applications: 8754 Results for lemma eq_mkseq: f g : f =1 g -> mkseq f =1 mkseq g FAILURE! Tactics applied: 10000 Original Proof: [by move=> Efg n; exact: eq_map Efg _.] Proof search time: 0 min, 12 sec Number of successful tactic applications: 128 Number of failed tactic applications: 9873 Results for lemma mem_drop: s x : x \in drop n0 s -> x \in s FAILURE! Tactics applied: 10000 Original Proof: [by move=> s0'x; rewrite -(cat_take_drop n0 s) mem_cat /= s0'x orbT.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 1432 Number of failed tactic applications: 8569 Results for lemma pmap_filter: s : map g (pmap s) = filter [eta f] s FAILURE! Tactics applied: 10000 Original Proof: [by elim: s => //= x s <-; rewrite -{3}(fK x); case: (f _).] Proof search time: 0 min, 30 sec Number of successful tactic applications: 3454 Number of failed tactic applications: 6547 Results for lemma mem_rem_uniq: s : uniq s -> rem s =i [predD1 s & x] FAILURE! Tactics applied: 10000 Original Proof: [by move/rem_filter=> -> y; rewrite mem_filter.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 713 Number of failed tactic applications: 9288 Results for lemma last_cons: x y s : last x (y :: s) = last y s SUCCESS! Proof Found in EFSM: elim : s => // y s IHs; Tactics applied: 9 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 8 Results for lemma foldr_cat: s1 s2 : foldr f z0 (s1 ++ s2) = foldr f (foldr f z0 s2) s1 SUCCESS! Proof Found in EFSM: by elim: s1 => //= x s1 ->. Tactics applied: 169 Original Proof: [by elim: s1 => //= x s1 ->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 8 Number of failed tactic applications: 161 Results for lemma has_nthP: (a : pred T) s x0 : reflect (exists2 i, i < size s & a (nth x0 s i)) (has a s) FAILURE! Tactics applied: 10000 Original Proof: [elim: s => [|x s IHs] /=; first by right; case. case nax: (a x); first by left; exists 0. by apply: (iffP IHs) => [[i]|[[|i]]]; [exists i.+1 | rewrite nax | exists i].] Proof search time: 0 min, 22 sec Number of successful tactic applications: 2268 Number of failed tactic applications: 7733 Results for lemma count_pred0: s : count pred0 s = 0 SUCCESS! Proof Found in EFSM: elim : s => // y s IHs; Tactics applied: 9 Original Proof: [by rewrite count_filter filter_pred0.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 8 Results for lemma nth_zip_cond: p s t i : nth p (zip s t) i = (if i < size (zip s t) then (nth p.1 s i, nth p.2 t i) else p) FAILURE! Tactics applied: 10000 Original Proof: [rewrite size_zip ltnNge geq_min. by elim: s t i => [|x s IHs] [|y t] [|i] //=; rewrite ?orbT -?IHs.] Proof search time: 0 min, 28 sec Number of successful tactic applications: 2835 Number of failed tactic applications: 7166 Results for lemma has_map: a s : has a (map s) = has (preim f a) s SUCCESS! Proof Found in EFSM: by elim: s => //= x s ->. Tactics applied: 128 Original Proof: [by elim: s => //= x s ->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 13 Number of failed tactic applications: 115 Results for lemma rev_uniq: s : uniq (rev s) = uniq s FAILURE! Tactics applied: 10000 Original Proof: [elim: s => // x s IHs. by rewrite rev_cons -cats1 cat_uniq /= andbT andbC mem_rev orbF IHs.] Proof search time: 0 min, 32 sec Number of successful tactic applications: 2365 Number of failed tactic applications: 7636 Results for lemma mem_pmap_sub: s u : (u \in pmap insT s) = (val u \in s) FAILURE! Tactics applied: 10000 Original Proof: [apply: (can2_mem_pmap (insubK _)); exact: valK.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 2039 Number of failed tactic applications: 7962 Results for lemma cat_rcons: x s1 s2 : rcons s1 x ++ s2 = s1 ++ x :: s2 FAILURE! Tactics applied: 316 Original Proof: [by rewrite -cats1 -catA.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 316 Results for lemma mask_cons: b m x s : mask (b :: m) (x :: s) = nseq b x ++ mask m s SUCCESS! Proof Found in EFSM: by case: b. Tactics applied: 105 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 100 Results for lemma sumn_nseq: x n : sumn (nseq n x) = x * n FAILURE! Tactics applied: 955 Original Proof: [by rewrite mulnC; elim: n => //= n ->.] Proof search time: 0 min, 2 sec Number of successful tactic applications: 3 Number of failed tactic applications: 952 Results for lemma set_set_nth: s n1 y1 n2 y2 (s2 := set_nth s n2 y2) : set_nth (set_nth s n1 y1) n2 y2 = if n1 == n2 then s2 else set_nth s2 n1 y1 FAILURE! Tactics applied: 10000 Original Proof: [have [-> | ne_n12] := altP eqP. apply: eq_from_nth => [|i _]; first by rewrite !size_set_nth maxnA maxnn. by do 2!rewrite !nth_set_nth /=; case: eqP. apply: eq_from_nth => [|i _]; first by rewrite !size_set_nth maxnCA. do 2!rewrite !nth_set_nth /=; case: eqP => // ->. by rewrite eq_sym -if_neg ne_n12.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 2223 Number of failed tactic applications: 7778 Results for lemma cat_take_drop: s : take n0 s ++ drop n0 s = s FAILURE! Tactics applied: 10000 Original Proof: [by elim: s n0 => [|x s IHs] [|n]; try exact (congr1 _ (IHs n)).] Proof search time: 0 min, 28 sec Number of successful tactic applications: 3653 Number of failed tactic applications: 6348 Results for lemma unzip1_zip: s t : size s <= size t -> unzip1 (zip s t) = s FAILURE! Tactics applied: 10000 Original Proof: [by elim: s t => [|x s IHs] [|y t] //= le_s_t; rewrite IHs.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 1094 Number of failed tactic applications: 8907 Results for lemma map_drop: s : map (drop n0 s) = drop n0 (map s) SUCCESS! Proof Found in EFSM: by elim: n0 s => [|n IHn] [|x s] //=; Tactics applied: 125 Original Proof: [by elim: n0 s => [|n IHn] [|x s] //=; rewrite IHn.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 13 Number of failed tactic applications: 112 Results for lemma rev_rcons: s x : rev (rcons s x) = x :: rev s FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -cats1 rev_cat.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 2583 Number of failed tactic applications: 7418 Results for lemma take_oversize: n s : size s <= n -> take n s = s FAILURE! Tactics applied: 10000 Original Proof: [by elim: n s => [|n IHn] [|x s] Hsn; try (congr cons; apply: IHn).] Proof search time: 0 min, 21 sec Number of successful tactic applications: 1945 Number of failed tactic applications: 8056 Results for lemma size_incr_nth: v i : size (incr_nth v i) = if i < size v then size v else i.+1 FAILURE! Tactics applied: 316 Original Proof: [elim: v i => [|n v IHv] [|i] //=; first by rewrite size_ncons /= addn1. rewrite IHv; exact: fun_if.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 316 Results for lemma last_ind: P : P [::] -> (forall s x, P s -> P (rcons s x)) -> forall s, P s FAILURE! Tactics applied: 10000 Original Proof: [move=> Hnil Hlast s; rewrite -(cat0s s). elim: s [::] Hnil => [|x s2 IHs] s1 Hs1; first by rewrite cats0. by rewrite -cat_rcons; auto.] Proof search time: 0 min, 10 sec Number of successful tactic applications: 162 Number of failed tactic applications: 9839 Results for lemma eqseqP: : Equality.axiom eqseq FAILURE! Tactics applied: 10000 Original Proof: [move; elim=> [|x1 s1 IHs] [|x2 s2]; do [by constructor | simpl]. case: (x1 =P x2) => [<-|neqx]; last by right; case. by apply: (iffP (IHs s2)) => [<-|[]].] Proof search time: 0 min, 10 sec Number of successful tactic applications: 119 Number of failed tactic applications: 9882 Results for lemma cat_cons: x s1 s2 : (x :: s1) ++ s2 = x :: s1 ++ s2 SUCCESS! Proof Found in EFSM: by []. Tactics applied: 80 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 79 Results for lemma index_map: s x : index (f x) (map f s) = index x s FAILURE! Tactics applied: 10000 Original Proof: [by rewrite /index; elim: s => //= y s IHs; rewrite (inj_eq Hf) IHs.] Proof search time: 0 min, 31 sec Number of successful tactic applications: 2995 Number of failed tactic applications: 7006 Results for lemma map_f: s x : x \in s -> f x \in map f s FAILURE! Tactics applied: 10000 Original Proof: [elim: s => [|y s IHs] //=. by case/predU1P=> [->|Hx]; [exact: predU1l | apply: predU1r; auto].] Proof search time: 0 min, 24 sec Number of successful tactic applications: 1477 Number of failed tactic applications: 8524 Results for lemma eq_in_filter: s : {in s, a1 =1 a2} -> filter a1 s = filter a2 s FAILURE! Tactics applied: 10000 Original Proof: [elim: s => //= x s IHs eq_a. rewrite eq_a ?mem_head ?IHs // => y s_y; apply: eq_a; exact: mem_behead.] Proof search time: 0 min, 37 sec Number of successful tactic applications: 2636 Number of failed tactic applications: 7365 Results for lemma takel_cat: s1 : n0 <= size s1 -> forall s2, take n0 (s1 ++ s2) = take n0 s1 FAILURE! Tactics applied: 10000 Original Proof: [move=> Hn0 s2; rewrite take_cat ltn_neqAle Hn0 andbT. by case: (n0 =P size s1) => //= ->; rewrite subnn take0 cats0 take_size.] Proof search time: 0 min, 12 sec Number of successful tactic applications: 473 Number of failed tactic applications: 9528 Results for lemma filter_uniq: s a : uniq s -> uniq (filter a s) FAILURE! Tactics applied: 10000 Original Proof: [elim: s => [|x s IHs] //= /andP[Hx Hs]; case (a x); auto. by rewrite /= mem_filter /= (negbTE Hx) andbF; auto.] Proof search time: 0 min, 35 sec Number of successful tactic applications: 2732 Number of failed tactic applications: 7269 Results for lemma cat1s: x s : [:: x] ++ s = x :: s SUCCESS! Proof Found in EFSM: elim : s => // y s IHs; Tactics applied: 9 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 8 Results for lemma count_uniq_mem: s x : uniq s -> count (pred1 x) s = (x \in s) FAILURE! Tactics applied: 10000 Original Proof: [elim: s => //= [y s IHs] /andP[/negbTE Hy /IHs-> {IHs}]. by rewrite in_cons eq_sym; case: eqP => // ->; rewrite Hy.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 1357 Number of failed tactic applications: 8644 Results for lemma size_eq0: s : (size s == 0) = (s == [::]) SUCCESS! Proof Found in EFSM: elim : s => // y s IHs; Tactics applied: 9 Original Proof: [apply/eqP/eqP=> [|-> //]; exact: size0nil.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 8 Results for lemma nilP: s : reflect (s = [::]) (nilp s) SUCCESS! Proof Found in EFSM: apply : (iffP idP) => [|->]; elim : s => // x s IHs; Tactics applied: 656 Original Proof: [by case: s => [|x s]; constructor.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 sec Number of successful tactic applications: 54 Number of failed tactic applications: 602 Results for lemma take_cat: s1 s2 : take n0 (s1 ++ s2) = if n0 < size s1 then take n0 s1 else s1 ++ take (n0 - size s1) s2 FAILURE! Tactics applied: 10000 Original Proof: [elim: s1 n0 => [|x s1 IHs] [|n] //=. by rewrite ltnS subSS -(fun_if (cons x)) -IHs.] Proof search time: 0 min, 31 sec Number of successful tactic applications: 2892 Number of failed tactic applications: 7109 Results for lemma constant_nseq: n x : constant (nseq n x) FAILURE! Tactics applied: 10000 Original Proof: [by case: n => //= n; rewrite all_pred1_nseq eqxx orbT.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 227 Number of failed tactic applications: 9774 Results for lemma drop_size_cat: n s1 s2 : size s1 = n -> drop n (s1 ++ s2) = s2 FAILURE! Tactics applied: 10000 Original Proof: [by move <-; elim: s1 => //=; rewrite drop0.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 1133 Number of failed tactic applications: 8868 Results for lemma mem_rot: s : rot n0 s =i s FAILURE! Tactics applied: 10000 Original Proof: [by move=> x; rewrite -{2}(cat_take_drop n0 s) !mem_cat /= orbC.] Proof search time: 0 min, 33 sec Number of successful tactic applications: 2739 Number of failed tactic applications: 7262 Results for lemma zip_unzip: s : zip (unzip1 s) (unzip2 s) = s FAILURE! Tactics applied: 10000 Original Proof: [by elim: s => [|[x y] s /= ->].] Proof search time: 0 min, 27 sec Number of successful tactic applications: 3432 Number of failed tactic applications: 6569 Results for lemma eq_all: a1 a2 : a1 =1 a2 -> all a1 =1 all a2 FAILURE! Tactics applied: 10000 Original Proof: [by move=> Ea s; rewrite !all_count (eq_count Ea).] Proof search time: 0 min, 11 sec Number of successful tactic applications: 202 Number of failed tactic applications: 9799 Results for lemma all_pred1_constant: x s : all (pred1 x) s -> constant s FAILURE! Tactics applied: 10000 Original Proof: [by case: s => //= y s /andP[/eqP->].] Proof search time: 0 min, 26 sec Number of successful tactic applications: 1439 Number of failed tactic applications: 8562 Results for lemma eq_map: (f1 f2 : T1 -> T2) : f1 =1 f2 -> map f1 =1 map f2 FAILURE! Tactics applied: 10000 Original Proof: [by move=> Ef; elim=> //= x s ->; rewrite Ef.] Proof search time: 0 min, 12 sec Number of successful tactic applications: 146 Number of failed tactic applications: 9855 Results for lemma map_nseq: x : map (nseq n0 x) = nseq n0 (f x) FAILURE! Tactics applied: 316 Original Proof: [by elim: n0 => // *; congr (_ :: _).] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 316 Results for lemma mask0: m : mask m [::] = [::] FAILURE! Tactics applied: 316 Original Proof: [by case: m.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 316 Results for lemma all_nthP: (a : pred T) s x0 : reflect (forall i, i < size s -> a (nth x0 s i)) (all a s) FAILURE! Tactics applied: 10000 Original Proof: [rewrite -(eq_all (fun x => negbK (a x))) all_predC. case: (has_nthP _ _ x0) => [na_s | a_s]; [right=> a_s | left=> i lti]. by case: na_s => i lti; rewrite a_s. by apply/idPn=> na_si; case: a_s; exists i.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 2608 Number of failed tactic applications: 7393 Results for lemma size_set_nth: s n y : size (set_nth s n y) = maxn n.+1 (size s) FAILURE! Tactics applied: 10000 Original Proof: [elim: s n => [|x s IHs] [|n] //=. - by rewrite size_ncons addn1 maxn0. - by rewrite maxnE subn1. by rewrite IHs -add1n addn_maxr.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 2861 Number of failed tactic applications: 7140 Results for lemma pmapS_filter: s : map some (pmap s) = map f (filter [eta f] s) FAILURE! Tactics applied: 10000 Original Proof: [by elim: s => //= x s; case fx: (f x) => //= [u] <-; congr (_ :: _).] Proof search time: 0 min, 30 sec Number of successful tactic applications: 3430 Number of failed tactic applications: 6571 Results for lemma perm_eq_size: s1 s2 : perm_eq s1 s2 -> size s1 = size s2 FAILURE! Tactics applied: 10000 Original Proof: [by move/perm_eqP=> eq12; rewrite -!count_predT eq12.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1180 Number of failed tactic applications: 8821 Results for lemma set_nth_default: T s (y0 x0 : T) n : n < size s -> nth x0 s n = nth y0 s n FAILURE! Tactics applied: 10000 Original Proof: [by elim: s n => [|y s' IHs] [|n] /=; auto.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 2202 Number of failed tactic applications: 7799 Results for lemma count_filter: s : count s = size (filter s) FAILURE! Tactics applied: 10000 Original Proof: [by elim: s => //= x s ->; case (a x).] Proof search time: 0 min, 29 sec Number of successful tactic applications: 3676 Number of failed tactic applications: 6325 Results for lemma has_mask: a m s : has a (mask m s) -> has a s FAILURE! Tactics applied: 10000 Original Proof: [elim: m s => [|b m IHm] [|x s] //; rewrite has_mask_cons /= andbC. by case: (a x) => //= /IHm.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1601 Number of failed tactic applications: 8400 Results for lemma count_predT: s : count predT s = size s SUCCESS! Proof Found in EFSM: elim : s => // y s IHs; Tactics applied: 9 Original Proof: [by rewrite count_filter filter_predT.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 8 Results for lemma rotK: : cancel (rot n0) (rotr n0) FAILURE! Tactics applied: 10000 Original Proof: [move=> s; rewrite /rotr size_rot -size_drop {2}/rot. by rewrite rot_size_cat cat_take_drop.] Proof search time: 0 min, 10 sec Number of successful tactic applications: 167 Number of failed tactic applications: 9834 Results for lemma iota_add: m n1 n2 : iota m (n1 + n2) = iota m n1 ++ iota (m + n1) n2 FAILURE! Tactics applied: 316 Original Proof: [by elim: n1 m => //= [|n1 IHn1] m; rewrite ?addn0 // -addSnnS -IHn1.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 316 Results for lemma filter_cat: s1 s2 : filter (s1 ++ s2) = filter s1 ++ filter s2 FAILURE! Tactics applied: 10000 Original Proof: [by elim: s1 => //= x s1 ->; case (a x).] Proof search time: 0 min, 27 sec Number of successful tactic applications: 3047 Number of failed tactic applications: 6954 Results for lemma find_map: a s : find a (map s) = find (preim f a) s SUCCESS! Proof Found in EFSM: by elim: s => //= x s ->. Tactics applied: 128 Original Proof: [by elim: s => //= x s ->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 13 Number of failed tactic applications: 115 Results for lemma perm_uniq: s1 s2 : s1 =i s2 -> size s1 = size s2 -> uniq s1 = uniq s2 FAILURE! Tactics applied: 10000 Original Proof: [by move=> Es12 Hs12; apply/idP/idP => Us; rewrite (uniq_size_uniq Us) ?Hs12 ?eqxx.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 1207 Number of failed tactic applications: 8794 Results for lemma last_nth: x s : last x s = nth (x :: s) (size s) SUCCESS! Proof Found in EFSM: by elim: s x => //= y s IHs x; Tactics applied: 164 Original Proof: [by elim: s x => [|y s IHs] x /=.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 7 Number of failed tactic applications: 157 Results for lemma perm_catC: s1 s2 : perm_eql (s1 ++ s2) (s2 ++ s1) FAILURE! Tactics applied: 10000 Original Proof: [by apply/perm_eqlP; apply/perm_eqP=> a; rewrite !count_cat addnC.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 1276 Number of failed tactic applications: 8725 Results for lemma take0: s : take 0 s = [::] SUCCESS! Proof Found in EFSM: elim : s => // y s IHs; Tactics applied: 9 Original Proof: [by case: s.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 8 Results for lemma rcons_uniq: s x : uniq (rcons s x) = (x \notin s) && uniq s FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -cats1 uniq_catC.] Proof search time: 0 min, 28 sec Number of successful tactic applications: 1445 Number of failed tactic applications: 8556 Results for lemma size_allpairs: s t : size (allpairs s t) = size s * size t FAILURE! Tactics applied: 10000 Original Proof: [by elim: s => //= x s IHs; rewrite size_cat size_map IHs.] Proof search time: 0 min, 30 sec Number of successful tactic applications: 3441 Number of failed tactic applications: 6560 Results for lemma nth_take: i : i < n0 -> forall s, nth (take n0 s) i = nth s i FAILURE! Tactics applied: 10000 Original Proof: [move=> lt_i_n0 s; case lt_n0_s: (n0 < size s). by rewrite -{2}[s]cat_take_drop nth_cat size_take lt_n0_s /= lt_i_n0. by rewrite -{1}[s]cats0 take_cat lt_n0_s /= cats0.] Proof search time: 0 min, 10 sec Number of successful tactic applications: 141 Number of failed tactic applications: 9860 Results for lemma nth_last: s : nth s (size s).-1 = last x0 s FAILURE! Tactics applied: 10000 Original Proof: [by case: s => //= x s; rewrite last_nth.] Proof search time: 0 min, 27 sec Number of successful tactic applications: 3677 Number of failed tactic applications: 6324 Results for lemma perm_eqlE: s1 s2 : perm_eql s1 s2 -> perm_eq s1 s2 FAILURE! Tactics applied: 10000 Original Proof: [by move->.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 1267 Number of failed tactic applications: 8734 Results for lemma revK: : involutive (@rev T) FAILURE! Tactics applied: 10000 Original Proof: [by elim=> //= x s IHs; rewrite rev_cons rev_rcons IHs.] Proof search time: 0 min, 10 sec Number of successful tactic applications: 136 Number of failed tactic applications: 9865 Results for lemma perm_map: s t : perm_eq s t -> perm_eq (map f s) (map f t) FAILURE! Tactics applied: 10000 Original Proof: [by move/perm_eqP=> Est; apply/perm_eqP=> a; rewrite !count_map Est.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 1631 Number of failed tactic applications: 8370 Results for lemma cons_uniq: x s : uniq (x :: s) = (x \notin s) && uniq s SUCCESS! Proof Found in EFSM: elim : s => // y s IHs; Tactics applied: 9 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 8 Results for lemma size1_zip: s t : size s <= size t -> size (zip s t) = size s FAILURE! Tactics applied: 10000 Original Proof: [by elim: s t => [|x s IHs] [|y t] //= Hs; rewrite IHs.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 1123 Number of failed tactic applications: 8878 Results for lemma pairmap_cat: x s1 s2 : pairmap x (s1 ++ s2) = pairmap x s1 ++ pairmap (last x s1) s2 FAILURE! Tactics applied: 316 Original Proof: [by elim: s1 x => //= y s1 IHs1 x; rewrite IHs1.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 0 Number of failed tactic applications: 316 Results for lemma subseq_uniqP: s1 s2 : uniq s2 -> reflect (s1 = filter (mem s1) s2) (subseq s1 s2) FAILURE! Tactics applied: 10000 Original Proof: [move=> uniq_s2; apply: (iffP idP) => [ss12 | ->]; last exact: filter_subseq. apply/eqP; rewrite -size_subseq_leqif ?subseq_filter ?(introT allP) //. apply/eqP/esym/perm_eq_size. rewrite uniq_perm_eq ?filter_uniq ?(subseq_uniq ss12) // => x. by rewrite mem_filter; apply: andb_idr; exact: (mem_subseq ss12).] Proof search time: 0 min, 22 sec Number of successful tactic applications: 1155 Number of failed tactic applications: 8846 Results for lemma rotS: n s : n < size s -> rot n.+1 s = rot 1 (rot n s) FAILURE! Tactics applied: 10000 Original Proof: [exact: (@rot_addn 1).] Proof search time: 0 min, 24 sec Number of successful tactic applications: 2258 Number of failed tactic applications: 7743 Results for lemma filter_predI: a1 a2 s : filter (predI a1 a2) s = filter a1 (filter a2 s) FAILURE! Tactics applied: 10000 Original Proof: [elim: s => //= x s IHs; rewrite andbC IHs. by case: (a2 x) => //=; case (a1 x).] Proof search time: 0 min, 31 sec Number of successful tactic applications: 3679 Number of failed tactic applications: 6322 Results for lemma nth_find: s : has s -> a (nth s (find s)) SUCCESS! Proof Found in EFSM: elim : s => //= x s IHs; try by exists s2. case : ifP => // /(contraFF (@s12 x))->. Tactics applied: 6924 Original Proof: [by elim: s => //= x s IHs; case Hx: (a x).] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 14 sec Number of successful tactic applications: 1251 Number of failed tactic applications: 5673 Results for lemma mem_seq1: x y : (x \in [:: y]) = (x == y) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite in_cons orbF.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 310 Number of failed tactic applications: 9691 Results for lemma mem_cat: x s1 s2 : (x \in s1 ++ s2) = (x \in s1) || (x \in s2) FAILURE! Tactics applied: 10000 Original Proof: [by elim: s1 => //= y s1 IHs; rewrite !inE /= -orbA -IHs.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 194 Number of failed tactic applications: 9807 Results for lemma index_mem: x s : (index x s < size s) = (x \in s) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -has_pred1 has_find.] Proof search time: 0 min, 28 sec Number of successful tactic applications: 1527 Number of failed tactic applications: 8474 Results for lemma eq_in_count: s : {in s, a1 =1 a2} -> count a1 s = count a2 s FAILURE! Tactics applied: 10000 Original Proof: [by move/eq_in_filter=> eq_a12; rewrite !count_filter eq_a12.] Proof search time: 0 min, 36 sec Number of successful tactic applications: 2636 Number of failed tactic applications: 7365 Results for lemma size_ncons: n x s : size (ncons n x s) = n + size s SUCCESS! Proof Found in EFSM: by elim: n => //= n ->. Tactics applied: 120 Original Proof: [by elim: n => //= n ->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 115 Results for lemma eq_in_all: s : {in s, a1 =1 a2} -> all a1 s = all a2 s FAILURE! Tactics applied: 10000 Original Proof: [by move=> eq_a12; rewrite !all_count eq_in_count.] Proof search time: 0 min, 36 sec Number of successful tactic applications: 2660 Number of failed tactic applications: 7341 Results for lemma drop_cat: s1 s2 : drop n0 (s1 ++ s2) = if n0 < size s1 then drop n0 s1 ++ s2 else drop (n0 - size s1) s2 FAILURE! Tactics applied: 10000 Original Proof: [by elim: s1 n0 => [|x s1 IHs] [|n]; try exact (IHs n).] Proof search time: 0 min, 32 sec Number of successful tactic applications: 2892 Number of failed tactic applications: 7109 Results for lemma mem_pmap: s u : (u \in pmap f s) = (Some u \in map f s) FAILURE! Tactics applied: 10000 Original Proof: [by elim: s => //= x s IHs; rewrite in_cons -IHs; case: (f x).] Proof search time: 0 min, 28 sec Number of successful tactic applications: 2065 Number of failed tactic applications: 7936 Results for lemma size_rev: s : size (rev s) = size s FAILURE! Tactics applied: 10000 Original Proof: [by elim: s => // x s IHs; rewrite rev_cons size_rcons IHs.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 3446 Number of failed tactic applications: 6555 Results for lemma rot_addn: m n s : m + n <= size s -> rot (m + n) s = rot m (rot n s) FAILURE! Tactics applied: 10000 Original Proof: [move=> sz_s; rewrite {1}/rot -[take _ s](cat_take_drop n). rewrite 5!(catA, =^~ rot_size_cat) !cat_take_drop. by rewrite size_drop !size_takel ?leq_addl ?addnK.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 2232 Number of failed tactic applications: 7769 Results for lemma perm_eqP: s1 s2 : reflect (count^~ s1 =1 count^~ s2) (perm_eq s1 s2) FAILURE! Tactics applied: 10000 Original Proof: [apply: (iffP allP) => [eq_cnt1 a | eq_cnt x _]; last exact/eqP. elim: {a}_.+1 {-2}a (ltnSn (count a (s1 ++ s2))) => // n IHn a le_an. case: (posnP (count a (s1 ++ s2))). by move/eqP; rewrite count_cat addn_eq0; do 2!case: eqP => // ->. rewrite -has_count => /hasP[x s12x a_x]; pose a' := predD1 a x. have cnt_a' s : count a s = count (pred1 x) s + count a' s. rewrite count_filter -(count_predC (pred1 x)) 2!count_filter. rewrite -!filter_predI -!count_filter; congr (_ + _). by apply: eq_count => y /=; case: eqP => // ->. rewrite !cnt_a' (eqnP (eq_cnt1 _ s12x)) (IHn a') // -ltnS. apply: leq_trans le_an. by rewrite ltnS cnt_a' -add1n leq_add2r -has_count has_pred1.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 2843 Number of failed tactic applications: 7158 Results for lemma size_takel: s : n0 <= size s -> size (take n0 s) = n0 FAILURE! Tactics applied: 10000 Original Proof: [by move/subnKC; rewrite -{2}(cat_take_drop s) size_cat size_drop => /addIn.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 1508 Number of failed tactic applications: 8493 Results for lemma size_rotr: s : size (rotr n0 s) = size s FAILURE! Tactics applied: 10000 Original Proof: [by rewrite size_rot.] Proof search time: 0 min, 28 sec Number of successful tactic applications: 3696 Number of failed tactic applications: 6305 Results for lemma rev_cat: s t : rev (s ++ t) = rev t ++ rev s FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -catrev_catr -catrev_catl.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 2833 Number of failed tactic applications: 7168 Results for lemma all_count: s : all s = (count s == size s) FAILURE! Tactics applied: 10000 Original Proof: [elim: s => //= x s; case: (a x) => _ //=. by rewrite add0n eqn_leq andbC ltnNge count_size.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 2438 Number of failed tactic applications: 7563 Results for lemma map_uniq: s : uniq (map f s) -> uniq s FAILURE! Tactics applied: 10000 Original Proof: [elim: s => //= x s IHs /andP[not_sfx /IHs->]; rewrite andbT. by apply: contra not_sfx => sx; apply/mapP; exists x.] Proof search time: 0 min, 28 sec Number of successful tactic applications: 2672 Number of failed tactic applications: 7329 Results for lemma uniq_leq_size: s1 s2 : uniq s1 -> {subset s1 <= s2} -> size s1 <= size s2 FAILURE! Tactics applied: 10000 Original Proof: [elim: s1 s2 => //= x s1 IHs s2 /andP[not_s1x Us1] /allP/=/andP[s2x /allP ss12]. have [i s3 def_s2] := rot_to s2x; rewrite -(size_rot i s2) def_s2. apply: IHs => // y s1y; have:= ss12 y s1y. by rewrite -(mem_rot i) def_s2 inE (negPf (memPn _ y s1y)).] Proof search time: 0 min, 22 sec Number of successful tactic applications: 1265 Number of failed tactic applications: 8736 Results for lemma iota_addl: m1 m2 n : iota (m1 + m2) n = map (addn m1) (iota m2 n) FAILURE! Tactics applied: 2233 Original Proof: [by elim: n m2 => //= n IHn m2; rewrite -addnS IHn.] Proof search time: 0 min, 5 sec Number of successful tactic applications: 9 Number of failed tactic applications: 2224 Results for lemma rotr_inj: : injective (@rotr T n0) FAILURE! Tactics applied: 10000 Original Proof: [exact (can_inj rotrK).] Proof search time: 0 min, 12 sec Number of successful tactic applications: 212 Number of failed tactic applications: 9789 Results for lemma count_mem_uniq: s : (forall x, count (pred1 x) s = (x \in s)) -> uniq s FAILURE! Tactics applied: 10000 Original Proof: [move=> count1_s; have Uus := undup_uniq s. suffices: perm_eq s (undup s) by move/perm_eq_uniq->. by apply/allP=> x _; apply/eqP; rewrite (count_uniq_mem x Uus) mem_undup.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 2322 Number of failed tactic applications: 7679 Results for lemma map_rev: s : map (rev s) = rev (map s) FAILURE! Tactics applied: 10000 Original Proof: [by elim: s => //= x s IHs; rewrite !rev_cons -!cats1 map_cat IHs.] Proof search time: 0 min, 31 sec Number of successful tactic applications: 3678 Number of failed tactic applications: 6323 Results for lemma catCA_perm_ind: P : (forall s1 s2 s3, P (s1 ++ s2 ++ s3) -> P (s2 ++ s1 ++ s3)) -> (forall s1 s2, perm_eq s1 s2 -> P s1 -> P s2) FAILURE! Tactics applied: 10000 Original Proof: [move=> PcatCA s1 s2 eq_s12; rewrite -[s1]cats0 -[s2]cats0. elim: s2 nil => [| x s2 IHs] s3 in s1 eq_s12 *. by case: s1 {eq_s12}(perm_eq_size eq_s12). have /rot_to[i s' def_s1]: x \in s1 by rewrite (perm_eq_mem eq_s12) mem_head. rewrite -(cat_take_drop i s1) -catA => /PcatCA. rewrite catA -/(rot i s1) def_s1 /= -cat1s => /PcatCA/IHs/PcatCA; apply. by rewrite -(perm_cons x) -def_s1 perm_rot.] Proof search time: 0 min, 12 sec Number of successful tactic applications: 194 Number of failed tactic applications: 9807 Results for lemma perm_cons: x s1 s2 : perm_eq (x :: s1) (x :: s2) = perm_eq s1 s2 FAILURE! Tactics applied: 10000 Original Proof: [exact: (perm_cat2l [::x]).] Proof search time: 0 min, 15 sec Number of successful tactic applications: 195 Number of failed tactic applications: 9806 Results for lemma mask_false: s n : mask (nseq n false) s = [::] SUCCESS! Proof Found in EFSM: by elim: s n => [|x s IHs] [|n] //= Hn; Tactics applied: 146 Original Proof: [by elim: s n => [|x s IHs] [|n] /=.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 9 Number of failed tactic applications: 137 Results for lemma count_map: a s : count a (map s) = count (preim f a) s SUCCESS! Proof Found in EFSM: by elim: s => //= x s ->. Tactics applied: 128 Original Proof: [by elim: s => //= x s ->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 13 Number of failed tactic applications: 115 Results for lemma behead_map: s : behead (map s) = map (behead s) SUCCESS! Proof Found in EFSM: elim : s => // y s IHs; Tactics applied: 9 Original Proof: [by case: s.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 8 Results for lemma perm_filterC: a s : perm_eql (filter a s ++ filter (predC a) s) s FAILURE! Tactics applied: 10000 Original Proof: [apply/perm_eqlP; elim: s => //= x s IHs. by case: (a x); last rewrite /= -cat1s perm_catCA; rewrite perm_cons.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 2390 Number of failed tactic applications: 7611 Results for lemma count_cat: s1 s2 : count (s1 ++ s2) = count s1 + count s2 FAILURE! Tactics applied: 10000 Original Proof: [by rewrite !count_filter filter_cat size_cat.] Proof search time: 0 min, 27 sec Number of successful tactic applications: 3065 Number of failed tactic applications: 6936 Results for lemma rem_subseq: s : subseq (rem s) s FAILURE! Tactics applied: 10000 Original Proof: [elim: s => //= y s IHs; rewrite eq_sym. by case: ifP => _; [exact: subseq_cons | rewrite eqxx].] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1099 Number of failed tactic applications: 8902 Results for lemma nth_drop: s i : nth (drop n0 s) i = nth s (n0 + i) FAILURE! Tactics applied: 10000 Original Proof: [have [lt_n0_s | le_s_n0] := ltnP n0 (size s). rewrite -{2}[s]cat_take_drop nth_cat size_take lt_n0_s /= addKn. by rewrite ltnNge leq_addr. rewrite !nth_default //; first exact: leq_trans (leq_addr _ _). by rewrite size_drop (eqnP le_s_n0).] Proof search time: 0 min, 24 sec Number of successful tactic applications: 3162 Number of failed tactic applications: 6839 Results for lemma rot1_cons: x s : rot 1 (x :: s) = rcons s x FAILURE! Tactics applied: 10000 Original Proof: [by rewrite /rot /= take0 drop0 -cats1.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 2960 Number of failed tactic applications: 7041 Results for lemma has_rcons: s x : has (rcons s x) = a x || has s FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -cats1 has_cat has_seq1 orbC.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1411 Number of failed tactic applications: 8590 Results for lemma map_inj_uniq: s : uniq (map f s) = uniq s FAILURE! Tactics applied: 10000 Original Proof: [apply: map_inj_in_uniq; exact: in2W.] Proof search time: 0 min, 28 sec Number of successful tactic applications: 2371 Number of failed tactic applications: 7630 Results for lemma has_cat: s1 s2 : has (s1 ++ s2) = has s1 || has s2 FAILURE! Tactics applied: 10000 Original Proof: [by elim: s1 => [|x s1 IHs] //=; rewrite IHs orbA.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 1703 Number of failed tactic applications: 8298 Results for lemma size_iota: m n : size (iota m n) = n FAILURE! Tactics applied: 10000 Original Proof: [by elim: n m => //= n IHn m; rewrite IHn.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 65 Number of failed tactic applications: 9936 Results for lemma lastP: s : last_spec s FAILURE! Tactics applied: 10000 Original Proof: [case: s => [|x s]; [left | rewrite lastI; right].] Proof search time: 0 min, 19 sec Number of successful tactic applications: 3316 Number of failed tactic applications: 6685 Results for lemma eqseq_rot: s1 s2 : (rot n0 s1 == rot n0 s2) = (s1 == s2) FAILURE! Tactics applied: 10000 Original Proof: [by apply: inj_eq; exact: rot_inj.] Proof search time: 0 min, 31 sec Number of successful tactic applications: 1270 Number of failed tactic applications: 8731 Results for lemma eq_find: a1 a2 : a1 =1 a2 -> find a1 =1 find a2 FAILURE! Tactics applied: 10000 Original Proof: [by move=> Ea; elim=> //= x s IHs; rewrite Ea IHs.] Proof search time: 0 min, 10 sec Number of successful tactic applications: 173 Number of failed tactic applications: 9828 Results for lemma rot_size_cat: s1 s2 : rot (size s1) (s1 ++ s2) = s2 ++ s1 FAILURE! Tactics applied: 10000 Original Proof: [by rewrite /rot take_size_cat ?drop_size_cat.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 2903 Number of failed tactic applications: 7098 Results for lemma drop_cons: x s : drop n0 (x :: s) = if n0 is n.+1 then drop n s else x :: s SUCCESS! Proof Found in EFSM: elim : s => // y s IHs; Tactics applied: 9 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 8 Results for lemma eqseq_cat: s1 s2 s3 s4 : size s1 = size s2 -> (s1 ++ s3 == s2 ++ s4) = (s1 == s2) && (s3 == s4) FAILURE! Tactics applied: 10000 Original Proof: [elim: s1 s2 => [|x1 s1 IHs] [|x2 s2] //= [sz12]. by rewrite !eqseq_cons -andbA IHs.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 1273 Number of failed tactic applications: 8728 Results for lemma all_predC: a s : all (predC a) s = ~~ has a s SUCCESS! Proof Found in EFSM: elim : s => //= x s IHs; try by exists s2. case : (a x) => //; Tactics applied: 2595 Original Proof: [by elim: s => //= x s ->; case (a x).] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 7 sec Number of successful tactic applications: 766 Number of failed tactic applications: 1829 Results for lemma perm_cat2l: s1 s2 s3 : perm_eq (s1 ++ s2) (s1 ++ s3) = perm_eq s2 s3 FAILURE! Tactics applied: 10000 Original Proof: [apply/perm_eqP/perm_eqP=> eq23 a; apply/eqP; by move/(_ a)/eqP: eq23; rewrite !count_cat eqn_add2l.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 1703 Number of failed tactic applications: 8298 Results for lemma mem_filter: x s : (x \in filter a s) = a x && (x \in s) FAILURE! Tactics applied: 10000 Original Proof: [rewrite andbC; elim: s => //= y s IHs. rewrite (fun_if (fun s' : seq T => x \in s')) !in_cons {}IHs. by case: eqP => [->|_]; case (a y); rewrite /= ?andbF.] Proof search time: 0 min, 27 sec Number of successful tactic applications: 1172 Number of failed tactic applications: 8829 Results for lemma nth_nseq: m x n : nth (nseq m x) n = (if n < m then x else x0) FAILURE! Tactics applied: 316 Original Proof: [by elim: m n => [|m IHm] [|n] //=; exact: IHm.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 316 Results for lemma has_rot: s a : has a (rot n0 s) = has a s FAILURE! Tactics applied: 10000 Original Proof: [by rewrite has_cat orbC -has_cat cat_take_drop.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 2403 Number of failed tactic applications: 7598 Results for lemma has_predU: a1 a2 s : has (predU a1 a2) s = has a1 s || has a2 s FAILURE! Tactics applied: 10000 Original Proof: [by elim: s => //= x s ->; rewrite -!orbA; do !bool_congr.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 2350 Number of failed tactic applications: 7651 Results for lemma belast_cat: x s1 s2 : belast x (s1 ++ s2) = belast x s1 ++ belast (last x s1) s2 FAILURE! Tactics applied: 316 Original Proof: [by elim: s1 x => [|y s1 IHs] x //=; rewrite IHs.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 316 Results for lemma nth_map: n s : n < size s -> nth x2 (map s) n = f (nth x1 s n) FAILURE! Tactics applied: 10000 Original Proof: [by elim: s n => [|x s IHs] [|n]; try exact (IHs n).] Proof search time: 0 min, 27 sec Number of successful tactic applications: 2251 Number of failed tactic applications: 7750 Results for lemma lastI: x s : x :: s = rcons (belast x s) (last x s) FAILURE! Tactics applied: 10000 Original Proof: [by elim: s x => [|y s IHs] x //=; rewrite IHs.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 2943 Number of failed tactic applications: 7058 Results for lemma mem_rotr: (s : seq T') : rotr n0 s =i s FAILURE! Tactics applied: 10000 Original Proof: [by move=> x; rewrite mem_rot.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 2721 Number of failed tactic applications: 7280 Results for lemma nth_rev: x0 n s : n < size s -> nth x0 (rev s) n = nth x0 s (size s - n.+1) FAILURE! Tactics applied: 10000 Original Proof: [elim/last_ind: s => // s x IHs in n *. rewrite rev_rcons size_rcons ltnS subSS -cats1 nth_cat /=. case: n => [|n] lt_n_s; first by rewrite subn0 ltnn subnn. by rewrite -{2}(subnK lt_n_s) -addSnnS leq_addr /= -IHs.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 2198 Number of failed tactic applications: 7803 Results for lemma drop_nth: n s : n < size s -> drop n s = nth s n :: drop n.+1 s FAILURE! Tactics applied: 10000 Original Proof: [by elim: s n => [|x s IHs] [|n] Hn //=; rewrite ?drop0 1?IHs.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 2251 Number of failed tactic applications: 7750 Results for lemma perm_catCA: s1 s2 s3 : perm_eql (s1 ++ s2 ++ s3) (s2 ++ s1 ++ s3) FAILURE! Tactics applied: 10000 Original Proof: [by apply/perm_eqlP; rewrite !catA perm_cat2r perm_catC.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1367 Number of failed tactic applications: 8634 Results for lemma last_cat: x s1 s2 : last x (s1 ++ s2) = last (last x s1) s2 SUCCESS! Proof Found in EFSM: by elim: s1 x => //= y s1 IHs1 x; Tactics applied: 177 Original Proof: [by elim: s1 x => [|y s1 IHs] x //=; rewrite IHs.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 176 Results for lemma count_predC: a s : count a s + count (predC a) s = size s FAILURE! Tactics applied: 10000 Original Proof: [by elim: s => //= x s IHs; rewrite addnCA -addnA IHs addnA addn_negb.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 3702 Number of failed tactic applications: 6299 Results for lemma drop_oversize: n s : size s <= n -> drop n s = [::] FAILURE! Tactics applied: 10000 Original Proof: [by elim: n s => [|n IHn] [|x s]; try exact (IHn s).] Proof search time: 0 min, 21 sec Number of successful tactic applications: 2276 Number of failed tactic applications: 7725 Results for lemma rem_uniq: s : uniq s -> uniq (rem s) FAILURE! Tactics applied: 10000 Original Proof: [by apply: subseq_uniq; exact: rem_subseq.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 1080 Number of failed tactic applications: 8921 Results for lemma mask_uniq: s : uniq s -> forall m, uniq (mask m s) FAILURE! Tactics applied: 10000 Original Proof: [elim: s => [|x s IHs] Uxs [|b m] //=. case: b Uxs => //= /andP[s'x Us]; rewrite {}IHs // andbT. by apply: contra s'x; exact: mem_mask.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 1587 Number of failed tactic applications: 8414 Results for lemma index_uniq: i s : i < size s -> uniq s -> index (nth s i) s = i FAILURE! Tactics applied: 10000 Original Proof: [elim: s i => [|x s IHs] //= [|i]; rewrite /= ?eqxx // ltnS => lt_i_s. case/andP=> not_s_x /(IHs i)-> {IHs}//. by case: eqP not_s_x => // ->; rewrite mem_nth.] Proof search time: 0 min, 31 sec Number of successful tactic applications: 1726 Number of failed tactic applications: 8275 Results for lemma has_mask_cons: a b m x s : has a (mask (b :: m) (x :: s)) = b && a x || has a (mask m s) SUCCESS! Proof Found in EFSM: by case: b. Tactics applied: 105 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 100 Results for lemma map_id: (s : seq T1) : map id s = s SUCCESS! Proof Found in EFSM: by elim: s => //= x s ->. Tactics applied: 128 Original Proof: [by elim: s => //= x s ->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 11 Number of failed tactic applications: 117 Results for lemma size_zip: s t : size (zip s t) = minn (size s) (size t) FAILURE! Tactics applied: 10000 Original Proof: [by elim: s t => [|x s IHs] [|t2 t] //=; rewrite IHs -add1n addn_minr.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 2834 Number of failed tactic applications: 7167 Results for lemma rev_rot: s : rev (rot n0 s) = rotr n0 (rev s) FAILURE! Tactics applied: 10000 Original Proof: [rewrite /rotr size_rev -{3}(cat_take_drop n0 s) {1}/rot !rev_cat. by rewrite -size_drop -size_rev rot_size_cat.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 3678 Number of failed tactic applications: 6323 Results for lemma eqseq_rcons: s1 s2 x1 x2 : (rcons s1 x1 == rcons s2 x2) = (s1 == s2) && (x1 == x2) FAILURE! Tactics applied: 10000 Original Proof: [elim: s1 s2 => [|y1 s1 IHs] [|y2 s2] /=; rewrite ?eqseq_cons ?andbT ?andbF // ?IHs 1?andbA // andbC; by [case s2 | case s1].] Proof search time: 0 min, 25 sec Number of successful tactic applications: 1256 Number of failed tactic applications: 8745 Results for lemma all_seq1: x : all [:: x] = a x SUCCESS! Proof Found in EFSM: apply : (can_inj negbK); rewrite /= ?cats0. case : (a x) => //; Tactics applied: 3950 Original Proof: [exact: andbT.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 6 sec Number of successful tactic applications: 146 Number of failed tactic applications: 3804 Results for lemma rcons_cat: x s1 s2 : rcons (s1 ++ s2) x = s1 ++ rcons s2 x FAILURE! Tactics applied: 316 Original Proof: [by rewrite -!cats1 catA.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 316 Results for lemma filter_all: s : all (filter s) FAILURE! Tactics applied: 10000 Original Proof: [by elim: s => //= x s IHs; case: ifP => //= ->.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 2382 Number of failed tactic applications: 7619 Results for lemma nth_index: x s : x \in s -> nth s (index x s) = x FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -has_pred1 => /(nth_find x0)/eqP.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 1411 Number of failed tactic applications: 8590 Results for lemma flatten_cat: ss1 ss2 : flatten (ss1 ++ ss2) = flatten ss1 ++ flatten ss2 FAILURE! Tactics applied: 316 Original Proof: [by elim: ss1 => //= s ss1 ->; rewrite catA.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 316 Results for lemma mem_head: x s : x \in x :: s SUCCESS! Proof Found in EFSM: apply : (can_inj negbK); rewrite inE; case : eqP => // ->. Tactics applied: 8991 Original Proof: [exact: predU1l.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 22 sec Number of successful tactic applications: 1048 Number of failed tactic applications: 7943 Results for lemma eq_pmap: (f1 f2 : aT -> option rT) : f1 =1 f2 -> pmap f1 =1 pmap f2 FAILURE! Tactics applied: 10000 Original Proof: [by move=> Ef; elim=> //= x s ->; rewrite Ef.] Proof search time: 0 min, 13 sec Number of successful tactic applications: 193 Number of failed tactic applications: 9808 Results for lemma nth_uniq: s i j : i < size s -> j < size s -> uniq s -> (nth s i == nth s j) = (i == j) FAILURE! Tactics applied: 10000 Original Proof: [move=> lt_i_s lt_j_s Us; apply/eqP/eqP=> [eq_sij|-> //]. by rewrite -(index_uniq lt_i_s Us) eq_sij index_uniq.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 826 Number of failed tactic applications: 9175 Results for lemma uniq_catC: s1 s2 : uniq (s1 ++ s2) = uniq (s2 ++ s1) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite !cat_uniq has_sym andbCA andbA andbC.] Proof search time: 0 min, 33 sec Number of successful tactic applications: 1622 Number of failed tactic applications: 8379 Results for lemma rot_rot: m n s : rot m (rot n s) = rot n (rot m s) FAILURE! Tactics applied: 10000 Original Proof: [case: (ltnP (size s) m) => Hm. by rewrite !(@rot_oversize T m) ?size_rot 1?ltnW. case: (ltnP (size s) n) => Hn. by rewrite !(@rot_oversize T n) ?size_rot 1?ltnW. by rewrite !rot_add_mod 1?addnC.] Proof search time: 0 min, 28 sec Number of successful tactic applications: 3495 Number of failed tactic applications: 6506 Results for lemma catrev_catl: s t u : catrev (s ++ t) u = catrev t (catrev s u) FAILURE! Tactics applied: 10000 Original Proof: [by elim: s u => /=.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 3422 Number of failed tactic applications: 6579 Results for lemma all_rcons: s x : all (rcons s x) = a x && all s FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -cats1 all_cat all_seq1 andbC.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 1423 Number of failed tactic applications: 8578 Results for lemma leq_size_perm: s1 s2 : uniq s1 -> {subset s1 <= s2} -> size s2 <= size s1 -> s1 =i s2 /\ size s1 = size s2 FAILURE! Tactics applied: 10000 Original Proof: [move=> Us1 ss12 le_s21; have Us2: uniq s2 := leq_size_uniq Us1 ss12 le_s21. suffices: s1 =i s2 by split; last by apply/eqP; rewrite -uniq_size_uniq. move=> x; apply/idP/idP=> [/ss12// | s2x]; apply: contraLR le_s21 => not_s1x. rewrite -ltnNge (@uniq_leq_size (x :: s1)) /= ?not_s1x //. by apply/allP; rewrite /= s2x; exact/allP.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 864 Number of failed tactic applications: 9137 Results for lemma cats1: s z : s ++ [:: z] = rcons s z SUCCESS! Proof Found in EFSM: by elim: s => //= x s ->. Tactics applied: 128 Original Proof: [by elim: s => //= x s ->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 13 Number of failed tactic applications: 115 Results for lemma size_pmap_sub: s : size (pmap (insub : T -> option sT) s) = count p s FAILURE! Tactics applied: 10000 Original Proof: [by rewrite size_pmap (eq_count (isSome_insub _)).] Proof search time: 0 min, 30 sec Number of successful tactic applications: 3430 Number of failed tactic applications: 6571 Results for lemma subseq_cons: s x : subseq s (x :: s) FAILURE! Tactics applied: 10000 Original Proof: [by exact: (@cat_subseq [::] s [:: x]).] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1101 Number of failed tactic applications: 8900 Results for lemma catCA_perm_subst: R F : (forall s1 s2 s3, F (s1 ++ s2 ++ s3) = F (s2 ++ s1 ++ s3) :> R) -> (forall s1 s2, perm_eq s1 s2 -> F s1 = F s2) FAILURE! Tactics applied: 10000 Original Proof: [move=> FcatCA s1 s2 /catCA_perm_ind => ind_s12. by apply: (ind_s12 (eq _ \o F)) => //= *; rewrite FcatCA.] Proof search time: 0 min, 13 sec Number of successful tactic applications: 224 Number of failed tactic applications: 9777 Results for lemma perm_eq_mem: s1 s2 : perm_eq s1 s2 -> s1 =i s2 FAILURE! Tactics applied: 10000 Original Proof: [by move/perm_eqP=> eq12 x; rewrite -!has_pred1 !has_count eq12.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1177 Number of failed tactic applications: 8824 Results for lemma all_cat: s1 s2 : all (s1 ++ s2) = all s1 && all s2 FAILURE! Tactics applied: 10000 Original Proof: [by elim: s1 => [|x s1 IHs] //=; rewrite IHs andbA.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 1591 Number of failed tactic applications: 8410 Results for lemma drop0: s : drop 0 s = s SUCCESS! Proof Found in EFSM: elim : s => // y s IHs; Tactics applied: 9 Original Proof: [by case: s.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 8 Results for lemma rot_inj: : injective (rot n0) FAILURE! Tactics applied: 10000 Original Proof: [exact (can_inj rotK).] Proof search time: 0 min, 11 sec Number of successful tactic applications: 232 Number of failed tactic applications: 9769 Results for lemma subseq_rcons: s x : subseq s (rcons s x) SUCCESS! Proof Found in EFSM: apply : (can_inj negbK); elim : s => //= y s IHs. by case: eqP => //= <-; Tactics applied: 4905 Original Proof: [by rewrite -{1}[s]cats0 -cats1 cat_subseq.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 10 sec Number of successful tactic applications: 859 Number of failed tactic applications: 4046 Results for lemma leq_size_uniq: s1 s2 : uniq s1 -> {subset s1 <= s2} -> size s2 <= size s1 -> uniq s2 FAILURE! Tactics applied: 10000 Original Proof: [elim: s1 s2 => [[] | x s1 IHs s2] // Us1x; have /andP[not_s1x Us1] := Us1x. case/allP/andP=> /rot_to[i s3 def_s2] /allP ss12 le_s21. rewrite -(rot_uniq i) -(size_rot i) def_s2 /= in le_s21 *. have ss13 y (s1y : y \in s1): y \in s3. by have:= ss12 y s1y; rewrite -(mem_rot i) def_s2 inE (negPf (memPn _ y s1y)). rewrite IHs // andbT; apply: contraL _ le_s21 => s3x; rewrite -leqNgt. by apply/(uniq_leq_size Us1x)/allP; rewrite /= s3x; exact/allP.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 871 Number of failed tactic applications: 9130 Results for lemma nth_iota: m n i : i < n -> nth 0 (iota m n) i = m + i FAILURE! Tactics applied: 10000 Original Proof: [by move/subnKC <-; rewrite addSnnS iota_add nth_cat size_iota ltnn subnn.] Proof search time: 0 min, 14 sec Number of successful tactic applications: 185 Number of failed tactic applications: 9816 Results for lemma perm_cat2r: s1 s2 s3 : perm_eq (s2 ++ s1) (s3 ++ s1) = perm_eq s2 s3 FAILURE! Tactics applied: 10000 Original Proof: [by do 2!rewrite perm_eq_sym perm_catC; exact: perm_cat2l.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 1691 Number of failed tactic applications: 8310 Results for lemma belast_rcons: x s z : belast x (rcons s z) = x :: s FAILURE! Tactics applied: 10000 Original Proof: [by rewrite lastI -!cats1 belast_cat.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 2956 Number of failed tactic applications: 7045 Results for lemma size_rcons: s x : size (rcons s x) = (size s).+1 FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -cats1 size_cat addnC.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 2952 Number of failed tactic applications: 7049 Results for lemma size_undup: s : size (undup s) <= size s FAILURE! Tactics applied: 10000 Original Proof: [by elim: s => //= x s IHs; case: (x \in s) => //=; exact: ltnW.] Proof search time: 0 min, 34 sec Number of successful tactic applications: 2394 Number of failed tactic applications: 7607 Results for lemma map_rot: s : map (rot n0 s) = rot n0 (map s) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite /rot map_cat map_take map_drop.] Proof search time: 0 min, 31 sec Number of successful tactic applications: 3679 Number of failed tactic applications: 6322 Results for lemma set_nth_nil: n y : set_nth [::] n y = ncons n x0 [:: y] SUCCESS! Proof Found in EFSM: by case: n. Tactics applied: 106 Original Proof: [by case: n.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 105 Results for lemma headI: T s (x : T) : rcons s x = head x s :: behead (rcons s x) SUCCESS! Proof Found in EFSM: elim : s => // y s IHs; Tactics applied: 9 Original Proof: [by case: s.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 8 Results for lemma has_seqb: (b : bool) x : has (nseq b x) = b && a x FAILURE! Tactics applied: 10000 Original Proof: [by case: b => //=; exact: orbF.] Proof search time: 0 min, 15 sec Number of successful tactic applications: 385 Number of failed tactic applications: 9616 Results for lemma pairmapK: : (forall x, cancel (f x) (g x)) -> forall x, cancel (pairmap x) (scanl x) FAILURE! Tactics applied: 10000 Original Proof: [by move=> Hgf x s; elim: s x => //= y s IHs x; rewrite Hgf IHs.] Proof search time: 0 min, 14 sec Number of successful tactic applications: 175 Number of failed tactic applications: 9826 Results for lemma filter_mask: T a (s : seq T) : filter a s = mask (map a s) s SUCCESS! Proof Found in EFSM: by elim: s => //= x s ->. Tactics applied: 128 Original Proof: [by elim: s => //= x s <-; case: (a x).] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 11 Number of failed tactic applications: 117 Results for lemma perm_eqlP: s1 s2 : reflect (perm_eql s1 s2) (perm_eq s1 s2) FAILURE! Tactics applied: 10000 Original Proof: [apply: (iffP idP) => [eq12 s3 | -> //]. apply/idP/idP; last exact: perm_eq_trans. by rewrite -!(perm_eq_sym s3); move/perm_eq_trans; apply.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 2301 Number of failed tactic applications: 7700 Results for lemma eq_filter: a1 a2 : a1 =1 a2 -> filter a1 =1 filter a2 FAILURE! Tactics applied: 10000 Original Proof: [by move=> Ea; elim=> //= x s IHs; rewrite Ea IHs.] Proof search time: 0 min, 10 sec Number of successful tactic applications: 146 Number of failed tactic applications: 9855 Results for lemma eq_all_r: s1 s2 : s1 =i s2 -> all^~ s1 =1 all^~ s2 FAILURE! Tactics applied: 10000 Original Proof: [by move=> Es12 a; apply/(allP a s1)/(allP a s2) => Hs x Hx; apply: Hs; rewrite Es12 in Hx *.] Proof search time: 0 min, 27 sec Number of successful tactic applications: 1177 Number of failed tactic applications: 8824 Results for lemma index_last: x s : uniq (x :: s) -> index (last x s) (x :: s) = size s FAILURE! Tactics applied: 10000 Original Proof: [rewrite lastI rcons_uniq -cats1 index_cat size_belast. by case: ifP => //=; rewrite eqxx addn0.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 1067 Number of failed tactic applications: 8934 Results for lemma reshapeKr: sh s : size s <= sumn sh -> flatten (reshape sh s) = s FAILURE! Tactics applied: 10000 Original Proof: [elim: sh s => [[]|n sh IHsh] //= s sz_s; rewrite IHsh ?cat_take_drop //. by rewrite size_drop leq_subLR.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 1095 Number of failed tactic applications: 8906 OVERALL RESULTS SUMMARY EFSMProver proved 90 out of 394 lemmas. Success rate of 22.84263959390863% There were 0 errors. 304 proof attempts exhausted the automaton On average, a proof was found after applying 607 tactics The longest proof consisted of 5 tactics There were 6 shorter proofs found Of the 304 failures, 275 of them used all 10000 tactics There were 75 reused proofs found There were 15 novel proofs found Of the 304 failures, the average number of tactics used was 9127 On average, a proof was found after 0 min, 2 sec On average, a failed proof attempt took 0 min, 21 sec On average, any (success or failure) proof attempt took 0 min, 16 sec The longest time to find a proof was 0 min, 22 sec The shortest time to find a proof was 0 min, 0 sec There were 0 proofs containing repeated tactics There were 9 proofs that repeated states