diff --git a/refman/.gitignore b/refman/.gitignore index 829b57d1f46154dcfedc0254301afeacbb749767..cbeb53ce01c965cf66483461a402bc663884654e 100644 --- a/refman/.gitignore +++ b/refman/.gitignore @@ -6,3 +6,4 @@ lisa.fls lisa.log lisa.out lisa.toc +src/.scala-build diff --git a/refman/lisa.pdf b/refman/lisa.pdf index d22d7da5a928e5881571fad1be52a1ad76fd4a2c..a0cf24de65a00e0dc54cfe5b385d572930ba6a6c 100644 Binary files a/refman/lisa.pdf and b/refman/lisa.pdf differ diff --git a/refman/lisa.tex b/refman/lisa.tex index 4e6ae055134bf0090ce2e90f40a885107d000a71..d52bd9482059c9d2f3701095e154b819f8467024 100644 --- a/refman/lisa.tex +++ b/refman/lisa.tex @@ -21,7 +21,8 @@ \date{} % PDF links and meta data -\usepackage{hyperref} +%\usepackage{hyperref} +\usepackage{bookmark} \makeatletter \hypersetup{ colorlinks=true, diff --git a/refman/macro.tex b/refman/macro.tex index 31938969ee9abf860752d65a29bce9641227ea8e..4a2bf14ec65ad0f34594ea83f58f45b41778fbf7 100644 --- a/refman/macro.tex +++ b/refman/macro.tex @@ -184,3 +184,6 @@ \DeclareMathOperator{\pick}{pick} +\newcommand{\lisaCode}[3]{ +\lstinputlisting[language=lisa, frame=single,caption=\href{#1}{#2}, #3]{#1} +} diff --git a/refman/prooflib.tex b/refman/prooflib.tex index 7daebca45e7f900d4e92f25313775d5124e3c7ca..47e372f8d844559ed4dc54208a7c2e858b3f2b81 100644 --- a/refman/prooflib.tex +++ b/refman/prooflib.tex @@ -6,34 +6,7 @@ Lisa provides a canonical way of writing and organizing Kernel proofs by mean of \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 { - 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} -\caption{An example of a theory file in Lisa} +\lisaCode{src/MyTheoryName.scala}{An example of a theory file in Lisa}{firstline=3} \label{fig:theoryFileExample} \end{figure} diff --git a/refman/src/MyTheoryName.scala b/refman/src/MyTheoryName.scala new file mode 100644 index 0000000000000000000000000000000000000000..b2a48eb45a31d8a8b20c05c2bc21ee3f7f4c4410 --- /dev/null +++ b/refman/src/MyTheoryName.scala @@ -0,0 +1,29 @@ +//> using scala 3.5.1 +//> using jar "../../../lisa/target/scala-3.5.1/lisa-assembly-0.7.jar" +object MyTheoryName extends lisa.Main: + val x = variable + val y = 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) + } + + @main def show = println(emptySetAxiom) +