Results for fold 1 Results for lemma cardinal_0: : forall s, exists l : list elt, NoDupA E.eq l /\ (forall x : elt, In x s <-> InA E.eq x l) /\ cardinal s = length l FAILURE! Tactics applied: 10000 Original Proof: [intros; exists (elements s); intuition; apply cardinal_1.] Proof search time: 0 min, 27 sec Number of successful tactic applications: 1836 Number of failed tactic applications: 8165 Results for lemma fold_0: : forall s (A : Type) (i : A) (f : elt -> A -> A), exists l : list elt, NoDup l /\ (forall x : elt, In x s <-> InA x l) /\ fold f s i = fold_right f i l FAILURE! Tactics applied: 10000 Original Proof: [intros; exists (rev (elements s)); split. apply NoDupA_rev; auto with *. split; intros. rewrite elements_iff; do 2 rewrite InA_alt. split; destruct 1; generalize (In_rev (elements s) x0); exists x0; intuition. apply fold_spec_right.] Proof search time: 0 min, 30 sec Number of successful tactic applications: 2146 Number of failed tactic applications: 7855 Results for lemma subset_remove_3: : s1[<=]s2 -> remove x s1 [<=] s2 SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 32 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 13 sec Number of successful tactic applications: 21 Number of failed tactic applications: 11 Results for lemma of_list_2: : forall l, equivlistA E.eq (to_list (of_list l)) l FAILURE! Tactics applied: 10000 Original Proof: [unfold to_list; red; intros. rewrite <- elements_iff; apply of_list_1.] Proof search time: 0 min, 27 sec Number of successful tactic applications: 2548 Number of failed tactic applications: 7453 Results for lemma subset_cardinal: : forall s s', s[<=]s' -> cardinal s <= cardinal s' FAILURE! Tactics applied: 10000 Original Proof: [intros. rewrite <- (diff_inter_cardinal s' s). rewrite (inter_sym s' s). rewrite (inter_subset_equal H); auto with arith.] Proof search time: 0 min, 27 sec Number of successful tactic applications: 1742 Number of failed tactic applications: 8259 Results for lemma add_cardinal_1: : forall s x, In x s -> cardinal (add x s) = cardinal s SUCCESS! Proof Found in EFSM: auto with *. Tactics applied: 92 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 13 sec Number of successful tactic applications: 33 Number of failed tactic applications: 59 Results for lemma union_subset_2: : s' [<=] union s s' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 32 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 13 sec Number of successful tactic applications: 5 Number of failed tactic applications: 27 Results for lemma inter_add_2: : ~ In x s' -> inter (add x s) s' [=] inter s s' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 32 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 13 sec Number of successful tactic applications: 21 Number of failed tactic applications: 11 Results for lemma cardinal_inv_1: : forall s, cardinal s = 0 -> Empty s FAILURE! Tactics applied: 10000 Original Proof: [intros; rewrite cardinal_Empty; auto.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 2438 Number of failed tactic applications: 7563 Results for lemma Equal_remove: : s[=]s' -> remove x s [=] remove x s' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 32 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 13 sec Number of successful tactic applications: 21 Number of failed tactic applications: 11 Results for lemma add_fold: : forall i s x, In x s -> eqA (fold f (add x s) i) (fold f s i) SUCCESS! Proof Found in EFSM: intros ; apply fold_equal; auto with *. Tactics applied: 2086 Original Proof: [intros; apply fold_equal; auto with set.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 16 sec Number of successful tactic applications: 480 Number of failed tactic applications: 1606 Results for lemma empty_diff_2: : Empty s -> diff s' s [=] s' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 32 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 13 sec Number of successful tactic applications: 21 Number of failed tactic applications: 11 Results for lemma not_in_union: : ~In x s -> ~In x s' -> ~In x (union s s') SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 32 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 13 sec Number of successful tactic applications: 21 Number of failed tactic applications: 11 Results for lemma fold_rec_weak: : forall (A:Type)(P : t -> A -> Type)(f : elt -> A -> A)(i:A), (forall s s' a, s[=]s' -> P s a -> P s' a) -> P empty i -> (forall x a s, ~In x s -> P s a -> P (add x s) (f x a)) -> forall s, P s (fold f s i) FAILURE! Tactics applied: 10000 Original Proof: [intros; apply fold_rec_bis; auto.] Proof search time: 0 min, 30 sec Number of successful tactic applications: 2085 Number of failed tactic applications: 7916 Results for fold 2 Results for lemma subset_empty: : empty[<=]s SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 38 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 10 Number of failed tactic applications: 28 Results for lemma empty_union_2: : Empty s -> union s' s [=] s' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 38 Original Proof: [fsetdec.] 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: 24 Results for lemma cardinal_2: : forall s s' x, ~ In x s -> Add x s s' -> cardinal s' = S (cardinal s) FAILURE! Tactics applied: 10000 Original Proof: [intros; do 2 rewrite cardinal_fold. change S with ((fun _ => S) x). apply fold_2; auto. split; congruence. congruence.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 1623 Number of failed tactic applications: 8378 Results for lemma inter_assoc: : inter (inter s s') s'' [=] inter s (inter s' s'') SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 38 Original Proof: [fsetdec.] 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: 26 Results for lemma cardinal_fold: : forall s, cardinal s = fold (fun _ => S) s 0 FAILURE! Tactics applied: 10000 Original Proof: [intros; rewrite cardinal_1; rewrite FM.fold_1. symmetry; apply fold_left_length; auto.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1273 Number of failed tactic applications: 8728 Results for lemma of_list_3: : forall s, of_list (to_list s) [=] s FAILURE! Tactics applied: 10000 Original Proof: [unfold to_list; red; intros. rewrite of_list_1; symmetry; apply elements_iff.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 1872 Number of failed tactic applications: 8129 Results for lemma remove_fold_2: : forall i s x, ~In x s -> eqA (fold f (remove x s) i) (fold f s i) FAILURE! Tactics applied: 10000 Original Proof: [intros. apply fold_equal; auto with set.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 2050 Number of failed tactic applications: 7951 Results for lemma double_inclusion: : s1[=]s2 <-> s1[<=]s2 /\ s2[<=]s1 SUCCESS! Proof Found in EFSM: intuition ; fsetdec. Tactics applied: 1408 Original Proof: [intuition fsetdec.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 5 sec Number of successful tactic applications: 316 Number of failed tactic applications: 1092 Results for lemma subset_trans: : s1[<=]s2 -> s2[<=]s3 -> s1[<=]s3 SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 38 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec Number of successful tactic applications: 10 Number of failed tactic applications: 28 Results for lemma fold_union_inter: : forall i s s', eqA (fold f (union s s') (fold f (inter s s') i)) (fold f s (fold f s' i)) FAILURE! Tactics applied: 10000 Original Proof: [intros; pattern s; apply set_induction; clear s; intros. transitivity (fold f s' (fold f (inter s s') i)). apply fold_equal; auto with set. transitivity (fold f s' i). apply fold_init; auto. apply fold_1; auto with set. symmetry; apply fold_1; auto. rename s'0 into s''. destruct (In_dec x s'). transitivity (fold f (union s'' s') (f x (fold f (inter s s') i))); auto with set. apply fold_init; auto. apply fold_2 with (eqA:=eqA); auto with set. rewrite inter_iff; intuition. transitivity (f x (fold f s (fold f s' i))). transitivity (fold f (union s s') (f x (fold f (inter s s') i))). apply fold_equal; auto. apply equal_sym; apply union_Equal with x; auto with set. transitivity (f x (fold f (union s s') (fold f (inter s s') i))). apply fold_commutes; auto. apply Comp; auto with relations. symmetry; apply fold_2 with (eqA:=eqA); auto. (* ~(In x s') *) transitivity (f x (fold f (union s s') (fold f (inter s'' s') i))). apply fold_2 with (eqA:=eqA); auto with set. transitivity (f x (fold f (union s s') (fold f (inter s s') i))). apply Comp;auto with relations. apply fold_init;auto. apply fold_equal;auto. apply equal_sym; apply inter_Add_2 with x; auto with set. transitivity (f x (fold f s (fold f s' i))). apply Comp; auto with relations. symmetry; apply fold_2 with (eqA:=eqA); auto.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 1763 Number of failed tactic applications: 8238 Results for lemma cardinal_inv_2b: : forall s, cardinal s <> 0 -> { x : elt | In x s } FAILURE! Tactics applied: 10000 Original Proof: [intro; generalize (@cardinal_inv_2 s); destruct cardinal; [intuition|eauto].] Proof search time: 0 min, 14 sec Number of successful tactic applications: 1187 Number of failed tactic applications: 8814 Results for lemma diff_inter_all: : union (diff s s') (inter s s') [=] s SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 38 Original Proof: [fsetdec.] 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: 26 Results for lemma union_assoc: : union (union s s') s'' [=] union s (union s' s'') SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 38 Original Proof: [fsetdec.] 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: 26 Results for lemma Add_add: : Add x s (add x s) SUCCESS! Proof Found in EFSM: expAdd ; fsetdec. Tactics applied: 115 Original Proof: [expAdd; fsetdec.] Shorter Proof Found? no Proof reused from union_Equal proof search time: 0 min, 2 sec Number of successful tactic applications: 30 Number of failed tactic applications: 85 Results for fold 3 Results for lemma inter_equal_2: : s'[=]s'' -> inter s s' [=] inter s s'' SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 8 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 7 sec Number of successful tactic applications: 1 Number of failed tactic applications: 7 Results for lemma subset_refl: : s[<=]s SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 8 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 7 sec Number of successful tactic applications: 1 Number of failed tactic applications: 7 Results for lemma union_subset_1: : s [<=] union s s' SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 8 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 7 sec Number of successful tactic applications: 1 Number of failed tactic applications: 7 Results for lemma remove_equal: : ~ In x s -> remove x s [=] s SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 8 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 7 sec Number of successful tactic applications: 1 Number of failed tactic applications: 7 Results for lemma cardinal_inv_2: : forall s n, cardinal s = S n -> { x : elt | In x s } FAILURE! Tactics applied: 10000 Original Proof: [intros; rewrite FM.cardinal_1 in H. generalize (elements_2 (s:=s)). destruct (elements s); try discriminate. exists e; auto with relations.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 1564 Number of failed tactic applications: 8437 Results for lemma singleton_cardinal: : forall x, cardinal (singleton x) = 1 FAILURE! Tactics applied: 10000 Original Proof: [intros. rewrite (singleton_equal_add x). replace 0 with (cardinal empty); auto with set. apply cardinal_2 with x; auto with set.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 1538 Number of failed tactic applications: 8463 Results for lemma empty_inter_2: : Empty s' -> Empty (inter s s') SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 8 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 7 sec Number of successful tactic applications: 3 Number of failed tactic applications: 5 Results for lemma set_induction_max: : forall P : t -> Type, (forall s : t, Empty s -> P s) -> (forall s s', P s -> forall x, Above x s -> Add x s s' -> P s') -> forall s : t, P s FAILURE! Tactics applied: 10000 Original Proof: [intros; remember (cardinal s) as n; revert s Heqn; induction n; intros; auto. case_eq (max_elt s); intros. apply X0 with (remove e s) e; auto with set. apply IHn. assert (S n = S (cardinal (remove e s))). rewrite Heqn; apply cardinal_2 with e; auto with set relations. inversion H0; auto. red; intros. rewrite remove_iff in H0; destruct H0. generalize (@max_elt_spec2 s e y H H0); order. assert (H0:=max_elt_spec3 H). rewrite cardinal_Empty in H0; rewrite H0 in Heqn; inversion Heqn.] Proof search time: 0 min, 30 sec Number of successful tactic applications: 1733 Number of failed tactic applications: 8268 Results for lemma empty_cardinal: : cardinal empty = 0 FAILURE! Tactics applied: 10000 Original Proof: [rewrite cardinal_fold; apply fold_1; auto with *.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 1629 Number of failed tactic applications: 8372 Results for lemma inter_subset_2: : inter s s' [<=] s' SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 8 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 7 sec Number of successful tactic applications: 1 Number of failed tactic applications: 7 Results for lemma remove_add: : ~In x s -> remove x (add x s) [=] s SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 8 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 7 sec Number of successful tactic applications: 1 Number of failed tactic applications: 7 Results for lemma empty_diff_1: : Empty s -> Empty (diff s s') SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 8 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 7 sec Number of successful tactic applications: 3 Number of failed tactic applications: 5 Results for lemma add_cardinal_2: : forall s x, ~In x s -> cardinal (add x s) = S (cardinal s) FAILURE! Tactics applied: 10000 Original Proof: [intros. do 2 rewrite cardinal_fold. change S with ((fun _ => S) x); apply fold_add with (eqA:=@Logic.eq nat); auto with *. congruence.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 1646 Number of failed tactic applications: 8355 Results for lemma add_add: : add x (add x' s) [=] add x' (add x s) SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 8 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 7 sec Number of successful tactic applications: 1 Number of failed tactic applications: 7 Results for fold 4 Results for lemma remove_fold_1: : forall i s x, In x s -> eqA (f x (fold f (remove x s) i)) (fold f s i) FAILURE! Tactics applied: 10000 Original Proof: [intros. symmetry. apply fold_2 with (eqA:=eqA); auto with set relations.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 2141 Number of failed tactic applications: 7860 Results for lemma set_induction_min: : forall P : t -> Type, (forall s : t, Empty s -> P s) -> (forall s s', P s -> forall x, Below x s -> Add x s s' -> P s') -> forall s : t, P s FAILURE! Tactics applied: 10000 Original Proof: [intros; remember (cardinal s) as n; revert s Heqn; induction n; intros; auto. case_eq (min_elt s); intros. apply X0 with (remove e s) e; auto with set. apply IHn. assert (S n = S (cardinal (remove e s))). rewrite Heqn; apply cardinal_2 with e; auto with set relations. inversion H0; auto. red; intros. rewrite remove_iff in H0; destruct H0. generalize (@min_elt_spec2 s e y H H0); order. assert (H0:=min_elt_spec3 H). rewrite cardinal_Empty in H0; auto; rewrite H0 in Heqn; inversion Heqn.] Proof search time: 0 min, 43 sec Number of successful tactic applications: 1806 Number of failed tactic applications: 8195 Results for lemma gtb_1: : forall x y, gtb x y = true <-> E.lt y x FAILURE! Tactics applied: 10000 Original Proof: [intros; rewrite <- compare_gt_iff. unfold gtb. destruct E.compare; intuition; try discriminate.] Proof search time: 0 min, 43 sec Number of successful tactic applications: 1168 Number of failed tactic applications: 8833 Results for lemma empty_union_1: : Empty s -> union s s' [=] s' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 17 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 5 sec Number of successful tactic applications: 6 Number of failed tactic applications: 11 Results for lemma elements_Add: : forall s s' x, ~In x s -> Add x s s' -> eqlistA E.eq (elements s') (elements_lt x s ++ x :: elements_ge x s) FAILURE! Tactics applied: 10000 Original Proof: [intros; unfold elements_ge, elements_lt. apply sort_equivlistA_eqlistA; auto with set. apply (@SortA_app _ E.eq); auto with *. apply (@filter_sort _ E.eq); auto with *; eauto with *. constructor; auto. apply (@filter_sort _ E.eq); auto with *; eauto with *. rewrite Inf_alt by (apply (@filter_sort _ E.eq); eauto with *). intros. rewrite filter_InA in H1; auto with *; destruct H1. rewrite leb_1 in H2. rewrite <- elements_iff in H1. assert (~E.eq x y). contradict H; rewrite H; auto. order. intros. rewrite filter_InA in H1; auto with *; destruct H1. rewrite gtb_1 in H3. inversion_clear H2. order. rewrite filter_InA in H4; auto with *; destruct H4. rewrite leb_1 in H4. order. red; intros a. rewrite InA_app_iff, InA_cons, !filter_InA, <-!elements_iff, leb_1, gtb_1, (H0 a) by (auto with *). intuition. elim_compare a x; intuition. right; right; split; auto. order.] Proof search time: 0 min, 25 sec Number of successful tactic applications: 2435 Number of failed tactic applications: 7566 Results for lemma set_induction: : forall P : t -> Type, (forall s, Empty s -> P s) -> (forall s s', P s -> forall x, ~In x s -> Add x s s' -> P s') -> forall s, P s FAILURE! Tactics applied: 10000 Original Proof: [intros. apply (@fold_rec _ (fun s _ => P s) (fun _ _ => tt) tt s); eauto.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 1678 Number of failed tactic applications: 8323 Results for lemma empty_inter_1: : Empty s -> Empty (inter s s') SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 17 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 5 sec Number of successful tactic applications: 5 Number of failed tactic applications: 12 Results for lemma fold_add: : forall i s x, ~In x s -> eqA (fold f (add x s) i) (f x (fold f s i)) FAILURE! Tactics applied: 10000 Original Proof: [intros; apply fold_2 with (eqA := eqA); auto with set.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 2146 Number of failed tactic applications: 7855 Results for lemma fold_rec_nodep: : forall (A:Type)(P : A -> Type)(f : elt -> A -> A)(i:A)(s:t), P i -> (forall x a, In x s -> P a -> P (f x a)) -> P (fold f s i) SUCCESS! Proof Found in EFSM: intros ; apply fold_rec; auto. Tactics applied: 893 Original Proof: [intros; apply fold_rec_bis with (P:=fun _ => P); auto.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 6 sec Number of successful tactic applications: 144 Number of failed tactic applications: 749 Results for lemma diff_subset: : diff s s' [<=] s SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 17 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 5 sec Number of successful tactic applications: 3 Number of failed tactic applications: 14 Results for lemma add_fold: : forall i s x, In x s -> eqA (fold f (add x s) i) (fold f s i) SUCCESS! Proof Found in EFSM: symmetry. apply fold_equal; auto with set. Tactics applied: 1066 Original Proof: [intros; apply fold_equal; auto with set.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 6 sec Number of successful tactic applications: 240 Number of failed tactic applications: 826 Results for lemma fold_equal: : forall i s s', s[=]s' -> eqA (fold f s i) (fold f s' i) FAILURE! Tactics applied: 10000 Original Proof: [intros i s; pattern s; apply set_induction; clear s; intros. transitivity i. apply fold_1; auto. symmetry; apply fold_1; auto. rewrite <- H0; auto. transitivity (f x (fold f s i)). apply fold_2 with (eqA := eqA); auto. symmetry; apply fold_2 with (eqA := eqA); auto. unfold Add in *; intros. rewrite <- H2; auto.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 2244 Number of failed tactic applications: 7757 Results for lemma inter_subset_3: : s''[<=]s -> s''[<=]s' -> s''[<=] inter s s' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 17 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 5 sec Number of successful tactic applications: 3 Number of failed tactic applications: 14 Results for lemma elements_Add_Above: : forall s s' x, Above x s -> Add x s s' -> eqlistA E.eq (elements s') (elements s ++ x::nil) FAILURE! Tactics applied: 10000 Original Proof: [intros. apply sort_equivlistA_eqlistA; auto with set. apply (@SortA_app _ E.eq); auto with *. intros. invlist InA. rewrite <- elements_iff in H1. setoid_replace y with x; auto. red; intros a. rewrite InA_app_iff, InA_cons, InA_nil, <-!elements_iff, (H0 a) by (auto with *). intuition.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 2361 Number of failed tactic applications: 7640 Results for fold 5 Results for lemma union_subset_3: : s[<=]s'' -> s'[<=]s'' -> union s s' [<=] s'' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 31 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 4 sec Number of successful tactic applications: 9 Number of failed tactic applications: 22 Results for lemma remove_diff_singleton: : remove x s [=] diff s (singleton x) SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 31 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 4 sec Number of successful tactic applications: 9 Number of failed tactic applications: 22 Results for lemma equal_refl: : s[=]s SUCCESS! Proof Found in EFSM: auto with *. Tactics applied: 23 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 4 sec Number of successful tactic applications: 9 Number of failed tactic applications: 14 Results for lemma fold_1: : forall s (A : Type) (eqA : A -> A -> Prop) (st : Equivalence eqA) (i : A) (f : elt -> A -> A), Empty s -> eqA (fold f s i) i FAILURE! Tactics applied: 10000 Original Proof: [unfold Empty; intros; destruct (fold_0 s i f) as (l,(H1, (H2, H3))). rewrite H3; clear H3. generalize H H2; clear H H2; case l; simpl; intros. reflexivity. elim (H e). elim (H2 e); intuition.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 1656 Number of failed tactic applications: 8345 Results for lemma inter_add_1: : In x s' -> inter (add x s) s' [=] add x (inter s s') SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 31 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 4 sec Number of successful tactic applications: 9 Number of failed tactic applications: 22 Results for lemma fold_1b: : forall s (A : Type)(i : A) (f : elt -> A -> A), Empty s -> (fold f s i) = i SUCCESS! Proof Found in EFSM: symmetry ; apply fold_rec; fsetdec. Tactics applied: 6755 Original Proof: [intros. rewrite FM.fold_1. rewrite elements_Empty in H; rewrite H; simpl; auto.] Shorter Proof Found? yes This is a novel proof This proof contained a loop around a state proof search time: 0 min, 13 sec Number of successful tactic applications: 1044 Number of failed tactic applications: 5711 Results for lemma union_subset_4: : s[<=]s' -> union s s'' [<=] union s' s'' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 31 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 4 sec Number of successful tactic applications: 9 Number of failed tactic applications: 22 Results for lemma fold_4: : forall s s' x (A : Type) (eqA : A -> A -> Prop) (st : Equivalence eqA) (i : A) (f : elt -> A -> A), Proper (E.eq==>eqA==>eqA) f -> Below x s -> Add x s s' -> eqA (fold f s' i) (fold f s (f x i)) FAILURE! Tactics applied: 10000 Original Proof: [intros. rewrite !fold_spec. change (eqA (fold_left (flip f) (elements s') i) (fold_left (flip f) (x::elements s) i)). unfold flip; rewrite <-!fold_left_rev_right. apply (@fold_right_eqlistA E.t E.eq A eqA st); auto. apply eqlistA_rev. apply elements_Add_Below; auto.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 2052 Number of failed tactic applications: 7949 Results for lemma fold_equal: : forall i s s', s[=]s' -> eqA (fold f s i) (fold f s' i) FAILURE! Tactics applied: 10000 Original Proof: [intros i s; pattern s; apply set_induction; clear s; intros. transitivity i. apply fold_1; auto. symmetry; apply fold_1; auto. rewrite <- H0; auto. transitivity (f x (fold f s i)). apply fold_2 with (eqA := eqA); auto. symmetry; apply fold_2 with (eqA := eqA); auto. unfold Add in *; intros. rewrite <- H2; auto.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 1722 Number of failed tactic applications: 8279 Results for lemma fold_diff_inter: : forall i s s', eqA (fold f (diff s s') (fold f (inter s s') i)) (fold f s i) FAILURE! Tactics applied: 10000 Original Proof: [intros. transitivity (fold f (union (diff s s') (inter s s')) (fold f (inter (diff s s') (inter s s')) i)). symmetry; apply fold_union_inter; auto. transitivity (fold f s (fold f (inter (diff s s') (inter s s')) i)). apply fold_equal; auto with set. apply fold_init; auto. apply fold_1; auto with set.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 1677 Number of failed tactic applications: 8324 Results for lemma set_induction_bis: : forall P : t -> Type, (forall s s', s [=] s' -> P s -> P s') -> P empty -> (forall x s, ~In x s -> P s -> P (add x s)) -> forall s, P s FAILURE! Tactics applied: 10000 Original Proof: [intros. apply (@fold_rec_bis _ (fun s _ => P s) (fun _ _ => tt) tt s); eauto.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 1347 Number of failed tactic applications: 8654 Results for lemma cardinal_1: : forall s, Empty s -> cardinal s = 0 FAILURE! Tactics applied: 10000 Original Proof: [intros; rewrite cardinal_fold; apply fold_1; auto with *.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 1164 Number of failed tactic applications: 8837 Results for lemma elements_Empty: : forall s, Empty s <-> elements s = nil FAILURE! Tactics applied: 10000 Original Proof: [intros. unfold Empty. split; intros. assert (forall a, ~ List.In a (elements s)). red; intros. apply (H a). rewrite elements_iff. rewrite InA_alt; exists a; auto with relations. destruct (elements s); auto. elim (H0 e); simpl; auto. red; intros. rewrite elements_iff in H0. rewrite InA_alt in H0; destruct H0. rewrite H in H0; destruct H0 as (_,H0); inversion H0.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 1202 Number of failed tactic applications: 8799 Results for lemma of_list_1: : forall l x, In x (of_list l) <-> InA E.eq x l FAILURE! Tactics applied: 10000 Original Proof: [induction l; simpl; intro x. rewrite empty_iff, InA_nil. intuition. rewrite add_iff, InA_cons, IHl. intuition.] Proof search time: 0 min, 16 sec Number of successful tactic applications: 1484 Number of failed tactic applications: 8517 Results for fold 6 Results for lemma inter_subset_1: : inter s s' [<=] s SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 1 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 7 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 Results for lemma fold_init: : forall i i' s, eqA i i' -> eqA (fold f s i) (fold f s i') FAILURE! Tactics applied: 10000 Original Proof: [intros. apply fold_rel with (R:=eqA); auto. intros; apply Comp; auto with relations.] Proof search time: 0 min, 27 sec Number of successful tactic applications: 1838 Number of failed tactic applications: 8163 Results for lemma union_equal_2: : s'[=]s'' -> union s s' [=] union s s'' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 1 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 7 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 Results for lemma diff_subset_equal: : s[<=]s' -> diff s s' [=] empty SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 1 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 7 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 Results for lemma union_Equal: : In x s'' -> Add x s s' -> union s s'' [=] union s' s'' SUCCESS! Proof Found in EFSM: expAdd ; fsetdec. Tactics applied: 207 Original Proof: [expAdd; fsetdec.] Shorter Proof Found? no Proof reused from inter_Add proof search time: 0 min, 8 sec Number of successful tactic applications: 41 Number of failed tactic applications: 166 Results for lemma subset_add_3: : In x s2 -> s1[<=]s2 -> add x s1 [<=] s2 SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 1 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 7 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 Results for lemma fold_union: : forall i s s', (forall x, ~(In x s/\In x s')) -> eqA (fold f (union s s') i) (fold f s (fold f s' i)) FAILURE! Tactics applied: 10000 Original Proof: [intros. transitivity (fold f (union s s') (fold f (inter s s') i)). apply fold_init; auto. symmetry; apply fold_1; auto with set. unfold Empty; intro a; generalize (H a); set_iff; tauto. apply fold_union_inter; auto.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 1943 Number of failed tactic applications: 8058 Results for lemma union_inter_2: : union (inter s s') s'' [=] inter (union s s'') (union s' s'') SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 1 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 7 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 Results for lemma Add_remove: : In x s -> Add x (remove x s) s SUCCESS! Proof Found in EFSM: expAdd ; fsetdec. Tactics applied: 207 Original Proof: [expAdd; fsetdec.] Shorter Proof Found? no Proof reused from inter_Add proof search time: 0 min, 8 sec Number of successful tactic applications: 39 Number of failed tactic applications: 168 Results for lemma remove_cardinal_2: : forall s x, ~In x s -> cardinal (remove x s) = cardinal s SUCCESS! Proof Found in EFSM: auto with *. Tactics applied: 17 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 7 sec Number of successful tactic applications: 9 Number of failed tactic applications: 8 Results for lemma union_remove_add_1: : union (remove x s) (add x s') [=] union (add x s) (remove x s') SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 1 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 7 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 Results for lemma fold_commutes: : forall i s x, eqA (fold f s (f x i)) (f x (fold f s i)) FAILURE! Tactics applied: 10000 Original Proof: [intros. apply fold_rel with (R:=fun u v => eqA u (f x v)); intros. reflexivity. transitivity (f x0 (f x b)); auto. apply Comp; auto with relations.] Proof search time: 0 min, 27 sec Number of successful tactic applications: 1938 Number of failed tactic applications: 8063 Results for lemma singleton_equal_add: : singleton x [=] add x empty SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 1 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 7 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 Results for lemma diff_inter_empty: : inter (diff s s') (inter s s') [=] empty SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 1 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 7 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 Results for fold 7 Results for lemma fold_rec: : forall (A:Type)(P : t -> A -> Type)(f : elt -> A -> A)(i:A)(s:t), (forall s', Empty s' -> P s' i) -> (forall x a s' s'', In x s -> ~In x s' -> Add x s' s'' -> P s' a -> P s'' (f x a)) -> P s (fold f s i) FAILURE! Tactics applied: 10000 Original Proof: [intros A P f i s Pempty Pstep. rewrite fold_spec_right. set (l:=rev (elements s)). assert (Pstep' : forall x a s' s'', InA x l -> ~In x s' -> Add x s' s'' -> P s' a -> P s'' (f x a)). intros; eapply Pstep; eauto. rewrite elements_iff, <- InA_rev; auto with *. assert (Hdup : NoDup l) by (unfold l; eauto using elements_3w, NoDupA_rev with *). assert (Hsame : forall x, In x s <-> InA x l) by (unfold l; intros; rewrite elements_iff, InA_rev; intuition). clear Pstep; clearbody l; revert s Hsame; induction l. intros s Hsame; simpl. apply Pempty. intro x. rewrite Hsame, InA_nil; intuition. intros s Hsame; simpl. apply Pstep' with (of_list l); auto with relations. inversion_clear Hdup; rewrite of_list_1; auto. red. intros. rewrite Hsame, of_list_1, InA_cons; intuition. apply IHl. intros; eapply Pstep'; eauto. inversion_clear Hdup; auto. exact (of_list_1 l).] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1428 Number of failed tactic applications: 8573 Results for lemma In_dec: : forall x s, {In x s} + {~ In x s} FAILURE! Tactics applied: 10000 Original Proof: [intros; generalize (mem_iff s x); case (mem x s); intuition.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 1312 Number of failed tactic applications: 8689 Results for lemma fold_rel: : forall (A B:Type)(R : A -> B -> Type) (f : elt -> A -> A)(g : elt -> B -> B)(i : A)(j : B)(s : t), R i j -> (forall x a b, In x s -> R a b -> R (f x a) (g x b)) -> R (fold f s i) (fold g s j) FAILURE! Tactics applied: 10000 Original Proof: [intros A B R f g i j s Rempty Rstep. rewrite 2 fold_spec_right. set (l:=rev (elements s)). assert (Rstep' : forall x a b, InA x l -> R a b -> R (f x a) (g x b)) by (intros; apply Rstep; auto; rewrite elements_iff, <- InA_rev; auto with *). clearbody l; clear Rstep s. induction l; simpl; auto with relations.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 1414 Number of failed tactic applications: 8587 Results for lemma subset_equal: : s[=]s' -> s[<=]s' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 38 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 4 sec Number of successful tactic applications: 9 Number of failed tactic applications: 29 Results for lemma diff_inter_cardinal: : forall s s', cardinal (diff s s') + cardinal (inter s s') = cardinal s FAILURE! Tactics applied: 10000 Original Proof: [intros; do 3 rewrite cardinal_fold. rewrite <- fold_plus. apply fold_diff_inter with (eqA:=@Logic.eq nat); auto with *. congruence.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 1859 Number of failed tactic applications: 8142 Results for lemma union_add: : union (add x s) s' [=] add x (union s s') SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 38 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 4 sec Number of successful tactic applications: 7 Number of failed tactic applications: 31 Results for lemma add_equal: : In x s -> add x s [=] s SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 38 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 4 sec Number of successful tactic applications: 9 Number of failed tactic applications: 29 Results for lemma cardinal_Empty: : forall s, Empty s <-> cardinal s = 0 FAILURE! Tactics applied: 10000 Original Proof: [intros. rewrite elements_Empty, FM.cardinal_1. destruct (elements s); intuition; discriminate.] Proof search time: 0 min, 21 sec Number of successful tactic applications: 2162 Number of failed tactic applications: 7839 Results for lemma inter_Add: : In x s'' -> Add x s s' -> Add x (inter s s'') (inter s' s'') SUCCESS! Proof Found in EFSM: expAdd ; fsetdec. Tactics applied: 311 Original Proof: [expAdd; fsetdec.] Shorter Proof Found? no Proof reused from union_Add proof search time: 0 min, 5 sec Number of successful tactic applications: 94 Number of failed tactic applications: 217 Results for lemma add_union_singleton: : add x s [=] union (singleton x) s SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 38 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 4 sec Number of successful tactic applications: 7 Number of failed tactic applications: 31 Results for lemma elements_Add_Below: : forall s s' x, Below x s -> Add x s s' -> eqlistA E.eq (elements s') (x::elements s) FAILURE! Tactics applied: 10000 Original Proof: [intros. apply sort_equivlistA_eqlistA; auto with set. change (sort E.lt ((x::nil) ++ elements s)). apply (@SortA_app _ E.eq); auto with *. intros. invlist InA. rewrite <- elements_iff in H2. setoid_replace x0 with x; auto. red; intros a. rewrite InA_cons, <- !elements_iff, (H0 a); intuition.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 2321 Number of failed tactic applications: 7680 Results for lemma subset_diff: : s1[<=]s3 -> diff s1 s2 [<=] s3 SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 38 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 4 sec Number of successful tactic applications: 9 Number of failed tactic applications: 29 Results for lemma union_cardinal_inter: : forall s s', cardinal (union s s') = cardinal s + cardinal s' - cardinal (inter s s') SUCCESS! Proof Found in EFSM: intros ; generalize (union_inter_cardinal s s'). auto with *. Tactics applied: 1213 Original Proof: [intros. rewrite <- union_inter_cardinal. rewrite Plus.plus_comm. auto with arith.] Shorter Proof Found? yes This is a novel proof This proof contained a loop around a state proof search time: 0 min, 6 sec Number of successful tactic applications: 234 Number of failed tactic applications: 979 Results for lemma fold_empty: : forall i, fold f empty i = i SUCCESS! Proof Found in EFSM: intros ; apply fold_1; auto with *. Tactics applied: 1186 Original Proof: [intros i; apply fold_1b; auto with set.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 6 sec Number of successful tactic applications: 159 Number of failed tactic applications: 1027 Results for fold 8 Results for lemma add_remove: : In x s -> add x (remove x s) [=] s SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 27 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 4 sec Number of successful tactic applications: 6 Number of failed tactic applications: 21 Results for lemma union_sym: : union s s' [=] union s' s SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 27 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 4 sec Number of successful tactic applications: 5 Number of failed tactic applications: 22 Results for lemma choose_equal: : forall s s', Equal s s' -> match choose s, choose s' with | Some x, Some x' => E.eq x x' | None, None => True | _, _ => False end FAILURE! Tactics applied: 10000 Original Proof: [intros s s' H; generalize (@choose_spec1 s)(@choose_spec2 s) (@choose_spec1 s')(@choose_spec2 s')(@choose_spec3 s s'); destruct (choose s); destruct (choose s'); simpl; intuition. apply H5 with e; rewrite <-H; auto. apply H5 with e; rewrite H; auto.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1707 Number of failed tactic applications: 8294 Results for lemma subset_add_2: : s1[<=]s2 -> s1[<=] add x s2 SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 27 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 4 sec Number of successful tactic applications: 6 Number of failed tactic applications: 21 Results for lemma fold_rec_bis: : forall (A:Type)(P : t -> A -> Type)(f : elt -> A -> A)(i:A)(s:t), (forall s s' a, s[=]s' -> P s a -> P s' a) -> (P empty i) -> (forall x a s', In x s -> ~In x s' -> P s' a -> P (add x s') (f x a)) -> P s (fold f s i) FAILURE! Tactics applied: 10000 Original Proof: [intros A P f i s Pmorphism Pempty Pstep. apply fold_rec; intros. apply Pmorphism with empty; auto with set. rewrite Add_Equal in H1; auto with set. apply Pmorphism with (add x s'); auto with set.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 1311 Number of failed tactic applications: 8690 Results for lemma empty_is_empty_1: : Empty s -> s[=]empty SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 27 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 4 sec Number of successful tactic applications: 8 Number of failed tactic applications: 19 Results for lemma remove_fold_2: : forall i s x, ~In x s -> eqA (fold f (remove x s) i) (fold f s i) SUCCESS! Proof Found in EFSM: intros ; apply fold_equal; auto with set. Tactics applied: 2057 Original Proof: [intros. apply fold_equal; auto with set.] Shorter Proof Found? no Proof reused from add_fold proof search time: 0 min, 7 sec Number of successful tactic applications: 366 Number of failed tactic applications: 1691 Results for lemma remove_cardinal_1: : forall s x, In x s -> S (cardinal (remove x s)) = cardinal s SUCCESS! Proof Found in EFSM: symmetry ; apply cardinal_2 with x; auto with *. Tactics applied: 6464 Original Proof: [intros. do 2 rewrite cardinal_fold. change S with ((fun _ =>S) x). apply remove_fold_1 with (eqA:=@Logic.eq nat); auto with *. congruence.] Shorter Proof Found? yes This is a novel proof This proof contained a loop around a state proof search time: 0 min, 13 sec Number of successful tactic applications: 1026 Number of failed tactic applications: 5438 Results for lemma union_Add: : Add x s s' -> Add x (union s s'') (union s' s'') SUCCESS! Proof Found in EFSM: expAdd ; intuition fsetdec. Tactics applied: 152 Original Proof: [expAdd; fsetdec.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 4 sec Number of successful tactic applications: 40 Number of failed tactic applications: 112 Results for lemma fold_spec_right: (s:t)(A:Type)(i:A)(f : elt -> A -> A) : fold f s i = List.fold_right f i (rev (elements s)) FAILURE! Tactics applied: 10000 Original Proof: [rewrite fold_spec. symmetry. apply fold_left_rev_right.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 1352 Number of failed tactic applications: 8649 Results for lemma fold_2: : forall s s' x (A : Type) (eqA : A -> A -> Prop) (st : Equivalence eqA) (i : A) (f : elt -> A -> A), Proper (E.eq==>eqA==>eqA) f -> transpose eqA f -> ~ In x s -> Add x s s' -> eqA (fold f s' i) (f x (fold f s i)) FAILURE! Tactics applied: 10000 Original Proof: [intros; destruct (fold_0 s i f) as (l,(Hl, (Hl1, Hl2))); destruct (fold_0 s' i f) as (l',(Hl', (Hl'1, Hl'2))). rewrite Hl2; rewrite Hl'2; clear Hl2 Hl'2. apply fold_right_add with (eqA:=E.eq)(eqB:=eqA); auto. eauto with *. rewrite <- Hl1; auto. intros a; rewrite InA_cons; rewrite <- Hl1; rewrite <- Hl'1; rewrite (H2 a); intuition.] Proof search time: 0 min, 31 sec Number of successful tactic applications: 1956 Number of failed tactic applications: 8045 Results for lemma fold_plus: : forall s p, fold (fun _ => S) s p = fold (fun _ => S) s 0 + p FAILURE! Tactics applied: 10000 Original Proof: [intros. apply fold_rel with (R:=fun u v => u = v + p); simpl; auto.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 1708 Number of failed tactic applications: 8293 Results for lemma Equal_cardinal: : forall s s', s[=]s' -> cardinal s = cardinal s' FAILURE! Tactics applied: 10000 Original Proof: [symmetry. remember (cardinal s) as n; symmetry in Heqn; revert s s' Heqn H. induction n; intros. apply cardinal_1; rewrite <- H; auto. destruct (cardinal_inv_2 Heqn) as (x,H2). revert Heqn. rewrite (cardinal_2 (s:=remove x s) (s':=s) (x:=x)); auto with set relations. rewrite (cardinal_2 (s:=remove x s') (s':=s') (x:=x)); eauto with set relations.] Proof search time: 0 min, 20 sec Number of successful tactic applications: 1616 Number of failed tactic applications: 8385 Results for lemma sort_equivlistA_eqlistA: : forall l l' : list elt, sort E.lt l -> sort E.lt l' -> equivlistA E.eq l l' -> eqlistA E.eq l l' FAILURE! Tactics applied: 10000 Original Proof: [apply SortA_equivlistA_eqlistA; eauto with *.] Proof search time: 0 min, 19 sec Number of successful tactic applications: 1562 Number of failed tactic applications: 8439 Results for fold 9 Results for lemma elements_empty: : elements empty = nil FAILURE! Tactics applied: 192 Original Proof: [rewrite <-elements_Empty; auto with set.] Proof search time: 0 min, 6 sec Number of successful tactic applications: 2 Number of failed tactic applications: 190 Results for lemma subset_antisym: : s[<=]s' -> s'[<=]s -> s[=]s' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 64 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 6 sec Number of successful tactic applications: 17 Number of failed tactic applications: 47 Results for lemma union_cardinal: : forall s s', (forall x, ~(In x s/\In x s')) -> cardinal (union s s')=cardinal s+cardinal s' FAILURE! Tactics applied: 10000 Original Proof: [intros; do 3 rewrite cardinal_fold. rewrite <- fold_plus. apply fold_union; auto. split; congruence. congruence.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 1722 Number of failed tactic applications: 8279 Results for lemma inter_subset_equal: : s[<=]s' -> inter s s' [=] s SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 64 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 6 sec Number of successful tactic applications: 17 Number of failed tactic applications: 47 Results for lemma union_equal_1: : s[=]s' -> union s s'' [=] union s' s'' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 64 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 6 sec Number of successful tactic applications: 17 Number of failed tactic applications: 47 Results for lemma union_subset_5: : s[<=]s' -> union s'' s [<=] union s'' s' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 64 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 6 sec Number of successful tactic applications: 17 Number of failed tactic applications: 47 Results for lemma equal_trans: : s1[=]s2 -> s2[=]s3 -> s1[=]s3 SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 64 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 6 sec Number of successful tactic applications: 17 Number of failed tactic applications: 47 Results for lemma leb_1: : forall x y, leb x y = true <-> ~E.lt y x FAILURE! Tactics applied: 10000 Original Proof: [intros; rewrite <- compare_gt_iff. unfold leb, gtb. destruct E.compare; intuition; try discriminate.] Proof search time: 0 min, 33 sec Number of successful tactic applications: 1789 Number of failed tactic applications: 8212 Results for lemma union_cardinal_le: : forall s s', cardinal (union s s') <= cardinal s + cardinal s' FAILURE! Tactics applied: 10000 Original Proof: [intros; generalize (union_inter_cardinal s s'). intros; rewrite <- H; auto with arith.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 1415 Number of failed tactic applications: 8586 Results for lemma subset_cardinal_lt: : forall s s' x, s[<=]s' -> In x s' -> ~In x s -> cardinal s < cardinal s' FAILURE! Tactics applied: 10000 Original Proof: [intros. rewrite <- (diff_inter_cardinal s' s). rewrite (inter_sym s' s). rewrite (inter_subset_equal H). generalize (@cardinal_inv_1 (diff s' s)). destruct (cardinal (diff s' s)). intro H2; destruct (H2 (eq_refl _) x). set_iff; auto. intros _. change (0 + cardinal s < S n + cardinal s). apply Plus.plus_lt_le_compat; auto with arith.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 1706 Number of failed tactic applications: 8295 Results for lemma fold_identity: : forall s, fold add s empty [=] s FAILURE! Tactics applied: 10000 Original Proof: [intros. apply fold_rec with (P:=fun s acc => acc[=]s); auto with set. intros. rewrite H2; rewrite Add_Equal in H1; auto with set.] Proof search time: 0 min, 26 sec Number of successful tactic applications: 2258 Number of failed tactic applications: 7743 Results for lemma union_remove_add_2: : In x s -> union (remove x s) (add x s') [=] union s s' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 64 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 6 sec Number of successful tactic applications: 17 Number of failed tactic applications: 47 Results for lemma empty_is_empty_2: : s[=]empty -> Empty s SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 64 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 6 sec Number of successful tactic applications: 19 Number of failed tactic applications: 45 Results for lemma equal_sym: : s[=]s' -> s'[=]s SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 64 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 6 sec Number of successful tactic applications: 17 Number of failed tactic applications: 47 Results for fold 10 Results for lemma union_subset_equal: : s[<=]s' -> union s s' [=] s' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 1 Original Proof: [fsetdec.] 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: 0 Results for lemma in_subset: : In x s1 -> s1[<=]s2 -> In x s2 SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 1 Original Proof: [fsetdec.] 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: 0 Results for lemma elements_split: : forall x s, elements s = elements_lt x s ++ elements_ge x s FAILURE! Tactics applied: 10000 Original Proof: [unfold elements_lt, elements_ge, leb; intros. eapply (@filter_split _ E.eq); eauto with *. intros. rewrite gtb_1 in H. assert (~E.lt y x). unfold gtb in *; elim_compare x y; intuition; try discriminate; order. order.] Proof search time: 0 min, 18 sec Number of successful tactic applications: 1756 Number of failed tactic applications: 8245 Results for lemma union_inter_1: : inter (union s s') s'' [=] union (inter s s'') (inter s' s'') SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 1 Original Proof: [fsetdec.] 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: 0 Results for lemma union_inter_cardinal: : forall s s', cardinal (union s s') + cardinal (inter s s') = cardinal s + cardinal s' FAILURE! Tactics applied: 10000 Original Proof: [intros. do 4 rewrite cardinal_fold. do 2 rewrite <- fold_plus. apply fold_union_inter with (eqA:=@Logic.eq nat); auto with *. congruence.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 1741 Number of failed tactic applications: 8260 Results for lemma inter_equal_1: : s[=]s' -> inter s s'' [=] inter s' s'' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 1 Original Proof: [fsetdec.] 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: 0 Results for lemma remove_singleton_empty: : In x s -> remove x s [=] empty -> singleton x [=] s SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 1 Original Proof: [fsetdec.] 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: 0 Results for lemma inter_Add_2: : ~In x s'' -> Add x s s' -> inter s s'' [=] inter s' s'' SUCCESS! Proof Found in EFSM: expAdd ; fsetdec. Tactics applied: 136 Original Proof: [expAdd; fsetdec.] Shorter Proof Found? no Proof reused from Add_add proof search time: 0 min, 4 sec Number of successful tactic applications: 12 Number of failed tactic applications: 124 Results for lemma Add_Equal: : forall x s s', Add x s s' <-> s' [=] add x s FAILURE! Tactics applied: 10000 Original Proof: [unfold Add. split; intros. red; intros. rewrite H; clear H. fsetdec. fsetdec.] Proof search time: 0 min, 17 sec Number of successful tactic applications: 1992 Number of failed tactic applications: 8009 Results for lemma inter_sym: : inter s s' [=] inter s' s SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 1 Original Proof: [fsetdec.] 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: 0 Results for lemma fold_3: : forall s s' x (A : Type) (eqA : A -> A -> Prop) (st : Equivalence eqA) (i : A) (f : elt -> A -> A), Proper (E.eq==>eqA==>eqA) f -> Above x s -> Add x s s' -> eqA (fold f s' i) (f x (fold f s i)) FAILURE! Tactics applied: 10000 Original Proof: [intros. rewrite 2 fold_spec_right. change (f x (fold_right f i (rev (elements s)))) with (fold_right f i (rev (x::nil)++rev (elements s))). apply (@fold_right_eqlistA E.t E.eq A eqA st); auto with *. rewrite <- distr_rev. apply eqlistA_rev. apply elements_Add_Above; auto.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 2459 Number of failed tactic applications: 7542 OVERALL RESULTS SUMMARY EFSMProver proved 78 out of 137 lemmas. Success rate of 56.934306569343065% There were 0 errors. 59 proof attempts exhausted the automaton On average, a proof was found after applying 332 tactics The longest proof consisted of 3 tactics There were 3 shorter proofs found Of the 59 failures, 58 of them used all 10000 tactics There were 69 reused proofs found There were 9 novel proofs found Of the 59 failures, the average number of tactics used was 9833 On average, a proof was found after 0 min, 6 sec On average, a failed proof attempt took 0 min, 24 sec On average, any (success or failure) proof attempt took 0 min, 14 sec The longest time to find a proof was 0 min, 16 sec The shortest time to find a proof was 0 min, 2 sec There were 0 proofs containing repeated tactics There were 5 proofs that repeated states