sreichelt / slate Goto Github PK
View Code? Open in Web Editor NEWThe Slate Interactive Theorem Prover
Home Page: https://slate-prover.org
License: MIT License
The Slate Interactive Theorem Prover
Home Page: https://slate-prover.org
License: MIT License
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.
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:
data/libraries
directory, or is there a better solution?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.
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, 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:
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.
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.
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.
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.
Add everything required to input proofs, including
Integrate the web app into the VSCode extension as a webview.
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.
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.
Currently, when the user starts editing an item and then either navigates to a different item or reloads the page, all changes are lost.
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.
Add buttons to create new items. Open a dialog to specify the type, name, and exact location. Let user edit and submit the result.
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.
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.
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.
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:
Improve display expression menus and dialogs by
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.
Extracted from #2: Run VSCode extension in isolation and dump information for regression testing.
Determine a framework for automated tests, and develop some tests that are particularly quick to implement. Ideas:
src/scripts/tidyLibrary.sh
.Regularly check all types, proofs, and dependencies of the entire library. Preferably, do not accept pushes to the main repository that break the library.
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.
Provide support for editing existing and new definitions and theorems.
Includes, among other things:
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.
Add overlay icons to library items to distinguish
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.
In implicit definitions, the condition sometimes implies that assumptions of the definitions are automatically satisfied. For example:
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".
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.
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:
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.
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.
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.
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:
$related
should produce a crossed-out variant (if one exists).$converse
of the relation should be rendered as the reversed symbol (if it exists and is different from the original symbol).$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.
When defining a set (construction or operator), optionally provide suggestions on how to use or construct an element of that set.
Currently, the following suggestions would be desirable:
Suggestions that are based on variables could show up directly in the list of variables.
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
:
@expectedAutoFillResult
in the docstring, similar to @expectedError
. (It is probably sufficient if we limit this feature to theorem claims.)Currently known bugs:
checkEquivalenceOfTemporarySetTerms
; see TODO item there.@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:
The Visual Studio Code extension runs into problems if a currently open file is renamed or moved. Two problems are known:
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.
Add the necessary checks to verify proofs, i.e.
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.
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.
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.
There should be documentation about
Some of this documentation should be in the form of code comments.
Regularly verify that all links in references of library definitions/theorems still work.
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.
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:
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.
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, the VSCode extension does not know which parameter lists belong to certain argument lists:
%BindingArg
%UseForall
%ProveExists
This has two main consequences:
%BindingArg
.Solving this requires extending the expressiveness of metamodels.
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.
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
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:
Cons:
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.
Users should be able to collect points of some sort for (accepted) additions to the library.
Some requirements:
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
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.