add equational_result attribute for tagging implications and negated implications

[dwrensha]

Adds an attribute @[equational_result] to be used for tagging theorems that represent proven implications or nonimplications in the graph.

Collects these results in an environment extension. The idea is that anyone who wants to analyze the data about what's been proven can grab the data from that extension. The data includes the filename where the result lives, and can include any other metadata we want to include.

Previously we had discussed getting the same information by scanning through the environment and collecting all theorems that have the correct shape. That approach would have the advantage of allowing the theorems to be more succinct in the source code (no need to add an attribute). However, I prefer the approach taken by this PR, because:

• If a theorem does not quite match the correct shape, the attribute handler can report the error immediately, at the theorem declaration.
• Recording the results (via an environment extension) just once avoids the need to linearly scan the whole environment (could get expensive) at each downstream usage point.

[Command-Master]

Shouldn't ParseImplications now be edited to use this instead of iterating over all theorems?

[Command-Master]

Also, there is duplication of Entry and EntryVariant in Conjecture and Result which should be extracted to a common definition

[dwrensha]

Shouldn't ParseImplications now be edited to use this instead of iterating over all theorems?

Yes, it should. There are some details to be worked out about how exactly to organize the shared logic.

[teorth]

Just a reminder to modify CONTRIBUTING.md to change the recommended syntax if this proposal gets implemented (it sounds reasonable to me so long as it doesn’t somehow break other Lean functionality concerning theorems)

[Command-Master]

Using result instead of theorem should also be updated in other files

[Command-Master]

Perhaps you can use the CLI from #102

[dwrensha]

could make sense in a later PR. For now, I want to focus on getting the core functionality here landed.

[dwrensha]

Shouldn't ParseImplications now be edited to use this instead of iterating over all theorems?

done.

[dwrensha]

Also, there is duplication of Entry and EntryVariant in Conjecture and Result which should be extracted to a common definition

The types do have differences and I don't see a benefit to trying to unify them.

It's possible that we may later decide to combine the conjecture and equational_result environment extensions. But for now I think this makes sense as-is.

[dwrensha]

Using result instead of theorem should also be updated in other files

In order to avoid making this PR unwieldy, I think it's best to defer updating the other files to later PRs.

[Command-Master]

Also, there is duplication of Entry and EntryVariant in Conjecture and Result which should be extracted to a common definition

The types do have differences and I don't see a benefit to trying to unify them.

It's possible that we may later decide to combine the conjecture and equational_result environment extensions. But for now I think this makes sense as-is.

What are the differences? To me they seem like the same thing, except one is missing a proof. The benefit of merging them is that later code, e.g. transitive closure, could use the same interface to process both of them

[nomeata]

These two are just instance of the general “∃ magma G such that equations {1,2,3} hold and {4,5,6} do not hold”. Note that that already entails 9 non-implicaitons. Once we add more exhaustive analysis of example magmas (as in #19), listing all non-implications here will not scale, and we’ll probably have to switch to the more compact representation.

Doesn't have to happen in this PR, of course; this is just a heads up.

[dwrensha]

I agree that we will want to add other ways to represent results. That can happen later as needed.

I don't see how "EquationN holds for all magmas" is an instance of "∃ magma G such that equations {1,2,3} hold and {4,5,6} do not hold".

[nomeata]

A, I misread the comment. My bad

[dwrensha]

Also, there is duplication of Entry and EntryVariant in Conjecture and Result which should be extracted to a common definition

The types do have differences and I don't see a benefit to trying to unify them.
It's possible that we may later decide to combine the conjecture and equational_result environment extensions. But for now I think this makes sense as-is.

What are the differences? To me they seem like the same thing, except one is missing a proof. The benefit of merging them is that later code, e.g. transitive closure, could use the same interface to process both of them

conjecture currently has an other variant because I wanted to support the ability to make conjectures whose types don't fit the enumerated shapes.

I could imagine that if we add new variants to support e.g. compactly representing many negated implications at once, that such things might only make sense as fully baked results, not as conjectures.

I could see it making sense to merge these into one environment extension or to keep them separate. Keeping them separate seems like the less invasive thing right now. We can adapt in the future. I think more important than nailing down this backend interface is putting the frontend in place, i.e. the conjecture command and the equational_result attribute, so that everyone else working on the project can start using them.