Stream: Coq users

Topic: ✔ Using `auto` tactic


view this post on Zulip Julin S (Oct 12 2022 at 09:43):

I was trying out the auto tactic with

Goal 3 < 5. Proof. auto. Qed.
Goal 3 < 6. Proof. auto. Qed.
Goal 3 < 7. Proof. auto. Qed.

All three of these goals were solved with auto.

But this one couldn't be:

Goal 3 < 8. Proof. auto. .

I guess it has something to do with auto works. What is it?

view this post on Zulip Pierre Castéran (Oct 12 2022 at 09:47):

auto has a search depth argument (default 5).
In your example auto 6(or bigger) works.

info_auto 6.
(* info auto: *)
unfold lt (in core).
 simple apply le_S (in core).
  simple apply le_S (in core).
   simple apply le_S (in core).
    simple apply le_S (in core).
     simple apply le_n (in core).

view this post on Zulip Julin S (Oct 12 2022 at 09:53):

Oh.. that makes sense. Thank you.

view this post on Zulip Julin S (Oct 12 2022 at 09:54):

Should've had a closer look at the docs.

view this post on Zulip Notification Bot (Oct 12 2022 at 09:54):

Julin S has marked this topic as resolved.


Last updated: Jan 31 2023 at 12:01 UTC