Results for fold 1 Results for lemma singleton_equal_add: : equal (singleton x) (add x empty)=true SUCCESS! Proof Found in EFSM: auto with set. Tactics applied: 118 Original Proof: [rewrite (singleton_equal_add x); auto with set.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 4 sec Number of successful tactic applications: 17 Number of failed tactic applications: 101 Results for fold 2 Results for lemma union_equal_2: : equal s' s''=true-> equal (union s s') (union s s'')=true SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 5 Original Proof: [auto with set.] 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: 2 Results for fold 3 Results for lemma remove_add: : mem x s=false -> equal (remove x (add x s)) s=true FAILURE! Tactics applied: 10000 Original Proof: [intros; apply equal_1; apply remove_add; auto. rewrite not_mem_iff; auto.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 2179 Number of failed tactic applications: 7822 Results for fold 4 Results for lemma mem_3: : ~In x s -> mem x s=false SUCCESS! Proof Found in EFSM: intros ; apply bool_1; intuition. Tactics applied: 3650 Original Proof: [intros; rewrite <- not_mem_iff; auto.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 7 sec Number of successful tactic applications: 838 Number of failed tactic applications: 2812 Results for fold 5 Results for lemma subset_trans: : subset s s'=true -> subset s' s''=true -> subset s s''=true FAILURE! Tactics applied: 10000 Original Proof: [do 3 rewrite <- subset_iff; intros. apply subset_trans with s'; auto.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 2447 Number of failed tactic applications: 7554 Results for fold 6 Results for lemma singleton_mem_1: : mem x (singleton x)=true SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 32 Original Proof: [auto with set relations.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Number of successful tactic applications: 1 Number of failed tactic applications: 31 Results for fold 7 Results for lemma choose_mem_4: : choose empty=None FAILURE! Tactics applied: 10000 Original Proof: [generalize (@choose_1 empty). case (@choose empty);intros;auto. elim (@empty_1 e); auto.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 2294 Number of failed tactic applications: 7707 Results for fold 8 Results for lemma mem_4: : mem x s=false -> ~In x s FAILURE! Tactics applied: 10000 Original Proof: [intros; rewrite not_mem_iff; auto.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 2741 Number of failed tactic applications: 7260 Results for fold 9 Results for lemma is_empty_cardinal: : is_empty s = zerob (cardinal s) FAILURE! Tactics applied: 10000 Original Proof: [intros; apply bool_1; split; intros. rewrite MP.cardinal_1; simpl; auto with set. assert (cardinal s = 0) by (apply zerob_true_elim; auto). auto with set.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 2426 Number of failed tactic applications: 7575 Results for fold 10 Results for lemma remove_mem_2: : ~E.eq x y -> mem y (remove x s)=mem y s FAILURE! Tactics applied: 10000 Original Proof: [apply remove_neq_b.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 1913 Number of failed tactic applications: 8088 Results for fold 11 Results for lemma equal_trans: : equal s s'=true -> equal s' s''=true -> equal s s''=true FAILURE! Tactics applied: 10000 Original Proof: [intros; rewrite (equal_2 H); auto.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 2615 Number of failed tactic applications: 7386 Results for fold 12 Results for lemma union_inter_1: : equal (inter (union s s') s'') (union (inter s s'') (inter s' s''))=true SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 12 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 3 Number of failed tactic applications: 9 Results for fold 13 Results for lemma inter_subset_equal: : subset s s'=true -> equal (inter s s') s=true SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 12 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 7 Number of failed tactic applications: 5 Results for fold 14 Results for lemma union_inter_2: : equal (union (inter s s') s'') (inter (union s s'') (union s' s''))=true SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 42 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 7 Number of failed tactic applications: 35 Results for fold 15 Results for lemma exists_mem_2: : forall s, exists_ f s=false -> forall x, mem x s=true -> f x=false FAILURE! Tactics applied: 10000 Original Proof: [intros. rewrite for_all_exists in H; auto. rewrite negb_false_iff in H. rewrite <- negb_true_iff. apply for_all_mem_2 with (2:=H); auto.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 1864 Number of failed tactic applications: 8137 Results for fold 16 Results for lemma remove_fold_1: : mem x s=true -> eqA (f x (fold f (remove x s) i)) (fold f s i) FAILURE! Tactics applied: 10000 Original Proof: [intros; apply remove_fold_1 with (eqA:=eqA); auto with set.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 2157 Number of failed tactic applications: 7844 Results for fold 17 Results for lemma inter_subset_1: : subset (inter s s') s=true SUCCESS! Proof Found in EFSM: auto with set. Tactics applied: 67 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 4 Number of failed tactic applications: 63 Results for fold 18 Results for lemma exclusive_set: : forall s s' x, ~(In x s/\In x s') <-> mem x s && mem x s'=false FAILURE! Tactics applied: 10000 Original Proof: [intros; do 2 rewrite mem_iff. destruct (mem x s); destruct (mem x s'); intuition.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 3252 Number of failed tactic applications: 6749 Results for fold 19 Results for lemma remove_equal: : mem x s=false -> equal (remove x s) s=true FAILURE! Tactics applied: 10000 Original Proof: [intros; apply equal_1; apply remove_equal. rewrite not_mem_iff; auto.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 3036 Number of failed tactic applications: 6965 Results for fold 20 Results for lemma exists_mem_4: : forall s, exists_ f s=true -> {x:elt | (mem x s)=true /\ (f x)=true} FAILURE! Tactics applied: 10000 Original Proof: [intros. rewrite for_all_exists in H; auto. rewrite negb_true_iff in H. elim (@for_all_mem_4 (fun x =>negb (f x)) Comp' s);intros;auto. elim p;intros. exists x;split;auto. rewrite <-negb_false_iff; auto.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 1659 Number of failed tactic applications: 8342 Results for fold 21 Results for lemma inter_subset_3: : subset s'' s=true -> subset s'' s'=true -> subset s'' (inter s s')=true SUCCESS! Proof Found in EFSM: auto with *. Tactics applied: 46 Original Proof: [intros; apply subset_1; apply inter_subset_3; auto with set.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 15 Number of failed tactic applications: 31 Results for fold 22 Results for lemma fold_union: : (forall x, mem x s && mem x s'=false) -> eqA (fold f (union s s') i) (fold f s (fold f s' i)) FAILURE! Tactics applied: 10000 Original Proof: [intros; apply fold_union with (eqA:=eqA); auto. intros; rewrite exclusive_set; auto.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 2334 Number of failed tactic applications: 7667 Results for fold 23 Results for lemma remove_inter_singleton: : equal (remove x s) (diff s (singleton x))=true SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 10 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 4 sec Number of successful tactic applications: 1 Number of failed tactic applications: 9 Results for fold 24 Results for lemma inter_assoc: : equal (inter (inter s s') s'') (inter s (inter s' s''))=true SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 33 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 5 Number of failed tactic applications: 28 Results for fold 25 Results for lemma filter_mem: : forall s x, mem x (filter f s)=mem x s && f x FAILURE! Tactics applied: 10000 Original Proof: [intros; apply filter_b; auto.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 2078 Number of failed tactic applications: 7923 Results for fold 26 Results for lemma for_all_mem_2: : forall s, (for_all f s)=true -> forall x,(mem x s)=true -> (f x)=true FAILURE! Tactics applied: 10000 Original Proof: [intros. rewrite for_all_filter in H; auto. rewrite is_empty_equal_empty in H. generalize (equal_mem_2 _ _ H x). rewrite filter_b; auto. rewrite empty_mem. rewrite H0; simpl;intros. rewrite <- negb_false_iff; auto.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 2068 Number of failed tactic applications: 7933 Results for fold 27 Results for lemma remove_fold_2: : mem x s=false -> eqA (fold f (remove x s) i) (fold f s i) FAILURE! Tactics applied: 10000 Original Proof: [intros; apply remove_fold_2 with (eqA:=eqA); auto. rewrite not_mem_iff; auto.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 2297 Number of failed tactic applications: 7704 Results for fold 28 Results for lemma add_filter_1: : forall s s' x, f x=true -> (Add x s s') -> (Add x (filter f s) (filter f s')) FAILURE! Tactics applied: 10000 Original Proof: [unfold Add, MP.Add; intros. repeat rewrite filter_iff; auto. rewrite H0; clear H0. intuition. setoid_replace y with x; auto with relations.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 2471 Number of failed tactic applications: 7530 Results for fold 29 Results for lemma filter_add_1: : forall s x, f x = true -> filter f (add x s) [=] add x (filter f s) FAILURE! Tactics applied: 10000 Original Proof: [red; intros; set_iff; do 2 (rewrite filter_iff; auto); set_iff. intuition. rewrite <- H; apply Comp; auto with relations.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 3239 Number of failed tactic applications: 6762 Results for fold 30 Results for lemma singleton_mem_3: : mem y (singleton x)=true -> E.eq x y FAILURE! Tactics applied: 10000 Original Proof: [intros; apply singleton_1; auto with set.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 3051 Number of failed tactic applications: 6950 Results for fold 31 Results for lemma filter_add_2: : forall s x, f x = false -> filter f (add x s) [=] filter f s FAILURE! Tactics applied: 10000 Original Proof: [red; intros; do 2 (rewrite filter_iff; auto); set_iff. intuition. assert (f x = f a) by (apply Comp; auto). rewrite H in H1; rewrite H2 in H1; discriminate.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 2408 Number of failed tactic applications: 7593 Results for fold 32 Results for lemma empty_mem: : mem x empty=false FAILURE! Tactics applied: 10000 Original Proof: [rewrite <- not_mem_iff; auto with set.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 2472 Number of failed tactic applications: 7529 Results for fold 33 Results for lemma sum_plus: : forall f g, Proper (E.eq==>Logic.eq) f -> Proper (E.eq==>Logic.eq) g -> forall s, sum (fun x =>f x+g x) s = sum f s + sum g s FAILURE! Tactics applied: 10000 Original Proof: [unfold sum. intros f g Hf Hg. assert (fc : compat_opL (fun x:elt =>plus (f x))) by (repeat red; intros; rewrite Hf; auto). assert (ft : transposeL (fun x:elt =>plus (f x))) by (red; intros; omega). assert (gc : compat_opL (fun x:elt => plus (g x))) by (repeat red; intros; rewrite Hg; auto). assert (gt : transposeL (fun x:elt =>plus (g x))) by (red; intros; omega). assert (fgc : compat_opL (fun x:elt =>plus ((f x)+(g x)))) by (repeat red; intros; rewrite Hf,Hg; auto). assert (fgt : transposeL (fun x:elt=>plus ((f x)+(g x)))) by (red; intros; omega). intros s;pattern s; apply set_rec. intros. rewrite <- (fold_equal _ _ _ _ fc ft 0 _ _ H). rewrite <- (fold_equal _ _ _ _ gc gt 0 _ _ H). rewrite <- (fold_equal _ _ _ _ fgc fgt 0 _ _ H); auto. intros; do 3 (rewrite fold_add; auto with *). do 3 rewrite fold_empty;auto.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 2109 Number of failed tactic applications: 7892 Results for fold 34 Results for lemma inter_add_1: : mem x s'=true -> equal (inter (add x s) s') (add x (inter s s'))=true SUCCESS! Proof Found in EFSM: auto with *. Tactics applied: 50 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 8 Number of failed tactic applications: 42 Results for fold 35 Results for lemma union_subset_equal: : subset s s'=true -> equal (union s s') s'=true SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 44 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 14 Number of failed tactic applications: 30 Results for fold 36 Results for lemma diff_inter_empty: : equal (inter (diff s s') (inter s s')) empty=true SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 19 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 3 Number of failed tactic applications: 16 Results for fold 37 Results for lemma add_remove: : mem x s=true -> equal (add x (remove x s)) s=true FAILURE! Tactics applied: 10000 Original Proof: [intros; apply equal_1; apply add_remove; auto with set.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 2552 Number of failed tactic applications: 7449 Results for fold 38 Results for lemma union_filter: : forall f g, Proper (E.eq==>Logic.eq) f -> Proper (E.eq==>Logic.eq) g -> forall s, union (filter f s) (filter g s) [=] filter (fun x=>orb (f x) (g x)) s FAILURE! Tactics applied: 10000 Original Proof: [clear Comp' Comp f. intros. assert (Proper (E.eq==>Logic.eq) (fun x => orb (f x) (g x))). repeat red; intros. rewrite (H x y H1); rewrite (H0 x y H1); auto. unfold Equal; intros; set_iff; repeat rewrite filter_iff; auto. assert (f a || g a = true <-> f a = true \/ g a = true). split; auto with bool. intro H3; destruct (orb_prop _ _ H3); auto. tauto.] Proof search time: 0 min, 34 sec Number of successful tactic applications: 2725 Number of failed tactic applications: 7276 Results for fold 39 Results for lemma for_all_filter: : forall s, for_all f s=is_empty (filter (fun x => negb (f x)) s) FAILURE! Tactics applied: 10000 Original Proof: [intros; apply bool_1; split; intros. apply is_empty_1. unfold Empty; intros. rewrite filter_iff; auto. red; destruct 1. rewrite <- (@for_all_iff s f) in H; auto. rewrite (H a H0) in H1; discriminate. apply for_all_1; auto; red; intros. revert H; rewrite <- is_empty_iff. unfold Empty; intro H; generalize (H x); clear H. rewrite filter_iff; auto. destruct (f x); auto.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 2220 Number of failed tactic applications: 7781 Results for fold 40 Results for lemma add_cardinal_1: : forall s x, mem x s=true -> cardinal (add x s)=cardinal s SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 26 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 13 Number of failed tactic applications: 13 Results for fold 41 Results for lemma fold_compat: : forall (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA) (f g:elt->A->A), Proper (E.eq==>eqA==>eqA) f -> transpose eqA f -> Proper (E.eq==>eqA==>eqA) g -> transpose eqA g -> forall (i:A)(s:t),(forall x:elt, (In x s) -> forall y, (eqA (f x y) (g x y))) -> (eqA (fold f s i) (fold g s i)) FAILURE! Tactics applied: 10000 Original Proof: [intros A eqA st f g fc ft gc gt i. intro s; pattern s; apply set_rec; intros. transitivity (fold f s0 i). apply fold_equal with (eqA:=eqA); auto. rewrite equal_sym; auto. transitivity (fold g s0 i). apply H0; intros; apply H1; auto with set. elim (equal_2 H x); auto with set; intros. apply fold_equal with (eqA:=eqA); auto with set. transitivity (f x (fold f s0 i)). apply fold_add with (eqA:=eqA); auto with set. transitivity (g x (fold f s0 i)); auto with set relations. transitivity (g x (fold g s0 i)); auto with set relations. apply gc; auto with set relations. symmetry; apply fold_add with (eqA:=eqA); auto. do 2 rewrite fold_empty; reflexivity.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 2245 Number of failed tactic applications: 7756 Results for fold 42 Results for lemma fold_add: : mem x s=false -> eqA (fold f (add x s) i) (f x (fold f s i)) FAILURE! Tactics applied: 10000 Original Proof: [intros; apply fold_add with (eqA:=eqA); auto. rewrite not_mem_iff; auto.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 2102 Number of failed tactic applications: 7899 Results for fold 43 Results for lemma add_fold: : mem x s=true -> eqA (fold f (add x s) i) (fold f s i) FAILURE! Tactics applied: 10000 Original Proof: [intros; apply add_fold with (eqA:=eqA); auto with set.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 2322 Number of failed tactic applications: 7679 Results for fold 44 Results for lemma equal_mem_2: : equal s s'=true -> forall a, mem a s=mem a s' FAILURE! Tactics applied: 10000 Original Proof: [intros; rewrite (equal_2 H); auto.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 2707 Number of failed tactic applications: 7294 Results for fold 45 Results for lemma diff_subset_equal: : subset s s'=true -> equal (diff s s') empty=true SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 41 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 13 Number of failed tactic applications: 28 Results for fold 46 Results for lemma union_subset_2: : subset s' (union s s')=true SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 25 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 3 Number of failed tactic applications: 22 Results for fold 47 Results for lemma add_cardinal_2: : forall s x, mem x s=false -> cardinal (add x s)=S (cardinal s) FAILURE! Tactics applied: 10000 Original Proof: [intros; apply add_cardinal_2; auto. rewrite not_mem_iff; auto.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 2773 Number of failed tactic applications: 7228 Results for fold 48 Results for lemma union_subset_1: : subset s (union s s')=true SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 30 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 5 Number of failed tactic applications: 25 Results for fold 49 Results for lemma equal_equal: : equal s s'=true -> equal s s''=equal s' s'' FAILURE! Tactics applied: 10000 Original Proof: [intros; rewrite (equal_2 H); auto.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 2394 Number of failed tactic applications: 7607 Results for fold 50 Results for lemma fold_empty: : (fold f empty i) = i FAILURE! Tactics applied: 10000 Original Proof: [apply fold_empty; auto.] Proof search time: 0 min, 27 sec Number of successful tactic applications: 2574 Number of failed tactic applications: 7427 Results for fold 51 Results for lemma union_subset_3: : subset s s''=true -> subset s' s''=true -> subset (union s s') s''=true SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 8 Original Proof: [intros; apply subset_1; apply union_subset_3; auto with set.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 6 Number of failed tactic applications: 2 Results for fold 52 Results for lemma inter_add_2: : mem x s'=false -> equal (inter (add x s) s') (inter s s')=true FAILURE! Tactics applied: 10000 Original Proof: [intros; apply equal_1; apply inter_add_2. rewrite not_mem_iff; auto.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 1777 Number of failed tactic applications: 8224 Results for fold 53 Results for lemma equal_sym: : equal s s'=equal s' s FAILURE! Tactics applied: 10000 Original Proof: [intros; apply bool_1; do 2 rewrite <- equal_iff; intuition.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 2149 Number of failed tactic applications: 7852 Results for fold 54 Results for lemma for_all_mem_3: : forall s x,(mem x s)=true -> (f x)=false -> (for_all f s)=false FAILURE! Tactics applied: 10000 Original Proof: [intros. apply (bool_eq_ind (for_all f s));intros;auto. rewrite for_all_filter in H1; auto. rewrite is_empty_equal_empty in H1. generalize (equal_mem_2 _ _ H1 x). rewrite filter_b; auto. rewrite empty_mem. rewrite H. rewrite H0. simpl;auto.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 2149 Number of failed tactic applications: 7852 Results for fold 55 Results for lemma add_mem_3: : mem y s=true -> mem y (add x s)=true SUCCESS! Proof Found in EFSM: auto with set. Tactics applied: 93 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Number of successful tactic applications: 21 Number of failed tactic applications: 72 Results for fold 56 Results for lemma add_mem_2: : ~E.eq x y -> mem y (add x s)=mem y s FAILURE! Tactics applied: 10000 Original Proof: [apply add_neq_b.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 1911 Number of failed tactic applications: 8090 Results for fold 57 Results for lemma for_all_mem_1: : forall s, (forall x, (mem x s)=true->(f x)=true) -> (for_all f s)=true FAILURE! Tactics applied: 10000 Original Proof: [intros. rewrite for_all_filter; auto. rewrite is_empty_equal_empty. apply equal_mem_1;intros. rewrite filter_b; auto. rewrite empty_mem. generalize (H a); case (mem a s);intros;auto. rewrite H0;auto.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 2082 Number of failed tactic applications: 7919 Results for fold 58 Results for lemma for_all_exists: : forall s, exists_ f s = negb (for_all (fun x =>negb (f x)) s) FAILURE! Tactics applied: 10000 Original Proof: [intros. rewrite for_all_b; auto. rewrite exists_b; auto. induction (elements s); simpl; auto. destruct (f a); simpl; auto.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 2131 Number of failed tactic applications: 7870 Results for fold 59 Results for lemma union_mem: : mem x (union s s')=mem x s || mem x s' FAILURE! Tactics applied: 10000 Original Proof: [apply union_b.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 1841 Number of failed tactic applications: 8160 Results for fold 60 Results for lemma subset_equal: : equal s s'=true -> subset s s'=true SUCCESS! Proof Found in EFSM: auto with set; Tactics applied: 16 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 3 Number of failed tactic applications: 13 Results for fold 61 Results for lemma diff_inter_all: : equal (union (diff s s') (inter s s')) s=true SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 42 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 5 Number of failed tactic applications: 37 Results for fold 62 Results for lemma filter_union: : forall s s', filter f (union s s') [=] union (filter f s) (filter f s') FAILURE! Tactics applied: 10000 Original Proof: [unfold Equal; intros; set_iff; repeat rewrite filter_iff; auto; set_iff; tauto.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 2775 Number of failed tactic applications: 7226 Results for fold 63 Results for lemma sum_compat: : forall f g, Proper (E.eq==>Logic.eq) f -> Proper (E.eq==>Logic.eq) g -> forall s, (forall x, In x s -> f x=g x) -> sum f s=sum g s FAILURE! Tactics applied: 10000 Original Proof: [intros. unfold sum; apply (@fold_compat _ (@Logic.eq nat)); repeat red; auto with *.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 3164 Number of failed tactic applications: 6837 Results for fold 64 Results for lemma set_rec: : forall (P:t->Type), (forall s s', equal s s'=true -> P s -> P s') -> (forall s x, mem x s=false -> P s -> P (add x s)) -> P empty -> forall s, P s FAILURE! Tactics applied: 10000 Original Proof: [intros. apply set_induction; auto; intros. apply X with empty; auto with set. apply X with (add x s0); auto with set. apply equal_1; intro a; rewrite add_iff; rewrite (H0 a); tauto. apply X0; auto with set; apply mem_3; auto.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 1557 Number of failed tactic applications: 8444 Results for fold 65 Results for lemma equal_mem_1: : (forall a, mem a s=mem a s') -> equal s s'=true FAILURE! Tactics applied: 10000 Original Proof: [intros; apply equal_1; unfold Equal; intros. do 2 rewrite mem_iff; rewrite H; tauto.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 2830 Number of failed tactic applications: 7171 Results for fold 66 Results for lemma sum_filter: : forall f : elt -> bool, Proper (E.eq==>Logic.eq) f -> forall s, (sum (fun x => if f x then 1 else 0) s) = (cardinal (filter f s)) FAILURE! Tactics applied: 10000 Original Proof: [unfold sum; intros f Hf. assert (st : Equivalence (@Logic.eq nat)) by (split; congruence). assert (cc : compat_opL (fun x => plus (if f x then 1 else 0))) by (repeat red; intros; rewrite Hf; auto). assert (ct : transposeL (fun x => plus (if f x then 1 else 0))) by (red; intros; omega). intros s;pattern s; apply set_rec. intros. change elt with E.t. rewrite <- (fold_equal _ _ st _ cc ct 0 _ _ H). apply equal_2 in H; rewrite <- H, <-H0; auto. intros; rewrite (fold_add _ _ st _ cc ct); auto. generalize (@add_filter_1 f Hf s0 (add x s0) x) (@add_filter_2 f Hf s0 (add x s0) x) . assert (~ In x (filter f s0)). intro H1; rewrite (mem_1 (filter_1 Hf H1)) in H; discriminate H. case (f x); simpl; intros. rewrite (MP.cardinal_2 H1 (H2 (eq_refl true) (MP.Add_add s0 x))); auto. rewrite <- (MP.Equal_cardinal (H3 (eq_refl false) (MP.Add_add s0 x))); auto. intros; rewrite fold_empty;auto. rewrite MP.cardinal_1; auto. unfold Empty; intros. rewrite filter_iff; auto; set_iff; tauto.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 1905 Number of failed tactic applications: 8096 Results for fold 67 Results for lemma equal_refl: : equal s s=true SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 15 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 1 Number of failed tactic applications: 14 Results for fold 68 Results for lemma inter_equal_2: : equal s' s''=true -> equal (inter s s') (inter s s'')=true SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 32 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 12 Number of failed tactic applications: 20 Results for fold 69 Results for lemma subset_mem_1: : (forall a, mem a s=true->mem a s'=true) -> subset s s'=true FAILURE! Tactics applied: 10000 Original Proof: [intros; apply subset_1; unfold Subset; intros a. do 2 rewrite mem_iff; auto.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 2148 Number of failed tactic applications: 7853 Results for fold 70 Results for lemma add_mem_1: : mem x (add x s)=true SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 32 Original Proof: [auto with set relations.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 5 Number of failed tactic applications: 27 Results for fold 71 Results for lemma partition_filter_2: : forall s, equal (snd (partition f s)) (filter (fun x => negb (f x)) s)=true SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 12 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Number of successful tactic applications: 9 Number of failed tactic applications: 3 Results for fold 72 Results for lemma remove_mem_1: : mem x (remove x s)=false FAILURE! Tactics applied: 10000 Original Proof: [rewrite <- not_mem_iff; auto with set relations.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 2077 Number of failed tactic applications: 7924 Results for fold 73 Results for lemma equal_cardinal: : equal s s'=true -> cardinal s=cardinal s' SUCCESS! Proof Found in EFSM: auto with *. Tactics applied: 73 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Number of successful tactic applications: 20 Number of failed tactic applications: 53 Results for fold 74 Results for lemma singleton_mem_2: : ~E.eq x y -> mem y (singleton x)=false FAILURE! Tactics applied: 10000 Original Proof: [intros; rewrite singleton_b. unfold eqb; destruct (E.eq_dec x y); intuition.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 2421 Number of failed tactic applications: 7580 Results for fold 75 Results for lemma subset_cardinal: : forall s s', subset s s'=true -> cardinal s<=cardinal s' SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 30 Original Proof: [intros; apply subset_cardinal; auto with set.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 3 sec Number of successful tactic applications: 17 Number of failed tactic applications: 13 Results for fold 76 Results for lemma diff_mem: : mem x (diff s s')=mem x s && negb (mem x s') FAILURE! Tactics applied: 10000 Original Proof: [apply diff_b.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 2384 Number of failed tactic applications: 7617 Results for fold 77 Results for lemma remove_cardinal_1: : forall s x, mem x s=true -> S (cardinal (remove x s))=cardinal s FAILURE! Tactics applied: 10000 Original Proof: [intros; apply remove_cardinal_1; auto with set.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 2098 Number of failed tactic applications: 7903 Results for fold 78 Results for lemma add_equal: : mem x s=true -> equal (add x s) s=true SUCCESS! Proof Found in EFSM: auto with *. Tactics applied: 29 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 4 Number of failed tactic applications: 25 Results for fold 79 Results for lemma subset_antisym: : subset s s'=true -> subset s' s=true -> equal s s'=true SUCCESS! Proof Found in EFSM: auto with set. Tactics applied: 116 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 23 Number of failed tactic applications: 93 Results for fold 80 Results for lemma add_union_singleton: : equal (add x s) (union (singleton x) s)=true SUCCESS! Proof Found in EFSM: auto with set. Tactics applied: 26 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Number of successful tactic applications: 5 Number of failed tactic applications: 21 Results for fold 81 Results for lemma remove_mem_3: : mem y (remove x s)=true -> mem y s=true FAILURE! Tactics applied: 10000 Original Proof: [rewrite remove_b; intros H;destruct (andb_prop _ _ H); auto.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 1944 Number of failed tactic applications: 8057 Results for fold 82 Results for lemma union_equal_1: : equal s s'=true-> equal (union s s'') (union s' s'')=true SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 31 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Number of successful tactic applications: 10 Number of failed tactic applications: 21 Results for fold 83 Results for lemma subset_mem_2: : subset s s'=true -> forall a, mem a s=true -> mem a s'=true FAILURE! Tactics applied: 10000 Original Proof: [intros H a; do 2 rewrite <- mem_iff; apply subset_2; auto.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 2370 Number of failed tactic applications: 7631 Results for fold 84 Results for lemma union_cardinal: : forall s s', (forall x, mem x s && mem x s'=false) -> cardinal (union s s')=cardinal s+cardinal s' FAILURE! Tactics applied: 10000 Original Proof: [intros; apply union_cardinal; auto; intros. rewrite exclusive_set; auto.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 1838 Number of failed tactic applications: 8163 Results for fold 85 Results for lemma for_all_mem_4: : forall s, for_all f s=false -> {x:elt | mem x s=true /\ f x=false} FAILURE! Tactics applied: 10000 Original Proof: [intros. rewrite for_all_filter in H; auto. destruct (choose_mem_3 _ H) as (x,(H0,H1));intros. exists x. rewrite filter_b in H1; auto. elim (andb_prop _ _ H1). split;auto. rewrite <- negb_true_iff; auto.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 1558 Number of failed tactic applications: 8443 Results for fold 86 Results for lemma choose_mem_2: : choose s=None -> is_empty s=true SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 13 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 4 Number of failed tactic applications: 9 Results for fold 87 Results for lemma inter_sym: : equal (inter s s') (inter s' s)=true SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 16 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 3 Number of failed tactic applications: 13 Results for fold 88 Results for lemma remove_cardinal_2: : forall s x, mem x s=false -> cardinal (remove x s)=cardinal s FAILURE! Tactics applied: 10000 Original Proof: [intros; apply Equal_cardinal; apply equal_2; auto with set.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 2210 Number of failed tactic applications: 7791 Results for fold 89 Results for lemma inter_mem: : mem x (inter s s')=mem x s && mem x s' FAILURE! Tactics applied: 10000 Original Proof: [apply inter_b.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 2095 Number of failed tactic applications: 7906 Results for fold 90 Results for lemma inter_subset_2: : subset (inter s s') s'=true SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 54 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Number of successful tactic applications: 9 Number of failed tactic applications: 45 Results for fold 91 Results for lemma partition_filter_1: : forall s, equal (fst (partition f s)) (filter f s)=true SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 58 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Number of successful tactic applications: 14 Number of failed tactic applications: 44 Results for fold 92 Results for lemma exists_mem_3: : forall s x, mem x s=true -> f x=true -> exists_ f s=true FAILURE! Tactics applied: 10000 Original Proof: [intros. rewrite for_all_exists; auto. rewrite negb_true_iff. apply for_all_mem_3 with x;auto. rewrite negb_false_iff; auto.] Proof search time: 0 min, 28 sec Number of successful tactic applications: 3235 Number of failed tactic applications: 6766 Results for fold 93 Results for lemma choose_mem_3: : is_empty s=false -> {x:elt|choose s=Some x /\ mem x s=true} FAILURE! Tactics applied: 10000 Original Proof: [intros. generalize (@choose_1 s) (@choose_2 s). destruct (choose s);intros. exists e;auto with set. generalize (H1 (eq_refl None)); clear H1. intros; rewrite (is_empty_1 H1) in H; discriminate.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 1843 Number of failed tactic applications: 8158 Results for fold 94 Results for lemma subset_refl: : subset s s=true SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 25 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 4 Number of failed tactic applications: 21 Results for fold 95 Results for lemma inter_equal_1: : equal s s'=true -> equal (inter s s'') (inter s' s'')=true SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 15 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 8 Number of failed tactic applications: 7 Results for fold 96 Results for lemma choose_mem_1: : choose s=Some x -> mem x s=true SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 40 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 13 Number of failed tactic applications: 27 Results for fold 97 Results for lemma mem_eq: : E.eq x y -> mem x s=mem y s FAILURE! Tactics applied: 10000 Original Proof: [intro H; rewrite H; auto.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 2181 Number of failed tactic applications: 7820 Results for fold 98 Results for lemma union_assoc: : equal (union (union s s') s'') (union s (union s' s''))=true SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 38 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 3 Number of failed tactic applications: 35 Results for fold 99 Results for lemma exists_mem_1: : forall s, (forall x, mem x s=true->f x=false) -> exists_ f s=false FAILURE! Tactics applied: 10000 Original Proof: [intros. rewrite for_all_exists; auto. rewrite for_all_mem_1;auto with bool. intros;generalize (H x H0);intros. rewrite negb_true_iff; auto.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 2115 Number of failed tactic applications: 7886 Results for fold 100 Results for lemma add_filter_2: : forall s s' x, f x=false -> (Add x s s') -> filter f s [=] filter f s' FAILURE! Tactics applied: 10000 Original Proof: [unfold Add, MP.Add, Equal; intros. repeat rewrite filter_iff; auto. rewrite H0; clear H0. intuition. setoid_replace x with a in H; auto. congruence.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 2929 Number of failed tactic applications: 7072 Results for fold 101 Results for lemma fold_equal: : equal s s'=true -> eqA (fold f s i) (fold f s' i) FAILURE! Tactics applied: 10000 Original Proof: [intros; apply fold_equal with (eqA:=eqA); auto with set.] Proof search time: 0 min, 27 sec Number of successful tactic applications: 2866 Number of failed tactic applications: 7135 Results for fold 102 Results for lemma diff_subset: : subset (diff s s') s=true SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 31 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Number of successful tactic applications: 4 Number of failed tactic applications: 27 Results for fold 103 Results for lemma union_add: : equal (union (add x s) s') (add x (union s s'))=true SUCCESS! Proof Found in EFSM: auto with set. Tactics applied: 57 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 4 Number of failed tactic applications: 53 Results for fold 104 Results for lemma is_empty_equal_empty: : is_empty s = equal s empty SUCCESS! Proof Found in EFSM: apply bool_1; intuition. Tactics applied: 545 Original Proof: [apply bool_1; split; intros. auto with set. rewrite <- is_empty_iff; auto with set.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 3 sec Number of successful tactic applications: 99 Number of failed tactic applications: 446 Results for fold 105 Results for lemma union_sym: : equal (union s s') (union s' s)=true SUCCESS! Proof Found in EFSM: auto with set. Tactics applied: 77 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 7 Number of failed tactic applications: 70 Results for fold 106 Results for lemma exists_filter: : forall s, exists_ f s=negb (is_empty (filter f s)) FAILURE! Tactics applied: 10000 Original Proof: [intros; apply bool_1; split; intros. destruct (exists_2 Comp H) as (a,(Ha1,Ha2)). apply bool_6. red; intros; apply (@is_empty_2 _ H0 a); auto with set. generalize (@choose_1 (filter f s)) (@choose_2 (filter f s)). destruct (choose (filter f s)). intros H0 _; apply exists_1; auto. exists e; generalize (H0 e); rewrite filter_iff; auto. intros _ H0. rewrite (is_empty_1 (H0 (eq_refl None))) in H; auto; discriminate.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 2137 Number of failed tactic applications: 7864 OVERALL RESULTS SUMMARY EFSMProver proved 44 out of 106 lemmas. Success rate of 41.509433962264154% There were 0 errors. 62 proof attempts exhausted the automaton On average, a proof was found after applying 131 tactics The longest proof consisted of 3 tactics There were 5 shorter proofs found Of the 62 failures, 62 of them used all 10000 tactics There were 42 reused proofs found There were 2 novel proofs found Of the 62 failures, the average number of tactics used was 10000 On average, a proof was found after 0 min, 2 sec On average, a failed proof attempt took 0 min, 21 sec On average, any (success or failure) proof attempt took 0 min, 13 sec The longest time to find a proof was 0 min, 7 sec The shortest time to find a proof was 0 min, 1 sec There were 0 proofs containing repeated tactics There were 1 proofs that repeated states