Results for fold 1 Results for lemma decPcases: : if b then P else ~ P SUCCESS! Proof Found in EFSM: by case: Pb; Tactics applied: 46 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: 43 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, 30 sec Number of successful tactic applications: 3374 Number of failed tactic applications: 6627 Results for lemma andb_idr: (a b : bool) : (a -> b) -> a && b = a FAILURE! Tactics applied: 245 Original Proof: [by case: a; case: b => // ->.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 240 Results for lemma app_predE: x p (ap : manifest_applicative_pred p) : ap x = (x \in p) FAILURE! Tactics applied: 109 Original Proof: [by case: ap => _ /= ->.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 109 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, 16 sec Number of successful tactic applications: 4245 Number of failed tactic applications: 5756 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: 154 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: 5 Number of failed tactic applications: 149 Results for lemma introTn: : ~ P -> b' FAILURE! Tactics applied: 147 Original Proof: [exact: introTFn true _.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 144 Results for lemma orbN: b : b || ~~ b = true SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 38 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: 37 Results for lemma orbF: : right_id false orb SUCCESS! Proof Found in EFSM: by case. Tactics applied: 33 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: 30 Results for lemma sub_refl: T (p : mem_pred T) : sub_mem p p SUCCESS! Proof Found in EFSM: by []. Tactics applied: 32 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: 29 Results for lemma if_same: : (if b then vT else vT) = vT SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 38 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: 37 Results for lemma in3W: : {all3 P3} -> {in D1 & D2 & D3, {all3 P3}} SUCCESS! Proof Found in EFSM: by move=> /= sub_dd'; Tactics applied: 70 Original Proof: [by move=> ? ?.] 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: 63 Results for lemma orb_andl: : left_distributive orb andb SUCCESS! Proof Found in EFSM: by do 3!case. Tactics applied: 59 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: 56 Results for lemma implybb: b : b ==> b SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 38 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: 37 Results for lemma in_applicative: x p (amp : applicative_mem_pred p) : in_mem x amp = p x FAILURE! Tactics applied: 109 Original Proof: [by case: amp => [[_ /= ->]].] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 109 Results for lemma orNb: b : ~~ b || b = true SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 38 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: 37 Results for lemma introNf: : P -> ~~ b = false SUCCESS! Proof Found in EFSM: by case: Pb; Tactics applied: 46 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: 45 Results for lemma andbT: : right_id true andb SUCCESS! Proof Found in EFSM: by case. Tactics applied: 33 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: 30 Results for lemma contra: (c b : bool) : (c -> b) -> ~~ b -> ~~ c FAILURE! Tactics applied: 264 Original Proof: [by case: b => //; case: c.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 6 Number of failed tactic applications: 258 Results for lemma subrelUr: r1 r2 : subrel r2 (relU r1 r2) FAILURE! Tactics applied: 207 Original Proof: [by move=> *; apply/orP; right.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 204 Results for lemma addbT: b : b (+) true = ~~ b SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 38 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: 37 Results for lemma simpl_predE: p : SimplPred p =1 p SUCCESS! Proof Found in EFSM: split => [eqiR | [Rxx trR] x y z]; Tactics applied: 30 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: 27 Results for lemma andb_id2l: (a b c : bool) : (a -> b = c) -> a && b = a && c FAILURE! Tactics applied: 245 Original Proof: [by case: a; case: b; case: c => // ->.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 240 Results for lemma sym_right_transitive: : right_transitive FAILURE! Tactics applied: 305 Original Proof: [by move=> x y /sym_left_transitive Rxy z; rewrite !(symR z) Rxy.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 6 Number of failed tactic applications: 299 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: 38 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: 37 Results for lemma andbN: b : b && ~~ b = false SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 38 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: 37 Results for lemma negbNE: b : ~~ ~~ b -> b SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 38 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: 35 Results for lemma addKb: : left_loop id addb SUCCESS! Proof Found in EFSM: by do 2!case. Tactics applied: 58 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: 55 Results for lemma orFb: : left_id false orb SUCCESS! Proof Found in EFSM: split => [eqiR | [Rxx trR] x y z]; Tactics applied: 30 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: 27 Results for lemma orb_andr: : right_distributive orb andb SUCCESS! Proof Found in EFSM: by case. Tactics applied: 33 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: 30 Results for lemma unless_contra: b C : (~~ b -> C) -> unless C b FAILURE! Tactics applied: 10000 Original Proof: [by case: b => [_ haveC | haveC _]; exact: haveC.] Proof search time: 0 min, 13 sec Number of successful tactic applications: 4121 Number of failed tactic applications: 5880 Results for lemma addbAC: : right_commutative addb SUCCESS! Proof Found in EFSM: by do 3!case. Tactics applied: 59 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: 56 Results for lemma canLR_in: x y : {in D1, cancel f g} -> y \in D1 -> x = f y -> g x = y FAILURE! Tactics applied: 760 Original Proof: [by move=> fK D1y ->; rewrite fK.] Proof search time: 0 min, 2 sec Number of successful tactic applications: 11 Number of failed tactic applications: 749 Results for lemma subon1: (Phf : ph (allQ1 f)) (Ph : ph (allQ1 f)) : prop_on1 d2' Phf Ph -> prop_on1 d2 Phf Ph SUCCESS! Proof Found in EFSM: move => T P [] // IH; auto. Tactics applied: 252 Original Proof: [by move=> allQ x /sub2; exact: allQ.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 sec Number of successful tactic applications: 6 Number of failed tactic applications: 246 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: 58 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: 5 Number of failed tactic applications: 53 Results for lemma bind_unless: C P {Q} : unless C P -> unless (unless C Q) P FAILURE! Tactics applied: 109 Original Proof: [by move=> haveP suffPQ suffQ; apply: haveP => /suffPQ; exact.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 109 Results for lemma on1lW: : allQ1l f h -> {on D2, allQ1l f & h} SUCCESS! Proof Found in EFSM: move => T P [] // IH; Tactics applied: 14 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: 11 Results for lemma orb_id2l: (a b c : bool) : (~~ a -> b = c) -> a || b = a || c FAILURE! Tactics applied: 245 Original Proof: [by case: a; case: b; case: c => // ->.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 240 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: 30 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: 29 Results for lemma introNTF: : (if c then ~ P else P) -> ~~ b = c FAILURE! Tactics applied: 7313 Original Proof: [by case c; case Hb.] Proof search time: 0 min, 12 sec Number of successful tactic applications: 68 Number of failed tactic applications: 7245 Results for lemma ifPn: : if_spec (~~ b) b (if b then vT else vF) FAILURE! Tactics applied: 109 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: 109 Results for lemma classic_imply: : forall P Q, (P -> classically Q) -> classically (P -> Q) FAILURE! Tactics applied: 1231 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, 2 sec Number of successful tactic applications: 28 Number of failed tactic applications: 1203 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, 18 sec Number of successful tactic applications: 4293 Number of failed tactic applications: 5708 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 FAILURE! Tactics applied: 305 Original Proof: [by move=> Hf x y /Hf; rewrite fgK.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 6 Number of failed tactic applications: 299 Results for lemma subrelUl: r1 r2 : subrel r1 (relU r1 r2) FAILURE! Tactics applied: 207 Original Proof: [by move=> *; apply/orP; left.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 204 Results for lemma ifN: : ~~ b -> (if b then vT else vF) = vF SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 38 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: 3 Number of failed tactic applications: 35 Results for lemma monoW: : {mono f : x / aP x >-> rP x} -> {homo f : x / aP x >-> rP x} FAILURE! Tactics applied: 305 Original Proof: [by move=> hf x ax; rewrite hf.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 6 Number of failed tactic applications: 299 Results for lemma orb_idr: (a b : bool) : (b -> a) -> a || b = a FAILURE! Tactics applied: 245 Original Proof: [by case: a; case: b => // ->.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 240 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: 305 Original Proof: [by move=> hf x y axy; rewrite hf.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 6 Number of failed tactic applications: 299 Results for lemma contraNF: (c b : bool) : (c -> b) -> ~~ b -> c = false FAILURE! Tactics applied: 264 Original Proof: [by move/contra=> notb_notc /notb_notc/negbTE.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 6 Number of failed tactic applications: 258 Results for lemma elimTF: : b = c -> if c then P else ~ P FAILURE! Tactics applied: 9320 Original Proof: [by move <-; case Hb.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 204 Number of failed tactic applications: 9116 Results for lemma ifT: : b -> (if b then vT else vF) = vT SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 38 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: 35 Results for lemma andbK: a b : a && b || a = a FAILURE! Tactics applied: 109 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: 109 Results for lemma not_false_is_true: : ~ false SUCCESS! Proof Found in EFSM: by []. Tactics applied: 32 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: 29 Results for lemma andb_addl: : left_distributive andb addb SUCCESS! Proof Found in EFSM: by do 3!case. Tactics applied: 59 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: 56 Results for lemma andFb: : left_zero false andb SUCCESS! Proof Found in EFSM: split => [eqiR | [Rxx trR] x y z]; Tactics applied: 30 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: 27 Results for lemma is_true_locked_true: : locked true FAILURE! Tactics applied: 109 Original Proof: [by unlock.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 109 Results for lemma andbA: : associative andb SUCCESS! Proof Found in EFSM: by case. Tactics applied: 33 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: 30 Results for lemma implybT: b : b ==> true SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 38 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: 37 Results for lemma symmetric_from_pre: : pre_symmetric -> symmetric FAILURE! Tactics applied: 207 Original Proof: [move=> symR x y; apply/idP/idP; exact: symR.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 204 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: 30 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: 29 Results for lemma andTb: : left_id true andb SUCCESS! Proof Found in EFSM: split => [eqiR | [Rxx trR] x y z]; Tactics applied: 30 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: 27 Results for lemma andbCA: : left_commutative andb SUCCESS! Proof Found in EFSM: by do 2!case. Tactics applied: 58 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: 55 Results for lemma addIb: : left_injective addb SUCCESS! Proof Found in EFSM: by do 3!case. Tactics applied: 59 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: 52 Results for lemma contraT: b : (~~ b -> false) -> b SUCCESS! Proof Found in EFSM: by case: b => // ->. Tactics applied: 51 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: 48 Results for lemma in1T: : {in T1, {all1 P1}} -> {all1 P1} SUCCESS! Proof Found in EFSM: move => P; auto. Tactics applied: 154 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: 3 Number of failed tactic applications: 151 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: 207 Original Proof: [by move=> mf x y; rewrite -{1}[x]fgK mf.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 204 Results for lemma contraFT: (c b : bool) : (~~ c -> b) -> b = false -> c FAILURE! Tactics applied: 264 Original Proof: [by move/contraR=> notb_c /negbT.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 6 Number of failed tactic applications: 258 Results for lemma contraL: (c b : bool) : (c -> ~~ b) -> b -> ~~ c FAILURE! Tactics applied: 264 Original Proof: [by case: b => //; case: c.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 6 Number of failed tactic applications: 258 Results for lemma on2T: : {on T2 &, allQ2 f} -> allQ2 f FAILURE! Tactics applied: 207 Original Proof: [by move=> ? ?; auto.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 204 Results for lemma subon_bij: (D2' : pred T2) : {subset D2 <= D2'} -> {on D2', bijective f} -> {on D2, bijective f} FAILURE! Tactics applied: 681 Original Proof: [by move=> subD [g' fK g'K]; exists g' => x; move/subD; [exact: fK | exact: g'K].] Proof search time: 0 min, 1 sec Number of successful tactic applications: 9 Number of failed tactic applications: 672 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: 109 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: 109 Results for lemma rwP: : P <-> b SUCCESS! Proof Found in EFSM: by case: Pb; Tactics applied: 46 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: 45 Results for lemma contraFN: (c b : bool) : (c -> b) -> b = false -> ~~ c FAILURE! Tactics applied: 264 Original Proof: [by move/contra=> notb_notc /negbT.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 6 Number of failed tactic applications: 258 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: 30 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: 29 Results for lemma introN: : ~ P -> ~~ b SUCCESS! Proof Found in EFSM: by case: Pb; Tactics applied: 46 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: 45 Results for lemma or3P: : reflect [\/ b1, b2 | b3] [|| b1, b2 | b3] 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. by constructor; case.] Proof search time: 0 min, 33 sec Number of successful tactic applications: 3835 Number of failed tactic applications: 6166 Results for lemma negPf: : reflect (b1 = false) (~~ b1) SUCCESS! Proof Found in EFSM: case b1; constructor ; auto ; Tactics applied: 155 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: 130 Results for lemma in3T: : {in T1 & T2 & T3, {all3 P3}} -> {all3 P3} SUCCESS! Proof Found in EFSM: move => P; auto. Tactics applied: 154 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: 5 Number of failed tactic applications: 149 Results for lemma orbK: a b : (a || b) && a = a FAILURE! Tactics applied: 109 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: 109 Results for lemma mem_topred: (pp : pT) : mem (topred pp) = mem pp FAILURE! Tactics applied: 109 Original Proof: [by rewrite /mem; case: pT pp => T1 app1 [mem1 /= ->].] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 109 Results for lemma elimTn: : b' -> ~ P FAILURE! Tactics applied: 109 Original Proof: [exact: elimTFn true _.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 109 Results for lemma addNb: a b : ~~ a (+) b = ~~ (a (+) b) FAILURE! Tactics applied: 109 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: 109 Results for lemma contraLR: (c b : bool) : (~~ c -> ~~ b) -> b -> c FAILURE! Tactics applied: 264 Original Proof: [by case: b => //; case: c.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 6 Number of failed tactic applications: 258 Results for lemma sumboolP: (decQ : decidable Q) : reflect Q decQ FAILURE! Tactics applied: 109 Original Proof: [by case: decQ; constructor.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 109 Results for lemma introP: : (b -> Q) -> (~~ b -> ~ Q) -> reflect Q b FAILURE! Tactics applied: 109 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: 109 Results for lemma orKb: a b : a && (b || a) = a FAILURE! Tactics applied: 109 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: 109 Results for lemma sub_in_bij: (D1' : pred T1) : {subset D1 <= D1'} -> {in D1', bijective f} -> {in D1, bijective f} FAILURE! Tactics applied: 681 Original Proof: [by move=> subD [g' fK g'K]; exists g' => x; move/subD; [exact: fK | exact: g'K].] Proof search time: 0 min, 1 sec Number of successful tactic applications: 9 Number of failed tactic applications: 672 Results for lemma addbF: : right_id false addb SUCCESS! Proof Found in EFSM: by case. Tactics applied: 33 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: 30 Results for lemma norP: : 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, 36 sec Number of successful tactic applications: 4108 Number of failed tactic applications: 5893 Results for lemma rev_trans: T (R : rel T) : transitive R -> transitive (fun x y => R y x) FAILURE! Tactics applied: 3070 Original Proof: [by move=> trR x y z Ryx Rzy; exact: trR Rzy Ryx.] Proof search time: 0 min, 5 sec Number of successful tactic applications: 62 Number of failed tactic applications: 3008 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, 29 sec Number of successful tactic applications: 4649 Number of failed tactic applications: 5352 Results for lemma on2W: : allQ2 f -> {on D2 &, allQ2 f} SUCCESS! Proof Found in EFSM: by move=> /= sub_dd'; Tactics applied: 70 Original Proof: [by move=> ? ?.] 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: 65 Results for lemma on_can_inj: : {on D2, cancel f & g} -> {on D2 &, injective f} FAILURE! Tactics applied: 3070 Original Proof: [by move=> fK x y /fK{2}<- /fK{2}<- ->.] Proof search time: 0 min, 7 sec Number of successful tactic applications: 46 Number of failed tactic applications: 3024 Results for lemma altP: : alt_spec b FAILURE! Tactics applied: 108 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: 108 Results for lemma negbRL: b c : ~~ b = c -> b = ~~ c FAILURE! Tactics applied: 245 Original Proof: [exact: canRL negbK.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 240 Results for lemma addTb: b : true (+) b = ~~ b SUCCESS! Proof Found in EFSM: split => [eqiR | [Rxx trR] x y z]; Tactics applied: 30 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: 29 Results for lemma can_in_inj: : {in D1, cancel f g} -> {in D1 &, injective f} FAILURE! Tactics applied: 3070 Original Proof: [by move=> fK x y /fK{2}<- /fK{2}<- ->.] Proof search time: 0 min, 6 sec Number of successful tactic applications: 46 Number of failed tactic applications: 3024 Results for lemma negPn: : reflect b1 (~~ ~~ b1) SUCCESS! Proof Found in EFSM: case b1; constructor ; auto ; Tactics applied: 155 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: 24 Number of failed tactic applications: 131 Results for lemma orbACA: : interchange orb orb SUCCESS! Proof Found in EFSM: by do 3!case. Tactics applied: 59 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: 7 Number of failed tactic applications: 52 Results for lemma addFb: : left_id false addb SUCCESS! Proof Found in EFSM: split => [eqiR | [Rxx trR] x y z]; Tactics applied: 30 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: 27 Results for lemma sub_in111: (Ph : ph {all3 P3}) : prop_in111 d1' d2' d3' Ph -> prop_in111 d1 d2 d3 Ph SUCCESS! Proof Found in EFSM: move => mf mg x y hx hy; auto. Tactics applied: 252 Original Proof: [by move=> allP x1 x2 x3 /sub1 d1x1 /sub2 d2x2 /sub3; exact: allP.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 sec Number of successful tactic applications: 11 Number of failed tactic applications: 241 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: 1152 Original Proof: [by move=> mf x y hx hy /=; rewrite -mf // !fgK_on.] Proof search time: 0 min, 2 sec Number of successful tactic applications: 23 Number of failed tactic applications: 1129 Results for lemma introF: : ~ P -> b = false SUCCESS! Proof Found in EFSM: by case: Pb; Tactics applied: 46 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: 1 Number of failed tactic applications: 45 Results for lemma orbC: : commutative orb SUCCESS! Proof Found in EFSM: by do 2!case. Tactics applied: 58 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: 55 Results for lemma addbCA: : left_commutative addb SUCCESS! Proof Found in EFSM: by do 2!case. Tactics applied: 58 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: 55 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, 30 sec Number of successful tactic applications: 3374 Number of failed tactic applications: 6627 Results for lemma implyb_idr: (a b : bool) : (b -> ~~ a) -> (a ==> b) = ~~ a FAILURE! Tactics applied: 245 Original Proof: [by case: a; case: b => // ->.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 240 Results for lemma sym_left_transitive: : left_transitive FAILURE! Tactics applied: 305 Original Proof: [by move=> x y Rxy z; apply/idP/idP; apply: trR; rewrite // symR.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 6 Number of failed tactic applications: 299 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: 55 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: 54 Results for lemma in2W: : {all2 P2} -> {in D1 & D2, {all2 P2}} SUCCESS! Proof Found in EFSM: by move=> /= sub_dd'; Tactics applied: 70 Original Proof: [by move=> ? ?.] 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: 65 Results for lemma canRL_in: x y : {in D1, cancel f g} -> x \in D1 -> f x = y -> x = g y FAILURE! Tactics applied: 760 Original Proof: [by move=> fK D1x <-; rewrite fK.] Proof search time: 0 min, 2 sec Number of successful tactic applications: 11 Number of failed tactic applications: 749 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 => mf mg x y; auto. Tactics applied: 252 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, 1 sec Number of successful tactic applications: 9 Number of failed tactic applications: 243 Results for lemma negb_imply: a b : ~~ (a ==> b) = a && ~~ b SUCCESS! Proof Found in EFSM: by case: a; Tactics applied: 48 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: 47 Results for lemma implybN: a b : (a ==> ~~ b) = (b ==> ~~ a) FAILURE! Tactics applied: 109 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: 109 Results for lemma elimT: : b -> P SUCCESS! Proof Found in EFSM: by case: Pb; Tactics applied: 46 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: 45 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, 33 sec Number of successful tactic applications: 3374 Number of failed tactic applications: 6627 Results for lemma negb_inj: : injective negb SUCCESS! Proof Found in EFSM: by do 2!case. Tactics applied: 58 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: 5 Number of failed tactic applications: 53 Results for lemma onW_bij: : bijective f -> {on D2, bijective f} FAILURE! Tactics applied: 245 Original Proof: [by case=> g' fK g'K; exists g' => * ? *; auto.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 6 Number of failed tactic applications: 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: 115 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: 113 Results for fold 2 Results for lemma orbb: : idempotent orb SUCCESS! Proof Found in EFSM: try by case. Tactics applied: 13 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: 12 Results for lemma orTb: : forall b, true || b SUCCESS! Proof Found in EFSM: try by case. Tactics applied: 13 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: 12 Results for lemma addbACA: : interchange addb addb SUCCESS! Proof Found in EFSM: by do 4!case. Tactics applied: 102 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: 3 Number of failed tactic applications: 99 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, 19 sec Number of successful tactic applications: 229 Number of failed tactic applications: 9772 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: 10000 Original Proof: [by move=> fK D2fy ->; rewrite fK.] Proof search time: 0 min, 30 sec Number of successful tactic applications: 209 Number of failed tactic applications: 9792 Results for lemma orbT: : forall b, b || true SUCCESS! Proof Found in EFSM: try by case. Tactics applied: 13 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: 12 Results for lemma forE: x P phP : @prop_for x P phP = P x SUCCESS! Proof Found in EFSM: rewrite // symR. 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 lemma addbN: a b : a (+) ~~ b = ~~ (a (+) b) SUCCESS! Proof Found in EFSM: by case: a; Tactics applied: 83 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: 3 Number of failed tactic applications: 80 Results for lemma mem_mem: (pp : pT) : (mem (mem pp) = mem pp) * (mem [mem pp] = mem pp) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -mem_topred.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 219 Number of failed tactic applications: 9782 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: 2199 Number of failed tactic applications: 7802 Results for lemma andb_idl: (a b : bool) : (b -> a) -> a && b = b SUCCESS! Proof Found in EFSM: case : b. by move->. by case: a; Tactics applied: 1193 Original Proof: [by case: a; case: b => // ->.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 1 sec Number of successful tactic applications: 58 Number of failed tactic applications: 1135 Results for lemma addbb: : self_inverse false addb SUCCESS! Proof Found in EFSM: try by case. Tactics applied: 13 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: 12 Results for lemma classicP: : forall P : Prop, classically P <-> ~ ~ P FAILURE! Tactics applied: 10000 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, 13 sec Number of successful tactic applications: 193 Number of failed tactic applications: 9808 Results for lemma inT_bij: : {in T1, bijective f} -> bijective f FAILURE! Tactics applied: 10000 Original Proof: [by case=> g' fK g'K; exists g' => * ? *; auto.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 219 Number of failed tactic applications: 9782 Results for lemma all_and3: (hP : forall x, [/\ P1 x, P2 x & P3 x]) : [/\ a P1, a P2 & a P3] FAILURE! Tactics applied: 10000 Original Proof: [by split=> x; case: (hP x).] Proof search time: 0 min, 14 sec Number of successful tactic applications: 181 Number of failed tactic applications: 9820 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, 21 sec Number of successful tactic applications: 217 Number of failed tactic applications: 9784 Results for lemma andbb: : idempotent andb SUCCESS! Proof Found in EFSM: try by case. Tactics applied: 13 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: 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, 12 sec Number of successful tactic applications: 599 Number of failed tactic applications: 9402 Results for lemma in2T: : {in T1 & T2, {all2 P2}} -> {all2 P2} SUCCESS! Proof Found in EFSM: auto ; Tactics applied: 184 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: 179 Results for lemma contraTF: (c b : bool) : (c -> ~~ b) -> b -> c = false SUCCESS! Proof Found in EFSM: case : b; by move/contra=> notb_notc /notb_notc/negbTE. Tactics applied: 477 Original Proof: [by move/contraL=> b_notc /b_notc/negbTE.] 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: 12 Number of failed tactic applications: 465 Results for lemma negbK: : involutive negb SUCCESS! Proof Found in EFSM: try by case. Tactics applied: 13 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: 12 Results for lemma equivP: : (P <-> Q) -> reflect Q b FAILURE! Tactics applied: 10000 Original Proof: [by case; exact: iffP.] Proof search time: 0 min, 14 sec Number of successful tactic applications: 470 Number of failed tactic applications: 9531 Results for lemma equivPif: : (Q -> P) -> (P -> Q) -> if b then Q else ~ Q SUCCESS! Proof Found in EFSM: case Hb. auto. auto ; Tactics applied: 8708 Original Proof: [by case Hb; auto.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 10 sec Number of successful tactic applications: 529 Number of failed tactic applications: 8179 Results for lemma xorPifn: : Q \/ P -> ~ (Q /\ P) -> if b then Q else ~ Q FAILURE! Tactics applied: 10000 Original Proof: [rewrite -if_neg; exact: xorPif.] Proof search time: 0 min, 13 sec Number of successful tactic applications: 500 Number of failed tactic applications: 9501 Results for lemma addbK: : right_loop id addb SUCCESS! Proof Found in EFSM: by do 2!case. Tactics applied: 100 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: 99 Results for lemma introFn: : P -> b' = false FAILURE! Tactics applied: 10000 Original Proof: [exact: introTFn false _.] Proof search time: 0 min, 13 sec Number of successful tactic applications: 327 Number of failed tactic applications: 9674 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, 20 sec Number of successful tactic applications: 204 Number of failed tactic applications: 9797 Results for lemma addbP: a b : reflect (~~ a = b) (a (+) b) FAILURE! Tactics applied: 10000 Original Proof: [by case: a; case: b; constructor.] Proof search time: 0 min, 14 sec Number of successful tactic applications: 248 Number of failed tactic applications: 9753 Results for lemma elimFn: : b' = false -> P FAILURE! Tactics applied: 10000 Original Proof: [exact: elimTFn false _.] Proof search time: 0 min, 13 sec Number of successful tactic applications: 353 Number of failed tactic applications: 9648 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: 95 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: 3 Number of failed tactic applications: 92 Results for lemma ifP: : if_spec (b = false) b (if b then vT else vF) FAILURE! Tactics applied: 10000 Original Proof: [by case def_b: b; constructor.] Proof search time: 0 min, 13 sec Number of successful tactic applications: 522 Number of failed tactic applications: 9479 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, 12 sec Number of successful tactic applications: 728 Number of failed tactic applications: 9273 Results for lemma equivPifn: : (Q -> P) -> (P -> Q) -> if b then ~ Q else Q FAILURE! Tactics applied: 10000 Original Proof: [rewrite -if_neg; exact: equivPif.] Proof search time: 0 min, 12 sec Number of successful tactic applications: 407 Number of failed tactic applications: 9594 Results for lemma andbC: : commutative andb SUCCESS! Proof Found in EFSM: by do 2!case. Tactics applied: 100 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: 99 Results for lemma boolP: : alt_spec b1 b1 b1 SUCCESS! Proof Found in EFSM: case b1; constructor => //; Tactics applied: 598 Original Proof: [exact: (altP idP).] 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: 39 Number of failed tactic applications: 559 Results for lemma andbAC: : right_commutative andb SUCCESS! Proof Found in EFSM: by do 3!case. Tactics applied: 101 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: 98 Results for lemma elimF: : b = false -> ~ P SUCCESS! Proof Found in EFSM: by case Pb. Tactics applied: 72 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: 71 Results for lemma is_true_true: : true SUCCESS! Proof Found in EFSM: rewrite // symR. 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 lemma negbT: b : b = false -> ~~ b SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 73 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: 72 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, 12 sec Number of successful tactic applications: 395 Number of failed tactic applications: 9606 Results for lemma orb_idl: (a b : bool) : (a -> b) -> a || b = b FAILURE! Tactics applied: 10000 Original Proof: [by case: a; case: b => // ->.] Proof search time: 0 min, 14 sec Number of successful tactic applications: 2205 Number of failed tactic applications: 7796 Results for lemma keyed_predE: : k_p =i p FAILURE! Tactics applied: 10000 Original Proof: [by case: k_p.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 209 Number of failed tactic applications: 9792 Results for lemma all_and2: (hP : forall x, [/\ P1 x & P2 x]) : [/\ a P1 & a P2] FAILURE! Tactics applied: 10000 Original Proof: [by split=> x; case: (hP x).] Proof search time: 0 min, 13 sec Number of successful tactic applications: 181 Number of failed tactic applications: 9820 Results for lemma implyNb: a b : (~~ a ==> b) = a || b SUCCESS! Proof Found in EFSM: by case: a; Tactics applied: 83 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: 3 Number of failed tactic applications: 80 Results for lemma iffP: : (P -> Q) -> (Q -> P) -> reflect Q b FAILURE! Tactics applied: 10000 Original Proof: [by case: Pb; constructor; auto.] Proof search time: 0 min, 13 sec Number of successful tactic applications: 398 Number of failed tactic applications: 9603 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 FAILURE! Tactics applied: 10000 Original Proof: [by move=> /= sub1 sub; exact: sub_in111.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 209 Number of failed tactic applications: 9792 Results for lemma elimNTF: : ~~ b = c -> if c then ~ P else P SUCCESS! Proof Found in EFSM: case Hb. by case c. by case c; Tactics applied: 7847 Original Proof: [by move <-; case Hb.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 10 sec Number of successful tactic applications: 461 Number of failed tactic applications: 7386 Results for lemma negbLR: b c : b = ~~ c -> ~~ b = c SUCCESS! Proof Found in EFSM: case : b; by case c; Tactics applied: 632 Original Proof: [exact: canLR negbK.] 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: 22 Number of failed tactic applications: 610 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: 10000 Original Proof: [by move=> /= sub_dd'; exact: sub_in111.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 209 Number of failed tactic applications: 9792 Results for lemma topredE: x (pp : pT) : topred pp x = (x \in pp) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -mem_topred.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 234 Number of failed tactic applications: 9767 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: 73 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: 72 Results for lemma contraR: (c b : bool) : (~~ c -> b) -> ~~ b -> c SUCCESS! Proof Found in EFSM: case : b; by case c; Tactics applied: 632 Original Proof: [by case: b => //; case: c.] 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: 47 Number of failed tactic applications: 585 Results for lemma andb_orr: : right_distributive andb orb SUCCESS! Proof Found in EFSM: try by case. Tactics applied: 13 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: 12 Results for lemma orbAC: : right_commutative orb SUCCESS! Proof Found in EFSM: by do 3!case. Tactics applied: 101 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: 98 Results for lemma negb_and: (a b : bool) : ~~ (a && b) = ~~ a || ~~ b SUCCESS! Proof Found in EFSM: by case: a; Tactics applied: 83 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: 3 Number of failed tactic applications: 80 Results for lemma idP: : reflect b1 b1 SUCCESS! Proof Found in EFSM: case b1; constructor => //; Tactics applied: 590 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: 39 Number of failed tactic applications: 551 Results for lemma on1W: : allQ1 f -> {on D2, allQ1 f} SUCCESS! Proof Found in EFSM: by move=> *; Tactics applied: 110 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: 107 Results for lemma implyTb: b : (true ==> b) = b SUCCESS! Proof Found in EFSM: rewrite // symR. 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 lemma and5P: : reflect [/\ b1, b2, b3, b4 & b5] [&& b1, b2, b3, b4 & b5] FAILURE! Tactics applied: 10000 Original Proof: [by case b1; case b2; case b3; case b4; case b5; constructor; try by case.] Proof search time: 0 min, 12 sec Number of successful tactic applications: 622 Number of failed tactic applications: 9379 Results for lemma andbACA: : interchange andb andb SUCCESS! Proof Found in EFSM: by do 3!case. Tactics applied: 101 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: 3 Number of failed tactic applications: 98 Results for lemma sub_in1: (Ph : ph {all1 P1}) : prop_in1 d1' Ph -> prop_in1 d1 Ph FAILURE! Tactics applied: 10000 Original Proof: [move=> allP x /sub1; exact: allP.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 209 Number of failed tactic applications: 9792 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, 20 sec Number of successful tactic applications: 204 Number of failed tactic applications: 9797 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, 14 sec Number of successful tactic applications: 602 Number of failed tactic applications: 9399 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: 73 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: 72 Results for lemma andbF: : right_zero false andb SUCCESS! Proof Found in EFSM: try by case. Tactics applied: 13 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: 12 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, 21 sec Number of successful tactic applications: 209 Number of failed tactic applications: 9792 Results for lemma onT_bij: : {on T2, bijective f} -> bijective f FAILURE! Tactics applied: 10000 Original Proof: [by case=> g' fK g'K; exists g' => * ? *; auto.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 219 Number of failed tactic applications: 9782 Results for lemma sameP: : reflect P c -> b = c SUCCESS! Proof Found in EFSM: case ; by case Pb. Tactics applied: 257 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, 0 sec Number of successful tactic applications: 10 Number of failed tactic applications: 247 Results for lemma on1T: : {on T2, allQ1 f} -> allQ1 f FAILURE! Tactics applied: 10000 Original Proof: [by move=> ? ?; auto.] Proof search time: 0 min, 27 sec Number of successful tactic applications: 209 Number of failed tactic applications: 9792 Results for lemma xorPif: : Q \/ P -> ~ (Q /\ P) -> if b then ~ Q else Q FAILURE! Tactics applied: 10000 Original Proof: [by case Hb => [? _ H ? | ? H _]; case: H.] Proof search time: 0 min, 14 sec Number of successful tactic applications: 458 Number of failed tactic applications: 9543 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, 12 sec Number of successful tactic applications: 2097 Number of failed tactic applications: 7904 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, 22 sec Number of successful tactic applications: 219 Number of failed tactic applications: 9782 Results for lemma orbCA: : left_commutative orb SUCCESS! Proof Found in EFSM: by do 2!case. Tactics applied: 100 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: 97 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: 10000 Original Proof: [by move=> /= sub_dd'; exact: sub_in11.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 209 Number of failed tactic applications: 9792 Results for lemma elimN: : ~~ b -> ~P SUCCESS! Proof Found in EFSM: by case Pb. Tactics applied: 72 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: 71 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: 10000 Original Proof: [by move=> Hf x y /Hf; rewrite fgK.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 217 Number of failed tactic applications: 9784 Results for lemma addbI: : right_injective addb SUCCESS! Proof Found in EFSM: by do 3!case. Tactics applied: 101 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: 96 Results for lemma ifF: : b = false -> (if b then vT else vF) = vF SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 73 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: 72 Results for lemma classic_pick: : forall T P, classically ({x : T | P x} + (forall x, ~ P x)) FAILURE! Tactics applied: 10000 Original Proof: [move=> T P [] // IH; apply IH; right=> x Px; case: notF. by apply: IH; left; exists x.] Proof search time: 0 min, 12 sec Number of successful tactic applications: 135 Number of failed tactic applications: 9866 Results for lemma implyb_idl: (a b : bool) : (~~ a -> b) -> (a ==> b) = b FAILURE! Tactics applied: 10000 Original Proof: [by case: a; case: b => // ->.] Proof search time: 0 min, 14 sec Number of successful tactic applications: 2205 Number of failed tactic applications: 7796 Results for lemma elimNf: : ~~ b = false -> P SUCCESS! Proof Found in EFSM: by case Pb. Tactics applied: 72 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: 71 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, 20 sec Number of successful tactic applications: 204 Number of failed tactic applications: 9797 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: 204 Number of failed tactic applications: 9797 Results for lemma ifE: : (if b then vT else vF) = if_expr SUCCESS! Proof Found in EFSM: rewrite // symR. 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 lemma on1lT: : {on T2, allQ1l f & h} -> allQ1l f h FAILURE! Tactics applied: 10000 Original Proof: [by move=> ? ?; auto.] Proof search time: 0 min, 28 sec Number of successful tactic applications: 209 Number of failed tactic applications: 9792 Results for lemma implyFb: b : false ==> b SUCCESS! Proof Found in EFSM: rewrite // symR. 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 lemma andKb: a b : a || b && a = a SUCCESS! Proof Found in EFSM: case : b; by case: a; Tactics applied: 1193 Original Proof: [by case: a; case: b.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 1 sec Number of successful tactic applications: 49 Number of failed tactic applications: 1144 Results for lemma introTF: : (if c then P else ~ P) -> b = c SUCCESS! Proof Found in EFSM: case Hb. by case c. by case c; Tactics applied: 7436 Original Proof: [by case c; case Hb.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 9 sec Number of successful tactic applications: 474 Number of failed tactic applications: 6962 Results for lemma contraFF: (c b : bool) : (c -> b) -> b = false -> c = false SUCCESS! Proof Found in EFSM: case : c. by case: b => // ->. rewrite // symR. Tactics applied: 6492 Original Proof: [by move/contraFN=> bF_notc /bF_notc/negbTE.] 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: 356 Number of failed tactic applications: 6136 Results for lemma orbA: : associative orb SUCCESS! Proof Found in EFSM: try by case. Tactics applied: 13 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: 12 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: 10000 Original Proof: [by move=> mf x y /=; rewrite -mf !fgK.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 229 Number of failed tactic applications: 9772 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: 294 Number of failed tactic applications: 9707 Results for lemma pair_andP: P Q : P /\ Q <-> P * Q SUCCESS! Proof Found in EFSM: constructor ; try by case. Tactics applied: 383 Original Proof: [by split; case.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 0 sec Number of successful tactic applications: 21 Number of failed tactic applications: 362 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, 12 sec Number of successful tactic applications: 642 Number of failed tactic applications: 9359 Results for lemma implybE: a b : (a ==> b) = ~~ a || b SUCCESS! Proof Found in EFSM: by case: a; Tactics applied: 83 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: 3 Number of failed tactic applications: 80 Results for lemma andNb: b : ~~ b && b = false SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 73 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: 70 Results for lemma negP: : reflect (~ b1) (~~ b1) SUCCESS! Proof Found in EFSM: case b1; constructor => //; Tactics applied: 598 Original Proof: [by case b1; constructor; auto.] Shorter Proof Found? yes 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: 39 Number of failed tactic applications: 559 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, 15 sec Number of successful tactic applications: 181 Number of failed tactic applications: 9820 Results for lemma andb_orl: : left_distributive andb orb SUCCESS! Proof Found in EFSM: by do 3!case. Tactics applied: 101 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: 98 Results for lemma negbF: b : (b : bool) -> ~~ b = false SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 73 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: 72 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: 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: 204 Number of failed tactic applications: 9797 Results for lemma andb_addr: : right_distributive andb addb SUCCESS! Proof Found in EFSM: try by case. Tactics applied: 13 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: 12 Results for lemma introT: : P -> b SUCCESS! Proof Found in EFSM: by case Pb. Tactics applied: 72 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: 71 Results for lemma and3P: : reflect [/\ b1, b2 & b3] [&& b1, b2 & b3] FAILURE! Tactics applied: 10000 Original Proof: [by case b1; case b2; case b3; constructor; try by case.] Proof search time: 0 min, 11 sec Number of successful tactic applications: 622 Number of failed tactic applications: 9379 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, 12 sec Number of successful tactic applications: 2638 Number of failed tactic applications: 7363 Results for lemma classic_EM: : forall P, classically (decidable P) FAILURE! Tactics applied: 10000 Original Proof: [by move=> P [] // IH; apply IH; right => ?; apply: notF (IH _); left.] Proof search time: 0 min, 11 sec Number of successful tactic applications: 135 Number of failed tactic applications: 9866 Results for lemma implybF: b : (b ==> false) = ~~ b SUCCESS! Proof Found in EFSM: rewrite // symR. 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: 3 Number of failed tactic applications: 14 Results for lemma sub_in11: (Ph : ph {all2 P2}) : prop_in11 d1' d2' Ph -> prop_in11 d1 d2 Ph FAILURE! Tactics applied: 10000 Original Proof: [move=> allP x1 x2 /sub1 d1x1 /sub2; exact: allP.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 204 Number of failed tactic applications: 9797 Results for lemma subon1l: (Phf : ph (allQ1l f)) (Ph : ph (allQ1l f h)) : prop_on1 d2' Phf Ph -> prop_on1 d2 Phf Ph FAILURE! Tactics applied: 10000 Original Proof: [by move=> allQ x /sub2; exact: allQ.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 209 Number of failed tactic applications: 9792 Results for lemma addbC: : commutative addb SUCCESS! Proof Found in EFSM: by do 2!case. Tactics applied: 100 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: 99 Results for lemma in1W: : {all1 P1} -> {in D1, {all1 P1}} SUCCESS! Proof Found in EFSM: by move=> *; Tactics applied: 110 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: 107 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, 20 sec Number of successful tactic applications: 209 Number of failed tactic applications: 9792 Results for lemma implybNN: a b : (~~ a ==> ~~ b) = b ==> a SUCCESS! Proof Found in EFSM: case : b; by case: a; Tactics applied: 823 Original Proof: [by case: a; case: b.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 1 sec Number of successful tactic applications: 31 Number of failed tactic applications: 792 Results for lemma addbA: : associative addb SUCCESS! Proof Found in EFSM: by do 3!case. Tactics applied: 101 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: 98 Results for lemma negb_or: (a b : bool) : ~~ (a || b) = ~~ a && ~~ b SUCCESS! Proof Found in EFSM: by case: a; Tactics applied: 83 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: 5 Number of failed tactic applications: 78 Results for lemma idPn: : reflect (~~ b1) (~~ b1) SUCCESS! Proof Found in EFSM: case b1; constructor => //; Tactics applied: 598 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: 39 Number of failed tactic applications: 559 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, 30 sec Number of successful tactic applications: 209 Number of failed tactic applications: 9792 Results for lemma wlog_neg: b : (~~ b -> b) -> b SUCCESS! Proof Found in EFSM: by case: b => // ->. Tactics applied: 88 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: 87 Results for lemma negbFE: b : ~~ b = false -> b SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 73 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: 72 Results for lemma negbTE: b : ~~ b -> b = false SUCCESS! Proof Found in EFSM: by case b. Tactics applied: 73 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: 72 OVERALL RESULTS SUMMARY EFSMProver proved 124 out of 240 lemmas. Success rate of 51.66666666666667% There were 0 errors. 116 proof attempts exhausted the automaton On average, a proof was found after applying 366 tactics The longest proof consisted of 3 tactics There were 9 shorter proofs found Of the 116 failures, 64 of them used all 10000 tactics There were 100 reused proofs found There were 24 novel proofs found Of the 116 failures, the average number of tactics used was 5853 On average, a proof was found after 0 min, 0 sec On average, a failed proof attempt took 0 min, 11 sec On average, any (success or failure) proof attempt took 0 min, 5 sec The longest time to find a proof was 0 min, 10 sec The shortest time to find a proof was 0 min, 0 sec There were 0 proofs containing repeated tactics There were 15 proofs that repeated states