The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Indeed, reification is the way you want to go if you want to manipulate ASTs, and your match problem was a problem of "binders"; there is no valid match for "?a" and "?b" in the example you gave, without referencing variables that are available to the goal; the terms in the "and" reference variables that are bound inside of the current scope, rather than outside of it, and so you don't have access to these variables.  This is why the example tactic I gave in a recent email matched on [and], rather than on [and ?a ?b].

If you want a quick-and-dirty way of manipulating ASTs, note that constructions using [context] are not type-checked until the term is used, so you can blow apart and reconstruct ASTs of Coq with clever use of [context] and [appcontext], without having to reify.  But if you want structured manipulation, reification is the way to go.

-Jason

On Tue, Jun 18, 2013 at 11:55 AM, Math Prover <mathprover AT gmail.com> wrote:

Resolved -- http://adam.chlipala.net/cpdt/html/Reflection.html#lab98 indeed is what I want.

On Tue, Jun 18, 2013 at 6:57 AM, Math Prover <mathprover AT gmail.com> wrote:

As a followup on this, are the formal terms I'm dealing with called:

  "reification" (changing Prop into a Coq List format) and

  "binders" (the forall problem I'm running into)

Furthermore, is understanding pages 314-317 of http://adam.chlipala.net/cpdt/cpdt.pdf the key to my problem?

Thanks!

On Tue, Jun 18, 2013 at 2:50 AM, Math Prover <mathprover AT gmail.com> wrote:

I have been thinking more about this question. And I think the problem is as follows:

  * in the intermediate stages of the my computation, the "Props" I'm passing around are NOT semantcailly valid props.

  * thus, what I want is a way to allow me to manipulate the AST of the Prop -- where it's okay for the intermedaite values to be invalid -- as long as my final output is a valid Prop

In particular, I'd love to somehow get this "Prop" as a nested list of symbols -- do some manipulation -- then convert it back to a Prop. I think this is the primitive / common theme I'm missing.

On Tue, Jun 18, 2013 at 1:26 AM, Math Prover <mathprover AT gmail.com> wrote:

Hi,

  This question si uncannily similar to my previous question. If I'm misunderstanding the same concept (and this is a repeat question), please call me out on it. However, I suspect something else is going on here:

## Goal:

  I want a tactic to transform hypothesis of the form:

  H: forall a b c d e, P1 /\ P2

  // P1 and P2 can depend on a, b, c, d, e

  into a hypothesis of the form:

  H1: forall a b c d e, P1

  H2: forall a b c d e, P2

## First step, "promoting the and"

== BEGIN ==

Ltac promote_and_hlpr P :=

    idtac "pah input   ==>" P;

  match P with

  | (forall x:?T, ?P') =>

    idtac "pah capture ==>" P'; promote_and_hlpr P'

  | _ => idtac "no match"

end.

Ltac promote_and :=

  match goal with

  | H: (forall x:?T, ?P) |- _ =>

      promote_and_hlpr (forall x:T, P)

  end.

Ltac promote_and2 :=

  match goal with

  | H: context [?a /\ ?b] |- _ =>

      idtac "matched"

  end.

Lemma lem1:

  (forall (x y: nat), (x = 1 \/ x <> 1) /\ (y = 0 \/ y <> 0))

    -> False.

intros.

  promote_and.

  promote_and2.

== END ==

## Problems I run into / Questions

Q1: promote_and2 fails to match. Is this because the "/\" is embedded within quantified variables, and this context can not match?

Q2: promote_and_hlpr only matches the outer, but fails to match the inner. In particular, the idtac output I get is:

== Begin ==

pah input   ==> (forall x y : nat, (x = 1 \/ x <> 1) /\ (y = 0 \/ y <> 0))

pah capture ==> (forall y : nat, (x = 1 \/ x <> 1) /\ (y = 0 \/ y <> 0))

pah input   ==> (forall y : nat, (x = 1 \/ x <> 1) /\ (y = 0 \/ y <> 0))

no match

== End ==

  Why is it failing to match on the second call?

Thanks!