diff options
| author | Vincent Laporte | 2020-01-18 20:35:42 +0100 |
|---|---|---|
| committer | Vincent Laporte | 2020-03-19 08:05:07 +0100 |
| commit | e138fbf1e1cd95bfae05e17074f94a1ebde2edf8 (patch) | |
| tree | d6d1698cb15f83a4bbfae057f2ec932971d8ea1a /theories/Lists | |
| parent | daad81ddd72f4a8892b683d4f2b72345ff0bb84f (diff) | |
firstorder: default tactic is “auto with core”
Diffstat (limited to 'theories/Lists')
| -rw-r--r-- | theories/Lists/List.v | 19 |
1 files changed, 11 insertions, 8 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 6a1554d102..f050f11170 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -1413,13 +1413,16 @@ End Fold_Right_Recursor. Lemma existsb_exists : forall l, existsb l = true <-> exists x, In x l /\ f x = true. Proof. - induction l; simpl; intuition. - inversion H. - firstorder. - destruct (orb_prop _ _ H1); firstorder. - firstorder. - subst. - rewrite H2; auto. + induction l as [ | a m IH ]; split; simpl. + - easy. + - intros [x [[]]]. + - rewrite orb_true_iff; intros [ H | H ]. + + exists a; auto. + + rewrite IH in H; destruct H as [ x [ Hxm Hfx ] ]. + exists x; auto. + - intros [ x [ [ Hax | Hxm ] Hfx ] ]. + + now rewrite Hax, Hfx. + + destruct IH as [ _ -> ]; eauto with bool. Qed. Lemma existsb_nth : forall l n d, n < length l -> @@ -2747,7 +2750,7 @@ Section Exists_Forall. Proof. split. - induction 1; firstorder; subst; auto. - - induction l; firstorder. + - induction l; firstorder auto with datatypes. Qed. Lemma Forall_nth l : |