Results for fold 1 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; intros. firstorder. discriminate. inv. destruct (f a) eqn:F. firstorder. rewrite IHs; auto. firstorder. inv. setoid_replace a with x in F; auto; congruence. exists x; auto.] Proof search time: 0 min, 46 sec Results for lemma singleton_spec: : forall x y : elt, In y (singleton x) <-> X.eq y x FAILURE! Tactics applied: 10000 Original Proof: [unfold singleton; simpl; split; intros; inv; auto.] Proof search time: 0 min, 10 sec Results for lemma empty_spec: : Empty empty FAILURE! Tactics applied: 10000 Original Proof: [unfold Empty, empty; intuition; inv.] Proof search time: 0 min, 14 sec Results for lemma max_elt_spec3: : forall s : t, max_elt s = None -> Empty s FAILURE! Tactics applied: 10000 Original Proof: [induction s as [ | a s IH]. red; intuition; inv. destruct s as [ | b s]. inversion 1. intros; elim IH with b; auto.] Proof search time: 0 min, 22 sec Results for lemma inter_inf: : forall (s s' : t) (a : elt) (Hs : Ok s) (Hs' : Ok s'), Inf a s -> Inf a s' -> Inf a (inter s s') FAILURE! Tactics applied: 10000 Original Proof: [induction2. apply Inf_lt with x; auto. apply Hrec'; auto. apply Inf_lt with x'; auto.] Proof search time: 0 min, 32 sec Results for fold 2 Results for lemma min_elt_spec2: : forall (s : t) (x y : elt) (Hs : Ok s), min_elt s = Some x -> In y s -> ~ X.lt y x FAILURE! Tactics applied: 10000 Original Proof: [induction s as [ | x s IH]; simpl; inversion 2; subst. intros; inv; try sort_inf_in; order.] Proof search time: 0 min, 25 sec Results for lemma max_elt_spec2: : forall (s : t) (x y : elt) (Hs : Ok s), max_elt s = Some x -> In y s -> ~ X.lt x y FAILURE! Tactics applied: 10000 Original Proof: [induction s as [ | a s IH]. inversion 2. destruct s as [ | b s]. inversion 2; subst. intros; inv; order. intros. inv; auto. assert (~X.lt x b) by (apply IH; auto). assert (X.lt a b) by auto. order.] Proof search time: 0 min, 26 sec 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; intros. split; intuition; inv. destruct (f a) eqn:F; rewrite !InA_cons, ?IHs; intuition. setoid_replace x with a; auto. setoid_replace a with x in F; auto; congruence.] Proof search time: 0 min, 20 sec 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. split; auto. intros x l Hrec f Hf. generalize (Hrec f Hf); clear Hrec. destruct (partition f l) as [s1 s2]; simpl; intros. case (f x); simpl; auto. split; inversion_clear 1; auto. constructor 2; rewrite <- H; auto. constructor 2; rewrite H; auto.] Proof search time: 0 min, 18 sec 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: 17 Original Proof: [intuition.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 3 sec Results for fold 3 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: [induction s as [ | x s IH]; intros [ | x' s'] Hs Hs'; simpl. intuition. split; intros H. discriminate. assert (In x' nil) by (rewrite H; auto). inv. split; intros H. discriminate. assert (In x nil) by (rewrite <-H; auto). inv. inv. elim_compare x x' as C; try discriminate. rewrite IH; auto. split; intros E y; specialize (E y). rewrite !InA_cons, E, C; intuition. rewrite !InA_cons, C in E. intuition; try sort_inf_in; order. split; intros E. discriminate. assert (In x (x'::s')) by (rewrite <- E; auto). inv; try sort_inf_in; order. split; intros E. discriminate. assert (In x' (x::s)) by (rewrite E; auto). inv; try sort_inf_in; order.] Proof search time: 0 min, 20 sec Results for lemma min_elt_spec1: : forall (s : t) (x : elt), min_elt s = Some x -> In x s FAILURE! Tactics applied: 10000 Original Proof: [destruct s; simpl; inversion 1; auto.] Proof search time: 0 min, 8 sec Results for lemma compare_spec_aux: : forall s s', CompSpec eq L.lt s s' (compare s s') FAILURE! Tactics applied: 10000 Original Proof: [induction s as [|x s IH]; intros [|x' s']; simpl; intuition. elim_compare x x'; auto.] Proof search time: 0 min, 11 sec Results for lemma max_elt_spec1: : forall (s : t) (x : elt), max_elt s = Some x -> In x s FAILURE! Tactics applied: 10000 Original Proof: [induction s as [ | x s IH]. inversion 1. destruct s as [ | y s]. simpl. inversion 1; subst; auto. right; apply IH; auto.] Proof search time: 0 min, 8 sec 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: [induction2; try rewrite ?InA_cons, ?Hrec, ?Hrec'; intuition; inv; auto. left; order.] Proof search time: 0 min, 38 sec Results for fold 4 Results for lemma elements_spec2w: : forall (s : t) (Hs : Ok s), NoDupA X.eq (elements s) FAILURE! Tactics applied: 10000 Original Proof: [intro s; repeat rewrite <- isok_iff; auto.] Proof search time: 0 min, 7 sec Results for lemma eq_leibniz: : forall s s', eq s s' -> s = s' FAILURE! Tactics applied: 10000 Original Proof: [intros [xs Hxs] [ys Hys] Heq. change (equivlistA X.eq xs ys) in Heq. assert (H : eqlistA X.eq xs ys). rewrite <- Raw.isok_iff in Hxs, Hys. apply SortA_equivlistA_eqlistA with X.lt; auto with *. apply eq_leibniz_list in H. subst ys. f_equal. apply Eqdep_dec.eq_proofs_unicity. intros x y; destruct (bool_dec x y); tauto.] Proof search time: 0 min, 8 sec Results for lemma min_elt_spec3: : forall s : t, min_elt s = None -> Empty s FAILURE! Tactics applied: 10000 Original Proof: [destruct s; simpl; red; intuition. inv. discriminate.] Proof search time: 0 min, 10 sec 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; intros. split; intros; auto. inv. destruct (f a) eqn:F. rewrite IHs; auto. firstorder. inv; auto. setoid_replace x with a; auto. split; intros H'. discriminate. rewrite H' in F; auto.] Proof search time: 0 min, 11 sec Results for lemma partition_inf2: : forall (s : t) (f : elt -> bool) (x : elt) (Hs : Ok s), Inf x s -> Inf x (snd (partition f s)) FAILURE! Tactics applied: 10000 Original Proof: [intros s f x; repeat rewrite <- isok_iff; revert s f x. simple induction s; simpl. intuition. intros x l Hrec f a Hs Ha; inv. generalize (Hrec f a H). case (f x); case (partition f l); simpl. intros; apply H2; apply Inf_lt with x; auto. auto.] Proof search time: 0 min, 9 sec Results for fold 5 Results for lemma is_empty_spec: : forall s : t, is_empty s = true <-> Empty s FAILURE! Tactics applied: 10000 Original Proof: [intros [ | x s]; simpl. split; auto. intros _ x H. inv. split. discriminate. intros H. elim (H x); auto.] Proof search time: 0 min, 11 sec Results for lemma mem_spec: : forall (s : t) (x : elt) (Hs : Ok s), mem x s = true <-> In x s FAILURE! Tactics applied: 10000 Original Proof: [induction s; intros x Hs; inv; simpl. intuition. discriminate. inv. elim_compare x a; rewrite InA_cons; intuition; try order. discriminate. sort_inf_in. order. rewrite <- IHs; auto. rewrite IHs; auto.] Proof search time: 0 min, 10 sec Results for lemma isok_iff: : forall l, sort X.lt l <-> Ok l FAILURE! Tactics applied: 10000 Original Proof: [intro l; split; intro H. elim H. constructor; fail. intros y ys Ha Hb Hc. change (inf y ys && isok ys = true). rewrite inf_iff in Hc. rewrite andb_true_iff; tauto. induction l as [|x xs]. constructor. change (inf x xs && isok xs = true) in H. rewrite andb_true_iff, <- inf_iff in H. destruct H; constructor; tauto.] Proof search time: 0 min, 10 sec 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. elim_compare x a; inv; rewrite !InA_cons, ?IHs; intuition. left; order.] Proof search time: 0 min, 11 sec Results for lemma compare_spec: : forall s s', Ok s -> Ok s' -> CompSpec eq lt s s' (compare s s') FAILURE! Tactics applied: 10000 Original Proof: [intros s s' Hs Hs'. destruct (compare_spec_aux s s'); constructor; auto. exists s, s'; repeat split; auto using @ok. exists s', s; repeat split; auto using @ok.] Proof search time: 0 min, 16 sec Results for fold 6 Results for lemma add_inf: : forall (s : t) (x a : elt), Inf a s -> X.lt a x -> Inf a (add x s) FAILURE! Tactics applied: 10000 Original Proof: [simple induction s; simpl. intuition. intros; elim_compare x a; inv; intuition.] Proof search time: 0 min, 9 sec 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: [induction2; try rewrite ?InA_cons, ?Hrec, ?Hrec'; intuition; inv; auto; try sort_inf_in; try order. left; order.] Proof search time: 0 min, 26 sec Results for lemma union_inf: : forall (s s' : t) (a : elt) (Hs : Ok s) (Hs' : Ok s'), Inf a s -> Inf a s' -> Inf a (union s s') SUCCESS! Proof Found in EFSM: [induction2 ] Tactics applied: 19 Original Proof: [induction2.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 0 sec Results for lemma elements_spec2: : forall (s : t) (Hs : Ok s), sort X.lt (elements s) FAILURE! Tactics applied: 10000 Original Proof: [intro s; repeat rewrite <- isok_iff; auto.] Proof search time: 0 min, 9 sec 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: [intros s s'; revert s. induction s' as [ | x' s' IH]; intros [ | x s] Hs Hs'; simpl; auto. split; try red; intros; auto. split; intros H. discriminate. assert (In x nil) by (apply H; auto). inv. split; try red; intros; auto. inv. inv. elim_compare x x' as C. rewrite IH; auto. split; intros S y; specialize (S y). rewrite !InA_cons, C. intuition. rewrite !InA_cons, C in S. intuition; try sort_inf_in; order. split; intros S. discriminate. assert (In x (x'::s')) by (apply S; auto). inv; try sort_inf_in; order. rewrite IH; auto. split; intros S y; specialize (S y). rewrite !InA_cons. intuition. rewrite !InA_cons in S. rewrite !InA_cons. intuition; try sort_inf_in; order.] Proof search time: 0 min, 16 sec Results for fold 7 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: [induction2; try rewrite ?InA_cons, ?Hrec, ?Hrec'; intuition; inv; auto; try sort_inf_in; try order. right; intuition; inv; auto.] Proof search time: 0 min, 23 sec Results for lemma partition_inf1: : forall (s : t) (f : elt -> bool) (x : elt) (Hs : Ok s), Inf x s -> Inf x (fst (partition f s)) FAILURE! Tactics applied: 10000 Original Proof: [intros s f x; repeat rewrite <- isok_iff; revert s f x. simple induction s; simpl. intuition. intros x l Hrec f a Hs Ha; inv. generalize (Hrec f a H). case (f x); case (partition f l); simpl. auto. intros; apply H2; apply Inf_lt with x; auto.] Proof search time: 0 min, 12 sec Results for lemma eq_leibniz_list: : forall xs ys, eqlistA X.eq xs ys -> xs = ys FAILURE! Tactics applied: 10000 Original Proof: [induction xs as [|x xs]; intros [|y ys] H; inversion H; [ | ]. reflexivity. f_equal. apply X.eq_leibniz; congruence. apply IHxs; subst; assumption.] Proof search time: 0 min, 11 sec 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. split; auto. intros x l Hrec f Hf. generalize (Hrec f Hf); clear Hrec. destruct (partition f l) as [s1 s2]; simpl; intros. case (f x); simpl; auto. split; inversion_clear 1; auto. constructor 2; rewrite <- H; auto. constructor 2; rewrite H; auto.] Proof search time: 0 min, 12 sec Results for lemma choose_spec3: : forall s s' x x', Ok s -> Ok s' -> choose s = Some x -> choose s' = Some x' -> Equal s s' -> X.eq x x' FAILURE! Tactics applied: 10000 Original Proof: [unfold choose; intros s s' x x' Hs Hs' Hx Hx' H. assert (~X.lt x x'). apply min_elt_spec2 with s'; auto. rewrite <-H; auto using min_elt_spec1. assert (~X.lt x' x). apply min_elt_spec2 with s; auto. rewrite H; auto using min_elt_spec1. order.] Proof search time: 0 min, 18 sec Results for fold 8 Results for lemma diff_inf: : forall (s s' : t) (Hs : Ok s) (Hs' : Ok s') (a : elt), Inf a s -> Inf a s' -> Inf a (diff s s') FAILURE! Tactics applied: 10000 Original Proof: [intros s s'; repeat rewrite <- isok_iff; revert s s'. induction2. apply Hrec; trivial. apply Inf_lt with x; auto. apply Inf_lt with x'; auto. apply Hrec'; auto. apply Inf_lt with x'; auto.] Proof search time: 0 min, 17 sec Results for lemma cardinal_spec: : forall (s : t) (Hs : Ok s), cardinal s = length (elements s) SUCCESS! Proof Found in EFSM: [intuition ] Tactics applied: 22 Original Proof: [auto.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec 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. elim_compare x a; inv; rewrite !InA_cons, ?IHs; intuition; try sort_inf_in; try order.] Proof search time: 0 min, 9 sec Results for lemma filter_inf: : forall (s : t) (x : elt) (f : elt -> bool) (Hs : Ok s), Inf x s -> Inf x (filter f s) FAILURE! Tactics applied: 10000 Original Proof: [simple induction s; simpl. intuition. intros x l Hrec a f Hs Ha; inv. case (f x); auto. apply Hrec; auto. apply Inf_lt with x; auto.] Proof search time: 0 min, 10 sec Results for lemma inf_iff: : forall x l, Inf x l <-> inf x l = true FAILURE! Tactics applied: 10000 Original Proof: [intros x l; split; intro H. destruct H; simpl in *. reflexivity. rewrite <- compare_lt_iff in H; rewrite H; reflexivity. destruct l as [|y ys]; simpl in *. constructor; fail. revert H; case_eq (X.compare x y); try discriminate; []. intros Ha _. rewrite compare_lt_iff in Ha. constructor; assumption.] Proof search time: 0 min, 5 sec Results for fold 9 Results for lemma remove_inf: : forall (s : t) (x a : elt) (Hs : Ok s), Inf a s -> Inf a (remove x s) FAILURE! Tactics applied: 10000 Original Proof: [induction s; simpl. intuition. intros; elim_compare x a; inv; auto. apply Inf_lt with a; auto.] Proof search time: 0 min, 7 sec 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: [reflexivity ] Tactics applied: 17 Original Proof: [reflexivity.] Shorter Proof Found? no Single step proof reused proof search time: 0 min, 2 sec OVERALL RESULTS SUMMARY EFSMProver proved 4 out of 42 lemmas. Success rate of 9.523809523809524% There were 0 errors. 38 proof attempts exhausted the automaton On average, a proof was found after applying 18 tactics The longest proof consisted of 1 tactics There were 0 shorter proofs found Of the 38 failures, 38 of them used all 10000 tactics There were 4 reused proofs found There were 0 novel proofs found Of the 38 failures, the average number of tactics used was 10000 On average, a proof was found after 0 min, 2 sec On average, a failed proof attempt took 0 min, 15 sec On average, any (success or failure) proof attempt took 0 min, 14 sec The longest time to find a proof was 0 min, 3 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