An evening experiment in finding lemmas

Why? Because normal Search won’t find it.

How to use: cocoricoogle --help, this README. You would probably need to do apt/pkg/… install rakudo.

~/H/cocoricoogle› ./cocoricoogle -in=ssrnat 'a + b - _ = b'
(* HI.                            *)
(* Loading.                       *)
(* Searching (ssrnat).            *)
(* 453 entries. 4077 to search.   *)

addKn
     : forall n : nat, cancel (addn n) (subn^~ n)
     : forall a b : nat, a + b - a = b


(* 1 found. THXBYE.               *)

V1 (master branch)

Get a list of definitions by doing Search _ in ⟨modules⟩. Try to match each using Check.

Speed: ≈10000/minute.

mode A

Query is forall a b…, … or … -> forall a b…, ….

./cocoricoogle -in=ssrnat  'forall x y z, x*_ = x*y + x*z'

mode B

Query doesn’t contain forall. Then --arity / -a comes into play. Default is 1-3. Free variables are assumed to be a, b, c, and so forth.

Cocoricoogle then will try all variants of arities and all permutations of variables, i. e.

(forall a b) (forall b a) (forall a b c) …

Gotchas (Check is too clever):

• WTF#1. Search for addnAC and get PeanoNat.Nat.add_shuffle0 for free.
• addnC matches forall a b, _ + b = _ + _ b.
• (1 * a)%coq_nat = a matches a + 0 = a.

V2

Match using Ltac. Does works and is measurably faster. Gothas:

• low boundary of arity cannot be arbitrary, because Ltac is defined once and match ty with forall a, a+b=_ => _ end is an error.
• different results of V1

V3

Get the definition list and do everything else in Ltac. Needs a way pass a large(ish) (at least 1000, but 50000 would be nice) list of definitions as an argument.

V4

Just fix Search.

TODO¹

• subterms/coercions
• ssr.ssrbool vs ssrbool
• a→b vs a==b vs reflect a b

¹) is because github doesn’t render it if it’s just a «TODO».