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 <mailinglists 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:19:53 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mailinglists AT robbertkrebbers.nl; spf=None smtp.mailfrom=mailinglists AT robbertkrebbers.nl; spf=None smtp.helo=postmaster AT smtp1.science.ru.nl
Ironport-phdr: 9a23:SkZ91xRK75E2dnAgXPZhOzKy4dpsv+yvbD5Q0YIujvd0So/mwa64YBGN2/xhgRfzUJnB7Loc0qyN4/6mATRIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/niabqo9X6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD86Fpy8kVWqLjOq88ULZwDTI8Mmlz6te4mwPESF614XEWX38K2jlSDgLP4QvhFsP0uyr+t+xy3CiBIdbeV7c+Uzm486RxRRXihT0ccTg9pjKEwvdshb5W9Ury7yd0xJTZNdmY

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 to 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