sreichelt / slate Goto Github PK

Regularly check all types, proofs, and dependencies of the entire library. Preferably, do not accept pushes to the main repository that break the library.

Integrate the web app into the VSCode extension as a webview.

• Ideally, the extension should use the compiled and minified web app as-is, so only one build is required. However, the web app must run in a slightly different mode.
• Synchronization of the selected file is important, in both directions.
• Content should also be updated in both directions. (However, the web app can only handle syntactically correct files.)

The HLM library should probably be in a separate repository so that it can be updated independently.

Some details still need to be worked out:

• If the library is checked out on its own, the "library" and "hlm" metamodels cannot be found. Shall we just declare that it must be checked out into the data/libraries directory, or is there a better solution?
• How does the web interface access the library? Directly from GitHub? Or via a dedicated server? Accessing it directly from GitHub does have the advantage that users can potentially work on their own fork, see #12.
• The development build of Slate should always use a local version of the library.

The Slate-specific React components need to be upgraded to the new lifecycle introduced in recent React versions, as described here: https://reactjs.org/docs/react-component.html#unsafe_componentwillreceiveprops

Users should be able to collect points of some sort for (accepted) additions to the library.
Some requirements:

• Users should be identified by their GitHub account.
• Determining users from the Git history would be possible except for two caveats:
  • Anonymous contributions should not increase the score of library maintainers that commit them.
  • Users can add proofs for existing theorems.
• So we should probably include "author" fields. The GUI should fill these automatically if the user is logged in. (What about the GUI running in VSCode?)
• An "early adopter bonus" would be nice, and we should reserve the option to shift priorities later while keeping existing scores. Does that mean we need to keep dates in addition to user names?
• Current statistics (i.e. hiscores) should be displayed on the front page. This should probably be a float that also contains a list of latest additions to the library.

There should be documentation about

• the architecture of Slate,
• the file format,
• how meta models are defined,
• and a lot more.

Some of this documentation should be in the form of code comments.

Extracted from #2: Run VSCode extension in isolation and dump information for regression testing.

After #28, automatically deduced arguments will frequently become very large unless they are automatically simplified. In the context of magmas and categories, we now have definitions that directly return a component of a decomposed object. These should be referenced in the construction so that they can be used instead of explicit decomposition.

This info is also required for #46. This suggests that we should attach the hints to constructions, not to constructors. It seems they are only relevant for constructions with single constructors anyway.

Hopefully, this will completely eliminate the need for %asElementOf.

Moreover, the same decomposition is required in order to apply equality definitions in the general case.

Currently, the user needs to use a character map tool in order to input non-latin or formatted characters. The web GUI should provide a graphical input method (with touch support) as well as a quick way to enter special characters via the keyboard (preferably using abbreviated LaTeX notation similarly to Lean in VSCode).

Somewhat related to #22.

Type checking is already implemented in the desktop version. In addition to a simple yes/no check, the type checker is responsible for auto-deduction of arguments.

Currently, propositions cannot be declared as parameters. The library includes definitions of properties and relations in set-theoretic terms, which adds some additional complexity.

A "proposition" parameter type could be used to define the sets of

• truth values,
• properties, and
• relations.

In the GUI, it could be hidden in parameter lists where it is not useful. (It is always useful in bound parameter lists, though.)

Pros:

• Makes some definitions simpler.
• Gives a somewhat more direct access to relations in proofs.
• Direct definitions of relations (not via predicates) can be rendered nicely.

Cons:

• The set-theoretic treatment may be more familiar.
• There does not seem to be any standard notation to define a relation "inline" except in set-theoretic terms.
• The closure of a relation with respect to a property is actually easier to define using a generalized intersection. (Or is it? What would the alternative look like?)

To solve the last point, there could be two alternative definitions of properties and relations, as is already the case with functions. But conversions between them are inconvenient. Then again, currently the set of properties is identical to the power set; this redundancy would be solved.

