diff options
Diffstat (limited to 'doc/RecTutorial')
| -rw-r--r-- | doc/RecTutorial/RecTutorial.tex | 6 | ||||
| -rw-r--r-- | doc/RecTutorial/RecTutorial.v | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/doc/RecTutorial/RecTutorial.tex b/doc/RecTutorial/RecTutorial.tex index d0884be0d..01369b900 100644 --- a/doc/RecTutorial/RecTutorial.tex +++ b/doc/RecTutorial/RecTutorial.tex @@ -2978,7 +2978,7 @@ definition of \textsl{div\_aux}: \begin{alltt} Definition div_aux (x y:nat)(H: Acc lt x):nat. - fix 3. + fix div_aux 3. intros. refine (if eq_nat_dec x 0 then 0 @@ -3010,10 +3010,10 @@ Definition div x y := div_aux x y (lt_wf x). Let us explain the proof above. In the definition of \citecoq{div\_aux}, what decreases is not $x$ but the \textsl{proof} of the accessibility -of $x$. The tactic ``~\texttt{fix 3}~'' is used to indicate that the proof +of $x$. The tactic ``~\texttt{fix div\_aux 3}~'' is used to indicate that the proof proceeds by structural induction on the third argument of the theorem --that is, on the accessibility proof. It also introduces a new -hypothesis in the context, named as the current theorem, and with the +hypothesis in the context, named ``~\texttt{div\_aux}~'', and with the same type as the goal. Then, the proof is refined with an incomplete proof term, containing a hole \texttt{\_}. This hole corresponds to the proof of accessibility for $x-y$, and is filled up with the (smaller!) diff --git a/doc/RecTutorial/RecTutorial.v b/doc/RecTutorial/RecTutorial.v index 4b0ab3125..4a17e0818 100644 --- a/doc/RecTutorial/RecTutorial.v +++ b/doc/RecTutorial/RecTutorial.v @@ -922,7 +922,7 @@ Print minus_decrease. Definition div_aux (x y:nat)(H: Acc lt x):nat. - fix 3. + fix div_aux 3. intros. refine (if eq_nat_dec x 0 then 0 |