After the line Definition manual_grade_for_destruct_induction : option (nat*string) := None.
in the code I get the error "Nested proofs are not allowed unless you turn the Nested Proofs Allowed flag on."
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