Results for fold 1 Results for lemma codomP: y : reflect (exists x, y = f x) (y \in codom f) FAILURE! Tactics applied: 100000 Original Proof: [by apply: (iffP (imageP _ y)) => [][x]; exists x.] Proof search time: 1 min, 46 sec Results for lemma card_uniqP: s : reflect (#|s| = size s) (uniq s) FAILURE! Tactics applied: 100000 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: 1 min, 55 sec Results for lemma eq_card_prod: (A : pred (T1 * T2)) : A =i predT -> #|A| = #|T1| * #|T2| FAILURE! Tactics applied: 100000 Original Proof: [exact: eq_card_trans card_prod.] Proof search time: 2 min, 8 sec Results for lemma rev_ord_proof: n (i : 'I_n) : n - i.+1 < n FAILURE! Tactics applied: 100000 Original Proof: [by case: n i => [|n] [i lt_i_n] //; rewrite ltnS subSS leq_subr.] Proof search time: 2 min, 5 sec Results for lemma injF_onto: y : y \in codom f FAILURE! Tactics applied: 100000 Original Proof: [exact: inj_card_onto.] Proof search time: 2 min, 4 sec Results for lemma subset_leqif_card: A B : A \subset B -> #|A| <= #|B| ?= iff (B \subset A) FAILURE! Tactics applied: 100000 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: 2 min, 5 sec Results for lemma map_preim: (s : seq T') : {subset s <= codom f} -> map f (preim_seq s) = s FAILURE! Tactics applied: 100000 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: 2 min, 6 sec Results for lemma bumpS: h i : bump h.+1 i.+1 = (bump h i).+1 FAILURE! Tactics applied: 100000 Original Proof: [exact: addnS.] Proof search time: 2 min, 5 sec 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: 100000 Original Proof: [rewrite eq_sym => /eqP neq_ih. by case Dui: (unlift h i) / (unliftP h i) => [j Dh|//]; exists j.] Proof search time: 2 min, 10 sec Results for lemma enum0: : enum pred0 = Nil T FAILURE! Tactics applied: 100000 Original Proof: [exact: filter_pred0.] Proof search time: 1 min, 57 sec Results for lemma enum_rankK: : cancel enum_rank enum_val FAILURE! Tactics applied: 100000 Original Proof: [by move=> x; exact: enum_rankK_in.] Proof search time: 2 min, 9 sec Results for lemma bool_enumP: : Finite.axiom [:: true; false] FAILURE! Tactics applied: 100000 Original Proof: [by case.] Proof search time: 2 min, 4 sec Results for lemma pred0P: P : reflect (P =1 pred0) (pred0b P) FAILURE! Tactics applied: 100000 Original Proof: [apply: (iffP eqP); [exact: card0_eq | exact: eq_card0].] Proof search time: 1 min, 56 sec Results for lemma inordK: m : m < n -> inord m = m :> nat FAILURE! Tactics applied: 100000 Original Proof: [by move=> lt_m; rewrite val_insubd lt_m.] Proof search time: 2 min, 6 sec Results for lemma subsetPn: A B : reflect (exists2 x, x \in A & x \notin B) (~~ (A \subset B)) FAILURE! Tactics applied: 100000 Original Proof: [rewrite unlock; apply: (iffP (pred0Pn _)) => [[x] | [x Ax nBx]]. by case/andP; exists x. by exists x; rewrite /= nBx.] Proof search time: 2 min, 4 sec Results for lemma eq_disjoint: A1 A2 : A1 =i A2 -> disjoint (mem A1) =1 disjoint (mem A2) FAILURE! Tactics applied: 100000 Original Proof: [by move=> eqA12 [B]; congr (_ == 0); apply: eq_card => x; rewrite !inE eqA12.] Proof search time: 2 min, 4 sec Results for lemma eq_codom: (f g : T -> T') : f =1 g -> codom f = codom g FAILURE! Tactics applied: 100000 Original Proof: [exact: eq_image.] Proof search time: 2 min, 3 sec Results for lemma neq_lift: n (h : 'I_n) i : h != lift h i FAILURE! Tactics applied: 100000 Original Proof: [exact: neq_bump.] Proof search time: 2 min, 8 sec 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: 100000 Original Proof: [move=> injf x fAfx Ax; apply: injf => //; [exact: mem_iinv | exact: f_iinv].] Proof search time: 2 min, 6 sec Results for lemma card_ord: : #|'I_n| = n FAILURE! Tactics applied: 100000 Original Proof: [by rewrite cardE size_enum_ord.] Proof search time: 1 min, 58 sec Results for lemma card_sub: : #|sfT| = #|[pred x | P x]| FAILURE! Tactics applied: 100000 Original Proof: [by rewrite !cardE enumT unlock -(size_map val) val_sub_enum.] Proof search time: 2 min, 5 sec Results for lemma mem_iinv: A y fAy : @iinv A y fAy \in A FAILURE! Tactics applied: 100000 Original Proof: [exact: s2valP (iinv_proof fAy).] Proof search time: 2 min, 8 sec Results for lemma enumT: : enum T = Finite.enum T FAILURE! Tactics applied: 100000 Original Proof: [exact: filter_predT.] Proof search time: 2 min, 1 sec Results for lemma card_size: s : #|s| <= size s FAILURE! Tactics applied: 100000 Original Proof: [elim: s => [|x s IHs] /=; first by rewrite card0. rewrite cardU1 /=; case: (~~ _) => //; exact: leqW.] Proof search time: 2 min, 1 sec Results for lemma eq_existsb: P1 P2 : P1 =1 P2 -> [exists x, P1 x] = [exists x, P2 x] FAILURE! Tactics applied: 100000 Original Proof: [by move=> eqP12; congr (_ != 0); apply: eq_card.] Proof search time: 2 min, 10 sec Results for fold 2 Results for lemma unlift_subproof: n (h : 'I_n) (u : {j | j != h}) : unbump h (val u) < n.-1 FAILURE! Tactics applied: 100000 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: 1 min, 41 sec Results for lemma proper_subn: A B : A \proper B -> ~~ (B \subset A) SUCCESS! Proof Found in EFSM: [by case/andP ] Tactics applied: 131 Original Proof: [by case/andP.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Results for lemma cast_ord_proof: n m (i : 'I_n) : n = m -> i < m SUCCESS! Proof Found in EFSM: [by case n i => [n] [i lt_i_n] //;, move <-] Tactics applied: 10542 Original Proof: [by move <-.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 20 sec Results for lemma rev_ord_inj: {n} : injective (@rev_ord n) FAILURE! Tactics applied: 100000 Original Proof: [exact: inv_inj (@rev_ordK n).] Proof search time: 1 min, 37 sec Results for lemma inj_card_bij: : bijective f FAILURE! Tactics applied: 100000 Original Proof: [by exists (fun y => iinv (inj_card_onto y)) => y; rewrite ?iinv_f ?f_iinv.] Proof search time: 1 min, 24 sec 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: 100000 Original Proof: [by apply: (iffP (exists_inP _ _)) => [] [x Dx /eqP]; exists x.] Proof search time: 1 min, 31 sec Results for lemma disjoint1: x A : [disjoint pred1 x & A] = (x \notin A) FAILURE! Tactics applied: 100000 Original Proof: [apply/negbRL/(sameP (pred0Pn _)). apply: introP => [Ax | notAx [_ /andP[/eqP->]]]; last exact: negP. by exists x; rewrite !inE eqxx.] Proof search time: 1 min, 26 sec Results for lemma injectivePn: : reflect (exists x, exists2 y, x != y & f x = f y) (~~ injectiveb) FAILURE! Tactics applied: 100000 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: 1 min, 27 sec Results for lemma properP: A B : reflect (A \subset B /\ (exists2 x, x \in B & x \notin A)) (A \proper B) FAILURE! Tactics applied: 100000 Original Proof: [by rewrite properE; apply: (iffP andP) => [] [-> /subsetPn].] Proof search time: 1 min, 22 sec Results for lemma subset_pred1: A x : (pred1 x \subset A) = (x \in A) FAILURE! Tactics applied: 100000 Original Proof: [by apply/subsetP/idP=> [-> // | Ax y /eqP-> //]; exact: eqxx.] Proof search time: 1 min, 21 sec Results for lemma card_unit: : #|{: unit}| = 1 SUCCESS! Proof Found in EFSM: [by rewrite cardT enumT unlock ] Tactics applied: 193 Original Proof: [by rewrite cardT enumT unlock.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 4 sec Results for lemma cardE: A : #|A| = size (enum A) SUCCESS! Proof Found in EFSM: [by rewrite unlock ] Tactics applied: 206 Original Proof: [by rewrite unlock.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Results for lemma subset_leq_card: A B : A \subset B -> #|A| <= #|B| FAILURE! Tactics applied: 100000 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: 1 min, 23 sec Results for lemma card_sum: : #|{: T1 + T2}| = #|T1| + #|T2| FAILURE! Tactics applied: 100000 Original Proof: [by rewrite !cardT !enumT {1}unlock size_cat !size_map.] Proof search time: 1 min, 34 sec Results for lemma sum_enum_uniq: : uniq sum_enum FAILURE! Tactics applied: 100000 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: 1 min, 34 sec Results for lemma card1: x : #|pred1 x| = 1 SUCCESS! Proof Found in EFSM: [rewrite unlock;, first by rewrite -count_filter enumP ] Tactics applied: 31016 Original Proof: [by rewrite cardE enum1.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 31 sec Results for lemma subset_predT: A : A \subset T SUCCESS! Proof Found in EFSM: [by apply/subsetPn;, case ] Tactics applied: 3387 Original Proof: [by apply/subsetP.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 6 sec Results for lemma split_subproof: m n (i : 'I_(m + n)) : i >= m -> i - m < n FAILURE! Tactics applied: 100000 Original Proof: [by move/subSn <-; rewrite leq_subLR.] Proof search time: 1 min, 45 sec Results for lemma injF_bij: : bijective f FAILURE! Tactics applied: 100000 Original Proof: [exact: inj_card_bij.] Proof search time: 1 min, 24 sec Results for lemma unliftP: n (h i : 'I_n) : unlift_spec h i (unlift h i) FAILURE! Tactics applied: 100000 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: 1 min, 37 sec Results for lemma eq_subxx: A B : A =i B -> A \subset B FAILURE! Tactics applied: 100000 Original Proof: [by move/eq_subset->.] Proof search time: 1 min, 26 sec Results for lemma properxx: A : (A \proper A) = false SUCCESS! Proof Found in EFSM: [by rewrite properE subxx ] Tactics applied: 208 Original Proof: [by rewrite properE subxx.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Results for lemma unit_enumP: : Finite.axiom [::tt] SUCCESS! Proof Found in EFSM: [constructor ] Tactics applied: 20 Original Proof: [by case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 4 sec Results for lemma neq_bump: h i : h != bump h i FAILURE! Tactics applied: 100000 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: 1 min, 39 sec Results for lemma image_pred0: : image f pred0 =i pred0 FAILURE! Tactics applied: 100000 Original Proof: [by move=> x; rewrite /image_mem /= enum0.] Proof search time: 1 min, 43 sec Results for fold 3 Results for lemma cardID: B A : #|[predI A & B]| + #|[predD A & B]| = #|A| FAILURE! Tactics applied: 0 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, 1 sec Results for lemma codom_f: x : f x \in codom f FAILURE! Tactics applied: 0 Original Proof: [by exact: image_f.] Proof search time: 0 min, 3 sec Results for lemma enum_val_ord: n i : enum_val i = cast_ord (card_ord n) i FAILURE! Tactics applied: 0 Original Proof: [by apply: canLR (@enum_rankK _) _; apply: val_inj; rewrite enum_rank_ord.] Proof search time: 0 min, 5 sec Results for lemma enum_uniq: : uniq (enum P) FAILURE! Tactics applied: 0 Original Proof: [by apply/filter_uniq/count_mem_uniq => x; rewrite enumP -enumT mem_enum.] Proof search time: 0 min, 1 sec Results for lemma size_codom: : size (codom f) = #|T| FAILURE! Tactics applied: 0 Original Proof: [exact: size_image.] Proof search time: 0 min, 3 sec Results for lemma subsetE: A B : (A \subset B) = pred0b [predD A & B] FAILURE! Tactics applied: 0 Original Proof: [by rewrite unlock.] Proof search time: 0 min, 1 sec Results for lemma cardD1: x A : #|A| = (x \in A) + #|[predD1 A & x]| FAILURE! Tactics applied: 0 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, 1 sec Results for lemma enum_val_nth: A x i : @enum_val A i = nth x (enum A) i FAILURE! Tactics applied: 0 Original Proof: [by apply: set_nth_default; rewrite cardE in i *; exact: ltn_ord.] Proof search time: 0 min, 4 sec Results for lemma ord_inj: : injective nat_of_ord FAILURE! Tactics applied: 0 Original Proof: [exact: val_inj.] Proof search time: 0 min, 4 sec Results for lemma max_card: A : #|A| <= #|T| FAILURE! Tactics applied: 0 Original Proof: [by rewrite -(cardC A) leq_addr.] Proof search time: 0 min, 1 sec Results for lemma subset_trans: A B C : A \subset B -> B \subset C -> A \subset C FAILURE! Tactics applied: 0 Original Proof: [by move/subsetP=> sAB /subsetP=> sBC; apply/subsetP=> x /sAB; exact: sBC.] Proof search time: 0 min, 2 sec Results for lemma count_enumP: : axiom count_enum FAILURE! Tactics applied: 0 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, 1 sec Results for lemma cast_ord_id: n eq_n i : cast_ord eq_n i = i :> 'I_n FAILURE! Tactics applied: 0 Original Proof: [exact: val_inj.] Proof search time: 0 min, 4 sec Results for lemma nth_enum_rank: x0 : cancel enum_rank (nth x0 (enum T)) FAILURE! Tactics applied: 0 Original Proof: [by move=> x; exact: nth_enum_rank_in.] Proof search time: 0 min, 4 sec Results for lemma canF_sym: : cancel g f FAILURE! Tactics applied: 0 Original Proof: [exact/(bij_can_sym (injF_bij (can_inj fK))).] Proof search time: 0 min, 3 sec Results for lemma cardT: : #|T| = size (enum T) FAILURE! Tactics applied: 0 Original Proof: [by rewrite cardE.] Proof search time: 0 min, 1 sec Results for lemma proper_irrefl: A : ~~ (A \proper A) FAILURE! Tactics applied: 0 Original Proof: [by rewrite properE subxx.] Proof search time: 0 min, 2 sec Results for lemma disjoint_sym: A B : [disjoint A & B] = [disjoint B & A] FAILURE! Tactics applied: 0 Original Proof: [by congr (_ == 0); apply: eq_card => x; exact: andbC.] Proof search time: 0 min, 2 sec Results for lemma subset_eqP: A B : reflect (A =i B) ((A \subset B) && (B \subset A)) FAILURE! Tactics applied: 0 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, 2 sec Results for lemma subsetP: A B : reflect {subset A <= B} (A \subset B) FAILURE! Tactics applied: 0 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, 1 sec 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: 0 Original Proof: [by rewrite -(nth_map _ y0) // -cardE.] Proof search time: 0 min, 4 sec Results for lemma val_seq_sub_enum: : uniq s -> map val seq_sub_enum = s FAILURE! Tactics applied: 0 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, 4 sec Results for lemma leq_bump2: h i j : (bump h i <= bump h j) = (i <= j) FAILURE! Tactics applied: 0 Original Proof: [by rewrite leq_bump bumpK.] Proof search time: 0 min, 5 sec Results for lemma card_option: : #|{: option T}| = #|T|.+1 FAILURE! Tactics applied: 0 Original Proof: [by rewrite !cardT !enumT {1}unlock /= !size_map.] Proof search time: 0 min, 4 sec Results for lemma sub_proper_trans: A B C : A \subset B -> B \proper C -> A \proper C FAILURE! Tactics applied: 0 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, 2 sec Results for fold 4 Results for lemma predT_subset: A : T \subset A -> forall x, x \in A FAILURE! Tactics applied: 0 Original Proof: [move/subsetP=> allA x; exact: allA.] Proof search time: 0 min, 2 sec Results for lemma val_ord_enum: : map val ord_enum = iota 0 n FAILURE! Tactics applied: 0 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, 4 sec Results for lemma sub_ordK: (i : 'I_n) : n' - (n' - i) = i FAILURE! Tactics applied: 0 Original Proof: [by rewrite subKn ?leq_ord.] Proof search time: 0 min, 5 sec Results for lemma cardX: (A1 : pred T1) (A2 : pred T2) : #|[predX A1 & A2]| = #|A1| * #|A2| FAILURE! Tactics applied: 0 Original Proof: [by rewrite -predX_prod_enum unlock -count_filter unlock.] Proof search time: 0 min, 5 sec Results for lemma image_f: A x : x \in A -> f x \in image f A FAILURE! Tactics applied: 0 Original Proof: [by move=> Ax; apply/imageP; exists x.] Proof search time: 0 min, 3 sec Results for lemma eq_subset: A1 A2 : A1 =i A2 -> subset (mem A1) =1 subset (mem A2) FAILURE! Tactics applied: 0 Original Proof: [move=> eqA12 [B]; rewrite !unlock; congr (_ == 0). by apply: eq_card => x; rewrite inE /= eqA12.] Proof search time: 0 min, 2 sec Results for lemma image_codom: A : {subset image f A <= codom f} FAILURE! Tactics applied: 0 Original Proof: [by move=> _ /imageP[x _ ->]; exact: codom_f.] Proof search time: 0 min, 3 sec 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: 0 Original Proof: [by apply: (iffP (forall_inP _ _)) => eq_f12 x Dx; apply/eqP/eq_f12.] Proof search time: 0 min, 2 sec Results for lemma inord_val: (i : 'I_n) : inord i = i FAILURE! Tactics applied: 0 Original Proof: [by rewrite /inord /insubd valK.] Proof search time: 0 min, 5 sec Results for lemma disjoint_has: s A : [disjoint s & A] = ~~ has (mem A) s FAILURE! Tactics applied: 0 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, 2 sec Results for lemma enum_rank_subproof: x0 A : x0 \in A -> 0 < #|A| FAILURE! Tactics applied: 0 Original Proof: [by move=> Ax0; rewrite (cardD1 x0) Ax0.] Proof search time: 0 min, 4 sec Results for lemma eq_subset_r: B1 B2 : B1 =i B2 -> (@subset T)^~ (mem B1) =1 (@subset T)^~ (mem B2) FAILURE! Tactics applied: 0 Original Proof: [move=> eqB12 [A]; rewrite !unlock; congr (_ == 0). by apply: eq_card => x; rewrite !inE /= eqB12.] Proof search time: 0 min, 2 sec Results for lemma enum1: x : enum (pred1 x) = [:: x] FAILURE! Tactics applied: 0 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, 1 sec Results for lemma negb_forall_in: D P : ~~ [forall (x | D x), P x] = [exists (x | D x), ~~ P x] FAILURE! Tactics applied: 0 Original Proof: [by apply: eq_existsb => x; rewrite negb_imply.] Proof search time: 0 min, 3 sec Results for lemma enum_rankK_in: x0 A Ax0 : {in A, cancel (@enum_rank_in x0 A Ax0) enum_val} FAILURE! Tactics applied: 0 Original Proof: [by move=> x; exact: nth_enum_rank_in.] Proof search time: 0 min, 4 sec Results for lemma properE: A B : A \proper B = (A \subset B) && ~~(B \subset A) FAILURE! Tactics applied: 0 Original Proof: [by [].] Proof search time: 0 min, 2 sec Results for lemma card_codom: : #|codom f| = #|T| FAILURE! Tactics applied: 0 Original Proof: [exact: card_image.] Proof search time: 0 min, 4 sec Results for lemma option_enumP: : Finite.axiom option_enum FAILURE! Tactics applied: 0 Original Proof: [by case=> [x|]; rewrite /= count_map (count_pred0, enumP).] Proof search time: 0 min, 4 sec Results for lemma negb_exists_in: D P : ~~ [exists (x | D x), P x] = [forall (x | D x), ~~ P x] FAILURE! Tactics applied: 0 Original Proof: [by rewrite negb_exists; apply/eq_forallb => x; rewrite [~~ _]fun_if.] Proof search time: 0 min, 3 sec Results for lemma iinv_f: x fTfx : @iinv T (f x) fTfx = x FAILURE! Tactics applied: 0 Original Proof: [by apply: in_iinv_f; first exact: in2W.] Proof search time: 0 min, 3 sec Results for lemma ord_enum_uniq: : uniq ord_enum FAILURE! Tactics applied: 0 Original Proof: [by rewrite pmap_sub_uniq ?iota_uniq.] Proof search time: 0 min, 4 sec Results for lemma lift_subproof: n h (i : 'I_n.-1) : bump h i < n FAILURE! Tactics applied: 0 Original Proof: [by case: n i => [[]|n] //= i; rewrite -addnS (leq_add (leq_b1 _)).] Proof search time: 0 min, 5 sec Results for lemma enum_rank_ord: n i : enum_rank i = cast_ord (esym (card_ord n)) i FAILURE! Tactics applied: 0 Original Proof: [by apply: val_inj; rewrite insubdK ?index_enum_ord // card_ord [_ \in _]ltn_ord.] Proof search time: 0 min, 5 sec Results for lemma card_preim: (B : pred T') : #|[preim f of B]| = #|[predI codom f & B]| FAILURE! Tactics applied: 0 Original Proof: [rewrite -card_image /=; apply: eq_card => y. by rewrite [y \in _]image_pre !inE andbC.] Proof search time: 0 min, 3 sec Results for lemma liftK: n (h : 'I_n) : pcancel (lift h) (unlift h) FAILURE! Tactics applied: 0 Original Proof: [by move=> i; case: (unlift_some (neq_lift h i)) => j; move/lift_inj->.] Proof search time: 0 min, 5 sec Results for fold 5 Results for lemma exists_inP: D P : reflect (exists2 x, D x & P x) [exists (x | D x), P x] FAILURE! Tactics applied: 0 Original Proof: [by apply: (iffP pred0Pn) => [[x /andP[]] | [x]]; exists x => //; apply/andP.] Proof search time: 0 min, 3 sec Results for lemma pickP: : pick_spec (pick P) FAILURE! Tactics applied: 0 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 Results for lemma mem_enum: A : enum A =i A FAILURE! Tactics applied: 0 Original Proof: [by move=> x; rewrite mem_filter andbC -has_pred1 has_count enumP.] Proof search time: 0 min, 1 sec Results for lemma cardC: A : #|A| + #|[predC A]| = #|T| FAILURE! Tactics applied: 0 Original Proof: [by rewrite !cardE -!count_filter count_predC.] Proof search time: 0 min, 1 sec Results for lemma eq_enum: P Q : P =i Q -> enum P = enum Q FAILURE! Tactics applied: 0 Original Proof: [move=> eqPQ; exact: eq_filter.] Proof search time: 0 min, 1 sec Results for lemma pcan_enumP: g : pcancel f g -> Finite.axiom (undup (pmap g (enumF fT))) FAILURE! Tactics applied: 0 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, 4 sec Results for lemma nth_ord_enum: (i0 i : 'I_n) : nth i0 (enum 'I_n) i = i FAILURE! Tactics applied: 0 Original Proof: [apply: val_inj; exact: nth_enum_ord.] Proof search time: 0 min, 4 sec Results for lemma bump_addl: h i k : bump (k + h) (k + i) = k + bump h i FAILURE! Tactics applied: 0 Original Proof: [by rewrite /bump leq_add2l addnCA.] Proof search time: 0 min, 5 sec Results for lemma disjoint0: A : [disjoint pred0 & A] FAILURE! Tactics applied: 0 Original Proof: [exact/pred0P.] Proof search time: 0 min, 2 sec Results for lemma f_iinv: A y fAy : f (@iinv A y fAy) = y FAILURE! Tactics applied: 0 Original Proof: [exact: s2valP' (iinv_proof fAy).] Proof search time: 0 min, 3 sec Results for lemma enumP: : Finite.axiom (Finite.enum T) FAILURE! Tactics applied: 0 Original Proof: [by rewrite unlock; case T => ? [? []].] Proof search time: 0 min, 1 sec Results for lemma disjoint_cons: x s B : [disjoint x :: s & B] = (x \notin B) && [disjoint s & B] FAILURE! Tactics applied: 0 Original Proof: [exact: disjointU1.] Proof search time: 0 min, 2 sec Results for lemma uniq_enumP: e : uniq e -> e =i T -> axiom e FAILURE! Tactics applied: 0 Original Proof: [by move=> Ue sT x; rewrite count_uniq_mem ?sT.] Proof search time: 0 min, 1 sec Results for lemma card_sig: : #|{: {x | P x}}| = #|[pred x | P x]| FAILURE! Tactics applied: 0 Original Proof: [exact: card_sub.] Proof search time: 0 min, 4 sec Results for lemma disjointU1: x A B : [disjoint predU1 x A & B] = (x \notin B) && [disjoint A & B] FAILURE! Tactics applied: 0 Original Proof: [by rewrite disjointU disjoint1.] Proof search time: 0 min, 2 sec Results for lemma cast_ordKV: n1 n2 eq_n : cancel (cast_ord (esym eq_n)) (@cast_ord n1 n2 eq_n) FAILURE! Tactics applied: 0 Original Proof: [by move=> i; exact: val_inj.] Proof search time: 0 min, 4 sec Results for lemma mem_ord_enum: i : i \in ord_enum FAILURE! Tactics applied: 0 Original Proof: [by rewrite -(mem_map ord_inj) val_ord_enum mem_iota ltn_ord.] Proof search time: 0 min, 4 sec Results for lemma card_seq_sub: : uniq s -> #|{:seq_sub}| = size s FAILURE! Tactics applied: 0 Original Proof: [by move=> Us; rewrite cardE enumT -(size_map val) unlock val_seq_sub_enum.] Proof search time: 0 min, 4 sec Results for lemma mem_sum_enum: u : u \in sum_enum FAILURE! Tactics applied: 0 Original Proof: [by case: u => x; rewrite mem_cat -!enumT map_f ?mem_enum ?orbT.] Proof search time: 0 min, 5 sec Results for lemma forall_inP: D P : reflect (forall x, D x -> P x) [forall (x | D x), P x] FAILURE! Tactics applied: 0 Original Proof: [by apply: (iffP (forallP _)) => /= P_ x /=; apply/implyP; apply: P_.] Proof search time: 0 min, 2 sec Results for lemma enum_rank_bij: : bijective enum_rank FAILURE! Tactics applied: 0 Original Proof: [by move: enum_rankK enum_valK; exists (@enum_val T).] Proof search time: 0 min, 4 sec Results for lemma image_injP: A : reflect {in A &, injective f} (#|image f A| == #|A|) FAILURE! Tactics applied: 0 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, 3 sec Results for lemma rev_ordK: n : involutive (@rev_ord n) FAILURE! Tactics applied: 0 Original Proof: [by case: n => [|n] [i lti] //; apply: val_inj; rewrite /= !subSS subKn.] Proof search time: 0 min, 4 sec Results for lemma subset_cardP: A B : #|A| = #|B| -> reflect (A =i B) (A \subset B) FAILURE! Tactics applied: 0 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, 2 sec Results for lemma eq_disjoint_r: B1 B2 : B1 =i B2 -> (@disjoint T)^~ (mem B1) =1 (@disjoint T)^~ (mem B2) FAILURE! Tactics applied: 0 Original Proof: [by move=> eqB12 [A]; congr (_ == 0); apply: eq_card => x; rewrite !inE eqB12.] Proof search time: 0 min, 2 sec Results for fold 6 Results for lemma eq_card: A B : A =i B -> #|A| = #|B| FAILURE! Tactics applied: 1 Original Proof: [by move=>eqAB; rewrite !cardE (eq_enum eqAB).] Proof search time: 0 min, 1 sec Results for lemma eq_disjoint1: x A B : A =i pred1 x -> [disjoint A & B] = (x \notin B) FAILURE! Tactics applied: 4 Original Proof: [by move/eq_disjoint->; exact: disjoint1.] Proof search time: 0 min, 2 sec Results for lemma bumpC: h1 h2 i : bump h1 (bump h2 i) = bump (bump h1 h2) (bump (unbump h2 h1) i) FAILURE! Tactics applied: 4 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, 5 sec Results for lemma invF_f: : cancel f invF FAILURE! Tactics applied: 4 Original Proof: [by move=> x; exact: iinv_f.] Proof search time: 0 min, 4 sec Results for lemma eq_cardT: A : A =i predT -> #|A| = size (enum T) FAILURE! Tactics applied: 4 Original Proof: [exact: eq_card_trans cardT.] Proof search time: 0 min, 1 sec Results for lemma imageP: A y : reflect (exists2 x, x \in A & y = f x) (y \in image f A) FAILURE! Tactics applied: 4 Original Proof: [by apply: (iffP mapP) => [] [x Ax y_fx]; exists x; rewrite // mem_enum in Ax *.] Proof search time: 0 min, 3 sec Results for lemma unbumpK: h : {in predC1 h, cancel (unbump h) (bump h)} FAILURE! Tactics applied: 4 Original Proof: [by move=> i; move/negbTE=> neq_h_i; rewrite unbumpKcond neq_h_i.] Proof search time: 0 min, 5 sec Results for lemma negb_exists: P : ~~ [exists x, P x] = [forall x, ~~ P x] FAILURE! Tactics applied: 4 Original Proof: [by apply/negbLR/esym/eq_existsb=> x; apply: negbK.] Proof search time: 0 min, 2 sec Results for lemma image_pre: (B : pred T') : image f [preim f of B] =i [predI B & codom f] FAILURE! Tactics applied: 4 Original Proof: [by move=> y; rewrite /image_mem -filter_map /= mem_filter -enumT.] Proof search time: 0 min, 3 sec Results for lemma val_enum_ord: : map val (enum 'I_n) = iota 0 n FAILURE! Tactics applied: 4 Original Proof: [by rewrite enumT unlock val_ord_enum.] Proof search time: 0 min, 4 sec Results for lemma unlift_none: n (h : 'I_n) : unlift h h = None FAILURE! Tactics applied: 4 Original Proof: [by case: unliftP => // j Dh; case/eqP: (neq_lift h j).] Proof search time: 0 min, 5 sec Results for lemma exists_eqP: f1 f2 : reflect (exists x, f1 x = f2 x) [exists x, f1 x == f2 x] FAILURE! Tactics applied: 4 Original Proof: [by apply: (iffP (existsP _)) => [] [x /eqP]; exists x.] Proof search time: 0 min, 2 sec Results for lemma negb_forall: P : ~~ [forall x, P x] = [exists x, ~~ P x] FAILURE! Tactics applied: 4 Original Proof: [by [].] Proof search time: 0 min, 2 sec Results for lemma arg_maxP: : extremum_spec geq arg_max FAILURE! Tactics applied: 4 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 Results for lemma bij_on_codom: (x0 : T) : {on [pred y in codom f], bijective f} FAILURE! Tactics applied: 4 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 Results for lemma card0: : #|@pred0 T| = 0 FAILURE! Tactics applied: 4 Original Proof: [by rewrite cardE enum0.] Proof search time: 0 min, 1 sec Results for lemma leq_bump: h i j : (i <= bump h j) = (unbump h i <= j) FAILURE! Tactics applied: 4 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, 5 sec Results for lemma lshift_subproof: m n (i : 'I_m) : i < m + n FAILURE! Tactics applied: 4 Original Proof: [by apply: leq_trans (valP i) _; exact: leq_addr.] Proof search time: 0 min, 5 sec Results for lemma val_sub_enum: : map val sub_enum = enum P FAILURE! Tactics applied: 4 Original Proof: [rewrite pmap_filter; last exact: insubK. by apply: eq_filter => x; exact: isSome_insub.] Proof search time: 0 min, 4 sec Results for lemma inj_card_onto: y : y \in codom f FAILURE! Tactics applied: 4 Original Proof: [by move: y; apply/subset_cardP; rewrite ?card_codom ?subset_predT.] Proof search time: 0 min, 3 sec Results for lemma leq_ord: (i : 'I_n) : i <= n' FAILURE! Tactics applied: 4 Original Proof: [exact: valP i.] Proof search time: 0 min, 5 sec Results for lemma subset_all: s A : (s \subset A) = all (mem A) s FAILURE! Tactics applied: 4 Original Proof: [by exact (sameP (subsetP _ _) allP).] Proof search time: 0 min, 2 sec Results for lemma enum_default: A : 'I_(#|A|) -> T FAILURE! Tactics applied: 4 Original Proof: [by rewrite cardE; case: (enum A) => [|//] [].] Proof search time: 0 min, 4 sec Results for lemma disjoint_cat: s1 s2 A : [disjoint s1 ++ s2 & A] = [disjoint s1 & A] && [disjoint s2 & A] FAILURE! Tactics applied: 4 Original Proof: [by rewrite !disjoint_has has_cat negb_or.] Proof search time: 0 min, 2 sec Results for lemma mem_sub_enum: u : u \in sub_enum FAILURE! Tactics applied: 4 Original Proof: [by rewrite mem_pmap_sub -enumT mem_enum.] Proof search time: 0 min, 3 sec Results for fold 7 Results for lemma splitP: m n (i : 'I_(m + n)) : split_spec i (split i) (i < m) FAILURE! Tactics applied: 3 Original Proof: [rewrite /split {-3}/leq. by case: (@ltnP i m) => cmp_i_m //=; constructor; rewrite ?subnKC.] Proof search time: 0 min, 5 sec Results for lemma dinjectiveP: D : reflect {in D &, injective f} (dinjectiveb D) FAILURE! Tactics applied: 3 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, 3 sec Results for lemma cardC1: x : #|predC1 x| = #|T|.-1 FAILURE! Tactics applied: 3 Original Proof: [by rewrite -(cardC (pred1 x)) card1.] Proof search time: 0 min, 1 sec Results for lemma size_image: A : size (image f A) = #|A| FAILURE! Tactics applied: 3 Original Proof: [by rewrite size_map -cardE.] Proof search time: 0 min, 3 sec Results for lemma eq_forallb: P1 P2 : P1 =1 P2 -> [forall x, P1 x] = [forall x, P2 x] FAILURE! Tactics applied: 3 Original Proof: [by move=> eqP12; apply/negb_inj/eq_existsb=> /= x; rewrite eqP12.] Proof search time: 0 min, 3 sec Results for lemma pre_image: A : [preim f of image f A] =i A FAILURE! Tactics applied: 3 Original Proof: [by move=> x; rewrite inE /= mem_image.] Proof search time: 0 min, 3 sec Results for lemma sub_enum_uniq: : uniq sub_enum FAILURE! Tactics applied: 3 Original Proof: [by rewrite pmap_sub_uniq // -enumT enum_uniq.] Proof search time: 0 min, 4 sec Results for lemma eq_card0: A : A =i pred0 -> #|A| = 0 FAILURE! Tactics applied: 3 Original Proof: [exact: eq_card_trans card0.] Proof search time: 0 min, 1 sec Results for lemma image_iinv: A y (fTy : y \in codom f) : (y \in image f A) = (iinv fTy \in A) FAILURE! Tactics applied: 3 Original Proof: [by rewrite -mem_image ?f_iinv.] Proof search time: 0 min, 3 sec Results for lemma enum_valP: A i : @enum_val A i \in A FAILURE! Tactics applied: 3 Original Proof: [by rewrite -mem_enum mem_nth -?cardE.] Proof search time: 0 min, 4 sec Results for lemma canF_RL: x y : g x = y -> x = f y FAILURE! Tactics applied: 3 Original Proof: [exact: canRL canF_sym.] Proof search time: 0 min, 4 sec Results for lemma eq_card_trans: A B n : #|A| = n -> B =i A -> #|B| = n FAILURE! Tactics applied: 3 Original Proof: [move <-; exact: eq_card.] Proof search time: 0 min, 1 sec Results for lemma lift0: (i : 'I_n') : lift ord0 i = i.+1 :> nat FAILURE! Tactics applied: 3 Original Proof: [by [].] Proof search time: 0 min, 5 sec Results for lemma enum_val_bij: : bijective (@enum_val T) FAILURE! Tactics applied: 3 Original Proof: [by move: enum_rankK enum_valK; exists enum_rank.] Proof search time: 0 min, 4 sec 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: 3 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, 4 sec Results for lemma ltn_ord: (i : ordinal) : i < n FAILURE! Tactics applied: 3 Original Proof: [exact: valP i.] Proof search time: 0 min, 4 sec Results for lemma proper_trans: A B C : A \proper B -> B \proper C -> A \proper C FAILURE! Tactics applied: 3 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, 2 sec Results for lemma bumpK: h : cancel (bump h) (unbump h) FAILURE! Tactics applied: 3 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, 5 sec Results for lemma canF_LR: x y : x = g y -> f x = y FAILURE! Tactics applied: 3 Original Proof: [exact: canLR canF_sym.] Proof search time: 0 min, 3 sec Results for lemma eq_card1: x A : A =i pred1 x -> #|A| = 1 FAILURE! Tactics applied: 3 Original Proof: [exact: eq_card_trans (card1 x).] Proof search time: 0 min, 1 sec Results for lemma card_tagged: : #|{: {i : I & T_ i}}| = sumn (map (fun i => #|T_ i|) (enum I)) FAILURE! Tactics applied: 3 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, 5 sec Results for lemma lift_max: (i : 'I_n') : lift ord_max i = i :> nat FAILURE! Tactics applied: 3 Original Proof: [by rewrite /= /bump leqNgt ltn_ord.] Proof search time: 0 min, 5 sec 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: 3 Original Proof: [exact: nth_image.] Proof search time: 0 min, 4 sec Results for lemma ltn_unsplit: m n (jk : 'I_m + 'I_n) : (unsplit jk < m) = jk FAILURE! Tactics applied: 3 Original Proof: [by case: jk => [j|k]; rewrite /= ?ltn_ord // ltnNge leq_addr.] Proof search time: 0 min, 5 sec Results for lemma card0_eq: A : #|A| = 0 -> A =i pred0 FAILURE! Tactics applied: 3 Original Proof: [by move=> A0 x; apply/idP => Ax; rewrite (cardD1 x) Ax in A0.] Proof search time: 0 min, 1 sec Results for fold 8 Results for lemma existsP: P : reflect (exists x, P x) [exists x, P x] FAILURE! Tactics applied: 0 Original Proof: [by apply: (iffP pred0Pn) => [] [x]; exists x.] Proof search time: 0 min, 3 sec Results for lemma subset_disjoint: A B : (A \subset B) = [disjoint A & [predC B]] FAILURE! Tactics applied: 0 Original Proof: [by rewrite disjoint_sym unlock.] Proof search time: 0 min, 2 sec 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: 0 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 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: 0 Original Proof: [by move=> eqAB eqfg; rewrite /image_mem (eq_enum eqAB) (eq_map eqfg).] Proof search time: 0 min, 3 sec Results for lemma card_prod: : #|{: T1 * T2}| = #|T1| * #|T2| FAILURE! Tactics applied: 0 Original Proof: [by rewrite -cardX; apply: eq_card; case.] Proof search time: 0 min, 5 sec Results for lemma enum_valK: : cancel enum_val enum_rank FAILURE! Tactics applied: 0 Original Proof: [by move=> x; exact: enum_valK_in.] Proof search time: 0 min, 4 sec Results for lemma codomE: : codom f = map f (enum T) FAILURE! Tactics applied: 0 Original Proof: [by [].] Proof search time: 0 min, 3 sec Results for lemma card2: x y : #|pred2 x y| = (x != y).+1 FAILURE! Tactics applied: 0 Original Proof: [by rewrite cardU1 card1 addn1.] Proof search time: 0 min, 1 sec Results for lemma mem_seq_sub_enum: x : x \in seq_sub_enum FAILURE! Tactics applied: 0 Original Proof: [by rewrite mem_undup mem_pmap -valK map_f ?ssvalP.] Proof search time: 0 min, 4 sec Results for lemma prod_enumP: : Finite.axiom prod_enum FAILURE! Tactics applied: 0 Original Proof: [by case=> x1 x2; rewrite (predX_prod_enum (pred1 x1) (pred1 x2)) !card1.] Proof search time: 0 min, 5 sec Results for lemma bij_on_image: A (x0 : T) : {on [pred y in image f A], bijective f} FAILURE! Tactics applied: 0 Original Proof: [exact: subon_bij (@image_codom A) (bij_on_codom x0).] Proof search time: 0 min, 3 sec Results for lemma arg_minP: : extremum_spec leq arg_min FAILURE! Tactics applied: 0 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, 3 sec Results for lemma eq_card_sub: (A : pred sfT) : A =i predT -> #|A| = #|[pred x | P x]| FAILURE! Tactics applied: 0 Original Proof: [exact: eq_card_trans card_sub.] Proof search time: 0 min, 4 sec Results for lemma enum_valK_in: x0 A Ax0 : cancel enum_val (@enum_rank_in x0 A Ax0) FAILURE! Tactics applied: 0 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, 4 sec Results for lemma eq_proper_r: A B : A =i B -> (@proper T)^~ (mem A) =1 (@proper T)^~ (mem B) FAILURE! Tactics applied: 0 Original Proof: [move=> eAB [C]; congr (_ && _); first exact: (eq_subset_r eAB). by rewrite (eq_subset eAB).] Proof search time: 0 min, 2 sec Results for lemma proper_card: A B : A \proper B -> #|A| < #|B| FAILURE! Tactics applied: 0 Original Proof: [by case/andP=> sAB nsBA; rewrite ltn_neqAle !(subset_leqif_card sAB) andbT.] Proof search time: 0 min, 2 sec Results for lemma eq_invF: f g injf injg : f =1 g -> @invF T f injf =1 @invF T g injg FAILURE! Tactics applied: 0 Original Proof: [by move=> eq_fg x; apply: (canLR (invF_f injf)); rewrite eq_fg f_invF.] Proof search time: 0 min, 4 sec Results for lemma enum_val_bij_in: x0 A : x0 \in A -> {on A, bijective (@enum_val A)} FAILURE! Tactics applied: 0 Original Proof: [move=> Ax0; exists (enum_rank_in Ax0) => [i _|]; last exact: enum_rankK_in. exact: enum_valK_in.] Proof search time: 0 min, 4 sec Results for lemma unbumpKcond: h i : bump h (unbump h i) = (i == h) + i FAILURE! Tactics applied: 0 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, 5 sec 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 FAILURE! Tactics applied: 0 Original Proof: [exact: val_inj.] Proof search time: 0 min, 4 sec Results for lemma nth_enum_ord: i0 m : m < n -> nth i0 (enum 'I_n) m = m :> nat FAILURE! Tactics applied: 0 Original Proof: [by move=> ?; rewrite -(nth_map _ 0) (size_enum_ord, val_enum_ord) // nth_iota.] Proof search time: 0 min, 4 sec Results for lemma canF_eq: x y : (f x == y) = (x == g y) FAILURE! Tactics applied: 0 Original Proof: [exact: (can2_eq fK canF_sym).] Proof search time: 0 min, 3 sec Results for lemma leq_image_card: A : #|image f A| <= #|A| FAILURE! Tactics applied: 0 Original Proof: [by rewrite (cardE A) -(size_map f) card_size.] Proof search time: 0 min, 3 sec Results for lemma disjoint_subset: A B : [disjoint A & B] = (A \subset [predC B]) FAILURE! Tactics applied: 0 Original Proof: [by rewrite subset_disjoint; apply: eq_disjoint_r => x; rewrite !inE /= negbK.] Proof search time: 0 min, 2 sec Results for lemma forallP: P : reflect (forall x, P x) [forall x, P x] FAILURE! Tactics applied: 0 Original Proof: [by apply: (iffP pred0P) => /= P_ x; rewrite /= ?P_ ?(negbFE (P_ x)).] Proof search time: 0 min, 2 sec Results for fold 9 Results for lemma pred0Pn: P : reflect (exists x, P x) (~~ pred0b P) FAILURE! Tactics applied: 1 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 Results for lemma subxx: (pT : predType T) (pA : pT) : pA \subset pA FAILURE! Tactics applied: 1 Original Proof: [by [].] Proof search time: 0 min, 2 sec Results for lemma canF_invF: : g =1 invF (can_inj fK) FAILURE! Tactics applied: 1 Original Proof: [by move=> y; apply: (canLR fK); rewrite f_invF.] Proof search time: 0 min, 4 sec Results for lemma mem_image: A x : (f x \in image f A) = (x \in A) FAILURE! Tactics applied: 1 Original Proof: [by rewrite mem_map ?mem_enum.] Proof search time: 0 min, 3 sec Results for lemma proper_sub_trans: A B C : A \proper B -> B \subset C -> A \proper C FAILURE! Tactics applied: 1 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, 2 sec Results for lemma cast_ord_inj: n1 n2 eq_n : injective (@cast_ord n1 n2 eq_n) FAILURE! Tactics applied: 1 Original Proof: [exact: can_inj (cast_ordK eq_n).] Proof search time: 0 min, 4 sec Results for lemma enum_ordS: : enum 'I_n = ord0 :: map (lift ord0) (enum 'I_n') FAILURE! Tactics applied: 1 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, 5 sec Results for lemma cardUI: A B : #|[predU A & B]| + #|[predI A & B]| = #|A| + #|B| FAILURE! Tactics applied: 1 Original Proof: [by rewrite !cardE -!count_filter count_predUI.] Proof search time: 0 min, 1 sec Results for lemma rshift_subproof: m n (i : 'I_n) : m + i < m + n FAILURE! Tactics applied: 1 Original Proof: [by rewrite ltn_add2l.] Proof search time: 0 min, 5 sec 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: 1 Original Proof: [by move=> eqP12; apply: eq_forallb => i; case Di: (D i); rewrite // eqP12.] Proof search time: 0 min, 3 sec Results for lemma tag_enumP: : Finite.axiom tag_enum FAILURE! Tactics applied: 1 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, 5 sec Results for lemma preim_iinv: A B y fAy : preim f B (@iinv A y fAy) = B y FAILURE! Tactics applied: 1 Original Proof: [by rewrite /= f_iinv.] Proof search time: 0 min, 3 sec Results for lemma cardU1: x A : #|[predU1 x & A]| = (x \notin A) + #|A| FAILURE! Tactics applied: 1 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, 1 sec Results for lemma unbump_addl: h i k : unbump (k + h) (k + i) = k + unbump h i FAILURE! Tactics applied: 1 Original Proof: [apply: (can_inj (bumpK (k + h))). by rewrite bump_addl !unbumpKcond eqn_add2l addnCA.] Proof search time: 0 min, 5 sec Results for lemma eqfunP: f1 f2 : reflect (forall x, f1 x = f2 x) [forall x, f1 x == f2 x] FAILURE! Tactics applied: 1 Original Proof: [by apply: (iffP (forallP _)) => eq_f12 x; apply/eqP/eq_f12.] Proof search time: 0 min, 2 sec 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: 1 Original Proof: [move=> x Ax; rewrite /= insubdK ?nth_index ?mem_enum //. by rewrite cardE [_ \in _]index_mem mem_enum.] Proof search time: 0 min, 4 sec Results for lemma widen_ord_proof: n m (i : 'I_n) : n <= m -> i < m FAILURE! Tactics applied: 1 Original Proof: [exact: leq_trans.] Proof search time: 0 min, 4 sec Results for lemma lift_inj: n (h : 'I_n) : injective (lift h) FAILURE! Tactics applied: 1 Original Proof: [move=> i1 i2; move/eqP; rewrite [_ == _](can_eq (@bumpK _)) => eq_i12. exact/eqP.] Proof search time: 0 min, 5 sec Results for lemma sub_ord_proof: m : n' - m < n FAILURE! Tactics applied: 1 Original Proof: [by rewrite ltnS leq_subr.] Proof search time: 0 min, 5 sec Results for lemma card_gt0P: A : reflect (exists i, i \in A) (#|A| > 0) FAILURE! Tactics applied: 1 Original Proof: [rewrite lt0n; exact: pred0Pn.] Proof search time: 0 min, 1 sec Results for lemma enum_val_inj: A : injective (@enum_val A) FAILURE! Tactics applied: 1 Original Proof: [by move=> i; exact: can_inj (enum_valK_in (enum_valP i)) (i).] Proof search time: 0 min, 4 sec Results for lemma unsplitK: m n : cancel (@unsplit m n) (@split m n) FAILURE! Tactics applied: 1 Original Proof: [move=> jk; have:= ltn_unsplit jk. by do [case: splitP; case: jk => //= i j] => [|/addnI] => /ord_inj->.] Proof search time: 0 min, 5 sec Results for lemma enum_rank_inj: : injective enum_rank FAILURE! Tactics applied: 1 Original Proof: [exact: can_inj enum_rankK.] Proof search time: 0 min, 4 sec Results for lemma eq_pick: P Q : P =1 Q -> pick P = pick Q FAILURE! Tactics applied: 1 Original Proof: [by move=> eqPQ; rewrite /pick (eq_enum eqPQ).] Proof search time: 0 min, 1 sec Results for lemma index_enum_ord: (i : 'I_n) : index i (enum 'I_n) = i FAILURE! Tactics applied: 1 Original Proof: [by rewrite -{1}(nth_ord_enum i i) index_uniq ?(enum_uniq, size_enum_ord).] Proof search time: 0 min, 4 sec Results for fold 10 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: 1 Original Proof: [by move=> eqP12; apply: eq_existsb => x; apply: andb_id2l => /eqP12.] Proof search time: 0 min, 3 sec Results for lemma unbumpS: h i : unbump h.+1 i.+1 = (unbump h i).+1 FAILURE! Tactics applied: 1 Original Proof: [exact: unbump_addl 1.] Proof search time: 0 min, 5 sec Results for lemma card_bool: : #|{: bool}| = 2 FAILURE! Tactics applied: 1 Original Proof: [by rewrite cardT enumT unlock.] Proof search time: 0 min, 4 sec Results for lemma card_in_image: A : {in A &, injective f} -> #|image f A| = #|A| FAILURE! Tactics applied: 1 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, 3 sec Results for lemma eq_disjoint0: A B : A =i pred0 -> [disjoint A & B] FAILURE! Tactics applied: 1 Original Proof: [by move/eq_disjoint->; exact: disjoint0.] Proof search time: 0 min, 2 sec Results for lemma size_enum_ord: : size (enum 'I_n) = n FAILURE! Tactics applied: 1 Original Proof: [by rewrite -(size_map val) val_enum_ord size_iota.] Proof search time: 0 min, 4 sec Results for lemma eq_proper: A B : A =i B -> proper (mem A) =1 proper (mem B) FAILURE! Tactics applied: 1 Original Proof: [move=> eAB [C]; congr (_ && _); first exact: (eq_subset eAB). by rewrite (eq_subset_r eAB).] Proof search time: 0 min, 2 sec Results for lemma f_invF: : cancel invF f FAILURE! Tactics applied: 1 Original Proof: [by move=> y; exact: f_iinv.] Proof search time: 0 min, 4 sec Results for lemma disjointU: A B C : [disjoint predU A B & C] = [disjoint A & C] && [disjoint B & C] FAILURE! Tactics applied: 1 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, 2 sec Results for lemma disjoint_trans: A B C : A \subset B -> [disjoint B & C] -> [disjoint A & C] FAILURE! Tactics applied: 1 Original Proof: [by rewrite 2!disjoint_subset; exact: subset_trans.] Proof search time: 0 min, 2 sec Results for lemma splitK: m n : cancel (@split m n) (@unsplit m n) FAILURE! Tactics applied: 1 Original Proof: [by move=> i; apply: val_inj; case: splitP.] Proof search time: 0 min, 5 sec Results for lemma injectiveP: : reflect (injective f) injectiveb FAILURE! Tactics applied: 1 Original Proof: [apply: (iffP (dinjectiveP _)) => injf x y => [|_ _]; exact: injf.] Proof search time: 0 min, 3 sec Results for lemma cast_ordK: n1 n2 eq_n : cancel (@cast_ord n1 n2 eq_n) (cast_ord (esym eq_n)) FAILURE! Tactics applied: 1 Original Proof: [by move=> i; exact: val_inj.] Proof search time: 0 min, 4 sec Results for lemma subxx_hint: (mA : mem_pred T) : subset mA mA FAILURE! Tactics applied: 1 Original Proof: [by case: mA => A; have:= introT (subsetP A A); rewrite !unlock => ->.] Proof search time: 0 min, 2 sec Results for lemma card_image: A : #|image f A| = #|A| FAILURE! Tactics applied: 1 Original Proof: [apply: card_in_image; exact: in2W.] Proof search time: 0 min, 3 sec Results for lemma proper_sub: A B : A \proper B -> A \subset B FAILURE! Tactics applied: 1 Original Proof: [by case/andP.] Proof search time: 0 min, 2 sec Results for lemma predX_prod_enum: (A1 : pred T1) (A2 : pred T2) : count [predX A1 & A2] prod_enum = #|A1| * #|A2| FAILURE! Tactics applied: 1 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, 5 sec Results for lemma seq_sub_pickleK: : pcancel seq_sub_pickle seq_sub_unpickle FAILURE! Tactics applied: 1 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, 4 sec OVERALL RESULTS SUMMARY EFSMProver proved 8 out of 243 lemmas. Success rate of 3.292181069958848% There were 0 errors. 235 proof attempts exhausted the automaton On average, a proof was found after applying 5712 tactics The longest proof consisted of 2 tactics There were 0 shorter proofs found Of the 235 failures, 42 of them used all 100000 tactics There were 5 reused proofs found There were 3 novel proofs found Of the 235 failures, the average number of tactics used was 17873On average, a proof was found after 0 min, 9 sec On average, a failed proof attempt took 0 min, 22 sec On average, any (success or failure) proof attempt took 0 min, 22 sec The longest time to find a proof was 0 min, 31 sec The shortest time to find a proof was 0 min, 1 sec There were 0 proofs containing repeated tactics There were 0 proofs that repeated states