Results for fold 1 Results for lemma uniq_enumP: e : uniq e -> e =i T -> axiom e FAILURE! Tactics applied: 2487 Original Proof: [by move=> Ue sT x; rewrite count_uniq_mem ?sT.] Proof search time: 0 min, 6 sec Number of successful tactic applications: 48 Number of failed tactic applications: 2439 Results for lemma exists_inP: D P : reflect (exists2 x, D x & P x) [exists (x | D x), P x] FAILURE! Tactics applied: 348 Original Proof: [by apply: (iffP pred0Pn) => [[x /andP[]] | [x]]; exists x => //; apply/andP.] Proof search time: 0 min, 12 sec Number of successful tactic applications: 0 Number of failed tactic applications: 348 Results for lemma proper_irrefl: A : ~~ (A \proper A) FAILURE! Tactics applied: 3199 Original Proof: [by rewrite properE subxx.] Proof search time: 0 min, 8 sec Number of successful tactic applications: 49 Number of failed tactic applications: 3150 Results for lemma lift_inj: n (h : 'I_n) : injective (lift h) FAILURE! Tactics applied: 8579 Original Proof: [move=> i1 i2; move/eqP; rewrite [_ == _](can_eq (@bumpK _)) => eq_i12. exact/eqP.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 189 Number of failed tactic applications: 8390 Results for lemma properxx: A : (A \proper A) = false FAILURE! Tactics applied: 10000 Original Proof: [by rewrite properE subxx.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 168 Number of failed tactic applications: 9833 Results for lemma enum_rank_bij: : bijective enum_rank FAILURE! Tactics applied: 4948 Original Proof: [by move: enum_rankK enum_valK; exists (@enum_val T).] Proof search time: 0 min, 10 sec Number of successful tactic applications: 82 Number of failed tactic applications: 4866 Results for lemma image_pre: (B : pred T') : image f [preim f of B] =i [predI B & codom f] FAILURE! Tactics applied: 5185 Original Proof: [by move=> y; rewrite /image_mem -filter_map /= mem_filter -enumT.] Proof search time: 0 min, 13 sec Number of successful tactic applications: 98 Number of failed tactic applications: 5087 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: 203 Original Proof: [exact: card_sub.] 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: 202 Results for lemma properP: A B : reflect (A \subset B /\ (exists2 x, x \in B & x \notin A)) (A \proper B) FAILURE! Tactics applied: 1266 Original Proof: [by rewrite properE; apply: (iffP andP) => [] [-> /subsetPn].] Proof search time: 0 min, 4 sec Number of successful tactic applications: 14 Number of failed tactic applications: 1252 Results for lemma val_seq_sub_enum: : uniq s -> map val seq_sub_enum = s FAILURE! Tactics applied: 6174 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, 14 sec Number of successful tactic applications: 132 Number of failed tactic applications: 6042 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, 24 sec Number of successful tactic applications: 210 Number of failed tactic applications: 9791 Results for lemma negb_forall: P : ~~ [forall x, P x] = [exists x, ~~ P x] SUCCESS! Proof Found in EFSM: constructor. Tactics applied: 74 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: 73 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: 73 Original Proof: [exact: val_inj.] 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: 72 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, 23 sec Number of successful tactic applications: 290 Number of failed tactic applications: 9711 Results for lemma tag_enumP: : Finite.axiom tag_enum FAILURE! Tactics applied: 7999 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, 16 sec Number of successful tactic applications: 169 Number of failed tactic applications: 7830 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, 24 sec Number of successful tactic applications: 284 Number of failed tactic applications: 9717 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, 32 sec Number of successful tactic applications: 303 Number of failed tactic applications: 9698 Results for lemma bumpK: h : cancel (bump h) (unbump h) FAILURE! Tactics applied: 5925 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, 12 sec Number of successful tactic applications: 114 Number of failed tactic applications: 5811 Results for lemma rev_ord_inj: {n} : injective (@rev_ord n) FAILURE! Tactics applied: 7150 Original Proof: [exact: inv_inj (@rev_ordK n).] Proof search time: 0 min, 14 sec Number of successful tactic applications: 156 Number of failed tactic applications: 6994 Results for lemma subset_eqP: A B : reflect (A =i B) ((A \subset B) && (B \subset A)) FAILURE! Tactics applied: 1266 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, 3 sec Number of successful tactic applications: 14 Number of failed tactic applications: 1252 Results for lemma image_codom: A : {subset image f A <= codom f} FAILURE! Tactics applied: 6688 Original Proof: [by move=> _ /imageP[x _ ->]; exact: codom_f.] Proof search time: 0 min, 14 sec Number of successful tactic applications: 140 Number of failed tactic applications: 6548 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: 173 Number of failed tactic applications: 9828 Results for lemma enum_valK_in: x0 A Ax0 : cancel enum_val (@enum_rank_in x0 A Ax0) FAILURE! Tactics applied: 7090 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, 16 sec Number of successful tactic applications: 144 Number of failed tactic applications: 6946 Results for lemma card_bool: : #|{: bool}| = 2 SUCCESS! Proof Found in EFSM: by rewrite cardT enumT unlock. Tactics applied: 232 Original Proof: [by rewrite cardT enumT unlock.] 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: 231 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, 17 sec Number of successful tactic applications: 156 Number of failed tactic applications: 9845 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: 176 Number of failed tactic applications: 9825 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: 3254 Original Proof: [by move=> eqP12; apply: eq_forallb => i; case Di: (D i); rewrite // eqP12.] Proof search time: 0 min, 7 sec Number of successful tactic applications: 60 Number of failed tactic applications: 3194 Results for lemma enum_ordS: : enum 'I_n = ord0 :: map (lift ord0) (enum 'I_n') FAILURE! Tactics applied: 6029 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, 13 sec Number of successful tactic applications: 103 Number of failed tactic applications: 5926 Results for lemma pred0Pn: P : reflect (exists x, P x) (~~ pred0b P) FAILURE! Tactics applied: 347 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: 0 Number of failed tactic applications: 347 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, 22 sec Number of successful tactic applications: 253 Number of failed tactic applications: 9748 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: 431 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, 2 sec Number of successful tactic applications: 1 Number of failed tactic applications: 430 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, 29 sec Number of successful tactic applications: 448 Number of failed tactic applications: 9553 Results for lemma splitP: m n (i : 'I_(m + n)) : split_spec i (split i) (i < m) FAILURE! Tactics applied: 348 Original Proof: [rewrite /split {-3}/leq. by case: (@ltnP i m) => cmp_i_m //=; constructor; rewrite ?subnKC.] Proof search time: 0 min, 2 sec Number of successful tactic applications: 0 Number of failed tactic applications: 348 Results for lemma subsetPn: A B : reflect (exists2 x, x \in A & x \notin B) (~~ (A \subset B)) FAILURE! Tactics applied: 1266 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, 4 sec Number of successful tactic applications: 14 Number of failed tactic applications: 1252 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, 22 sec Number of successful tactic applications: 273 Number of failed tactic applications: 9728 Results for lemma ord_inj: : injective nat_of_ord SUCCESS! Proof Found in EFSM: exact : val_inj. Tactics applied: 73 Original Proof: [exact: val_inj.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 25 Number of failed tactic applications: 48 Results for lemma lift_max: (i : 'I_n') : lift ord_max i = i :> nat FAILURE! Tactics applied: 6029 Original Proof: [by rewrite /= /bump leqNgt ltn_ord.] Proof search time: 0 min, 12 sec Number of successful tactic applications: 103 Number of failed tactic applications: 5926 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, 20 sec Number of successful tactic applications: 192 Number of failed tactic applications: 9809 Results for lemma invF_f: : cancel f invF FAILURE! Tactics applied: 5412 Original Proof: [by move=> x; exact: iinv_f.] Proof search time: 0 min, 11 sec Number of successful tactic applications: 154 Number of failed tactic applications: 5258 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: 235 Original Proof: [exact: disjointU1.] 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: 234 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, 21 sec Number of successful tactic applications: 216 Number of failed tactic applications: 9785 Results for lemma cast_ord_proof: n m (i : 'I_n) : n = m -> i < m FAILURE! Tactics applied: 6599 Original Proof: [by move <-.] Proof search time: 0 min, 13 sec Number of successful tactic applications: 137 Number of failed tactic applications: 6462 Results for lemma enum_rank_inj: : injective enum_rank FAILURE! Tactics applied: 6251 Original Proof: [exact: can_inj enum_rankK.] Proof search time: 0 min, 13 sec Number of successful tactic applications: 125 Number of failed tactic applications: 6126 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, 21 sec Number of successful tactic applications: 431 Number of failed tactic applications: 9570 Results for lemma card_ord: : #|'I_n| = n SUCCESS! Proof Found in EFSM: rewrite unlock; rewrite ?count_pred0. by rewrite -(size_map val) val_enum_ord size_iota. Tactics applied: 2798 Original Proof: [by rewrite cardE size_enum_ord.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 7 sec Number of successful tactic applications: 71 Number of failed tactic applications: 2727 Results for lemma bumpS: h i : bump h.+1 i.+1 = (bump h i).+1 FAILURE! Tactics applied: 5968 Original Proof: [exact: addnS.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 94 Number of failed tactic applications: 5874 Results for lemma cardT: : #|T| = size (enum T) SUCCESS! Proof Found in EFSM: by rewrite cardE; Tactics applied: 230 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: 1 Number of failed tactic applications: 229 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: 348 Original Proof: [by apply: (iffP (exists_inP _ _)) => [] [x Dx /eqP]; exists x.] Proof search time: 0 min, 2 sec Number of successful tactic applications: 0 Number of failed tactic applications: 348 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, 21 sec Number of successful tactic applications: 286 Number of failed tactic applications: 9715 Results for fold 2 Results for lemma injF_onto: y : y \in codom f FAILURE! Tactics applied: 282 Original Proof: [exact: inj_card_onto.] Proof search time: 0 min, 3 sec Number of successful tactic applications: 0 Number of failed tactic applications: 282 Results for lemma disjoint_cat: s1 s2 A : [disjoint s1 ++ s2 & A] = [disjoint s1 & A] && [disjoint s2 & A] FAILURE! Tactics applied: 282 Original Proof: [by rewrite !disjoint_has has_cat negb_or.] Proof search time: 0 min, 3 sec Number of successful tactic applications: 0 Number of failed tactic applications: 282 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: 902 Original Proof: [move=> injf x fAfx Ax; apply: injf => //; [exact: mem_iinv | exact: f_iinv].] Proof search time: 0 min, 4 sec Number of successful tactic applications: 20 Number of failed tactic applications: 882 Results for lemma index_enum_ord: (i : 'I_n) : index i (enum 'I_n) = i FAILURE! Tactics applied: 282 Original Proof: [by rewrite -{1}(nth_ord_enum i i) index_uniq ?(enum_uniq, size_enum_ord).] Proof search time: 0 min, 3 sec Number of successful tactic applications: 0 Number of failed tactic applications: 282 Results for lemma existsP: P : reflect (exists x, P x) [exists x, P x] FAILURE! Tactics applied: 460 Original Proof: [by apply: (iffP pred0Pn) => [] [x]; exists x.] Proof search time: 0 min, 3 sec Number of successful tactic applications: 10 Number of failed tactic applications: 450 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, 30 sec Number of successful tactic applications: 1115 Number of failed tactic applications: 8886 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, 32 sec Number of successful tactic applications: 963 Number of failed tactic applications: 9038 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: 2666 Number of failed tactic applications: 7335 Results for lemma neq_lift: n (h : 'I_n) i : h != lift h i FAILURE! Tactics applied: 282 Original Proof: [exact: neq_bump.] Proof search time: 0 min, 3 sec Number of successful tactic applications: 0 Number of failed tactic applications: 282 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, 22 sec Number of successful tactic applications: 1404 Number of failed tactic applications: 8597 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, 30 sec Number of successful tactic applications: 457 Number of failed tactic applications: 9544 Results for lemma eq_proper: A B : A =i B -> proper (mem A) =1 proper (mem B) FAILURE! Tactics applied: 1648 Original Proof: [move=> eAB [C]; congr (_ && _); first exact: (eq_subset eAB). by rewrite (eq_subset_r eAB).] Proof search time: 0 min, 7 sec Number of successful tactic applications: 86 Number of failed tactic applications: 1562 Results for lemma eq_codom: (f g : T -> T') : f =1 g -> codom f = codom g FAILURE! Tactics applied: 778 Original Proof: [exact: eq_image.] Proof search time: 0 min, 4 sec Number of successful tactic applications: 16 Number of failed tactic applications: 762 Results for lemma bool_enumP: : Finite.axiom [:: true; false] FAILURE! Tactics applied: 1174 Original Proof: [by case.] Proof search time: 0 min, 5 sec Number of successful tactic applications: 31 Number of failed tactic applications: 1143 Results for lemma size_codom: : size (codom f) = #|T| FAILURE! Tactics applied: 10000 Original Proof: [exact: size_image.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 2526 Number of failed tactic applications: 7475 Results for lemma bij_on_codom: (x0 : T) : {on [pred y in codom f], bijective f} FAILURE! Tactics applied: 281 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, 3 sec Number of successful tactic applications: 0 Number of failed tactic applications: 281 Results for lemma mem_seq_sub_enum: x : x \in seq_sub_enum FAILURE! Tactics applied: 282 Original Proof: [by rewrite mem_undup mem_pmap -valK map_f ?ssvalP.] Proof search time: 0 min, 3 sec Number of successful tactic applications: 0 Number of failed tactic applications: 282 Results for lemma val_enum_ord: : map val (enum 'I_n) = iota 0 n FAILURE! Tactics applied: 281 Original Proof: [by rewrite enumT unlock val_ord_enum.] Proof search time: 0 min, 3 sec Number of successful tactic applications: 0 Number of failed tactic applications: 281 Results for lemma sub_ordK: (i : 'I_n) : n' - (n' - i) = i FAILURE! Tactics applied: 282 Original Proof: [by rewrite subKn ?leq_ord.] Proof search time: 0 min, 3 sec Number of successful tactic applications: 0 Number of failed tactic applications: 282 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, 29 sec Number of successful tactic applications: 768 Number of failed tactic applications: 9233 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, 27 sec Number of successful tactic applications: 2492 Number of failed tactic applications: 7509 Results for lemma injF_bij: : bijective f FAILURE! Tactics applied: 281 Original Proof: [exact: inj_card_bij.] Proof search time: 0 min, 3 sec Number of successful tactic applications: 0 Number of failed tactic applications: 281 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: 1318 Number of failed tactic applications: 8683 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, 21 sec Number of successful tactic applications: 1376 Number of failed tactic applications: 8625 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, 23 sec Number of successful tactic applications: 2225 Number of failed tactic applications: 7776 Results for lemma disjoint_sym: A B : [disjoint A & B] = [disjoint B & A] FAILURE! Tactics applied: 281 Original Proof: [by congr (_ == 0); apply: eq_card => x; exact: andbC.] Proof search time: 0 min, 3 sec Number of successful tactic applications: 0 Number of failed tactic applications: 281 Results for lemma iinv_f: x fTfx : @iinv T (f x) fTfx = x FAILURE! Tactics applied: 282 Original Proof: [by apply: in_iinv_f; first exact: in2W.] Proof search time: 0 min, 3 sec Number of successful tactic applications: 0 Number of failed tactic applications: 282 Results for lemma unit_enumP: : Finite.axiom [::tt] SUCCESS! Proof Found in EFSM: by []. Tactics applied: 79 Original Proof: [by case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Number of successful tactic applications: 17 Number of failed tactic applications: 62 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, 28 sec Number of successful tactic applications: 2936 Number of failed tactic applications: 7065 Results for lemma unbumpS: h i : unbump h.+1 i.+1 = (unbump h i).+1 FAILURE! Tactics applied: 1388 Original Proof: [exact: unbump_addl 1.] Proof search time: 0 min, 5 sec Number of successful tactic applications: 33 Number of failed tactic applications: 1355 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, 29 sec Number of successful tactic applications: 1448 Number of failed tactic applications: 8553 Results for lemma eq_existsb: P1 P2 : P1 =1 P2 -> [exists x, P1 x] = [exists x, P2 x] FAILURE! Tactics applied: 776 Original Proof: [by move=> eqP12; congr (_ != 0); apply: eq_card.] Proof search time: 0 min, 4 sec Number of successful tactic applications: 16 Number of failed tactic applications: 760 Results for lemma enum0: : enum pred0 = Nil T FAILURE! Tactics applied: 282 Original Proof: [exact: filter_pred0.] Proof search time: 0 min, 3 sec Number of successful tactic applications: 0 Number of failed tactic applications: 282 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: 1264 Number of failed tactic applications: 8737 Results for lemma unliftP: n (h i : 'I_n) : unlift_spec h i (unlift h i) FAILURE! Tactics applied: 280 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, 3 sec Number of successful tactic applications: 0 Number of failed tactic applications: 280 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; last first. exact : val_inj. Tactics applied: 2366 Original Proof: [by move=> i; exact: val_inj.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 7 sec Number of successful tactic applications: 84 Number of failed tactic applications: 2282 Results for lemma enum_rankK: : cancel enum_rank enum_val FAILURE! Tactics applied: 10000 Original Proof: [by move=> x; exact: enum_rankK_in.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 2875 Number of failed tactic applications: 7126 Results for lemma exists_eqP: f1 f2 : reflect (exists x, f1 x = f2 x) [exists x, f1 x == f2 x] FAILURE! Tactics applied: 282 Original Proof: [by apply: (iffP (existsP _)) => [] [x /eqP]; exists x.] Proof search time: 0 min, 3 sec Number of successful tactic applications: 0 Number of failed tactic applications: 282 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, 30 sec Number of successful tactic applications: 1957 Number of failed tactic applications: 8044 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, 25 sec Number of successful tactic applications: 2496 Number of failed tactic applications: 7505 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, 30 sec Number of successful tactic applications: 2693 Number of failed tactic applications: 7308 Results for lemma subsetE: A B : (A \subset B) = pred0b [predD A & B] SUCCESS! Proof Found in EFSM: by rewrite unlock. Tactics applied: 226 Original Proof: [by rewrite unlock.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Number of successful tactic applications: 1 Number of failed tactic applications: 225 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, 27 sec Number of successful tactic applications: 2492 Number of failed tactic applications: 7509 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, 25 sec Number of successful tactic applications: 2895 Number of failed tactic applications: 7106 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, 28 sec Number of successful tactic applications: 2929 Number of failed tactic applications: 7072 Results for lemma f_invF: : cancel invF f FAILURE! Tactics applied: 716 Original Proof: [by move=> y; exact: f_iinv.] Proof search time: 0 min, 4 sec Number of successful tactic applications: 14 Number of failed tactic applications: 702 Results for lemma disjointU: A B C : [disjoint predU A B & C] = [disjoint A & C] && [disjoint B & C] FAILURE! Tactics applied: 281 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, 3 sec Number of successful tactic applications: 0 Number of failed tactic applications: 281 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, 22 sec Number of successful tactic applications: 2913 Number of failed tactic applications: 7088 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, 29 sec Number of successful tactic applications: 786 Number of failed tactic applications: 9215 Results for fold 3 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, 24 sec Number of successful tactic applications: 1087 Number of failed tactic applications: 8914 Results for lemma properE: A B : A \proper B = (A \subset B) && ~~(B \subset A) SUCCESS! Proof Found in EFSM: constructor ; Tactics applied: 8 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: 7 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, 29 sec Number of successful tactic applications: 2471 Number of failed tactic applications: 7530 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, 25 sec Number of successful tactic applications: 1967 Number of failed tactic applications: 8034 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, 20 sec Number of successful tactic applications: 392 Number of failed tactic applications: 9609 Results for lemma codomE: : codom f = map f (enum T) SUCCESS! Proof Found in EFSM: constructor ; Tactics applied: 8 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: 7 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, 23 sec Number of successful tactic applications: 1258 Number of failed tactic applications: 8743 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, 28 sec Number of successful tactic applications: 2557 Number of failed tactic applications: 7444 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, 25 sec Number of successful tactic applications: 803 Number of failed tactic applications: 9198 Results for lemma subset_predT: A : A \subset T SUCCESS! Proof Found in EFSM: apply /subsetP=> y Ay; constructor ; Tactics applied: 894 Original Proof: [by apply/subsetP.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 3 sec Number of successful tactic applications: 42 Number of failed tactic applications: 852 Results for lemma card_unit: : #|{: unit}| = 1 SUCCESS! Proof Found in EFSM: by rewrite cardT enumT unlock. Tactics applied: 318 Original Proof: [by rewrite cardT enumT unlock.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 5 Number of failed tactic applications: 313 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, 25 sec Number of successful tactic applications: 1232 Number of failed tactic applications: 8769 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, 24 sec Number of successful tactic applications: 547 Number of failed tactic applications: 9454 Results for lemma ltn_ord: (i : ordinal) : i < n SUCCESS! Proof Found in EFSM: exact : valP i. Tactics applied: 74 Original Proof: [exact: valP i.] 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: 73 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, 21 sec Number of successful tactic applications: 341 Number of failed tactic applications: 9660 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, 19 sec Number of successful tactic applications: 274 Number of failed tactic applications: 9727 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, 24 sec Number of successful tactic applications: 955 Number of failed tactic applications: 9046 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, 28 sec Number of successful tactic applications: 1522 Number of failed tactic applications: 8479 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, 22 sec Number of successful tactic applications: 1049 Number of failed tactic applications: 8952 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, 21 sec Number of successful tactic applications: 341 Number of failed tactic applications: 9660 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, 23 sec Number of successful tactic applications: 486 Number of failed tactic applications: 9515 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, 28 sec Number of successful tactic applications: 484 Number of failed tactic applications: 9517 Results for lemma dinjectiveP: D : reflect {in D &, injective f} (dinjectiveb D) FAILURE! Tactics applied: 336 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, 2 sec Number of successful tactic applications: 0 Number of failed tactic applications: 336 Results for lemma subxx: (pT : predType T) (pA : pT) : pA \subset pA SUCCESS! Proof Found in EFSM: rewrite // eqP12. Tactics applied: 101 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: 100 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, 20 sec Number of successful tactic applications: 340 Number of failed tactic applications: 9661 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, 29 sec Number of successful tactic applications: 1898 Number of failed tactic applications: 8103 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, 25 sec Number of successful tactic applications: 1322 Number of failed tactic applications: 8679 Results for lemma leq_bump2: h i j : (bump h i <= bump h j) = (i <= j) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite leq_bump bumpK.] Proof search time: 0 min, 28 sec Number of successful tactic applications: 1244 Number of failed tactic applications: 8757 Results for lemma arg_maxP: : extremum_spec geq arg_max FAILURE! Tactics applied: 10000 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, 30 sec Number of successful tactic applications: 1926 Number of failed tactic applications: 8075 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, 21 sec Number of successful tactic applications: 580 Number of failed tactic applications: 9421 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, 27 sec Number of successful tactic applications: 628 Number of failed tactic applications: 9373 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, 20 sec Number of successful tactic applications: 649 Number of failed tactic applications: 9352 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, 23 sec Number of successful tactic applications: 405 Number of failed tactic applications: 9596 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: 1355 Number of failed tactic applications: 8646 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: 1035 Number of failed tactic applications: 8966 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, 26 sec Number of successful tactic applications: 1880 Number of failed tactic applications: 8121 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: 75 Original Proof: [exact: val_inj.] 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: 74 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, 26 sec Number of successful tactic applications: 2518 Number of failed tactic applications: 7483 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: 353 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, 2 sec Number of successful tactic applications: 22 Number of failed tactic applications: 331 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, 23 sec Number of successful tactic applications: 1886 Number of failed tactic applications: 8115 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: 469 Number of failed tactic applications: 9532 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, 29 sec Number of successful tactic applications: 2023 Number of failed tactic applications: 7978 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, 27 sec Number of successful tactic applications: 2491 Number of failed tactic applications: 7510 Results for lemma card1: x : #|pred1 x| = 1 SUCCESS! Proof Found in EFSM: rewrite unlock; first by rewrite -count_filter enumP. Tactics applied: 367 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, 2 sec Number of successful tactic applications: 7 Number of failed tactic applications: 360 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, 22 sec Number of successful tactic applications: 995 Number of failed tactic applications: 9006 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, 22 sec Number of successful tactic applications: 797 Number of failed tactic applications: 9204 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: 746 Number of failed tactic applications: 9255 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, 21 sec Number of successful tactic applications: 995 Number of failed tactic applications: 9006 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, 28 sec Number of successful tactic applications: 1337 Number of failed tactic applications: 8664 Results for fold 4 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, 17 sec Number of successful tactic applications: 726 Number of failed tactic applications: 9275 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, 19 sec Number of successful tactic applications: 229 Number of failed tactic applications: 9772 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, 23 sec Number of successful tactic applications: 367 Number of failed tactic applications: 9634 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, 19 sec Number of successful tactic applications: 247 Number of failed tactic applications: 9754 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: 316 Number of failed tactic applications: 9685 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, 20 sec Number of successful tactic applications: 453 Number of failed tactic applications: 9548 Results for lemma arg_minP: : extremum_spec leq arg_min FAILURE! Tactics applied: 443 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, 1 sec Number of successful tactic applications: 2 Number of failed tactic applications: 441 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, 17 sec Number of successful tactic applications: 225 Number of failed tactic applications: 9776 Results for lemma cardE: A : #|A| = size (enum A) SUCCESS! Proof Found in EFSM: by rewrite unlock. Tactics applied: 379 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: 5 Number of failed tactic applications: 374 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, 21 sec Number of successful tactic applications: 254 Number of failed tactic applications: 9747 Results for lemma pickP: : pick_spec (pick P) FAILURE! Tactics applied: 386 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, 1 sec Number of successful tactic applications: 0 Number of failed tactic applications: 386 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, 19 sec Number of successful tactic applications: 672 Number of failed tactic applications: 9329 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, 19 sec Number of successful tactic applications: 434 Number of failed tactic applications: 9567 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, 23 sec Number of successful tactic applications: 728 Number of failed tactic applications: 9273 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, 18 sec Number of successful tactic applications: 243 Number of failed tactic applications: 9758 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, 26 sec Number of successful tactic applications: 372 Number of failed tactic applications: 9629 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, 18 sec Number of successful tactic applications: 709 Number of failed tactic applications: 9292 Results for lemma proper_sub: A B : A \proper B -> A \subset B SUCCESS! Proof Found in EFSM: by case/andP. Tactics applied: 263 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: 15 Number of failed tactic applications: 248 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, 18 sec Number of successful tactic applications: 294 Number of failed tactic applications: 9707 Results for lemma card0: : #|@pred0 T| = 0 FAILURE! Tactics applied: 10000 Original Proof: [by rewrite cardE enum0.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 300 Number of failed tactic applications: 9701 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, 20 sec Number of successful tactic applications: 250 Number of failed tactic applications: 9751 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: 350 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: 6 Number of failed tactic applications: 344 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, 20 sec Number of successful tactic applications: 352 Number of failed tactic applications: 9649 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, 24 sec Number of successful tactic applications: 397 Number of failed tactic applications: 9604 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, 17 sec Number of successful tactic applications: 222 Number of failed tactic applications: 9779 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, 17 sec Number of successful tactic applications: 744 Number of failed tactic applications: 9257 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, 19 sec Number of successful tactic applications: 237 Number of failed tactic applications: 9764 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, 17 sec Number of successful tactic applications: 265 Number of failed tactic applications: 9736 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, 23 sec Number of successful tactic applications: 870 Number of failed tactic applications: 9131 Results for lemma lift0: (i : 'I_n') : lift ord0 i = i.+1 :> nat SUCCESS! Proof Found in EFSM: congr (_ + _). Tactics applied: 44 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: 43 Results for lemma leq_ord: (i : 'I_n) : i <= n' SUCCESS! Proof Found in EFSM: exact : valP i. Tactics applied: 128 Original Proof: [exact: valP i.] 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: 127 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, 21 sec Number of successful tactic applications: 395 Number of failed tactic applications: 9606 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, 21 sec Number of successful tactic applications: 225 Number of failed tactic applications: 9776 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: 1572 Original Proof: [by move=> i; exact: val_inj.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 3 sec Number of successful tactic applications: 69 Number of failed tactic applications: 1503 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, 20 sec Number of successful tactic applications: 193 Number of failed tactic applications: 9808 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, 21 sec Number of successful tactic applications: 296 Number of failed tactic applications: 9705 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, 23 sec Number of successful tactic applications: 487 Number of failed tactic applications: 9514 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, 20 sec Number of successful tactic applications: 217 Number of failed tactic applications: 9784 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, 18 sec Number of successful tactic applications: 295 Number of failed tactic applications: 9706 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, 19 sec Number of successful tactic applications: 761 Number of failed tactic applications: 9240 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, 25 sec Number of successful tactic applications: 263 Number of failed tactic applications: 9738 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, 21 sec Number of successful tactic applications: 754 Number of failed tactic applications: 9247 Results for lemma injectiveP: : reflect (injective f) injectiveb FAILURE! Tactics applied: 389 Original Proof: [apply: (iffP (dinjectiveP _)) => injf x y => [|_ _]; exact: injf.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 0 Number of failed tactic applications: 389 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, 21 sec Number of successful tactic applications: 256 Number of failed tactic applications: 9745 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, 25 sec Number of successful tactic applications: 486 Number of failed tactic applications: 9515 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, 21 sec Number of successful tactic applications: 253 Number of failed tactic applications: 9748 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, 21 sec Number of successful tactic applications: 293 Number of failed tactic applications: 9708 Results for lemma imageP: A y : reflect (exists2 x, x \in A & y = f x) (y \in image f A) FAILURE! Tactics applied: 387 Original Proof: [by apply: (iffP mapP) => [] [x Ax y_fx]; exists x; rewrite // mem_enum in Ax *.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 0 Number of failed tactic applications: 387 Results for lemma card_codom: : #|codom f| = #|T| SUCCESS! Proof Found in EFSM: apply : card_in_image; exact : in2W. Tactics applied: 1278 Original Proof: [exact: card_image.] Shorter Proof Found? no Proof reused from card_image proof search time: 0 min, 3 sec Number of successful tactic applications: 47 Number of failed tactic applications: 1231 Results for fold 5 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, 28 sec Number of successful tactic applications: 389 Number of failed tactic applications: 9612 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, 25 sec Number of successful tactic applications: 531 Number of failed tactic applications: 9470 Results for lemma enumT: : enum T = Finite.enum T SUCCESS! Proof Found in EFSM: apply /all_filterP. by apply/allP => x; Tactics applied: 672 Original Proof: [exact: filter_predT.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 1 sec Number of successful tactic applications: 21 Number of failed tactic applications: 651 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, 32 sec Number of successful tactic applications: 251 Number of failed tactic applications: 9750 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: 1712 Number of failed tactic applications: 8289 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, 20 sec Number of successful tactic applications: 438 Number of failed tactic applications: 9563 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, 22 sec Number of successful tactic applications: 376 Number of failed tactic applications: 9625 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, 22 sec Number of successful tactic applications: 820 Number of failed tactic applications: 9181 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, 21 sec Number of successful tactic applications: 280 Number of failed tactic applications: 9721 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, 25 sec Number of successful tactic applications: 375 Number of failed tactic applications: 9626 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, 21 sec Number of successful tactic applications: 380 Number of failed tactic applications: 9621 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, 27 sec Number of successful tactic applications: 391 Number of failed tactic applications: 9610 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: 513 Number of failed tactic applications: 9488 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, 22 sec Number of successful tactic applications: 341 Number of failed tactic applications: 9660 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, 27 sec Number of successful tactic applications: 251 Number of failed tactic applications: 9750 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, 25 sec Number of successful tactic applications: 401 Number of failed tactic applications: 9600 Results for lemma injectivePn: : reflect (exists x, exists2 y, x != y & f x = f y) (~~ injectiveb) FAILURE! Tactics applied: 548 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, 1 sec Number of successful tactic applications: 2 Number of failed tactic applications: 546 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, 26 sec Number of successful tactic applications: 277 Number of failed tactic applications: 9724 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, 22 sec Number of successful tactic applications: 348 Number of failed tactic applications: 9653 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, 22 sec Number of successful tactic applications: 448 Number of failed tactic applications: 9553 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: 228 Number of failed tactic applications: 9773 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, 20 sec Number of successful tactic applications: 881 Number of failed tactic applications: 9120 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, 24 sec Number of successful tactic applications: 437 Number of failed tactic applications: 9564 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: 361 Number of failed tactic applications: 9640 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, 24 sec Number of successful tactic applications: 374 Number of failed tactic applications: 9627 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, 22 sec Number of successful tactic applications: 514 Number of failed tactic applications: 9487 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, 27 sec Number of successful tactic applications: 3817 Number of failed tactic applications: 6184 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, 23 sec Number of successful tactic applications: 533 Number of failed tactic applications: 9468 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, 25 sec Number of successful tactic applications: 309 Number of failed tactic applications: 9692 Results for lemma nth_codom: T' y0 (f : T -> T') (i : 'I_#|T|) : nth y0 (codom f) i = f (enum_val i) FAILURE! Tactics applied: 10000 Original Proof: [exact: nth_image.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 1718 Number of failed tactic applications: 8283 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: 2172 Original Proof: [by move=> x; exact: nth_enum_rank_in.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 6 sec Number of successful tactic applications: 81 Number of failed tactic applications: 2091 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: 386 Number of failed tactic applications: 9615 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: 395 Number of failed tactic applications: 9606 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, 18 sec Number of successful tactic applications: 358 Number of failed tactic applications: 9643 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, 23 sec Number of successful tactic applications: 874 Number of failed tactic applications: 9127 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, 20 sec Number of successful tactic applications: 279 Number of failed tactic applications: 9722 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, 19 sec Number of successful tactic applications: 688 Number of failed tactic applications: 9313 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, 33 sec Number of successful tactic applications: 260 Number of failed tactic applications: 9741 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, 22 sec Number of successful tactic applications: 380 Number of failed tactic applications: 9621 Results for lemma canF_sym: : cancel g f FAILURE! Tactics applied: 10000 Original Proof: [exact/(bij_can_sym (injF_bij (can_inj fK))).] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1304 Number of failed tactic applications: 8697 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, 21 sec Number of successful tactic applications: 525 Number of failed tactic applications: 9476 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, 36 sec Number of successful tactic applications: 465 Number of failed tactic applications: 9536 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, 28 sec Number of successful tactic applications: 419 Number of failed tactic applications: 9582 Results for lemma disjoint0: A : [disjoint pred0 & A] SUCCESS! Proof Found in EFSM: apply /idPn; by rewrite -lt0n eq_card0 //; Tactics applied: 807 Original Proof: [exact/pred0P.] 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: 39 Number of failed tactic applications: 768 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: 456 Number of failed tactic applications: 9545 Results for lemma proper_subn: A B : A \proper B -> ~~ (B \subset A) SUCCESS! Proof Found in EFSM: by case/andP. Tactics applied: 245 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: 23 Number of failed tactic applications: 222 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, 24 sec Number of successful tactic applications: 2362 Number of failed tactic applications: 7639 OVERALL RESULTS SUMMARY EFSMProver proved 31 out of 243 lemmas. Success rate of 12.757201646090536% There were 0 errors. 212 proof attempts exhausted the automaton On average, a proof was found after applying 538 tactics The longest proof consisted of 3 tactics There were 1 shorter proofs found Of the 212 failures, 157 of them used all 10000 tactics There were 22 reused proofs found There were 9 novel proofs found Of the 212 failures, the average number of tactics used was 7995 On average, a proof was found after 0 min, 2 sec On average, a failed proof attempt took 0 min, 19 sec On average, any (success or failure) proof attempt took 0 min, 17 sec The longest time to find a proof was 0 min, 7 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