Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] finer control over typeclass instance refinement

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] finer control over typeclass instance refinement


Chronological Thread 
  • From: Jason Gross <jasongross9 AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] finer control over typeclass instance refinement
  • Date: Tue, 27 Sep 2016 23:56:49 +0000
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f169.google.com
  • Ironport-phdr: 9a23:yfKHZBQy0xqLcIf40QAyucJghNpsv+yvbD5Q0YIujvd0So/mwa64ZBCN2/xhgRfzUJnB7Loc0qyN4vqmADJLuMnJ8ChbNscTB1ld0YRetjdjKfDGIHWzFOTtYS0+EZYKf35e1Fb/D3JoHt3jbUbZuHy44G1aMBz+MQ1oOra9QdaK3Iyfntq/8JzLYghOmCH1IfYrdE33/k3tsZw9hpIqAaIswFOdqXxRPu9S2GlAJFSJnh+66N3mr7B59CEFmfs68MgIfr/9ZL9wGb5RFzMgPHoy/9a6nRbGRAqLoHAbVzNFwVJzHwHZ4USiDd/KuSzgu784gXHCMA==

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

Tactic Notation "oexact" uconstr(term) := lazymatch goal with |- ?G => oexact' (term : G) end.

Otherwise, the following fails:
Goal 0 = 1 -> False.
  oexact (fun H => match H with eq_refl => fun p => p end).

(Note that [exact] and [refine] do bidirectional typechecking.)

On Tue, Sep 27, 2016 at 7:45 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:
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





Archive powered by MHonArc 2.6.18.

Top of Page