Results for fold 1 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, 25 sec Number of successful tactic applications: 2097 Number of failed tactic applications: 7904 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, 21 sec Number of successful tactic applications: 1791 Number of failed tactic applications: 8210 Results for lemma empty_union_1: : 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, 5 sec Number of successful tactic applications: 19 Number of failed tactic applications: 19 Results for lemma Add_remove: : In x s -> Add x (remove x s) s SUCCESS! Proof Found in EFSM: expAdd ; fsetdec. Tactics applied: 192 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: 61 Number of failed tactic applications: 131 Results for lemma singleton_equal_add: : singleton x [=] add x empty 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, 5 sec Number of successful tactic applications: 5 Number of failed tactic applications: 33 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, 5 sec Number of successful tactic applications: 5 Number of failed tactic applications: 33 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, 19 sec Number of successful tactic applications: 1532 Number of failed tactic applications: 8469 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, 21 sec Number of successful tactic applications: 2038 Number of failed tactic applications: 7963 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, 32 sec Number of successful tactic applications: 2645 Number of failed tactic applications: 7356 Results for lemma inter_subset_1: : 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, 5 sec Number of successful tactic applications: 5 Number of failed tactic applications: 33 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, 5 sec Number of successful tactic applications: 5 Number of failed tactic applications: 33 Results for lemma remove_add: : ~In x s -> remove x (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, 5 sec Number of successful tactic applications: 17 Number of failed tactic applications: 21 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, 22 sec Number of successful tactic applications: 1260 Number of failed tactic applications: 8741 Results for lemma inter_subset_equal: : 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, 5 sec Number of successful tactic applications: 17 Number of failed tactic applications: 21 Results for lemma union_subset_3: : s[<=]s'' -> s'[<=]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, 5 sec Number of successful tactic applications: 17 Number of failed tactic applications: 21 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, 21 sec Number of successful tactic applications: 2045 Number of failed tactic applications: 7956 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 with set. Tactics applied: 917 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, 5 sec Number of successful tactic applications: 72 Number of failed tactic applications: 845 Results for lemma equal_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, 5 sec Number of successful tactic applications: 17 Number of failed tactic applications: 21 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, 16 sec Number of successful tactic applications: 997 Number of failed tactic applications: 9004 Results for lemma in_subset: : In x s1 -> s1[<=]s2 -> In x s2 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, 5 sec Number of successful tactic applications: 17 Number of failed tactic applications: 21 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: 190 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: 65 Number of failed tactic applications: 125 Results for lemma union_subset_4: : s[<=]s' -> union s 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, 5 sec Number of successful tactic applications: 17 Number of failed tactic applications: 21 Results for lemma diff_subset: : diff 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, 5 sec Number of successful tactic applications: 5 Number of failed tactic applications: 33 Results for lemma remove_diff_singleton: : remove x s [=] diff s (singleton x) 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, 5 sec Number of successful tactic applications: 5 Number of failed tactic applications: 33 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: 1738 Number of failed tactic applications: 8263 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: 38 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 5 sec Number of successful tactic applications: 17 Number of failed tactic applications: 21 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: 2121 Number of failed tactic applications: 7880 Results for lemma equal_sym: : 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, 5 sec Number of successful tactic applications: 17 Number of failed tactic applications: 21 Results for fold 2 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, 13 sec Number of successful tactic applications: 1503 Number of failed tactic applications: 8498 Results for lemma empty_diff_1: : Empty s -> Empty (diff s s') 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, 1 sec Number of successful tactic applications: 13 Number of failed tactic applications: 45 Results for lemma add_add: : add x (add x' s) [=] add x' (add x s) 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, 1 sec Number of successful tactic applications: 13 Number of failed tactic applications: 45 Results for lemma union_subset_2: : s' [<=] union s s' 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, 1 sec Number of successful tactic applications: 11 Number of failed tactic applications: 47 Results for lemma union_sym: : union s s' [=] union s' s 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, 1 sec Number of successful tactic applications: 13 Number of failed tactic applications: 45 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, 14 sec Number of successful tactic applications: 1424 Number of failed tactic applications: 8577 Results for lemma diff_inter_empty: : inter (diff s s') (inter s s') [=] empty 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, 1 sec Number of successful tactic applications: 13 Number of failed tactic applications: 45 Results for lemma add_union_singleton: : add x s [=] union (singleton x) s 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, 1 sec Number of successful tactic applications: 13 Number of failed tactic applications: 45 Results for lemma empty_inter_2: : Empty s' -> Empty (inter s s') 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, 1 sec Number of successful tactic applications: 13 Number of failed tactic applications: 45 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, 19 sec Number of successful tactic applications: 2153 Number of failed tactic applications: 7848 Results for lemma empty_diff_2: : Empty s -> diff s' s [=] s' 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, 1 sec Number of successful tactic applications: 15 Number of failed tactic applications: 43 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, 21 sec Number of successful tactic applications: 1628 Number of failed tactic applications: 8373 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, 16 sec Number of successful tactic applications: 1759 Number of failed tactic applications: 8242 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, 16 sec Number of successful tactic applications: 1816 Number of failed tactic applications: 8185 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, 14 sec Number of successful tactic applications: 1295 Number of failed tactic applications: 8706 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, 14 sec Number of successful tactic applications: 1906 Number of failed tactic applications: 8095 Results for lemma add_cardinal_1: : forall s x, In x s -> cardinal (add x s) = cardinal s SUCCESS! Proof Found in EFSM: intuition. Tactics applied: 61 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 1 sec Number of successful tactic applications: 6 Number of failed tactic applications: 55 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: 147 Original Proof: [expAdd; fsetdec.] Shorter Proof Found? no Proof reused from Add_add proof search time: 0 min, 1 sec Number of successful tactic applications: 26 Number of failed tactic applications: 121 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, 20 sec Number of successful tactic applications: 1775 Number of failed tactic applications: 8226 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) SUCCESS! Proof Found in EFSM: symmetry ; apply fold_2 with (eqA := eqA); auto with *. Tactics applied: 7071 Original Proof: [intros. symmetry. apply fold_2 with (eqA:=eqA); auto with set relations.] Shorter Proof Found? yes 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: 1335 Number of failed tactic applications: 5736 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: 4283 Original Proof: [intros. apply fold_equal; auto with set.] Shorter Proof Found? no Proof reused from add_fold proof search time: 0 min, 9 sec Number of successful tactic applications: 713 Number of failed tactic applications: 3570 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, 14 sec Number of successful tactic applications: 1161 Number of failed tactic applications: 8840 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: 1299 Number of failed tactic applications: 8702 Results for lemma subset_remove_3: : s1[<=]s2 -> remove x s1 [<=] s2 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, 1 sec Number of successful tactic applications: 11 Number of failed tactic applications: 47 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: 147 Original Proof: [expAdd; fsetdec.] Shorter Proof Found? no Proof reused from Add_add proof search time: 0 min, 1 sec Number of successful tactic applications: 30 Number of failed tactic applications: 117 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, 14 sec Number of successful tactic applications: 1259 Number of failed tactic applications: 8742 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: 4239 Original Proof: [intros; apply fold_equal; auto with set.] Shorter Proof Found? no Proof reused from add_fold proof search time: 0 min, 9 sec Number of successful tactic applications: 683 Number of failed tactic applications: 3556 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, 17 sec Number of successful tactic applications: 1507 Number of failed tactic applications: 8494 Results for fold 3 Results for lemma Equal_remove: : s[=]s' -> remove 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, 4 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 Results for lemma union_assoc: : union (union s s') s'' [=] union 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, 4 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 Results for lemma empty_inter_1: : 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, 4 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 Results for lemma diff_inter_all: : union (diff s s') (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, 4 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 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, 17 sec Number of successful tactic applications: 1357 Number of failed tactic applications: 8644 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, 25 sec Number of successful tactic applications: 2012 Number of failed tactic applications: 7989 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, 4 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 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, 4 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 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: 50 Original Proof: [auto with set.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 4 sec Number of successful tactic applications: 17 Number of failed tactic applications: 33 Results for lemma union_subset_1: : 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, 4 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 Results for lemma inter_subset_2: : 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, 4 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 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, 19 sec Number of successful tactic applications: 1854 Number of failed tactic applications: 8147 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, 16 sec Number of successful tactic applications: 1282 Number of failed tactic applications: 8719 Results for lemma empty_is_empty_2: : s[=]empty -> Empty 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 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, 19 sec Number of successful tactic applications: 1401 Number of failed tactic applications: 8600 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, 16 sec Number of successful tactic applications: 1665 Number of failed tactic applications: 8336 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, 17 sec Number of successful tactic applications: 1649 Number of failed tactic applications: 8352 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, 22 sec Number of successful tactic applications: 1713 Number of failed tactic applications: 8288 Results for lemma add_equal: : In x s -> add x 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 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, 17 sec Number of successful tactic applications: 1335 Number of failed tactic applications: 8666 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, 22 sec Number of successful tactic applications: 2146 Number of failed tactic applications: 7855 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, 17 sec Number of successful tactic applications: 1830 Number of failed tactic applications: 8171 Results for lemma Add_add: : Add x s (add x s) SUCCESS! Proof Found in EFSM: expAdd ; fsetdec. Tactics applied: 165 Original Proof: [expAdd; fsetdec.] Shorter Proof Found? no Proof reused from inter_Add proof search time: 0 min, 4 sec Number of successful tactic applications: 13 Number of failed tactic applications: 152 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, 17 sec Number of successful tactic applications: 1405 Number of failed tactic applications: 8596 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: 1542 Number of failed tactic applications: 8459 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, 4 sec Number of successful tactic applications: 1 Number of failed tactic applications: 0 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, 19 sec Number of successful tactic applications: 1347 Number of failed tactic applications: 8654 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: 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 fold 4 Results for lemma subset_antisym: : s[<=]s' -> s'[<=]s -> s[=]s' SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 35 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Number of successful tactic applications: 16 Number of failed tactic applications: 19 Results for lemma remove_singleton_empty: : In x s -> remove x s [=] empty -> singleton x [=] s SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 35 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Number of successful tactic applications: 16 Number of failed tactic applications: 19 Results for lemma subset_trans: : s1[<=]s2 -> s2[<=]s3 -> s1[<=]s3 SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 35 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Number of successful tactic applications: 12 Number of failed tactic applications: 23 Results for lemma empty_is_empty_1: : Empty s -> s[=]empty SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 35 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Number of successful tactic applications: 16 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: symmetry ; apply fold_equal; intuition fsetdec. Tactics applied: 3688 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, 10 sec Number of successful tactic applications: 706 Number of failed tactic applications: 2982 Results for lemma fold_empty: : forall i, fold f empty i = i SUCCESS! Proof Found in EFSM: symmetry ; apply fold_rec; intuition fsetdec. Tactics applied: 1241 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, 4 sec Number of successful tactic applications: 178 Number of failed tactic applications: 1063 Results for lemma union_subset_equal: : s[<=]s' -> union s s' [=] s' SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 35 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Number of successful tactic applications: 16 Number of failed tactic applications: 19 Results for lemma union_equal_2: : s'[=]s'' -> union s s' [=] union s s'' SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 35 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Number of successful tactic applications: 16 Number of failed tactic applications: 19 Results for lemma subset_diff: : s1[<=]s3 -> diff s1 s2 [<=] s3 SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 35 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Number of successful tactic applications: 12 Number of failed tactic applications: 23 Results for lemma inter_equal_2: : s'[=]s'' -> inter s s' [=] inter s s'' SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 35 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Number of successful tactic applications: 16 Number of failed tactic applications: 19 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, 21 sec Number of successful tactic applications: 1585 Number of failed tactic applications: 8416 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, 18 sec Number of successful tactic applications: 1593 Number of failed tactic applications: 8408 Results for lemma empty_cardinal: : cardinal empty = 0 SUCCESS! Proof Found in EFSM: apply cardinal_1. intuition. Tactics applied: 195 Original Proof: [rewrite cardinal_fold; apply fold_1; auto with *.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 3 sec Number of successful tactic applications: 10 Number of failed tactic applications: 185 Results for lemma union_inter_1: : inter (union s s') s'' [=] union (inter s s'') (inter s' s'') SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 35 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Number of successful tactic applications: 15 Number of failed tactic applications: 20 Results for lemma equal_refl: : s[=]s SUCCESS! Proof Found in EFSM: reflexivity. Tactics applied: 24 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Number of successful tactic applications: 11 Number of failed tactic applications: 13 Results for lemma subset_equal: : s[=]s' -> s[<=]s' SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 35 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Number of successful tactic applications: 12 Number of failed tactic applications: 23 Results for lemma add_remove: : In x s -> add x (remove x s) [=] s SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 35 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Number of successful tactic applications: 16 Number of failed tactic applications: 19 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, 23 sec Number of successful tactic applications: 1700 Number of failed tactic applications: 8301 Results for lemma inter_equal_1: : s[=]s' -> inter s s'' [=] inter s' s'' SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 35 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Number of successful tactic applications: 16 Number of failed tactic applications: 19 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, 16 sec Number of successful tactic applications: 1482 Number of failed tactic applications: 8519 Results for lemma empty_union_2: : Empty s -> union s' s [=] s' SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 35 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Number of successful tactic applications: 16 Number of failed tactic applications: 19 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, 12 sec Number of successful tactic applications: 970 Number of failed tactic applications: 9031 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; intuition. Tactics applied: 3687 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, 10 sec Number of successful tactic applications: 705 Number of failed tactic applications: 2982 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, 17 sec Number of successful tactic applications: 1238 Number of failed tactic applications: 8763 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, 16 sec Number of successful tactic applications: 1230 Number of failed tactic applications: 8771 Results for lemma inter_sym: : inter s s' [=] inter s' s SUCCESS! Proof Found in EFSM: intuition fsetdec. Tactics applied: 35 Original Proof: [fsetdec.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Number of successful tactic applications: 15 Number of failed tactic applications: 20 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. rewrite 2 fold_spec_right. apply (@fold_right_eqlistA E.t E.eq A eqA st); auto. apply eqlistA_rev. apply sort_equivlistA_eqlistA; auto with set. red; intro a; do 2 rewrite <- elements_iff; auto.] Proof search time: 0 min, 23 sec Number of successful tactic applications: 2421 Number of failed tactic applications: 7580 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, 15 sec Number of successful tactic applications: 1311 Number of failed tactic applications: 8690 Results for fold 5 Results for lemma union_subset_5: : s[<=]s' -> union s'' s [<=] union s'' s' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 26 Original Proof: [fsetdec.] 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: 8 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: 26 Original Proof: [fsetdec.] 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: 8 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, 26 sec Number of successful tactic applications: 1912 Number of failed tactic applications: 8089 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, 19 sec Number of successful tactic applications: 1819 Number of failed tactic applications: 8182 Results for lemma fold_identity: : forall s, fold add s empty [=] s SUCCESS! Proof Found in EFSM: intros ; apply fold_rec_bis; fsetdec. Tactics applied: 3956 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 This proof contained a loop around a state proof search time: 0 min, 12 sec Number of successful tactic applications: 931 Number of failed tactic applications: 3025 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: 6977 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 proof search time: 0 min, 16 sec Number of successful tactic applications: 1209 Number of failed tactic applications: 5768 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: 146 Original Proof: [expAdd; fsetdec.] Shorter Proof Found? no Proof reused from Add_remove proof search time: 0 min, 5 sec Number of successful tactic applications: 39 Number of failed tactic applications: 107 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: 26 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: 23 Results for lemma subset_refl: : s[<=]s SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 26 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: 23 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: 3547 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, 10 sec Number of successful tactic applications: 695 Number of failed tactic applications: 2852 Results for lemma union_equal_1: : s[=]s' -> union s s'' [=] union s' s'' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 26 Original Proof: [fsetdec.] 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: 8 Results for lemma double_inclusion: : s1[=]s2 <-> s1[<=]s2 /\ s2[<=]s1 SUCCESS! Proof Found in EFSM: intuition ; fsetdec. Tactics applied: 487 Original Proof: [intuition fsetdec.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 6 sec Number of successful tactic applications: 114 Number of failed tactic applications: 373 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, 18 sec Number of successful tactic applications: 2128 Number of failed tactic applications: 7873 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, 46 sec Number of successful tactic applications: 1987 Number of failed tactic applications: 8014 Results for lemma union_add: : union (add x s) s' [=] add x (union s s') SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 26 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: 23 Results for lemma inter_subset_3: : s''[<=]s -> s''[<=]s' -> s''[<=] inter s s' SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 26 Original Proof: [fsetdec.] 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: 8 Results for lemma diff_subset_equal: : s[<=]s' -> diff s s' [=] empty SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 26 Original Proof: [fsetdec.] 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: 8 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, 22 sec Number of successful tactic applications: 1648 Number of failed tactic applications: 8353 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, 30 sec Number of successful tactic applications: 2089 Number of failed tactic applications: 7912 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: 1 min, 5 sec Number of successful tactic applications: 1527 Number of failed tactic applications: 8474 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. rewrite 2 fold_spec_right. apply (@fold_right_eqlistA E.t E.eq A eqA st); auto. apply eqlistA_rev. apply sort_equivlistA_eqlistA; auto with set. red; intro a; do 2 rewrite <- elements_iff; auto.] Proof search time: 0 min, 24 sec Number of successful tactic applications: 2440 Number of failed tactic applications: 7561 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: 26 Original Proof: [fsetdec.] 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: 8 Results for lemma remove_equal: : ~ In x s -> remove x s [=] s SUCCESS! Proof Found in EFSM: fsetdec. Tactics applied: 26 Original Proof: [fsetdec.] 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: 8 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, 21 sec Number of successful tactic applications: 1431 Number of failed tactic applications: 8570 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, 21 sec Number of successful tactic applications: 1493 Number of failed tactic applications: 8508 OVERALL RESULTS SUMMARY EFSMProver proved 81 out of 137 lemmas. Success rate of 59.12408759124088% There were 0 errors. 56 proof attempts exhausted the automaton On average, a proof was found after applying 534 tactics The longest proof consisted of 3 tactics There were 5 shorter proofs found Of the 56 failures, 56 of them used all 10000 tactics There were 71 reused proofs found There were 10 novel proofs found Of the 56 failures, the average number of tactics used was 10000 On average, a proof was found after 0 min, 4 sec On average, a failed proof attempt took 0 min, 20 sec On average, any (success or failure) proof attempt took 0 min, 11 sec The longest time to find a proof was 0 min, 16 sec The shortest time to find a proof was 0 min, 1 sec There were 0 proofs containing repeated tactics There were 6 proofs that repeated states