The Coq mailing list

[David Delahaye <delahaye AT jurancon.inria.fr>]

    Hi Laurent,

> This is possible in Coq using the tactic Cut 
> 
> Cut a0=b0; [Intros Fact1 | Idtac]
> 
> Macros definition can make the syntax close to what you propose.

    Of course, it's a possibility but with your solution, you see all the 
goals
of the main proof you don't want to deal with. With a real subproof, you can
focus on the goals generated only by this subproof and that's it. Randy's idea
which makes subproofs be local to the main proof rather than declared at
toplevel is quite natural.

> In HOL they also have a tactic "by" inspired by Mizard that is pretty handy:
> 
> a0=b0 by THE_TACTIC_THAT_PROVES_A0=BO
> 
> It gives a nice declarative flavor to your proof scripts. 

    In Mizar itself, you have a local proof system you use as follows:

    <label>: <Proposition>
             proof
             ...
             end

    ... by <label>

    Which can appear in a proof script.

> You can define one. In my proofs I often use the following constant:
> 
> Definition LetP: (A, B:Set) (h:A) ((u:A) u =h ->B) ->B.
> Intros A B h H'.
> Apply H' with u := h.
> Auto.
> Defined.
> 
> When I want to name an object locally I simply apply LetP.

    Yes, but in that way, it is not primitive.

    Regards.

    David.

===============================================================================
David Delahaye                                 <Email>: 
David.Delahaye AT inria.fr
<Laboratory>: The Coq Project                                  <Domain>: 
Proofs
<Adress>: INRIA-Rocquencourt Domaine de Voluceau BP105 78153 Le Chesnay Cedex
          FRANCE
<Tel>: (33)-(0)1 39 63 57 53
<Fax>: (33)-(0)1 39 63 56 84
<Url>: http://pauillac.inria.fr/~delahaye
===============================================================================

[If you have time to waste, you can have a look on my pretty proof that
 1=0.9999...:

   a=0.9999...            (a simple definition)
   10*a=9.9999...         (multiplication by 10)
   10*a=9+0.9999...       (separation of the integer and fractional parts)
   10*a=9+a               (by defintion of a)
   10*a-a=9               (we put a in the left-hand side)
   9*a=9                  (simplification of the left member)
   a=1                    (we divide the two members by 9)

 So 1=0.9999... Two writes for the same number? It's quite strange, isn't it?]