coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] is_class and is_instance in 8.6

From: Jonathan Leivent <jonikelee AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] is_class and is_instance in 8.6
Date: Sat, 19 Nov 2016 15:52:01 -0500
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-qt0-f180.google.com
Ironport-phdr: 9a23:owij2hBZX7jN5dlsu61mUyQJP3N1i/DPJgcQr6AfoPdwSP77r8bcNUDSrc9gkEXOFd2CrakV0KyM6+u5BTVIoc7Y9itdINoUD15NoP5VtjJjKfbNMVf8Iv/uYn5yN+V5f3ghwUuGN1NIEt31fVzYry76xzcTHhLiKVg9fbytScb6xv663OGq+pDVfx4AxH/kOeszf12KqlD6sdBeqo9/IO5lwRzQ53BMZu5+xGVyJFvVkQyqtemq+5s20SNWsu4h/sgIdaj7Yak+UfQMDjMgMmM44MDmnRbGRAqLoHAbVzNFwVJzHwHZ4USiDd/KuSzgu784gXHCMA==

I thought that it wasn't possible to write an is_class or is_instance predicate in Ltac. But, here they are in 8.6 - and probably do-able in 8.5 as well (uscore would need to be rewritten)...

Definition Any := forall A, A.

Hint Extern 0 =>
lazymatch goal with H : Any |- _ => apply H end : typeclass_instances.

Ltac uscore term :=
match goal with
| _ => uscore open_constr:(term _) (*fails if there are too many _'s*)
| _ => fun tac => tac term
end.

Ltac is_class H :=
let x := constr:(_:Any -> H) in idtac.

Ltac uis_class C :=
try (tryif uscore C is_class
then fail 0
else fail 1).

Ltac is_instance X :=
let tX := type of X in
uis_class tX.

(****)
Class Foo := {}.

Class Bar (A:Type) := bar : A.

Instance Bar1 (n:nat) : Bar nat := n.

Goal True.
Fail is_class True.
is_class Foo.
is_class (Bar True).
Fail is_class Bar.
uis_class Bar.
Fail is_class nat.
is_instance Bar1.
Fail is_instance I.
exact I.
Qed.

-- Jonathan

[Coq-Club] is_class and is_instance in 8.6, Jonathan Leivent, 11/19/2016