The Coq mailing list

[Math Prover <mathprover AT gmail.com>]

Hi Vincent,


  Thanks for your instructive example. What I found really insightful about your example -- is that it's a bit "lisp-ish" in the sense of "code is data; data is code", except here you're doing

  "coq Lists -> coq Props" (Fixpoints And, Imp, ImpMP ) and
  "coq Props -> coq Lists" (Ltacs constr_lB, constr_lP, tail_lP )

which was rather eye-opening in breaking down the barrier between "coq Code I write" and "statements I want to prove."

  I'm going to claim I fully understand this example yet -- but thanks for sharing this new technique!

  I have one question about your example: I don't understand what "constr:" means.

  Google brought up 

== BEGIN ==

http://adam.chlipala.net/cpdt/html/Match.html

Each position within an Ltac script has a default applicable non-terminal, where constrand ltac are the main options worth thinking about, standing respectively for terms of Gallina and Ltac. The explicit colon notation can always be used to override the default non-terminal choice, though code being parsed as Gallina can no longer use such overrides. Within the ltac non-terminal, top-level function applications are treated as applications in Ltac, not Gallina; but the arguments to such functions are parsed withconstr by default. This choice may seem strange, until we realize that we have been relying on it all along in all the proof scripts we write! For instance, the apply tactic is an Ltac function, and it is natural to interpret its argument as a term of Gallina, not Ltac. We use an ltac prefix to parse Ltac function arguments as Ltac terms themselves, as in the call to map above. For some simple cases, Ltac terms may be passed without an extra prefix. For instance, an identifier that has an Ltac meaning but no Gallina meaning will be interpreted in Ltac automatically.

== END ==

  Is the following interpretation correct?

  > At a high level, there's "ltac" functions (defined with Ltac) and "gallina" functions (defined with Fixpoint, Definition, Function) -- "constr:" basically says "execute this next block of code with gallina functions?"

Thanks!



On Mon, Jun 17, 2013 at 8:56 AM, Vincent Demange <vincent.demange AT ensiie.fr> wrote:
>
> Hi MathProver,
>
> Here I come with another solution (source file joined):
>
> the idea is to prove
> (P_0 -> ... -> P_n -> B_0 /\ ... B_m) ->
>    /\_i (P_0 -> ... -> P_n -> B_i)
>
> then by applying it to an hypothesis of the form
> (P_0 -> ... -> P_n -> B_0 /\ ... /\ B_m)
>
> we can generate all the hypotheses you want
> (P_0 -> ... -> P_n -> B_i)
>
>
> Since P_0 -> ... -> P_n -> B_0 is expressed by induction on the list
> [P_0; ...; P_n], and And also, we need to use tactics to build those
> lists.
>
>
> The resulting proof term is small and beautiful !
>
>
> Cheers,
> Vincent.
>
> Le lundi 17 juin 2013 à 02:16 -0700, Math Prover a écrit :
> > Hi,
> >
> >
> >   I want to destruct a "scoped and". See attached tac.v
> >
> >
> >   My existing implementation is somewhat ugly -- for each length, I
> > need to create (a) two lemmas and (b) an extra line in the tactic.
> >
> >
> >   I was wondering if there was a simpler way to do this in "one shot"
>