coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Basic question on navigating inductive proofs
- Date: Wed, 05 Sep 2007 10:57:37 +0200
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:user-agent:mime-version:cc:subject:references:in-reply-to:content-type:content-transfer-encoding:sender; b=FKewPJM4BKpZLoJPUOZRTGSCYTyk7m0G6mdUSPC/ZqNskjzXc1t4NuIErty798Z9+RnoMemNecDzTIhcgJcnFWdksOqC9iMqbDj3LyQr+Raf2AdQJ4AIRg69V0OdmUVxExEcLTuUWokBrm3EAu2jj7FQ9xxl8slmdHfzN4udIfs=
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hi thread,
I'm kinda sorry, I was a bit abroad, didn't read all the mails, let the mailling lists bombing me with thousands of new technical stuff every day.
However, I guess I had to mention that some work around the proof engine is currently being done. One of the feature that is meant to be implemented is related to that. Even though its final form is not currently known, the goal is to give a native tool (not only manual indentation and commenting) to structure a proof. Unfortunately, we will not be able at this point to provide some stuff like "Case 0", "Case S", though this was seen as an interesting long term option. But we want to introduce keywords to ensure that a certain goal is being solved entirely before we move to the next one, which resembles the feature you are asking for.
PS : in any case, the old dirty way is still possible, thus tacticals won't be affected. This is an optional mechanism.
Arnaud Spiwack
Benjamin Pierce a écrit :
When writing or reading big inductive proofs in Coq, I find it's quite difficult to keep track of which case of the induction one is in at any given moment: The proof script doesn't signal explicitly when one case is finished and we are moving on to the next.
What do people do about this?
Here's one idea I've been wondering about. I suppose it would not be impossible to write a variant of the induction tactic (say, induction_with_cases) that would somehow leave a marker at the top of each subgoal, containing the name of the case that generated it. (I.e., a subgoal "prove P" arising from case C of an inductive definition would become a goal of the form "prove something trivial involving the string C and then prove P.") Then one could have a tactic "Case C" that would supply the trivial proof involving C and uncover the subgoal P to be proved next. Now a proof by induction would look like this:
Proof.
intros.
induction_with_cases H1.
Case C1. ...
Case C2. ...
...
Qed.
One problem I can see with this is that notations like "induction; ..." would not work so well -- perhaps there would need to be a variant of ; (or something to put at the beginning of the "...") that would treat the case markers in the subgoals transparently. And perhaps there are other problems that I don't see. :-)
Would this be a good idea? Has it been done?
Thanks,
- Benjamin
P.S. I'm sure this general topic must have been discussed before, but I'm not sure what keywords to search for...! Pointers appreciated.
--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
- Re: [Coq-Club] Basic question on navigating inductive proofs, Arnaud Spiwack
- RE: [Coq-Club] Basic question on navigating inductive proofs,
Georges Gonthier
- Re: [Coq-Club] Basic question on navigating inductive proofs, Benjamin Pierce
- RE: [Coq-Club] Basic question on navigating inductive proofs,
Georges Gonthier
Archive powered by MhonArc 2.6.16.