coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] typeclass resolution and unfold

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] typeclass resolution and unfold
Date: Thu, 6 Jul 2017 17:37:54 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr0-f182.google.com
Ironport-phdr: 9a23:/HUQyxCzEuAITn8DMKqEUyQJP3N1i/DPJgcQr6AfoPdwSPvzpMbcNUDSrc9gkEXOFd2CrakV1KyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fdbghMhjexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Qiqp4bt1RxD0iScHLz85/3/Risxsl6JQvRatqwViz4LIfI2ZMfxzdb7fc9wHX2pMRsReVyJBDI2ybIUBEvQPMvpDoobnu1cDtwGzCRWwCO7tzDJDm3/43bc90+QkCQzIxg0gEMwUsHTOstr+KbkfUeeozKnS0TXDbu1Z2Srg44XPahAhoO+DXahqccXP00UgCwTFjkiKqYz5PjOayPkNvnOU7+plT+2vimonpxttrTiow8chk4/EjZ8WxFDc7Sh13po5KNmiREN4YdOoCoZcuz+ZOodsX88vQH9ktSAnwbMco5G7ZjIFyJE/yh7fdfOHd4+I7wrmVOmLIDd4gGtpebylhxqu6ESgxPDwW8qq3FpQoSpFld7Mtn8J1xPN8MSIVvx9/kK51TaO0QDc9P1ELFgqmabHL5Mt2L09m5oJvUjeACP7m1/6gLKVe0k64uSo7v7oYrTipp+SLY90jQT+P7w2msy+H+s4KBIOUHaB9eug073j4Ff5QKlLjvIoj6nUq5/aJcEBqa64Bw9ZyJos6xG6Dzu+ytQXgWEHLE5ZeBKAl4XmJ1bOIOnhAfijh1SsjSxkyuvdPrzhB5XNNmLMnK3gfbZ78U5cyRA8wcpR55JOWfk9J6fYXVa5n9jFBFdtOAuthu3jFd9V14UEWGvJDLXPY43Itlrd3uMiOfOBLKQSpSzhKvU4r6r2jHIjg1Jbdq60x4cWZW2QEfFvIkHfan3p1IRSWVwWtxYzGbS5wGaJViReMjPrB/ox

Hi Julien,

I usually use tactic notation to deal with names like this:

Tactic Notation "myunfold" reference(x) := (unfold x).

Best regards,

Pierre

2017-07-06 17:12 GMT+02:00 Julien Narboux <jnarboux AT narboux.fr>:

Hello,

I have defined a type class, and definitions depending on fields of the type class.
I would like to write a tactic which unfold the definition given as an argument.

How can I do that ?

Here is a small test case:

Class foo:= {
A : Type;
B: A -> A -> Prop;
babar a b := B a b /\ B b a;
}.

Ltac myunfold t := unfold t.

Section bar.

Context `{Ax:foo}.

Lemma titi : forall a b, babar a b.
Proof.
intros.
(* unfold babar. works *)
myunfold babar.
(* In nested Ltac calls to "myunfold" and "unfold t", last call failed.
Error: Ltac variable t is bound to babar which cannot be coerced to
an evaluable reference. *)

Julien

[Coq-Club] typeclass resolution and unfold, Julien Narboux, 07/06/2017
- Re: [Coq-Club] typeclass resolution and unfold, Pierre Courtieu, 07/06/2017