Results for fold 1 Results for lemma subset_diff: : s1[<=]s3 -> diff s1 s2 [<=] s3 SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 20 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 8 sec Number of successful tactic applications: 13 Number of failed tactic applications: 7 Results for fold 2 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_bis; intuition ; Tactics applied: 7550 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, 16 sec Number of successful tactic applications: 1102 Number of failed tactic applications: 6448 Results for fold 3 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, 21 sec Number of successful tactic applications: 1815 Number of failed tactic applications: 8186 Results for fold 4 Results for lemma equal_refl: : s[=]s SUCCESS! Proof Found in EFSM: auto with set relations. Tactics applied: 10 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 9 sec Number of successful tactic applications: 1 Number of failed tactic applications: 9 Results for fold 5 Results for lemma diff_subset_equal: : s[<=]s' -> diff s s' [=] empty SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 17 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: 8 Results for fold 6 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, 29 sec Number of successful tactic applications: 2039 Number of failed tactic applications: 7962 Results for fold 7 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, 30 sec Number of successful tactic applications: 1976 Number of failed tactic applications: 8025 Results for fold 8 Results for lemma union_subset_5: : s[<=]s' -> union s'' s [<=] union s'' s' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 76 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 11 sec Number of successful tactic applications: 6 Number of failed tactic applications: 70 Results for fold 9 Results for lemma Add_remove: : In x s -> Add x (remove x s) s SUCCESS! Proof Found in EFSM: expAdd ; fsetdec. Tactics applied: 164 Original Proof: [expAdd; fsetdec.] Shorter Proof Found? no Proof reused from inter_Add_2 proof search time: 0 min, 13 sec Number of successful tactic applications: 22 Number of failed tactic applications: 142 Results for fold 10 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: intros ; apply fold_1; auto with *; Tactics applied: 4626 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, 17 sec Number of successful tactic applications: 994 Number of failed tactic applications: 3632 Results for fold 11 Results for lemma add_remove: : In x s -> add x (remove x s) [=] s SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 36 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 8 sec Number of successful tactic applications: 7 Number of failed tactic applications: 29 Results for fold 12 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, 20 sec Number of successful tactic applications: 1682 Number of failed tactic applications: 8319 Results for fold 13 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, 7 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 Results for fold 14 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, 21 sec Number of successful tactic applications: 1838 Number of failed tactic applications: 8163 Results for fold 15 Results for lemma inter_subset_2: : inter s s' [<=] s' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 6 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 6 sec Number of successful tactic applications: 1 Number of failed tactic applications: 5 Results for fold 16 Results for lemma union_subset_4: : s[<=]s' -> union s s'' [<=] union s' s'' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 20 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 9 sec Number of successful tactic applications: 14 Number of failed tactic applications: 6 Results for fold 17 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, 26 sec Number of successful tactic applications: 2153 Number of failed tactic applications: 7848 Results for fold 18 Results for lemma union_subset_1: : s [<=] union s s' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 66 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 8 sec Number of successful tactic applications: 13 Number of failed tactic applications: 53 Results for fold 19 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: 222 Original Proof: [expAdd; fsetdec.] Shorter Proof Found? no Proof reused from union_Equal proof search time: 0 min, 9 sec Number of successful tactic applications: 65 Number of failed tactic applications: 157 Results for fold 20 Results for lemma diff_inter_empty: : inter (diff s s') (inter s s') [=] empty SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 12 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 11 sec Number of successful tactic applications: 3 Number of failed tactic applications: 9 Results for fold 21 Results for lemma double_inclusion: : s1[=]s2 <-> s1[<=]s2 /\ s2[<=]s1 SUCCESS! Proof Found in EFSM: intuition ; red ; fsetdec. Tactics applied: 6950 Original Proof: [intuition fsetdec.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 24 sec Number of successful tactic applications: 1177 Number of failed tactic applications: 5773 Results for fold 22 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, 25 sec Number of successful tactic applications: 1706 Number of failed tactic applications: 8295 Results for fold 23 Results for lemma inter_equal_1: : s[=]s' -> inter s s'' [=] inter s' s'' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 11 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: 6 Results for fold 24 Results for lemma empty_inter_1: : Empty s -> Empty (inter s s') SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 66 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 11 sec Number of successful tactic applications: 26 Number of failed tactic applications: 40 Results for fold 25 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: 234 Original Proof: [expAdd; fsetdec.] Shorter Proof Found? no Proof reused from union_Add proof search time: 0 min, 10 sec Number of successful tactic applications: 40 Number of failed tactic applications: 194 Results for fold 26 Results for lemma subset_empty: : empty[<=]s SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 49 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 8 sec Number of successful tactic applications: 5 Number of failed tactic applications: 44 Results for fold 27 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, 27 sec Number of successful tactic applications: 1571 Number of failed tactic applications: 8430 Results for fold 28 Results for lemma add_equal: : In x s -> add x s [=] s SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 100 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 9 sec Number of successful tactic applications: 38 Number of failed tactic applications: 62 Results for fold 29 Results for lemma empty_is_empty_2: : s[=]empty -> Empty s SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 95 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 9 sec Number of successful tactic applications: 24 Number of failed tactic applications: 71 Results for fold 30 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, 30 sec Number of successful tactic applications: 1992 Number of failed tactic applications: 8009 Results for fold 31 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, 19 sec Number of successful tactic applications: 1494 Number of failed tactic applications: 8507 Results for fold 32 Results for lemma remove_equal: : ~ In x s -> remove x s [=] s SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 20 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 8 sec Number of successful tactic applications: 6 Number of failed tactic applications: 14 Results for fold 33 Results for lemma inter_subset_1: : inter s s' [<=] s SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 23 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 10 sec Number of successful tactic applications: 5 Number of failed tactic applications: 18 Results for fold 34 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, 22 sec Number of successful tactic applications: 1424 Number of failed tactic applications: 8577 Results for fold 35 Results for lemma union_Add: : Add x s s' -> Add x (union s s'') (union s' s'') SUCCESS! Proof Found in EFSM: expAdd ; fsetdec. Tactics applied: 167 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: 34 Number of failed tactic applications: 133 Results for fold 36 Results for lemma equal_trans: : s1[=]s2 -> s2[=]s3 -> s1[=]s3 SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 58 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: 41 Results for fold 37 Results for lemma remove_add: : ~In x s -> remove x (add x 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, 8 sec Number of successful tactic applications: 6 Number of failed tactic applications: 11 Results for fold 38 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, 26 sec Number of successful tactic applications: 2079 Number of failed tactic applications: 7922 Results for fold 39 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: 5 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: 4 Results for fold 40 Results for lemma diff_inter_all: : union (diff s s') (inter s s') [=] s SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 72 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 6 sec Number of successful tactic applications: 10 Number of failed tactic applications: 62 Results for fold 41 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, 22 sec Number of successful tactic applications: 1925 Number of failed tactic applications: 8076 Results for fold 42 Results for lemma diff_subset: : 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, 10 sec Number of successful tactic applications: 3 Number of failed tactic applications: 29 Results for fold 43 Results for lemma inter_sym: : inter s s' [=] inter s' s SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 9 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: 6 Results for fold 44 Results for lemma add_add: : add x (add x' s) [=] add x' (add x s) SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 5 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 6 sec Number of successful tactic applications: 1 Number of failed tactic applications: 4 Results for fold 45 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, 33 sec Number of successful tactic applications: 1958 Number of failed tactic applications: 8043 Results for fold 46 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, 22 sec Number of successful tactic applications: 2234 Number of failed tactic applications: 7767 Results for fold 47 Results for lemma union_equal_2: : s'[=]s'' -> union s s' [=] union s s'' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 133 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 6 sec Number of successful tactic applications: 16 Number of failed tactic applications: 117 Results for fold 48 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, 28 sec Number of successful tactic applications: 1835 Number of failed tactic applications: 8166 Results for fold 49 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)) SUCCESS! Proof Found in EFSM: intros ; apply fold_2 with (eqA:=eqA); auto with set. Tactics applied: 2540 Original Proof: [intros; apply fold_2 with (eqA := eqA); auto with set.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 12 sec Number of successful tactic applications: 579 Number of failed tactic applications: 1961 Results for fold 50 Results for lemma union_equal_1: : s[=]s' -> union s s'' [=] union s' s'' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 47 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 9 sec Number of successful tactic applications: 14 Number of failed tactic applications: 33 Results for fold 51 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, 20 sec Number of successful tactic applications: 1997 Number of failed tactic applications: 8004 Results for fold 52 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, 27 sec Number of successful tactic applications: 2017 Number of failed tactic applications: 7984 Results for fold 53 Results for lemma inter_subset_equal: : s[<=]s' -> inter s s' [=] s SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 78 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 9 sec Number of successful tactic applications: 26 Number of failed tactic applications: 52 Results for fold 54 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, 20 sec Number of successful tactic applications: 1494 Number of failed tactic applications: 8507 Results for fold 55 Results for lemma empty_inter_2: : Empty s' -> Empty (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, 10 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 Results for fold 56 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: 87 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 10 sec Number of successful tactic applications: 16 Number of failed tactic applications: 71 Results for fold 57 Results for lemma subset_trans: : s1[<=]s2 -> s2[<=]s3 -> s1[<=]s3 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, 12 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 Results for fold 58 Results for lemma subset_add_3: : In x s2 -> s1[<=]s2 -> add x s1 [<=] s2 SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 96 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 9 sec Number of successful tactic applications: 9 Number of failed tactic applications: 87 Results for fold 59 Results for lemma empty_diff_2: : Empty s -> diff s' s [=] s' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 71 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 12 sec Number of successful tactic applications: 23 Number of failed tactic applications: 48 Results for fold 60 Results for lemma inter_assoc: : inter (inter s s') s'' [=] inter 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, 10 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 Results for fold 61 Results for lemma inter_equal_2: : s'[=]s'' -> inter s s' [=] inter s s'' SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 32 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 8 sec Number of successful tactic applications: 6 Number of failed tactic applications: 26 Results for fold 62 Results for lemma union_subset_3: : s[<=]s'' -> s'[<=]s'' -> union s s' [<=] s'' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 79 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 12 sec Number of successful tactic applications: 24 Number of failed tactic applications: 55 Results for fold 63 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; fsetdec. Tactics applied: 3663 Original Proof: [intros. apply fold_equal; auto with set.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 14 sec Number of successful tactic applications: 704 Number of failed tactic applications: 2959 Results for fold 64 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, 19 sec Number of successful tactic applications: 1661 Number of failed tactic applications: 8340 Results for fold 65 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, 21 sec Number of successful tactic applications: 1382 Number of failed tactic applications: 8619 Results for fold 66 Results for lemma equal_sym: : s[=]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 fold 67 Results for lemma union_subset_2: : s' [<=] union s s' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 10 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: 5 Results for fold 68 Results for lemma Add_add: : Add x s (add x s) SUCCESS! Proof Found in EFSM: expAdd ; fsetdec. Tactics applied: 112 Original Proof: [expAdd; fsetdec.] Shorter Proof Found? no Proof reused from inter_Add proof search time: 0 min, 11 sec Number of successful tactic applications: 38 Number of failed tactic applications: 74 Results for fold 69 Results for lemma remove_cardinal_1: : forall s x, In x s -> S (cardinal (remove x s)) = cardinal s FAILURE! Tactics applied: 10000 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.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 1801 Number of failed tactic applications: 8200 Results for fold 70 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: 1154 Number of failed tactic applications: 8847 Results for fold 71 Results for lemma subset_antisym: : s[<=]s' -> s'[<=]s -> s[=]s' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 61 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 11 sec Number of successful tactic applications: 29 Number of failed tactic applications: 32 Results for fold 72 Results for lemma empty_is_empty_1: : Empty s -> s[=]empty SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 55 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 5 sec Number of successful tactic applications: 25 Number of failed tactic applications: 30 Results for fold 73 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, 20 sec Number of successful tactic applications: 1373 Number of failed tactic applications: 8628 Results for fold 74 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: 35 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 5 sec Number of successful tactic applications: 16 Number of failed tactic applications: 19 Results for fold 75 Results for lemma subset_refl: : s[<=]s SUCCESS! Proof Found in EFSM: auto with *. Tactics applied: 15 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 11 sec Number of successful tactic applications: 1 Number of failed tactic applications: 14 Results for fold 76 Results for lemma add_union_singleton: : add x s [=] union (singleton x) s SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 52 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 11 sec Number of successful tactic applications: 7 Number of failed tactic applications: 45 Results for fold 77 Results for lemma union_subset_equal: : s[<=]s' -> union s s' [=] s' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 73 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 9 sec Number of successful tactic applications: 23 Number of failed tactic applications: 50 Results for fold 78 Results for lemma singleton_equal_add: : singleton x [=] add x empty SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 64 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 7 sec Number of successful tactic applications: 10 Number of failed tactic applications: 54 Results for fold 79 Results for lemma subset_remove_3: : s1[<=]s2 -> remove x s1 [<=] s2 SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 52 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: 47 Results for fold 80 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 set. Tactics applied: 2598 Original Proof: [intros; apply fold_equal; auto with set.] Shorter Proof Found? no Proof reused from add_fold proof search time: 0 min, 8 sec Number of successful tactic applications: 506 Number of failed tactic applications: 2092 Results for fold 81 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, 29 sec Number of successful tactic applications: 1994 Number of failed tactic applications: 8007 Results for fold 82 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, 25 sec Number of successful tactic applications: 1662 Number of failed tactic applications: 8339 Results for fold 83 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, 21 sec Number of successful tactic applications: 1305 Number of failed tactic applications: 8696 Results for fold 84 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, 24 sec Number of successful tactic applications: 2301 Number of failed tactic applications: 7700 Results for fold 85 Results for lemma union_assoc: : union (union s s') s'' [=] union s (union s' s'') SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 26 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 12 sec Number of successful tactic applications: 1 Number of failed tactic applications: 25 Results for fold 86 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, 31 sec Number of successful tactic applications: 1736 Number of failed tactic applications: 8265 Results for fold 87 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, 26 sec Number of successful tactic applications: 1766 Number of failed tactic applications: 8235 Results for fold 88 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, 31 sec Number of successful tactic applications: 1910 Number of failed tactic applications: 8091 Results for fold 89 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: 99 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: 85 Results for fold 90 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, 20 sec Number of successful tactic applications: 1676 Number of failed tactic applications: 8325 Results for fold 91 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: 101 Original Proof: [expAdd; fsetdec.] Shorter Proof Found? no Proof reused from Add_remove This proof contained a loop around a state proof search time: 0 min, 5 sec Number of successful tactic applications: 23 Number of failed tactic applications: 78 Results for fold 92 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, 23 sec Number of successful tactic applications: 1125 Number of failed tactic applications: 8876 Results for fold 93 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, 23 sec Number of successful tactic applications: 2014 Number of failed tactic applications: 7987 Results for fold 94 Results for lemma inter_subset_3: : s''[<=]s -> s''[<=]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, 9 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 Results for fold 95 Results for lemma union_add: : union (add x s) s' [=] add x (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, 5 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 Results for fold 96 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, 16 sec Number of successful tactic applications: 1550 Number of failed tactic applications: 8451 Results for fold 97 Results for lemma empty_union_1: : Empty s -> union s s' [=] s' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 27 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 10 sec Number of successful tactic applications: 13 Number of failed tactic applications: 14 Results for fold 98 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, 26 sec Number of successful tactic applications: 1304 Number of failed tactic applications: 8697 Results for fold 99 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, 27 sec Number of successful tactic applications: 1707 Number of failed tactic applications: 8294 Results for fold 100 Results for lemma union_sym: : union s s' [=] union s' s SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 126 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 9 sec Number of successful tactic applications: 13 Number of failed tactic applications: 113 Results for fold 101 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, 25 sec Number of successful tactic applications: 1758 Number of failed tactic applications: 8243 Results for fold 102 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: 1717 Number of failed tactic applications: 8284 Results for fold 103 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, 24 sec Number of successful tactic applications: 2257 Number of failed tactic applications: 7744 Results for fold 104 Results for lemma subset_add_2: : s1[<=]s2 -> s1[<=] add 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, 7 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 Results for fold 105 Results for lemma union_cardinal_inter: : forall s s', cardinal (union s s') = cardinal s + cardinal s' - cardinal (inter s s') FAILURE! Tactics applied: 10000 Original Proof: [intros. rewrite <- union_inter_cardinal. rewrite Plus.plus_comm. auto with arith.] Proof search time: 0 min, 32 sec Number of successful tactic applications: 2310 Number of failed tactic applications: 7691 Results for fold 106 Results for lemma remove_diff_singleton: : remove x s [=] diff s (singleton x) SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 96 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 16 sec Number of successful tactic applications: 14 Number of failed tactic applications: 82 Results for fold 107 Results for lemma empty_diff_1: : Empty s -> Empty (diff s s') SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 12 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 7 sec Number of successful tactic applications: 5 Number of failed tactic applications: 7 Results for fold 108 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, 27 sec Number of successful tactic applications: 2402 Number of failed tactic applications: 7599 Results for fold 109 Results for lemma Equal_remove: : s[=]s' -> remove x s [=] remove x s' SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 50 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 7 sec Number of successful tactic applications: 13 Number of failed tactic applications: 37 Results for fold 110 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, 21 sec Number of successful tactic applications: 1434 Number of failed tactic applications: 8567 Results for fold 111 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, 23 sec Number of successful tactic applications: 1784 Number of failed tactic applications: 8217 Results for fold 112 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, 24 sec Number of successful tactic applications: 1833 Number of failed tactic applications: 8168 Results for fold 113 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: 12 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 10 sec Number of successful tactic applications: 10 Number of failed tactic applications: 2 Results for fold 114 Results for lemma empty_union_2: : Empty s -> union s' s [=] s' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 22 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 6 sec Number of successful tactic applications: 9 Number of failed tactic applications: 13 Results for fold 115 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, 25 sec Number of successful tactic applications: 2090 Number of failed tactic applications: 7911 Results for fold 116 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, 40 sec Number of successful tactic applications: 1528 Number of failed tactic applications: 8473 Results for fold 117 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, 29 sec Number of successful tactic applications: 2508 Number of failed tactic applications: 7493 Results for fold 118 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, 17 sec Number of successful tactic applications: 1324 Number of failed tactic applications: 8677 Results for fold 119 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, 32 sec Number of successful tactic applications: 1975 Number of failed tactic applications: 8026 Results for fold 120 Results for lemma fold_identity: : forall s, fold add s empty [=] s SUCCESS! Proof Found in EFSM: intuition ; apply fold_rec_bis; fsetdec. Tactics applied: 6495 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.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 20 sec Number of successful tactic applications: 1460 Number of failed tactic applications: 5035 Results for fold 121 Results for lemma elements_empty: : elements empty = nil FAILURE! Tactics applied: 10000 Original Proof: [rewrite <-elements_Empty; auto with set.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 732 Number of failed tactic applications: 9269 Results for fold 122 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: 24 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 12 sec Number of successful tactic applications: 15 Number of failed tactic applications: 9 Results for fold 123 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, 31 sec Number of successful tactic applications: 2202 Number of failed tactic applications: 7799 Results for fold 124 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, 21 sec Number of successful tactic applications: 1535 Number of failed tactic applications: 8466 Results for fold 125 Results for lemma fold_empty: : forall i, fold f empty i = i FAILURE! Tactics applied: 10000 Original Proof: [intros i; apply fold_1b; auto with set.] Proof search time: 0 min, 22 sec Number of successful tactic applications: 1329 Number of failed tactic applications: 8672 Results for fold 126 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, 29 sec Number of successful tactic applications: 1859 Number of failed tactic applications: 8142 Results for fold 127 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: 91 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 14 sec Number of successful tactic applications: 35 Number of failed tactic applications: 56 Results for fold 128 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: 4906 Original Proof: [intros; apply fold_equal; auto with set.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 20 sec Number of successful tactic applications: 1187 Number of failed tactic applications: 3719 Results for fold 129 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: 4823 Original Proof: [intros. apply fold_equal; auto with set.] Shorter Proof Found? no Proof reused from add_fold proof search time: 0 min, 21 sec Number of successful tactic applications: 960 Number of failed tactic applications: 3863 Results for fold 130 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, 43 sec Number of successful tactic applications: 2233 Number of failed tactic applications: 7768 Results for fold 131 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, 20 sec Number of successful tactic applications: 1318 Number of failed tactic applications: 8683 Results for fold 132 Results for lemma remove_singleton_empty: : In x s -> remove x s [=] empty -> singleton x [=] 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, 6 sec Number of successful tactic applications: 7 Number of failed tactic applications: 10 Results for fold 133 Results for lemma subset_equal: : s[=]s' -> s[<=]s' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 19 Original Proof: [fsetdec.] 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: 16 Results for fold 134 Results for lemma in_subset: : In x s1 -> s1[<=]s2 -> In x s2 SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 20 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 11 sec Number of successful tactic applications: 14 Number of failed tactic applications: 6 Results for fold 135 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: 85 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 5 sec Number of successful tactic applications: 18 Number of failed tactic applications: 67 Results for fold 136 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, 22 sec Number of successful tactic applications: 2273 Number of failed tactic applications: 7728 Results for fold 137 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, 25 sec Number of successful tactic applications: 1708 Number of failed tactic applications: 8293 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 612 tactics The longest proof consisted of 3 tactics There were 2 shorter proofs found Of the 59 failures, 59 of them used all 10000 tactics There were 71 reused proofs found There were 7 novel proofs found Of the 59 failures, the average number of tactics used was 10000 On average, a proof was found after 0 min, 9 sec On average, a failed proof attempt took 0 min, 25 sec On average, any (success or failure) proof attempt took 0 min, 16 sec The longest time to find a proof was 0 min, 24 sec The shortest time to find a proof was 0 min, 3 sec There were 0 proofs containing repeated tactics There were 2 proofs that repeated states