The Coq mailing list

[Math Prover <mathprover AT gmail.com>]

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!