Results for fold 1 Results for lemma lex_Opp: : forall u v u' v', u = CompOpp u' -> v = CompOpp v' -> lex u v = CompOpp (lex u' v') FAILURE! Tactics applied: 10000 Original Proof: [intros ? ? u' ? -> ->. case u'; reflexivity.] Proof search time: 0 min, 35 sec Number of successful tactic applications: 2078 Number of failed tactic applications: 7923 Results for lemma ct_lex: : forall u v w u' v' w', ct u v w -> ct u' v' w' -> ct (lex u u') (lex v v') (lex w w') FAILURE! Tactics applied: 10000 Original Proof: [intros u v w u' v' w' H H'. inversion_clear H; inversion_clear H'; ct; destruct w; ct; destruct w'; ct.] Proof search time: 0 min, 34 sec Number of successful tactic applications: 2030 Number of failed tactic applications: 7971 Results for lemma ct_lxl: : forall x, ct Lt x Lt SUCCESS! Proof Found in EFSM: destruct x; constructor. Tactics applied: 97 Original Proof: [destruct x; constructor.] Shorter Proof Found? no Proof reused from ct_gxg proof search time: 0 min, 24 sec Number of successful tactic applications: 22 Number of failed tactic applications: 75 Results for lemma compare_eq: : forall s s', compare s s' = Eq -> eq s s' FAILURE! Tactics applied: 10000 Original Proof: [unfold eq. intros s s'. rewrite compare_equal, equal_spec. trivial.] Proof search time: 0 min, 37 sec Number of successful tactic applications: 2503 Number of failed tactic applications: 7498 Results for lemma lt_rev_append: : forall j x y, E.lt x y -> E.lt (j@x) (j@y) FAILURE! Tactics applied: 10000 Original Proof: [induction j; intros; simpl; auto.] Proof search time: 0 min, 36 sec Number of successful tactic applications: 1910 Number of failed tactic applications: 8091 Results for lemma for_all_spec: : forall s f, compat_bool E.eq f -> (for_all f s = true <-> For_all (fun x => f x = true) s) FAILURE! Tactics applied: 10000 Original Proof: [intros. apply xforall_spec.] Proof search time: 0 min, 37 sec Number of successful tactic applications: 1963 Number of failed tactic applications: 8038 Results for lemma elements_spec2: : forall s, sort E.lt (elements s) FAILURE! Tactics applied: 10000 Original Proof: [unfold elements. assert (H: forall s j acc, sort E.lt acc -> (forall x y, In x s -> InL y acc -> E.lt (j@x) y) -> sort E.lt (xelements s j acc)). induction s as [|l IHl o r IHr]; simpl; trivial. intros j acc Hacc Hsacc. destruct o. apply IHl. constructor. apply IHr. apply Hacc. intros x y Hx Hy. apply Hsacc; assumption. case_eq (xelements r j~1 acc). constructor. intros z q H. constructor. assert (H': InL z (xelements r j~1 acc)). rewrite H. constructor. reflexivity. clear H q. rewrite xelements_spec in H'. destruct H' as [Hy|[x [-> Hx]]]. apply (Hsacc 1 z); trivial. reflexivity. simpl. apply lt_rev_append. exact I. intros x y Hx Hy. inversion_clear Hy. rewrite H. simpl. apply lt_rev_append. exact I. rewrite xelements_spec in H. destruct H as [Hy|[z [-> Hy]]]. apply Hsacc; assumption. simpl. apply lt_rev_append. exact I. apply IHl. apply IHr. apply Hacc. intros x y Hx Hy. apply Hsacc; assumption. intros x y Hx Hy. rewrite xelements_spec in Hy. destruct Hy as [Hy|[z [-> Hy]]]. apply Hsacc; assumption. simpl. apply lt_rev_append. exact I. intros. apply H. constructor. intros x y _ H'. inversion H'.] Proof search time: 0 min, 36 sec Number of successful tactic applications: 1798 Number of failed tactic applications: 8203 Results for lemma equal_spec: : forall s s', equal s s' = true <-> Equal s s' FAILURE! Tactics applied: 10000 Original Proof: [intros. rewrite equal_subset. rewrite andb_true_iff. rewrite 2subset_spec. unfold Equal, Subset. firstorder.] Proof search time: 0 min, 37 sec Number of successful tactic applications: 1952 Number of failed tactic applications: 8049 Results for lemma ct_xgg: : forall x, ct x Gt Gt SUCCESS! Proof Found in EFSM: destruct x; constructor. Tactics applied: 97 Original Proof: [destruct x; constructor.] Shorter Proof Found? no Proof reused from ct_gxg proof search time: 0 min, 24 sec Number of successful tactic applications: 22 Number of failed tactic applications: 75 Results for lemma equal_subset: : forall s s', equal s s' = subset s s' && subset s' s FAILURE! Tactics applied: 10000 Original Proof: [induction s as [|l IHl o r IHr]; intros [|l' o' r']; simpl; trivial. destruct o. reflexivity. rewrite andb_comm. reflexivity. rewrite <- 6andb_lazy_alt. rewrite eq_iff_eq_true. rewrite 7andb_true_iff, eqb_true_iff. rewrite IHl, IHr, 2andb_true_iff. clear IHl IHr. intuition subst. destruct o'; reflexivity. destruct o'; reflexivity. destruct o; auto. destruct o'; trivial.] Proof search time: 0 min, 38 sec Number of successful tactic applications: 1845 Number of failed tactic applications: 8156 Results for lemma compare_equal: : forall s s', compare s s' = Eq <-> equal s s' = true FAILURE! Tactics applied: 10000 Original Proof: [induction s as [|l IHl o r IHr]; destruct s' as [|l' o' r']. simpl. tauto. unfold compare, equal. case is_empty; intuition discriminate. unfold compare, equal. case is_empty; intuition discriminate. simpl. rewrite <- 2andb_lazy_alt, 2andb_true_iff. rewrite <- IHl, <- IHr, <- compare_bool_Eq. clear IHl IHr. rewrite and_assoc. rewrite <- 2lex_Eq. reflexivity.] Proof search time: 0 min, 38 sec Number of successful tactic applications: 1964 Number of failed tactic applications: 8037 Results for lemma remove_spec: : forall s x y, In y (remove x s) <-> In y s /\ y<>x FAILURE! Tactics applied: 10000 Original Proof: [unfold In. intros s x y; revert x y s. induction x; intros [y|y|] [|l o r]; simpl remove; rewrite ?mem_node; simpl mem; try (rewrite IHx; clear IHx); rewrite ?mem_Leaf; intuition congruence.] Proof search time: 0 min, 40 sec Number of successful tactic applications: 3120 Number of failed tactic applications: 6881 Results for lemma filter_spec: : forall s x f, compat_bool E.eq f -> (In x (filter f s) <-> In x s /\ f x = true) FAILURE! Tactics applied: 10000 Original Proof: [intros. apply xfilter_spec.] Proof search time: 0 min, 41 sec Number of successful tactic applications: 3202 Number of failed tactic applications: 6799 Results for lemma ct_xce: : forall x, ct x (CompOpp x) Eq SUCCESS! Proof Found in EFSM: destruct x; constructor. Tactics applied: 97 Original Proof: [destruct x; constructor.] Shorter Proof Found? no Proof reused from ct_gxg proof search time: 0 min, 24 sec Number of successful tactic applications: 22 Number of failed tactic applications: 75 Results for fold 2 Results for lemma choose_empty: : forall s, is_empty s = true -> choose s = None FAILURE! Tactics applied: 10000 Original Proof: [intros s Hs. case_eq (choose s); trivial. intros p Hp. apply choose_spec1 in Hp. apply is_empty_spec in Hs. elim (Hs _ Hp).] Proof search time: 0 min, 41 sec Number of successful tactic applications: 2969 Number of failed tactic applications: 7032 Results for lemma singleton_spec: : forall x y, In y (singleton x) <-> y=x FAILURE! Tactics applied: 10000 Original Proof: [unfold singleton. intros x y. rewrite add_spec. intuition. unfold In in *. rewrite mem_Leaf in *. discriminate.] Proof search time: 0 min, 33 sec Number of successful tactic applications: 1782 Number of failed tactic applications: 8219 Results for lemma min_elt_spec2: : forall s x y, min_elt s = Some x -> In y s -> ~ E.lt y x FAILURE! Tactics applied: 10000 Original Proof: [unfold In. induction s as [|l IHl o r IHr]; intros x y H H'. discriminate. simpl in H. case_eq (min_elt l). intros p Hp. rewrite Hp in H. injection H; intros <-. destruct y as [z|z|]; simpl; intro; trivial. apply (IHl p z); trivial. intro Hp; rewrite Hp in H. apply min_elt_spec3 in Hp. destruct o. injection H. intros <- Hl. clear H. destruct y as [z|z|]; simpl; trivial. elim (Hp _ H'). destruct (min_elt r). injection H. intros <-. clear H. destruct y as [z|z|]. apply (IHr p z); trivial. elim (Hp _ H'). discriminate. discriminate.] Proof search time: 0 min, 38 sec Number of successful tactic applications: 3595 Number of failed tactic applications: 6406 Results for lemma add_spec: : forall s x y, In y (add x s) <-> y=x \/ In y s FAILURE! Tactics applied: 10000 Original Proof: [unfold In. intros s x y; revert x y s. induction x; intros [y|y|] [|l o r]; simpl mem; try (rewrite IHx; clear IHx); rewrite ?mem_Leaf; intuition congruence.] Proof search time: 0 min, 36 sec Number of successful tactic applications: 2840 Number of failed tactic applications: 7161 Results for lemma fold_spec: : forall s (A : Type) (i : A) (f : elt -> A -> A), fold f s i = fold_left (fun a e => f e a) (elements s) i FAILURE! Tactics applied: 10000 Original Proof: [unfold fold, elements. intros s A i f. revert s i. set (f' := fun a e => f e a). assert (H: forall s i j acc, fold_left f' acc (xfold f s i j) = fold_left f' (xelements s j acc) i). induction s as [|l IHl o r IHr]; intros; trivial. destruct o; simpl xelements; simpl xfold. rewrite IHr, <- IHl. reflexivity. rewrite IHr. apply IHl. intros. exact (H s i 1 nil).] Proof search time: 0 min, 39 sec Number of successful tactic applications: 3157 Number of failed tactic applications: 6844 Results for lemma choose_spec1: : forall s x, choose s = Some x -> In x s FAILURE! Tactics applied: 10000 Original Proof: [induction s as [| l IHl o r IHr]; simpl. intros. discriminate. destruct o. intros x H. injection H; intros; subst. reflexivity. revert IHl. case choose. intros p Hp x H. injection H; intros; subst; clear H. apply Hp. reflexivity. intros _ x. revert IHr. case choose. intros p Hp H. injection H; intros; subst; clear H. apply Hp. reflexivity. intros. discriminate.] Proof search time: 0 min, 35 sec Number of successful tactic applications: 3021 Number of failed tactic applications: 6980 Results for lemma mem_Leaf: : forall x, mem x Leaf = false SUCCESS! Proof Found in EFSM: destruct x; constructor. Tactics applied: 130 Original Proof: [destruct x; trivial.] Shorter Proof Found? no Proof reused from ct_gxg proof search time: 0 min, 19 sec Number of successful tactic applications: 26 Number of failed tactic applications: 104 Results for lemma max_elt_spec1: : forall s x, max_elt s = Some x -> In x s FAILURE! Tactics applied: 10000 Original Proof: [unfold In. induction s as [| l IHl o r IHr]; simpl. intros. discriminate. intros x. destruct (max_elt r); intros. injection H. intros <-. apply IHr. reflexivity. destruct o; simpl. injection H. intros <-. reflexivity. destruct (max_elt l); simpl in *. injection H. intros <-. apply IHl. reflexivity. discriminate.] Proof search time: 0 min, 35 sec Number of successful tactic applications: 3021 Number of failed tactic applications: 6980 Results for lemma diff_spec: : forall s s' x, In x (diff s s') <-> In x s /\ ~ In x s' FAILURE! Tactics applied: 10000 Original Proof: [unfold In. intros s s' x; revert x s s'. induction x; destruct s; destruct s' as [|l' o' r']; simpl diff; rewrite ?mem_node; simpl mem; try (rewrite IHx; clear IHx); try intuition congruence. rewrite andb_true_iff. destruct o'; intuition discriminate.] Proof search time: 0 min, 40 sec Number of successful tactic applications: 3568 Number of failed tactic applications: 6433 Results for lemma choose_spec2: : forall s, choose s = None -> Empty s FAILURE! Tactics applied: 10000 Original Proof: [unfold Empty, In. intros s H. induction s as [|l IHl o r IHr]. intro. apply empty_spec. destruct o. discriminate. simpl in H. destruct (choose l). discriminate. destruct (choose r). discriminate. intros [a|a|]. apply IHr. reflexivity. apply IHl. reflexivity. discriminate.] Proof search time: 0 min, 34 sec Number of successful tactic applications: 2748 Number of failed tactic applications: 7253 Results for lemma xelements_spec: : forall s j acc y, InL y (xelements s j acc) <-> InL y acc \/ exists x, y=(j@x) /\ mem x s = true FAILURE! Tactics applied: 10000 Original Proof: [induction s as [|l IHl o r IHr]; simpl. intros. split; intro H. left. assumption. destruct H as [H|[x [Hx Hx']]]. assumption. elim (empty_spec Hx'). intros j acc y. case o. rewrite IHl. rewrite InA_cons. rewrite IHr. clear IHl IHr. split. intros [[H|[H|[x [-> H]]]]|[x [-> H]]]; eauto. right. exists x~1. auto. right. exists x~0. auto. intros [H|[x [-> H]]]. eauto. destruct x. left. right. right. exists x; auto. right. exists x; auto. left. left. reflexivity. rewrite IHl, IHr. clear IHl IHr. split. intros [[H|[x [-> H]]]|[x [-> H]]]. eauto. right. exists x~1. auto. right. exists x~0. auto. intros [H|[x [-> H]]]. eauto. destruct x. left. right. exists x; auto. right. exists x; auto. discriminate.] Proof search time: 0 min, 47 sec Number of successful tactic applications: 2644 Number of failed tactic applications: 7357 Results for lemma xexists_spec: : forall f s i, xexists f s i = true <-> Exists (fun x => f (i@x) = true) s FAILURE! Tactics applied: 10000 Original Proof: [unfold Exists, In. intro f. induction s as [|l IHl o r IHr]; intros i; simpl. setoid_rewrite mem_Leaf. firstorder. rewrite <- 2orb_lazy_alt, 2orb_true_iff, <- andb_lazy_alt, andb_true_iff. rewrite IHl, IHr. clear IHl IHr. split. intros [[Hi|[x Hr]]|[x Hl]]. exists 1. exact Hi. exists x~1. exact Hr. exists x~0. exact Hl. intros [[x|x|] H]; eauto.] Proof search time: 0 min, 36 sec Number of successful tactic applications: 1826 Number of failed tactic applications: 8175 Results for lemma elements_spec1: : forall s x, InL x (elements s) <-> In x s FAILURE! Tactics applied: 10000 Original Proof: [unfold elements. intros. rewrite xelements_spec. split; [ intros [A|(y & B & C)] | intros IN ]. inversion A. simpl in *. congruence. right. exists x. auto.] Proof search time: 0 min, 34 sec Number of successful tactic applications: 2564 Number of failed tactic applications: 7437 Results for lemma compare_spec: : forall x y, CompSpec eq lt x y (compare x y) FAILURE! Tactics applied: 10000 Original Proof: [unfold eq, lt. induction x; destruct y; try constructor; simpl; auto. destruct (IHx y); subst; auto. destruct (IHx y); subst; auto.] Proof search time: 0 min, 35 sec Number of successful tactic applications: 1597 Number of failed tactic applications: 8404 Results for fold 3 Results for lemma compare_spec: : forall s s' : t, CompSpec eq lt s s' (compare s s') FAILURE! Tactics applied: 10000 Original Proof: [unfold eq, lt. induction x; destruct y; try constructor; simpl; auto. destruct (IHx y); subst; auto. destruct (IHx y); subst; auto.] Proof search time: 0 min, 44 sec Number of successful tactic applications: 605 Number of failed tactic applications: 9396 Results for lemma max_elt_spec2: : forall s x y, max_elt s = Some x -> In y s -> ~ E.lt x y FAILURE! Tactics applied: 10000 Original Proof: [unfold In. induction s as [|l IHl o r IHr]; intros x y H H'. discriminate. simpl in H. case_eq (max_elt r). intros p Hp. rewrite Hp in H. injection H; intros <-. destruct y as [z|z|]; simpl; intro; trivial. apply (IHr p z); trivial. intro Hp; rewrite Hp in H. apply max_elt_spec3 in Hp. destruct o. injection H. intros <- Hl. clear H. destruct y as [z|z|]; simpl; trivial. elim (Hp _ H'). destruct (max_elt l). injection H. intros <-. clear H. destruct y as [z|z|]. elim (Hp _ H'). apply (IHl p z); trivial. discriminate. discriminate.] Proof search time: 0 min, 49 sec Number of successful tactic applications: 2431 Number of failed tactic applications: 7570 Results for lemma union_spec: : forall s s' x, In x (union s s') <-> In x s \/ In x s' FAILURE! Tactics applied: 10000 Original Proof: [unfold In. intros s s' x; revert x s s'. induction x; destruct s; destruct s'; simpl union; simpl mem; try (rewrite IHx; clear IHx); try intuition congruence. apply orb_true_iff.] Proof search time: 0 min, 50 sec Number of successful tactic applications: 2353 Number of failed tactic applications: 7648 Results for lemma ct_gxg: : forall x, ct Gt x Gt SUCCESS! Proof Found in EFSM: destruct x; try constructor; Tactics applied: 63 Original Proof: [destruct x; constructor.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 32 sec Number of successful tactic applications: 16 Number of failed tactic applications: 47 Results for lemma is_empty_spec: : forall s, is_empty s = true <-> Empty s FAILURE! Tactics applied: 10000 Original Proof: [unfold Empty, In. induction s as [|l IHl o r IHr]; simpl. setoid_rewrite mem_Leaf. firstorder. rewrite <- 2andb_lazy_alt, 2andb_true_iff, IHl, IHr. clear IHl IHr. destruct o; simpl; split. intuition discriminate. intro H. elim (H 1). reflexivity. intros H [a|a|]; apply H || intro; discriminate. intro H. split. split. reflexivity. intro a. apply (H a~0). intro a. apply (H a~1).] Proof search time: 0 min, 45 sec Number of successful tactic applications: 1444 Number of failed tactic applications: 8557 Results for lemma bits_lt_antirefl: : forall x : positive, ~ bits_lt x x SUCCESS! Proof Found in EFSM: induction x; intros ; simpl ; auto. Tactics applied: 2307 Original Proof: [induction x; simpl; auto.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 34 sec Number of successful tactic applications: 220 Number of failed tactic applications: 2087 Results for lemma choose_spec3: : forall s s' x y, choose s = Some x -> choose s' = Some y -> Equal s s' -> E.eq x y FAILURE! Tactics applied: 10000 Original Proof: [intros s s' x y Hx Hy H. apply choose_spec3' in H. congruence.] Proof search time: 0 min, 54 sec Number of successful tactic applications: 2564 Number of failed tactic applications: 7437 Results for lemma compare_x_empty: : forall a, is_empty a = true -> forall b, compare b a = if is_empty b then Eq else Gt FAILURE! Tactics applied: 10000 Original Proof: [setoid_rewrite <- compare_x_Leaf. intros. rewrite 2(compare_inv b), (compare_empty_x _ H). reflexivity.] Proof search time: 0 min, 48 sec Number of successful tactic applications: 1684 Number of failed tactic applications: 8317 Results for lemma cardinal_spec: : forall s, cardinal s = length (elements s) FAILURE! Tactics applied: 10000 Original Proof: [unfold elements. assert (H: forall s j acc, (cardinal s + length acc)%nat = length (xelements s j acc)). induction s as [|l IHl b r IHr]; intros j acc; simpl; trivial. destruct b. rewrite <- IHl. simpl. rewrite <- IHr. rewrite <- plus_n_Sm, Plus.plus_assoc. reflexivity. rewrite <- IHl, <- IHr. rewrite Plus.plus_assoc. reflexivity. intros. rewrite <- H. simpl. rewrite Plus.plus_comm. reflexivity.] Proof search time: 0 min, 44 sec Number of successful tactic applications: 1492 Number of failed tactic applications: 8509 Results for lemma xforall_spec: : forall f s i, xforall f s i = true <-> For_all (fun x => f (i@x) = true) s FAILURE! Tactics applied: 10000 Original Proof: [unfold For_all, In. intro f. induction s as [|l IHl o r IHr]; intros i; simpl. setoid_rewrite mem_Leaf. intuition discriminate. rewrite <- 2andb_lazy_alt, <- orb_lazy_alt, 2 andb_true_iff. rewrite IHl, IHr. clear IHl IHr. split. intros [[Hi Hr] Hl] x. destruct x; simpl; intro H. apply Hr, H. apply Hl, H. rewrite H in Hi. assumption. intro H; intuition. specialize (H 1). destruct o. apply H. reflexivity. reflexivity. apply H. assumption. apply H. assumption.] Proof search time: 0 min, 46 sec Number of successful tactic applications: 1543 Number of failed tactic applications: 8458 Results for lemma compare_empty_x: : forall a, is_empty a = true -> forall b, compare a b = if is_empty b then Eq else Lt FAILURE! Tactics applied: 10000 Original Proof: [induction a as [|l IHl o r IHr]; trivial. destruct o. intro; discriminate. simpl is_empty. rewrite <- andb_lazy_alt, andb_true_iff. intros [Hl Hr]. destruct b as [|l' [|] r']; simpl compare; trivial. rewrite Hl, Hr. trivial. rewrite (IHl Hl), (IHr Hr). simpl. case (is_empty l'); case (is_empty r'); trivial.] Proof search time: 0 min, 48 sec Number of successful tactic applications: 1722 Number of failed tactic applications: 8279 Results for lemma choose_spec3': : forall s s', Equal s s' -> choose s = choose s' FAILURE! Tactics applied: 10000 Original Proof: [setoid_rewrite <- equal_spec. induction s as [|l IHl o r IHr]. intros. symmetry. apply choose_empty. assumption. destruct s' as [|l' o' r']. generalize (Node l o r) as s. simpl. intros. apply choose_empty. rewrite equal_spec in H. symmetry in H. rewrite <- equal_spec in H. assumption. simpl. rewrite <- 2andb_lazy_alt, 2andb_true_iff, eqb_true_iff. intros [[<- Hl] Hr]. rewrite (IHl _ Hl), (IHr _ Hr). reflexivity.] Proof search time: 0 min, 51 sec Number of successful tactic applications: 1760 Number of failed tactic applications: 8241 Results for lemma partition_spec1: : forall s f, compat_bool E.eq f -> Equal (fst (partition f s)) (filter f s) FAILURE! Tactics applied: 10000 Original Proof: [intros. rewrite partition_filter. reflexivity.] Proof search time: 0 min, 46 sec Number of successful tactic applications: 1791 Number of failed tactic applications: 8210 Results for lemma min_elt_spec3: : forall s, min_elt s = None -> Empty s FAILURE! Tactics applied: 10000 Original Proof: [unfold Empty, In. intros s H. induction s as [|l IHl o r IHr]. intro. apply empty_spec. intros [a|a|]. apply IHr. revert H. clear. simpl. destruct (min_elt r); trivial. case min_elt; intros; try discriminate. destruct o; discriminate. apply IHl. revert H. clear. simpl. destruct (min_elt l); trivial. intro; discriminate. revert H. clear. simpl. case min_elt; intros; try discriminate. destruct o; discriminate.] Proof search time: 0 min, 44 sec Number of successful tactic applications: 1757 Number of failed tactic applications: 8244 Results for fold 4 Results for lemma subset_Leaf_s: : forall s, Leaf [<=] s SUCCESS! Proof Found in EFSM: intros H [a|a|]; intuition discriminate. Tactics applied: 1646 Original Proof: [intros s i Hi. apply empty_spec in Hi. elim Hi.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 21 sec Number of successful tactic applications: 447 Number of failed tactic applications: 1199 Results for lemma ct_compare: : forall a b c, ct (compare a b) (compare b c) (compare a c) FAILURE! Tactics applied: 10000 Original Proof: [induction a as [|l IHl o r IHr]; intros s' s''. destruct s' as [|l' o' r']; destruct s'' as [|l'' o'' r'']; ct. rewrite compare_inv. ct. unfold compare at 1. case_eq (is_empty (Node l' o' r')); intro H'. rewrite (compare_empty_x _ H'). ct. unfold compare at 2. case_eq (is_empty (Node l'' o'' r'')); intro H''. rewrite (compare_x_empty _ H''), H'. ct. ct. destruct s' as [|l' o' r']; destruct s'' as [|l'' o'' r'']. ct. unfold compare at 2. rewrite compare_x_Leaf. case_eq (is_empty (Node l o r)); intro H. rewrite (compare_empty_x _ H). ct. case_eq (is_empty (Node l'' o'' r'')); intro H''. rewrite (compare_x_empty _ H''), H. ct. ct. rewrite 2 compare_x_Leaf. case_eq (is_empty (Node l o r)); intro H. rewrite compare_inv, (compare_x_empty _ H). ct. case_eq (is_empty (Node l' o' r')); intro H'. rewrite (compare_x_empty _ H'), H. ct. ct. simpl compare. apply ct_lex. apply ct_compare_bool. apply ct_lex; trivial.] Proof search time: 0 min, 35 sec Number of successful tactic applications: 2129 Number of failed tactic applications: 7872 Results for lemma xfilter_spec: : forall f s x i, In x (xfilter f s i) <-> In x s /\ f (i@x) = true FAILURE! Tactics applied: 10000 Original Proof: [intro f. unfold In. induction s as [|l IHl o r IHr]; intros x i; simpl xfilter. rewrite mem_Leaf. intuition discriminate. rewrite mem_node. destruct x; simpl. rewrite IHr. reflexivity. rewrite IHl. reflexivity. rewrite <- andb_lazy_alt. apply andb_true_iff.] Proof search time: 0 min, 37 sec Number of successful tactic applications: 3104 Number of failed tactic applications: 6897 Results for lemma max_elt_spec3: : forall s, max_elt s = None -> Empty s FAILURE! Tactics applied: 10000 Original Proof: [unfold Empty, In. intros s H. induction s as [|l IHl o r IHr]. intro. apply empty_spec. intros [a|a|]. apply IHr. revert H. clear. simpl. destruct (max_elt r); trivial. intro; discriminate. apply IHl. revert H. clear. simpl. destruct (max_elt l); trivial. case max_elt; intros; try discriminate. destruct o; discriminate. revert H. clear. simpl. case max_elt; intros; try discriminate. destruct o; discriminate.] Proof search time: 0 min, 33 sec Number of successful tactic applications: 2582 Number of failed tactic applications: 7419 Results for lemma compare_gt: : forall s s', compare s s' = Gt -> lt s' s FAILURE! Tactics applied: 10000 Original Proof: [unfold lt. intros s s'. rewrite compare_inv. case compare; trivial; intros; discriminate.] Proof search time: 0 min, 35 sec Number of successful tactic applications: 2625 Number of failed tactic applications: 7376 Results for lemma ct_cxe: : forall x, ct (CompOpp x) x Eq SUCCESS! Proof Found in EFSM: destruct x; constructor. Tactics applied: 1050 Original Proof: [destruct x; constructor.] Shorter Proof Found? no Proof reused from ct_lxl proof search time: 0 min, 20 sec Number of successful tactic applications: 184 Number of failed tactic applications: 866 Results for lemma mem_node: : forall x l o r, mem x (node l o r) = mem x (Node l o r) FAILURE! Tactics applied: 10000 Original Proof: [intros x l o r. case o; trivial. destruct l; trivial. destruct r; trivial. symmetry. destruct x. apply mem_Leaf. apply mem_Leaf. reflexivity.] Proof search time: 0 min, 38 sec Number of successful tactic applications: 2531 Number of failed tactic applications: 7470 Results for lemma partition_filter: : forall s f, partition f s = (filter f s, filter (fun x => negb (f x)) s) FAILURE! Tactics applied: 10000 Original Proof: [unfold partition, filter. intros s f. generalize 1 as j. induction s as [|l IHl o r IHr]; intro j. reflexivity. destruct o; simpl; rewrite IHl, IHr; reflexivity.] Proof search time: 0 min, 32 sec Number of successful tactic applications: 1723 Number of failed tactic applications: 8278 Results for lemma subset_spec: : forall s s', subset s s' = true <-> s [<=] s' FAILURE! Tactics applied: 10000 Original Proof: [induction s as [|l IHl o r IHr]; intros [|l' o' r']; simpl. split; intros. apply subset_Leaf_s. reflexivity. split; intros. apply subset_Leaf_s. reflexivity. rewrite <- 2andb_lazy_alt, 2andb_true_iff, 2is_empty_spec. destruct o; simpl. split. intuition discriminate. intro H. elim (@empty_spec 1). apply H. reflexivity. split; intro H. destruct H as [[_ Hl] Hr]. intros [i|i|] Hi. elim (Hr i Hi). elim (Hl i Hi). discriminate. split. split. reflexivity. unfold Empty. intros a H1. apply (@empty_spec (a~0)), H. assumption. unfold Empty. intros a H1. apply (@empty_spec (a~1)), H. assumption. rewrite <- 2andb_lazy_alt, 2andb_true_iff, IHl, IHr. clear. destruct o; simpl. split; intro H. destruct H as [[Ho' Hl] Hr]. rewrite Ho'. intros i Hi. destruct i. apply (Hr i). assumption. apply (Hl i). assumption. assumption. split. split. destruct o'; trivial. specialize (H 1). unfold In in H. simpl in H. apply H. reflexivity. intros i Hi. apply (H i~0). apply Hi. intros i Hi. apply (H i~1). apply Hi. split; intros. intros i Hi. destruct i; destruct H as [[H Hl] Hr]. apply (Hr i). assumption. apply (Hl i). assumption. discriminate Hi. split. split. reflexivity. intros i Hi. apply (H i~0). apply Hi. intros i Hi. apply (H i~1). apply Hi.] Proof search time: 0 min, 32 sec Number of successful tactic applications: 2032 Number of failed tactic applications: 7969 Results for lemma ct_xll: : forall x, ct x Lt Lt SUCCESS! Proof Found in EFSM: destruct x; constructor. Tactics applied: 1050 Original Proof: [destruct x; constructor.] Shorter Proof Found? no Proof reused from ct_lxl proof search time: 0 min, 20 sec Number of successful tactic applications: 178 Number of failed tactic applications: 872 Results for lemma compare_bool_inv: : forall b b', compare_bool b b' = CompOpp (compare_bool b' b) SUCCESS! Proof Found in EFSM: intros [|] [|]; trivial. Tactics applied: 903 Original Proof: [intros [|] [|]; reflexivity.] Shorter Proof Found? no This is a novel proof proof search time: 0 min, 20 sec Number of successful tactic applications: 136 Number of failed tactic applications: 767 Results for lemma elements_spec2w: : forall s, NoDupA E.eq (elements s) FAILURE! Tactics applied: 10000 Original Proof: [intro. apply SortA_NoDupA with E.lt; auto with *. apply E.eq_equiv. apply elements_spec2.] Proof search time: 0 min, 31 sec Number of successful tactic applications: 1680 Number of failed tactic applications: 8321 Results for lemma eq_dec: : forall s s', { eq s s' } + { ~ eq s s' } FAILURE! Tactics applied: 10000 Original Proof: [unfold eq. intros. case_eq (equal s s'); intro H. left. apply equal_spec, H. right. rewrite <- equal_spec. congruence. Defined.] Proof search time: 0 min, 29 sec Number of successful tactic applications: 1514 Number of failed tactic applications: 8487 Results for lemma min_elt_spec1: : forall s x, min_elt s = Some x -> In x s FAILURE! Tactics applied: 10000 Original Proof: [unfold In. induction s as [| l IHl o r IHr]; simpl. intros. discriminate. intros x. destruct (min_elt l); intros. injection H. intros <-. apply IHl. reflexivity. destruct o; simpl. injection H. intros <-. reflexivity. destruct (min_elt r); simpl in *. injection H. intros <-. apply IHr. reflexivity. discriminate.] Proof search time: 0 min, 35 sec Number of successful tactic applications: 2939 Number of failed tactic applications: 7062 Results for fold 5 Results for lemma compare_inv: : forall s s', compare s s' = CompOpp (compare s' s) FAILURE! Tactics applied: 10000 Original Proof: [induction s as [|l IHl o r IHr]; destruct s' as [|l' o' r']; trivial. unfold compare. case is_empty; reflexivity. unfold compare. case is_empty; reflexivity. simpl. rewrite compare_bool_inv. case compare_bool; simpl; trivial; apply lex_Opp; auto.] Proof search time: 0 min, 39 sec Number of successful tactic applications: 1951 Number of failed tactic applications: 8050 Results for lemma bits_lt_trans: : forall x y z : positive, bits_lt x y -> bits_lt y z -> bits_lt x z FAILURE! Tactics applied: 10000 Original Proof: [induction x; destruct y,z; simpl; eauto; intuition.] Proof search time: 0 min, 36 sec Number of successful tactic applications: 2002 Number of failed tactic applications: 7999 Results for lemma partition_spec2: : forall s f, compat_bool E.eq f -> Equal (snd (partition f s)) (filter (fun x => negb (f x)) s) FAILURE! Tactics applied: 10000 Original Proof: [intros. rewrite partition_filter. reflexivity.] Proof search time: 0 min, 42 sec Number of successful tactic applications: 2600 Number of failed tactic applications: 7401 Results for lemma lex_Eq: : forall u v, lex u v = Eq <-> u=Eq /\ v=Eq SUCCESS! Proof Found in EFSM: intros j acc; induction j; intuition congruence. Tactics applied: 9480 Original Proof: [intros u v; destruct u; intuition discriminate.] Shorter Proof Found? no This is a novel proof This proof contained a loop around a state proof search time: 0 min, 36 sec Number of successful tactic applications: 1564 Number of failed tactic applications: 7916 Results for lemma exists_spec: : forall s f, compat_bool E.eq f -> (exists_ f s = true <-> Exists (fun x => f x = true) s) FAILURE! Tactics applied: 10000 Original Proof: [intros. apply xexists_spec.] Proof search time: 0 min, 41 sec Number of successful tactic applications: 2296 Number of failed tactic applications: 7705 Results for lemma inter_spec: : forall s s' x, In x (inter s s') <-> In x s /\ In x s' FAILURE! Tactics applied: 10000 Original Proof: [unfold In. intros s s' x; revert x s s'. induction x; destruct s; destruct s'; simpl inter; rewrite ?mem_node; simpl mem; try (rewrite IHx; clear IHx); try intuition congruence. apply andb_true_iff.] Proof search time: 0 min, 43 sec Number of successful tactic applications: 2947 Number of failed tactic applications: 7054 Results for lemma mem_spec: : forall s x, mem x s = true <-> In x s SUCCESS! Proof Found in EFSM: reflexivity. Tactics applied: 42 Original Proof: [unfold In. intuition.] Shorter Proof Found? yes Single step proof reused proof search time: 0 min, 26 sec Number of successful tactic applications: 22 Number of failed tactic applications: 20 Results for lemma ct_compare_bool: : forall a b c, ct (compare_bool a b) (compare_bool b c) (compare_bool a c) FAILURE! Tactics applied: 10000 Original Proof: [intros [|] [|] [|]; constructor.] Proof search time: 0 min, 36 sec Number of successful tactic applications: 1797 Number of failed tactic applications: 8204 Results for lemma compare_x_Leaf: : forall s, compare s Leaf = if is_empty s then Eq else Gt SUCCESS! Proof Found in EFSM: intros [|l' o' r']; reflexivity. Tactics applied: 395 Original Proof: [intros. rewrite compare_inv. simpl. case (is_empty s); reflexivity.] Shorter Proof Found? yes This is a novel proof proof search time: 0 min, 27 sec Number of successful tactic applications: 66 Number of failed tactic applications: 329 Results for lemma compare_bool_Eq: : forall b1 b2, compare_bool b1 b2 = Eq <-> eqb b1 b2 = true FAILURE! Tactics applied: 10000 Original Proof: [intros [|] [|]; intuition discriminate.] Proof search time: 0 min, 36 sec Number of successful tactic applications: 1679 Number of failed tactic applications: 8322 Results for lemma empty_spec: : Empty empty SUCCESS! Proof Found in EFSM: intros j acc; induction j; intuition discriminate. Tactics applied: 7019 Original Proof: [unfold Empty, In. intro. rewrite mem_Leaf. discriminate.] Shorter Proof Found? yes This is a novel proof This proof contained a loop around a state proof search time: 0 min, 32 sec Number of successful tactic applications: 994 Number of failed tactic applications: 6025 OVERALL RESULTS SUMMARY EFSMProver proved 14 out of 67 lemmas. Success rate of 20.8955223880597% There were 0 errors. 53 proof attempts exhausted the automaton On average, a proof was found after applying 1741 tactics The longest proof consisted of 4 tactics There were 4 shorter proofs found Of the 53 failures, 53 of them used all 10000 tactics There were 7 reused proofs found There were 7 novel proofs found Of the 53 failures, the average number of tactics used was 10000 On average, a proof was found after 0 min, 26 sec On average, a failed proof attempt took 0 min, 39 sec On average, any (success or failure) proof attempt took 0 min, 36 sec The longest time to find a proof was 0 min, 36 sec The shortest time to find a proof was 0 min, 10 sec There were 0 proofs containing repeated tactics There were 2 proofs that repeated states