Stream: Coq users

Topic: Allowing nested proof in Coq


view this post on Zulip 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.

view this post on Zulip Fabian Kunze (Nov 26 2020 at 09:33):

Set Nested Proofs Allowed.

view this post on Zulip Fabian Kunze (Nov 26 2020 at 09:34):

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

view this post on Zulip 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.

view this post on Zulip Théo Winterhalter (Nov 26 2020 at 09:35):

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

view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip Fabian Kunze (Nov 26 2020 at 09:43):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Théo Winterhalter (Nov 26 2020 at 09:52):

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

view this post on Zulip 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. .

view this post on Zulip Jovial Cheukam (Nov 26 2020 at 09:57):

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

view this post on Zulip 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)?

view this post on Zulip Théo Winterhalter (Nov 26 2020 at 10:01):

Please use

```coq
your code

view this post on Zulip 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).

view this post on Zulip 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".

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Fabian Kunze (Nov 26 2020 at 11:01):

coq/coq#13482

view this post on Zulip Théo Zimmermann (Nov 26 2020 at 11:08):

Great answers and thanks for the PR!

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Nov 26 2020 at 11:13):

we see the extra confusing aspects instead

view this post on Zulip 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

view this post on Zulip Fabian Kunze (Nov 26 2020 at 11:18):

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

view this post on Zulip Théo Zimmermann (Nov 26 2020 at 11:22):

Feel free to participate in reviewing the PR ;-)


Last updated: Feb 01 2023 at 11:04 UTC