Results for fold 1
Results for lemma split_spec2: : forall s x y `{Ok s}, (InT y (split x s)#r <-> InT y s /\ X.lt x y)
FAILURE!
Tactics applied: 1380
Original Proof: [induct s x. intuition_in. intuition_in; order. specialize (IHl x y). destruct (split x l); simpl in *. rewrite join_spec, IHl; intuition_in; order. specialize (IHr x y). destruct (split x r); simpl in *. rewrite IHr; intuition_in; order.]
Proof search time: 0 min, 6 sec
Number of successful tactic applications: 271
Number of failed tactic applications: 1109
Results for lemma inter_spec_ok: : forall s1 s2 `{Ok s1, Ok s2}, Ok (inter s1 s2) /\ (forall y, InT y (inter s1 s2) <-> InT y s1 /\ InT y s2)
FAILURE!
Tactics applied: 1379
Original Proof: [intros s1 s2; functional induction inter s1 s2; intros B1 B2; [intuition_in|intuition_in | | ]; factornode s2; destruct_split; inv; destruct IHt0 as (IHo1,IHi1), IHt1 as (IHo2,IHi2); auto with *; split; intros. - apply join_ok; auto with *; intro y; rewrite ?IHi1, ?IHi2; intuition. - rewrite join_spec, IHi1, IHi2, split_spec1, split_spec2; intuition_in. setoid_replace y with x1; auto. rewrite <- split_spec3; auto. - apply concat_ok; auto with *; intros y1 y2; rewrite IHi1, IHi2; intuition; order. - rewrite concat_spec, IHi1, IHi2, split_spec1, split_spec2; auto. intuition_in. absurd (InT x1 s2). rewrite <- split_spec3; auto; congruence. setoid_replace x1 with y; auto.]
Proof search time: 0 min, 40 sec
Number of successful tactic applications: 625
Number of failed tactic applications: 754
Results for lemma split_spec1: : forall s x y `{Ok s}, (InT y (split x s)#l <-> InT y s /\ X.lt y x)
FAILURE!
Tactics applied: 1380
Original Proof: [induct s x. intuition_in. intuition_in; order. specialize (IHl x y). destruct (split x l); simpl in *. rewrite IHl; intuition_in; order. specialize (IHr x y). destruct (split x r); simpl in *. rewrite join_spec, IHr; intuition_in; order.]
Proof search time: 0 min, 5 sec
Number of successful tactic applications: 271
Number of failed tactic applications: 1109
Results for lemma join_spec: : forall l x r y, InT y (join l x r) <-> X.eq y x \/ InT y l \/ InT y r
FAILURE!
Tactics applied: 649
Original Proof: [join_tac. simpl. rewrite add_spec'; intuition_in. rewrite add_spec'; intuition_in. rewrite bal_spec, Hlr; clear Hlr Hrl; intuition_in. rewrite bal_spec, Hrl; clear Hlr Hrl; intuition_in. apply create_spec.]
Proof search time: 0 min, 18 sec
Number of successful tactic applications: 237
Number of failed tactic applications: 412
Results for lemma split_ok: : forall s x `{Ok s}, Ok (split x s)#l /\ Ok (split x s)#r
FAILURE!
Tactics applied: 1144
Original Proof: [induct s x; simpl; auto. specialize (IHl x). generalize (fun y => @split_spec2 l x y _). destruct (split x l); simpl in *; intuition. apply join_ok; auto. intros y; rewrite H; intuition. specialize (IHr x). generalize (fun y => @split_spec1 r x y _). destruct (split x r); simpl in *; intuition. apply join_ok; auto. intros y; rewrite H; intuition.]
Proof search time: 0 min, 7 sec
Number of successful tactic applications: 235
Number of failed tactic applications: 909
Results for lemma remove_min_gt_tree: : forall l x r h `{Ok (Node h l x r)}, gt_tree (remove_min l x r)#2 (remove_min l x r)#1
FAILURE!
Tactics applied: 1189
Original Proof: [intros l x r; functional induction (remove_min l x r); simpl; intros. inv; auto. assert (O : Ok (Node _x ll lx lr)) by (inv; auto). assert (L : lt_tree x (Node _x ll lx lr)) by (inv; auto). specialize IHp with (1:=O); rewrite e0 in IHp; simpl in IHp. intro y; rewrite bal_spec; intuition; specialize (L m); rewrite remove_min_spec, e0 in L; simpl in L; [setoid_replace y with x|inv]; eauto.]
Proof search time: 0 min, 32 sec
Number of successful tactic applications: 529
Number of failed tactic applications: 660
Results for fold 2
Results for lemma bal_spec: : forall l x r y, InT y (bal l x r) <-> X.eq y x \/ InT y l \/ InT y r
FAILURE!
Tactics applied: 10000
Original Proof: [intros l x r; functional induction bal l x r; intros; try clear e0; rewrite !create_spec; intuition_in.]
Proof search time: 0 min, 52 sec
Number of successful tactic applications: 3846
Number of failed tactic applications: 6155
Results for lemma diff_spec_ok: : forall s1 s2 `{Ok s1, Ok s2}, Ok (diff s1 s2) /\ (forall y, InT y (diff s1 s2) <-> InT y s1 /\ ~InT y s2)
FAILURE!
Tactics applied: 10000
Original Proof: [intros s1 s2; functional induction diff s1 s2; intros B1 B2; [intuition_in|intuition_in | | ]; factornode s2; destruct_split; inv; destruct IHt0 as (IHb1,IHi1), IHt1 as (IHb2,IHi2); auto with *; split; intros. - apply concat_ok; auto; intros y1 y2; rewrite IHi1, IHi2; intuition; order. - rewrite concat_spec, IHi1, IHi2, split_spec1, split_spec2; intuition_in. absurd (InT x1 s2). + setoid_replace x1 with y; auto. + rewrite <- split_spec3; auto; congruence. - apply join_ok; auto; intro y; rewrite ?IHi1, ?IHi2; intuition. - rewrite join_spec, IHi1, IHi2, split_spec1, split_spec2; auto with *. intuition_in. absurd (InT x1 s2); auto. * rewrite <- split_spec3; auto; congruence. * setoid_replace x1 with y; auto.]
Proof search time: 2 min, 18 sec
Number of successful tactic applications: 3974
Number of failed tactic applications: 6027
Results for lemma concat_spec: : forall s1 s2 y, InT y (concat s1 s2) <-> InT y s1 \/ InT y s2
FAILURE!
Tactics applied: 10000
Original Proof: [intros s1 s2; functional induction (concat s1 s2); intros; try factornode s1. intuition_in. intuition_in. rewrite join_spec, remove_min_spec, e1; simpl; intuition.]
Proof search time: 1 min, 7 sec
Number of successful tactic applications: 5511
Number of failed tactic applications: 4490
Results for lemma add_spec: : forall s x y `{Ok s}, InT y (add x s) <-> X.eq y x \/ InT y s
FAILURE!
Tactics applied: 10000
Original Proof: [intros; apply add_spec'.]
Proof search time: 3 min, 2 sec
Number of successful tactic applications: 4734
Number of failed tactic applications: 5267
Results for lemma union_spec: : forall s1 s2 y `{Ok s1, Ok s2}, (InT y (union s1 s2) <-> InT y s1 \/ InT y s2)
FAILURE!
Tactics applied: 10000
Original Proof: [intros s1 s2; functional induction union s1 s2; intros y B1 B2. intuition_in. intuition_in. factornode s2; destruct_split; inv. rewrite join_spec, IHt0, IHt1, split_spec1, split_spec2; auto with *. destruct (X.compare_spec y x1); intuition_in.]
Proof search time: 1 min, 9 sec
Number of successful tactic applications: 4705
Number of failed tactic applications: 5296
Results for lemma add_spec': : forall s x y, InT y (add x s) <-> X.eq y x \/ InT y s
FAILURE!
Tactics applied: 10000
Original Proof: [induct s x; try rewrite ?bal_spec, ?IHl, ?IHr; intuition_in. setoid_replace y with x'; eauto.]
Proof search time: 2 min, 16 sec
Number of successful tactic applications: 4745
Number of failed tactic applications: 5256
Results for fold 3
Results for lemma diff_spec: : forall s1 s2 y `{Ok s1, Ok s2}, (InT y (diff s1 s2) <-> InT y s1 /\ ~InT y s2)
FAILURE!
Tactics applied: 10000
Original Proof: [intros; destruct (@diff_spec_ok s1 s2); auto.]
Proof search time: 6 min, 25 sec
Number of successful tactic applications: 4070
Number of failed tactic applications: 5931
Results for lemma partition_spec1: s f : Proper (X.eq==>Logic.eq) f -> Equal (partition f s)#1 (filter f s)
FAILURE!
Tactics applied: 2781
Original Proof: [now rewrite partition_spec1'.]
Proof search time: 0 min, 20 sec
Number of successful tactic applications: 998
Number of failed tactic applications: 1783
Results for lemma singleton_spec: : forall x y, InT y (singleton x) <-> X.eq y x
FAILURE!
Tactics applied: 165
Original Proof: [unfold singleton; intuition_in.]
Proof search time: 0 min, 1 sec
Number of successful tactic applications: 12
Number of failed tactic applications: 153
Results for lemma filter_spec: : forall s x f, Proper (X.eq==>Logic.eq) f -> (InT x (filter f s) <-> InT x s /\ f x = true)
FAILURE!
Tactics applied: 10000
Original Proof: [induction s as [ |h l Hl x0 r Hr]; intros x f Hf; simpl. - intuition_in. - case_eq (f x0); intros Hx0. * rewrite join_spec, Hl, Hr; intuition_in. now setoid_replace x with x0. * rewrite concat_spec, Hl, Hr; intuition_in. assert (f x = f x0) by auto. congruence.]
Proof search time: 9 min, 58 sec
Number of successful tactic applications: 3688
Number of failed tactic applications: 6313
Results for lemma remove_spec: : forall s x y `{Ok s}, (InT y (remove x s) <-> InT y s /\ ~ X.eq y x)
FAILURE!
Tactics applied: 10000
Original Proof: [induct s x. intuition_in. rewrite merge_spec; intuition; [order|order|intuition_in]. elim H2; eauto. rewrite bal_spec, IHl; clear IHl IHr; intuition; [order|order|intuition_in]. rewrite bal_spec, IHr; clear IHl IHr; intuition; [order|order|intuition_in].]
Proof search time: 6 min, 33 sec
Number of successful tactic applications: 3916
Number of failed tactic applications: 6085
Results for lemma partition_spec2: s f : Proper (X.eq==>Logic.eq) f -> Equal (partition f s)#2 (filter (fun x => negb (f x)) s)
FAILURE!
Tactics applied: 2781
Original Proof: [now rewrite partition_spec2'.]
Proof search time: 0 min, 22 sec
Number of successful tactic applications: 998
Number of failed tactic applications: 1783
Results for fold 4
Results for lemma filter_weak_spec: : forall s x f, InT x (filter f s) -> InT x s
FAILURE!
Tactics applied: 10000
Original Proof: [induction s as [ |h l Hl x0 r Hr]; intros x f; simpl. - trivial. - destruct (f x0). * rewrite join_spec; intuition_in; eauto. * rewrite concat_spec; intuition_in; eauto.]
Proof search time: 1 min, 18 sec
Number of successful tactic applications: 1971
Number of failed tactic applications: 8030
Results for lemma create_spec: : forall l x r y, InT y (create l x r) <-> X.eq y x \/ InT y l \/ InT y r
FAILURE!
Tactics applied: 10000
Original Proof: [unfold create; split; [ inversion_clear 1 | ]; intuition.]
Proof search time: 2 min, 9 sec
Number of successful tactic applications: 1863
Number of failed tactic applications: 8138
Results for lemma merge_spec: : forall s1 s2 y, InT y (merge s1 s2) <-> InT y s1 \/ InT y s2
FAILURE!
Tactics applied: 10000
Original Proof: [intros s1 s2; functional induction (merge s1 s2); intros; try factornode s1. intuition_in. intuition_in. rewrite bal_spec, remove_min_spec, e1; simpl; intuition.]
Proof search time: 0 min, 56 sec
Number of successful tactic applications: 1995
Number of failed tactic applications: 8006
Results for lemma split_spec3: : forall s x `{Ok s}, ((split x s)#b = true <-> InT x s)
FAILURE!
Tactics applied: 10000
Original Proof: [induct s x. intuition_in; try discriminate. intuition. specialize (IHl x). destruct (split x l); simpl in *. rewrite IHl; intuition_in; order. specialize (IHr x). destruct (split x r); simpl in *. rewrite IHr; intuition_in; order.]
Proof search time: 0 min, 45 sec
Number of successful tactic applications: 1799
Number of failed tactic applications: 8202
Results for lemma remove_min_spec: : forall l x r y h, InT y (Node h l x r) <-> X.eq y (remove_min l x r)#2 \/ InT y (remove_min l x r)#1
FAILURE!
Tactics applied: 10000
Original Proof: [intros l x r; functional induction (remove_min l x r); simpl in *; intros. intuition_in. rewrite bal_spec, In_node_iff, IHp, e0; simpl; intuition.]
Proof search time: 2 min, 13 sec
Number of successful tactic applications: 2116
Number of failed tactic applications: 7885
Results for lemma partition_spec1': s f : (partition f s)#1 = filter f s
FAILURE!
Tactics applied: 43
Original Proof: [induction s as [ | h l Hl x r Hr ]; simpl. - trivial. - rewrite <- Hl, <- Hr. now destruct (partition f l), (partition f r), (f x).]
Proof search time: 0 min, 0 sec
Number of successful tactic applications: 12
Number of failed tactic applications: 31
Results for fold 5
Results for lemma inter_spec: : forall s1 s2 y `{Ok s1, Ok s2}, (InT y (inter s1 s2) <-> InT y s1 /\ InT y s2)
FAILURE!
Tactics applied: 10000
Original Proof: [intros; destruct (@inter_spec_ok s1 s2); auto.]
Proof search time: 2 min, 51 sec
Number of successful tactic applications: 3853
Number of failed tactic applications: 6148
Results for lemma partition_spec2': s f : (partition f s)#2 = filter (fun x => negb (f x)) s
FAILURE!
Tactics applied: 2549
Original Proof: [induction s as [ | h l Hl x r Hr ]; simpl. - trivial. - rewrite <- Hl, <- Hr. now destruct (partition f l), (partition f r), (f x).]
Proof search time: 0 min, 27 sec
Number of successful tactic applications: 530
Number of failed tactic applications: 2019
OVERALL RESULTS SUMMARY
EFSMProver proved 0 out of 26 lemmas. Success rate of 0.0%
There were 0 errors.
26 proof attempts exhausted the automaton
The longest proof consisted of 0 tactics
There were 0 shorter proofs found
Of the 26 failures, 15 of them used all 10000 tactics
There were 0 reused proofs found
There were 0 novel proofs found
Of the 26 failures, the average number of tactics used was 6363
On average, a proof was found after 0 min, 0 sec
On average, a failed proof attempt took 1 min, 48 sec
On average, any (success or failure) proof attempt took 1 min, 48 sec
The longest time to find a proof was 0 min, 0 sec
The shortest time to find a proof was 0 min, 10 sec
There were 0 proofs containing repeated tactics
There were 0 proofs that repeated states