coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] finer control over typeclass instance refinement

From: Jonathan Leivent <jonikelee AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] finer control over typeclass instance refinement
Date: Tue, 27 Sep 2016 19:44:54 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f172.google.com
Ironport-phdr: 9a23:aLXSMhbvQ61Rk8870tiZnQT/LSx+4OfEezUN459isYplN5qZpcy9bnLW6fgltlLVR4KTs6sC0LuM9fm+EjVfqdbZ6TZZL8wKD0dEwewt3CUeQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2ap42N2uuz45zeZRlTzHr4OOsqbUb+kQKEnc4PyaBmN6x5nhDOuz5Df/lc7WJuP1Oa2RjmsJSe5plmpgZXvfs998dGGYH3fro1S6AQWDYhNWE26cnmuDHMSAKO4j0XVWBAwUkAOBTM8ByvBsS5iSD9rOconXDCZcA=

If you're using typeclasses, you may have run into cases where refinement runs when you'd rather it didn't. Here are a few very simple tactics that can help: orefine and simple orefine, which act like refine and simple refine, except that they don't run instance refinement in holes:

Tactic Notation "oexact" open_constr(term) := exact term.

Tactic Notation "orefine" uconstr(term) := unshelve oexact term; shelve_unifiable.

Tactic Notation "simple" "orefine" uconstr(term) := unshelve oexact term.

(*Example:*)
Variable Foo : Type.
Existing Class Foo.
Variable Foo1 : Foo.
Goal True.
refine (let f := _ : Foo in _). (*f := Foo1 : Foo*)
orefine (let g := _ : Foo in _). (*g := ?f : Foo*)

However, beware of bug 4416...

-- Jonathan

[Coq-Club] finer control over typeclass instance refinement, Jonathan Leivent, 09/28/2016
- Re: [Coq-Club] finer control over typeclass instance refinement, Jason Gross, 09/28/2016
  - Re: [Coq-Club] finer control over typeclass instance refinement, Jonathan Leivent, 09/28/2016