The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

Hello --

I'm trying to benchmark rewrite_strat and I'm having trouble constructing a strategy that lifts all existential quantifiers over conjunctions. Here are the two lemmas that I'm using:

Theorem pull_ex_and_left

: forall T P Q, Basics.flip Basics.impl ((@ex T P) /\ Q) (exists n, P n /\ Q).

Admitted.

Theorem pull_ex_and_right

: forall T P Q, Basics.flip Basics.impl (Q /\ (@ex T P)) (exists n, Q /\ P n).

Admitted.

Hint Rewrite pull_ex_and_left : pulling.

Hint Rewrite pull_ex_and_right : pulling.

Here is a simple goal that I've been using for testing:

Goal ((((exists _ : nat, 0 = 0) /\ (exists _ : nat, 0 = 0)) /\

     (exists _ : nat, 0 = 0) /\ (exists _ : nat, 0 = 0)) /\

    ((exists _ : nat, 0 = 0) /\ (exists _ : nat, 0 = 0)) /\

    (exists _ : nat, 0 = 0) /\ (exists _ : nat, 0 = 0)) /\

   (((exists _ : nat, 0 = 0) /\ (exists _ : nat, 0 = 0)) /\ 0 = 0 /\ 0 = 0) /\

   (0 = 0 /\ 0 = 0) /\ 0 = 0 /\ 0 = 0.

My idea for the procedure was lift existentials bottom up. When you hit a conjunction, pull all the exisentials out of each side. This seems to require top-down rewriting so I tried:

rewrite_strat (bottomup (repeat (topdown (hints pulling)))).

but this is not able to pull all of the quantifiers in one invocation. Is there something that I am missing about how rewrite_strat works? Or am I just making a foolish mistake.

Thanks so much.

--

gregory malecha