Implement a user login system, so that users can submit under a specific account instead of anonymously.

Maybe we do not even need to have our own database of users, but can just connect everything directly to GitHub. Then users can actually submit changes directly as GitHub pull requests under their own user account. And maybe we could even serve the contents from their own fork instead of the main repository.

It should be possible to whitelist users so they can push library changes directly to the main repository.

It would be nice to visually combine relations whenever possible. The two relations do not necessarily have to be the same, "a<b<=c" is fine as well.

Note that writing "a=b=c" is already possible.

Currently, when the user starts editing an item and then either navigates to a different item or reloads the page, all changes are lost.

• Navigating between items can be useful while entering a theorem. It might even make sense to interrupt editing and input something else first. All unsaved data should be preserved and be made visible in the GUI.
• Reloading the page should trigger a warning. See https://developer.mozilla.org/en-US/docs/Web/API/WindowEventHandlers/onbeforeunload.
• The page should stay in edit mode while the submission is in progress. If the user makes further edits, it must be evident that these have not been submitted yet. A failed submission attempt should stay open.

When using a relation symbol as a variable, it can currently only be used as-is. There are three manipulations that are already in use but do not yield readable results:

• Negating $related should produce a crossed-out variant (if one exists).
• The $converse of the relation should be rendered as the reversed symbol (if it exists and is different from the original symbol).
• The $strict variant of a relation with a "half-equals" sign should be rendered as the same symbol without the "half-equals" sign.

This feature requires a table of character transformations, which should somehow be merged with the symbol information that is now contained in templates.slate.

Somewhat related to #39.

Add everything required to input proofs, including

• menus and dialogs for all inference rules,
• visualization of open and closed goals, and
• inline proofs.

Theorems in the library could be used as basic building blocks for a computer algebra system, particularly those theorems that state equalities. For every transformation, such a CAS would be able to output a proof in terms of these theorems.

The CAS itself would probably be of limited use at first, but the real benefit would be to provide suggestions during proof input, hopefully eliminating some of the most tedious and uninteresting steps.

The "shortcut" concept in HLM is intended for better readability, but a specialization for certain cases of structural induction would be even better. Therefore the library should be converted to explicitly use structural induction everywhere, and then the "shortcut" concept should be removed from the logic.

In cases with only one constructor, we will usually want to replace the shortcut notation with conventional mathematical "abuse of notation." See e.g. http://slate-prover.herokuapp.com/libraries/hlm/Algebra/Magmas/Free%20magma/free%20on%20set.

Instead of axioms, the HLM logic has rules to prevent certain circularities that lead to paradoxes. These can only be implemented by checking the entire library at once.

In order to define the category of all small(er) categories, the rules have been extended by levels given as natural numbers. This needs to be fully specified.

Provide support for editing existing and new definitions and theorems.

Includes, among other things:

