coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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 thesubterms again. On a term t, bottomup tac repeatedly applies bottomup tac if tacrewrote t to t'.Cheers,-- MatthieuOn 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
- [Coq-Club] rewrite_strat Question, Gregory Malecha, 01/07/2016
- Re: [Coq-Club] rewrite_strat Question, Gregory Malecha, 01/07/2016
- Re: [Coq-Club] rewrite_strat Question, Matthieu Sozeau, 01/07/2016
- Re: [Coq-Club] rewrite_strat Question, Gregory Malecha, 01/08/2016
- Re: [Coq-Club] rewrite_strat Question, Matthieu Sozeau, 01/07/2016
- Re: [Coq-Club] rewrite_strat Question, Gregory Malecha, 01/07/2016
Archive powered by MHonArc 2.6.18.