Results for fold 1 Results for lemma cardinal_spec: : forall (s : t) {Hs : Ok s}, cardinal s = length (elements s) SUCCESS! Proof Found in EFSM: reflexivity. Tactics applied: 25 Original Proof: [auto.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Number of successful tactic applications: 3 Number of failed tactic applications: 22 Results for fold 2 Results for lemma diff_spec: : forall (s s' : t) (x : elt) {Hs : Ok s} {Hs' : Ok s'}, In x (diff s s') <-> In x s /\ ~In x s' FAILURE! Tactics applied: 10000 Original Proof: [unfold diff; intros s s'; revert s. induction s'; simpl; unfold flip. intuition; inv. intros. inv. rewrite IHs', remove_spec, InA_cons; intuition.] Proof search time: 0 min, 38 sec Number of successful tactic applications: 4497 Number of failed tactic applications: 5504 Results for fold 3 Results for lemma exists_spec: : forall (s : t) (f : elt -> bool), Proper (X.eq==>eq) f -> (exists_ f s = true <-> Exists (fun x => f x = true) s) FAILURE! Tactics applied: 10000 Original Proof: [unfold Exists; induction s; simpl. split; [discriminate| intros (x & Hx & _); inv]. intros. destruct (f a) eqn:F. split; auto. exists a; auto. rewrite IHs; firstorder. inv. setoid_replace a with x in F; auto; congruence. exists x; auto.] Proof search time: 1 min, 9 sec Number of successful tactic applications: 4786 Number of failed tactic applications: 5215 Results for fold 4 Results for lemma In_compat: : Proper (X.eq==>eq==>iff) In FAILURE! Tactics applied: 30 Original Proof: [repeat red; intros. subst. rewrite H; auto.] Proof search time: 0 min, 1 sec Number of successful tactic applications: 0 Number of failed tactic applications: 30 Results for fold 5 Results for lemma singleton_ok: : forall x : elt, Ok (singleton x) SUCCESS! Proof Found in EFSM: unfold singleton; intuition. Tactics applied: 34 Original Proof: [unfold singleton; simpl; constructors; auto. intro; inv.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 1 sec Number of successful tactic applications: 6 Number of failed tactic applications: 28 Results for fold 6 Results for lemma empty_ok: : Ok empty SUCCESS! Proof Found in EFSM: unfold Empty, empty; auto. Tactics applied: 50 Original Proof: [unfold empty; constructors.] 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: 41 Results for fold 7 Results for lemma equal_spec: : forall (s s' : t) {Hs : Ok s} {Hs' : Ok s'}, equal s s' = true <-> Equal s s' FAILURE! Tactics applied: 10000 Original Proof: [unfold Equal, equal; intros. rewrite andb_true_iff, !subset_spec. unfold Subset; intuition. rewrite <- H; auto. rewrite H; auto.] Proof search time: 0 min, 36 sec Number of successful tactic applications: 4470 Number of failed tactic applications: 5531 Results for fold 8 Results for lemma elements_spec2w: : forall (s : t) {Hs : Ok s}, NoDup (elements s) SUCCESS! Proof Found in EFSM: auto ; Tactics applied: 31 Original Proof: [unfold elements; auto.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 7 Number of failed tactic applications: 24 Results for fold 9 Results for lemma add_spec: : forall (s : t) (x y : elt) {Hs : Ok s}, In y (add x s) <-> X.eq y x \/ In y s FAILURE! Tactics applied: 10000 Original Proof: [induction s; simpl; intros. intuition; inv; auto. destruct X.eq_dec; inv; rewrite InA_cons, ?IHs; intuition. left; eauto. inv; auto.] Proof search time: 0 min, 47 sec Number of successful tactic applications: 4695 Number of failed tactic applications: 5306 Results for fold 10 Results for lemma union_spec: : forall (s s' : t) (x : elt) {Hs : Ok s} {Hs' : Ok s'}, In x (union s s') <-> In x s \/ In x s' FAILURE! Tactics applied: 10000 Original Proof: [induction s; simpl in *; unfold flip; intros; auto; inv. intuition; inv. rewrite IHs, add_spec, InA_cons; intuition.] Proof search time: 1 min, 31 sec Number of successful tactic applications: 4126 Number of failed tactic applications: 5875 Results for fold 11 Results for lemma filter_spec': : forall s x f, In x (filter f s) -> In x s FAILURE! Tactics applied: 10000 Original Proof: [induction s; simpl. intuition; inv. intros; destruct (f a); inv; intuition; right; eauto.] Proof search time: 0 min, 32 sec Number of successful tactic applications: 5036 Number of failed tactic applications: 4965 Results for fold 12 Results for lemma fold_spec: : forall (s : t) (A : Type) (i : A) (f : elt -> A -> A), fold f s i = fold_left (flip f) (elements s) i SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 30 Original Proof: [reflexivity.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 9 Number of failed tactic applications: 21 Results for fold 13 Results for lemma empty_spec: : Empty empty SUCCESS! Proof Found in EFSM: unfold empty; intros s s'; inv ; Tactics applied: 794 Original Proof: [unfold Empty, empty; red; intros; inv.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 2 sec Number of successful tactic applications: 321 Number of failed tactic applications: 473 Results for fold 14 Results for lemma inter_spec: : forall (s s' : t) (x : elt) {Hs : Ok s} {Hs' : Ok s'}, In x (inter s s') <-> In x s /\ In x s' FAILURE! Tactics applied: 10000 Original Proof: [unfold inter, fold, flip; intros. set (acc := nil (A:=elt)) in *. assert (Hacc : Ok acc) by constructors. assert (IFF : (In x s /\ In x s') <-> (In x s /\ In x s') \/ In x acc). intuition; unfold acc in *; inv. rewrite IFF; clear IFF. clearbody acc. revert acc Hacc x s' Hs Hs'. induction s; simpl; intros. intuition; inv. inv. case_eq (mem a s'); intros Hm. rewrite IHs, add_spec, InA_cons; intuition. rewrite mem_spec in Hm; auto. left; split; auto. rewrite H1; auto. rewrite IHs, InA_cons; intuition. rewrite H2, <- mem_spec in H3; auto. congruence.] Proof search time: 1 min, 21 sec Number of successful tactic applications: 3713 Number of failed tactic applications: 6288 Results for fold 15 Results for lemma remove_spec: : forall (s : t) (x y : elt) {Hs : Ok s}, In y (remove x s) <-> In y s /\ ~X.eq y x FAILURE! Tactics applied: 10000 Original Proof: [induction s; simpl; intros. intuition; inv; auto. destruct X.eq_dec; inv; rewrite !InA_cons, ?IHs; intuition. elim H. setoid_replace a with y; eauto. elim H3. setoid_replace x with y; eauto. elim n. eauto.] Proof search time: 0 min, 53 sec Number of successful tactic applications: 5125 Number of failed tactic applications: 4876 Results for fold 16 Results for lemma for_all_spec: : forall (s : t) (f : elt -> bool), Proper (X.eq==>eq) f -> (for_all f s = true <-> For_all (fun x => f x = true) s) FAILURE! Tactics applied: 10000 Original Proof: [unfold For_all; induction s; simpl. intuition. inv. intros; inv. destruct (f a) eqn:F. rewrite IHs; intuition. inv; auto. setoid_replace x with a; auto. split; intros H'; try discriminate. intros. rewrite <- F, <- (H' a); auto.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 4646 Number of failed tactic applications: 5355 Results for fold 17 Results for lemma subset_spec: : forall (s s' : t) {Hs : Ok s} {Hs' : Ok s'}, subset s s' = true <-> Subset s s' FAILURE! Tactics applied: 10000 Original Proof: [unfold subset, Subset; intros. rewrite is_empty_spec. unfold Empty; intros. intuition. specialize (H a). rewrite diff_spec in H; intuition. rewrite <- (mem_spec a) in H |- *. destruct (mem a s'); intuition. rewrite diff_spec in H0; intuition.] Proof search time: 0 min, 39 sec Number of successful tactic applications: 4460 Number of failed tactic applications: 5541 Results for fold 18 Results for lemma elements_spec1: : forall (s : t) (x : elt), In x (elements s) <-> In x s SUCCESS! Proof Found in EFSM: reflexivity. Tactics applied: 27 Original Proof: [unfold elements; intuition.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 7 Number of failed tactic applications: 20 Results for fold 19 Results for lemma singleton_spec: : forall x y : elt, In y (singleton x) <-> X.eq y x FAILURE! Tactics applied: 10000 Original Proof: [unfold singleton; simpl; split; intros. inv; auto. left; auto.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 3298 Number of failed tactic applications: 6703 Results for fold 20 Results for lemma isok_iff: : forall l, Ok l <-> isok l = true SUCCESS! Proof Found in EFSM: reflexivity. Tactics applied: 5 Original Proof: [induction l. intuition. simpl. rewrite andb_true_iff. rewrite negb_true_iff. rewrite <- IHl. split; intros H. inv. split; auto. apply not_true_is_false. rewrite mem_spec; auto. destruct H; constructors; auto. rewrite <- mem_spec; auto; congruence.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 3 Number of failed tactic applications: 2 Results for fold 21 Results for lemma partition_spec2: : forall (s : t) (f : elt -> bool), Proper (X.eq==>eq) f -> Equal (snd (partition f s)) (filter (fun x => negb (f x)) s) FAILURE! Tactics applied: 10000 Original Proof: [simple induction s; simpl; auto; unfold Equal. firstorder. intros x l Hrec f Hf. generalize (Hrec f Hf); clear Hrec. case (partition f l); intros s1 s2; simpl; intros. case (f x); simpl; firstorder; inversion H0; intros; firstorder.] Proof search time: 0 min, 45 sec Number of successful tactic applications: 5917 Number of failed tactic applications: 4084 Results for fold 22 Results for lemma partition_ok1': : forall (s : t) {Hs : Ok s} (f : elt -> bool)(x:elt), In x (fst (partition f s)) -> In x s FAILURE! Tactics applied: 10000 Original Proof: [induction s; simpl; auto; intros. inv. generalize (IHs H1 f x). destruct (f a); destruct (partition f s); simpl in *; auto. inversion_clear H; auto.] Proof search time: 0 min, 43 sec Number of successful tactic applications: 5347 Number of failed tactic applications: 4654 Results for fold 23 Results for lemma partition_ok2': : forall (s : t) {Hs : Ok s} (f : elt -> bool)(x:elt), In x (snd (partition f s)) -> In x s FAILURE! Tactics applied: 10000 Original Proof: [induction s; simpl; auto; intros. inv. generalize (IHs H1 f x). destruct (f a); destruct (partition f s); simpl in *; auto. inversion_clear H; auto.] Proof search time: 0 min, 42 sec Number of successful tactic applications: 5644 Number of failed tactic applications: 4357 Results for fold 24 Results for lemma partition_spec1: : forall (s : t) (f : elt -> bool), Proper (X.eq==>eq) f -> Equal (fst (partition f s)) (filter f s) FAILURE! Tactics applied: 10000 Original Proof: [simple induction s; simpl; auto; unfold Equal. firstorder. intros x l Hrec f Hf. generalize (Hrec f Hf); clear Hrec. case (partition f l); intros s1 s2; simpl; intros. case (f x); simpl; firstorder; inversion H0; intros; firstorder.] Proof search time: 0 min, 34 sec Number of successful tactic applications: 5106 Number of failed tactic applications: 4895 Results for fold 25 Results for lemma is_empty_spec: : forall s : t, is_empty s = true <-> Empty s FAILURE! Tactics applied: 10000 Original Proof: [unfold Empty; destruct s; simpl; split; intros; auto. intro; inv. discriminate. elim (H e); auto.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 4370 Number of failed tactic applications: 5631 Results for fold 26 Results for lemma filter_spec: : forall (s : t) (x : elt) (f : elt -> bool), Proper (X.eq==>eq) f -> (In x (filter f s) <-> In x s /\ f x = true) FAILURE! Tactics applied: 10000 Original Proof: [induction s; simpl. intuition; inv. intros. destruct (f a) eqn:E; rewrite ?InA_cons, IHs; intuition. setoid_replace x with a; auto. setoid_replace a with x in E; auto. congruence.] Proof search time: 0 min, 58 sec Number of successful tactic applications: 5678 Number of failed tactic applications: 4323 Results for fold 27 Results for lemma mem_spec: : forall s x `{Ok s}, mem x s = true <-> In x s FAILURE! Tactics applied: 10000 Original Proof: [induction s; intros. split; intros; inv. discriminate. simpl; destruct (X.eq_dec x a); split; intros; inv; auto. right; rewrite <- IHs; auto. rewrite IHs; auto.] Proof search time: 0 min, 56 sec Number of successful tactic applications: 3589 Number of failed tactic applications: 6412 OVERALL RESULTS SUMMARY EFSMProver proved 8 out of 27 lemmas. Success rate of 29.629629629629626% There were 0 errors. 19 proof attempts exhausted the automaton On average, a proof was found after applying 124 tactics The longest proof consisted of 3 tactics There were 5 shorter proofs found Of the 19 failures, 18 of them used all 10000 tactics There were 5 reused proofs found There were 3 novel proofs found Of the 19 failures, the average number of tactics used was 9475 On average, a proof was found after 0 min, 1 sec On average, a failed proof attempt took 0 min, 44 sec On average, any (success or failure) proof attempt took 0 min, 32 sec The longest time to find a proof was 0 min, 3 sec The shortest time to find a proof was 0 min, 1 sec There were 0 proofs containing repeated tactics There were 0 proofs that repeated states