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 15:55:00 +0100
Authentication-results: mail2-smtp-roc.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:KG+o2hMSDC2OYpjr1r4l6mtUPXoX/o7sNwtQ0KIMzox0KPj+rarrMEGX3/hxlliBBdydsKIazbKO+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuStCU15z//tvx0qOQSj0AvCC6b7J2IUf+hiTqne5Sv7FfLL0swADCuHpCdrce72ppIVWOg0S0vZ/or9YwuxhX7vkm7otLVbjwV6U+V71RSjo8YE4v48i+jx7JRwaV+jM/SGgcmBdSGECR6Rj7Wpb3vS/7rfZm8DOdN8f7V6w3Qzmo5apxU1nujHFUZHYC7GjLh5ko3+pgqxW7qkknzg==

Pierre: I missed the two dots, thank for clarifying.

Guillaume: thanks! Your tactic notation looks useful to support the kinds of rewrites I wish to deal with, I will give it a try.

On 12/23/2015 11:39 AM, Guillaume Melquiond wrote:

On 23/12/2015 10:40, Pierre Courtieu wrote:

Hi,

I am not sure that Guillaume's suggestion has been understood
completely here. In the following (the ".." is real syntax here)

tac;[> tac' | tac''..].

This will apply tac' to the first subgoal and tac' to *all others* ASFAIU.

Right, and just to make it even clearer, here is an example:

Require Import ssreflect.
Tactic Notation "\" tactic(t1) "by" tactic(t2) := t1 ; [| t2 ; fail ..].
Goal forall x, (0 = 0 -> 1 = 1 -> x = 2) -> 3 = 4.
move => x H.
\rewrite -{2}H by trivial.

Best regards,

Guillaume

[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