After the line ** Definition manual_grade_for_destruct_induction : option (nat*string) := None.
** in the code I get the error

What's the manner to turn on the use of nested proofs , please ? Thanks in advance.

`Set Nested Proofs Allowed.`

Flags can be `Set $flag.`

and `Unset $flag.`

I would suggest not using nested proofs in the "final" product, but they can be usefull during development.

Right, did you intend to use nested proofs at all?

I am newbie in Coq so I don't understand about "final" product. And Yes , I want to learn how to use nested proof, so should I put the command `Set Nested Proofs Allowed.`

in the file of code before the **proof** ?

Nested proof means you start a new lemma _inside_ the `Proof. ... Qed.`

of another lemma.

That can confuse your IDE, and usually one just cut/paste the "new" lemma before the current lemma and proves it there instead.

(And then one does not need to allow nested proofs at all)

Especially if you are new to Coq I would discourage the use of nested proofs.

If you want to have a local lemma in a proof, you should rather use the `assert`

tactic.

```
Lemma foo : 0 = 0.
Proof.
assert (aux : forall (n : nat), n = n).
{ intro. reflexivity. }
apply aux.
Qed.
```

Ok! I understand. But can you do that for this code ? ```
Theorem plus_rearrange_firsttry : forall n m p q : nat,
(n + m) + (p + q) = (m + n) + (p + q).
```

where you must use the `Lemma plus_comm: forall n m : nat, m+n = n+m.`

To use a pre-existing lemma, you can use `apply`

or, in this case, `rewrite`

to rewrite with an equality.

But as far as I see, SF itself shows exactly how to use `assert`

in this case, did you look into the chapter?

Just prove the lemma before the theorem as suggested by Fabian.

Ok! But when I want to just cut/paste the "new" lemma before the current lemma and proves it there instead, i get the error suggested early because of the line ** Definition manual_grade_for_destruct_induction : option (nat*string) := None.
**.

I am working in the file *induction.v* of **sofware fundations**

Can you show you the part of your file with the lemma, where you want to apply it, and everything in between (if it's not too long)?

Please use

```
```coq
your code
```

A wild guess of what might have gone wrong would be that somewhere before the definition `manual_grade_for_destruct_induction`

, you forgot the final `Qed`

(or `Admitted`

) to close the proof (for example at `Theorem evenb_S`

maybe).

FTR: the option `Set Nested Proofs Allowed.`

is there to enable very few and very specific use cases. In general it should be avoided and in common practice the error "Nested proofs are not allowed unless you turn the Nested Proofs Allowed flag on." really means "You forgot to end a proof with Qed".

Thanks and excuse me for inconvenience caused...I forgot the `Qed' as you said Fabian. THanks again.

No worries, actually, this hints that the error message is not clear enough! Let's CC a doc maintainer @Théo Zimmermann

No problem, I think I will put op a pull request to change coq for more helpfull error messages

Great answers and thanks for the PR!

BTW @Jovial Cheukam, don't be sorry. We *love* getting confused beginners' questions because this is how we learn what is wrong / unclear with the doc, error messages, etc. All of us are so used to this system that we can't see confusing aspects anymore.

we see the extra confusing aspects instead

for someone who started using Coq when nested proofs were allowed, the meaning is 100% clear, so I hope you add to the error message rather than rewriting it completely

I think both things shall and will be mentioned in the eror message.

Feel free to participate in reviewing the PR ;-)

Last updated: Oct 13 2024 at 01:02 UTC