Results for fold 1 Results for lemma disjoint_sym: A B : [disjoint A & B] = [disjoint B & A] FAILURE! Tactics applied: 10000 Original Proof: [by congr (_ == 0); apply: eq_card => x; exact: andbC.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 423 Number of failed tactic applications: 9578 Results for fold 2 Results for lemma card_option: : #|{: option T}| = #|T|.+1 FAILURE! Tactics applied: 10000 Original Proof: [by rewrite !cardT !enumT {1}unlock /= !size_map.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 264 Number of failed tactic applications: 9737 Results for fold 3 Results for lemma enum_val_bij_in: x0 A : x0 \in A -> {on A, bijective (@enum_val A)} FAILURE! Tactics applied: 10000 Original Proof: [move=> Ax0; exists (enum_rank_in Ax0) => [i _|]; last exact: enum_rankK_in. exact: enum_valK_in.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 611 Number of failed tactic applications: 9390 Results for fold 4 Results for lemma enum_val_nth: A x i : @enum_val A i = nth x (enum A) i FAILURE! Tactics applied: 10000 Original Proof: [by apply: set_nth_default; rewrite cardE in i *; exact: ltn_ord.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 335 Number of failed tactic applications: 9666 Results for fold 5 Results for lemma rev_ord_inj: {n} : injective (@rev_ord n) FAILURE! Tactics applied: 10000 Original Proof: [exact: inv_inj (@rev_ordK n).] Proof search time: 0 min, 20 sec Number of successful tactic applications: 336 Number of failed tactic applications: 9665 Results for fold 6 Results for lemma nth_enum_rank: x0 : cancel enum_rank (nth x0 (enum T)) SUCCESS! Proof Found in EFSM: move => Ax0; rewrite /= insubdK ?nth_index ?mem_enum //. by rewrite cardE [_ \in _]index_mem mem_enum. Tactics applied: 2724 Original Proof: [by move=> x; exact: nth_enum_rank_in.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 8 sec Number of successful tactic applications: 83 Number of failed tactic applications: 2641 Results for fold 7 Results for lemma eq_subxx: A B : A =i B -> A \subset B FAILURE! Tactics applied: 10000 Original Proof: [by move/eq_subset->.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 541 Number of failed tactic applications: 9460 Results for fold 8 Results for lemma card_sig: : #|{: {x | P x}}| = #|[pred x | P x]| SUCCESS! Proof Found in EFSM: by rewrite !cardE enumT unlock -(size_map val) val_sub_enum. Tactics applied: 431 Original Proof: [exact: card_sub.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 7 Number of failed tactic applications: 424 Results for fold 9 Results for lemma exists_eq_inP: D f1 f2 : reflect (exists2 x, D x & f1 x = f2 x) [exists (x | D x), f1 x == f2 x] FAILURE! Tactics applied: 609 Original Proof: [by apply: (iffP (exists_inP _ _)) => [] [x Dx /eqP]; exists x.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 0 Number of failed tactic applications: 609 Results for fold 10 Results for lemma card_in_image: A : {in A &, injective f} -> #|image f A| = #|A| FAILURE! Tactics applied: 10000 Original Proof: [move=> injf; rewrite (cardE A) -(size_map f); apply/card_uniqP. rewrite map_inj_in_uniq ?enum_uniq // => x y; rewrite !mem_enum; exact: injf.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 204 Number of failed tactic applications: 9797 Results for fold 11 Results for lemma proper_subn: A B : A \proper B -> ~~ (B \subset A) SUCCESS! Proof Found in EFSM: by case/andP. Tactics applied: 351 Original Proof: [by case/andP.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 27 Number of failed tactic applications: 324 Results for fold 12 Results for lemma option_enumP: : Finite.axiom option_enum FAILURE! Tactics applied: 10000 Original Proof: [by case=> [x|]; rewrite /= count_map (count_pred0, enumP).] Proof search time: 0 min, 21 sec Number of successful tactic applications: 299 Number of failed tactic applications: 9702 Results for fold 13 Results for lemma disjoint1: x A : [disjoint pred1 x & A] = (x \notin A) FAILURE! Tactics applied: 10000 Original Proof: [apply/negbRL/(sameP (pred0Pn _)). apply: introP => [Ax | notAx [_ /andP[/eqP->]]]; last exact: negP. by exists x; rewrite !inE eqxx.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 272 Number of failed tactic applications: 9729 Results for fold 14 Results for lemma eq_enum: P Q : P =i Q -> enum P = enum Q FAILURE! Tactics applied: 10000 Original Proof: [move=> eqPQ; exact: eq_filter.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 1386 Number of failed tactic applications: 8615 Results for fold 15 Results for lemma exists_inP: D P : reflect (exists2 x, D x & P x) [exists (x | D x), P x] FAILURE! Tactics applied: 767 Original Proof: [by apply: (iffP pred0Pn) => [[x /andP[]] | [x]]; exists x => //; apply/andP.] Proof search time: 0 min, 2 sec Number of successful tactic applications: 7 Number of failed tactic applications: 760 Results for fold 16 Results for lemma codomP: y : reflect (exists x, y = f x) (y \in codom f) FAILURE! Tactics applied: 10000 Original Proof: [by apply: (iffP (imageP _ y)) => [][x]; exists x.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 3066 Number of failed tactic applications: 6935 Results for fold 17 Results for lemma size_image: A : size (image f A) = #|A| FAILURE! Tactics applied: 10000 Original Proof: [by rewrite size_map -cardE.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 338 Number of failed tactic applications: 9663 Results for fold 18 Results for lemma dinjectivePn: D : reflect (exists2 x, x \in D & exists2 y, y \in [predD1 D & x] & f x = f y) (~~ dinjectiveb D) FAILURE! Tactics applied: 1783 Original Proof: [apply: (iffP idP) => [injf | [x Dx [y Dxy eqfxy]]]; last first. move: Dx; rewrite -(mem_enum D) => /rot_to[i E defE]. rewrite /dinjectiveb -(rot_uniq i) -map_rot defE /=; apply/nandP; left. rewrite inE /= -(mem_enum D) -(mem_rot i) defE inE in Dxy. rewrite andb_orr andbC andbN in Dxy. by rewrite eqfxy map_f //; case/andP: Dxy. pose p := [pred x in D | [exists (y | y \in [predD1 D & x]), f x == f y]]. case: (pickP p) => [x /= /andP[Dx /exists_inP[y Dxy /eqP eqfxy]] | no_p]. by exists x; last exists y. rewrite /dinjectiveb map_inj_in_uniq ?enum_uniq // in injf => x y Dx Dy eqfxy. apply: contraNeq (negbT (no_p x)) => ne_xy /=; rewrite -mem_enum Dx. by apply/existsP; exists y; rewrite /= !inE eq_sym ne_xy -mem_enum Dy eqfxy /=.] Proof search time: 0 min, 3 sec Number of successful tactic applications: 3 Number of failed tactic applications: 1780 Results for fold 19 Results for lemma negb_forall_in: D P : ~~ [forall (x | D x), P x] = [exists (x | D x), ~~ P x] FAILURE! Tactics applied: 10000 Original Proof: [by apply: eq_existsb => x; rewrite negb_imply.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 238 Number of failed tactic applications: 9763 Results for fold 20 Results for lemma enumT: : enum T = Finite.enum T FAILURE! Tactics applied: 5962 Original Proof: [exact: filter_predT.] Proof search time: 0 min, 14 sec Number of successful tactic applications: 186 Number of failed tactic applications: 5776 Results for fold 21 Results for lemma prod_enumP: : Finite.axiom prod_enum FAILURE! Tactics applied: 10000 Original Proof: [by case=> x1 x2; rewrite (predX_prod_enum (pred1 x1) (pred1 x2)) !card1.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 362 Number of failed tactic applications: 9639 Results for fold 22 Results for lemma disjoint_subset: A B : [disjoint A & B] = (A \subset [predC B]) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite subset_disjoint; apply: eq_disjoint_r => x; rewrite !inE /= negbK.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 413 Number of failed tactic applications: 9588 Results for fold 23 Results for lemma card_seq_sub: : uniq s -> #|{:seq_sub}| = size s FAILURE! Tactics applied: 10000 Original Proof: [by move=> Us; rewrite cardE enumT -(size_map val) unlock val_seq_sub_enum.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 248 Number of failed tactic applications: 9753 Results for fold 24 Results for lemma eq_forallb_in: D P1 P2 : (forall x, D x -> P1 x = P2 x) -> [forall (x | D x), P1 x] = [forall (x | D x), P2 x] FAILURE! Tactics applied: 10000 Original Proof: [by move=> eqP12; apply: eq_forallb => i; case Di: (D i); rewrite // eqP12.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 324 Number of failed tactic applications: 9677 Results for fold 25 Results for lemma sub_ord_proof: m : n' - m < n FAILURE! Tactics applied: 10000 Original Proof: [by rewrite ltnS leq_subr.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 436 Number of failed tactic applications: 9565 Results for fold 26 Results for lemma image_f: A x : x \in A -> f x \in image f A FAILURE! Tactics applied: 10000 Original Proof: [by move=> Ax; apply/imageP; exists x.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 500 Number of failed tactic applications: 9501 Results for fold 27 Results for lemma index_enum_ord: (i : 'I_n) : index i (enum 'I_n) = i FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -{1}(nth_ord_enum i i) index_uniq ?(enum_uniq, size_enum_ord).] Proof search time: 0 min, 20 sec Number of successful tactic applications: 374 Number of failed tactic applications: 9627 Results for fold 28 Results for lemma pickP: : pick_spec (pick P) FAILURE! Tactics applied: 495 Original Proof: [rewrite /pick; case: (enum _) (mem_enum P) => [|x s] Pxs /=. by right; exact: fsym. by left; rewrite -[P _]Pxs mem_head.] Proof search time: 0 min, 4 sec Number of successful tactic applications: 4 Number of failed tactic applications: 491 Results for fold 29 Results for lemma bij_on_image: A (x0 : T) : {on [pred y in image f A], bijective f} FAILURE! Tactics applied: 10000 Original Proof: [exact: subon_bij (@image_codom A) (bij_on_codom x0).] Proof search time: 0 min, 26 sec Number of successful tactic applications: 2146 Number of failed tactic applications: 7855 Results for fold 30 Results for lemma neq_lift: n (h : 'I_n) i : h != lift h i FAILURE! Tactics applied: 10000 Original Proof: [exact: neq_bump.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 538 Number of failed tactic applications: 9463 Results for fold 31 Results for lemma enum_rankK_in: x0 A Ax0 : {in A, cancel (@enum_rank_in x0 A Ax0) enum_val} FAILURE! Tactics applied: 10000 Original Proof: [by move=> x; exact: nth_enum_rank_in.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 564 Number of failed tactic applications: 9437 Results for fold 32 Results for lemma unlift_subproof: n (h : 'I_n) (u : {j | j != h}) : unbump h (val u) < n.-1 FAILURE! Tactics applied: 10000 Original Proof: [case: n h u => [|n h] [] //= j ne_jh. rewrite -(leq_bump2 h.+1) bumpS unbumpK // /bump. case: (ltngtP n h) => [|_|eq_nh]; rewrite ?(leqNgt _ h) ?ltn_ord //. by rewrite ltn_neqAle [j <= _](valP j) {2}eq_nh andbT.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 479 Number of failed tactic applications: 9522 Results for fold 33 Results for lemma subset_predT: A : A \subset T SUCCESS! Proof Found in EFSM: rewrite unlock; exact /pred0P. Tactics applied: 1569 Original Proof: [by apply/subsetP.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 6 sec Number of successful tactic applications: 46 Number of failed tactic applications: 1523 Results for fold 34 Results for lemma negb_exists: P : ~~ [exists x, P x] = [forall x, ~~ P x] FAILURE! Tactics applied: 10000 Original Proof: [by apply/negbLR/esym/eq_existsb=> x; apply: negbK.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 259 Number of failed tactic applications: 9742 Results for fold 35 Results for lemma in_iinv_f: A : {in A &, injective f} -> forall x fAfx, x \in A -> @iinv A (f x) fAfx = x FAILURE! Tactics applied: 10000 Original Proof: [move=> injf x fAfx Ax; apply: injf => //; [exact: mem_iinv | exact: f_iinv].] Proof search time: 0 min, 23 sec Number of successful tactic applications: 282 Number of failed tactic applications: 9719 Results for fold 36 Results for lemma f_invF: : cancel invF f FAILURE! Tactics applied: 10000 Original Proof: [by move=> y; exact: f_iinv.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 184 Number of failed tactic applications: 9817 Results for fold 37 Results for lemma eq_pick: P Q : P =1 Q -> pick P = pick Q FAILURE! Tactics applied: 10000 Original Proof: [by move=> eqPQ; rewrite /pick (eq_enum eqPQ).] Proof search time: 0 min, 23 sec Number of successful tactic applications: 397 Number of failed tactic applications: 9604 Results for fold 38 Results for lemma enum_uniq: : uniq (enum P) FAILURE! Tactics applied: 10000 Original Proof: [by apply/filter_uniq/count_mem_uniq => x; rewrite enumP -enumT mem_enum.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 371 Number of failed tactic applications: 9630 Results for fold 39 Results for lemma card_gt0P: A : reflect (exists i, i \in A) (#|A| > 0) FAILURE! Tactics applied: 10000 Original Proof: [rewrite lt0n; exact: pred0Pn.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 295 Number of failed tactic applications: 9706 Results for fold 40 Results for lemma mem_enum: A : enum A =i A FAILURE! Tactics applied: 10000 Original Proof: [by move=> x; rewrite mem_filter andbC -has_pred1 has_count enumP.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 883 Number of failed tactic applications: 9118 Results for fold 41 Results for lemma eq_disjoint0: A B : A =i pred0 -> [disjoint A & B] FAILURE! Tactics applied: 10000 Original Proof: [by move/eq_disjoint->; exact: disjoint0.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 579 Number of failed tactic applications: 9422 Results for fold 42 Results for lemma enum0: : enum pred0 = Nil T FAILURE! Tactics applied: 10000 Original Proof: [exact: filter_pred0.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 678 Number of failed tactic applications: 9323 Results for fold 43 Results for lemma eq_cardT: A : A =i predT -> #|A| = size (enum T) FAILURE! Tactics applied: 10000 Original Proof: [exact: eq_card_trans cardT.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 456 Number of failed tactic applications: 9545 Results for fold 44 Results for lemma nth_codom: T' y0 (f : T -> T') (i : 'I_#|T|) : nth y0 (codom f) i = f (enum_val i) SUCCESS! Proof Found in EFSM: by rewrite -(nth_map _ y0) // -cardE. Tactics applied: 271 Original Proof: [exact: nth_image.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 1 Number of failed tactic applications: 270 Results for fold 45 Results for lemma eq_disjoint1: x A B : A =i pred1 x -> [disjoint A & B] = (x \notin B) FAILURE! Tactics applied: 10000 Original Proof: [by move/eq_disjoint->; exact: disjoint1.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 303 Number of failed tactic applications: 9698 Results for fold 46 Results for lemma max_card: A : #|A| <= #|T| FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -(cardC A) leq_addr.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 463 Number of failed tactic applications: 9538 Results for fold 47 Results for lemma neq_bump: h i : h != bump h i FAILURE! Tactics applied: 10000 Original Proof: [rewrite /bump eqn_leq; have [le_hi | lt_ih] := leqP h i. by rewrite ltnNge le_hi andbF. by rewrite leqNgt lt_ih.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 322 Number of failed tactic applications: 9679 Results for fold 48 Results for lemma nth_ord_enum: (i0 i : 'I_n) : nth i0 (enum 'I_n) i = i FAILURE! Tactics applied: 10000 Original Proof: [apply: val_inj; exact: nth_enum_ord.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 1322 Number of failed tactic applications: 8679 Results for fold 49 Results for lemma subset_eqP: A B : reflect (A =i B) ((A \subset B) && (B \subset A)) FAILURE! Tactics applied: 10000 Original Proof: [apply: (iffP andP) => [[sAB sBA] x| eqAB]; last by rewrite !eq_subxx. by apply/idP/idP; apply: subsetP.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 2217 Number of failed tactic applications: 7784 Results for fold 50 Results for lemma enum1: x : enum (pred1 x) = [:: x] FAILURE! Tactics applied: 10000 Original Proof: [rewrite [enum _](all_pred1P x _ _); first by rewrite -count_filter enumP. by apply/allP=> y; rewrite mem_enum.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 1264 Number of failed tactic applications: 8737 Results for fold 51 Results for lemma sub_ordK: (i : 'I_n) : n' - (n' - i) = i FAILURE! Tactics applied: 10000 Original Proof: [by rewrite subKn ?leq_ord.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 290 Number of failed tactic applications: 9711 Results for fold 52 Results for lemma split_subproof: m n (i : 'I_(m + n)) : i >= m -> i - m < n FAILURE! Tactics applied: 10000 Original Proof: [by move/subSn <-; rewrite leq_subLR.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 316 Number of failed tactic applications: 9685 Results for fold 53 Results for lemma leq_ord: (i : 'I_n) : i <= n' SUCCESS! Proof Found in EFSM: exact : valP i. Tactics applied: 297 Original Proof: [exact: valP i.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 4 sec Number of successful tactic applications: 1 Number of failed tactic applications: 296 Results for fold 54 Results for lemma subset_leq_card: A B : A \subset B -> #|A| <= #|B| FAILURE! Tactics applied: 10000 Original Proof: [move=> sAB. rewrite -(cardID A B) [#|predI _ _|](@eq_card _ A) ?leq_addr //= => x. rewrite !inE andbC; case Ax: (x \in A) => //; exact: subsetP Ax.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 463 Number of failed tactic applications: 9538 Results for fold 55 Results for lemma proper_sub_trans: A B C : A \proper B -> B \subset C -> A \proper C FAILURE! Tactics applied: 10000 Original Proof: [case/properP=> sAB [x Bx nAx] sBC; rewrite properE (subset_trans sAB) //. by apply/subsetPn; exists x; rewrite ?(subsetP _ _ sBC).] Proof search time: 0 min, 24 sec Number of successful tactic applications: 490 Number of failed tactic applications: 9511 Results for fold 56 Results for lemma cast_ordKV: n1 n2 eq_n : cancel (cast_ord (esym eq_n)) (@cast_ord n1 n2 eq_n) SUCCESS! Proof Found in EFSM: case => i x; apply /eqP; exact : eqxx. Tactics applied: 6299 Original Proof: [by move=> i; exact: val_inj.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 13 sec Number of successful tactic applications: 176 Number of failed tactic applications: 6123 Results for fold 57 Results for lemma enum_val_inj: A : injective (@enum_val A) FAILURE! Tactics applied: 10000 Original Proof: [by move=> i; exact: can_inj (enum_valK_in (enum_valP i)) (i).] Proof search time: 0 min, 21 sec Number of successful tactic applications: 365 Number of failed tactic applications: 9636 Results for fold 58 Results for lemma card0_eq: A : #|A| = 0 -> A =i pred0 FAILURE! Tactics applied: 10000 Original Proof: [by move=> A0 x; apply/idP => Ax; rewrite (cardD1 x) Ax in A0.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 358 Number of failed tactic applications: 9643 Results for fold 59 Results for lemma count_enumP: : axiom count_enum FAILURE! Tactics applied: 10000 Original Proof: [apply: uniq_enumP (pmap_uniq (@pickle_invK T) (iota_uniq _ _)) _ => x. by rewrite mem_pmap -pickleK_inv map_f // mem_iota ubT.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 335 Number of failed tactic applications: 9666 Results for fold 60 Results for lemma iinv_f: x fTfx : @iinv T (f x) fTfx = x FAILURE! Tactics applied: 10000 Original Proof: [by apply: in_iinv_f; first exact: in2W.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 228 Number of failed tactic applications: 9773 Results for fold 61 Results for lemma val_seq_sub_enum: : uniq s -> map val seq_sub_enum = s FAILURE! Tactics applied: 10000 Original Proof: [move=> Us; rewrite /seq_sub_enum undup_id ?pmap_sub_uniq //. rewrite (pmap_filter (@insubK _ _ _)); apply/all_filterP. by apply/allP => x; rewrite isSome_insub.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 352 Number of failed tactic applications: 9649 Results for fold 62 Results for lemma proper_irrefl: A : ~~ (A \proper A) SUCCESS! Proof Found in EFSM: by rewrite properE subxx. Tactics applied: 512 Original Proof: [by rewrite properE subxx.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 11 Number of failed tactic applications: 501 Results for fold 63 Results for lemma nth_enum_ord: i0 m : m < n -> nth i0 (enum 'I_n) m = m :> nat FAILURE! Tactics applied: 10000 Original Proof: [by move=> ?; rewrite -(nth_map _ 0) (size_enum_ord, val_enum_ord) // nth_iota.] Proof search time: 0 min, 27 sec Number of successful tactic applications: 432 Number of failed tactic applications: 9569 Results for fold 64 Results for lemma splitK: m n : cancel (@split m n) (@unsplit m n) FAILURE! Tactics applied: 10000 Original Proof: [by move=> i; apply: val_inj; case: splitP.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 517 Number of failed tactic applications: 9484 Results for fold 65 Results for lemma codom_f: x : f x \in codom f FAILURE! Tactics applied: 10000 Original Proof: [by exact: image_f.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 318 Number of failed tactic applications: 9683 Results for fold 66 Results for lemma disjoint_trans: A B C : A \subset B -> [disjoint B & C] -> [disjoint A & C] FAILURE! Tactics applied: 10000 Original Proof: [by rewrite 2!disjoint_subset; exact: subset_trans.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 570 Number of failed tactic applications: 9431 Results for fold 67 Results for lemma ord_enum_uniq: : uniq ord_enum FAILURE! Tactics applied: 10000 Original Proof: [by rewrite pmap_sub_uniq ?iota_uniq.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 262 Number of failed tactic applications: 9739 Results for fold 68 Results for lemma unit_enumP: : Finite.axiom [::tt] SUCCESS! Proof Found in EFSM: by []. Tactics applied: 87 Original Proof: [by case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 21 Number of failed tactic applications: 66 Results for fold 69 Results for lemma subsetE: A B : (A \subset B) = pred0b [predD A & B] SUCCESS! Proof Found in EFSM: by rewrite unlock. Tactics applied: 193 Original Proof: [by rewrite unlock.] 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: 192 Results for fold 70 Results for lemma canF_LR: x y : x = g y -> f x = y FAILURE! Tactics applied: 10000 Original Proof: [exact: canLR canF_sym.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 418 Number of failed tactic applications: 9583 Results for fold 71 Results for lemma canF_invF: : g =1 invF (can_inj fK) FAILURE! Tactics applied: 10000 Original Proof: [by move=> y; apply: (canLR fK); rewrite f_invF.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 320 Number of failed tactic applications: 9681 Results for fold 72 Results for lemma card0: : #|@pred0 T| = 0 FAILURE! Tactics applied: 10000 Original Proof: [by rewrite cardE enum0.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 453 Number of failed tactic applications: 9548 Results for fold 73 Results for lemma mem_sum_enum: u : u \in sum_enum FAILURE! Tactics applied: 10000 Original Proof: [by case: u => x; rewrite mem_cat -!enumT map_f ?mem_enum ?orbT.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 353 Number of failed tactic applications: 9648 Results for fold 74 Results for lemma bool_enumP: : Finite.axiom [:: true; false] SUCCESS! Proof Found in EFSM: by case. Tactics applied: 184 Original Proof: [by case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 23 Number of failed tactic applications: 161 Results for fold 75 Results for lemma injF_onto: y : y \in codom f FAILURE! Tactics applied: 10000 Original Proof: [exact: inj_card_onto.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 1474 Number of failed tactic applications: 8527 Results for fold 76 Results for lemma forall_inP: D P : reflect (forall x, D x -> P x) [forall (x | D x), P x] FAILURE! Tactics applied: 10000 Original Proof: [by apply: (iffP (forallP _)) => /= P_ x /=; apply/implyP; apply: P_.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 493 Number of failed tactic applications: 9508 Results for fold 77 Results for lemma image_iinv: A y (fTy : y \in codom f) : (y \in image f A) = (iinv fTy \in A) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -mem_image ?f_iinv.] Proof search time: 0 min, 32 sec Number of successful tactic applications: 265 Number of failed tactic applications: 9736 Results for fold 78 Results for lemma widen_ord_proof: n m (i : 'I_n) : n <= m -> i < m FAILURE! Tactics applied: 10000 Original Proof: [exact: leq_trans.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 320 Number of failed tactic applications: 9681 Results for fold 79 Results for lemma existsP: P : reflect (exists x, P x) [exists x, P x] FAILURE! Tactics applied: 432 Original Proof: [by apply: (iffP pred0Pn) => [] [x]; exists x.] Proof search time: 0 min, 3 sec Number of successful tactic applications: 1 Number of failed tactic applications: 431 Results for fold 80 Results for lemma bumpC: h1 h2 i : bump h1 (bump h2 i) = bump (bump h1 h2) (bump (unbump h2 h1) i) FAILURE! Tactics applied: 10000 Original Proof: [rewrite {1 5}/bump -leq_bump addnCA; congr (_ + (_ + _)). rewrite 2!leq_bump /unbump /bump; case: (leqP h1 h2) => [le_h12 | lt_h21]. by rewrite subn0 ltnS le_h12 subn1. by rewrite subn1 (ltn_predK lt_h21) (leqNgt h1) lt_h21 subn0.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 803 Number of failed tactic applications: 9198 Results for fold 81 Results for lemma cast_ordK: n1 n2 eq_n : cancel (@cast_ord n1 n2 eq_n) (cast_ord (esym eq_n)) SUCCESS! Proof Found in EFSM: rewrite /seq_sub_unpickle => x. exact : val_inj. Tactics applied: 2356 Original Proof: [by move=> i; exact: val_inj.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 5 sec Number of successful tactic applications: 117 Number of failed tactic applications: 2239 Results for fold 82 Results for lemma preim_iinv: A B y fAy : preim f B (@iinv A y fAy) = B y FAILURE! Tactics applied: 10000 Original Proof: [by rewrite /= f_iinv.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 550 Number of failed tactic applications: 9451 Results for fold 83 Results for lemma inordK: m : m < n -> inord m = m :> nat SUCCESS! Proof Found in EFSM: move => Ax0; rewrite /= insubdK ?nth_index ?mem_enum //. Tactics applied: 450 Original Proof: [by move=> lt_m; rewrite val_insubd lt_m.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 sec Number of successful tactic applications: 25 Number of failed tactic applications: 425 Results for fold 84 Results for lemma bump_addl: h i k : bump (k + h) (k + i) = k + bump h i FAILURE! Tactics applied: 10000 Original Proof: [by rewrite /bump leq_add2l addnCA.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 266 Number of failed tactic applications: 9735 Results for fold 85 Results for lemma inord_val: (i : 'I_n) : inord i = i FAILURE! Tactics applied: 10000 Original Proof: [by rewrite /inord /insubd valK.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 316 Number of failed tactic applications: 9685 Results for fold 86 Results for lemma image_pre: (B : pred T') : image f [preim f of B] =i [predI B & codom f] FAILURE! Tactics applied: 10000 Original Proof: [by move=> y; rewrite /image_mem -filter_map /= mem_filter -enumT.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 373 Number of failed tactic applications: 9628 Results for fold 87 Results for lemma canF_sym: : cancel g f FAILURE! Tactics applied: 1534 Original Proof: [exact/(bij_can_sym (injF_bij (can_inj fK))).] Proof search time: 0 min, 5 sec Number of successful tactic applications: 26 Number of failed tactic applications: 1508 Results for fold 88 Results for lemma map_preim: (s : seq T') : {subset s <= codom f} -> map f (preim_seq s) = s FAILURE! Tactics applied: 10000 Original Proof: [elim: s => //= y s IHs; case: pickP => [x /eqP fx_y | nfTy] fTs. by rewrite /= fx_y IHs // => z s_z; apply: fTs; exact: predU1r. by case/imageP: (fTs y (mem_head y s)) => x _ fx_y; case/eqP: (nfTy x).] Proof search time: 0 min, 20 sec Number of successful tactic applications: 427 Number of failed tactic applications: 9574 Results for fold 89 Results for lemma rev_ord_proof: n (i : 'I_n) : n - i.+1 < n FAILURE! Tactics applied: 10000 Original Proof: [by case: n i => [|n] [i lt_i_n] //; rewrite ltnS subSS leq_subr.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 3308 Number of failed tactic applications: 6693 Results for fold 90 Results for lemma card_tagged: : #|{: {i : I & T_ i}}| = sumn (map (fun i => #|T_ i|) (enum I)) FAILURE! Tactics applied: 10000 Original Proof: [rewrite cardE !enumT {1}unlock size_flatten /shape -map_comp. by congr (sumn _); apply: eq_map => i; rewrite /= size_map -enumT -cardE.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 396 Number of failed tactic applications: 9605 Results for fold 91 Results for lemma card_preim: (B : pred T') : #|[preim f of B]| = #|[predI codom f & B]| FAILURE! Tactics applied: 10000 Original Proof: [rewrite -card_image /=; apply: eq_card => y. by rewrite [y \in _]image_pre !inE andbC.] Proof search time: 0 min, 28 sec Number of successful tactic applications: 471 Number of failed tactic applications: 9530 Results for fold 92 Results for lemma eq_codom: (f g : T -> T') : f =1 g -> codom f = codom g FAILURE! Tactics applied: 10000 Original Proof: [exact: eq_image.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 367 Number of failed tactic applications: 9634 Results for fold 93 Results for lemma enum_rank_ord: n i : enum_rank i = cast_ord (esym (card_ord n)) i FAILURE! Tactics applied: 10000 Original Proof: [by apply: val_inj; rewrite insubdK ?index_enum_ord // card_ord [_ \in _]ltn_ord.] Proof search time: 0 min, 34 sec Number of successful tactic applications: 331 Number of failed tactic applications: 9670 Results for fold 94 Results for lemma sub_enum_uniq: : uniq sub_enum FAILURE! Tactics applied: 10000 Original Proof: [by rewrite pmap_sub_uniq // -enumT enum_uniq.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 322 Number of failed tactic applications: 9679 Results for fold 95 Results for lemma val_enum_ord: : map val (enum 'I_n) = iota 0 n FAILURE! Tactics applied: 10000 Original Proof: [by rewrite enumT unlock val_ord_enum.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 542 Number of failed tactic applications: 9459 Results for fold 96 Results for lemma cardC: A : #|A| + #|[predC A]| = #|T| FAILURE! Tactics applied: 10000 Original Proof: [by rewrite !cardE -!count_filter count_predC.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 309 Number of failed tactic applications: 9692 Results for fold 97 Results for lemma sum_enum_uniq: : uniq sum_enum FAILURE! Tactics applied: 10000 Original Proof: [rewrite cat_uniq -!enumT !(enum_uniq, map_inj_uniq); try by move=> ? ? []. by rewrite andbT; apply/hasP=> [[_ /mapP[x _ ->] /mapP[]]].] Proof search time: 0 min, 21 sec Number of successful tactic applications: 305 Number of failed tactic applications: 9696 Results for fold 98 Results for lemma leq_image_card: A : #|image f A| <= #|A| FAILURE! Tactics applied: 10000 Original Proof: [by rewrite (cardE A) -(size_map f) card_size.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 380 Number of failed tactic applications: 9621 Results for fold 99 Results for lemma nth_image: T' y0 (f : T -> T') A (i : 'I_#|A|) : nth y0 (image f A) i = f (enum_val i) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -(nth_map _ y0) // -cardE.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 316 Number of failed tactic applications: 9685 Results for fold 100 Results for lemma eq_subset: A1 A2 : A1 =i A2 -> subset (mem A1) =1 subset (mem A2) FAILURE! Tactics applied: 10000 Original Proof: [move=> eqA12 [B]; rewrite !unlock; congr (_ == 0). by apply: eq_card => x; rewrite inE /= eqA12.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 279 Number of failed tactic applications: 9722 Results for fold 101 Results for lemma negb_exists_in: D P : ~~ [exists (x | D x), P x] = [forall (x | D x), ~~ P x] FAILURE! Tactics applied: 10000 Original Proof: [by rewrite negb_exists; apply/eq_forallb => x; rewrite [~~ _]fun_if.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 221 Number of failed tactic applications: 9780 Results for fold 102 Results for lemma subset_disjoint: A B : (A \subset B) = [disjoint A & [predC B]] FAILURE! Tactics applied: 10000 Original Proof: [by rewrite disjoint_sym unlock.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 296 Number of failed tactic applications: 9705 Results for fold 103 Results for lemma properE: A B : A \proper B = (A \subset B) && ~~(B \subset A) SUCCESS! Proof Found in EFSM: rewrite /= ?ltn_ord // ltnNge leq_addr. Tactics applied: 131 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: 130 Results for fold 104 Results for lemma eq_forallb: P1 P2 : P1 =1 P2 -> [forall x, P1 x] = [forall x, P2 x] FAILURE! Tactics applied: 10000 Original Proof: [by move=> eqP12; apply/negb_inj/eq_existsb=> /= x; rewrite eqP12.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 409 Number of failed tactic applications: 9592 Results for fold 105 Results for lemma subset_leqif_card: A B : A \subset B -> #|A| <= #|B| ?= iff (B \subset A) FAILURE! Tactics applied: 10000 Original Proof: [move=> sAB; split; [exact: subset_leq_card | apply/eqP/idP]. by move/subset_cardP=> sABP; rewrite (eq_subset_r (sABP sAB)). by move=> sBA; apply: eq_card; apply/subset_eqP; rewrite sAB.] Proof search time: 0 min, 28 sec Number of successful tactic applications: 462 Number of failed tactic applications: 9539 Results for fold 106 Results for lemma bumpK: h : cancel (bump h) (unbump h) FAILURE! Tactics applied: 10000 Original Proof: [rewrite /bump /unbump => i. have [le_hi | lt_ih] := leqP h i; first by rewrite ltnS le_hi subn1. by rewrite ltnNge ltnW ?subn0.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 568 Number of failed tactic applications: 9433 Results for fold 107 Results for lemma canF_RL: x y : g x = y -> x = f y FAILURE! Tactics applied: 10000 Original Proof: [exact: canRL canF_sym.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 855 Number of failed tactic applications: 9146 Results for fold 108 Results for lemma forallP: P : reflect (forall x, P x) [forall x, P x] FAILURE! Tactics applied: 10000 Original Proof: [by apply: (iffP pred0P) => /= P_ x; rewrite /= ?P_ ?(negbFE (P_ x)).] Proof search time: 0 min, 22 sec Number of successful tactic applications: 527 Number of failed tactic applications: 9474 Results for fold 109 Results for lemma cardUI: A B : #|[predU A & B]| + #|[predI A & B]| = #|A| + #|B| FAILURE! Tactics applied: 10000 Original Proof: [by rewrite !cardE -!count_filter count_predUI.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 369 Number of failed tactic applications: 9632 Results for fold 110 Results for lemma enum_default: A : 'I_(#|A|) -> T FAILURE! Tactics applied: 10000 Original Proof: [by rewrite cardE; case: (enum A) => [|//] [].] Proof search time: 0 min, 17 sec Number of successful tactic applications: 451 Number of failed tactic applications: 9550 Results for fold 111 Results for lemma predX_prod_enum: (A1 : pred T1) (A2 : pred T2) : count [predX A1 & A2] prod_enum = #|A1| * #|A2| FAILURE! Tactics applied: 10000 Original Proof: [rewrite !cardE -!count_filter -!enumT /prod_enum. elim: (enum T1) => //= x1 s1 IHs; rewrite count_cat {}IHs count_map /preim /=. by case: (x1 \in A1); rewrite ?count_pred0.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 2570 Number of failed tactic applications: 7431 Results for fold 112 Results for lemma eq_card_prod: (A : pred (T1 * T2)) : A =i predT -> #|A| = #|T1| * #|T2| FAILURE! Tactics applied: 10000 Original Proof: [exact: eq_card_trans card_prod.] Proof search time: 0 min, 28 sec Number of successful tactic applications: 545 Number of failed tactic applications: 9456 Results for fold 113 Results for lemma arg_minP: : extremum_spec leq arg_min FAILURE! Tactics applied: 10000 Original Proof: [rewrite /arg_min; case: pickP => [i /andP[Pi /forallP/= min_i] | no_i]. by split=> // j; apply/implyP. case/ex_minnP: exFP => n ex_i min_i; case/pred0P: ex_i => i /=. apply: contraFF (no_i i) => /andP[Pi /eqP def_n]; rewrite /= Pi. by apply/forall_inP=> j Pj; rewrite def_n min_i ?FP_F.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 347 Number of failed tactic applications: 9654 Results for fold 114 Results for lemma cast_ord_proof: n m (i : 'I_n) : n = m -> i < m FAILURE! Tactics applied: 10000 Original Proof: [by move <-.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 415 Number of failed tactic applications: 9586 Results for fold 115 Results for lemma enum_valP: A i : @enum_val A i \in A FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -mem_enum mem_nth -?cardE.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 710 Number of failed tactic applications: 9291 Results for fold 116 Results for lemma lshift_subproof: m n (i : 'I_m) : i < m + n FAILURE! Tactics applied: 10000 Original Proof: [by apply: leq_trans (valP i) _; exact: leq_addr.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 699 Number of failed tactic applications: 9302 Results for fold 117 Results for lemma pre_image: A : [preim f of image f A] =i A FAILURE! Tactics applied: 10000 Original Proof: [by move=> x; rewrite inE /= mem_image.] Proof search time: 0 min, 27 sec Number of successful tactic applications: 831 Number of failed tactic applications: 9170 Results for fold 118 Results for lemma unbumpK: h : {in predC1 h, cancel (unbump h) (bump h)} FAILURE! Tactics applied: 10000 Original Proof: [by move=> i; move/negbTE=> neq_h_i; rewrite unbumpKcond neq_h_i.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 399 Number of failed tactic applications: 9602 Results for fold 119 Results for lemma canF_eq: x y : (f x == y) = (x == g y) FAILURE! Tactics applied: 10000 Original Proof: [exact: (can2_eq fK canF_sym).] Proof search time: 0 min, 28 sec Number of successful tactic applications: 2366 Number of failed tactic applications: 7635 Results for fold 120 Results for lemma rev_ordK: n : involutive (@rev_ord n) FAILURE! Tactics applied: 10000 Original Proof: [by case: n => [|n] [i lti] //; apply: val_inj; rewrite /= !subSS subKn.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 1470 Number of failed tactic applications: 8531 Results for fold 121 Results for lemma eq_invF: f g injf injg : f =1 g -> @invF T f injf =1 @invF T g injg FAILURE! Tactics applied: 10000 Original Proof: [by move=> eq_fg x; apply: (canLR (invF_f injf)); rewrite eq_fg f_invF.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 1624 Number of failed tactic applications: 8377 Results for fold 122 Results for lemma unlift_some: n (h i : 'I_n) : h != i -> {j | i = lift h j & unlift h i = Some j} FAILURE! Tactics applied: 10000 Original Proof: [rewrite eq_sym => /eqP neq_ih. by case Dui: (unlift h i) / (unliftP h i) => [j Dh|//]; exists j.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 281 Number of failed tactic applications: 9720 Results for fold 123 Results for lemma ltn_ord: (i : ordinal) : i < n SUCCESS! Proof Found in EFSM: exact : valP i. Tactics applied: 39 Original Proof: [exact: valP i.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 5 sec Number of successful tactic applications: 1 Number of failed tactic applications: 38 Results for fold 124 Results for lemma pred0P: P : reflect (P =1 pred0) (pred0b P) FAILURE! Tactics applied: 10000 Original Proof: [apply: (iffP eqP); [exact: card0_eq | exact: eq_card0].] Proof search time: 0 min, 25 sec Number of successful tactic applications: 2466 Number of failed tactic applications: 7535 Results for fold 125 Results for lemma image_codom: A : {subset image f A <= codom f} FAILURE! Tactics applied: 10000 Original Proof: [by move=> _ /imageP[x _ ->]; exact: codom_f.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 930 Number of failed tactic applications: 9071 Results for fold 126 Results for lemma subset_cardP: A B : #|A| = #|B| -> reflect (A =i B) (A \subset B) FAILURE! Tactics applied: 10000 Original Proof: [move=> eqcAB; case: (subsetP A B) (subset_eqP A B) => //= sAB. case: (subsetP B A) => [//|[]] x Bx; apply/idPn => Ax. case/idP: (ltnn #|A|); rewrite {2}eqcAB (cardD1 x B) Bx /=. apply: subset_leq_card; apply/subsetP=> y Ay; rewrite inE /= andbC. by rewrite sAB //; apply/eqP => eqyx; rewrite -eqyx Ay in Ax.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 966 Number of failed tactic applications: 9035 Results for fold 127 Results for lemma card_codom: : #|codom f| = #|T| SUCCESS! Proof Found in EFSM: apply : card_in_image; exact : in2W. Tactics applied: 1468 Original Proof: [exact: card_image.] Shorter Proof Found? no Proof reused from card_image This proof contained a loop around a state proof search time: 0 min, 4 sec Number of successful tactic applications: 61 Number of failed tactic applications: 1407 Results for fold 128 Results for lemma dinjectiveP: D : reflect {in D &, injective f} (dinjectiveb D) FAILURE! Tactics applied: 378 Original Proof: [rewrite -[dinjectiveb D]negbK. case: dinjectivePn=> [noinjf | injf]; constructor. case: noinjf => x Dx [y /andP[neqxy /= Dy] eqfxy] injf. by case/eqP: neqxy; exact: injf. move=> x y Dx Dy /= eqfxy; apply/eqP; apply/idPn=> nxy; case: injf. by exists x => //; exists y => //=; rewrite inE /= eq_sym nxy.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 0 Number of failed tactic applications: 378 Results for fold 129 Results for lemma ord_inj: : injective nat_of_ord SUCCESS! Proof Found in EFSM: apply : val_inj; Tactics applied: 107 Original Proof: [exact: val_inj.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 37 Number of failed tactic applications: 70 Results for fold 130 Results for lemma exists_eqP: f1 f2 : reflect (exists x, f1 x = f2 x) [exists x, f1 x == f2 x] FAILURE! Tactics applied: 401 Original Proof: [by apply: (iffP (existsP _)) => [] [x /eqP]; exists x.] Proof search time: 0 min, 2 sec Number of successful tactic applications: 0 Number of failed tactic applications: 401 Results for fold 131 Results for lemma enum_valK_in: x0 A Ax0 : cancel enum_val (@enum_rank_in x0 A Ax0) FAILURE! Tactics applied: 10000 Original Proof: [move=> x; apply: ord_inj; rewrite insubdK; last first. by rewrite cardE [_ \in _]index_mem mem_nth // -cardE. by rewrite index_uniq ?enum_uniq // -cardE.] Proof search time: 0 min, 27 sec Number of successful tactic applications: 226 Number of failed tactic applications: 9775 Results for fold 132 Results for lemma injF_bij: : bijective f FAILURE! Tactics applied: 10000 Original Proof: [exact: inj_card_bij.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 957 Number of failed tactic applications: 9044 Results for fold 133 Results for lemma liftK: n (h : 'I_n) : pcancel (lift h) (unlift h) FAILURE! Tactics applied: 10000 Original Proof: [by move=> i; case: (unlift_some (neq_lift h i)) => j; move/lift_inj->.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 359 Number of failed tactic applications: 9642 Results for fold 134 Results for lemma cardC1: x : #|predC1 x| = #|T|.-1 FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -(cardC (pred1 x)) card1.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 661 Number of failed tactic applications: 9340 Results for fold 135 Results for lemma unsplitK: m n : cancel (@unsplit m n) (@split m n) FAILURE! Tactics applied: 10000 Original Proof: [move=> jk; have:= ltn_unsplit jk. by do [case: splitP; case: jk => //= i j] => [|/addnI] => /ord_inj->.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 470 Number of failed tactic applications: 9531 Results for fold 136 Results for lemma properP: A B : reflect (A \subset B /\ (exists2 x, x \in B & x \notin A)) (A \proper B) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite properE; apply: (iffP andP) => [] [-> /subsetPn].] Proof search time: 0 min, 17 sec Number of successful tactic applications: 98 Number of failed tactic applications: 9903 Results for fold 137 Results for lemma cast_ord_inj: n1 n2 eq_n : injective (@cast_ord n1 n2 eq_n) FAILURE! Tactics applied: 10000 Original Proof: [exact: can_inj (cast_ordK eq_n).] Proof search time: 0 min, 22 sec Number of successful tactic applications: 498 Number of failed tactic applications: 9503 Results for fold 138 Results for lemma mem_ord_enum: i : i \in ord_enum FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -(mem_map ord_inj) val_ord_enum mem_iota ltn_ord.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 306 Number of failed tactic applications: 9695 Results for fold 139 Results for lemma cast_ord_id: n eq_n i : cast_ord eq_n i = i :> 'I_n SUCCESS! Proof Found in EFSM: exact : val_inj. Tactics applied: 60 Original Proof: [exact: val_inj.] 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: 59 Results for fold 140 Results for lemma cardU1: x A : #|[predU1 x & A]| = (x \notin A) + #|A| FAILURE! Tactics applied: 10000 Original Proof: [case Ax: (x \in A). by apply: eq_card => y; rewrite inE /=; case: eqP => // ->. rewrite /= -(card1 x) -cardUI addnC. rewrite [#|predI _ _|]eq_card0 => [|y /=]; first exact: eq_card. by rewrite !inE; case: eqP => // ->.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 434 Number of failed tactic applications: 9567 Results for fold 141 Results for lemma eqfun_inP: D f1 f2 : reflect {in D, forall x, f1 x = f2 x} [forall (x | x \in D), f1 x == f2 x] FAILURE! Tactics applied: 10000 Original Proof: [by apply: (iffP (forall_inP _ _)) => eq_f12 x Dx; apply/eqP/eq_f12.] Proof search time: 0 min, 32 sec Number of successful tactic applications: 331 Number of failed tactic applications: 9670 Results for fold 142 Results for lemma rshift_subproof: m n (i : 'I_n) : m + i < m + n FAILURE! Tactics applied: 10000 Original Proof: [by rewrite ltn_add2l.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 318 Number of failed tactic applications: 9683 Results for fold 143 Results for lemma eq_card: A B : A =i B -> #|A| = #|B| FAILURE! Tactics applied: 10000 Original Proof: [by move=>eqAB; rewrite !cardE (eq_enum eqAB).] Proof search time: 0 min, 22 sec Number of successful tactic applications: 450 Number of failed tactic applications: 9551 Results for fold 144 Results for lemma subset_all: s A : (s \subset A) = all (mem A) s FAILURE! Tactics applied: 10000 Original Proof: [by exact (sameP (subsetP _ _) allP).] Proof search time: 0 min, 23 sec Number of successful tactic applications: 345 Number of failed tactic applications: 9656 Results for fold 145 Results for lemma subsetPn: A B : reflect (exists2 x, x \in A & x \notin B) (~~ (A \subset B)) FAILURE! Tactics applied: 10000 Original Proof: [rewrite unlock; apply: (iffP (pred0Pn _)) => [[x] | [x Ax nBx]]. by case/andP; exists x. by exists x; rewrite /= nBx.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 153 Number of failed tactic applications: 9848 Results for fold 146 Results for lemma mem_iinv: A y fAy : @iinv A y fAy \in A FAILURE! Tactics applied: 10000 Original Proof: [exact: s2valP (iinv_proof fAy).] Proof search time: 0 min, 23 sec Number of successful tactic applications: 288 Number of failed tactic applications: 9713 Results for fold 147 Results for lemma eq_card1: x A : A =i pred1 x -> #|A| = 1 FAILURE! Tactics applied: 10000 Original Proof: [exact: eq_card_trans (card1 x).] Proof search time: 0 min, 21 sec Number of successful tactic applications: 464 Number of failed tactic applications: 9537 Results for fold 148 Results for lemma disjoint0: A : [disjoint pred0 & A] FAILURE! Tactics applied: 10000 Original Proof: [exact/pred0P.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 293 Number of failed tactic applications: 9708 Results for fold 149 Results for lemma inj_card_bij: : bijective f FAILURE! Tactics applied: 10000 Original Proof: [by exists (fun y => iinv (inj_card_onto y)) => y; rewrite ?iinv_f ?f_iinv.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 408 Number of failed tactic applications: 9593 Results for fold 150 Results for lemma eq_subset_r: B1 B2 : B1 =i B2 -> (@subset T)^~ (mem B1) =1 (@subset T)^~ (mem B2) FAILURE! Tactics applied: 10000 Original Proof: [move=> eqB12 [A]; rewrite !unlock; congr (_ == 0). by apply: eq_card => x; rewrite !inE /= eqB12.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 435 Number of failed tactic applications: 9566 Results for fold 151 Results for lemma enum_rank_bij: : bijective enum_rank FAILURE! Tactics applied: 10000 Original Proof: [by move: enum_rankK enum_valK; exists (@enum_val T).] Proof search time: 0 min, 23 sec Number of successful tactic applications: 301 Number of failed tactic applications: 9700 Results for fold 152 Results for lemma enum_valK: : cancel enum_val enum_rank FAILURE! Tactics applied: 10000 Original Proof: [by move=> x; exact: enum_valK_in.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 415 Number of failed tactic applications: 9586 Results for fold 153 Results for lemma enum_val_bij: : bijective (@enum_val T) FAILURE! Tactics applied: 10000 Original Proof: [by move: enum_rankK enum_valK; exists enum_rank.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 2762 Number of failed tactic applications: 7239 Results for fold 154 Results for lemma val_sub_enum: : map val sub_enum = enum P FAILURE! Tactics applied: 10000 Original Proof: [rewrite pmap_filter; last exact: insubK. by apply: eq_filter => x; exact: isSome_insub.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 415 Number of failed tactic applications: 9586 Results for fold 155 Results for lemma sub_proper_trans: A B C : A \subset B -> B \proper C -> A \proper C FAILURE! Tactics applied: 10000 Original Proof: [move=> sAB /properP[sBC [x Cx nBx]]; rewrite properE (subset_trans sAB) //. by apply/subsetPn; exists x => //; apply: contra nBx; exact: subsetP.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 506 Number of failed tactic applications: 9495 Results for fold 156 Results for lemma lift_max: (i : 'I_n') : lift ord_max i = i :> nat FAILURE! Tactics applied: 10000 Original Proof: [by rewrite /= /bump leqNgt ltn_ord.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 306 Number of failed tactic applications: 9695 Results for fold 157 Results for lemma eq_disjoint: A1 A2 : A1 =i A2 -> disjoint (mem A1) =1 disjoint (mem A2) FAILURE! Tactics applied: 10000 Original Proof: [by move=> eqA12 [B]; congr (_ == 0); apply: eq_card => x; rewrite !inE eqA12.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 878 Number of failed tactic applications: 9123 Results for fold 158 Results for lemma disjointU1: x A B : [disjoint predU1 x A & B] = (x \notin B) && [disjoint A & B] FAILURE! Tactics applied: 10000 Original Proof: [by rewrite disjointU disjoint1.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 421 Number of failed tactic applications: 9580 Results for fold 159 Results for lemma arg_maxP: : extremum_spec geq arg_max FAILURE! Tactics applied: 640 Original Proof: [rewrite /arg_max; case: pickP => [i /andP[Pi /forall_inP/= max_i] | no_i]. by split=> // j; apply/implyP. have (n): FP n -> n <= foldr maxn 0 (map F (enum P)). case/existsP=> i; rewrite -[P i]mem_enum andbC /= => /andP[/eqP <-]. elim: (enum P) => //= j e IHe; rewrite leq_max orbC !inE. by case/predU1P=> [-> | /IHe-> //]; rewrite leqnn orbT. case/ex_maxnP=> // n ex_i max_i; case/pred0P: ex_i => i /=. apply: contraFF (no_i i) => /andP[Pi def_n]; rewrite /= Pi. by apply/forall_inP=> j Pj; rewrite (eqP def_n) max_i ?FP_F.] Proof search time: 0 min, 3 sec Number of successful tactic applications: 9 Number of failed tactic applications: 631 Results for fold 160 Results for lemma eq_card0: A : A =i pred0 -> #|A| = 0 FAILURE! Tactics applied: 10000 Original Proof: [exact: eq_card_trans card0.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 359 Number of failed tactic applications: 9642 Results for fold 161 Results for lemma injectivePn: : reflect (exists x, exists2 y, x != y & f x = f y) (~~ injectiveb) FAILURE! Tactics applied: 422 Original Proof: [apply: (iffP (dinjectivePn _)) => [[x _ [y nxy eqfxy]] | [x [y nxy eqfxy]]]; by exists x => //; exists y => //; rewrite inE /= andbT eq_sym in nxy *.] Proof search time: 0 min, 2 sec Number of successful tactic applications: 0 Number of failed tactic applications: 422 Results for fold 162 Results for lemma codomE: : codom f = map f (enum T) SUCCESS! Proof Found in EFSM: constructor ; Tactics applied: 121 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 1 Number of failed tactic applications: 120 Results for fold 163 Results for lemma invF_f: : cancel f invF SUCCESS! Proof Found in EFSM: move => Ax0; apply : injf => //; exact : f_iinv. Tactics applied: 1784 Original Proof: [by move=> x; exact: iinv_f.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 5 sec Number of successful tactic applications: 97 Number of failed tactic applications: 1687 Results for fold 164 Results for lemma subxx: (pT : predType T) (pA : pT) : pA \subset pA SUCCESS! Proof Found in EFSM: by []. Tactics applied: 151 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: 150 Results for fold 165 Results for lemma bij_on_codom: (x0 : T) : {on [pred y in codom f], bijective f} FAILURE! Tactics applied: 10000 Original Proof: [pose g y := iinv (valP (insigd (codom_f x0) y)). by exists g => [x fAfx | y fAy]; first apply: injf; rewrite f_iinv insubdK.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 298 Number of failed tactic applications: 9703 Results for fold 166 Results for lemma unliftP: n (h i : 'I_n) : unlift_spec h i (unlift h i) FAILURE! Tactics applied: 10000 Original Proof: [rewrite /unlift; case: insubP => [u nhi | ] def_i /=; constructor. by apply: val_inj; rewrite /= def_i unbumpK. by rewrite negbK in def_i; exact/eqP.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 79 Number of failed tactic applications: 9922 Results for fold 167 Results for lemma subxx_hint: (mA : mem_pred T) : subset mA mA FAILURE! Tactics applied: 10000 Original Proof: [by case: mA => A; have:= introT (subsetP A A); rewrite !unlock => ->.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 347 Number of failed tactic applications: 9654 Results for fold 168 Results for lemma image_pred0: : image f pred0 =i pred0 FAILURE! Tactics applied: 10000 Original Proof: [by move=> x; rewrite /image_mem /= enum0.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 274 Number of failed tactic applications: 9727 Results for fold 169 Results for lemma unbumpKcond: h i : bump h (unbump h i) = (i == h) + i FAILURE! Tactics applied: 10000 Original Proof: [rewrite /bump /unbump leqNgt -subSKn. case: (ltngtP i h) => /= [-> | ltih | ->] //; last by rewrite ltnn. by rewrite subn1 /= leqNgt !(ltn_predK ltih, ltih, add1n).] Proof search time: 0 min, 18 sec Number of successful tactic applications: 401 Number of failed tactic applications: 9600 Results for fold 170 Results for lemma predT_subset: A : T \subset A -> forall x, x \in A FAILURE! Tactics applied: 10000 Original Proof: [move/subsetP=> allA x; exact: allA.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 428 Number of failed tactic applications: 9573 Results for fold 171 Results for lemma lift_subproof: n h (i : 'I_n.-1) : bump h i < n FAILURE! Tactics applied: 10000 Original Proof: [by case: n i => [[]|n] //= i; rewrite -addnS (leq_add (leq_b1 _)).] Proof search time: 0 min, 24 sec Number of successful tactic applications: 374 Number of failed tactic applications: 9627 Results for fold 172 Results for lemma enum_rank_inj: : injective enum_rank FAILURE! Tactics applied: 10000 Original Proof: [exact: can_inj enum_rankK.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 325 Number of failed tactic applications: 9676 Results for fold 173 Results for lemma eq_card_trans: A B n : #|A| = n -> B =i A -> #|B| = n FAILURE! Tactics applied: 10000 Original Proof: [move <-; exact: eq_card.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 2010 Number of failed tactic applications: 7991 Results for fold 174 Results for lemma enum_ordS: : enum 'I_n = ord0 :: map (lift ord0) (enum 'I_n') FAILURE! Tactics applied: 10000 Original Proof: [apply: (inj_map val_inj); rewrite val_enum_ord /= -map_comp. by rewrite (map_comp (addn 1)) val_enum_ord -iota_addl.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 652 Number of failed tactic applications: 9349 Results for fold 175 Results for lemma size_codom: : size (codom f) = #|T| SUCCESS! Proof Found in EFSM: by rewrite size_map -cardE. Tactics applied: 337 Original Proof: [exact: size_image.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 6 Number of failed tactic applications: 331 Results for fold 176 Results for lemma unbump_addl: h i k : unbump (k + h) (k + i) = k + unbump h i FAILURE! Tactics applied: 10000 Original Proof: [apply: (can_inj (bumpK (k + h))). by rewrite bump_addl !unbumpKcond eqn_add2l addnCA.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 218 Number of failed tactic applications: 9783 Results for fold 177 Results for lemma f_iinv: A y fAy : f (@iinv A y fAy) = y FAILURE! Tactics applied: 10000 Original Proof: [exact: s2valP' (iinv_proof fAy).] Proof search time: 0 min, 24 sec Number of successful tactic applications: 452 Number of failed tactic applications: 9549 Results for fold 178 Results for lemma mem_sub_enum: u : u \in sub_enum FAILURE! Tactics applied: 10000 Original Proof: [by rewrite mem_pmap_sub -enumT mem_enum.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 344 Number of failed tactic applications: 9657 Results for fold 179 Results for lemma disjoint_has: s A : [disjoint s & A] = ~~ has (mem A) s FAILURE! Tactics applied: 10000 Original Proof: [rewrite -(@eq_has _ (mem (enum A))) => [|x]; last exact: mem_enum. rewrite has_sym has_filter -filter_predI -has_filter has_count -eqn0Ngt. by rewrite count_filter /disjoint /pred0b unlock.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 488 Number of failed tactic applications: 9513 Results for fold 180 Results for lemma eqfunP: f1 f2 : reflect (forall x, f1 x = f2 x) [forall x, f1 x == f2 x] FAILURE! Tactics applied: 10000 Original Proof: [by apply: (iffP (forallP _)) => eq_f12 x; apply/eqP/eq_f12.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 226 Number of failed tactic applications: 9775 Results for fold 181 Results for lemma proper_trans: A B C : A \proper B -> B \proper C -> A \proper C FAILURE! Tactics applied: 10000 Original Proof: [case/properP=> sAB [x Bx nAx] /properP[sBC [y Cy nBy]]. rewrite properE (subset_trans sAB) //=; apply/subsetPn; exists y => //. by apply: contra nBy; exact: subsetP.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 509 Number of failed tactic applications: 9492 Results for fold 182 Results for lemma leq_bump: h i j : (i <= bump h j) = (unbump h i <= j) FAILURE! Tactics applied: 10000 Original Proof: [rewrite /bump leq_subLR. case: (leqP i h) (leqP h j) => [le_i_h | lt_h_i] [le_h_j | lt_j_h] //. by rewrite leqW (leq_trans le_i_h). by rewrite !(leqNgt i) ltnW (leq_trans _ lt_h_i).] Proof search time: 0 min, 28 sec Number of successful tactic applications: 317 Number of failed tactic applications: 9684 Results for fold 183 Results for lemma uniq_enumP: e : uniq e -> e =i T -> axiom e FAILURE! Tactics applied: 10000 Original Proof: [by move=> Ue sT x; rewrite count_uniq_mem ?sT.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 634 Number of failed tactic applications: 9367 Results for fold 184 Results for lemma cardE: A : #|A| = size (enum A) SUCCESS! Proof Found in EFSM: by rewrite unlock. Tactics applied: 286 Original Proof: [by rewrite unlock.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 3 Number of failed tactic applications: 283 Results for fold 185 Results for lemma properxx: A : (A \proper A) = false SUCCESS! Proof Found in EFSM: by rewrite properE subxx. Tactics applied: 448 Original Proof: [by rewrite properE subxx.] 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: 442 Results for fold 186 Results for lemma mem_image: A x : (f x \in image f A) = (x \in A) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite mem_map ?mem_enum.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 294 Number of failed tactic applications: 9707 Results for fold 187 Results for lemma tag_enumP: : Finite.axiom tag_enum FAILURE! Tactics applied: 10000 Original Proof: [case=> i x; rewrite -(enumP i) /tag_enum -enumT. elim: (enum I) => //= j e IHe. rewrite count_cat count_map {}IHe; congr (_ + _). rewrite count_filter -cardE /=; case: eqP => [-> | ne_j_i]. by apply: (@eq_card1 _ x) => y; rewrite -topredE /= tagged_asE ?eqxx. by apply: eq_card0 => y.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 91 Number of failed tactic applications: 9910 Results for fold 188 Results for lemma card_prod: : #|{: T1 * T2}| = #|T1| * #|T2| SUCCESS! Proof Found in EFSM: by rewrite -predX_prod_enum unlock -count_filter unlock. Tactics applied: 303 Original Proof: [by rewrite -cardX; apply: eq_card; case.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 3 Number of failed tactic applications: 300 Results for fold 189 Results for lemma enum_rank_subproof: x0 A : x0 \in A -> 0 < #|A| FAILURE! Tactics applied: 10000 Original Proof: [by move=> Ax0; rewrite (cardD1 x0) Ax0.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 393 Number of failed tactic applications: 9608 Results for fold 190 Results for lemma unbumpS: h i : unbump h.+1 i.+1 = (unbump h i).+1 FAILURE! Tactics applied: 10000 Original Proof: [exact: unbump_addl 1.] Proof search time: 0 min, 28 sec Number of successful tactic applications: 165 Number of failed tactic applications: 9836 Results for fold 191 Results for lemma subset_trans: A B C : A \subset B -> B \subset C -> A \subset C FAILURE! Tactics applied: 10000 Original Proof: [by move/subsetP=> sAB /subsetP=> sBC; apply/subsetP=> x /sAB; exact: sBC.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 543 Number of failed tactic applications: 9458 Results for fold 192 Results for lemma splitP: m n (i : 'I_(m + n)) : split_spec i (split i) (i < m) FAILURE! Tactics applied: 10000 Original Proof: [rewrite /split {-3}/leq. by case: (@ltnP i m) => cmp_i_m //=; constructor; rewrite ?subnKC.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 3666 Number of failed tactic applications: 6335 Results for fold 193 Results for lemma injectiveP: : reflect (injective f) injectiveb FAILURE! Tactics applied: 10000 Original Proof: [apply: (iffP (dinjectiveP _)) => injf x y => [|_ _]; exact: injf.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 3337 Number of failed tactic applications: 6664 Results for fold 194 Results for lemma eq_proper_r: A B : A =i B -> (@proper T)^~ (mem A) =1 (@proper T)^~ (mem B) FAILURE! Tactics applied: 10000 Original Proof: [move=> eAB [C]; congr (_ && _); first exact: (eq_subset_r eAB). by rewrite (eq_subset eAB).] Proof search time: 0 min, 25 sec Number of successful tactic applications: 369 Number of failed tactic applications: 9632 Results for fold 195 Results for lemma cardID: B A : #|[predI A & B]| + #|[predD A & B]| = #|A| FAILURE! Tactics applied: 10000 Original Proof: [rewrite -cardUI addnC [#|predI _ _|]eq_card0 => [|x] /=. by apply: eq_card => x; rewrite !inE andbC -andb_orl orbN. by rewrite !inE -!andbA andbC andbA andbN.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 534 Number of failed tactic applications: 9467 Results for fold 196 Results for lemma bumpS: h i : bump h.+1 i.+1 = (bump h i).+1 FAILURE! Tactics applied: 854 Original Proof: [exact: addnS.] Proof search time: 0 min, 2 sec Number of successful tactic applications: 8 Number of failed tactic applications: 846 Results for fold 197 Results for lemma subsetP: A B : reflect {subset A <= B} (A \subset B) FAILURE! Tactics applied: 10000 Original Proof: [rewrite unlock; apply: (iffP (pred0P _)) => [AB0 x | sAB x /=]. by apply/implyP; apply/idPn; rewrite negb_imply andbC [_ && _]AB0. by rewrite andbC -negb_imply; apply/negbF/implyP; exact: sAB.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 2120 Number of failed tactic applications: 7881 Results for fold 198 Results for lemma negb_forall: P : ~~ [forall x, P x] = [exists x, ~~ P x] SUCCESS! Proof Found in EFSM: by []. Tactics applied: 58 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: 57 Results for fold 199 Results for lemma size_enum_ord: : size (enum 'I_n) = n FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -(size_map val) val_enum_ord size_iota.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 319 Number of failed tactic applications: 9682 Results for fold 200 Results for lemma inj_card_onto: y : y \in codom f FAILURE! Tactics applied: 10000 Original Proof: [by move: y; apply/subset_cardP; rewrite ?card_codom ?subset_predT.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 238 Number of failed tactic applications: 9763 Results for fold 201 Results for lemma proper_sub: A B : A \proper B -> A \subset B SUCCESS! Proof Found in EFSM: by case/andP. Tactics applied: 343 Original Proof: [by case/andP.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 27 Number of failed tactic applications: 316 Results for fold 202 Results for lemma ltn_unsplit: m n (jk : 'I_m + 'I_n) : (unsplit jk < m) = jk FAILURE! Tactics applied: 10000 Original Proof: [by case: jk => [j|k]; rewrite /= ?ltn_ord // ltnNge leq_addr.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 229 Number of failed tactic applications: 9772 Results for fold 203 Results for lemma leq_bump2: h i j : (bump h i <= bump h j) = (i <= j) FAILURE! Tactics applied: 583 Original Proof: [by rewrite leq_bump bumpK.] Proof search time: 0 min, 2 sec Number of successful tactic applications: 6 Number of failed tactic applications: 577 Results for fold 204 Results for lemma val_ord_enum: : map val ord_enum = iota 0 n FAILURE! Tactics applied: 10000 Original Proof: [rewrite pmap_filter; last exact: insubK. by apply/all_filterP; apply/allP=> i; rewrite mem_iota isSome_insub.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 279 Number of failed tactic applications: 9722 Results for fold 205 Results for lemma disjoint_cat: s1 s2 A : [disjoint s1 ++ s2 & A] = [disjoint s1 & A] && [disjoint s2 & A] FAILURE! Tactics applied: 10000 Original Proof: [by rewrite !disjoint_has has_cat negb_or.] Proof search time: 0 min, 27 sec Number of successful tactic applications: 334 Number of failed tactic applications: 9667 Results for fold 206 Results for lemma enumP: : Finite.axiom (Finite.enum T) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite unlock; case T => ? [? []].] Proof search time: 0 min, 22 sec Number of successful tactic applications: 396 Number of failed tactic applications: 9605 Results for fold 207 Results for lemma enum_val_ord: n i : enum_val i = cast_ord (card_ord n) i FAILURE! Tactics applied: 10000 Original Proof: [by apply: canLR (@enum_rankK _) _; apply: val_inj; rewrite enum_rank_ord.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 313 Number of failed tactic applications: 9688 Results for fold 208 Results for lemma card_size: s : #|s| <= size s FAILURE! Tactics applied: 10000 Original Proof: [elim: s => [|x s IHs] /=; first by rewrite card0. rewrite cardU1 /=; case: (~~ _) => //; exact: leqW.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 224 Number of failed tactic applications: 9777 Results for fold 209 Results for lemma cardX: (A1 : pred T1) (A2 : pred T2) : #|[predX A1 & A2]| = #|A1| * #|A2| FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -predX_prod_enum unlock -count_filter unlock.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 300 Number of failed tactic applications: 9701 Results for fold 210 Results for lemma pcan_enumP: g : pcancel f g -> Finite.axiom (undup (pmap g (enumF fT))) FAILURE! Tactics applied: 10000 Original Proof: [move=> fK x; rewrite count_uniq_mem ?undup_uniq // mem_undup. by rewrite mem_pmap -fK map_f // -enumT mem_enum.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 247 Number of failed tactic applications: 9754 Results for fold 211 Results for lemma eq_existsb_in: D P1 P2 : (forall x, D x -> P1 x = P2 x) -> [exists (x | D x), P1 x] = [exists (x | D x), P2 x] FAILURE! Tactics applied: 10000 Original Proof: [by move=> eqP12; apply: eq_existsb => x; apply: andb_id2l => /eqP12.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 402 Number of failed tactic applications: 9599 Results for fold 212 Results for lemma card_sum: : #|{: T1 + T2}| = #|T1| + #|T2| FAILURE! Tactics applied: 10000 Original Proof: [by rewrite !cardT !enumT {1}unlock size_cat !size_map.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 506 Number of failed tactic applications: 9495 Results for fold 213 Results for lemma lift0: (i : 'I_n') : lift ord0 i = i.+1 :> nat SUCCESS! Proof Found in EFSM: by []. Tactics applied: 146 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Number of successful tactic applications: 3 Number of failed tactic applications: 143 Results for fold 214 Results for lemma card_ord: : #|'I_n| = n FAILURE! Tactics applied: 10000 Original Proof: [by rewrite cardE size_enum_ord.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 344 Number of failed tactic applications: 9657 Results for fold 215 Results for lemma nth_enum_rank_in: x00 x0 A Ax0 : {in A, cancel (@enum_rank_in x0 A Ax0) (nth x00 (enum A))} FAILURE! Tactics applied: 10000 Original Proof: [move=> x Ax; rewrite /= insubdK ?nth_index ?mem_enum //. by rewrite cardE [_ \in _]index_mem mem_enum.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 384 Number of failed tactic applications: 9617 Results for fold 216 Results for lemma eq_existsb: P1 P2 : P1 =1 P2 -> [exists x, P1 x] = [exists x, P2 x] FAILURE! Tactics applied: 10000 Original Proof: [by move=> eqP12; congr (_ != 0); apply: eq_card.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 263 Number of failed tactic applications: 9738 Results for fold 217 Results for lemma seq_sub_pickleK: : pcancel seq_sub_pickle seq_sub_unpickle FAILURE! Tactics applied: 10000 Original Proof: [rewrite /seq_sub_unpickle => x. by rewrite (nth_map x) ?nth_index ?index_mem ?mem_seq_sub_enum.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 345 Number of failed tactic applications: 9656 Results for fold 218 Results for lemma fin_all_exists: U (P : forall x : T, U x -> Prop) : (forall x, exists u, P x u) -> (exists u, forall x, P x (u x)) FAILURE! Tactics applied: 10000 Original Proof: [move=> ex_u; pose Q m x := enum_rank x < m -> {ux | P x ux}. suffices: forall m, m <= #|T| -> exists w : forall x, Q m x, True. case/(_ #|T|)=> // w _; pose u x := sval (w x (ltn_ord _)). by exists u => x; rewrite {}/u; case: (w x _). elim=> [|m IHm] ltmX; first by have w x: Q 0 x by []; exists w. have{IHm} [w _] := IHm (ltnW ltmX); pose i := Ordinal ltmX. have [u Pu] := ex_u (enum_val i); suffices w' x: Q m.+1 x by exists w'. rewrite /Q ltnS leq_eqVlt (val_eqE _ i); case: eqP => [def_i _ | _ /w //]. by rewrite -def_i enum_rankK in u Pu; exists u.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 290 Number of failed tactic applications: 9711 Results for fold 219 Results for lemma eq_proper: A B : A =i B -> proper (mem A) =1 proper (mem B) FAILURE! Tactics applied: 10000 Original Proof: [move=> eAB [C]; congr (_ && _); first exact: (eq_subset eAB). by rewrite (eq_subset_r eAB).] Proof search time: 0 min, 23 sec Number of successful tactic applications: 363 Number of failed tactic applications: 9638 Results for fold 220 Results for lemma card_sub: : #|sfT| = #|[pred x | P x]| FAILURE! Tactics applied: 10000 Original Proof: [by rewrite !cardE enumT unlock -(size_map val) val_sub_enum.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 317 Number of failed tactic applications: 9684 Results for fold 221 Results for lemma cardD1: x A : #|A| = (x \in A) + #|[predD1 A & x]| FAILURE! Tactics applied: 10000 Original Proof: [case Ax: (x \in A); last first. by apply: eq_card => y; rewrite !inE /=; case: eqP => // ->. rewrite /= -(card1 x) -cardUI addnC /=. rewrite [#|predI _ _|]eq_card0 => [|y]; last by rewrite !inE; case: eqP. by apply: eq_card => y; rewrite !inE; case: eqP => // ->.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 256 Number of failed tactic applications: 9745 Results for fold 222 Results for lemma card_unit: : #|{: unit}| = 1 SUCCESS! Proof Found in EFSM: by rewrite cardT enumT unlock. Tactics applied: 470 Original Proof: [by rewrite cardT enumT unlock.] 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: 467 Results for fold 223 Results for lemma lift_inj: n (h : 'I_n) : injective (lift h) FAILURE! Tactics applied: 10000 Original Proof: [move=> i1 i2; move/eqP; rewrite [_ == _](can_eq (@bumpK _)) => eq_i12. exact/eqP.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 1640 Number of failed tactic applications: 8361 Results for fold 224 Results for lemma image_injP: A : reflect {in A &, injective f} (#|image f A| == #|A|) FAILURE! Tactics applied: 10000 Original Proof: [apply: (iffP eqP) => [eqfA |]; last exact: card_in_image. by apply/dinjectiveP; apply/card_uniqP; rewrite size_map -cardE.] Proof search time: 0 min, 33 sec Number of successful tactic applications: 436 Number of failed tactic applications: 9565 Results for fold 225 Results for lemma mem_seq_sub_enum: x : x \in seq_sub_enum FAILURE! Tactics applied: 10000 Original Proof: [by rewrite mem_undup mem_pmap -valK map_f ?ssvalP.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 227 Number of failed tactic applications: 9774 Results for fold 226 Results for lemma enum_rankK: : cancel enum_rank enum_val SUCCESS! Proof Found in EFSM: rewrite /seq_sub_unpickle => x. exact : nth_enum_rank_in. Tactics applied: 2177 Original Proof: [by move=> x; exact: enum_rankK_in.] 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: 58 Number of failed tactic applications: 2119 Results for fold 227 Results for lemma cardT: : #|T| = size (enum T) SUCCESS! Proof Found in EFSM: by rewrite cardE; Tactics applied: 476 Original Proof: [by rewrite cardE.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 9 Number of failed tactic applications: 467 Results for fold 228 Results for lemma pred0Pn: P : reflect (exists x, P x) (~~ pred0b P) FAILURE! Tactics applied: 963 Original Proof: [case: (pickP P) => [x Px | P0]. by rewrite (introN (pred0P P)) => [|P0]; [left; exists x | rewrite P0 in Px]. by rewrite -lt0n eq_card0 //; right=> [[x]]; rewrite P0.] Proof search time: 0 min, 2 sec Number of successful tactic applications: 6 Number of failed tactic applications: 957 Results for fold 229 Results for lemma subset_pred1: A x : (pred1 x \subset A) = (x \in A) FAILURE! Tactics applied: 10000 Original Proof: [by apply/subsetP/idP=> [-> // | Ax y /eqP-> //]; exact: eqxx.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 492 Number of failed tactic applications: 9509 Results for fold 230 Results for lemma card_uniqP: s : reflect (#|s| = size s) (uniq s) FAILURE! Tactics applied: 10000 Original Proof: [elim: s => [|x s IHs]; first by left; exact card0. rewrite cardU1 /= /addn; case: {+}(x \in s) => /=. by right=> card_Ssz; have:= card_size s; rewrite card_Ssz ltnn. by apply: (iffP IHs) => [<-| [<-]].] Proof search time: 0 min, 16 sec Number of successful tactic applications: 93 Number of failed tactic applications: 9908 Results for fold 231 Results for lemma card2: x y : #|pred2 x y| = (x != y).+1 FAILURE! Tactics applied: 10000 Original Proof: [by rewrite cardU1 card1 addn1.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 273 Number of failed tactic applications: 9728 Results for fold 232 Results for lemma card_bool: : #|{: bool}| = 2 SUCCESS! Proof Found in EFSM: by rewrite cardT enumT unlock. Tactics applied: 384 Original Proof: [by rewrite cardT enumT unlock.] 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: 383 Results for fold 233 Results for lemma card_image: A : #|image f A| = #|A| FAILURE! Tactics applied: 10000 Original Proof: [apply: card_in_image; exact: in2W.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 419 Number of failed tactic applications: 9582 Results for fold 234 Results for lemma disjoint_cons: x s B : [disjoint x :: s & B] = (x \notin B) && [disjoint s & B] SUCCESS! Proof Found in EFSM: by rewrite disjointU disjoint1. Tactics applied: 348 Original Proof: [exact: disjointU1.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 2 Number of failed tactic applications: 346 Results for fold 235 Results for lemma unlift_none: n (h : 'I_n) : unlift h h = None FAILURE! Tactics applied: 10000 Original Proof: [by case: unliftP => // j Dh; case/eqP: (neq_lift h j).] Proof search time: 0 min, 21 sec Number of successful tactic applications: 309 Number of failed tactic applications: 9692 Results for fold 236 Results for lemma eq_disjoint_r: B1 B2 : B1 =i B2 -> (@disjoint T)^~ (mem B1) =1 (@disjoint T)^~ (mem B2) FAILURE! Tactics applied: 10000 Original Proof: [by move=> eqB12 [A]; congr (_ == 0); apply: eq_card => x; rewrite !inE eqB12.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 1410 Number of failed tactic applications: 8591 Results for fold 237 Results for lemma disjointU: A B C : [disjoint predU A B & C] = [disjoint A & C] && [disjoint B & C] FAILURE! Tactics applied: 576 Original Proof: [case: [disjoint A & C] / (pred0P (xpredI A C)) => [A0 | nA0] /=. by congr (_ == 0); apply: eq_card => x; rewrite [x \in _]andb_orl A0. apply/pred0P=> nABC; case: nA0 => x; apply/idPn=> /=; move/(_ x): nABC. by rewrite [_ x]andb_orl; case/norP.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 5 Number of failed tactic applications: 571 Results for fold 238 Results for lemma eq_card_sub: (A : pred sfT) : A =i predT -> #|A| = #|[pred x | P x]| FAILURE! Tactics applied: 10000 Original Proof: [exact: eq_card_trans card_sub.] Proof search time: 0 min, 30 sec Number of successful tactic applications: 1174 Number of failed tactic applications: 8827 Results for fold 239 Results for lemma proper_card: A B : A \proper B -> #|A| < #|B| FAILURE! Tactics applied: 10000 Original Proof: [by case/andP=> sAB nsBA; rewrite ltn_neqAle !(subset_leqif_card sAB) andbT.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 369 Number of failed tactic applications: 9632 Results for fold 240 Results for lemma cast_ord_comp: n1 n2 n3 eq_n2 eq_n3 i : @cast_ord n2 n3 eq_n3 (@cast_ord n1 n2 eq_n2 i) = cast_ord (etrans eq_n2 eq_n3) i SUCCESS! Proof Found in EFSM: exact : val_inj. Tactics applied: 83 Original Proof: [exact: val_inj.] 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: 82 Results for fold 241 Results for lemma imageP: A y : reflect (exists2 x, x \in A & y = f x) (y \in image f A) FAILURE! Tactics applied: 10000 Original Proof: [by apply: (iffP mapP) => [] [x Ax y_fx]; exists x; rewrite // mem_enum in Ax *.] Proof search time: 0 min, 30 sec Number of successful tactic applications: 3164 Number of failed tactic applications: 6837 Results for fold 242 Results for lemma card1: x : #|pred1 x| = 1 SUCCESS! Proof Found in EFSM: rewrite unlock; first by rewrite -count_filter enumP. Tactics applied: 1985 Original Proof: [by rewrite cardE enum1.] 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: 50 Number of failed tactic applications: 1935 Results for fold 243 Results for lemma eq_image: (A B : pred T) (f g : T -> T') : A =i B -> f =1 g -> image f A = image g B FAILURE! Tactics applied: 10000 Original Proof: [by move=> eqAB eqfg; rewrite /image_mem (eq_enum eqAB) (eq_map eqfg).] Proof search time: 0 min, 19 sec Number of successful tactic applications: 136 Number of failed tactic applications: 9865 OVERALL RESULTS SUMMARY EFSMProver proved 35 out of 243 lemmas. Success rate of 14.40329218106996% There were 0 errors. 208 proof attempts exhausted the automaton On average, a proof was found after applying 783 tactics The longest proof consisted of 3 tactics There were 1 shorter proofs found Of the 208 failures, 193 of them used all 10000 tactics There were 27 reused proofs found There were 8 novel proofs found Of the 208 failures, the average number of tactics used was 9357 On average, a proof was found after 0 min, 3 sec On average, a failed proof attempt took 0 min, 21 sec On average, any (success or failure) proof attempt took 0 min, 19 sec The longest time to find a proof was 0 min, 13 sec The shortest time to find a proof was 0 min, 0 sec There were 0 proofs containing repeated tactics There were 3 proofs that repeated states