The Coq mailing list

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

Dear Jonathan, Daniel,

> I don't think there is a way tactically to decide if a definition is an 
> instance

I thought about it once more: one issue with eauto is that it will also use 
local hypothesis. So these must be cleared before the test and this must be 
undone after the test. Below is a tactic which does this with a few test 
cases.

Best regards,

Michael


Inductive t := Inst | Hyp | Def.

Class C := { c : t }.

Instance i   : C := { c:= Inst }.
Definition d : C := Build_C Def.
Definition h : C := Build_C Hyp.

(* Basic is instance tactic *)

Ltac is_instance_basic term :=
  let Hex := fresh "InstExists" in 
  let Heq := fresh "InstEqual" in 
  let T := type of term in
  pose ( ltac:(eauto 1 with nocore typeclass_instances) : T ) as Hex;
  assert( Hex = term ) as Heq by reflexivity;
  clear Heq;
  clear Hex.

(* Remove all hypotheis of the type in question and wrap this in a double 
inversion to undo the removal *)

Ltac is_instance term :=
  tryif (
    let T := type of term in
    repeat match goal with H : T |- _ => clear H end;
    tryif is_instance_basic term then fail else idtac
  ) then fail else idtac.


Goal True.

(* is_instance_basic and is_instance work fine without hypotheis of type C *)
is_instance_basic i.
Fail (is_instance_basic d).
Fail (is_instance_basic h).

is_instance i.
Fail (is_instance d).
Fail (is_instance h).

(* With hypothesis of type C, only is_instance works *)
pose( Build_C Hyp ) as Chyp.

Fail (is_instance_basic i).
Fail (is_instance_basic d).
is_instance_basic h.

is_instance i.
Fail (is_instance d).
Fail (is_instance h).

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