The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Le mardi 4 août 2015, Soegtrop, Michael <michael.soegtrop AT intel.com> a écrit :

Dear Pierre,

 

the reason I am using nested lemmas instead of assert is that I want to add them to a hint database. I don’t think this works with assert. There are several reasons for using hint databases:

I would support the feature of adding temporarily hypothesis to hint db. I think there is a limited support for that in 8.5. 

 

 

-          I might have several remaining goals which might profit from the new lemma. An assert is limited to the current goal.

I also had this problem and couldn't manage to move the [assert] high enough in the proof script to share it among all subgoals. I still think that moving the nested lemma outside does not harm. Adding a comment saying "technical lemma, see where it is applied for details."

 

-          It might be very tedious to use the new lemma without the proof automation system.

 

If I want to do this without nested lemmas, I can only go back and start the proof from scratch.

I also do use nested lemmas but only temporarily. Generally I proceed as follows.

1) first use an assert. This is faster.

2) once proved I restate the assert to be closed under context and make it a nested lemma. 

3) when I can (i.e. have some time) I move the nested lemma to a non nested position.

 

The documentation argument can of cause be discussed. I still think this style gives the motivation for a lemma, but I wouldn’t call it justification. Quite a few of the lemmas I create this way are useful in other contexts as well, but it is sometimes quite hard to explain in which situation this lemma is useful. If someone is interested, he can still go to the specific point in the proof and see why the lemma is useful at least in this specific case.

Shouldn't you then point to the places it is *used*? No matter where it is proved. If the lemma is used blindly by an automated tactic then put a comment (* this makes use of technical lemma foo*).

 

This usually gives good hints on why it might be useful in other cases as well. For the not so curious reader of a proof, her does still see that this lemma was required to get through this proof without additional documentation.

 

I think it is an interesting question if somebody uses the current proof context in the new lemma as you described. I actually never did this. The lemmas I proof nested are independent lemmas and could be stated at the top level in the same way. Otherwise it wouldn’t make sense to add them to a hint database. So would it simplify things if we restrict nested lemmas such that they may not depend in any way on the current proof context?

It is the case afaik. This may sound reasonable but it is actually a way to break the logical structure of the proof document as it is now. But we can probably imagine a refined document model where independent nested lemma are allowed. 

P. 

 I think if I would like to have a lemma only useful in the current context, I rather would use assert as you suggest.

Best regards,

Michael