Results for fold 1 Results for lemma ltn_code: s : all (fun j => j < code s) s FAILURE! Tactics applied: 59 Original Proof: [elim: s => //= i s IHs; rewrite -[_.+1]muln1 leq_mul 1?ltn_expl //=. apply: sub_all IHs => j /leqW lejs; rewrite -[j.+1]mul1n leq_mul ?expn_gt0 //. by rewrite ltnS -[j]mul1n -mul2n leq_mul.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 59 Results for fold 2 Results for lemma pickleK: : @pcancel nat T pickle unpickle FAILURE! Tactics applied: 200 Original Proof: [exact: Countable.pickleK.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 9 Number of failed tactic applications: 191 Results for fold 3 Results for lemma sig2_eqW: (vT : eqType) (P : pred T) (lhs rhs : T -> vT) : (exists2 x, P x & lhs x = rhs x) -> {x | P x & lhs x = rhs x} FAILURE! Tactics applied: 152 Original Proof: [move=> exP; suffices [x Px /eqP Ex]: {x | P x & lhs x == rhs x} by exists x. by apply: sig2W; have [x Px /eqP Ex] := exP; exists x.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 17 Number of failed tactic applications: 135 Results for fold 4 Results for lemma codeK: : pcancel encode decode FAILURE! Tactics applied: 385 Original Proof: [move=> t; rewrite /decode; set fs := (_, _). suffices ->: foldr decode_step fs (encode t) = (t :: fs.1, fs.2) by []. elim: t => //= n f IHt in (fs) *; elim: f IHt => //= t f IHf []. by rewrite rcons_cat foldr_cat => -> /= /IHf[-> -> ->].] Proof search time: 0 min, 0 sec Number of successful tactic applications: 6 Number of failed tactic applications: 379 Results for fold 5 Results for lemma pcan_pickleK: sT f f' : @pcancel T sT f f' -> pcancel (pickle \o f) (pcomp f' unpickle) FAILURE! Tactics applied: 573 Original Proof: [by move=> fK x; rewrite /pcomp pickleK /= fK.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 34 Number of failed tactic applications: 539 Results for fold 6 Results for lemma sig2W: P Q : (exists2 x, P x & Q x) -> {x | P x & Q x} FAILURE! Tactics applied: 163 Original Proof: [move=> exPQ; have [|x /andP[]] := @sigW (predI P Q); last by exists x. by have [x Px Qx] := exPQ; exists x; exact/andP.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 13 Number of failed tactic applications: 150 Results for fold 7 Results for lemma sig_eqW: (vT : eqType) (lhs rhs : T -> vT) : (exists x, lhs x = rhs x) -> {x | lhs x = rhs x} FAILURE! Tactics applied: 151 Original Proof: [move=> exP; suffices [x /eqP Ex]: {x | lhs x == rhs x} by exists x. by apply: sigW; have [x /eqP Ex] := exP; exists x.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 17 Number of failed tactic applications: 134 Results for fold 8 Results for lemma pickle_invK: : ocancel pickle_inv pickle FAILURE! Tactics applied: 147 Original Proof: [by rewrite /pickle_inv => n; case def_x: (unpickle n) => //= [x]; case: eqP.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 9 Number of failed tactic applications: 138 Results for fold 9 Results for lemma pickleK_inv: : pcancel pickle pickle_inv FAILURE! Tactics applied: 155 Original Proof: [by rewrite /pickle_inv => x; rewrite pickleK /= eqxx.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 9 Number of failed tactic applications: 146 Results for fold 10 Results for lemma decodeK: : cancel decode code FAILURE! Tactics applied: 1168 Original Proof: [have m2s: forall n, n.*2 - n = n by move=> n; rewrite -addnn addnK. case=> //= n; rewrite -[n.+1]mul1n -(expn0 2) -{3}[n]m2s. elim: n {2 4}n {1 3}0 => [|q IHq] [|[|r]] v //=; rewrite {}IHq ?mul1n ?m2s //. by rewrite expnSr -mulnA mul2n.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 24 Number of failed tactic applications: 1144 Results for fold 11 Results for lemma chooseP: P x0 : P x0 -> P (choose P x0) FAILURE! Tactics applied: 175 Original Proof: [by move=> Px0; rewrite /choose insubT xchooseP.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 17 Number of failed tactic applications: 158 Results for fold 12 Results for lemma pickle_seqK: : pcancel pickle_seq unpickle_seq FAILURE! Tactics applied: 408 Original Proof: [by move=> s; rewrite /unpickle_seq CodeSeq.codeK (map_pK pickleK).] Proof search time: 0 min, 0 sec Number of successful tactic applications: 11 Number of failed tactic applications: 397 Results for fold 13 Results for lemma opair_of_sumK: : pcancel opair_of_sum sum_of_opair SUCCESS! Proof Found in EFSM: elim => //= v s IHs; Tactics applied: 27 Original Proof: [by case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 9 Number of failed tactic applications: 18 Results for fold 14 Results for lemma gtn_decode: n : all (ltn^~ n) (decode n) FAILURE! Tactics applied: 56 Original Proof: [by rewrite -{1}[n]decodeK ltn_code.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 56 Results for fold 15 Results for lemma eq_choose: P Q : P =1 Q -> choose P =1 choose Q FAILURE! Tactics applied: 191 Original Proof: [rewrite /choose => eqPQ x0. do [case: insubP; rewrite eqPQ] => [[x Px] Qx0 _| ?]; last by rewrite insubN. by rewrite insubT; exact: eq_xchoose.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 33 Number of failed tactic applications: 158 Results for fold 16 Results for lemma seq_of_optK: : cancel seq_of_opt ohead SUCCESS! Proof Found in EFSM: elim => //= v s IHs; Tactics applied: 38 Original Proof: [by case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 9 Number of failed tactic applications: 29 Results for fold 17 Results for lemma xchooseP: P exP : P (@xchoose P exP) FAILURE! Tactics applied: 60 Original Proof: [by rewrite /xchoose; case: (xchoose_subproof exP) => x /= /correct.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 0 Number of failed tactic applications: 60 Results for fold 18 Results for lemma bool_of_unitK: : cancel (fun _ => true) (fun _ => tt) SUCCESS! Proof Found in EFSM: by case. Tactics applied: 4 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: 3 Results for fold 19 Results for lemma eq_xchoose: P Q exP exQ : P =1 Q -> @xchoose P exP = @xchoose Q exQ FAILURE! Tactics applied: 185 Original Proof: [rewrite /xchoose => eqPQ. case: (xchoose_subproof exP) => x; case: (xchoose_subproof exQ) => y /=. case: ex_minnP => n; case: ex_minnP => m. rewrite -(extensional eqPQ) {1}(extensional eqPQ). move=> Qm minPm Pn minQn; suffices /eqP->: m == n by move=> -> []. by rewrite eqn_leq minQn ?minPm.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 14 Number of failed tactic applications: 171 Results for fold 20 Results for lemma pickle_taggedK: : pcancel pickle_tagged unpickle_tagged FAILURE! Tactics applied: 292 Original Proof: [by case=> i x; rewrite /unpickle_tagged CodeSeq.codeK /= pickleK /= pickleK.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 11 Number of failed tactic applications: 281 Results for fold 21 Results for lemma sigW: P : (exists x, P x) -> {x | P x} FAILURE! Tactics applied: 971 Original Proof: [by move=> exP; exists (xchoose exP); exact: xchooseP.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 19 Number of failed tactic applications: 952 Results for fold 22 Results for lemma tag_of_pairK: : cancel tag_of_pair pair_of_tag SUCCESS! Proof Found in EFSM: elim => //= v s IHs; Tactics applied: 52 Original Proof: [by case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 9 Number of failed tactic applications: 43 Results for fold 23 Results for lemma correct: P n x : find P n = Some x -> P x FAILURE! Tactics applied: 329 Original Proof: [by case: T => _ [_ []] //= in P n x *.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 8 Number of failed tactic applications: 321 Results for fold 24 Results for lemma complete: P : (exists x, P x) -> (exists n, find P n) FAILURE! Tactics applied: 423 Original Proof: [by case: T => _ [_ []] //= in P *.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 12 Number of failed tactic applications: 411 Results for fold 25 Results for lemma choose_id: P x0 y0 : P x0 -> P y0 -> choose P x0 = choose P y0 FAILURE! Tactics applied: 152 Original Proof: [by move=> Px0 Py0; rewrite /choose !insubT /=; exact: eq_xchoose.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 17 Number of failed tactic applications: 135 Results for fold 26 Results for lemma pair_of_tagK: : cancel pair_of_tag tag_of_pair SUCCESS! Proof Found in EFSM: elim => //= v s IHs; Tactics applied: 17 Original Proof: [by case.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Number of successful tactic applications: 9 Number of failed tactic applications: 8 Results for fold 27 Results for lemma nat_pickleK: : pcancel id (@Some nat) SUCCESS! Proof Found in EFSM: elim => //= v s IHs; Tactics applied: 8 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: 7 Results for fold 28 Results for lemma codeK: : cancel code decode ERROR! Error: The reference code was not found in the current environment. Original Proof: [move=> t; rewrite /decode; set fs := (_, _). suffices ->: foldr decode_step fs (encode t) = (t :: fs.1, fs.2) by []. elim: t => //= n f IHt in (fs) *; elim: f IHt => //= t f IHf []. by rewrite rcons_cat foldr_cat => -> /= /IHf[-> -> ->].] Proof effort time: 0 min, 0 sec Results for fold 29 Results for lemma PcanChoiceMixin: f' : pcancel f f' -> choiceMixin sT FAILURE! Tactics applied: 812 Original Proof: [move=> fK; pose liftP sP := [pred x | oapp sP false (f' x)]. pose sf sP := [fun n => obind f' (find (liftP sP) n)]. exists sf => [sP n x | sP [y sPy] | sP sQ eqPQ n] /=. - by case Df: (find _ n) => //= [?] Dx; have:= correct Df; rewrite /= Dx. - have [|n Pn] := @complete T (liftP sP); first by exists (f y); rewrite /= fK. exists n; case Df: (find _ n) Pn => //= [x] _. by have:= correct Df => /=; case: (f' x). by congr (obind _ _); apply: extensional => x /=; case: (f' x) => /=.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 13 Number of failed tactic applications: 799 Results for fold 30 Results for lemma extensional: P Q : P =1 Q -> find P =1 find Q FAILURE! Tactics applied: 236 Original Proof: [by case: T => _ [_ []] //= in P Q *.] Proof search time: 0 min, 0 sec Number of successful tactic applications: 8 Number of failed tactic applications: 228 OVERALL RESULTS SUMMARY EFSMProver proved 6 out of 30 lemmas. Success rate of 20.0% There were 0 errors. 23 proof attempts exhausted the automaton On average, a proof was found after applying 24 tactics The longest proof consisted of 1 tactics There were 0 shorter proofs found Of the 23 failures, 0 of them used all 10000 tactics There were 6 reused proofs found There were 0 novel proofs found Of the 23 failures, the average number of tactics used was 323 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