coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] very slow rewrite in *|- in 8.5beta3

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] very slow rewrite in *|- in 8.5beta3
Date: Fri, 13 Nov 2015 13:56:57 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ob0-f171.google.com
Ironport-phdr: 9a23:wo8J5BWkJ2F2E6xemAnn8qFGg7XV8LGtZVwlr6E/grcLSJyIuqrYZhCAt8tkgFKBZ4jH8fUM07OQ6PC9HzFaqs7Q+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8CVPl8D3Gv1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu2pN5g/GLdfFXEtN30/rJngsgCGRg+S7FMdVH8Xm1xGGV6Wwgv9W8LTuzD9sKJSwi6BJoWiT7kvXjKt9aBwU07AhyIONjp/+2bS3J8jxJlHqQ6s8kQsi7XfZ5uYYaJz

Is [abstract (rewrite in |- *; admit)] faster than than [rewrite in |- *; admit]?

There's a vernacular (or tactic) that compacts the evar map, right?

On Fri, Nov 13, 2015 at 1:50 PM, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

On 13/11/2015 17:43, Jonathan Leivent wrote:
> So, "rewrite in |-*" is carrying around some burden from prior subgoals
> in the same proof. Perhaps it is performing the search on the entire
> proof term up to that point (which is large if I don't do those admits
> or abstracts), instead of just on the particular subgoal's context?

I don't see where it could be doing so, but that's difficult to judge
without a test-case... The only thing that grows up during the proof is
the evar map, but it shouldn't affect tactics except marginally.

PMP

[Coq-Club] very slow rewrite in *|- in 8.5beta3, Jonathan Leivent, 11/13/2015
- Re: [Coq-Club] very slow rewrite in *|- in 8.5beta3, Pierre-Marie Pédrot, 11/13/2015
  - Re: [Coq-Club] very slow rewrite in *|- in 8.5beta3, Jonathan Leivent, 11/13/2015
    - Re: [Coq-Club] very slow rewrite in *|- in 8.5beta3, Jonathan Leivent, 11/13/2015
      - Re: [Coq-Club] very slow rewrite in *|- in 8.5beta3, Pierre-Marie Pédrot, 11/13/2015
        
        Re: [Coq-Club] very slow rewrite in *|- in 8.5beta3, Jason Gross, 11/13/2015
        
        Re: [Coq-Club] very slow rewrite in *|- in 8.5beta3, Clément Pit--Claudel, 11/13/2015
        
        Re: [Coq-Club] very slow rewrite in *|- in 8.5beta3, Jonathan Leivent, 11/13/2015
        
        Re: [Coq-Club] very slow rewrite in *|- in 8.5beta3, Jonathan Leivent, 11/16/2015
        
        Re: [Coq-Club] very slow rewrite in *|- in 8.5beta3, Pierre-Marie Pédrot, 11/16/2015