Results for fold 1 Results for lemma pair_eqP: : Equality.axiom pair_eq FAILURE! Tactics applied: 1019 Original Proof: [move=> [x1 x2] [y1 y2] /=; apply: (iffP andP) => [[]|[<- <-]] //=. by do 2!move/eqP->.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 12 Number of failed tactic applications: 1007 Results for lemma val_eqE: (u v : sT) : (val u == val v) = (u == v) SUCCESS! Proof Found in EFSM: constructor. Tactics applied: 2 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: 1 Results for lemma eqP: T : Equality.axiom (@eq_op T) FAILURE! Tactics applied: 707 Original Proof: [by case: T => ? [].] Proof search time: 0 min, 0 sec Number of successful tactic applications: 8 Number of failed tactic applications: 699 Results for lemma bij_eq: : bijective f -> forall x y, (f x == f y) = (x == y) FAILURE! Tactics applied: 733 Original Proof: [move/bij_inj; apply: inj_eq.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 10 Number of failed tactic applications: 723 Results for lemma memPn: A x : reflect {in A, forall y, y != x} (x \notin A) FAILURE! Tactics applied: 149 Original Proof: [apply: (iffP idP) => [notDx y | notDx]; first by apply: contraTneq => ->. exact: contraL (notDx x) _.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 147 Results for lemma val_inj: : injective (@val sT) FAILURE! Tactics applied: 727 Original Proof: [exact: pcan_inj valK.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 8 Number of failed tactic applications: 719 Results for lemma pair_eq1: (u v : T1 * T2) : u == v -> u.1 == v.1 SUCCESS! Proof Found in EFSM: by case/andP. Tactics applied: 75 Original Proof: [by case/andP.] 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: 70 Results for lemma contraTneq: b x y : (x = y -> ~~ b) -> b -> x != y FAILURE! Tactics applied: 298 Original Proof: [by move=> imp; apply: contraTN => /eqP.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 293 Results for lemma contra_neq: x1 y1 x2 y2 : (x2 = y2 -> x1 = y1) -> x1 != y1 -> x2 != y2 FAILURE! Tactics applied: 10000 Original Proof: [by move=> imp; apply: contraNneq => /imp->.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 708 Number of failed tactic applications: 9293 Results for lemma inj_eqAxiom: : injective f -> Equality.axiom (fun x y => f x == f y) FAILURE! Tactics applied: 1012 Original Proof: [by move=> f_inj x y; apply: (iffP eqP) => [|-> //]; exact: f_inj.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 12 Number of failed tactic applications: 1000 Results for lemma tag_eqP: : Equality.axiom tag_eq FAILURE! Tactics applied: 1019 Original Proof: [rewrite /tag_eq => [] [i x] [j] /=. case: eqP => [<-|Hij] y; last by right; case. by apply: (iffP eqP) => [->|<-]; rewrite tagged_asE.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 12 Number of failed tactic applications: 1007 Results for lemma tagged_asE: u x : tagged_as u (Tagged T_ x) = x FAILURE! Tactics applied: 146 Original Proof: [by rewrite /tagged_as /=; case: eqP => // eq_uu; rewrite [eq_uu]eq_axiomK.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 145 Results for lemma valK: : pcancel (@val _) insub FAILURE! Tactics applied: 143 Original Proof: [case/SubP=> x Px; rewrite SubK; exact: insubT.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 143 Results for lemma inj_eq: : injective f -> forall x y, (f x == f y) = (x == y) FAILURE! Tactics applied: 728 Original Proof: [by move=> inj_f x y; apply/eqP/eqP=> [|-> //]; exact: inj_f.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 10 Number of failed tactic applications: 718 Results for lemma SubP: u : Sub_spec u FAILURE! Tactics applied: 143 Original Proof: [by case: sT Sub_spec SubSpec u => T' _ C rec /= _.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 143 Results for lemma eqVneq: : {x = y} + {x != y} SUCCESS! Proof Found in EFSM: case : eqP. by [constructor | apply: (iffP eqP) => [|[]] ->]. by [left | right]. Tactics applied: 362 Original Proof: [by case: eqP; [left | right].] 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: 16 Number of failed tactic applications: 346 Results for lemma can_in_eq: : {in D, cancel f g} -> {in D &, forall x y, (f x == f y) = (x == y)} FAILURE! Tactics applied: 733 Original Proof: [by move/can_in_inj; exact: inj_in_eq.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 10 Number of failed tactic applications: 723 Results for fold 2 Results for lemma bool_irrelevance: (x y : bool) (E E' : x = y) : E = E' FAILURE! Tactics applied: 163 Original Proof: [exact: eq_irrelevance.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 162 Results for lemma contra_eqT: b x y : (~~ b -> x != y) -> x = y -> b FAILURE! Tactics applied: 489 Original Proof: [by move=> imp /eqP; apply: contraLR.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 5 Number of failed tactic applications: 484 Results for lemma svalP: : forall u : sig P, P (sval u) SUCCESS! Proof Found in EFSM: case. by []. Tactics applied: 556 Original Proof: [by case.] 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: 546 Results for lemma eq_tag: u v : u == v -> tag u = tag v SUCCESS! Proof Found in EFSM: case : eqP => [<-|Hij] y; exact /eqP. Tactics applied: 999 Original Proof: [by move/eqP->.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 2 sec Number of successful tactic applications: 29 Number of failed tactic applications: 970 Results for lemma insubT: x Px : insub x = Some (Sub x Px) FAILURE! Tactics applied: 322 Original Proof: [case: insubP; last by case/negP. case/SubP=> y Py _ def_x; rewrite -def_x SubK in Px *. congr (Some (Sub _ _)); exact: bool_irrelevance.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 321 Results for lemma eqbE: : eqb = eq_op SUCCESS! Proof Found in EFSM: constructor. Tactics applied: 2 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: 1 Results for lemma contraFeq: b x y : (x != y -> b) -> b = false -> x = y SUCCESS! Proof Found in EFSM: case : eqP => // eq_uu; by move->; Tactics applied: 265 Original Proof: [by move=> imp /negbT; apply: contraNeq.] 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: 5 Number of failed tactic applications: 260 Results for lemma vrefl: : forall x, P x -> x = x SUCCESS! Proof Found in EFSM: constructor. Tactics applied: 2 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: 1 Results for lemma contraNeq: b x y : (x != y -> b) -> ~~ b -> x = y SUCCESS! Proof Found in EFSM: case : eqP => // eq_uu; by move->; Tactics applied: 265 Original Proof: [by move=> imp hyp; apply/eqP; apply: contraNT hyp.] 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: 5 Number of failed tactic applications: 260 Results for lemma valP: (u : sT) : P (val u) SUCCESS! Proof Found in EFSM: apply : contraTeq. by move->. constructor. Tactics applied: 2578 Original Proof: [by case/SubP: u => x Px; rewrite SubK.] 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: 81 Number of failed tactic applications: 2497 Results for lemma insubF: x : P x = false -> insub x = None SUCCESS! Proof Found in EFSM: case : insubP => [u -> | /negPf->]. by []. constructor. Tactics applied: 485 Original Proof: [by move/idP; case: insubP.] 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: 18 Number of failed tactic applications: 467 Results for lemma tag_eqE: : tag_eq = eq_op SUCCESS! Proof Found in EFSM: constructor. Tactics applied: 2 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: 1 Results for lemma insubP: x : insub_spec x (insub x) FAILURE! Tactics applied: 159 Original Proof: [by rewrite /insub; case: {-}_ / idP; [left; rewrite ?SubK | right; exact/negP].] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 159 Results for lemma s2valP: u : P (s2val u) SUCCESS! Proof Found in EFSM: by case: u. Tactics applied: 94 Original Proof: [by case: u.] 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: 93 Results for lemma val_eqP: : ev_ax sT val SUCCESS! Proof Found in EFSM: move => inj_h x; apply : (iffP eqP) => [|-> //]; apply : val_inj; Tactics applied: 1520 Original Proof: [exact: inj_eqAxiom val_inj.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 2 sec Number of successful tactic applications: 25 Number of failed tactic applications: 1495 Results for lemma unit_eqP: : Equality.axiom (fun _ _ : unit => true) SUCCESS! Proof Found in EFSM: case. case. by [constructor | apply: (iffP eqP) => [|[]] ->]. Tactics applied: 1040 Original Proof: [by do 2!case; left.] 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, 1 sec Number of successful tactic applications: 14 Number of failed tactic applications: 1026 Results for lemma insubN: x : ~~ P x -> insub x = None SUCCESS! Proof Found in EFSM: case : insubP => [u -> | /negPf->]. by []. constructor. Tactics applied: 485 Original Proof: [by move/negPf/insubF.] 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: 16 Number of failed tactic applications: 469 Results for fold 3 Results for lemma can_eq: : cancel f g -> forall x y, (f x == f y) = (x == y) FAILURE! Tactics applied: 98 Original Proof: [move/can_inj; exact: inj_eq.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 98 Results for lemma predU1P: : reflect (x = y \/ b) ((x == y) || b) FAILURE! Tactics applied: 100 Original Proof: [apply: (iffP orP) => [] []; by [right | move/eqP; left].] Proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 99 Results for lemma pred1E: : pred1 =2 eq_op FAILURE! Tactics applied: 98 Original Proof: [move=> x y; exact: eq_sym.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 98 Results for lemma invariant_inj: : injective h -> invariant f (h \o k) =1 invariant f k FAILURE! Tactics applied: 98 Original Proof: [move=> inj_h x; exact: (inj_eq inj_h).] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 98 Results for lemma eq_frel: f f' : f =1 f' -> frel f =2 frel f' FAILURE! Tactics applied: 98 Original Proof: [by move=> eq_f x y; rewrite /= eq_f.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 98 Results for lemma eqE: T x : eq_op x = Equality.op (Equality.class T) x SUCCESS! Proof Found in EFSM: by []. 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 val_insubd: u0 x : val (insubd u0 x) = if P x then x else val u0 FAILURE! Tactics applied: 98 Original Proof: [by rewrite /insubd; case: insubP => [u -> | /negPf->].] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 98 Results for lemma valKd: u0 : cancel (@val _) (insubd u0) FAILURE! Tactics applied: 322 Original Proof: [by move=> u; rewrite /insubd valK.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 6 Number of failed tactic applications: 316 Results for lemma eq_refl: (T : eqType) (x : T) : x == x SUCCESS! Proof Found in EFSM: by case: eqP; Tactics applied: 30 Original Proof: [exact/eqP.] 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: 28 Results for lemma contra_eq: x1 y1 x2 y2 : (x2 != y2 -> x1 != y1) -> x1 = y1 -> x2 = y2 FAILURE! Tactics applied: 98 Original Proof: [by move=> imp /eqP; apply: contraTeq.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 98 Results for lemma invariant_comp: : subpred (invariant f k) (invariant f (h \o k)) FAILURE! Tactics applied: 98 Original Proof: [by move=> x eq_kfx; rewrite /= (eqP eq_kfx).] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 98 Results for lemma isSome_insub: : ([eta insub] : pred T) =1 P FAILURE! Tactics applied: 98 Original Proof: [by apply: fsym => x; case: insubP => // /negPf.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 98 Results for lemma sum_eqP: : Equality.axiom sum_eq FAILURE! Tactics applied: 126 Original Proof: [case=> x [] y /=; by [right | apply: (iffP eqP) => [->|[->]]].] Proof search time: 0 min, 0 sec Number of successful tactic applications: 4 Number of failed tactic applications: 122 Results for lemma pair_eqE: : pair_eq = eq_op :> rel _ SUCCESS! Proof Found in EFSM: by []. 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 negb_add: b1 b2 : ~~ (b1 (+) b2) = (b1 == b2) FAILURE! Tactics applied: 98 Original Proof: [by rewrite -addNb.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 98 Results for lemma eqbF_neg: b : (b == false) = ~~ b SUCCESS! Proof Found in EFSM: by case: b. Tactics applied: 27 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: 26 Results for lemma s2valP': u : Q (s2val u) SUCCESS! Proof Found in EFSM: by case: u. Tactics applied: 34 Original Proof: [by case: u.] 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 4 Results for lemma compareP: : Equality.axiom compareb FAILURE! Tactics applied: 256 Original Proof: [by move=> x y; exact: sumboolP.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 4 Number of failed tactic applications: 252 Results for lemma eqbP: : Equality.axiom eqb FAILURE! Tactics applied: 256 Original Proof: [by do 2!case; constructor.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 4 Number of failed tactic applications: 252 Results for lemma innew_val: T nT : cancel val (@innew T nT) FAILURE! Tactics applied: 354 Original Proof: [by move=> u; apply: val_inj; exact: SubK.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 10 Number of failed tactic applications: 344 Results for lemma contra_eqF: b x y : (b -> x != y) -> x = y -> b = false FAILURE! Tactics applied: 220 Original Proof: [by move=> imp /eqP; apply: contraTF.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 215 Results for lemma sum_eqE: : sum_eq = eq_op 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: 1 Number of failed tactic applications: 26 Results for lemma insubdK: u0 : {in P, cancel (insubd u0) (@val _)} FAILURE! Tactics applied: 256 Original Proof: [by move=> x Px; rewrite /= val_insubd [P x]Px.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 4 Number of failed tactic applications: 252 Results for lemma can2_eq: : cancel f g -> cancel g f -> forall x y, (f x == y) = (x == g y) FAILURE! Tactics applied: 332 Original Proof: [by move=> fK gK x y; rewrite -{1}[y]gK; exact: can_eq.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 6 Number of failed tactic applications: 326 Results for lemma pair_eq2: (u v : T1 * T2) : u == v -> u.2 == v.2 SUCCESS! Proof Found in EFSM: by case/andP. Tactics applied: 41 Original Proof: [by case/andP.] 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: 38 Results for lemma eqb_negLR: b1 b2 : (~~ b1 == b2) = (b1 == ~~ b2) FAILURE! Tactics applied: 10000 Original Proof: [by case: b1; case: b2.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 2311 Number of failed tactic applications: 7690 Results for lemma contra_eqN: b x y : (b -> x != y) -> x = y -> ~~ b FAILURE! Tactics applied: 220 Original Proof: [by move=> imp /eqP; apply: contraL.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 5 Number of failed tactic applications: 215 Results for lemma eq_Tagged: u x :(u == Tagged _ x) = (tagged u == x) FAILURE! Tactics applied: 10000 Original Proof: [by rewrite -tag_eqE /tag_eq eqxx tagged_asE.] Proof search time: 0 min, 36 sec Number of successful tactic applications: 2697 Number of failed tactic applications: 7304 Results for lemma predU1r: : b -> (x == y) || b SUCCESS! Proof Found in EFSM: by case: eqP; Tactics applied: 44 Original Proof: [by move->; rewrite orbT.] 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: 43 Results for lemma contraTeq: b x y : (x != y -> ~~ b) -> b -> x = y FAILURE! Tactics applied: 3354 Original Proof: [by move=> imp hyp; apply/eqP; apply: contraTT hyp.] Proof search time: 0 min, 5 sec Number of successful tactic applications: 87 Number of failed tactic applications: 3267 Results for lemma ifN_eqC: R x y vT vF : x != y -> (if y == x then vT else vF) = vF :> R SUCCESS! Proof Found in EFSM: case : eqP. by []. case : eqP => // eq_uu; by case. Tactics applied: 894 Original Proof: [by rewrite eq_sym; apply: ifN.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 sec Number of successful tactic applications: 78 Number of failed tactic applications: 816 Results for lemma SubK: x Px : @val sT (Sub x Px) = x FAILURE! Tactics applied: 105 Original Proof: [by case: sT.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 104 Results for lemma inj_in_eq: : {in D &, injective f} -> {in D &, forall x y, (f x == f y) = (x == y)} FAILURE! Tactics applied: 256 Original Proof: [by move=> inj_f x y Dx Dy; apply/eqP/eqP=> [|-> //]; exact: inj_f.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 4 Number of failed tactic applications: 252 Results for lemma inv_eq: f : involutive f -> forall x y : T, (f x == y) = (x == f y) FAILURE! Tactics applied: 332 Original Proof: [by move=> fK; exact: can2_eq.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 6 Number of failed tactic applications: 326 Results for fold 5 Results for lemma pred2P: : reflect (x = y \/ z = u) ((x == y) || (z == u)) FAILURE! Tactics applied: 10000 Original Proof: [by apply: (iffP orP) => [] [] /eqP; by [left | right].] Proof search time: 0 min, 23 sec Number of successful tactic applications: 262 Number of failed tactic applications: 9739 Results for lemma insub_eqE: : insub_eq =1 insub FAILURE! Tactics applied: 160 Original Proof: [rewrite /insub_eq /insub => x; case: {2 3}_ / idP (erefl _) => // Px Px'. by congr (Some _); apply: val_inj; rewrite !SubK.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 160 Results for lemma insubK: : ocancel insub (@val _) FAILURE! Tactics applied: 160 Original Proof: [by move=> x; case: insubP.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 160 Results for lemma predU1l: : x = y -> (x == y) || b SUCCESS! Proof Found in EFSM: case : eqP => // eq_uu; Tactics applied: 64 Original Proof: [by move->; rewrite eqxx.] 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: 63 Results for lemma predD1P: : reflect (x <> y /\ b) ((x != y) && b) FAILURE! Tactics applied: 480 Original Proof: [by apply: (iffP andP)=> [] [] // /eqP.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 3 Number of failed tactic applications: 477 Results for lemma eqb_id: b : (b == true) = b SUCCESS! Proof Found in EFSM: exact : eq_sym. Tactics applied: 47 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: 5 Number of failed tactic applications: 42 Results for lemma contraFneq: b x y : (x = y -> b) -> b = false -> x != y SUCCESS! Proof Found in EFSM: case : eqP => // eq_uu; by move->; Tactics applied: 262 Original Proof: [by move=> imp /negbT; apply: contraNneq.] 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: 3 Number of failed tactic applications: 259 Results for lemma eq_irrelevance: (T : eqType) x y : forall e1 e2 : x = y :> T, e1 = e2 FAILURE! Tactics applied: 160 Original Proof: [pose proj z e := if x =P z is ReflectT e0 then e0 else e. suff: injective (proj y) by rewrite /proj => injp e e'; apply: injp; case: eqP. pose join (e : x = _) := etrans (esym e). apply: can_inj (join x y (proj x (erefl x))) _. by case: y /; case: _ / (proj x _).] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 160 Results for lemma contraNneq: b x y : (x = y -> b) -> ~~ b -> x != y SUCCESS! Proof Found in EFSM: case : eqP => // eq_uu; by move->; Tactics applied: 260 Original Proof: [by move=> imp; apply: contraNN => /eqP.] 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: 3 Number of failed tactic applications: 257 Results for lemma ifN_eq: R x y vT vF : x != y -> (if x == y then vT else vF) = vF :> R SUCCESS! Proof Found in EFSM: apply : ifN. Tactics applied: 35 Original Proof: [exact: ifN.] 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 lemma eq_sym: (T : eqType) (x y : T) : (x == y) = (y == x) SUCCESS! Proof Found in EFSM: apply /eqP/eqP=> [|-> //]; exact : eq_sym. Tactics applied: 207 Original Proof: [exact/eqP/eqP.] 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: 200 Results for lemma xpair_eqE: (x1 y1 : T1) (x2 y2 : T2) : ((x1, x2) == (y1, y2)) = ((x1 == y1) && (x2 == y2)) SUCCESS! Proof Found in EFSM: constructor. Tactics applied: 2 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: 1 Results for lemma negb_eqb: b1 b2 : (b1 != b2) = b1 (+) b2 SUCCESS! Proof Found in EFSM: apply : contraTeq. by move->. constructor. Tactics applied: 5922 Original Proof: [by rewrite -addNb negbK.] 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: 5448 Results for lemma opt_eqP: : Equality.axiom opt_eq FAILURE! Tactics applied: 1600 Original Proof: [case=> [x|] [y|] /=; by [constructor | apply: (iffP eqP) => [|[]] ->].] Proof search time: 0 min, 2 sec Number of successful tactic applications: 9 Number of failed tactic applications: 1591 OVERALL RESULTS SUMMARY EFSMProver proved 33 out of 82 lemmas. Success rate of 40.243902439024396% There were 0 errors. 49 proof attempts exhausted the automaton On average, a proof was found after applying 504 tactics The longest proof consisted of 4 tactics There were 3 shorter proofs found Of the 49 failures, 4 of them used all 10000 tactics There were 18 reused proofs found There were 15 novel proofs found Of the 49 failures, the average number of tactics used was 1196 On average, a proof was found after 0 min, 1 sec On average, a failed proof attempt took 0 min, 2 sec On average, any (success or failure) proof attempt took 0 min, 2 sec The longest time to find a proof was 0 min, 9 sec The shortest time to find a proof was 0 min, 0 sec There were 1 proofs containing repeated tactics There were 12 proofs that repeated states