From 6417e942447763385bed9dd3ba630b64d08bfefc Mon Sep 17 00:00:00 2001 From: adelon <22380201+adelon@users.noreply.github.com> Date: Tue, 25 Jun 2024 17:15:27 +0200 Subject: Add `\neg` --- source/Syntax/Lexicon.hs | 1 + 1 file changed, 1 insertion(+) (limited to 'source/Syntax/Lexicon.hs') diff --git a/source/Syntax/Lexicon.hs b/source/Syntax/Lexicon.hs index b5e4f58..463dd18 100644 --- a/source/Syntax/Lexicon.hs +++ b/source/Syntax/Lexicon.hs @@ -109,6 +109,7 @@ prefixOps = , ([Just (Command "fst"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "fst")) , ([Just (Command "snd"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "snd")) , ([Just (Command "pow"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "pow")) + , ([Just (Command "neg"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "neg")) , (ConsSymbol, (NonAssoc, "cons")) , (PairSymbol, (NonAssoc, "pair")) -- NOTE Is now defined and hence no longer necessary , (ApplySymbol, (NonAssoc, "apply")) -- cgit v1.2.3 From b71f135d5762f2a12bf08c71ecdcd221ed87cff0 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Sat, 6 Jul 2024 19:22:03 +0200 Subject: Formalisation of integers. --- library/numbers.tex | 123 ++++++++++++++++++++++++++++++++++++++--------- source/Syntax/Lexicon.hs | 1 + 2 files changed, 101 insertions(+), 23 deletions(-) (limited to 'source/Syntax/Lexicon.hs') diff --git a/library/numbers.tex b/library/numbers.tex index a185940..08cbc70 100644 --- a/library/numbers.tex +++ b/library/numbers.tex @@ -371,19 +371,18 @@ \end{lemma} +\subsection{Axioms of the reals Part One} +We seen before that we can proof the common behavior of the naturals. +Since we now want to get furhter in a more efficient way, we introduce the basis axioms of the reals. +Such that we can introduce the integers and raitionals as smooth as possible. +\begin{axiom}\label{reals_rmul} + For all $n,m \in \reals$ we have $(n \rmul m) \in \reals$. +\end{axiom} - - - - - - - -\subsection{The Intergers} - - - +\begin{axiom}\label{reals_add} + For all $n,m \in \reals$ we have $(n + m) \in \reals$. +\end{axiom} \begin{axiom}\label{reals_axiom_dense} For all $x,y \in \reals$ if $x < y$ then @@ -423,20 +422,104 @@ such that $x < z < y$. \end{axiom} -\begin{proposition}\label{reals_disstro2} +\begin{axiom}\label{reals_disstro2} For all $x,y,z \in \reals$ $(y + z) \rmul x = (y \rmul x) + (z \rmul x)$. -\end{proposition} +\end{axiom} + + +\begin{axiom}\label{reals_reducion_on_addition} + For all $x,y,z \in \reals$ if $x + y = x + z$ then $y = z$. +\end{axiom} + + + + + + + +\subsection{The Intergers} + + +\begin{axiom}\label{neg} + For all $n \in \reals$ we have $\neg{n} \in \reals$ and $n + \neg{n} = \zero$. +\end{axiom} + +\begin{axiom}\label{neg_of_zero} + $\neg{\zero} = \zero$. +\end{axiom} + +\begin{definition}\label{minus} + $n - m = n + \neg{m}$. +\end{definition} + +\begin{lemma}\label{minus_in_reals} + Suppose $n,m \in \reals$. + Then $n - m \in \reals$. +\end{lemma} \begin{proof} - Omitted. + \begin{byCase} + \caseOf{$m = \zero$.} Trivial.%Follows by \cref{neg_of_zero,minus,neg,reals_add}. + \caseOf{$m \neq \zero$.} Trivial.% Follows by \cref{neg_of_zero,minus,neg,reals_add}. + \end{byCase} \end{proof} -\begin{proposition}\label{reals_reducion_on_addition} - For all $x,y,z \in \reals$ if $x + y = x + z$ then $y = z$. +\begin{proposition}\label{negation_of_negation_is_id} + For all $r \in \reals$ we have $\neg{\neg{r}} = r$. \end{proposition} \begin{proof} - Omitted. + Fix $r \in \reals$. + $r + \neg{r} = \zero$. + $\neg{r} + \neg{\neg{r}} = \zero$. + Follows by \cref{reals_reducion_on_addition,neg,reals_axiom_kommu}. \end{proof} +\begin{definition}\label{integers} + $\integers = \{ z \in \reals \mid \exists n \in \naturals. z \in \naturals \lor n + z = \zero\}$. +\end{definition} + +\begin{lemma}\label{n_subset_z} + $\naturals \subseteq \integers$. +\end{lemma} + +\begin{lemma}\label{neg_of_naturals_in_integers} + For all $n \in \naturals$ we have $\neg{n} \in \integers$. +\end{lemma} + +\begin{lemma}\label{integers_eq_naturals_and_negativ_naturals} + $\integers = \{ z \in \reals \mid \exists n \in \naturals. n = z \lor \neg{n} = z\}$. +\end{lemma} +\begin{proof} + Let $P = \{ z \in \reals \mid \exists n \in \naturals. n = z \lor \neg{n} = z\}$. + \begin{byCase} + \caseOf{$\integers \subseteq P$.} Trivial. + \caseOf{$P \subseteq \integers$.} Trivial. + \end{byCase} +\end{proof} + + + + +\subsection{The Rationals} + +%\begin{definition} +% $\inv{x} +%\end{definition} +% +%\begin{axiom} +% For all $x,y \in \reals$ we have $\rfrac{x}{y} \in \reals$. +%\end{axiom} +% +%\begin{definition} +% $\rationals = \{ q \in \reals \mid \exists z \in \integers. \exists n \in \integers. q = \rfrac{z}{n} \}$. +%\end{definition} + + + + + + + + %\begin{signature}\label{invers_is_set} % $\addInv{y}$ is a set. @@ -608,9 +691,3 @@ \begin{proposition}\label{safe} Contradiction. \end{proposition} - -\section{The integers} - -%\begin{definition} -% $\integers = \{z \in \reals \mid z = \zero or \} $. -%\end{definition} \ No newline at end of file diff --git a/source/Syntax/Lexicon.hs b/source/Syntax/Lexicon.hs index 463dd18..65072ee 100644 --- a/source/Syntax/Lexicon.hs +++ b/source/Syntax/Lexicon.hs @@ -95,6 +95,7 @@ builtinMixfix = Seq.fromList $ (HM.fromList <$>) builtinIdentifiers = identifier <$> [ "emptyset" , "naturals" + , "integers" , "rationals" , "reals" , "unit" -- cgit v1.2.3 From 36e03142465e482f2b5506cd35dab5ef9cc9fd66 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Sat, 6 Jul 2024 19:53:50 +0200 Subject: Formalisation of rationals. --- library/numbers.tex | 66 +++++++++++++++++++++++++----------------------- source/Syntax/Lexicon.hs | 1 + 2 files changed, 35 insertions(+), 32 deletions(-) (limited to 'source/Syntax/Lexicon.hs') diff --git a/library/numbers.tex b/library/numbers.tex index 08cbc70..4ccba67 100644 --- a/library/numbers.tex +++ b/library/numbers.tex @@ -431,7 +431,14 @@ Such that we can introduce the integers and raitionals as smooth as possible. For all $x,y,z \in \reals$ if $x + y = x + z$ then $y = z$. \end{axiom} +\begin{axiom}\label{zero_less_one} + $\zero < 1$. +\end{axiom} +\begin{axiom}\label{reals_axiom_order_def} + Suppose $x,y,z,w \in \reals$. + If $x + y < z + w$ then $x < z \lor y < w$. +\end{axiom} @@ -501,42 +508,37 @@ Such that we can introduce the integers and raitionals as smooth as possible. \subsection{The Rationals} -%\begin{definition} -% $\inv{x} -%\end{definition} -% -%\begin{axiom} -% For all $x,y \in \reals$ we have $\rfrac{x}{y} \in \reals$. -%\end{axiom} -% -%\begin{definition} -% $\rationals = \{ q \in \reals \mid \exists z \in \integers. \exists n \in \integers. q = \rfrac{z}{n} \}$. -%\end{definition} - - - - +\begin{axiom}\label{invers_reals} + For all $q \in \reals$ we have $\inv{q} \rmul q = 1$. +\end{axiom} +\begin{abbreviation}\label{rfrac} + $\rfrac{x}{y} = x \rmul \inv{y}$. +\end{abbreviation} +\begin{abbreviation}\label{naturalsplus} + $\naturalsPlus = \naturals \setminus \{\zero\}$. +\end{abbreviation} +\begin{definition}\label{rationals} + $\rationals = \{ q \in \reals \mid \exists z \in \integers. \exists n \in \naturalsPlus. q = \rfrac{z}{n} \}$. +\end{definition} -%\begin{signature}\label{invers_is_set} -% $\addInv{y}$ is a set. -%\end{signature} -%\begin{definition}\label{add_inverse} -% $\addInv{y} = \{ x \mid \exists k \in \reals. k + y = \zero \land x \in k\}$. -%\end{definition} - +\subsection{Order on the reals} -%\begin{definition}\label{add_inverse_natural_language} -% $x$ is additiv inverse of $y$ iff $x = \addInv{y}$. -%\end{definition} +\begin{lemma}\label{plus_one_order} + For all $r\in \reals$ we have $ r < r + 1$. +\end{lemma} +\begin{proof} + %Follows by \cref{reals_axiom_one,reals_axiom_order,reals_axiom_order_def,zero_less_one,reals}. +\end{proof} -%\begin{lemma}\label{rminus} -% $x \rminus \addInv{x} = \zero$. -%\end{lemma} +\begin{lemma}\label{negation_and_order} + Suppose $r \in \reals$. + $r \leq \zero$ iff $\zero \leq \neg{r}$. +\end{lemma} @@ -546,7 +548,7 @@ Such that we can introduce the integers and raitionals as smooth as possible. Then $x + y$ is positiv. \end{lemma} \begin{proof} - Omitted. + \end{proof} \begin{lemma}\label{reals_mul_of_positiv} @@ -688,6 +690,6 @@ Such that we can introduce the integers and raitionals as smooth as possible. -\begin{proposition}\label{safe} - Contradiction. -\end{proposition} +%\begin{proposition}\label{safe} +% Contradiction. +%\end{proposition} diff --git a/source/Syntax/Lexicon.hs b/source/Syntax/Lexicon.hs index 65072ee..de6d966 100644 --- a/source/Syntax/Lexicon.hs +++ b/source/Syntax/Lexicon.hs @@ -111,6 +111,7 @@ prefixOps = , ([Just (Command "snd"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "snd")) , ([Just (Command "pow"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "pow")) , ([Just (Command "neg"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "neg")) + , ([Just (Command "inv"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "inv")) , (ConsSymbol, (NonAssoc, "cons")) , (PairSymbol, (NonAssoc, "pair")) -- NOTE Is now defined and hence no longer necessary , (ApplySymbol, (NonAssoc, "apply")) -- cgit v1.2.3 From c4894bc4e788fae079b76b824a8d86c167098cc8 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Mon, 12 Aug 2024 00:12:07 +0200 Subject: more more way more urysohn --- library/topology/urysohn.tex | 127 ++++++++++++++++++++++++++++++++++++++++--- source/Api.hs | 8 +-- source/CommandLine.hs | 5 +- source/Syntax/Lexicon.hs | 1 + 4 files changed, 127 insertions(+), 14 deletions(-) (limited to 'source/Syntax/Lexicon.hs') diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex index f34f12f..6662706 100644 --- a/library/topology/urysohn.tex +++ b/library/topology/urysohn.tex @@ -36,7 +36,12 @@ The first tept will be a formalisation of chain constructions. - +%%----------------------- +% Idea: +% A sequence could be define as a family of sets, +% together with the existence of an indexing function. +% +%%----------------------- \begin{struct}\label{sequence} A sequence $X$ is a onesorted structure equipped with \begin{enumerate} @@ -148,8 +153,9 @@ The first tept will be a formalisation of chain constructions. \end{definition} \begin{definition}\label{refinmant} - $C'$ is a refinmant of $C$ iff for all $x \in C$ we have $x \in C'$ and - for all $y \in C$ such that $y \subset x$ we have there exist $c \in C'$ such that $y \subset c \subset x$ + $C'$ is a refinmant of $C$ iff $C'$ is a urysohnchain in $X$ + and for all $x \in C$ we have $x \in C'$ + and for all $y \in C$ such that $y \subset x$ we have there exist $c \in C'$ such that $y \subset c \subset x$ and for all $g \in C'$ such that $g \neq c$ we have not $y \subset g \subset x$. \end{definition} @@ -312,9 +318,9 @@ The first tept will be a formalisation of chain constructions. % U = ( A_{0}, A_{1}, A_{2}, ... , A_{n-1}, A_{n}) % U' = ( A_{0}, A'_{1}, A_{1}, A'_{2}, A_{2}, ... A_{n-1}, A'_{n}, A_{n}) - Let $m = \max{\indexset[U]}$. - For all $n \in (\indexset[U] \setminus \{m\})$ we have there exist $C \subseteq X$ - such that $\closure{\index[U](n)}{X} \subseteq \interior{C}{X} \subseteq \closure{C}{X} \subseteq \interior{\index[U](n+1)}{X}$. + % Let $m = \max{\indexset[U]}$. + % For all $n \in (\indexset[U] \setminus \{m\})$ we have there exist $C \subseteq X$ + % such that $\closure{\index[U](n)}{X} \subseteq \interior{C}{X} \subseteq \closure{C}{X} \subseteq \interior{\index[U](n+1)}{X}$. %\begin{definition}\label{refinmant} @@ -347,6 +353,58 @@ The first tept will be a formalisation of chain constructions. + +\begin{abbreviation}\label{sequence_of_functions} + $f$ is a sequence of functions iff $f$ is a sequence + and for all $g \in \carrier[f]$ we have $g$ is a function. +\end{abbreviation} + +\begin{abbreviation}\label{sequence_in_reals} + $s$ is a sequence of real numbers iff $s$ is a sequence + and for all $r \in \carrier[s]$ we have $r \in \reals$. +\end{abbreviation} + + + +\begin{axiom}\label{abs_behavior1} + If $x \geq \zero$ then $\abs{x} = x$. +\end{axiom} + +\begin{axiom}\label{abs_behavior2} + If $x < \zero$ then $\abs{x} = \neg{x}$. +\end{axiom} + +\begin{abbreviation}\label{converge} + $s$ converges iff $s$ is a sequence of real numbers + and $\indexset[s]$ is infinite + and for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have + there exist $N \in \indexset[s]$ such that + for all $m \in \indexset[s]$ such that $m > N$ + we have $\abs{\index[s](N) - \index[s](m)} < \epsilon$. +\end{abbreviation} + + +\begin{definition}\label{limit_of_sequence} + $x$ is the limit of $s$ iff $s$ is a sequence of real numbers + and $x \in \reals$ and + for all $\epsilon \in \reals$ such that $\epsilon > \zero$ + we have there exist $n \in \indexset[s]$ such that + for all $m \in \indexset[s]$ such that $m > n$ + we have $\abs{x - \index[s](n)} < \epsilon$. +\end{definition} + +\begin{proposition}\label{existence_of_limit} + Let $s$ be a sequence of real numbers. + Then $s$ converges iff there exist $x \in \reals$ + such that $x$ is the limit of $s$. +\end{proposition} +\begin{proof} + Omitted. +\end{proof} + + + + \begin{theorem}\label{urysohn} Let $X$ be a urysohn space. Suppose $A,B \in \closeds{X}$. @@ -381,12 +439,65 @@ The first tept will be a formalisation of chain constructions. We show that for all $n \in \indexset[\zeta]$ we have $\index[\zeta](n)$ has cardinality $\pot(n)$. \begin{subproof} - Trivial. + Omitted. \end{subproof} - + For all $m \in \indexset[\zeta]$ we have $\pot(m) \neq \zero$. + %%------------- Maybe use Abstrect.hs line 368 "Local Function". + + We show that for all $m \in \indexset[\zeta]$ we have there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ + and for all $n \in \indexset[\index[\zeta](m)]$ we have for all $x \in \index[\index[\zeta](m)](n)$ + we have $f(x) = \rfrac{n}{\pot(m)}$. + \begin{subproof} + % Fix $m \in \indexset[\zeta]$. + % $\index[\zeta](m)$ is a urysohnchain in $X$. + % + % Follows by \cref{existence_of_staircase_function}. + + Omitted. + \end{subproof} + + + + %The sequenc of the functions + Let $\gamma = \{ + (n,f) \mid + n \in \naturals \mid + + \forall n' \in \indexset[\index[\zeta](n)]. + \forall x \in \carrier[X]. + + + f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}} \land + + + % (n,f) \in \gamma <=> \phi(n,f) + % with \phi (n,f) := (x \in (A_k) \ (A_k-1)) => f(x) = ( k / 2^n ) + % \/ (x \notin A_k for all k \in {1,..,n} => f(x) = 1 + + ( (n' = \zero) + \land (x \in \index[\index[\zeta](n)](n')) + \land (f(x)= \zero) ) + + \lor + + ( (n' > \zero) + \land (x \in \index[\index[\zeta](n)](n')) + \land (x \notin \index[\index[\zeta](n)](n'-1)) + \land (f(x) = \rfrac{n'}{\pot(n)}) ) + + \lor + + ( (x \notin \index[\index[\zeta](n)](n')) + \land (f(x) = 1) ) + + \}$. + + + + %Suppose $\eta$ is a urysohnchain in $X$. %Suppose $\carrier[\eta] =\{A, (X \setminus B)\}$ diff --git a/source/Api.hs b/source/Api.hs index f597153..3fb0ca2 100644 --- a/source/Api.hs +++ b/source/Api.hs @@ -292,10 +292,10 @@ exportMegalodon file = do -- | This could be expandend with the dump case, with dump off just this and if dump is on it could show the number off the task. For quick use showFailedTask :: (a, ProverAnswer) -> IO() showFailedTask (_, Yes ) = Text.putStrLn "" -showFailedTask (_, No tptp) = Text.putStrLn (Text.pack ("Prover found countermodel: " ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp))))) -showFailedTask (_, ContradictoryAxioms tptp) = Text.putStrLn (Text.pack ("Contradictory axioms: " ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp))))) -showFailedTask (_, Uncertain tptp) = Text.putStrLn (Text.pack ("Out of resources: " ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp))))) -showFailedTask (_, Error _ tptp _) = Text.putStrLn (Text.pack ("Error at: " ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp))))) +showFailedTask (_, No tptp) = Text.putStrLn (Text.pack ("\ESC[31mProver found countermodel: \ESC[0m" ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp))))) +showFailedTask (_, ContradictoryAxioms tptp) = Text.putStrLn (Text.pack ("\ESC[31mContradictory axioms: \ESC[0m" ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp))))) +showFailedTask (_, Uncertain tptp) = Text.putStrLn (Text.pack ("\ESC[31mOut of resources: \ESC[0m" ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp))))) +showFailedTask (_, Error _ tptp _) = Text.putStrLn (Text.pack ("\ESC[31mError at: \ESC[0m" ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp))))) --showFailedTask (_, _) = Text.putStrLn "Error!" diff --git a/source/CommandLine.hs b/source/CommandLine.hs index 47efe22..711f7f0 100644 --- a/source/CommandLine.hs +++ b/source/CommandLine.hs @@ -87,15 +87,16 @@ run = do Text.hPutStrLn stderr tptp Error err tptp task -> do putStr "Error at:" + Text.putStrLn task Text.putStrLn err Text.putStrLn tptp WithFailList -> liftIO case result of - VerificationSuccess -> putStrLn "Verification successful." + VerificationSuccess -> putStrLn "\ESC[32mVerification successful.\ESC[0m" VerificationFailure [] -> error "Empty verification fail" VerificationFailure fails -> do - putStrLn "Following task couldn't be solved by the ATP: " + putStrLn "\ESC[35mFollowing task couldn't be solved by the ATP: \ESC[0m" traverse_ showFailedTask fails Text.hPutStrLn stderr "Don't give up!" diff --git a/source/Syntax/Lexicon.hs b/source/Syntax/Lexicon.hs index de6d966..4fe8730 100644 --- a/source/Syntax/Lexicon.hs +++ b/source/Syntax/Lexicon.hs @@ -112,6 +112,7 @@ prefixOps = , ([Just (Command "pow"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "pow")) , ([Just (Command "neg"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "neg")) , ([Just (Command "inv"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "inv")) + , ([Just (Command "abs"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "abs")) , (ConsSymbol, (NonAssoc, "cons")) , (PairSymbol, (NonAssoc, "pair")) -- NOTE Is now defined and hence no longer necessary , (ApplySymbol, (NonAssoc, "apply")) -- cgit v1.2.3