The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Gregory,

  Maybe bottomup does too much, why do you think topdown should be needed?

In a situation where you end up with exists n, P n /\ (exists n', Q n') it goes into the

subterms again. On a term t, bottomup tac repeatedly applies bottomup tac if tac 

rewrote t to t'. 

Cheers,

-- Matthieu

On Thu, Jan 7, 2016 at 10:09 PM Gregory Malecha <gmalecha AT gmail.com> wrote:

I figured out the problem. I was missing an [eval cbv beta] to reduce the term. This works:

rewrite_strat (bottomup (hints pulling ; eval cbv beta)).

I'm a little surprised that I don't need to do another pass.

On Thu, Jan 7, 2016 at 12:50 PM, Gregory Malecha <gmalecha AT gmail.com> wrote:

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

--

gregory malecha