-
Notifications
You must be signed in to change notification settings - Fork 19
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
* Starting a layer of abstraction. * swrdgv * sedgf * ONgoing work. FOL structure mostly implemented, substitutions ongoing. * continued * further changes * LisaObject has a self type being self * More improvements on substitution * More work * multivar substitution * improvements to MapProofTest * finished fol, need to do prooflib * started work on prooflib, cut plenty unused code in Library.scala * more work on substitutions * updated WithTheorems * finished BasicSteptactics and substitutions * more corrections of tactics using unifier * fixed F and K imports * finished PrrofHelpers and definitions. Definitions possibly not final * Done most of the simpleDeducedSteps * ongoing work on types * added doc in Common.scala * more doc, some simplification * more doc and simplification of unneeded parts * fixed some export issues. Commented some tests. translation left for the future. * remove some debug code * add missing files * continue F integration. FInished with Set theory library files, now doing CommonTactics.scala (part is Dario's work). * simplifier remaining * renaming and mroe compatibility * more adaptations * merge build.sbt * fixing * transforming unification to Front * weird issues with match types and dotty * Compiles..? Need to simplify use of Arity in formula labels now. Finger crossed. * add missing files * still compiles * Term**0 |-> Term * Does not compile (dotty crash). Possibly due to covariant schematic labels. * Labels are contravariant * Weird "inherits conflicting instances of non-variant base trait LisaObject" * structure seems to work; Constant extends ConstantFunctionSymbol[0], issue with case class (has to reimplement). * back to the "common super type with case classes" structure * finished predicates, compiles. Connector left * Finished datastructure. TODO: Underlyings, Arity, uncomment asFront * Compiles, checked arity and underlyings (mostly) * Rehabilited asFront. Next stop, Substitution. * porting unificationUtils * half of unificationUtils done. Need to make Common even closer structure to kernel (variableFormula extends PredicateFormula) * progress through unification * compiles, progressing * safe for reset * only applySubst remaining. Note: given ```scala val s: Seq[(Variable, Term)] ``` `s.toMap` crashes dotty. Instead, do `Map(s*)`. * Substitution done, everything compiles. * rehabilited commented function * utils tests compiles and pass. * Finished setTheorzLibrary, close to finish OLPropositionalSolver * Quantifiers.scala work, completed BasicProofTactic, implemented printing of terms and formulas * progress on compilation and run of SetTheory.scala * ordinals1 works * Everything works, even example package. Some tests are still commentated. Simplified a couple proofs. * Small improvements * Ready for demo * scalafix, scalafmt * git add * Add a Quick User Guide as chapter 1 of the reference manual * small changes to manual * update colors and date * git add quickguide.tex * small manual update * Add a section on special characters (unicode and ligatures), spellcheck.
- Loading branch information
1 parent
265ed45
commit 49d235f
Showing
12 changed files
with
1,017 additions
and
578 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Binary file not shown.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,99 +1,51 @@ | ||
| \chapter{Developping Mathematics with Prooflib} | ||
|
|
||
| \section{Writing theory files} | ||
| LISA provides a canonical way of writing and organizing Kernel proofs by mean of a set of utilities and a DSL made possible by some of Scala 3's features such as string interpolation, extension and implicits. | ||
| The way to write a new theory file to mathematical development is: | ||
| \begin{lstlisting}[language=Scala, frame=single] | ||
| \label{chapt:prooflib} | ||
| LISA's kernel offers all the necessary tools to develops proofs, but reading and writing proofs written directly in its language is cumbersome. | ||
| To develop and maintain a library of mathematical development, LISA offers a dedicate interface and DSL to write proofs: Prooflib | ||
| LISA provides a canonical way of writing and organizing Kernel proofs by mean of a set of utilities and a DSL made possible by some of Scala 3's features. | ||
| \autoref{fig:theoryFileExample} is a reminder from \autoref{chapt:quickguide} of the canonical way to write a theory file in LISA. | ||
|
|
||
| \begin{figure} | ||
| \begin{lstlisting}[language=lisa, frame=single] | ||
| object MyTheoryName extends lisa.Main { | ||
|
|
||
| } | ||
| \end{lstlisting} | ||
| and that's it! To write a theorem, the recommended syntax is: | ||
|
|
||
| \begin{lstlisting}[language=Scala, frame=single] | ||
| object MyTheoryName extends lisa.Main { | ||
|
|
||
| THEOREM("theoremName") of "desired conclusion" PROOF { | ||
|
|
||
| ???: Proof | ||
|
|
||
| } using (listOfJustifications) | ||
| show | ||
| } | ||
| \end{lstlisting} | ||
| \lstinline|show|{} is optional and prints the last proven theorem. We can similarily make the definition: | ||
|
|
||
| % avoid page breaking | ||
| \noindent | ||
| \begin{minipage}{\textwidth} | ||
| \begin{lstlisting}[language=Scala, frame=single] | ||
| object MyTheoryName extends lisa.Main { | ||
|
|
||
| val myFunction = | ||
| DEFINE("symbol", x, y) as definition(x,y) | ||
| show | ||
| val x = variable | ||
| val f = function[1] | ||
| val P = predicate[1] | ||
|
|
||
| val fixedPointDoubleApplication = Theorem( | ||
| ∀(x, P(x) ==> P(f(x))) |- P(x) ==> P(f(f(x))) | ||
| ) { | ||
| assume(∀(x, P(x) ==> P(f(x)))) | ||
| val step1 = have(P(x) ==> P(f(x))) by InstantiateForall | ||
| val step2 = have(P(f(x)) ==> P(f(f(x)))) by InstantiateForall | ||
| have(thesis) by Tautology.from(step1, step2) | ||
| } | ||
|
|
||
|
|
||
| val emptySetIsASubset = Theorem( | ||
| ∅ ⊆ x | ||
| ) { | ||
| have((y ∈ ∅) ==> (y ∈ x)) by Tautology.from( | ||
| emptySetAxiom of (x := y)) | ||
| val rhs = thenHave (∀(y, (y ∈ ∅) ==> (y ∈ x))) by RightForall | ||
| have(thesis) by Tautology.from( | ||
| subsetAxiom of (x := ∅, y := x), rhs) | ||
| } | ||
| \end{lstlisting} | ||
| \end{minipage} | ||
| % | ||
| This works for definitions of function and predicate symbols with a direct definition. for indirect definitions (via $\exists !$), use the following: | ||
| % | ||
| \begin{lstlisting}[language=Scala, frame=single] | ||
| object MyTheoryName extends lisa.Main { | ||
|
|
||
| val testdef = | ||
| DEFINE("symbol", x, y) asThe z suchThat { | ||
| ???:Formula | ||
| } PROOF { | ||
| ???:Proof | ||
| } using (listOfJustifications) | ||
| show | ||
| } | ||
| \end{lstlisting} | ||
| \caption{An example of a theory file in LISA} | ||
| \label{fig:theoryFileExample} | ||
| \end{figure} | ||
|
|
||
| In this chapter, we will describe how each of these construct is made possible and how they translate to statements in the Kernel. | ||
|
|
||
| ======= | ||
| It is important to note that when multiple such files are developed, they all use the same underlying \lstinline|RunningTheory|{}. This makes it possible to use results proved previously by means of a simple \lstinline|import|{} statement as one would import a regular object. Similarly, one should also import as usual automation and tactics developed alongside. It is expected in the medium term that \lstinline|lisa.Main|{} will come with basic automation. | ||
|
|
||
| To check the result of a developed file, and verify that the proofs contain no error, it is possible to run such a library object. | ||
| % specify which object | ||
| All imported theory objects will be run through as well, but only the result of the selected one will be printed. | ||
| \section*{WIP} | ||
|
|
||
| It is possible to refer to a theorem or axiom that has been previously proven or added using its name. The syntax is \lstinline|thm``theoremName''|{} or \lstinline|ax``axiomName''|{}. This makes it possible to write, for example, \lstinline|thm``theoremName''.show|{} and \lstinline|... using (ax``comprehensionSchema'')| Figure \ref{fig:kernellibrary} shows a typical example of set theory development. | ||
| %It is important to note that when multiple such files are developed, they all use the same underlying \lstinline|RunningTheory|{}. This makes it possible to use results proved previously by means of a simple \lstinline|import|{} statement as one would import a regular object. Similarly, one should also import as usual automation and tactics developed alongside. It is expected in the medium term that \lstinline|lisa.Main|{} will come with basic automation. | ||
| %All imported theory objects will be run through as well, but only the result of the selected one will be printed. | ||
|
|
||
|
|
||
| \begin{figure}[hp] | ||
| \begin{lstlisting}[language=Scala, frame=single] | ||
| object MyTheoryName extends lisa.Main { | ||
| THEOREM("russelParadox") of | ||
| (*@ $\forall$ @*)x. (x(*@$\in$@*)?y)(*@$\leftrightarrow$@*) (*@$\neg$@*)(x(*@$\in$@*)x)(*@$\vdash$@*) PROOF { | ||
| val y = VariableLabel("y") | ||
| val x = VariableLabel("x") | ||
| val s0 = RewriteTrue(in(y, y) <=> !in(y, y) |-()) | ||
| val s1 = LeftForall( | ||
| forall(x, in(x, y) <=> !in(x, x)) |- (), | ||
| 0, in(x, y) <=> !in(x, x), x, y | ||
| ) | ||
| Proof(s0, s1) | ||
| } using () | ||
| thm"russelParadox".show | ||
|
|
||
|
|
||
| THEOREM("unorderedPair_symmetry") of | ||
| "(*@$\vdash$@*)(*@$\forall$@*)y, x. {x, y} = {y, x}" PROOF { | ||
| ... | ||
| } using (ax"extensionalityAxiom", ax"pairAxiom") | ||
| show | ||
|
|
||
|
|
||
| val oPair = | ||
| DEFINE("", x, y) as pair(pair(x, y), pair(x, x)) | ||
|
|
||
| } | ||
| \end{lstlisting} | ||
| \caption{Example of library development in LISA Kernel} | ||
| \label{fig:kernellibrary} | ||
| \end{figure} | ||
|
|
||
|
|
||
|
|
Oops, something went wrong.