Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] rewrite_strat Question

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] rewrite_strat Question


Chronological Thread 
  • From: Gregory Malecha <gmalecha AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] rewrite_strat Question
  • Date: Thu, 7 Jan 2016 19:06:01 -0800
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gmalecha AT gmail.com; spf=Pass smtp.mailfrom=gmalecha AT gmail.com; spf=None smtp.helo=postmaster AT mail-yk0-f178.google.com
  • Ironport-phdr: 9a23:O9ry2xRWP+d6URn0WRIKfjIY8tpsv+yvbD5Q0YIujvd0So/mwa64YhCN2/xhgRfzUJnB7Loc0qyN4/6mATRIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/niabqo9X6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD89pozcNLUL37cqIkVvQYSW1+ayFmrPHs4DLEVEOk4mYWGjEdlQMNCAzY5jn7WI3wu230rLwu9jOdOJjZV707Xi6zp4JiTBLjiC5PYzE8+WXagcx5pK1eqROl4Rd4xtiHM8muKPNic/aFLpshTm1bU5MUDnQZDw==

Hi, Matthieu --

My thought was that [bottomup rw] would be: 1) recursively rewrite the sub-terms with [bottomup rw], 2) rewrite the term (only at the top) using [rw], return the result. In this case, a pull_ex_right would convert [P /\ exists x y, Q x y] into [exists x, P /\ exists y, Q y] but it would not apply a second time because the head symbol is not a conjunction. This is why I thought that I would need a [topdown] since [topdown rw] would perform this rewrite, and then rewrite in the subterms of the resulting term, one of which would be [P /\ exists y, Q y] which would rewrite into [exists y, P /\ Q y].

Does your definition mean that [repeat (bottomup x)] is the same as [bottomup x]?


On Thu, Jan 7, 2016 at 2:33 PM, Matthieu Sozeau <mattam AT mattam.org> wrote:
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

--
gregory malecha



Archive powered by MHonArc 2.6.18.

Top of Page