The Coq mailing list

[Damien Pous <Damien.Pous AT ens-lyon.fr>]

Hi,

Did some of you encountered the following situation, and did you find
a satisfactory solution ?

1. We prove a rather involved theorem, by heavily relying on
FSets/FMaps (we need sets of lists of nats, sets/maps of positive, and
sets/maps of sets of positive). However, the theorem is not about
finite sets at all. At the end, we get a module M, that contains the
theorem.

2. Since we want to use this theorem, we "Require M".

3. Now all proofs involving typeclasses become *very* slow : the hint
databases now contain all lemmas about the various finite sets and
finite maps we used to prove our theorem... (notably the
typeclass_instance database grows from 110 lines to 1500 lines, and
simple setoid_rewrites are ten times slower than before).

We will never use these hints/instances: they are specific to M's
implementation.
We managed to hide the hints we added by ourselves using the section
mechanism, but we cannot hide FSets/FMaps hints.

Maybe hints should not survive to the end of modules by default, and
be activated only when the modules are exported ?

Below is some concrete code, to be tested with the current version of
our ATBR library
(ad: http://sardes.inrialpes.fr/~braibant/atbr/atbr-1.1.tar.gz)

Damien and Thomas




Require Import Classes.

(* the following modules define various tactics which we would like to
   use in the sequel (although we don't in this example).

   if we do not import these modules, that's fine, otherwise the hint
   databases contains way too much lemmas, so that we get a big
   overhead when using these libraries (notably with typeclasses)
*)

Require SemiLattice.         (* uses fsets of nats *)
Require Monoid.              (* imports SemiLattice *)
Require SemiRing.            (* imports SemiLattice, uses fsets of
lists of nats *)
Require KleeneAlgebra.       (* imports SemiRing *)
Require DecideKleeneAlgebra. (* imports KleeneAlgebra, uses
fsets/fmaps of positives and fsets/fmaps of fsets of positives *)

Print HintDb core.                (* 50  -> 1600 lines (less than 100
useful ones) *)
Print HintDb typeclass_instances. (* 110 -> 1500 lines (less than 200
useful ones) *)

Section a.
  Context `{KA: KleeneAlgebra}.
  Goal forall A (x y z: X A A), x==y -> z*x+z == z*y+z.
    intros.
    Time rewrite H. (* 0.1 s -> 0.9 s : 9 times slower, on this very
simple example *)
    reflexivity.
  Qed.
End a.