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