Results for fold 1
Results for lemma compare_spec: : forall s s' : t, CompSpec eq lt s s' (compare s s')
FAILURE!
Tactics applied: 10000
Original Proof: [intros. case_eq (compare s s'); intro H; constructor. apply compare_eq, H. assumption. apply compare_gt, H.]
Proof search time: 0 min, 15 sec
Number of successful tactic applications: 2131
Number of failed tactic applications: 7870
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, 16 sec
Number of successful tactic applications: 2592
Number of failed tactic applications: 7409
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, 20 sec
Number of successful tactic applications: 2718
Number of failed tactic applications: 7283
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, 17 sec
Number of successful tactic applications: 2543
Number of failed tactic applications: 7458
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, 17 sec
Number of successful tactic applications: 2596
Number of failed tactic applications: 7405
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, 17 sec
Number of successful tactic applications: 2636
Number of failed tactic applications: 7365
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, 14 sec
Number of successful tactic applications: 1683
Number of failed tactic applications: 8318
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, 16 sec
Number of successful tactic applications: 2202
Number of failed tactic applications: 7799
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, 16 sec
Number of successful tactic applications: 2137
Number of failed tactic applications: 7864
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, 17 sec
Number of successful tactic applications: 2043
Number of failed tactic applications: 7958
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, 18 sec
Number of successful tactic applications: 2630
Number of failed tactic applications: 7371
Results for lemma ct_xgg: : forall x, ct x Gt Gt
SUCCESS!
Proof Found in EFSM: induction x; constructor.
Tactics applied: 188
Original Proof: [destruct x; constructor.]
Shorter Proof Found? no
This is a novel proof
proof search time: 0 min, 3 sec
Number of successful tactic applications: 37
Number of failed tactic applications: 151
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, 20 sec
Number of successful tactic applications: 2815
Number of failed tactic applications: 7186
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, 16 sec
Number of successful tactic applications: 2202
Number of failed tactic applications: 7799
Results for lemma ct_gxg: : forall x, ct Gt x Gt
SUCCESS!
Proof Found in EFSM: induction x; constructor.
Tactics applied: 188
Original Proof: [destruct x; constructor.]
Shorter Proof Found? no
This is a novel proof
proof search time: 0 min, 3 sec
Number of successful tactic applications: 37
Number of failed tactic applications: 151
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, 19 sec
Number of successful tactic applications: 2752
Number of failed tactic applications: 7249
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, 17 sec
Number of successful tactic applications: 2271
Number of failed tactic applications: 7730
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, 19 sec
Number of successful tactic applications: 2550
Number of failed tactic applications: 7451
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, 23 sec
Number of successful tactic applications: 2869
Number of failed tactic applications: 7132
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, 17 sec
Number of successful tactic applications: 2584
Number of failed tactic applications: 7417
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, 17 sec
Number of successful tactic applications: 2630
Number of failed tactic applications: 7371
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, 17 sec
Number of successful tactic applications: 2007
Number of failed tactic applications: 7994
Results for lemma compare_x_Leaf: : forall s, compare s Leaf = if is_empty s then Eq else Gt
SUCCESS!
Proof Found in EFSM: induction s as [| l IHl o r IHr]; constructor.
Tactics applied: 192
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, 3 sec
Number of successful tactic applications: 46
Number of failed tactic applications: 146
Results for lemma mem_spec: : forall s x, mem x s = true <-> In x s
SUCCESS!
Proof Found in EFSM: reflexivity.
Tactics applied: 110
Original Proof: [unfold In. intuition.]
Shorter Proof Found? yes
Single step proof reused
proof search time: 0 min, 2 sec
Number of successful tactic applications: 39
Number of failed tactic applications: 71
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, 16 sec
Number of successful tactic applications: 2105
Number of failed tactic applications: 7896
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, 16 sec
Number of successful tactic applications: 1994
Number of failed tactic applications: 8007
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, 15 sec
Number of successful tactic applications: 2045
Number of failed tactic applications: 7956
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, 16 sec
Number of successful tactic applications: 1994
Number of failed tactic applications: 8007
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, 17 sec
Number of successful tactic applications: 2642
Number of failed tactic applications: 7359
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, 18 sec
Number of successful tactic applications: 2340
Number of failed tactic applications: 7661
Results for lemma lex_Eq: : forall u v, lex u v = Eq <-> u=Eq /\ v=Eq
FAILURE!
Tactics applied: 10000
Original Proof: [intros u v; destruct u; intuition discriminate.]
Proof search time: 0 min, 14 sec
Number of successful tactic applications: 1404
Number of failed tactic applications: 8597
Results for lemma ct_compare_bool: : forall a b c, ct (compare_bool a b) (compare_bool b c) (compare_bool a c)
SUCCESS!
Proof Found in EFSM: induction a as [|l IHl o r IHr]; intros [|] [|]; intuition.
Tactics applied: 7291
Original Proof: [intros [|] [|] [|]; constructor.]
Shorter Proof Found? no
This is a novel proof
proof search time: 0 min, 11 sec
Number of successful tactic applications: 1643
Number of failed tactic applications: 5648
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, 15 sec
Number of successful tactic applications: 2005
Number of failed tactic applications: 7996
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, 20 sec
Number of successful tactic applications: 2749
Number of failed tactic applications: 7252
Results for fold 2
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, 21 sec
Number of successful tactic applications: 1875
Number of failed tactic applications: 8126
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, 21 sec
Number of successful tactic applications: 1695
Number of failed tactic applications: 8306
Results for lemma bits_lt_antirefl: : forall x : positive, ~ bits_lt x x
FAILURE!
Tactics applied: 10000
Original Proof: [induction x; simpl; auto.]
Proof search time: 0 min, 17 sec
Number of successful tactic applications: 815
Number of failed tactic applications: 9186
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, 19 sec
Number of successful tactic applications: 1604
Number of failed tactic applications: 8397
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, 20 sec
Number of successful tactic applications: 1637
Number of failed tactic applications: 8364
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, 21 sec
Number of successful tactic applications: 2043
Number of failed tactic applications: 7958
Results for lemma ct_cxe: : forall x, ct (CompOpp x) x Eq
SUCCESS!
Proof Found in EFSM: destruct x; constructor.
Tactics applied: 53
Original Proof: [destruct x; constructor.]
Shorter Proof Found? no
Proof reused from ct_xgg
This proof contained a loop around a state
proof search time: 0 min, 8 sec
Number of successful tactic applications: 12
Number of failed tactic applications: 41
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, 18 sec
Number of successful tactic applications: 1136
Number of failed tactic applications: 8865
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, 20 sec
Number of successful tactic applications: 1678
Number of failed tactic applications: 8323
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, 21 sec
Number of successful tactic applications: 2040
Number of failed tactic applications: 7961
Results for lemma ct_lxl: : forall x, ct Lt x Lt
SUCCESS!
Proof Found in EFSM: destruct x; constructor.
Tactics applied: 53
Original Proof: [destruct x; constructor.]
Shorter Proof Found? no
Proof reused from ct_xgg
This proof contained a loop around a state
proof search time: 0 min, 8 sec
Number of successful tactic applications: 12
Number of failed tactic applications: 41
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, 20 sec
Number of successful tactic applications: 1946
Number of failed tactic applications: 8055
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, 25 sec
Number of successful tactic applications: 2405
Number of failed tactic applications: 7596
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, 21 sec
Number of successful tactic applications: 1593
Number of failed tactic applications: 8408
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, 27 sec
Number of successful tactic applications: 2725
Number of failed tactic applications: 7276
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, 22 sec
Number of successful tactic applications: 2212
Number of failed tactic applications: 7789
Results for lemma compare_spec: : forall x y, CompSpec eq lt x y (compare x y)
FAILURE!
Tactics applied: 10000
Original Proof: [intros. case_eq (compare s s'); intro H; constructor. apply compare_eq, H. assumption. apply compare_gt, H.]
Proof search time: 0 min, 19 sec
Number of successful tactic applications: 1472
Number of failed tactic applications: 8529
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, 22 sec
Number of successful tactic applications: 1926
Number of failed tactic applications: 8075
Results for lemma compare_bool_inv: : forall b b', compare_bool b b' = CompOpp (compare_bool b' b)
FAILURE!
Tactics applied: 10000
Original Proof: [intros [|] [|]; reflexivity.]
Proof search time: 0 min, 18 sec
Number of successful tactic applications: 1244
Number of failed tactic applications: 8757
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, 20 sec
Number of successful tactic applications: 2036
Number of failed tactic applications: 7965
Results for lemma empty_spec: : Empty empty
SUCCESS!
Proof Found in EFSM: intros u v; destruct u; intuition discriminate.
Tactics applied: 1556
Original Proof: [unfold Empty, In. intro. rewrite mem_Leaf. discriminate.]
Shorter Proof Found? yes
Proof reused from lex_Eq
proof search time: 0 min, 9 sec
Number of successful tactic applications: 206
Number of failed tactic applications: 1350
Results for lemma subset_Leaf_s: : forall s, Leaf [<=] s
SUCCESS!
Proof Found in EFSM: intro f. intros u v; destruct u; intuition discriminate.
Tactics applied: 9300
Original Proof: [intros s i Hi. apply empty_spec in Hi. elim Hi.]
Shorter Proof Found? no
This is a novel proof
proof search time: 0 min, 17 sec
Number of successful tactic applications: 1693
Number of failed tactic applications: 7607
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, 25 sec
Number of successful tactic applications: 2735
Number of failed tactic applications: 7266
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, 21 sec
Number of successful tactic applications: 2124
Number of failed tactic applications: 7877
Results for lemma mem_Leaf: : forall x, mem x Leaf = false
SUCCESS!
Proof Found in EFSM: destruct x; constructor.
Tactics applied: 53
Original Proof: [destruct x; trivial.]
Shorter Proof Found? no
Proof reused from ct_xgg
This proof contained a loop around a state
proof search time: 0 min, 8 sec
Number of successful tactic applications: 12
Number of failed tactic applications: 41
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, 21 sec
Number of successful tactic applications: 2368
Number of failed tactic applications: 7633
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, 25 sec
Number of successful tactic applications: 2492
Number of failed tactic applications: 7509
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, 25 sec
Number of successful tactic applications: 2718
Number of failed tactic applications: 7283
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, 23 sec
Number of successful tactic applications: 2180
Number of failed tactic applications: 7821
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, 20 sec
Number of successful tactic applications: 1972
Number of failed tactic applications: 8029
Results for lemma ct_xce: : forall x, ct x (CompOpp x) Eq
SUCCESS!
Proof Found in EFSM: destruct x; constructor.
Tactics applied: 53
Original Proof: [destruct x; constructor.]
Shorter Proof Found? no
Proof reused from ct_xgg
This proof contained a loop around a state
proof search time: 0 min, 8 sec
Number of successful tactic applications: 12
Number of failed tactic applications: 41
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, 20 sec
Number of successful tactic applications: 1923
Number of failed tactic applications: 8078
Results for lemma ct_xll: : forall x, ct x Lt Lt
SUCCESS!
Proof Found in EFSM: destruct x; constructor.
Tactics applied: 53
Original Proof: [destruct x; constructor.]
Shorter Proof Found? no
Proof reused from ct_xgg
This proof contained a loop around a state
proof search time: 0 min, 8 sec
Number of successful tactic applications: 12
Number of failed tactic applications: 41
OVERALL RESULTS SUMMARY
EFSMProver proved 12 out of 67 lemmas. Success rate of 17.91044776119403%
There were 0 errors.
55 proof attempts exhausted the automaton
On average, a proof was found after applying 1590 tactics
The longest proof consisted of 4 tactics
There were 3 shorter proofs found
Of the 55 failures, 55 of them used all 10000 tactics
There were 7 reused proofs found
There were 5 novel proofs found
Of the 55 failures, the average number of tactics used was 10000
On average, a proof was found after 0 min, 7 sec
On average, a failed proof attempt took 0 min, 19 sec
On average, any (success or failure) proof attempt took 0 min, 17 sec
The longest time to find a proof was 0 min, 17 sec
The shortest time to find a proof was 0 min, 2 sec
There were 0 proofs containing repeated tactics
There were 5 proofs that repeated states