search

teorth / equational_theories

A project to map out the relations between different equational theories of Magmas.
Apache License 2.0
78 stars 20 forks source link

add extract_implications.lean #22

Closed dwrensha closed 4 hours ago

dwrensha commented 15 hours ago

This is a start on porting process_implications.py into Lean.

When I run this on the current repo via lake exe extract_implications, it outputs:

{"nonimplications":
 [{"rhs": "Equation387", "lhs": "Equation4512"},
  {"rhs": "Equation43", "lhs": "Equation42"},
  {"rhs": "Equation3", "lhs": "Equation4512"},
  {"rhs": "Equation4512", "lhs": "Equation42"},
  {"rhs": "Equation4582", "lhs": "Equation43"},
  {"rhs": "Equation4582", "lhs": "Equation42"},
  {"rhs": "Equation3", "lhs": "Equation42"},
  {"rhs": "Equation4512", "lhs": "Equation4513"},
  {"rhs": "Equation43", "lhs": "Equation387"},
  {"rhs": "Equation4513", "lhs": "Equation4522"},
  {"rhs": "Equation4", "lhs": "Equation43"},
  {"rhs": "Equation46", "lhs": "Equation4"},
  {"rhs": "Equation43", "lhs": "Equation3"},
  {"rhs": "Equation46", "lhs": "Equation3"},
  {"rhs": "Equation43", "lhs": "Equation4512"},
  {"rhs": "Equation387", "lhs": "Equation42"},
  {"rhs": "Equation42", "lhs": "Equation4512"},
  {"rhs": "Equation42", "lhs": "Equation43"},
  {"rhs": "Equation4", "lhs": "Equation4582"}],
 "implications":
 [{"rhs": "Equation46", "lhs": "Equation2"},
  {"rhs": "Equation4513", "lhs": "Equation4522"},
  {"rhs": "Equation7", "lhs": "Equation2"},
  {"rhs": "Equation387", "lhs": "Equation46"},
  {"rhs": "Equation4512", "lhs": "Equation4513"},
  {"rhs": "Equation4", "lhs": "Equation2"},
  {"rhs": "Equation6", "lhs": "Equation2"},
  {"rhs": "Equation2", "lhs": "Equation7"},
  {"rhs": "Equation4522", "lhs": "Equation4"},
  {"rhs": "Equation43", "lhs": "Equation387"},
  {"rhs": "Equation3", "lhs": "Equation4"},
  {"rhs": "Equation42", "lhs": "Equation4"},
  {"rhs": "Equation41", "lhs": "Equation7"},
  {"rhs": "Equation4582", "lhs": "Equation46"},
  {"rhs": "Equation42", "lhs": "Equation46"},
  {"rhs": "Equation2", "lhs": "Equation6"},
  {"rhs": "Equation4522", "lhs": "Equation4582"}]}
amirlb commented 15 hours ago

Will it be easy to detect Facts statements from https://github.com/teorth/equational_theories/pull/19 when it's merged, and generate non-implications from them? This will help us avoid writing O(n^2) non-implications as Lean theorems.

dwrensha commented 15 hours ago

It should be straightforward to expand this logic to accommodate whatever conventions we adopt.

dwrensha commented 13 hours ago

Currently, this iterates over all items in the equational_theories.Basic module. Once we have results living in multiple files, we'll need some other strategy.

As discussed on zulip, one way to do that would be to look in the environment for all items under a given namespace (EquationalTheories perhaps).

We could do that like this:

      for ⟨name, const_info⟩ in env.constants do
         if Name.isPrefixOf `EquationalTheories name then
           -- process `const_info`

You might worry that this is slow, because the environment is going to include stuff from mathlib, which is larger. However, when I tried it just now, it was tolerably fast (less than a second) with env.constants having 626k elements (from all of mathlib).