coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Ltac extend

From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Ltac extend
Date: Thu, 22 Sep 2016 10:27:35 +0200
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:YswfKBLFBIgdUtQ4a9mcpTZWNBhigK39O0sv0rFitYgULvnxwZ3uMQTl6Ol3ixeRBMOAuqgC07ad6/qocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+kQMiK04/vjaibwN76W01wnj2zYLd/fl2djD76kY0ou7ZkMbs70RDTo3FFKKx8zGJsIk+PzV6nvp/jtM0rzyMFsPU4ssVETK/SfqIiTLUeAi51HXoy4ZjRshPJQBGTrlgGX28cnwBTS1zA5RD+X5H+tirhqvFVwi6QN8DsUbMuVD6o4r1wDhns3nRUfwUl+X3a35QjxJlQpwis8kRy

On 09/22/2016 10:15 AM, Frédéric Besson wrote:

Otherwise:

Class is_var_bool {T} (x : T) := decide_is_var : bool.
Hint Extern 0 (is_var_bool ?x) => first [ is_var x; exact true | exact false
] : typeclass_instances.
Ltac is_var_bool x := constr:(_ : is_var_bool x).

This is what I would call Ltac kung-fu.
A dark art which I sincerely admire but do not intend to practice.

Jason's trick can be simplified as follows:

Ltac is_var_bool x :=
constr:(ltac:(first [is_var x; exact true|exact false])).

I sometimes use this constr:(ltac:t) trick to define tactics that return a term while being implemented using possibly side-effecting tactics.

IMHO my solution isn't very pretty either...

[Coq-Club] Ltac extend, Frédéric Besson, 09/20/2016
- Re: [Coq-Club] Ltac extend, Pierre-Marie Pédrot, 09/20/2016
  - Re: [Coq-Club] Ltac extend, Frédéric Besson, 09/21/2016
    - Re: [Coq-Club] Ltac extend, Jason Gross, 09/21/2016
      - Re: [Coq-Club] Ltac extend, Frédéric Besson, 09/22/2016
        
        Re: [Coq-Club] Ltac extend, Robbert Krebbers, 09/22/2016
        
        Re: [Coq-Club] Ltac extend, Frédéric Besson, 09/22/2016
        
        Re: [Coq-Club] Ltac extend, Laurent Thery, 09/22/2016
        Re: [Coq-Club] Ltac extend, Jason Gross, 09/22/2016
        
        Re: [Coq-Club] Ltac extend, Jonathan Leivent, 09/22/2016