Stream: Coq users

Topic: Allowing nested proof in Coq

Jovial Cheukam (Nov 26 2020 at 09:32):

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.

Fabian Kunze (Nov 26 2020 at 09:33):

Set Nested Proofs Allowed.

Fabian Kunze (Nov 26 2020 at 09:34):

Flags can be Set $flag. and Unset $flag.

Fabian Kunze (Nov 26 2020 at 09:34):

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

Théo Winterhalter (Nov 26 2020 at 09:35):

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

Jovial Cheukam (Nov 26 2020 at 09:41):

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 ?

Fabian Kunze (Nov 26 2020 at 09:43):

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.

Fabian Kunze (Nov 26 2020 at 09:43):

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

Théo Winterhalter (Nov 26 2020 at 09:47):

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.

Jovial Cheukam (Nov 26 2020 at 09:49):

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.

Fabian Kunze (Nov 26 2020 at 09:52):

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?

Théo Winterhalter (Nov 26 2020 at 09:52):

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

Jovial Cheukam (Nov 26 2020 at 09:55):

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. .

Jovial Cheukam (Nov 26 2020 at 09:57):

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

Théo Winterhalter (Nov 26 2020 at 10:00):

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)?

Théo Winterhalter (Nov 26 2020 at 10:01):

Please use

```coq
your code

Fabian Kunze (Nov 26 2020 at 10:12):

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_Smaybe).

Enrico Tassi (Nov 26 2020 at 10:30):

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".

Jovial Cheukam (Nov 26 2020 at 10:42):

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

Enrico Tassi (Nov 26 2020 at 10:48):

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

Fabian Kunze (Nov 26 2020 at 10:48):

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

Fabian Kunze (Nov 26 2020 at 11:01):

coq/coq#13482

Théo Zimmermann (Nov 26 2020 at 11:08):

Great answers and thanks for the PR!

Théo Zimmermann (Nov 26 2020 at 11:10):

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.

Gaëtan Gilbert (Nov 26 2020 at 11:13):

we see the extra confusing aspects instead

Karl Palmskog (Nov 26 2020 at 11:15):

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

Fabian Kunze (Nov 26 2020 at 11:18):

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

Théo Zimmermann (Nov 26 2020 at 11:22):

Feel free to participate in reviewing the PR ;-)

Last updated: Apr 19 2024 at 14:02 UTC