coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Ssreflect rewrite term matching in vanilla Coq

From: Robbert Krebbers <mail AT robbertkrebbers.nl>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Ssreflect rewrite term matching in vanilla Coq
Date: Wed, 23 Dec 2015 00:18:24 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mail AT robbertkrebbers.nl; spf=None smtp.mailfrom=mail AT robbertkrebbers.nl; spf=None smtp.helo=postmaster AT smtp1.science.ru.nl
Ironport-phdr: 9a23:yOZ/wBcGvZ+Prr7tGl577k0AlGMj4u6mDksu8pMizoh2WeGdxc65Yx7h7PlgxGXEQZ/co6odzbGG7ea4ASQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTpkbjqs7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR5RZCi4nOiY7/p7Frx7GGDGI7HERSHlesQBFCQLI9gqyCpL4sy/SrO130iSAIc7sQLo+VC65qaFvHky7wBwbPiI0pTmEwvd7i7hW9Uqs

On 12/22/2015 07:33 PM, Enrico Tassi wrote:

rewrite foo by eauto using foo bar baz

In that case I would suggest something along the lines of what Guillaume
proposes:

rewrite foo; last by eauto using foo bar baz.

(It could be "first by ...", I don't recall now).

This is problematic when rewriting with foo gives rise multiple side-conditions. Does ssreflect have a construct similar to "first"/"last" that applies a tactic to all generated subgoals _apart from_ the first/last one?

[Coq-Club] Ssreflect rewrite term matching in vanilla Coq, Robbert Krebbers, 12/21/2015
- Re: [Coq-Club] Ssreflect rewrite term matching in vanilla Coq, Guillaume Melquiond, 12/21/2015
  - Re: [Coq-Club] Ssreflect rewrite term matching in vanilla Coq, Enrico Tassi, 12/21/2015
    - Re: [Coq-Club] Ssreflect rewrite term matching in vanilla Coq, Robbert Krebbers, 12/21/2015
      - Re: [Coq-Club] Ssreflect rewrite term matching in vanilla Coq, Enrico Tassi, 12/22/2015
        
        Re: [Coq-Club] Ssreflect rewrite term matching in vanilla Coq, Robbert Krebbers, 12/23/2015
        
        Re: [Coq-Club] Ssreflect rewrite term matching in vanilla Coq, Robbert Krebbers, 12/23/2015
        
        Re: [Coq-Club] Ssreflect rewrite term matching in vanilla Coq, Enrico Tassi, 12/23/2015
  - Re: [Coq-Club] Ssreflect rewrite term matching in vanilla Coq, Pierre Courtieu, 12/23/2015
    - Re: [Coq-Club] Ssreflect rewrite term matching in vanilla Coq, Guillaume Melquiond, 12/23/2015
      - Re: [Coq-Club] Ssreflect rewrite term matching in vanilla Coq, Robbert Krebbers, 12/23/2015