The Coq mailing list

[Math Prover <mathprover AT gmail.com>]

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!