Correctly gathering the list of proved equational results?

Stream: Equational

[Anand Rao Tadipatri]

I'm automatically generating some proofs of non-implications and I'd like to first filter out results that have already been established.

What I'm doing so far is along the lines of

import equational_theories.Closure

open Lean

def extractResults : CoreM Unit := do
  searchPathRef.set compile_time_search_path%
  let env ← importModules #[
    { module := `equational_theories },
    { module := `equational_theories.Equations.All }] .empty
  withEnv env do
    let eqnThms ← Result.extractEquationalResults
      let closure ← Closure.closure <| eqnThms.map Entry.variant
      let nonImplications := closure.filterMap fun
        | .implication _ => none
        | .nonimplication e => some e

However, my outputs contain far more results than I'd expect, which makes me think that the filtering is not happening correctly (though it definitely seems to be happening to some extent). Am I extracting the results correctly, or is there some other function that I should be calling? Does the environment that I've chosen to run the computation in contain all the results proved in the project so far? Any help would be appreciated.

[Anand Rao Tadipatri]

Actually, I now have reason to believe that I'm gathering these results correctly after all, and that the high count is coming from considering equations that aren't a part of the initial set of 4694 equations.

[Vlad Tsyrklevich]

There are not many implications for the sporadic equations in the closure last time I checked. My local results are:

$ egrep -v "(5105|28381|374794)" ../equational_theories/main_implications.closure.csv | wc -l
 8173585

[Vlad Tsyrklevich]

Does that match what you see? Without filtering sporadic equations I see 8178144.

[Andrés Goens]

how does this relate to extract_implications.lean?

[Vlad Tsyrklevich]

Actually I guess my closure data is slightly dated, 28381 was deleted from main on Thursday. Anyways extract_implications --closure (with or without --only-implications) should tell you the ground truth.

[Amir Livne Bar-on]

I find the output of the outcomes sub-command useful, it's a large table that says whether an implication is known, whether it appears explicitly or through inference, and whether a conjecture is needed to know it