Julin S (Oct 12 2022 at 09:43): 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?
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).
Oh.. that makes sense. Thank you.
Julin S (Oct 12 2022 at 09:54):Should've had a closer look at the docs.
Notification Bot (Oct 12 2022 at 09:54):Julin S has marked this topic as resolved.
Last updated: Sep 30 2023 at 05:01 UTC