The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Beta, Jason,

 

wouldn’t this also solve the question from Jason on stopping type class search when a certain pattern is hit? Couldn’t one insert an extern hint into the type class database which cuts and fails when it finds a certain pattern? As far as I know cuts work in typeclass eauto.

 

Best regards,

 

Michael

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of Beta Ziliani
Sent: Wednesday, June 1, 2016 12:38 PM
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Getting tactics in terms to fire later?

 

What we do in Mtac is to use the typeclass mechanism to do the trick:

Class runner A  (f : Mtac A) := { eval : A }.

Arguments runner {A} _.

Arguments Build_runner {A} _ _.

Arguments eval {A} _ {_}.

Hint Extern 20 (runner ?f) => (exact (Build_runner f ltac:(rrun f)))  : typeclass_instances.

Hope it helps.
Beta

```

​

 

On Wed, Jun 1, 2016 at 5:15 AM, Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

Dear Gregory,

 

it is not an elegant solution, and maybe not a solution at all for your real case, but what I do in such situations is this:

 

Definition foon (ls : nat) : nat := 0.

Definition foob (ls : bool) : nat := 0.

Definition foonl (ls : list nat) : nat := 0.

Definition foobl (ls : list bool) : nat := 0.

 

Open Scope list_scope.

 

Ltac try_something :=

 lazymatch goal with

  | |- nat => exact 0

  | |- bool => exact true

  | |- list ?t => let value := fresh "value" in assert(t) as value by try_something; exact (value :: nil)

  end.

 

Notation "'it'" := ltac:(try_something) (at level 0).

 

Definition barn : nat := foon ( it ).

Definition barb : nat := foob ( it ).

Definition barnl : nat := foonl ( it ).

Definition barbl : nat := foobl ( it ).

 

This way at least the number of terms you need to specify is not the product of the number of base types and the number of parameterized types, but their sum.

 

Best regards,

 

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

 

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928