generate_most_wanted_list.py

#!/usr/bin/env python3

"""
Example usage:

```sh
$ python scripts/generate_most_wanted_list.py equational_theories/Subgraph.lean
$ less most_wanted.md
```
"""

from process_implications import *
from itertools import product
from datetime import datetime


def close(known_implies):
    # copilot wrote this
    new_pairs = closure = set(known_implies)
    while new_pairs:
        new_pairs = {
            (a, d) for a, b in new_pairs for c, d in known_implies if b == c
        } - closure
        closure |= new_pairs
    return closure


if __name__ == "__main__":
    try:
        file_name = argv[1]
        assert os.path.exists(file_name)
    except:
        print("Usage: python generate_most_wanted_list.py <file_name.lean>")
        exit(1)

    universe, known_implies, known_not_implies = parse_proofs_file(file_name)
    known_implies = close(known_implies)

    ascendants = defaultdict(int)  # equation -> equations it's implied by
    descendants = defaultdict(int)  # equation -> equations it implies
    for a, b in known_implies:
        if a != b:
            descendants[a] += 1
            ascendants[b] += 1

    edge_value = {}  # (a, b) -> value of the a->b implication
    for a, b in product(universe, universe):
        if (a, b) in known_implies or (a, b) in known_not_implies:
            continue

        # This doesn't work with cycles
        v = ascendants[a] + descendants[b]
        # speed things up by not recording explicitly zero-value edges
        if v > 0:
            edge_value[(a, b)] = v

    with open("most_wanted.md", "w+") as fh:
        fh.write(
            f"# Most Wanted list of implications as of ({datetime.now().strftime('%Y-%m-%d %H:%M:%S')})"
            + "\n\n"
        )
        for a, b in sorted(edge_value, key=lambda ab: edge_value[ab], reverse=True):
            fh.write(
                f"* `{a}` -> `{b}` (implied by {ascendants[a]} -> implies {descendants[b]} = {edge_value[(a,b)]})"
                + "\n"
            )