Results for fold 1 Results for lemma andNb: b : ~~ b && b = false SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 8 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 7 Results for fold 2 Results for lemma contraFF: (c b : bool) : (c -> b) -> b = false -> c = false FAILURE! Tactics applied: 10000 Original Proof: [by move/contraFN=> bF_notc /bF_notc/negbTE.] Proof search time: 0 min, 7 sec Number of successful tactic applications: 181 Number of failed tactic applications: 9820 Results for fold 3 Results for lemma in2W: : {all2 P2} -> {in D1 & D2, {all2 P2}} SUCCESS! Proof Found in EFSM: by move=> *; Tactics applied: 51 Original Proof: [by move=> ? ?.] 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: 50 Results for fold 4 Results for lemma on2T: : {on T2 &, allQ2 f} -> allQ2 f SUCCESS! Proof Found in EFSM: move => symR x y; auto. Tactics applied: 389 Original Proof: [by move=> ? ?; auto.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 0 sec Number of successful tactic applications: 14 Number of failed tactic applications: 375 Results for fold 5 Results for lemma orb_idl: (a b : bool) : (a -> b) -> a || b = b FAILURE! Tactics applied: 2016 Original Proof: [by case: a; case: b => // ->.] Proof search time: 0 min, 2 sec Number of successful tactic applications: 50 Number of failed tactic applications: 1966 Results for fold 6 Results for lemma orTb: : forall b, true || b SUCCESS! Proof Found in EFSM: by []. Tactics applied: 1 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: 0 Results for fold 7 Results for lemma orbACA: : interchange orb orb SUCCESS! Proof Found in EFSM: by do 3!case. Tactics applied: 38 Original Proof: [by do 4!case.] 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: 37 Results for fold 8 Results for lemma on2W: : allQ2 f -> {on D2 &, allQ2 f} SUCCESS! Proof Found in EFSM: by move=> *; Tactics applied: 67 Original Proof: [by move=> ? ?.] 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: 66 Results for fold 9 Results for lemma introN: : ~ P -> ~~ b SUCCESS! Proof Found in EFSM: by case Pb. Tactics applied: 7 Original Proof: [exact: introNTF true _.] 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: 6 Results for fold 10 Results for lemma andbK: a b : a && b || a = a FAILURE! Tactics applied: 167 Original Proof: [by case: a; case: b.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 167 Results for fold 11 Results for lemma can_mono_in: : {in aD &, {mono f : x y / aR x y >-> rR x y}} -> {in rD &, {mono g : x y / rR x y >-> aR x y}} FAILURE! Tactics applied: 10000 Original Proof: [by move=> mf x y hx hy /=; rewrite -mf // !fgK_on.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 396 Number of failed tactic applications: 9605 Results for fold 12 Results for lemma introTFn: : (if c then ~ P else P) -> b = c FAILURE! Tactics applied: 10000 Original Proof: [by move/(introNTF Hb) <-; case b.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 809 Number of failed tactic applications: 9192 Results for fold 13 Results for lemma is_true_locked_true: : locked true FAILURE! Tactics applied: 162 Original Proof: [by unlock.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 162 Results for fold 14 Results for lemma ifE: : (if b then vT else vF) = if_expr SUCCESS! Proof Found in EFSM: by []. Tactics applied: 1 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: 0 Results for fold 15 Results for lemma negbFE: b : ~~ b = false -> b SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 8 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 7 Results for fold 16 Results for lemma elimTF: : b = c -> if c then P else ~ P SUCCESS! Proof Found in EFSM: rewrite -if_neg; case Hb. case : c => // ->. case : c => // ->. Tactics applied: 1752 Original Proof: [by move <-; case Hb.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state This proof contained a sequence of repeated tactics proof search time: 0 min, 2 sec Number of successful tactic applications: 56 Number of failed tactic applications: 1696 Results for fold 17 Results for lemma negb_imply: a b : ~~ (a ==> b) = a && ~~ b SUCCESS! Proof Found in EFSM: by case: a; Tactics applied: 37 Original Proof: [by case: a; case: b.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 36 Results for fold 18 Results for lemma introF: : ~ P -> b = false SUCCESS! Proof Found in EFSM: by case Pb. Tactics applied: 56 Original Proof: [exact: introTF false _.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 53 Results for fold 19 Results for lemma negb_and: (a b : bool) : ~~ (a && b) = ~~ a || ~~ b SUCCESS! Proof Found in EFSM: by case: a; Tactics applied: 52 Original Proof: [by case: a; case: b.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 51 Results for fold 20 Results for lemma symmetric_from_pre: : pre_symmetric -> symmetric FAILURE! Tactics applied: 559 Original Proof: [move=> symR x y; apply/idP/idP; exact: symR.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 554 Results for fold 21 Results for lemma onW_bij: : bijective f -> {on D2, bijective f} FAILURE! Tactics applied: 196 Original Proof: [by case=> g' fK g'K; exists g' => * ? *; auto.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 4 Number of failed tactic applications: 192 Results for fold 22 Results for lemma all_and4: (hP : forall x, [/\ P1 x, P2 x, P3 x & P4 x]) : [/\ a P1, a P2, a P3 & a P4] FAILURE! Tactics applied: 163 Original Proof: [by split=> x; case: (hP x).] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 163 Results for fold 23 Results for lemma app_predE: x p (ap : manifest_applicative_pred p) : ap x = (x \in p) FAILURE! Tactics applied: 162 Original Proof: [by case: ap => _ /= ->.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 162 Results for fold 24 Results for lemma classic_EM: : forall P, classically (decidable P) FAILURE! Tactics applied: 207 Original Proof: [by move=> P [] // IH; apply IH; right => ?; apply: notF (IH _); left.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 4 Number of failed tactic applications: 203 Results for fold 25 Results for lemma sub_refl: T (p : mem_pred T) : sub_mem p p SUCCESS! Proof Found in EFSM: by []. Tactics applied: 27 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 24 Results for fold 26 Results for lemma andbA: : associative andb SUCCESS! Proof Found in EFSM: by case. Tactics applied: 2 Original Proof: [by do 3!case.] 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: 1 Results for fold 27 Results for lemma orbb: : idempotent orb SUCCESS! Proof Found in EFSM: by case. Tactics applied: 2 Original Proof: [by case.] 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: 1 Results for fold 28 Results for lemma orb_andl: : left_distributive orb andb SUCCESS! Proof Found in EFSM: by do 3!case. Tactics applied: 38 Original Proof: [by do 3!case.] 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: 37 Results for fold 29 Results for lemma implyNb: a b : (~~ a ==> b) = a || b SUCCESS! Proof Found in EFSM: by case: a; Tactics applied: 21 Original Proof: [by case: a; case: b.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 20 Results for fold 30 Results for lemma introNf: : P -> ~~ b = false SUCCESS! Proof Found in EFSM: by case Pb. Tactics applied: 7 Original Proof: [exact: introNTF false _.] 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: 6 Results for fold 31 Results for lemma contraTF: (c b : bool) : (c -> ~~ b) -> b -> c = false FAILURE! Tactics applied: 10000 Original Proof: [by move/contraL=> b_notc /b_notc/negbTE.] Proof search time: 0 min, 14 sec Number of successful tactic applications: 525 Number of failed tactic applications: 9476 Results for fold 32 Results for lemma introP: : (b -> Q) -> (~~ b -> ~ Q) -> reflect Q b FAILURE! Tactics applied: 167 Original Proof: [by case b; constructor; auto.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 167 Results for fold 33 Results for lemma on1W: : allQ1 f -> {on D2, allQ1 f} SUCCESS! Proof Found in EFSM: move => T P [] // IH; Tactics applied: 9 Original Proof: [by move=> ? ?.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 6 Results for fold 34 Results for lemma contraR: (c b : bool) : (~~ c -> b) -> ~~ b -> c FAILURE! Tactics applied: 10000 Original Proof: [by case: b => //; case: c.] Proof search time: 0 min, 14 sec Number of successful tactic applications: 528 Number of failed tactic applications: 9473 Results for fold 35 Results for lemma andb_orr: : right_distributive andb orb SUCCESS! Proof Found in EFSM: by case. Tactics applied: 2 Original Proof: [by do 3!case.] 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: 1 Results for fold 36 Results for lemma if_same: : (if b then vT else vT) = vT SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 37 Original Proof: [by case b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 36 Results for fold 37 Results for lemma implybE: a b : (a ==> b) = ~~ a || b SUCCESS! Proof Found in EFSM: by case: a; Tactics applied: 50 Original Proof: [by case: a; case: b.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 49 Results for fold 38 Results for lemma implybN: a b : (a ==> ~~ b) = (b ==> ~~ a) FAILURE! Tactics applied: 162 Original Proof: [by case: a; case: b.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 162 Results for fold 39 Results for lemma addbC: : commutative addb SUCCESS! Proof Found in EFSM: by do 2!case. Tactics applied: 66 Original Proof: [by do 2!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 61 Results for fold 40 Results for lemma andbT: : right_id true andb SUCCESS! Proof Found in EFSM: by case. Tactics applied: 2 Original Proof: [by case.] 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: 1 Results for fold 41 Results for lemma orb_andr: : right_distributive orb andb SUCCESS! Proof Found in EFSM: by case. Tactics applied: 2 Original Proof: [by do 3!case.] 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: 1 Results for fold 42 Results for lemma andb_idl: (a b : bool) : (b -> a) -> a && b = b FAILURE! Tactics applied: 10000 Original Proof: [by case: a; case: b => // ->.] Proof search time: 0 min, 13 sec Number of successful tactic applications: 1000 Number of failed tactic applications: 9001 Results for fold 43 Results for lemma implyb_idl: (a b : bool) : (~~ a -> b) -> (a ==> b) = b FAILURE! Tactics applied: 8980 Original Proof: [by case: a; case: b => // ->.] Proof search time: 0 min, 12 sec Number of successful tactic applications: 289 Number of failed tactic applications: 8691 Results for fold 44 Results for lemma andb_orl: : left_distributive andb orb SUCCESS! Proof Found in EFSM: by do 3!case. Tactics applied: 38 Original Proof: [by do 3!case.] 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: 37 Results for fold 45 Results for lemma not_false_is_true: : ~ false SUCCESS! Proof Found in EFSM: by []. Tactics applied: 1 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: 0 Results for fold 46 Results for lemma equivPif: : (Q -> P) -> (P -> Q) -> if b then Q else ~ Q FAILURE! Tactics applied: 10000 Original Proof: [by case Hb; auto.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 68 Number of failed tactic applications: 9933 Results for fold 47 Results for lemma sym_right_transitive: : right_transitive FAILURE! Tactics applied: 10000 Original Proof: [by move=> x y /sym_left_transitive Rxy z; rewrite !(symR z) Rxy.] Proof search time: 0 min, 14 sec Number of successful tactic applications: 432 Number of failed tactic applications: 9569 Results for fold 48 Results for lemma elimNTF: : ~~ b = c -> if c then ~ P else P FAILURE! Tactics applied: 10000 Original Proof: [by move <-; case Hb.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 139 Number of failed tactic applications: 9862 Results for fold 49 Results for lemma sub_in_bij: (D1' : pred T1) : {subset D1 <= D1'} -> {in D1', bijective f} -> {in D1, bijective f} FAILURE! Tactics applied: 10000 Original Proof: [by move=> subD [g' fK g'K]; exists g' => x; move/subD; [exact: fK | exact: g'K].] Proof search time: 0 min, 21 sec Number of successful tactic applications: 327 Number of failed tactic applications: 9674 Results for fold 50 Results for lemma andbCA: : left_commutative andb SUCCESS! Proof Found in EFSM: by do 2!case. Tactics applied: 37 Original Proof: [by do 3!case.] 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: 36 Results for fold 51 Results for lemma monoLR_in: : {in aD &, {mono f : x y / aR x y >-> rR x y}} -> {in aD & rD, forall x y, rR (f x) y = aR x (g y)} FAILURE! Tactics applied: 10000 Original Proof: [by move=> mf x y hx hy; rewrite -{1}[y]fgK_on // mf.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 295 Number of failed tactic applications: 9706 Results for fold 52 Results for lemma ifP: : if_spec (b = false) b (if b then vT else vF) FAILURE! Tactics applied: 165 Original Proof: [by case def_b: b; constructor.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 165 Results for fold 53 Results for lemma wlog_neg: b : (~~ b -> b) -> b SUCCESS! Proof Found in EFSM: by case: b => // ->. Tactics applied: 26 Original Proof: [by case: b => // ->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 25 Results for fold 54 Results for lemma ifT: : b -> (if b then vT else vF) = vT SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 49 Original Proof: [by move->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 46 Results for fold 55 Results for lemma on_can_inj: : {on D2, cancel f & g} -> {on D2 &, injective f} SUCCESS! Proof Found in EFSM: by move=> fK x y /fK{2}<- /fK{2}<- ->. Tactics applied: 86 Original Proof: [by move=> fK x y /fK{2}<- /fK{2}<- ->.] 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: 85 Results for fold 56 Results for lemma rwP2: : reflect Q b -> (P <-> Q) FAILURE! Tactics applied: 10000 Original Proof: [by move=> Qb; split=> ?; [exact: appP | apply: elimT; case: Qb].] Proof search time: 0 min, 13 sec Number of successful tactic applications: 876 Number of failed tactic applications: 9125 Results for fold 57 Results for lemma monoW_in: : {in aD &, {mono f : x y / aR x y >-> rR x y}} -> {in aD &, {homo f : x y / aR x y >-> rR x y}} FAILURE! Tactics applied: 10000 Original Proof: [by move=> hf x y hx hy axy; rewrite hf.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 229 Number of failed tactic applications: 9772 Results for fold 58 Results for lemma implyFb: b : false ==> b SUCCESS! Proof Found in EFSM: by []. Tactics applied: 1 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: 0 Results for fold 59 Results for lemma decPcases: : if b then P else ~ P SUCCESS! Proof Found in EFSM: by case def_b: b / Pb; Tactics applied: 60 Original Proof: [by case Pb.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 57 Results for fold 60 Results for lemma homo_mono_in: : {in aD &, {homo f : x y / aR x y >-> rR x y}} -> {in rD &, {homo g : x y / rR x y >-> aR x y}} -> {in rD &, {mono g : x y / rR x y >-> aR x y}} FAILURE! Tactics applied: 10000 Original Proof: [move=> mf mg x y hx hy; case: (boolP (rR _ _))=> [/mg //|]; first exact. by apply: contraNF=> /mf; rewrite !fgK_on //; apply.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 313 Number of failed tactic applications: 9688 Results for fold 61 Results for lemma inW_bij: : bijective f -> {in D1, bijective f} FAILURE! Tactics applied: 10000 Original Proof: [by case=> g' fK g'K; exists g' => * ? *; auto.] Proof search time: 0 min, 32 sec Number of successful tactic applications: 279 Number of failed tactic applications: 9722 Results for fold 62 Results for lemma implybF: b : (b ==> false) = ~~ b SUCCESS! Proof Found in EFSM: split => [eqiR | [Rxx trR] x y z *]; Tactics applied: 17 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 16 Results for fold 63 Results for lemma addbI: : right_injective addb SUCCESS! Proof Found in EFSM: by do 3!case. Tactics applied: 38 Original Proof: [by do 3!case.] 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: 37 Results for fold 64 Results for lemma monoLR: : {mono f : x y / aR x y >-> rR x y} -> forall x y, rR (f x) y = aR x (g y) FAILURE! Tactics applied: 10000 Original Proof: [by move=> mf x y; rewrite -{1}[y]fgK mf.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 418 Number of failed tactic applications: 9583 Results for fold 65 Results for lemma in_collective: x p (msp : manifest_simpl_pred p) : (x \in collective_pred_of_simpl msp) = p x SUCCESS! Proof Found in EFSM: by case: msp => _ /= ->. Tactics applied: 98 Original Proof: [by case: msp => _ /= ->.] 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: 97 Results for fold 66 Results for lemma in2T: : {in T1 & T2, {all2 P2}} -> {all2 P2} SUCCESS! Proof Found in EFSM: auto. Tactics applied: 21 Original Proof: [by move=> ? ?; auto.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 16 Results for fold 67 Results for lemma iffP: : (P -> Q) -> (Q -> P) -> reflect Q b FAILURE! Tactics applied: 196 Original Proof: [by case: Pb; constructor; auto.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 196 Results for fold 68 Results for lemma canRL_in: x y : {in D1, cancel f g} -> x \in D1 -> f x = y -> x = g y FAILURE! Tactics applied: 7787 Original Proof: [by move=> fK D1x <-; rewrite fK.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 164 Number of failed tactic applications: 7623 Results for fold 69 Results for lemma can_in_inj: : {in D1, cancel f g} -> {in D1 &, injective f} SUCCESS! Proof Found in EFSM: by move=> fK x y /fK{2}<- /fK{2}<- ->. Tactics applied: 128 Original Proof: [by move=> fK x y /fK{2}<- /fK{2}<- ->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 11 Number of failed tactic applications: 117 Results for fold 70 Results for lemma sub_in11: (Ph : ph {all2 P2}) : prop_in11 d1' d2' Ph -> prop_in11 d1 d2 Ph FAILURE! Tactics applied: 267 Original Proof: [move=> allP x1 x2 /sub1 d1x1 /sub2; exact: allP.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 8 Number of failed tactic applications: 259 Results for fold 71 Results for lemma elimF: : b = false -> ~ P SUCCESS! Proof Found in EFSM: by case Pb. Tactics applied: 55 Original Proof: [exact: elimTF false _.] 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: 54 Results for fold 72 Results for lemma bind_unless: C P {Q} : unless C P -> unless (unless C Q) P FAILURE! Tactics applied: 1010 Original Proof: [by move=> haveP suffPQ suffQ; apply: haveP => /suffPQ; exact.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 11 Number of failed tactic applications: 999 Results for fold 73 Results for lemma addbCA: : left_commutative addb SUCCESS! Proof Found in EFSM: by do 2!case. Tactics applied: 37 Original Proof: [by do 3!case.] 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: 36 Results for fold 74 Results for lemma idPn: : reflect (~~ b1) (~~ b1) SUCCESS! Proof Found in EFSM: case b1; first by constructor. constructor => //; Tactics applied: 345 Original Proof: [by case b1; constructor.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 0 sec Number of successful tactic applications: 26 Number of failed tactic applications: 319 Results for fold 75 Results for lemma equivalence_relP: : equivalence_rel <-> reflexive /\ left_transitive FAILURE! Tactics applied: 10000 Original Proof: [split=> [eqiR | [Rxx trR] x y z]; last by split=> [|/trR->]. by split=> [x | x y Rxy z]; [rewrite (eqiR x x x) | rewrite (eqiR x y z)].] Proof search time: 0 min, 15 sec Number of successful tactic applications: 409 Number of failed tactic applications: 9592 Results for fold 76 Results for lemma negbT: b : b = false -> ~~ b SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 53 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 50 Results for fold 77 Results for lemma in1T: : {in T1, {all1 P1}} -> {all1 P1} SUCCESS! Proof Found in EFSM: auto. Tactics applied: 32 Original Proof: [by move=> ? ?; auto.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 29 Results for fold 78 Results for lemma all_and5: (hP : forall x, [/\ P1 x, P2 x, P3 x, P4 x & P5 x]) : [/\ a P1, a P2, a P3, a P4 & a P5] FAILURE! Tactics applied: 10000 Original Proof: [by split=> x; case: (hP x).] Proof search time: 0 min, 14 sec Number of successful tactic applications: 96 Number of failed tactic applications: 9905 Results for fold 79 Results for lemma negPf: : reflect (b1 = false) (~~ b1) SUCCESS! Proof Found in EFSM: case b1; constructor => //; Tactics applied: 365 Original Proof: [by case b1; constructor.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 0 sec Number of successful tactic applications: 25 Number of failed tactic applications: 340 Results for fold 80 Results for lemma andbF: : right_zero false andb SUCCESS! Proof Found in EFSM: by case. Tactics applied: 2 Original Proof: [by case.] 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: 1 Results for fold 81 Results for lemma keyed_predE: : k_p =i p FAILURE! Tactics applied: 975 Original Proof: [by case: k_p.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 15 Number of failed tactic applications: 960 Results for fold 82 Results for lemma andKb: a b : a || b && a = a FAILURE! Tactics applied: 195 Original Proof: [by case: a; case: b.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 194 Results for fold 83 Results for lemma andbb: : idempotent andb SUCCESS! Proof Found in EFSM: by case. Tactics applied: 14 Original Proof: [by case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 11 Results for fold 84 Results for lemma subon_bij: (D2' : pred T2) : {subset D2 <= D2'} -> {on D2', bijective f} -> {on D2, bijective f} FAILURE! Tactics applied: 209 Original Proof: [by move=> subD [g' fK g'K]; exists g' => x; move/subD; [exact: fK | exact: g'K].] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 207 Results for fold 85 Results for lemma andb_id2r: (a b c : bool) : (b -> a = c) -> a && b = c && b FAILURE! Tactics applied: 10000 Original Proof: [by case: a; case: b; case: c => // ->.] Proof search time: 0 min, 14 sec Number of successful tactic applications: 1164 Number of failed tactic applications: 8837 Results for fold 86 Results for lemma negbRL: b c : ~~ b = c -> b = ~~ c FAILURE! Tactics applied: 246 Original Proof: [exact: canRL negbK.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 241 Results for fold 87 Results for lemma negbF: b : (b : bool) -> ~~ b = false SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 33 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 30 Results for fold 88 Results for lemma sub_in2: T d d' (P : T -> T -> Prop) : sub_mem d d' -> forall Ph : ph {all2 P}, prop_in2 d' Ph -> prop_in2 d Ph FAILURE! Tactics applied: 273 Original Proof: [by move=> /= sub_dd'; exact: sub_in11.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 9 Number of failed tactic applications: 264 Results for fold 89 Results for lemma andP: : reflect (b1 /\ b2) (b1 && b2) FAILURE! Tactics applied: 10000 Original Proof: [by case b1; case b2; constructor=> //; case.] Proof search time: 0 min, 12 sec Number of successful tactic applications: 524 Number of failed tactic applications: 9477 Results for fold 90 Results for lemma contraFN: (c b : bool) : (c -> b) -> b = false -> ~~ c FAILURE! Tactics applied: 10000 Original Proof: [by move/contra=> notb_notc /negbT.] Proof search time: 0 min, 8 sec Number of successful tactic applications: 415 Number of failed tactic applications: 9586 Results for fold 91 Results for lemma ifF: : b = false -> (if b then vT else vF) = vF SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 43 Original Proof: [by move->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 40 Results for fold 92 Results for lemma subon1: (Phf : ph (allQ1 f)) (Ph : ph (allQ1 f)) : prop_on1 d2' Phf Ph -> prop_on1 d2 Phf Ph FAILURE! Tactics applied: 231 Original Proof: [by move=> allQ x /sub2; exact: allQ.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 6 Number of failed tactic applications: 225 Results for fold 93 Results for lemma mem_simpl: sp : mem sp = sp :> pred T SUCCESS! Proof Found in EFSM: split => [eqiR | [Rxx trR] x y z *]; Tactics applied: 7 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: 6 Results for fold 94 Results for lemma implyP: : reflect (b1 -> b2) (b1 ==> b2) FAILURE! Tactics applied: 10000 Original Proof: [by case b1; case b2; constructor; auto.] Proof search time: 0 min, 12 sec Number of successful tactic applications: 931 Number of failed tactic applications: 9070 Results for fold 95 Results for lemma all_and3: (hP : forall x, [/\ P1 x, P2 x & P3 x]) : [/\ a P1, a P2 & a P3] FAILURE! Tactics applied: 674 Original Proof: [by split=> x; case: (hP x).] Proof search time: 0 min, 0 sec Number of successful tactic applications: 6 Number of failed tactic applications: 668 Results for fold 96 Results for lemma orbAC: : right_commutative orb SUCCESS! Proof Found in EFSM: by do 3!case. Tactics applied: 96 Original Proof: [by do 3!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 91 Results for fold 97 Results for lemma and3P: : reflect [/\ b1, b2 & b3] [&& b1, b2 & b3] FAILURE! Tactics applied: 170 Original Proof: [by case b1; case b2; case b3; constructor; try by case.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 168 Results for fold 98 Results for lemma in_applicative: x p (amp : applicative_mem_pred p) : in_mem x amp = p x FAILURE! Tactics applied: 168 Original Proof: [by case: amp => [[_ /= ->]].] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 168 Results for fold 99 Results for lemma fun_if: : f (if b then vT else vF) = if b then f vT else f vF SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 8 Original Proof: [by case b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 7 Results for fold 100 Results for lemma orbK: a b : (a || b) && a = a FAILURE! Tactics applied: 168 Original Proof: [by case: a; case: b.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 168 Results for fold 101 Results for lemma contraLR: (c b : bool) : (~~ c -> ~~ b) -> b -> c FAILURE! Tactics applied: 191 Original Proof: [by case: b => //; case: c.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 189 Results for fold 102 Results for lemma sub_in1: (Ph : ph {all1 P1}) : prop_in1 d1' Ph -> prop_in1 d1 Ph FAILURE! Tactics applied: 251 Original Proof: [move=> allP x /sub1; exact: allP.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 6 Number of failed tactic applications: 245 Results for fold 103 Results for lemma homoRL_in: : {in aD &, {homo f : x y / aR x y >-> rR x y}} -> {in rD & aD, forall x y, aR (g x) y -> rR x (f y)} FAILURE! Tactics applied: 10000 Original Proof: [by move=> Hf x y hx hy /Hf; rewrite fgK_on //; apply.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 413 Number of failed tactic applications: 9588 Results for fold 104 Results for lemma negbNE: b : ~~ ~~ b -> b SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 50 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 47 Results for fold 105 Results for lemma orbF: : right_id false orb SUCCESS! Proof Found in EFSM: by case. Tactics applied: 22 Original Proof: [by case.] 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: 21 Results for fold 106 Results for lemma introFn: : P -> b' = false FAILURE! Tactics applied: 170 Original Proof: [exact: introTFn false _.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 170 Results for fold 107 Results for lemma altP: : alt_spec b FAILURE! Tactics applied: 179 Original Proof: [by case def_b: b / Pb; constructor; rewrite ?def_b.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 179 Results for fold 108 Results for lemma in1W: : {all1 P1} -> {in D1, {all1 P1}} SUCCESS! Proof Found in EFSM: move => T P [] // IH; Tactics applied: 9 Original Proof: [by move=> ? ?.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 6 Results for fold 109 Results for lemma elimN: : ~~ b -> ~P SUCCESS! Proof Found in EFSM: by case Pb. Tactics applied: 55 Original Proof: [exact: elimNTF true _.] 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: 54 Results for fold 110 Results for lemma orNb: b : ~~ b || b = true SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 52 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 51 Results for fold 111 Results for lemma addbN: a b : a (+) ~~ b = ~~ (a (+) b) SUCCESS! Proof Found in EFSM: by case: a; Tactics applied: 43 Original Proof: [by case: a; case: b.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 42 Results for fold 112 Results for lemma prop_congr: : forall b b' : bool, b = b' -> b = b' :> Prop SUCCESS! Proof Found in EFSM: by do 2!case. Tactics applied: 60 Original Proof: [by move=> b b' ->.] 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: 59 Results for fold 113 Results for lemma introT: : P -> b SUCCESS! Proof Found in EFSM: by case Pb. Tactics applied: 11 Original Proof: [exact: introTF true _.] 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: 10 Results for fold 114 Results for lemma elimT: : b -> P SUCCESS! Proof Found in EFSM: by case Pb. Tactics applied: 44 Original Proof: [exact: elimTF true _.] 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 fold 115 Results for lemma negb_inj: : injective negb SUCCESS! Proof Found in EFSM: by do 2!case. Tactics applied: 91 Original Proof: [exact: can_inj negbK.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 9 Number of failed tactic applications: 82 Results for fold 116 Results for lemma monoW: : {mono f : x / aP x >-> rP x} -> {homo f : x / aP x >-> rP x} FAILURE! Tactics applied: 5220 Original Proof: [by move=> hf x ax; rewrite hf.] Proof search time: 0 min, 10 sec Number of successful tactic applications: 189 Number of failed tactic applications: 5031 Results for fold 117 Results for lemma addbP: a b : reflect (~~ a = b) (a (+) b) FAILURE! Tactics applied: 181 Original Proof: [by case: a; case: b; constructor.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 181 Results for fold 118 Results for lemma andbACA: : interchange andb andb SUCCESS! Proof Found in EFSM: by do 3!case. Tactics applied: 88 Original Proof: [by do 4!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 11 Number of failed tactic applications: 77 Results for fold 119 Results for lemma orb_id2r: (a b c : bool) : (~~ b -> a = c) -> a || b = c || b FAILURE! Tactics applied: 10000 Original Proof: [by case: a; case: b; case: c => // ->.] Proof search time: 0 min, 9 sec Number of successful tactic applications: 354 Number of failed tactic applications: 9647 Results for fold 120 Results for lemma andb_idr: (a b : bool) : (a -> b) -> a && b = a FAILURE! Tactics applied: 806 Original Proof: [by case: a; case: b => // ->.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 28 Number of failed tactic applications: 778 Results for fold 121 Results for lemma orbT: : forall b, b || true SUCCESS! Proof Found in EFSM: by case. Tactics applied: 58 Original Proof: [by case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 53 Results for fold 122 Results for lemma addKb: : left_loop id addb SUCCESS! Proof Found in EFSM: by do 2!case. Tactics applied: 93 Original Proof: [by do 2!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 88 Results for fold 123 Results for lemma rwP: : P <-> b SUCCESS! Proof Found in EFSM: by case Pb. Tactics applied: 56 Original Proof: [by split; [exact: introT | exact: elimT].] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 55 Results for fold 124 Results for lemma classic_imply: : forall P Q, (P -> classically Q) -> classically (P -> Q) FAILURE! Tactics applied: 10000 Original Proof: [move=> P Q IH [] // notPQ; apply notPQ; move/IH=> hQ; case: notF. by apply: hQ => hQ; case: notF; exact: notPQ.] Proof search time: 0 min, 12 sec Number of successful tactic applications: 1532 Number of failed tactic applications: 8469 Results for fold 125 Results for lemma andbC: : commutative andb SUCCESS! Proof Found in EFSM: by do 2!case. Tactics applied: 73 Original Proof: [by do 2!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 70 Results for fold 126 Results for lemma ifN: : ~~ b -> (if b then vT else vF) = vF SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 35 Original Proof: [by move/negbTE->.] 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: 34 Results for fold 127 Results for lemma introTF: : (if c then P else ~ P) -> b = c FAILURE! Tactics applied: 10000 Original Proof: [by case c; case Hb.] Proof search time: 0 min, 12 sec Number of successful tactic applications: 436 Number of failed tactic applications: 9565 Results for fold 128 Results for lemma sub_in12: T1 T d1 d1' d d' (P : T1 -> T -> T -> Prop) : sub_mem d1 d1' -> sub_mem d d' -> forall Ph : ph {all3 P}, prop_in12 d1' d' Ph -> prop_in12 d1 d Ph SUCCESS! Proof Found in EFSM: move => mf mg x y hx hy; auto ; Tactics applied: 179 Original Proof: [by move=> /= sub1 sub; exact: sub_in111.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 0 sec Number of successful tactic applications: 7 Number of failed tactic applications: 172 Results for fold 129 Results for lemma canLR_in: x y : {in D1, cancel f g} -> y \in D1 -> x = f y -> g x = y FAILURE! Tactics applied: 10000 Original Proof: [by move=> fK D1y ->; rewrite fK.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 322 Number of failed tactic applications: 9679 Results for fold 130 Results for lemma negbK: : involutive negb SUCCESS! Proof Found in EFSM: by case. Tactics applied: 54 Original Proof: [by case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 49 Results for fold 131 Results for lemma andFb: : left_zero false andb SUCCESS! Proof Found in EFSM: split => [eqiR | [Rxx trR] x y z *]; Tactics applied: 17 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 14 Results for fold 132 Results for lemma contraNF: (c b : bool) : (c -> b) -> ~~ b -> c = false SUCCESS! Proof Found in EFSM: case : c => // ->. case : b => // ->. split => [eqiR | [Rxx trR] x y z *]; Tactics applied: 513 Original Proof: [by move/contra=> notb_notc /notb_notc/negbTE.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 0 sec Number of successful tactic applications: 36 Number of failed tactic applications: 477 Results for fold 133 Results for lemma elimTFn: : b = c -> if c then ~ P else P FAILURE! Tactics applied: 10000 Original Proof: [by move <-; apply: (elimNTF Hb); case b.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 277 Number of failed tactic applications: 9724 Results for fold 134 Results for lemma andb_addr: : right_distributive andb addb SUCCESS! Proof Found in EFSM: by case. Tactics applied: 31 Original Proof: [by do 3!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 7 Number of failed tactic applications: 24 Results for fold 135 Results for lemma classicP: : forall P : Prop, classically P <-> ~ ~ P FAILURE! Tactics applied: 163 Original Proof: [move=> P; split=> [cP nP | nnP [] // nP]; last by case nnP; move/nP. by have: P -> false; [move/nP | move/cP].] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 163 Results for fold 136 Results for lemma implyb_id2l: (a b c : bool) : (a -> b = c) -> (a ==> b) = (a ==> c) FAILURE! Tactics applied: 10000 Original Proof: [by case: a; case: b; case: c => // ->.] Proof search time: 0 min, 12 sec Number of successful tactic applications: 1945 Number of failed tactic applications: 8056 Results for fold 137 Results for lemma andb_id2l: (a b c : bool) : (a -> b = c) -> a && b = a && c FAILURE! Tactics applied: 10000 Original Proof: [by case: a; case: b; case: c => // ->.] Proof search time: 0 min, 11 sec Number of successful tactic applications: 426 Number of failed tactic applications: 9575 Results for fold 138 Results for lemma all_and2: (hP : forall x, [/\ P1 x & P2 x]) : [/\ a P1 & a P2] FAILURE! Tactics applied: 6484 Original Proof: [by split=> x; case: (hP x).] Proof search time: 0 min, 6 sec Number of successful tactic applications: 55 Number of failed tactic applications: 6429 Results for fold 139 Results for lemma addNb: a b : ~~ a (+) b = ~~ (a (+) b) FAILURE! Tactics applied: 388 Original Proof: [by case: a; case: b.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 387 Results for fold 140 Results for lemma addbK: : right_loop id addb SUCCESS! Proof Found in EFSM: by do 2!case. Tactics applied: 63 Original Proof: [by do 2!case.] 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: 62 Results for fold 141 Results for lemma mono2W_in: : {in aD, {mono f : x / aP x >-> rP x}} -> {in aD, {homo f : x / aP x >-> rP x}} FAILURE! Tactics applied: 10000 Original Proof: [by move=> hf x hx ax; rewrite hf.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 335 Number of failed tactic applications: 9666 Results for fold 142 Results for lemma orbN: b : b || ~~ b = true SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 8 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 7 Results for fold 143 Results for lemma and4P: : reflect [/\ b1, b2, b3 & b4] [&& b1, b2, b3 & b4] FAILURE! Tactics applied: 10000 Original Proof: [by case b1; case b2; case b3; case b4; constructor; try by case.] Proof search time: 0 min, 10 sec Number of successful tactic applications: 450 Number of failed tactic applications: 9551 Results for fold 144 Results for lemma classic_pick: : forall T P, classically ({x : T | P x} + (forall x, ~ P x)) FAILURE! Tactics applied: 359 Original Proof: [move=> T P [] // IH; apply IH; right=> x Px; case: notF. by apply: IH; left; exists x.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 7 Number of failed tactic applications: 352 Results for fold 145 Results for lemma elimTn: : b' -> ~ P FAILURE! Tactics applied: 181 Original Proof: [exact: elimTFn true _.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 181 Results for fold 146 Results for lemma monoRL: : {mono f : x y / aR x y >-> rR x y} -> forall x y, rR x (f y) = aR (g x) y FAILURE! Tactics applied: 428 Original Proof: [by move=> mf x y; rewrite -{1}[x]fgK mf.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 9 Number of failed tactic applications: 419 Results for fold 147 Results for lemma elimNf: : ~~ b = false -> P SUCCESS! Proof Found in EFSM: by case Pb. Tactics applied: 69 Original Proof: [exact: elimNTF false _.] 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: 68 Results for fold 148 Results for lemma orP: : reflect (b1 \/ b2) (b1 || b2) FAILURE! Tactics applied: 10000 Original Proof: [by case b1; case b2; constructor; auto; case.] Proof search time: 0 min, 13 sec Number of successful tactic applications: 765 Number of failed tactic applications: 9236 Results for fold 149 Results for lemma subrelUl: r1 r2 : subrel r1 (relU r1 r2) SUCCESS! Proof Found in EFSM: move => symR x y; apply /orP; auto. Tactics applied: 738 Original Proof: [by move=> *; apply/orP; left.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 0 sec Number of successful tactic applications: 23 Number of failed tactic applications: 715 Results for fold 150 Results for lemma negP: : reflect (~ b1) (~~ b1) SUCCESS! Proof Found in EFSM: case b1; constructor => //; Tactics applied: 188 Original Proof: [by case b1; constructor; auto.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 183 Results for fold 151 Results for lemma subon2: (Phf : ph (allQ2 f)) (Ph : ph (allQ2 f)) : prop_on2 d2' Phf Ph -> prop_on2 d2 Phf Ph SUCCESS! Proof Found in EFSM: move => P Q IH [] // notPQ; auto ; Tactics applied: 260 Original Proof: [by move=> allQ x y /sub2=> d2fx /sub2; exact: allQ.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 0 sec Number of successful tactic applications: 14 Number of failed tactic applications: 246 Results for fold 152 Results for lemma contraL: (c b : bool) : (c -> ~~ b) -> b -> ~~ c FAILURE! Tactics applied: 188 Original Proof: [by case: b => //; case: c.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 186 Results for fold 153 Results for lemma and5P: : reflect [/\ b1, b2, b3, b4 & b5] [&& b1, b2, b3, b4 & b5] FAILURE! Tactics applied: 173 Original Proof: [by case b1; case b2; case b3; case b4; case b5; constructor; try by case.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 171 Results for fold 154 Results for lemma addbAC: : right_commutative addb SUCCESS! Proof Found in EFSM: by do 3!case. Tactics applied: 38 Original Proof: [by do 3!case.] 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: 37 Results for fold 155 Results for lemma in_simpl: x p (msp : manifest_simpl_pred p) : in_mem x (Mem [eta fun_of_simpl (msp : simpl_pred T)]) = p x SUCCESS! Proof Found in EFSM: by case: msp => _ /= ->. Tactics applied: 34 Original Proof: [by case: msp => _ /= ->.] 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: 33 Results for fold 156 Results for lemma nandP: : reflect (~~ b1 \/ ~~ b2) (~~ (b1 && b2)) FAILURE! Tactics applied: 10000 Original Proof: [by case b1; case b2; constructor; auto; case; auto.] Proof search time: 0 min, 11 sec Number of successful tactic applications: 453 Number of failed tactic applications: 9548 Results for fold 157 Results for lemma andbN: b : b && ~~ b = false SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 58 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 57 Results for fold 158 Results for lemma on1T: : {on T2, allQ1 f} -> allQ1 f FAILURE! Tactics applied: 328 Original Proof: [by move=> ? ?; auto.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 6 Number of failed tactic applications: 322 Results for fold 159 Results for lemma negbTE: b : ~~ b -> b = false SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 8 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 7 Results for fold 160 Results for lemma negPn: : reflect b1 (~~ ~~ b1) SUCCESS! Proof Found in EFSM: case b1; first by constructor. by constructor; Tactics applied: 1218 Original Proof: [by case b1; constructor.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 sec Number of successful tactic applications: 121 Number of failed tactic applications: 1097 Results for fold 161 Results for lemma in3T: : {in T1 & T2 & T3, {all3 P3}} -> {all3 P3} SUCCESS! Proof Found in EFSM: move => P; auto. Tactics applied: 231 Original Proof: [by move=> ? ?; auto.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 0 sec Number of successful tactic applications: 8 Number of failed tactic applications: 223 Results for fold 162 Results for lemma forE: x P phP : @prop_for x P phP = P x SUCCESS! Proof Found in EFSM: by []. Tactics applied: 1 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: 0 Results for fold 163 Results for lemma sumboolP: (decQ : decidable Q) : reflect Q decQ FAILURE! Tactics applied: 10000 Original Proof: [by case: decQ; constructor.] Proof search time: 0 min, 10 sec Number of successful tactic applications: 461 Number of failed tactic applications: 9540 Results for fold 164 Results for lemma subrelUr: r1 r2 : subrel r2 (relU r1 r2) SUCCESS! Proof Found in EFSM: move => symR x y; apply /orP; constructor 2. auto ; Tactics applied: 2729 Original Proof: [by move=> *; apply/orP; right.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 3 sec Number of successful tactic applications: 68 Number of failed tactic applications: 2661 Results for fold 165 Results for lemma orbCA: : left_commutative orb SUCCESS! Proof Found in EFSM: by do 2!case. Tactics applied: 71 Original Proof: [by do 3!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 66 Results for fold 166 Results for lemma addbACA: : interchange addb addb SUCCESS! Proof Found in EFSM: by do 4!case. Tactics applied: 70 Original Proof: [by do 4!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 12 Number of failed tactic applications: 58 Results for fold 167 Results for lemma onT_bij: : {on T2, bijective f} -> bijective f FAILURE! Tactics applied: 6076 Original Proof: [by case=> g' fK g'K; exists g' => * ? *; auto.] Proof search time: 0 min, 10 sec Number of successful tactic applications: 85 Number of failed tactic applications: 5991 Results for fold 168 Results for lemma sub_in21: T T3 d d' d3 d3' (P : T -> T -> T3 -> Prop) : sub_mem d d' -> sub_mem d3 d3' -> forall Ph : ph {all3 P}, prop_in21 d' d3' Ph -> prop_in21 d d3 Ph SUCCESS! Proof Found in EFSM: move => mf mg x y hx hy; auto. Tactics applied: 201 Original Proof: [by move=> /= sub sub3; exact: sub_in111.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 0 sec Number of successful tactic applications: 8 Number of failed tactic applications: 193 Results for fold 169 Results for lemma xorPif: : Q \/ P -> ~ (Q /\ P) -> if b then ~ Q else Q FAILURE! Tactics applied: 172 Original Proof: [by case Hb => [? _ H ? | ? H _]; case: H.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 4 Number of failed tactic applications: 168 Results for fold 170 Results for lemma equivPifn: : (Q -> P) -> (P -> Q) -> if b then ~ Q else Q FAILURE! Tactics applied: 225 Original Proof: [rewrite -if_neg; exact: equivPif.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 4 Number of failed tactic applications: 221 Results for fold 171 Results for lemma on1lW: : allQ1l f h -> {on D2, allQ1l f & h} SUCCESS! Proof Found in EFSM: move => T P [] // IH; Tactics applied: 25 Original Proof: [by move=> ? ?.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 22 Results for fold 172 Results for lemma implyTb: b : (true ==> b) = b SUCCESS! Proof Found in EFSM: split => [eqiR | [Rxx trR] x y z *]; Tactics applied: 17 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: 16 Results for fold 173 Results for lemma topredE: x (pp : pT) : topred pp x = (x \in pp) SUCCESS! Proof Found in EFSM: by rewrite -mem_topred. Tactics applied: 186 Original Proof: [by rewrite -mem_topred.] 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: 185 Results for fold 174 Results for lemma is_true_true: : true SUCCESS! Proof Found in EFSM: split => [eqiR | [Rxx trR] x y z *]; Tactics applied: 17 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: 16 Results for fold 175 Results for lemma mono2W: : {mono f : x y / aR x y >-> rR x y} -> {homo f : x y / aR x y >-> rR x y} FAILURE! Tactics applied: 1696 Original Proof: [by move=> hf x y axy; rewrite hf.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 20 Number of failed tactic applications: 1676 Results for fold 176 Results for lemma if_arg: (fT fF : A -> B) : (if b then fT else fF) x = if b then fT x else fF x SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 68 Original Proof: [by case b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 67 Results for fold 177 Results for lemma ifPn: : if_spec (~~ b) b (if b then vT else vF) FAILURE! Tactics applied: 184 Original Proof: [by case def_b: b; constructor; rewrite ?def_b.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 184 Results for fold 178 Results for lemma sym_left_transitive: : left_transitive FAILURE! Tactics applied: 10000 Original Proof: [by move=> x y Rxy z; apply/idP/idP; apply: trR; rewrite // symR.] Proof search time: 0 min, 15 sec Number of successful tactic applications: 270 Number of failed tactic applications: 9731 Results for fold 179 Results for lemma idP: : reflect b1 b1 SUCCESS! Proof Found in EFSM: case b1; case b4; by constructor; Tactics applied: 308 Original Proof: [by case b1; constructor.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 0 sec Number of successful tactic applications: 33 Number of failed tactic applications: 275 Results for fold 180 Results for lemma canLR_on: x y : {on D2, cancel f & g} -> f y \in D2 -> x = f y -> g x = y FAILURE! Tactics applied: 210 Original Proof: [by move=> fK D2fy ->; rewrite fK.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 4 Number of failed tactic applications: 206 Results for fold 181 Results for lemma unless_contra: b C : (~~ b -> C) -> unless C b FAILURE! Tactics applied: 300 Original Proof: [by case: b => [_ haveC | haveC _]; exact: haveC.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 4 Number of failed tactic applications: 296 Results for fold 182 Results for lemma addbb: : self_inverse false addb SUCCESS! Proof Found in EFSM: by case. Tactics applied: 45 Original Proof: [by case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 40 Results for fold 183 Results for lemma orbA: : associative orb SUCCESS! Proof Found in EFSM: by case. Tactics applied: 56 Original Proof: [by do 3!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 7 Number of failed tactic applications: 49 Results for fold 184 Results for lemma sameP: : reflect P c -> b = c SUCCESS! Proof Found in EFSM: case. move /introT; case : b => // ->. by case Pb. Tactics applied: 4907 Original Proof: [case; [exact: introT | exact: introF].] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 6 sec Number of successful tactic applications: 298 Number of failed tactic applications: 4609 Results for fold 185 Results for lemma homoRL: : {homo f : x y / aR x y >-> rR x y} -> forall x y, aR (g x) y -> rR x (f y) FAILURE! Tactics applied: 279 Original Proof: [by move=> Hf x y /Hf; rewrite fgK.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 12 Number of failed tactic applications: 267 Results for fold 186 Results for lemma elimFn: : b' = false -> P FAILURE! Tactics applied: 203 Original Proof: [exact: elimTFn false _.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 203 Results for fold 187 Results for lemma implybNN: a b : (~~ a ==> ~~ b) = b ==> a FAILURE! Tactics applied: 202 Original Proof: [by case: a; case: b.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 202 Results for fold 188 Results for lemma norP: : reflect (~~ b1 /\ ~~ b2) (~~ (b1 || b2)) FAILURE! Tactics applied: 177 Original Proof: [by case b1; case b2; constructor; auto; case; auto.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 175 Results for fold 189 Results for lemma contraFT: (c b : bool) : (~~ c -> b) -> b = false -> c FAILURE! Tactics applied: 10000 Original Proof: [by move/contraR=> notb_c /negbT.] Proof search time: 0 min, 11 sec Number of successful tactic applications: 516 Number of failed tactic applications: 9485 Results for fold 190 Results for lemma introNTF: : (if c then ~ P else P) -> ~~ b = c FAILURE! Tactics applied: 10000 Original Proof: [by case c; case Hb.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 96 Number of failed tactic applications: 9905 Results for fold 191 Results for lemma introTn: : ~ P -> b' FAILURE! Tactics applied: 184 Original Proof: [exact: introTFn true _.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 182 Results for fold 192 Results for lemma if_neg: : (if ~~ b then vT else vF) = if b then vF else vT SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 8 Original Proof: [by case b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 7 Results for fold 193 Results for lemma qualifE: n T p x : (x \in @Qualifier n T p) = p x SUCCESS! Proof Found in EFSM: split => [eqiR | [Rxx trR] x y z *]; Tactics applied: 5 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: 4 Results for fold 194 Results for lemma addbA: : associative addb SUCCESS! Proof Found in EFSM: by do 3!case. Tactics applied: 65 Original Proof: [by do 3!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 62 Results for fold 195 Results for lemma or4P: : reflect [\/ b1, b2, b3 | b4] [|| b1, b2, b3 | b4] FAILURE! Tactics applied: 10000 Original Proof: [case b1; first by constructor; constructor 1. case b2; first by constructor; constructor 2. case b3; first by constructor; constructor 3. case b4; first by constructor; constructor 4. by constructor; case.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 1255 Number of failed tactic applications: 8746 Results for fold 196 Results for lemma orb_id2l: (a b c : bool) : (~~ a -> b = c) -> a || b = a || c FAILURE! Tactics applied: 212 Original Proof: [by case: a; case: b; case: c => // ->.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 6 Number of failed tactic applications: 206 Results for fold 197 Results for lemma canRL_on: x y : {on D2, cancel f & g} -> f x \in D2 -> f x = y -> x = g y FAILURE! Tactics applied: 10000 Original Proof: [by move=> fK D2fx <-; rewrite fK.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 222 Number of failed tactic applications: 9779 Results for fold 198 Results for lemma negb_or: (a b : bool) : ~~ (a || b) = ~~ a && ~~ b SUCCESS! Proof Found in EFSM: by case: a; Tactics applied: 65 Original Proof: [by case: a; case: b.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 64 Results for fold 199 Results for lemma pair_andP: P Q : P /\ Q <-> P * Q FAILURE! Tactics applied: 166 Original Proof: [by split; case.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 166 Results for fold 200 Results for lemma on1lT: : {on T2, allQ1l f & h} -> allQ1l f h FAILURE! Tactics applied: 563 Original Proof: [by move=> ? ?; auto.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 558 Results for fold 201 Results for lemma inT_bij: : {in T1, bijective f} -> bijective f FAILURE! Tactics applied: 525 Original Proof: [by case=> g' fK g'K; exists g' => * ? *; auto.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 13 Number of failed tactic applications: 512 Results for fold 202 Results for lemma appP: : reflect Q b -> P -> Q FAILURE! Tactics applied: 10000 Original Proof: [by move=> Qb; move/introT; case: Qb.] Proof search time: 0 min, 13 sec Number of successful tactic applications: 545 Number of failed tactic applications: 9456 Results for fold 203 Results for lemma andb_addl: : left_distributive andb addb SUCCESS! Proof Found in EFSM: by do 3!case. Tactics applied: 90 Original Proof: [by do 3!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 85 Results for fold 204 Results for lemma monoRL_in: : {in aD &, {mono f : x y / aR x y >-> rR x y}} -> {in rD & aD, forall x y, rR x (f y) = aR (g x) y} FAILURE! Tactics applied: 10000 Original Proof: [by move=> mf x y hx hy; rewrite -{1}[x]fgK_on // mf.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 164 Number of failed tactic applications: 9837 Results for fold 205 Results for lemma contraT: b : (~~ b -> false) -> b SUCCESS! Proof Found in EFSM: by case: b => // ->. Tactics applied: 78 Original Proof: [by case: b => // ->.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 75 Results for fold 206 Results for lemma addbT: b : b (+) true = ~~ b SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 63 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 62 Results for fold 207 Results for lemma in3W: : {all3 P3} -> {in D1 & D2 & D3, {all3 P3}} SUCCESS! Proof Found in EFSM: by move=> *; Tactics applied: 108 Original Proof: [by move=> ? ?.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 9 Number of failed tactic applications: 99 Results for fold 208 Results for lemma addbF: : right_id false addb SUCCESS! Proof Found in EFSM: by case. Tactics applied: 57 Original Proof: [by case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 54 Results for fold 209 Results for lemma orb_idr: (a b : bool) : (b -> a) -> a || b = a FAILURE! Tactics applied: 4584 Original Proof: [by case: a; case: b => // ->.] Proof search time: 0 min, 4 sec Number of successful tactic applications: 52 Number of failed tactic applications: 4532 Results for fold 210 Results for lemma orFb: : left_id false orb SUCCESS! Proof Found in EFSM: try by case. Tactics applied: 40 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 35 Results for fold 211 Results for lemma implybT: b : b ==> true SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 67 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 65 Results for fold 212 Results for lemma mem_mem: (pp : pT) : (mem (mem pp) = mem pp) * (mem [mem pp] = mem pp) SUCCESS! Proof Found in EFSM: by rewrite -mem_topred. Tactics applied: 165 Original Proof: [by rewrite -mem_topred.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 160 Results for fold 213 Results for lemma implyb_idr: (a b : bool) : (b -> ~~ a) -> (a ==> b) = ~~ a FAILURE! Tactics applied: 4470 Original Proof: [by case: a; case: b => // ->.] Proof search time: 0 min, 3 sec Number of successful tactic applications: 40 Number of failed tactic applications: 4430 Results for fold 214 Results for lemma mem_topred: (pp : pT) : mem (topred pp) = mem pp FAILURE! Tactics applied: 392 Original Proof: [by rewrite /mem; case: pT pp => T1 app1 [mem1 /= ->].] Proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 391 Results for fold 215 Results for lemma unfold_in: x p : (x \in ([eta p] : pred T)) = p x SUCCESS! Proof Found in EFSM: split => [eqiR | [Rxx trR] x y z *]; Tactics applied: 1 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: 0 Results for fold 216 Results for lemma homoLR: : {homo f : x y / aR x y >-> rR x y} -> forall x y, aR x (g y) -> rR (f x) y SUCCESS! Proof Found in EFSM: move => mf mg x y; rewrite -{1}[x]fgK mf. split => ?. auto. Tactics applied: 3261 Original Proof: [by move=> Hf x y /Hf; rewrite fgK.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 5 sec Number of successful tactic applications: 230 Number of failed tactic applications: 3031 Results for fold 217 Results for lemma contra: (c b : bool) : (c -> b) -> ~~ b -> ~~ c FAILURE! Tactics applied: 202 Original Proof: [by case: b => //; case: c.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 200 Results for fold 218 Results for lemma xorPifn: : Q \/ P -> ~ (Q /\ P) -> if b then Q else ~ Q FAILURE! Tactics applied: 810 Original Proof: [rewrite -if_neg; exact: xorPif.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 12 Number of failed tactic applications: 798 Results for fold 219 Results for lemma sub_in111: (Ph : ph {all3 P3}) : prop_in111 d1' d2' d3' Ph -> prop_in111 d1 d2 d3 Ph FAILURE! Tactics applied: 272 Original Proof: [by move=> allP x1 x2 x3 /sub1 d1x1 /sub2 d2x2 /sub3; exact: allP.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 8 Number of failed tactic applications: 264 Results for fold 220 Results for lemma negbLR: b c : b = ~~ c -> ~~ b = c FAILURE! Tactics applied: 194 Original Proof: [exact: canLR negbK.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 192 Results for fold 221 Results for lemma orbC: : commutative orb SUCCESS! Proof Found in EFSM: by do 2!case. Tactics applied: 82 Original Proof: [by do 2!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 77 Results for fold 222 Results for lemma andTb: : left_id true andb SUCCESS! Proof Found in EFSM: split => [eqiR | [Rxx trR] x y z *]; Tactics applied: 37 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 32 Results for fold 223 Results for lemma orKb: a b : a && (b || a) = a FAILURE! Tactics applied: 167 Original Proof: [by case: a; case: b.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 167 Results for fold 224 Results for lemma can_mono: : {mono f : x y / aR x y >-> rR x y} -> {mono g : x y / rR x y >-> aR x y} FAILURE! Tactics applied: 243 Original Proof: [by move=> mf x y /=; rewrite -mf !fgK.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 8 Number of failed tactic applications: 235 Results for fold 225 Results for lemma rev_trans: T (R : rel T) : transitive R -> transitive (fun x y => R y x) FAILURE! Tactics applied: 1633 Original Proof: [by move=> trR x y z Ryx Rzy; exact: trR Rzy Ryx.] Proof search time: 0 min, 2 sec Number of successful tactic applications: 41 Number of failed tactic applications: 1592 Results for fold 226 Results for lemma simpl_predE: p : SimplPred p =1 p SUCCESS! Proof Found in EFSM: by []. Tactics applied: 1 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: 0 Results for fold 227 Results for lemma boolP: : alt_spec b1 b1 b1 SUCCESS! Proof Found in EFSM: case b1; first by constructor; constructor 1. constructor => //; Tactics applied: 198 Original Proof: [exact: (altP idP).] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 0 sec Number of successful tactic applications: 9 Number of failed tactic applications: 189 Results for fold 228 Results for lemma addIb: : left_injective addb SUCCESS! Proof Found in EFSM: by do 3!case. Tactics applied: 81 Original Proof: [by do 3!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 13 Number of failed tactic applications: 68 Results for fold 229 Results for lemma homoLR_in: : {in aD &, {homo f : x y / aR x y >-> rR x y}} -> {in aD & rD, forall x y, aR x (g y) -> rR (f x) y} FAILURE! Tactics applied: 290 Original Proof: [by move=> Hf x y hx hy /Hf; rewrite fgK_on //; apply.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 12 Number of failed tactic applications: 278 Results for fold 230 Results for lemma equivP: : (P <-> Q) -> reflect Q b FAILURE! Tactics applied: 174 Original Proof: [by case; exact: iffP.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 172 Results for fold 231 Results for lemma addTb: b : true (+) b = ~~ b SUCCESS! Proof Found in EFSM: by []. Tactics applied: 1 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: 0 Results for fold 232 Results for lemma addFb: : left_id false addb SUCCESS! Proof Found in EFSM: by []. Tactics applied: 1 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: 0 Results for fold 233 Results for lemma sub_in3: T d d' (P : T -> T -> T -> Prop) : sub_mem d d' -> forall Ph : ph {all3 P}, prop_in3 d' Ph -> prop_in3 d Ph FAILURE! Tactics applied: 234 Original Proof: [by move=> /= sub_dd'; exact: sub_in111.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 6 Number of failed tactic applications: 228 Results for fold 234 Results for lemma implybb: b : b ==> b SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 50 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 49 Results for fold 235 Results for lemma homo_mono: : {homo f : x y / aR x y >-> rR x y} -> {homo g : x y / rR x y >-> aR x y} -> {mono g : x y / rR x y >-> aR x y} FAILURE! Tactics applied: 10000 Original Proof: [move=> mf mg x y; case: (boolP (rR _ _))=> [/mg //|]. by apply: contraNF=> /mf; rewrite !fgK.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 193 Number of failed tactic applications: 9808 Results for fold 236 Results for lemma or3P: : reflect [\/ b1, b2 | b3] [|| b1, b2 | b3] FAILURE! Tactics applied: 183 Original Proof: [case b1; first by constructor; constructor 1. case b2; first by constructor; constructor 2. case b3; first by constructor; constructor 3. by constructor; case.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 181 Results for fold 237 Results for lemma subon1l: (Phf : ph (allQ1l f)) (Ph : ph (allQ1l f h)) : prop_on1 d2' Phf Ph -> prop_on1 d2 Phf Ph SUCCESS! Proof Found in EFSM: move => T P [] // IH; auto. Tactics applied: 372 Original Proof: [by move=> allQ x /sub2; exact: allQ.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 0 sec Number of successful tactic applications: 10 Number of failed tactic applications: 362 Results for fold 238 Results for lemma andbAC: : right_commutative andb SUCCESS! Proof Found in EFSM: by do 3!case. Tactics applied: 46 Original Proof: [by do 3!case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 43 Results for fold 239 Results for lemma equivalence_relP_in: T (R : rel T) (A : pred T) : {in A & &, equivalence_rel R} <-> {in A, reflexive R} /\ {in A &, forall x y, R x y -> {in A, R x =1 R y}} FAILURE! Tactics applied: 169 Original Proof: [split=> [eqiR | [Rxx trR] x y z *]; last by split=> [|/trR-> //]; exact: Rxx. by split=> [x Ax|x y Ax Ay Rxy z Az]; [rewrite (eqiR x x) | rewrite (eqiR x y)].] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 167 Results for fold 240 Results for lemma classic_bind: : forall P Q, (P -> classically Q) -> (classically P -> classically Q) FAILURE! Tactics applied: 10000 Original Proof: [by move=> P Q IH IH_P b IH_Q; apply: IH_P; move/IH; exact.] Proof search time: 0 min, 12 sec Number of successful tactic applications: 1002 Number of failed tactic applications: 8999 OVERALL RESULTS SUMMARY EFSMProver proved 123 out of 240 lemmas. Success rate of 51.24999999999999% There were 0 errors. 117 proof attempts exhausted the automaton On average, a proof was found after applying 183 tactics The longest proof consisted of 4 tactics There were 10 shorter proofs found Of the 117 failures, 44 of them used all 10000 tactics There were 105 reused proofs found There were 18 novel proofs found Of the 117 failures, the average number of tactics used was 4331 On average, a proof was found after 0 min, 0 sec On average, a failed proof attempt took 0 min, 6 sec On average, any (success or failure) proof attempt took 0 min, 3 sec The longest time to find a proof was 0 min, 6 sec The shortest time to find a proof was 0 min, 0 sec There were 1 proofs containing repeated tactics There were 4 proofs that repeated states