Meaning of `eato 10`?

[rhs0266]

At 12_05 assignment, I believe my halve is well-defined.

I passed Example halve_type: empty |- halve \in TArrow TNat TNat. Proof. unfold halve; eauto 10. Qed.

Example halve_10: tapp halve (tnat 10) ==>* tnat 5. Proof. unfold halve; normalize. Qed.

Example halve_11: tapp halve (tnat 11) ==>* tnat 5. Proof. unfold halve; normalize. Qed. All of those examples.

1. What is the meaning of eauto 10 at first example?
2. Why can't I pass

Example halve_30: tapp halve (tnat 11) ==>* tnat 15. Proof. unfold halve; normalize. Qed.

with this error,

In nested Ltac calls to "normalize" and "apply multi_refl" (expanded to "apply multi_refl"), last call failed. ?

Is there limit of stack depth when using normalize?

[jaewooklee93]

eauto is basically searching for proof over tree. It has default search depth of 5. eauto 10 specifies the search depth to be 10 to get much extensive search (but slower at the same time). There are rare cases simple eauto fails but eauto 10 succeeds.

normalize is not an official tactic but author's custom tactic defined at the file Types.v

Tactic Notation "normalize" := 
   repeat (print_goal; eapply multi_step ; 
             [ (eauto 10; fail) | (instantiate; simpl)]);
   apply multi_refl.

Now you may see the reason. The definition of normalize already fixed its search depth to 10. Therefore, the following works.

Tactic Notation "deep_normalize" := 
   repeat (print_goal; eapply multi_step ; 
             [ (eauto 20; fail) | (instantiate; simpl)]);
   apply multi_refl.

Example halve_30: tapp halve (tnat 30) ==>* tnat 15.
Proof.
unfold halve; deep_normalize.
Qed.

[rhs0266]

Wow... I've never heard about existence of 'depth'... Thank you very much

[woong8556]

For a simpler example, try the following:

Example eauto10_example : 3<11. Proof. try eauto. eauto 10. Qed.