add custom_typeclass_db

README.md

@@ -2,6 +2,6 @@
 
 This repository contain a collection of interesting tricks and facts about Coq that were useful during the development of Iris.
 
-- [slow_qed.v](theories/slow_qed.v) Causes for slow Qed times
-- TODO: How to use custom typeclass databases
+- [slow_qed.v](theories/slow_qed.v): Causes for slow Qed times
+- [custom_typeclass_db.v](theories/custom_typeclass_db.v): How to use custom typeclass databases
 - TODO: How to iterate over all solutions for typeclass search

_CoqProject

@@ -7,4 +7,5 @@
 
 -Q theories tricks
 
-theories/slow_qed.v
\ No newline at end of file
+theories/slow_qed.v
+theories/custom_typeclass_db.v
\ No newline at end of file

theories/custom_typeclass_db.v

+(** This file shows how to setup a custom hint database for tactics. *)
+From Coq Require Export Utf8 EqdepFacts PArith NArith ZArith NPeano.
+
+(** Let's say we want to create a tactic to convert nat terms to Z
+terms using typeclasses. First, we do this naively using the standard
+hint database for typeclasses, then we will discover some problems
+with this approach and finally solve these problems by using a custom
+hint database.
+
+For this we first create a class [NatToZ n z] that converts the nat
+[n] to the Z [z]: *)
+Class NatToZ (n : nat) (z : Z) := {
+    nat_to_Z_proof : Z.of_nat n = z
+}.
+(** We will use [NatToZ] with a concrete number for the first argument
+and an evar for [z], so we setup the Hint Mode accordingly. *)
+Global Hint Mode NatToZ + - : typeclass_instances.
+
+(** Let us prove some cases: *)
+Lemma nat_to_z_add n1 n2 z1 z2 :
+  NatToZ n1 z1 → NatToZ n2 z2 → NatToZ (n1 + n2) (z1 + z2).
+Proof. intros [<-] [<-]. constructor. apply Nat2Z.inj_add. Qed.
+Lemma nat_to_z_S n1 z1:
+  NatToZ n1 z1 → NatToZ (S n1) (Z.succ z1).
+Proof. intros [<-]. constructor. apply Nat2Z.inj_succ. Qed.
+Lemma nat_to_z_O : NatToZ 0 0.
+Proof. constructor. reflexivity. Qed.
+(** Also a fallback: *)
+Lemma nat_to_z_fallback n :
+  NatToZ n (Z.of_nat n).
+Proof. constructor. reflexivity. Qed.
+
+(** Now we just need to add the rules to the typeclass_instances database: *)
+Global Hint Resolve nat_to_z_add | 10 : typeclass_instances.
+Global Hint Resolve nat_to_z_S | 10 : typeclass_instances.
+Global Hint Resolve nat_to_z_O | 10 : typeclass_instances.
+(** The fallback should be tried last so we give it a high number. *)
+Global Hint Resolve nat_to_z_fallback | 1000 : typeclass_instances.
+
+(** Let's try our typeclass: *)
+Goal ∀ n : nat, ∃ z, NatToZ (n + S n) z ∧ z = (Z.of_nat n + Z.succ (Z.of_nat n))%Z.
+  intros n. eexists _. split; [apply _|]. reflexivity.
+Abort.
+
+(** Constants result in many Z.succ, but we don't care about that for the moment. *)
+Goal ∃ z, NatToZ 5 z ∧ z = Z.succ (Z.succ (Z.succ (Z.succ (Z.succ 0)))).
+  eexists _. split; [apply _|]. reflexivity.
+Abort.
+
+(** But there is a problem: *)
+Goal ∀ n : nat, ∃ z, NatToZ (S n + S n) z ∧ z = (Z.succ (Z.of_nat n) + Z.succ (Z.of_nat n))%Z.
+  intros n. eexists _. split; [apply _|].
+  Fail reflexivity.
+  (** Our typeclass resulted in [Z.succ (Z.of_nat n + Z.succ (Z.of_nat
+  n))] which corresponds to [S (n + S n)]. This happened because
+  typeclass search unfolded (_ + _) before applying [nat_to_z_S]. *)
+Abort.
+
+(** One way to fix this is to make [_ + _] opaque for typeclass search  *)
+Global Hint Opaque plus : typeclass_instances.
+(** Or equivalently [Typeclasses Opaque plus.] *)
+Goal ∀ n : nat, ∃ z, NatToZ (S n + S n) z ∧ z = (Z.succ (Z.of_nat n) + Z.succ (Z.of_nat n))%Z.
+  intros n. eexists _. split; [apply _|]. reflexivity.
+Abort.
+(** This solves this problem but this opaqueness hint affects *all*
+typeclasses, not just NatToZ and thus maybe breaks completely
+unrelated proofs. Also explicitly making everying opaque can be quite
+tedious.  *)
+
+(** We solve this problem by using a custom hint database instead of
+typeclass_instances as this allows us to better control the opacity of
+constants: ([discriminated] selects the newer implementation hint
+databases) *)
+Create HintDb nat_to_z discriminated.
+
+(** Now we can declare that all constants should be treated as opaque
+by default in the new database. *)
+Global Hint Constants Opaque : nat_to_z.
+(** We can also declare that let-bindings should be treated as opaque. *)
+Global Hint Variables Opaque : nat_to_z.
+
+(** Now we just need to add our hints to the new database: *)
+Global Hint Mode NatToZ + - : nat_to_z.
+Global Hint Resolve nat_to_z_add | 10 : nat_to_z.
+Global Hint Resolve nat_to_z_S | 10 : nat_to_z.
+Global Hint Resolve nat_to_z_O | 10 : nat_to_z.
+Global Hint Resolve nat_to_z_fallback | 1000 : nat_to_z.
+
+(** And use [typeclasses eauto with nat_to_z] instead of [apply _] *)
+Goal ∀ n : nat, ∃ z, NatToZ (S n + S n) z ∧ z = (Z.succ (Z.of_nat n) + Z.succ (Z.of_nat n))%Z.
+  intros n. eexists _. split; [typeclasses eauto with nat_to_z|]. reflexivity.
+  (** The problem of unfolding [_ + _] is gone without an explicit Hint Opaque! *)
+Abort.
+
+Section test.
+(** We can add an explicit hint to make [_ + _] transparent make the
+problem reappear. We do this inside a section such that the hint gets
+removed after the section again. *)
+Local Hint Transparent plus : nat_to_z.
+Goal ∀ n : nat, ∃ z, NatToZ (S n + S n) z ∧ z = (Z.succ (Z.of_nat n) + Z.succ (Z.of_nat n))%Z.
+  intros n. eexists _. split; [typeclasses eauto with nat_to_z|]. Fail reflexivity.
+Abort.
+End test.
+
+
+(** There is another advantage when using a custom hint database with
+opaque constants: Typeclass search can use a faster procedure for
+finding the right hints since it does not need to use unification to
+decide whether a hint would apply. *)
+
+(** To demonstrate this, we first make plus transparent again: *)
+Global Hint Transparent plus : typeclass_instances.
+Goal ∀ n, ∃ z, NatToZ (n + n) z ∧ z = (Z.of_nat n + Z.of_nat n)%Z.
+  intros n. eexists _.
+  (** Now if we look at the debugging output of typeclass search, we
+   see that Coq tries to use unification to match the hints against
+   the goal. This can be seen based on the following lines:
+   [Cannot unify (NatToZ (?M1426 + ?M1427) (?M1428 + ?M1429)) and (NatToZ n ?z1)]
+   This means that performance of typeclass search scales linearly with the number
+   of registered rules as Coq needs to unify each rule with the goal. *)
+  Set Typeclasses Debug Verbosity 2.
+  split; [apply _|].
+  reflexivity.
+Abort.
+
+Goal ∀ n, ∃ z, NatToZ (n + n) z ∧ z = (Z.of_nat n + Z.of_nat n)%Z.
+  intros n. eexists _.
+  (** However, this problem does not occur with the custom hint
+  database as Coq can use an efficient discrimination tree to prune
+  unnecessary hints without using unification. *)
+  Set Typeclasses Debug Verbosity 2.
+  split; [typeclasses eauto with nat_to_z|].
+  reflexivity.
+Abort.