Results for fold 1
Results for lemma empty_spec: : Empty empty
SUCCESS!
Proof Found in EFSM: unfold empty; intros s s'; inv ;
Tactics applied: 353
Original Proof: [unfold Empty, empty; red; intros; inv.]
Shorter Proof Found? yes
This is a novel proof
proof search time: 0 min, 2 sec
Number of successful tactic applications: 138
Number of failed tactic applications: 215
Results for lemma elements_spec1: : forall (s : t) (x : elt), In x (elements s) <-> In x s
SUCCESS!
Proof Found in EFSM: reflexivity.
Tactics applied: 6
Original Proof: [unfold elements; intuition.]
Shorter Proof Found? yes
Single step proof reused
proof search time: 0 min, 2 sec
Number of successful tactic applications: 5
Number of failed tactic applications: 1
Results for lemma elements_spec2w: : forall (s : t) {Hs : Ok s}, NoDup (elements s)
SUCCESS!
Proof Found in EFSM: auto ;
Tactics applied: 27
Original Proof: [unfold elements; auto.]
Shorter Proof Found? yes
Single step proof reused
proof search time: 0 min, 2 sec
Number of successful tactic applications: 5
Number of failed tactic applications: 22
Results for lemma In_compat: : Proper (X.eq==>eq==>iff) In
FAILURE!
Tactics applied: 33
Original Proof: [repeat red; intros. subst. rewrite H; auto.]
Proof search time: 0 min, 2 sec
Number of successful tactic applications: 0
Number of failed tactic applications: 33
Results for lemma singleton_ok: : forall x : elt, Ok (singleton x)
SUCCESS!
Proof Found in EFSM: intuition.
Tactics applied: 33
Original Proof: [unfold singleton; simpl; constructors; auto. intro; inv.]
Shorter Proof Found? yes
Single step proof reused
proof search time: 0 min, 2 sec
Number of successful tactic applications: 3
Number of failed tactic applications: 30
Results for lemma remove_spec: : forall (s : t) (x y : elt) {Hs : Ok s}, In y (remove x s) <-> In y s /\ ~X.eq y x
FAILURE!
Tactics applied: 10000
Original Proof: [induction s; simpl; intros. intuition; inv; auto. destruct X.eq_dec; inv; rewrite !InA_cons, ?IHs; intuition. elim H. setoid_replace a with y; eauto. elim H3. setoid_replace x with y; eauto. elim n. eauto.]
Proof search time: 1 min, 4 sec
Number of successful tactic applications: 5156
Number of failed tactic applications: 4845
Results for fold 2
Results for lemma partition_spec1: : forall (s : t) (f : elt -> bool), Proper (X.eq==>eq) f -> Equal (fst (partition f s)) (filter f s)
FAILURE!
Tactics applied: 10000
Original Proof: [simple induction s; simpl; auto; unfold Equal. firstorder. intros x l Hrec f Hf. generalize (Hrec f Hf); clear Hrec. case (partition f l); intros s1 s2; simpl; intros. case (f x); simpl; firstorder; inversion H0; intros; firstorder.]
Proof search time: 0 min, 40 sec
Number of successful tactic applications: 5347
Number of failed tactic applications: 4654
Results for lemma inter_spec: : forall (s s' : t) (x : elt) {Hs : Ok s} {Hs' : Ok s'}, In x (inter s s') <-> In x s /\ In x s'
FAILURE!
Tactics applied: 10000
Original Proof: [unfold inter, fold, flip; intros. set (acc := nil (A:=elt)) in *. assert (Hacc : Ok acc) by constructors. assert (IFF : (In x s /\ In x s') <-> (In x s /\ In x s') \/ In x acc). intuition; unfold acc in *; inv. rewrite IFF; clear IFF. clearbody acc. revert acc Hacc x s' Hs Hs'. induction s; simpl; intros. intuition; inv. inv. case_eq (mem a s'); intros Hm. rewrite IHs, add_spec, InA_cons; intuition. rewrite mem_spec in Hm; auto. left; split; auto. rewrite H1; auto. rewrite IHs, InA_cons; intuition. rewrite H2, <- mem_spec in H3; auto. congruence.]
Proof search time: 2 min, 21 sec
Number of successful tactic applications: 4142
Number of failed tactic applications: 5859
Results for lemma diff_spec: : forall (s s' : t) (x : elt) {Hs : Ok s} {Hs' : Ok s'}, In x (diff s s') <-> In x s /\ ~In x s'
FAILURE!
Tactics applied: 10000
Original Proof: [unfold diff; intros s s'; revert s. induction s'; simpl; unfold flip. intuition; inv. intros. inv. rewrite IHs', remove_spec, InA_cons; intuition.]
Proof search time: 2 min, 27 sec
Number of successful tactic applications: 4088
Number of failed tactic applications: 5913
Results for lemma exists_spec: : forall (s : t) (f : elt -> bool), Proper (X.eq==>eq) f -> (exists_ f s = true <-> Exists (fun x => f x = true) s)
FAILURE!
Tactics applied: 10000
Original Proof: [unfold Exists; induction s; simpl. split; [discriminate| intros (x & Hx & _); inv]. intros. destruct (f a) eqn:F. split; auto. exists a; auto. rewrite IHs; firstorder. inv. setoid_replace a with x in F; auto; congruence. exists x; auto.]
Proof search time: 1 min, 4 sec
Number of successful tactic applications: 4473
Number of failed tactic applications: 5528
Results for lemma subset_spec: : forall (s s' : t) {Hs : Ok s} {Hs' : Ok s'}, subset s s' = true <-> Subset s s'
FAILURE!
Tactics applied: 10000
Original Proof: [unfold subset, Subset; intros. rewrite is_empty_spec. unfold Empty; intros. intuition. specialize (H a). rewrite diff_spec in H; intuition. rewrite <- (mem_spec a) in H |- *. destruct (mem a s'); intuition. rewrite diff_spec in H0; intuition.]
Proof search time: 0 min, 36 sec
Number of successful tactic applications: 4098
Number of failed tactic applications: 5903
Results for lemma singleton_spec: : forall x y : elt, In y (singleton x) <-> X.eq y x
SUCCESS!
Proof Found in EFSM: unfold singleton; intuition ; inv ; auto.
Tactics applied: 541
Original Proof: [unfold singleton; simpl; split; intros. inv; auto. left; auto.]
Shorter Proof Found? yes
This is a novel proof
proof search time: 0 min, 1 sec
Number of successful tactic applications: 245
Number of failed tactic applications: 296
Results for fold 3
Results for lemma isok_iff: : forall l, Ok l <-> isok l = true
FAILURE!
Tactics applied: 31
Original Proof: [induction l. intuition. simpl. rewrite andb_true_iff. rewrite negb_true_iff. rewrite <- IHl. split; intros H. inv. split; auto. apply not_true_is_false. rewrite mem_spec; auto. destruct H; constructors; auto. rewrite <- mem_spec; auto; congruence.]
Proof search time: 0 min, 0 sec
Number of successful tactic applications: 4
Number of failed tactic applications: 27
Results for lemma union_spec: : forall (s s' : t) (x : elt) {Hs : Ok s} {Hs' : Ok s'}, In x (union s s') <-> In x s \/ In x s'
FAILURE!
Tactics applied: 10000
Original Proof: [induction s; simpl in *; unfold flip; intros; auto; inv. intuition; inv. rewrite IHs, add_spec, InA_cons; intuition.]
Proof search time: 1 min, 27 sec
Number of successful tactic applications: 4642
Number of failed tactic applications: 5359
Results for lemma fold_spec: : forall (s : t) (A : Type) (i : A) (f : elt -> A -> A), fold f s i = fold_left (flip f) (elements s) i
SUCCESS!
Proof Found in EFSM: auto.
Tactics applied: 27
Original Proof: [reflexivity.]
Shorter Proof Found? no
Single step proof reused
proof search time: 0 min, 0 sec
Number of successful tactic applications: 9
Number of failed tactic applications: 18
Results for lemma equal_spec: : forall (s s' : t) {Hs : Ok s} {Hs' : Ok s'}, equal s s' = true <-> Equal s s'
FAILURE!
Tactics applied: 10000
Original Proof: [unfold Equal, equal; intros. rewrite andb_true_iff, !subset_spec. unfold Subset; intuition. rewrite <- H; auto. rewrite H; auto.]
Proof search time: 0 min, 35 sec
Number of successful tactic applications: 4517
Number of failed tactic applications: 5484
Results for lemma filter_spec': : forall s x f, In x (filter f s) -> In x s
FAILURE!
Tactics applied: 10000
Original Proof: [induction s; simpl. intuition; inv. intros; destruct (f a); inv; intuition; right; eauto.]
Proof search time: 0 min, 36 sec
Number of successful tactic applications: 4988
Number of failed tactic applications: 5013
Results for lemma is_empty_spec: : forall s : t, is_empty s = true <-> Empty s
FAILURE!
Tactics applied: 10000
Original Proof: [unfold Empty; destruct s; simpl; split; intros; auto. intro; inv. discriminate. elim (H e); auto.]
Proof search time: 0 min, 30 sec
Number of successful tactic applications: 4244
Number of failed tactic applications: 5757
Results for fold 4
Results for lemma filter_spec: : forall (s : t) (x : elt) (f : elt -> bool), Proper (X.eq==>eq) f -> (In x (filter f s) <-> In x s /\ f x = true)
FAILURE!
Tactics applied: 10000
Original Proof: [induction s; simpl. intuition; inv. intros. destruct (f a) eqn:E; rewrite ?InA_cons, IHs; intuition. setoid_replace x with a; auto. setoid_replace a with x in E; auto. congruence.]
Proof search time: 1 min, 42 sec
Number of successful tactic applications: 6494
Number of failed tactic applications: 3507
Results for lemma empty_ok: : Ok empty
SUCCESS!
Proof Found in EFSM: unfold Empty, empty; intuition.
Tactics applied: 49
Original Proof: [unfold empty; constructors.]
Shorter Proof Found? no
This is a novel proof
proof search time: 0 min, 2 sec
Number of successful tactic applications: 15
Number of failed tactic applications: 34
Results for lemma partition_ok2': : forall (s : t) {Hs : Ok s} (f : elt -> bool)(x:elt), In x (snd (partition f s)) -> In x s
FAILURE!
Tactics applied: 10000
Original Proof: [induction s; simpl; auto; intros. inv. generalize (IHs H1 f x). destruct (f a); destruct (partition f s); simpl in *; auto. inversion_clear H; auto.]
Proof search time: 0 min, 51 sec
Number of successful tactic applications: 5846
Number of failed tactic applications: 4155
Results for lemma partition_ok1': : forall (s : t) {Hs : Ok s} (f : elt -> bool)(x:elt), In x (fst (partition f s)) -> In x s
FAILURE!
Tactics applied: 10000
Original Proof: [induction s; simpl; auto; intros. inv. generalize (IHs H1 f x). destruct (f a); destruct (partition f s); simpl in *; auto. inversion_clear H; auto.]
Proof search time: 0 min, 51 sec
Number of successful tactic applications: 5846
Number of failed tactic applications: 4155
Results for lemma cardinal_spec: : forall (s : t) {Hs : Ok s}, cardinal s = length (elements s)
SUCCESS!
Proof Found in EFSM: reflexivity.
Tactics applied: 25
Original Proof: [auto.]
Shorter Proof Found? no
Single step proof reused
proof search time: 0 min, 2 sec
Number of successful tactic applications: 5
Number of failed tactic applications: 20
Results for lemma partition_spec2: : forall (s : t) (f : elt -> bool), Proper (X.eq==>eq) f -> Equal (snd (partition f s)) (filter (fun x => negb (f x)) s)
FAILURE!
Tactics applied: 10000
Original Proof: [simple induction s; simpl; auto; unfold Equal. firstorder. intros x l Hrec f Hf. generalize (Hrec f Hf); clear Hrec. case (partition f l); intros s1 s2; simpl; intros. case (f x); simpl; firstorder; inversion H0; intros; firstorder.]
Proof search time: 0 min, 47 sec
Number of successful tactic applications: 5494
Number of failed tactic applications: 4507
Results for fold 5
Results for lemma for_all_spec: : forall (s : t) (f : elt -> bool), Proper (X.eq==>eq) f -> (for_all f s = true <-> For_all (fun x => f x = true) s)
FAILURE!
Tactics applied: 10000
Original Proof: [unfold For_all; induction s; simpl. intuition. inv. intros; inv. destruct (f a) eqn:F. rewrite IHs; intuition. inv; auto. setoid_replace x with a; auto. split; intros H'; try discriminate. intros. rewrite <- F, <- (H' a); auto.]
Proof search time: 0 min, 24 sec
Number of successful tactic applications: 5178
Number of failed tactic applications: 4823
Results for lemma mem_spec: : forall s x `{Ok s}, mem x s = true <-> In x s
FAILURE!
Tactics applied: 10000
Original Proof: [induction s; intros. split; intros; inv. discriminate. simpl; destruct (X.eq_dec x a); split; intros; inv; auto. right; rewrite <- IHs; auto. rewrite IHs; auto.]
Proof search time: 0 min, 22 sec
Number of successful tactic applications: 5440
Number of failed tactic applications: 4561
Results for lemma add_spec: : forall (s : t) (x y : elt) {Hs : Ok s}, In y (add x s) <-> X.eq y x \/ In y s
FAILURE!
Tactics applied: 10000
Original Proof: [induction s; simpl; intros. intuition; inv; auto. destruct X.eq_dec; inv; rewrite InA_cons, ?IHs; intuition. left; eauto. inv; auto.]
Proof search time: 0 min, 25 sec
Number of successful tactic applications: 5423
Number of failed tactic applications: 4578
OVERALL RESULTS SUMMARY
EFSMProver proved 8 out of 27 lemmas. Success rate of 29.629629629629626%
There were 0 errors.
19 proof attempts exhausted the automaton
On average, a proof was found after applying 132 tactics
The longest proof consisted of 4 tactics
There were 5 shorter proofs found
Of the 19 failures, 17 of them used all 10000 tactics
There were 5 reused proofs found
There were 3 novel proofs found
Of the 19 failures, the average number of tactics used was 8950
On average, a proof was found after 0 min, 2 sec
On average, a failed proof attempt took 0 min, 53 sec
On average, any (success or failure) proof attempt took 0 min, 38 sec
The longest time to find a proof was 0 min, 2 sec
The shortest time to find a proof was 0 min, 0 sec
There were 0 proofs containing repeated tactics
There were 0 proofs that repeated states