Results for fold 1 Results for lemma eq_can: f' g' : cancel f f' -> f =1 g -> f' =1 g' -> cancel g g' FAILURE! Tactics applied: 38 Original Proof: [by move=> fK eqfg eqfg' x; rewrite -eqfg -eqfg'.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 36 Results for lemma inv_inj: : injective f FAILURE! Tactics applied: 38 Original Proof: [exact: can_inj Hf.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 36 Results for lemma bij_inj: : injective f FAILURE! Tactics applied: 38 Original Proof: [by case: bijf => g fK _; apply: can_inj fK.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 36 Results for lemma can_pcan: g : cancel g -> pcancel (fun y => Some (g y)) FAILURE! Tactics applied: 34 Original Proof: [by move=> fK x; congr (Some _).] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 34 Results for lemma inv_bij: : bijective f FAILURE! Tactics applied: 34 Original Proof: [by exists f.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 34 Results for lemma bij_can_sym: f' : cancel f' f <-> cancel f f' FAILURE! Tactics applied: 34 Original Proof: [split=> fK; first exact: inj_can_sym fK bij_inj. by case: bijf => h _ hK x; rewrite -[x]hK fK.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 34 Results for fold 2 Results for lemma bij_can_bij: : bijective f -> forall f', cancel f f' -> bijective f' FAILURE! Tactics applied: 114 Original Proof: [by move=> bijf; exists f; first by apply/(bij_can_sym bijf).] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 112 Results for lemma eq_bij: : bijective f -> forall g, f =1 g -> bijective g FAILURE! Tactics applied: 114 Original Proof: [by case=> f' fK f'K g eqfg; exists f'; eapply eq_can; eauto.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 112 Results for lemma fsym: f g : eqfun f g -> eqfun g f SUCCESS! Proof Found in EFSM: by move=> fK fK'; Tactics applied: 18 Original Proof: [by move=> eq_fg x.] 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: 17 Results for lemma pcan_pcomp: f' h' : pcancel f f' -> pcancel h h' -> pcancel (f \o h) (pcomp h' f') FAILURE! Tactics applied: 114 Original Proof: [by move=> fK hK x; rewrite /pcomp fK /= hK.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 112 Results for lemma can_comp: f' h' : cancel f f' -> cancel h h' -> cancel (f \o h) (h' \o f') FAILURE! Tactics applied: 114 Original Proof: [by move=> fK hK x; rewrite /= fK hK.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 112 Results for lemma can_inj: g : cancel g -> injective FAILURE! Tactics applied: 111 Original Proof: [by move/can_pcan; exact: pcan_inj.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 109 Results for fold 3 Results for lemma unitE: : all_equal_to tt FAILURE! Tactics applied: 67 Original Proof: [by case.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 67 Results for lemma inj_id: : injective (@id A) SUCCESS! Proof Found in EFSM: by []. Tactics applied: 6 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: 5 Results for lemma canRL: g x y : cancel g -> f x = y -> x = g y FAILURE! Tactics applied: 67 Original Proof: [by move=> fK <-.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 67 Results for lemma inj_can_sym: f' : cancel f f' -> injective f' -> cancel f' f FAILURE! Tactics applied: 67 Original Proof: [move=> fK injf' x; exact: injf'.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 67 Results for lemma canLR: g x y : cancel g -> x = f y -> g x = y FAILURE! Tactics applied: 67 Original Proof: [by move=> fK ->.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 67 Results for lemma esymK: T x y : cancel (@esym T x y) (@esym T y x) FAILURE! Tactics applied: 67 Original Proof: [by case: y /.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 67 Results for fold 4 Results for lemma bij_can_eq: f' f'' : cancel f f' -> cancel f f'' -> f' =1 f'' FAILURE! Tactics applied: 171 Original Proof: [by move=> fK fK'; apply: (inj_can_eq _ bij_inj); apply/bij_can_sym.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 169 Results for lemma Some_inj: {T} : injective (@Some T) FAILURE! Tactics applied: 171 Original Proof: [by move=> x y [].] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 169 Results for lemma rrefl: r : eqrel r r SUCCESS! Proof Found in EFSM: split => fK; Tactics applied: 1 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 Results for lemma bij_comp: : bijective f -> bijective h -> bijective (f \o h) FAILURE! Tactics applied: 57 Original Proof: [by move=> [f' fK f'K] [h' hK h'K]; exists (h' \o f'); apply: can_comp; auto.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 57 Results for lemma eq_comp: f f' g g' : f =1 f' -> g =1 g' -> comp f g =1 comp f' g' FAILURE! Tactics applied: 171 Original Proof: [by move=> eq_ff' eq_gg' x; rewrite /= eq_gg' eq_ff'.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 169 Results for lemma pcan_inj: g : pcancel g -> injective FAILURE! Tactics applied: 171 Original Proof: [by move=> fK x y /(congr1 g); rewrite !fK => [[]].] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 169 Results for fold 5 Results for lemma frefl: f : eqfun f f SUCCESS! Proof Found in EFSM: split => fK; Tactics applied: 1 Original Proof: [by [].] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 Results for lemma inj_comp: : injective f -> injective h -> injective (f \o h) FAILURE! Tactics applied: 63 Original Proof: [move=> injf injh x y /injf; exact: injh.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 61 Results for lemma eq_inj: : injective f -> f =1 g -> injective g FAILURE! Tactics applied: 63 Original Proof: [by move=> injf eqfg x y; rewrite -2!eqfg; exact: injf.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 61 Results for lemma inj_can_eq: f' : cancel f f' -> injective f' -> cancel g f' -> f =1 g FAILURE! Tactics applied: 61 Original Proof: [by move=> fK injf' gK x; apply: injf'; rewrite fK.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 59 Results for lemma ftrans: f g h : eqfun f g -> eqfun g h -> eqfun f h FAILURE! Tactics applied: 63 Original Proof: [by move=> eq_fg eq_gh x; rewrite eq_fg.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 2 Number of failed tactic applications: 61 Results for lemma etrans_id: T x y (eqxy : x = y :> T) : etrans (erefl x) eqxy = eqxy FAILURE! Tactics applied: 61 Original Proof: [by case: y / eqxy.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 61 OVERALL RESULTS SUMMARY EFSMProver proved 4 out of 30 lemmas. Success rate of 13.333333333333334% There were 0 errors. 26 proof attempts exhausted the automaton On average, a proof was found after applying 6 tactics The longest proof consisted of 1 tactics There were 0 shorter proofs found Of the 26 failures, 0 of them used all 10000 tactics There were 4 reused proofs found There were 0 novel proofs found Of the 26 failures, the average number of tactics used was 83 On average, a proof was found after 0 min, 0 sec On average, a failed proof attempt took 0 min, 0 sec On average, any (success or failure) proof attempt took 0 min, 0 sec The longest time to find a proof was 0 min, 0 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