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