The Coq mailing list

[Per Lindgren <per.lindgren AT ltu.se>]

Hi

Would it be possible for Coq to check that the below cases (and potentially other problematic ones) is not  present, and accept them in such cases?

In that case, we might have the best of “two worlds”. 

Best,

  Per

On 04 Aug 2015, at 11:07, Cedric Auger <sedrikov AT gmail.com> wrote:

I still think of the context problem.

I mainly see these bad things:

* The lemma statement might depend on the context.

  That mainly implies that when you read the lemma statement

  written in the script, you have to run the script up to the

  point where the lemma is defined to get the full context, and

  understand what variables are (especially when you use a local definition).

* Some hypothesis may be present in the context, but not restated in the lemma,

  Thus you can see confusing things like "Lemma foo : forall y, y>=x." without

  having a "forall (x:nat), x=0 ->" prefixing the lemma, which can be confusing.

  (And again, you have to run the script up to that point to understand what the

   lemma means.)

* During the proof, some variable overloading may occur, bringing more confusion to

  what is what.

  Variable x : nat.

  Lemma foo: x>0 -> x≠0.

  Proof.

    destruct x as [|x].

    + <script solving 0>0 -> 0≠0>

    + Lemma bar: (S x)≠0.

      <script solving it>

      Qed.

      <end of proof>

  Qed.

  In this settings, you are tempted to believe that the "x" in "bar" is the same as

  the one in "foo", which would make "bar" look totally useless.

* There is still the problem of not having cleaned the context before defining the

  nested lemma. Someone who would compile the file as a .vo file, and then print

  its contents to see what lemmas could be usefull to him can be flooded with a lemma

  containing long unneeded hypotheses.

* Always with not cleaning context before proving the nested lemma: if at

  a later point, in which some unneeded hypothesis has been cleaned or has never existed in

  this branch, then your lemma won't apply even if it looks like it could.

2015-08-04 9:55 GMT+02:00 Soegtrop, Michael <michael.soegtrop AT intel.com>:

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 might have several remaining goals which might profit from the new lemma. An assert is limited to the current goal.

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

 

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

 

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Pierre Courtieu
Sent: Monday, August 03, 2015 9:57 PM
To: coq-club AT inria.fr
Subject: [Coq-Club] "Nested proofs are deprecated and will stop working in the next Coq version" - Can we keep this?

 

Hi, my two cents:

 

IMHO there is a contradiction between the "documentation" argument and the need of having nested lemma visible outside their scope. If you consider a lemma is only justified by the current state of the outer proof then it has no reason to be visible outside, and you should use assert. If your lemma is useful outside the current proof then it should not stay nested except temporarily for efficiency reason and it should be documented on its own. The same probably applies to Adam's remark on the bad side effects of moving a lemma from the nested position to the outside position. If your nested lemma is used elsewhere then the side effect is likely to appear later anyway. Better play with hint stuff inside lemmas then (btw is it possible to add a hypothesis to hints?)

 

I think that having a strict document structure is important. For scalability, tooling, documenting etc. nested lemmas as they are currently implemented is a serious hole in this structure. That said I use them very frequently but always as a temporary state when it would take too much time right now to rerun the current proof. I also hope that this use will remain possible.

 

Best

Pierre

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Prof. Dr. Hermann Eul
Chairperson of the Supervisory Board: Tiffany Doon Silva
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928