• Making context information available via generated code.
• Filtering trees by item type and logical type.
• Adding editing functionality to macros (including dialog-based data input as in "operator as function").
• (Handling special rendering features such as properties. => #56)

Editing existing items can break dependencies. Renaming parameters should probably just be forbidden (or later handled correctly) if there are dependencies. Other changes should be accepted, since they might be corrections, but we should warn the user about dependencies that could be broken by the change.

While the type-checking code for full expressions is reasonably straight-forward and well-tested, things become more complex and ad-hoc in the presence of placeholders. Initially, this situation could only be tested manually by creating appropriate partial objects in the GUI, so it did not fit well into the existing testing framework. However, reading files with placeholders is possible now, so it is possible to write these tests as .slate files in shared/logics/hlm/__tests__/data now.

This requires three additions to checker.test.ts:

• The reader and checker must be configured to support placeholders.
• For tests about auto-filling, there needs to be a mechanism to declare what the final result should be; something like @expectedAutoFillResult in the docstring, similar to @expectedError. (It is probably sufficient if we limit this feature to theorem claims.)
• And finally, auto-filling must be triggered, and the result must be compared.

Currently known bugs:

• There is an unexpected dependency on the order of operations in checkEquivalenceOfTemporarySetTerms; see TODO item there.
• Placeholders that are not marked as "auto" are sometimes not filled even when they should be. E.g.:
  • "Let f,g : X -> X be functions such that f ° g is injective ..."
  • "Let G be a group, g in G... g = e_?."
  • Sometimes, category arguments are not filled automatically when dealing with objects or morphisms in that category. E.g. in the following case, the implict arguments of the outer composition are not filled automatically:
    "Let C be a category, X be an object of C. f := id_X ° id_X"
• In certain complicated expressions with several placeholders, the type checker essentially "gives up" and lets the user enter everything. TODO: Collect some examples. (Does the VSCode extension display a type error in these cases? If not, we can add test cases with @expectedError, but if yes, it will be more complicated to test.)

Quite possibly, testing will uncover a lot of problems that can only be fixed by using more general algorithms.

Further ideas; should probably be moved to a separate issue:

• Test cases can be constructed programmatically by replacing parts of existing expressions in the library with placeholders and checking whether it is possible to fill these placeholders such that the original result is recovered. Caveats: This only catches false negatives but not false positives. Some situations only occur with multiple placeholders.
• Given a list of expressions that are deemed compatible with a placeholder, it makes sense to check whether every item in that list leads to at least one complete well-typed expression. However, a negative result is not necessarily an error.

After having entered a, the user should be able to change it to a + b without losing a. The desktop version had support for this via right-click; the web GUI should display a visible dropdown menu instead.

It should be possible to select an operator directly as a function. The corresponding macro should be instantiated automatically, as it is more or less invisible to the user.

Currently, the VSCode extension does not know which parameter lists belong to certain argument lists:

• %BindingArg
• %UseForall
• %ProveExists

This has two main consequences:

• Convenience features like signature help and autocompletion don't work.
• The parameter names are not found by "find all references" and "rename." This is problematic in the case of %BindingArg.

Solving this requires extending the expressiveness of metamodels.

Greet new users with an interactive tutorial. While stepping through the tutorial, the next step is shown as a popup. Submitting items has no effect as long as the user is in tutorial mode.

In implicit definitions, the condition sometimes implies that assumptions of the definitions are automatically satisfied. For example:

• If the function f has an inverse g, then f is bijective and f^-1 = g.
• If a series (a_n) converges to l, then (a_n) is convergent and lim a_n = l.

Especially in the second case, we would like to simply state lim a_n = l as a theorem, and prove it by showing that (a_n) converges to l, with the intention that the theorem also implies that (a_n) is convergent. (The proof obviously does.)

In theory, this could be handled purely in the library, by defining a predicate that is rendered as "lim a_n = l." However, this seems confusing, since it essentially overloads equality. So it might be better to mark the assumption as "implied", so that "lim a_n = l" really means "(a_n) is convergent and lim a_n = l" -- unless the equality is negated.

In addition, it could be helpful to add a proof that the assumption actually follows from the given definition, so that a proof of "lim a_n = l" can simply be given as a proof of "(a_n) converges to l".

The system (client and/or server) should search for proofs in the background, both when entering proofs and regularly on the entire library.

In Slate, it would not necessarily be convenient to have tactics that perform complex searches to prove a particular result. Instead, the system could try to close individual subgoals of the current proof, filling in the steps automatically when finished.

It would be nice to search for counterexamples as well, in case the user has made a mistake.

Operators and predicates defined on a set with an embedding frequently extend their counterparts on the embedded subset. Such compatibility declarations can be stated as theorems, but this currently looks confusing because the symbols are not distinguishable. Rather than fixing the visualization, it would be nice to declare and prove compatibility directly in the definitions of the operators and predicates.

Ideally, this should also work for other cases where notation is overloaded, e.g. when defining exponentiation in several steps.

Example: In empty.slate, 0 <= 0 for cardinal numbers should reduce to 0 <= 0 for natural numbers, which will be handled by the corresponding macro.

After declaring that an operator or operation is associative, the system should omit parentheses both visually and when working with the operator/operation.

There are at least three different situations where this should happen:

• For an operator or set operator, it should be possible to label a theorem that directly states its associativity. The theorem statement must follow a specific structure that can be derived from the definition of the operator. The most important examples of this case are set intersection/union and function composition.
• For an operator, the theorem can also convert the operator to an operation, and state the associativity of that operation.
• For an operation, the associativity is usually only a known fact in the current (proof or other) context. Sometimes this even requires following some definitions. The operator that returns the value of an operation should declare its conditional associativity.
• The same type of conditional associativity occurs in an algebra context, e.g. for associative magmas.

Once associativity of a particular expression has been established, this fact should be marked, e.g.:
$sum(a={a}, b={%associative($sum(a={b}, b={c}))})
Then the renderer only needs to look at the expression itself to determine where to omit parentheses.

When defining a set (construction or operator), optionally provide suggestions on how to use or construct an element of that set.

• Usage suggestions should apply to variables in the current context (including variables that are not directly applicable at the given location). In certain cases, they should also extend the library tree; see below.
• Construction suggestions should apply whenever a term of the given set is expected.

Currently, the following suggestions would be desirable:

• Usage (using data provided for #36):
  • Properties: "has property"
  • Relations: "related"
  • Functions and operations: "value"
  • Any structure: "Carrier"
    • This will solve the case "Let G be a group, g in G".
    • To avoid confusion, it should also extend to definitions in the library. I.e. it should become possible to directly enter something like "Let g in S_42".
    • Do we need any additional convenience functionality for explicit structure definitions, similarly to type classes or canonical structures in other provers?
• Construction:
  • Wherever a number is required, it should be possible to enter this number directly. This is strongly connected to #74.
  • If there is only a single constructor with a single parameter, and this constructor can be applied to a variable in the current context, that should become a suggestion.
  • If there is only a single constructor and that constructor contains a binding (e.g. property, relation, function, operator), there should be an immediate way to select a predicate or operator in a way that makes the special rendering due to #68 transparent (see outdated issue #9).
  • If a macro exists that produces an element of the given set, that macro should be suggested. Low priority because currently, this would only provide suggestions for tuples and matrices of fixed size (which are rare), if numbers are already handled differently.

Suggestions that are based on variables could show up directly in the list of variables.

After a definition or theorem statement has been entered completely, the user should get a chance to fill all remaining unfilled placeholders, instead of getting an error upon submission. Possible solution:

• Show these placeholders in a popup.
• Turn off the corresponding custom notation temporarily.
• Show the source code, and display placeholders there instead of question marks.

Implement a basic framework to check individual files according to the rules of the logic, and provide a first implementation for HLM. Initial checks merely concern core language parts that are not covered by the metamodel (see below). Stubs for type checking and proof checking should be included.

The framework should be used from the "logic extension" part of the VSCode extension.

Initial checks should include:

• Parameter types cannot be used as proof steps and vice versa (except for definitions).
• Optional parameters, list parameters, default arguments, array types, and dependencies are not allowed.
• Set terms, element terms, and formulas only allow a restricted set of expressions. Referenced variables must be set/element/proposition variables.
• The number of indices of variable references must match their binding depth.
• All arguments of definition references must be filled, except constraints.
• "previous" can only be used if the previous/outer parameter matches.
• Parameter lists of cases and equality definitions need to match their original sources.
• Case formulas must be chosen so that exactly one case applies.

Implement a basic typescript interface and registration mechanism for macros, i.e. code that is part of the library but injected into the proof checker.

The initial implementation of each macro only needs "resolve" functionality. This is necessary for type checking.

Moving .slate files in VSCode currently breaks references both in the moved files and in other files that require them. Since we will definitely reorganize the library quite a bit over time, automatically updating the references would be really nice. Depends on microsoft/vscode#43768, however.

Determine a framework for automated tests, and develop some tests that are particularly quick to implement. Ideas:

• Read and rewrite the entire library, and compare with repository. The read/write functionality already exists as src/scripts/tidyLibrary.sh.
• Render the entire library as text, and compare with previously accepted result. Would require a "blind" acceptance after every library change, but would likely catch errors when working on rendering code.
• A generic black-box test for the VSCode language extension would be nice. https://code.visualstudio.com/api/working-with-extensions/testing-extension describes how to write unit tests, but it seems cheaper to query the extension for all links/tooltips/codelenses/etc. in a file and dump them, to detect unwanted changes.
• The desktop version had unit tests for the type checker, based on a separate miniature library. These should be converted to TypeScript, and the library could also be used as a starting point for rendering tests.

Add buttons to create new items. Open a dialog to specify the type, name, and exact location. Let user edit and submit the result.

Currently, in Ker(?,?,id_G), the two placeholders are not automatically filled with G. This is a problem because they are invisible.

Part of the reason is probably that id_G is only known to be an element of the set of functions from the underlying set of G to itself, but not an element of Hom(G,G). This makes the constraints between the placeholders less than straightforward, but it should still work.

Currently, remarks are pure Markdown text. References to library items are encoded as HTTP links. It would be nice if they could be written in .slate file syntax instead.

Something similar already exists in documentation comments of other languages, and we should use the same syntax if possible.

It should be supported in four places:

• In the web GUI, when viewing an item (obviously).
• In the preview mode of the markdown editor in the web GUI (if possible).
• In VSCode tooltips (if this can be done easily).
• In VSCode, as source code: All applicable features of the extension should work, in particular the syntax should be checked, links should work, and the content should be found by "find all references" and "rename."

Improve display expression menus and dialogs by

• displaying tooltips,
• displaying previews,
• making suggestions based on the type of object and number of parameters, and
• asking the user whether parameters should be marked as "auto" if they do not appear in the result.

Equality definitions can be labelled as "isomorphic" to make well-definedness proofs unnecessary. Currently this can only be done by directly editing the source code of the definition, and the system does not check whether the definition really is isomorphic.

• Whenever possible, the system should suggest a suitable isomorphic equality definition to the user and label it accordingly.
• The check whether the label is correct needs to be added to the type and proof checks.

An appropriate check still needs to be worked out for the definition of functors in category theory.

Remark: After #65 is completed, HLM will be equipped a little better to formulate the condition of being "isomorphic" internally: It will be possible to state something like "for all propositions p for each set S and ..., p_(X,...) is equivalent to p_(Y,...)," i.e. "all properties of one structure also apply to the other." By default, such a proposition is not provable, but there could be something like an axiom scheme saying that it follows from the corresponding "isomorphic" equality definition. (Not sure whether this would be useful or not.)

Moreover, well-definedness proofs of structural expressions are currently impossible to provide if arbitrary sets are involved, because of type mismatches in the goal. In such cases, the goal should be changed from requiring equality to requiring the existence of an isomorphism between the original structures that maps between the left and right side of the equality.

Currently, opening the application causes lots of requests to https://raw.githubusercontent.com/, one for each library item that is loaded. To improve performance, the server should prepare a bundled version of the library, to be preloaded by the client at startup.

• The server can store the data in memory; no disk storage is necessary.
• The server should regularly check whether the GitHub repository has changed, and update its cache accordingly.
• The server should reduce the amount of data by omitting proofs, reducing whitespace, and offering a compressed version.
• The client should immediately download the data at startup. However, the data must not be used until the client has determined that no local changes exist in the user's repository (if any). I.e. it can only be used in those cases where the data is read from the main library repository.
• Before an item is displayed in an editor, the full version must be downloaded from GitHub. To avoid delays, preloading from GitHub can be triggered the same way it works at the moment, even in cases where the full version is not yet needed.

Add the ability to search for items in the library, e.g. by filtering the tree, as in the desktop version.

Maybe add keywords to make finding items easier.

Should use the same filtering mechanism as #8.

The Visual Studio Code extension runs into problems if a currently open file is renamed or moved. Two problems are known:

• If the file had errors before renaming, these errors are not cleared, and VSCode complains when clicking on them.
• Code lenses referring to the file are not shown even after all errors have been fixed.

This is probably due to the fact that the document reference stays the same.
Maybe this can actually be exploited to solve #1.

Also, if a file is copied, errors are not shown until the new file is modified. Maybe VSCode actually uses the existing document to refer to the new file.

Constructions can be equipped with an embedSubsets feature that allows treating elements of one instance of the construction as elements of another. This needs to be subject to certain well-definedness conditions that still need to be worked out. They can probably be checked purely syntactically.

Regularly verify that all links in references of library definitions/theorems still work.

Since HLM lacks a small verification kernel, there should eventually be a way to ensure its correctness, or at least ensure the correctness of the current library. The most promising method seems to be a translation to a simpler intermediate logic, and then to other systems.

This should be possible for every statement and proof, but not necessarily for every definition. E.g. the statement that the set of groups of order 4 has cardinality 2 can be broken down step by step into the statement that there are two non-isomorphic groups of order 4, given as sets with operations, such that every group of order 4 is isomorphic to one of them. This will be a long statement, but it avoids all of the definitions involved in the original statement that do not have a counterpart in other systems.

Implementation idea: The simplification and translation could be built as a series of library transformations with HLM that can be performed individually. Each translation eliminates the use of a single advanced HLM feature, e.g.

• sets as constructor parameters,
• embeddings,
• binding parameters,
• symbol parameters,
• macros.

The result ought to be translatable to practically any set theory, type theory, or higher order logic. However, there needs to be a mapping between some basic definitions in the library and their counterparts in the standard library of the target system.

Certain definitions, particularly the intersection and union of sets, are independent of the argument of some parameter. Therefore, this parameter is omitted in the notation. However, the parameter still exists, so two equal-looking expressions may in fact be syntactically different.

There should be a built-in way to prove the independence from that parameter, to the effect that expressions that differ only in that one argument are considered equal. Such a built-in equality is similar to #29.

The existence of two embeddings with the same source, e.g. from natural numbers to cardinal numbers and to ordinal numbers, should not permit direct comparisons of elements of the two targets. While restricting this in the logic seems tricky, it should at least be handled in the GUI. The reason it is important is that it is not clear what e.g. the comparison between aleph-0 and omega actually means -- the simple interpretation would be that equality would imply that both are natural numbers, so they are provably unequal, which is confusing at least.

Add the necessary checks to verify proofs, i.e.

• whether the parameters and goal of the proof match the requirements,
• whether all of the steps in a proof are valid, and
• whether the proof completely proves the goal.

Add overlay icons to library items to distinguish

• fully proved theorems (green),
• theorems that lack a proof (yellow),
• theorems that have one or more proofs but none of them are fully verified from first principles (no icon, but the user should be able to find out where the gaps are),
• definitions or theorem statements where inline or well-definedness proofs are missing (yellow, but at some point we will no longer accept such submissions),
• definitions or theorem statements where inline proofs depend on unproved results (also yellow?), and
• definitions where everything is OK (no icon).

When submitting a proof, at least the icon of that item should be updated immediately. In general, the verification status could be determined during a check of the entire library, see #18. It should probably be stored in the _index.slate files; if the library check touches those, that's OK.

Possibly include more info about dependencies, like e.g. in Metamath.