The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

Until this is implemented, let me suggest a very ugly combination of
assert + abstract. The ugly part is that the definition name generated
by abstract is automatically chosen by coq (it seems deterministic
however) and that you have to look at the environment to know it. The
other ugly part is that you have to put the abstract on the hole set
of tactics used to prove the sub-lemma, which forces you to put
semi-colons everywhere.


Require Export Arith.
Lemma big: forall x y:nat, x<y \/ x<=y.
Proof.
  intros x y.
  (* let us start a subproof. *)
  assert (sub: x=0 \/ x > 0).
  abstract (destruct x; auto with arith). (* the whole subproof should
be one abstracted tactic. *)
  Inspect 1. (* Tells you the name of definition generated by abstract. *)
  Print big_subproof. (* the body of the subproof can be used. *)
  ...
  Qed.


Notice that only the hypothesis really used in the body of the
subproof are generalized.

Notice also that coqide is not completely synchronize with abstract
tactical, that is if you want to reset big_subproof you will have to
restart the proof of big itself, otherwise abstract will generate
another big_subproof0. Proofgeneral deals with this a bit better.

Yes it *is* ugly.

Hope this helps anyway,
Pierre


2010/4/7 AUGER 
<Cedric.Auger AT lri.fr>:
> Le Wed, 07 Apr 2010 14:11:24 +0200, Pierre-Marie Pédrot
>Â <pierremarie.pedrot AT ens-lyon.fr>
>  a écrit:
>
>> AUGER wrote:
>>>
>>> I think this feature should be "consistant with Coq spirit",
>>> but it is not implemented so.
>>
>> Yet obviously it deserves to, so I filed a bug report:
>>
>> http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2291
>>
>> Feel free to add some details.
>>
>> PMP
>>
> That is not really what I meant:
> I said that nested lemmas should be generalized according to current local
> hypothesis,
> and not start an interactive proof with an empty environnement,
> allowing you to have:
>
> Section foo.
>  Lemma bar: foobar.
>  Proof.
>  ...
>  (*A*)
>  Let x : barfoo.
>  Proof.
>   (*B*)
>   ...
>  Defined.
>  ...
>  Qed.
> End foo.
>
> So that in point (*B*) we have exactly same hypotheses as in point (*A*).
>
> The tactic assert_body you suggest is less readable, but shorter and usable
> in Ltac;
> but I am almost certain it cannot be done without the "Defined/Qed"
> verification at the end
> of the new subproof, as we want the terms appearing in hypotheses to be well
> typed/formed,
> so that type checking will be performed in more than one place and the
> tactic will be a little
> slower than you may expect.
>
> If "x" is very important in the proof, I think it deserves a "Let",
> which would be generalized at "Defined" time according to the used
> hypothesis of (*A*)
>
> Personnaly, I would rather call "transparent assert" your "assert_body", but
> that is
> purely personnal taste.
>
> --
> Cédric AUGER
>
> Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay
>
>