Results for fold 1 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: 562 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, 2 sec 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: 500 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, 3 sec Results for lemma cardinal_spec: : forall (s : t) {Hs : Ok s}, cardinal s = length (elements s) SUCCESS! Proof Found in EFSM: [reflexivity ] Tactics applied: 14 Original Proof: [auto.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for fold 2 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: 361 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, 2 sec 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: 16 Original Proof: [unfold elements; intuition.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec 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: 502 Original Proof: [induction s; simpl in *; unfold flip; intros; auto; inv. intuition; inv. rewrite IHs, add_spec, InA_cons; intuition.] Proof search time: 0 min, 2 sec Results for fold 3 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: 483 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: 0 min, 2 sec 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: [auto ] Tactics applied: 12 Original Proof: [reflexivity.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma empty_ok: : Ok empty SUCCESS! Proof Found in EFSM: [unfold Empty, empty;, intuition ] Tactics applied: 19 Original Proof: [unfold empty; constructors.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 0 sec Results for fold 4 Results for lemma singleton_spec: : forall x y : elt, In y (singleton x) <-> X.eq y x FAILURE! Tactics applied: 197 Original Proof: [unfold singleton; simpl; split; intros. inv; auto. left; auto.] Proof search time: 0 min, 0 sec 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: 564 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: 0 min, 4 sec Results for lemma singleton_ok: : forall x : elt, Ok (singleton x) FAILURE! Tactics applied: 197 Original Proof: [unfold singleton; simpl; constructors; auto. intro; inv.] Proof search time: 0 min, 0 sec Results for fold 5 Results for lemma isok_iff: : forall l, Ok l <-> isok l = true FAILURE! Tactics applied: 213 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.] Proof search time: 0 min, 0 sec Results for lemma is_empty_spec: : forall s : t, is_empty s = true <-> Empty s FAILURE! Tactics applied: 553 Original Proof: [unfold Empty; destruct s; simpl; split; intros; auto. intro; inv. discriminate. elim (H e); auto.] Proof search time: 0 min, 1 sec 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 SUCCESS! Proof Found in EFSM: [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 ] Tactics applied: 1515 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.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 23 sec Results for fold 6 Results for lemma filter_spec': : forall s x f, In x (filter f s) -> In x s FAILURE! Tactics applied: 505 Original Proof: [induction s; simpl. intuition; inv. intros; destruct (f a); inv; intuition; right; eauto.] Proof search time: 0 min, 2 sec Results for lemma elements_spec2w: : forall (s : t) {Hs : Ok s}, NoDup (elements s) SUCCESS! Proof Found in EFSM: [auto ] Tactics applied: 16 Original Proof: [unfold elements; auto.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 0 sec 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: 405 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, 2 sec Results for fold 7 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 SUCCESS! Proof Found in EFSM: [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 ] Tactics applied: 1516 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.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 21 sec 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) SUCCESS! Proof Found in EFSM: [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 ] Tactics applied: 2560 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.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 38 sec Results for lemma empty_spec: : Empty empty FAILURE! Tactics applied: 325 Original Proof: [unfold Empty, empty; red; intros; inv.] Proof search time: 0 min, 0 sec Results for fold 8 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: 1010 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, 16 sec Results for lemma In_compat: : Proper (X.eq==>eq==>iff) In FAILURE! Tactics applied: 283 Original Proof: [repeat red; intros. subst. rewrite H; auto.] Proof search time: 0 min, 0 sec Results for lemma partition_spec1: : forall (s : t) (f : elt -> bool), Proper (X.eq==>eq) f -> Equal (fst (partition f s)) (filter f s) SUCCESS! Proof Found in EFSM: [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 ] Tactics applied: 2249 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.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 35 sec 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: 100000 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: 1 min, 9 sec 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: 100000 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: 1 min, 10 sec Results for lemma mem_spec: : forall s x `{Ok s}, mem x s = true <-> In x s FAILURE! Tactics applied: 100000 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: 1 min, 9 sec Results for fold 10 OVERALL RESULTS SUMMARY EFSMProver proved 9 out of 27 lemmas. Success rate of 33.33333333333333% There were 0 errors. 18 proof attempts exhausted the automaton On average, a proof was found after applying 879 tactics The longest proof consisted of 18 tactics There were 2 shorter proofs found Of the 18 failures, 3 of them used all 100000 tactics There were 4 reused proofs found There were 5 novel proofs found Of the 18 failures, the average number of tactics used was 17036 On average, a proof was found after 0 min, 13 sec On average, a failed proof attempt took 0 min, 14 sec On average, any (success or failure) proof attempt took 0 min, 13 sec The longest time to find a proof was 0 min, 38 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