Results for fold 1 Results for lemma unit_eqP: : Equality.axiom (fun _ _ : unit => true) SUCCESS! Proof Found in EFSM: [by do 2!case;, constructor ] Tactics applied: 381 Original Proof: [by do 2!case; left.] Shorter Proof Found? no Proof reused from eqbP proof search time: 0 min, 0 sec Results for lemma contraNneq: b x y : (x = y -> b) -> ~~ b -> x != y FAILURE! Tactics applied: 1942 Original Proof: [by move=> imp; apply: contraNN => /eqP.] Proof search time: 0 min, 2 sec Results for lemma pair_eqP: : Equality.axiom pair_eq FAILURE! Tactics applied: 2074 Original Proof: [move=> [x1 x2] [y1 y2] /=; apply: (iffP andP) => [[]|[<- <-]] //=. by do 2!move/eqP->.] Proof search time: 0 min, 3 sec Results for lemma contraTeq: b x y : (x != y -> ~~ b) -> b -> x = y FAILURE! Tactics applied: 1975 Original Proof: [by move=> imp hyp; apply/eqP; apply: contraTT hyp.] Proof search time: 0 min, 2 sec Results for lemma ifN_eqC: R x y vT vF : x != y -> (if y == x then vT else vF) = vF :> R FAILURE! Tactics applied: 1975 Original Proof: [by rewrite eq_sym; apply: ifN.] Proof search time: 0 min, 2 sec Results for lemma contra_eqF: b x y : (b -> x != y) -> x = y -> b = false FAILURE! Tactics applied: 1975 Original Proof: [by move=> imp /eqP; apply: contraTF.] Proof search time: 0 min, 2 sec Results for lemma valKd: u0 : cancel (@val _) (insubd u0) FAILURE! Tactics applied: 2154 Original Proof: [by move=> u; rewrite /insubd valK.] Proof search time: 0 min, 3 sec Results for lemma innew_val: T nT : cancel val (@innew T nT) FAILURE! Tactics applied: 2232 Original Proof: [by move=> u; apply: val_inj; exact: SubK.] Proof search time: 0 min, 3 sec 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: [by case eqP] Tactics applied: 29 Original Proof: [exact: ifN.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for fold 2 Results for lemma sum_eqP: : Equality.axiom sum_eq FAILURE! Tactics applied: 4878 Original Proof: [case=> x [] y /=; by [right | apply: (iffP eqP) => [->|[->]]].] Proof search time: 0 min, 6 sec Results for lemma insubP: x : insub_spec x (insub x) FAILURE! Tactics applied: 4403 Original Proof: [by rewrite /insub; case: {-}_ / idP; [left; rewrite ?SubK | right; exact/negP].] Proof search time: 0 min, 2 sec Results for lemma contra_eq: x1 y1 x2 y2 : (x2 != y2 -> x1 != y1) -> x1 = y1 -> x2 = y2 FAILURE! Tactics applied: 4877 Original Proof: [by move=> imp /eqP; apply: contraTeq.] Proof search time: 0 min, 5 sec Results for lemma xpair_eqE: (x1 y1 : T1) (x2 y2 : T2) : ((x1, x2) == (y1, y2)) = ((x1 == y1) && (x2 == y2)) SUCCESS! Proof Found in EFSM: [by [] ] Tactics applied: 14 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma tag_eqP: : Equality.axiom tag_eq FAILURE! Tactics applied: 5015 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, 6 sec Results for lemma insubT: x Px : insub x = Some (Sub x Px) FAILURE! Tactics applied: 4467 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, 3 sec Results for lemma inj_eqAxiom: : injective f -> Equality.axiom (fun x y => f x == f y) FAILURE! Tactics applied: 4877 Original Proof: [by move=> f_inj x y; apply: (iffP eqP) => [|-> //]; exact: f_inj.] Proof search time: 0 min, 6 sec Results for lemma inj_eq: : injective f -> forall x y, (f x == f y) = (x == y) FAILURE! Tactics applied: 4707 Original Proof: [by move=> inj_f x y; apply/eqP/eqP=> [|-> //]; exact: inj_f.] Proof search time: 0 min, 6 sec Results for lemma eqVneq: : {x = y} + {x != y} FAILURE! Tactics applied: 4605 Original Proof: [by case: eqP; [left | right].] Proof search time: 0 min, 3 sec Results for fold 3 Results for lemma valK: : pcancel (@val _) insub FAILURE! Tactics applied: 4054 Original Proof: [case/SubP=> x Px; rewrite SubK; exact: insubT.] Proof search time: 0 min, 4 sec Results for lemma tag_eqE: : tag_eq = eq_op SUCCESS! Proof Found in EFSM: [by [] ] Tactics applied: 14 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma negb_add: b1 b2 : ~~ (b1 (+) b2) = (b1 == b2) SUCCESS! Proof Found in EFSM: [by case b1;, case b2 ] Tactics applied: 425 Original Proof: [by rewrite -addNb.] Shorter Proof Found? no Proof reused from eqb_negLR proof search time: 0 min, 0 sec Results for lemma sum_eqE: : sum_eq = eq_op SUCCESS! Proof Found in EFSM: [by [] ] Tactics applied: 14 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma predU1P: : reflect (x = y \/ b) ((x == y) || b) FAILURE! Tactics applied: 4166 Original Proof: [apply: (iffP orP) => [] []; by [right | move/eqP; left].] Proof search time: 0 min, 3 sec Results for lemma eqbP: : Equality.axiom eqb SUCCESS! Proof Found in EFSM: [by do 2!case;, by [constructor apply (iffP eqP) => [[]] ->] ] Tactics applied: 602 Original Proof: [by do 2!case; constructor.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 0 sec Results for lemma insub_eqE: : insub_eq =1 insub FAILURE! Tactics applied: 4054 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, 4 sec Results for lemma eq_tag: u v : u == v -> tag u = tag v SUCCESS! Proof Found in EFSM: [by do 2!case;, case eqP => [<-Hij] y] Tactics applied: 517 Original Proof: [by move/eqP->.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 sec Results for lemma s2valP: u : P (s2val u) SUCCESS! Proof Found in EFSM: [by case u ] Tactics applied: 27 Original Proof: [by case: u.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for fold 4 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: 26 Original Proof: [by case/andP.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma invariant_comp: : subpred (invariant f k) (invariant f (h \o k)) FAILURE! Tactics applied: 4796 Original Proof: [by move=> x eq_kfx; rewrite /= (eqP eq_kfx).] Proof search time: 0 min, 5 sec Results for lemma contraNeq: b x y : (x != y -> b) -> ~~ b -> x = y FAILURE! Tactics applied: 4498 Original Proof: [by move=> imp hyp; apply/eqP; apply: contraNT hyp.] Proof search time: 0 min, 5 sec Results for lemma eqb_id: b : (b == true) = b SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 28 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma memPn: A x : reflect {in A, forall y, y != x} (x \notin A) FAILURE! Tactics applied: 4498 Original Proof: [apply: (iffP idP) => [notDx y | notDx]; first by apply: contraTneq => ->. exact: contraL (notDx x) _.] Proof search time: 0 min, 3 sec Results for lemma inv_eq: f : involutive f -> forall x y : T, (f x == y) = (x == f y) FAILURE! Tactics applied: 4743 Original Proof: [by move=> fK; exact: can2_eq.] Proof search time: 0 min, 6 sec Results for lemma compareP: : Equality.axiom compareb FAILURE! Tactics applied: 4620 Original Proof: [by move=> x y; exact: sumboolP.] Proof search time: 0 min, 4 sec Results for lemma SubK: x Px : @val sT (Sub x Px) = x FAILURE! Tactics applied: 4269 Original Proof: [by case: sT.] Proof search time: 0 min, 3 sec Results for lemma contra_eqN: b x y : (b -> x != y) -> x = y -> ~~ b FAILURE! Tactics applied: 4498 Original Proof: [by move=> imp /eqP; apply: contraL.] Proof search time: 0 min, 4 sec Results for fold 5 Results for lemma eq_Tagged: u x :(u == Tagged _ x) = (tagged u == x) FAILURE! Tactics applied: 4312 Original Proof: [by rewrite -tag_eqE /tag_eq eqxx tagged_asE.] Proof search time: 0 min, 6 sec Results for lemma negb_eqb: b1 b2 : (b1 != b2) = b1 (+) b2 SUCCESS! Proof Found in EFSM: [by case b1;, case b2 ] Tactics applied: 587 Original Proof: [by rewrite -addNb negbK.] Shorter Proof Found? no Proof reused from eqb_negLR proof search time: 0 min, 0 sec Results for lemma eqP: T : Equality.axiom (@eq_op T) FAILURE! Tactics applied: 3955 Original Proof: [by case: T => ? [].] Proof search time: 0 min, 4 sec Results for lemma eq_irrelevance: (T : eqType) x y : forall e1 e2 : x = y :> T, e1 = e2 FAILURE! Tactics applied: 4312 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, 4 sec Results for lemma contraFeq: b x y : (x != y -> b) -> b = false -> x = y FAILURE! Tactics applied: 4312 Original Proof: [by move=> imp /negbT; apply: contraNeq.] Proof search time: 0 min, 4 sec Results for lemma eq_sym: (T : eqType) (x y : T) : (x == y) = (y == x) FAILURE! Tactics applied: 4312 Original Proof: [exact/eqP/eqP.] Proof search time: 0 min, 3 sec Results for lemma tagged_asE: u x : tagged_as u (Tagged T_ x) = x FAILURE! Tactics applied: 4312 Original Proof: [by rewrite /tagged_as /=; case: eqP => // eq_uu; rewrite [eq_uu]eq_axiomK.] Proof search time: 0 min, 4 sec Results for lemma SubP: u : Sub_spec u FAILURE! Tactics applied: 4312 Original Proof: [by case: sT Sub_spec SubSpec u => T' _ C rec /= _.] Proof search time: 0 min, 3 sec Results for lemma eq_frel: f f' : f =1 f' -> frel f =2 frel f' FAILURE! Tactics applied: 4536 Original Proof: [by move=> eq_f x y; rewrite /= eq_f.] Proof search time: 0 min, 5 sec Results for fold 6 Results for lemma bool_irrelevance: (x y : bool) (E E' : x = y) : E = E' FAILURE! Tactics applied: 7719 Original Proof: [exact: eq_irrelevance.] Proof search time: 0 min, 7 sec Results for lemma insubdK: u0 : {in P, cancel (insubd u0) (@val _)} FAILURE! Tactics applied: 7954 Original Proof: [by move=> x Px; rewrite /= val_insubd [P x]Px.] Proof search time: 0 min, 14 sec Results for lemma svalP: : forall u : sig P, P (sval u) FAILURE! Tactics applied: 7513 Original Proof: [by case.] Proof search time: 0 min, 10 sec Results for lemma eqbF_neg: b : (b == false) = ~~ b SUCCESS! Proof Found in EFSM: [by case b ] Tactics applied: 21 Original Proof: [by case: b.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma val_inj: : injective (@val sT) FAILURE! Tactics applied: 7990 Original Proof: [exact: pcan_inj valK.] Proof search time: 0 min, 13 sec Results for lemma insubF: x : P x = false -> insub x = None SUCCESS! Proof Found in EFSM: [by do 2!case;, case insubP => [u -> /negPf->] ] Tactics applied: 469 Original Proof: [by move/idP; case: insubP.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 0 sec Results for lemma predU1l: : x = y -> (x == y) || b SUCCESS! Proof Found in EFSM: [by case eqP] Tactics applied: 23 Original Proof: [by move->; rewrite eqxx.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Results for lemma inj_in_eq: : {in D &, injective f} -> {in D &, forall x y, (f x == f y) = (x == y)} FAILURE! Tactics applied: 7954 Original Proof: [by move=> inj_f x y Dx Dy; apply/eqP/eqP=> [|-> //]; exact: inj_f.] Proof search time: 0 min, 18 sec Results for lemma valP: (u : sT) : P (val u) FAILURE! Tactics applied: 7482 Original Proof: [by case/SubP: u => x Px; rewrite SubK.] Proof search time: 0 min, 8 sec Results for fold 7 Results for lemma vrefl: : forall x, P x -> x = x SUCCESS! Proof Found in EFSM: [by [] ] Tactics applied: 18 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma eq_refl: (T : eqType) (x : T) : x == x SUCCESS! Proof Found in EFSM: [by case eqP] Tactics applied: 27 Original Proof: [exact/eqP.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma opt_eqP: : Equality.axiom opt_eq FAILURE! Tactics applied: 5057 Original Proof: [case=> [x|] [y|] /=; by [constructor | apply: (iffP eqP) => [|[]] ->].] Proof search time: 0 min, 6 sec Results for lemma s2valP': u : Q (s2val u) SUCCESS! Proof Found in EFSM: [by case u ] Tactics applied: 30 Original Proof: [by case: u.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma contraFneq: b x y : (x = y -> b) -> b = false -> x != y SUCCESS! Proof Found in EFSM: [by move=> imp /negbT;, apply contraNN => /eqP ] Tactics applied: 899 Original Proof: [by move=> imp /negbT; apply: contraNneq.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 sec Results for lemma contra_neq: x1 y1 x2 y2 : (x2 = y2 -> x1 = y1) -> x1 != y1 -> x2 != y2 FAILURE! Tactics applied: 5034 Original Proof: [by move=> imp; apply: contraNneq => /imp->.] Proof search time: 0 min, 7 sec Results for lemma insubK: : ocancel insub (@val _) SUCCESS! Proof Found in EFSM: [by apply fsym => x;, case insubP ] Tactics applied: 398 Original Proof: [by move=> x; case: insubP.] Shorter Proof Found? no Proof reused from isSome_insub proof search time: 0 min, 0 sec Results for lemma predD1P: : reflect (x <> y /\ b) ((x != y) && b) FAILURE! Tactics applied: 4913 Original Proof: [by apply: (iffP andP)=> [] [] // /eqP.] Proof search time: 0 min, 4 sec Results for lemma invariant_inj: : injective h -> invariant f (h \o k) =1 invariant f k SUCCESS! Proof Found in EFSM: [move => x y;, exact inj_eq ] Tactics applied: 289 Original Proof: [move=> inj_h x; exact: (inj_eq inj_h).] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 0 sec Results for fold 8 Results for lemma eqb_negLR: b1 b2 : (~~ b1 == b2) = (b1 == ~~ b2) FAILURE! Tactics applied: 6054 Original Proof: [by case: b1; case: b2.] Proof search time: 0 min, 4 sec Results for lemma eqE: T x : eq_op x = Equality.op (Equality.class T) x SUCCESS! Proof Found in EFSM: [by [] ] Tactics applied: 16 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec 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: 21 Original Proof: [by case/andP.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma pred2P: : reflect (x = y \/ z = u) ((x == y) || (z == u)) FAILURE! Tactics applied: 6192 Original Proof: [by apply: (iffP orP) => [] [] /eqP; by [left | right].] Proof search time: 0 min, 4 sec Results for lemma val_eqE: (u v : sT) : (val u == val v) = (u == v) SUCCESS! Proof Found in EFSM: [by [] ] Tactics applied: 16 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma pair_eqE: : pair_eq = eq_op :> rel _ SUCCESS! Proof Found in EFSM: [by [] ] Tactics applied: 16 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec 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: 6324 Original Proof: [by move/can_in_inj; exact: inj_in_eq.] Proof search time: 0 min, 8 sec Results for lemma predU1r: : b -> (x == y) || b SUCCESS! Proof Found in EFSM: [by case eqP] Tactics applied: 24 Original Proof: [by move->; rewrite orbT.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec Results for lemma can_eq: : cancel f g -> forall x y, (f x == f y) = (x == y) FAILURE! Tactics applied: 6372 Original Proof: [move/can_inj; exact: inj_eq.] Proof search time: 0 min, 7 sec Results for fold 9 Results for lemma pred1E: : pred1 =2 eq_op SUCCESS! Proof Found in EFSM: [by move=> imp hyp;, apply /eqP/eqP=> [-> //]] Tactics applied: 733 Original Proof: [move=> x y; exact: eq_sym.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 sec Results for lemma contraTneq: b x y : (x = y -> ~~ b) -> b -> x != y FAILURE! Tactics applied: 3881 Original Proof: [by move=> imp; apply: contraTN => /eqP.] Proof search time: 0 min, 5 sec Results for lemma can2_eq: : cancel f g -> cancel g f -> forall x y, (f x == y) = (x == g y) FAILURE! Tactics applied: 4031 Original Proof: [by move=> fK gK x y; rewrite -{1}[y]gK; exact: can_eq.] Proof search time: 0 min, 6 sec Results for lemma contra_eqT: b x y : (~~ b -> x != y) -> x = y -> b FAILURE! Tactics applied: 3913 Original Proof: [by move=> imp /eqP; apply: contraLR.] Proof search time: 0 min, 5 sec Results for lemma val_eqP: : ev_ax sT val FAILURE! Tactics applied: 4069 Original Proof: [exact: inj_eqAxiom val_inj.] Proof search time: 0 min, 7 sec Results for lemma val_insubd: u0 x : val (insubd u0 x) = if P x then x else val u0 FAILURE! Tactics applied: 3762 Original Proof: [by rewrite /insubd; case: insubP => [u -> | /negPf->].] Proof search time: 0 min, 3 sec Results for lemma isSome_insub: : ([eta insub] : pred T) =1 P FAILURE! Tactics applied: 3793 Original Proof: [by apply: fsym => x; case: insubP => // /negPf.] Proof search time: 0 min, 5 sec Results for lemma bij_eq: : bijective f -> forall x y, (f x == f y) = (x == y) FAILURE! Tactics applied: 3912 Original Proof: [move/bij_inj; apply: inj_eq.] Proof search time: 0 min, 6 sec Results for lemma eqbE: : eqb = eq_op SUCCESS! Proof Found in EFSM: [by [] ] Tactics applied: 15 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for fold 10 Results for lemma insubN: x : ~~ P x -> insub x = None SUCCESS! Proof Found in EFSM: [by do 2!case;, case insubP => [u -> /negPf->] ] Tactics applied: 782 Original Proof: [by move/negPf/insubF.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 1 sec OVERALL RESULTS SUMMARY EFSMProver proved 29 out of 82 lemmas. Success rate of 35.36585365853659% There were 0 errors. 53 proof attempts exhausted the automaton On average, a proof was found after applying 222 tactics The longest proof consisted of 2 tactics There were 2 shorter proofs found Of the 53 failures, 0 of them used all 100000 tactics There were 22 reused proofs found There were 7 novel proofs found Of the 53 failures, the average number of tactics used was 4615On average, a proof was found after 0 min, 0 sec On average, a failed proof attempt took 0 min, 5 sec On average, any (success or failure) proof attempt took 0 min, 3 sec The longest time to find a proof was 0 min, 1 sec The shortest time to find a proof was 0 min, 0 sec There were 0 proofs containing repeated tactics There were 0 proofs that repeated states