From 6129ebdf0d8549f3e4d23aa771f2c06020182b7e Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Wed, 7 Aug 2024 15:28:45 +0200 Subject: Created first urysohn formalization --- source/CommandLine.hs | 60 +++++++++++++++++++++++++++++++++++---------------- 1 file changed, 42 insertions(+), 18 deletions(-) (limited to 'source/CommandLine.hs') diff --git a/source/CommandLine.hs b/source/CommandLine.hs index a9fb00d..47efe22 100644 --- a/source/CommandLine.hs +++ b/source/CommandLine.hs @@ -18,7 +18,7 @@ import UnliftIO import UnliftIO.Directory import UnliftIO.Environment (lookupEnv) import System.FilePath.Posix - +import qualified Tptp.UnsortedFirstOrder as Syntax.Internal runCommandLine :: IO () runCommandLine = do @@ -69,23 +69,42 @@ run = do WithDefaultProver -> Provers.vampire vampirePathPath let proverInstance = prover Provers.Silent (withTimeLimit opts) (withMemoryLimit opts) result <- verify proverInstance (inputPath opts) - liftIO case result of - VerificationSuccess -> (Text.putStrLn "Verification successful.") - VerificationFailure [] -> error "Empty verification fail" - VerificationFailure ((_, proverAnswer) : _) -> case proverAnswer of - Yes -> - skip - No tptp -> do - putStrLn "Verification failed: prover found countermodel" - Text.hPutStrLn stderr tptp - ContradictoryAxioms tptp -> do - putStrLn "Verification failed: contradictory axioms" - Text.hPutStrLn stderr tptp - Uncertain tptp -> do - putStrLn "Verification failed: out of resources" - Text.hPutStrLn stderr tptp - Error err -> - Text.hPutStrLn stderr err + case withFailList opts of + WithoutFailList -> liftIO case result of + VerificationSuccess -> putStrLn "Verification successful." + VerificationFailure [] -> error "Empty verification fail" + VerificationFailure ((_, proverAnswer) : _) -> case proverAnswer of + Yes -> + skip + No tptp -> do + putStrLn "Verification failed: prover found countermodel" + Text.hPutStrLn stderr tptp + ContradictoryAxioms tptp -> do + putStrLn "Verification failed: contradictory axioms" + Text.hPutStrLn stderr tptp + Uncertain tptp -> do + putStrLn "Verification failed: out of resources" + 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." + VerificationFailure [] -> error "Empty verification fail" + VerificationFailure fails -> do + putStrLn "Following task couldn't be solved by the ATP: " + traverse_ showFailedTask fails + Text.hPutStrLn stderr "Don't give up!" + + + + + + + @@ -104,6 +123,7 @@ parseOptions = do withVersion <- withVersionParser withMegalodon <- withMegalodonParser withDumpPremselTraining <- withDumpPremselTrainingParser + withFailList <- withFailListParser pure Options{..} withTimeLimitParser :: Parser Provers.TimeLimit @@ -160,3 +180,7 @@ withDumpPremselTrainingParser = flag' WithDumpPremselTraining (long "premseldump withMegalodonParser :: Parser WithMegalodon withMegalodonParser = flag' WithMegalodon (long "megalodon" <> help "Export to Megalodon.") <|> pure WithoutMegalodon -- Default to using the cache. + +withFailListParser :: Parser WithFailList +withFailListParser = flag' WithFailList (long "list_fails" <> help "Will list all unproven task with possible reason of failure.") + <|> pure WithoutFailList -- Default to using the cache. \ No newline at end of file -- 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/CommandLine.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 From b51f61e6be5be4729e61ede79fb0bd3cb26f57a6 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Mon, 12 Aug 2024 14:41:32 +0200 Subject: way way more urysohn --- library/topology/urysohn.tex | 82 +++++++++++++++++++++++--------------------- source/CommandLine.hs | 3 ++ 2 files changed, 45 insertions(+), 40 deletions(-) (limited to 'source/CommandLine.hs') diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex index d8b1e14..414043f 100644 --- a/library/topology/urysohn.tex +++ b/library/topology/urysohn.tex @@ -526,6 +526,11 @@ The first tept will be a formalisation of chain constructions. Omitted. \end{subproof} + We show that for all $n \in \naturals$ for all $x \in \carrier[X]$ we have $\apply{\gamma(n)}{x} \in \intervalclosed{\zero}{1}$. + \begin{subproof} + Omitted. + \end{subproof} + We show that there exist $g$ such that @@ -535,18 +540,7 @@ The first tept will be a formalisation of chain constructions. there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(n)}{x} - k} < \epsilon$ and $g(x)= k$. - \begin{subproof} - - %Let $G(x) = \{k \in \carrier[X] \mid \forall \epsilon \in \realsplus. \exists N \in \naturals. \forall N' \in \naturals. (N' > N) \land (\abs{\apply{\gamma(n)}{x} - k} < \epsilon)\}$ for $x \in \carrier[X]$. -% - %We show that for all $x \in \carrier[X]$ we have $G(x)$ has cardinality $1$. - %\begin{subproof} - % Omitted. - %\end{subproof} -% - %Let $H(x) = \unions{G(x)}$ for $x \in \carrier[X]$. - %For all $x \in \carrier[X]$ we have $\{H(x)\} = G(x)$. - + \begin{subproof} We show that for all $x \in \carrier[X]$ we have there exist $k \in \reals$ such that for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have @@ -554,10 +548,9 @@ The first tept will be a formalisation of chain constructions. for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(n)}{x} - k} < \epsilon$. \begin{subproof} - Omitted. + Fix $x \in \carrier[X]$. + Follows by \cref{two_in_naturals,function_apply_default,reals_axiom_zero_in_reals,dom_emptyset,notin_emptyset,funs_type_apply,neg,minus,abs_behavior1}. \end{subproof} - - \end{subproof} @@ -581,44 +574,53 @@ The first tept will be a formalisation of chain constructions. %\begin{subproof} % Omitted. %\end{subproof} + + Let $G(x) = g(x)$ for $x \in \carrier[X]$. + We have $\dom{G} = \carrier[X]$. - - We show that $F \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$. - \begin{subproof} + %For all $x \in \carrier[X]$ for all $n \in \naturals$ we have $g(x) \leq \apply{\gamma(n)}{x}$. + + We show that for all $x \in \dom{G}$ we have $G(x) \in \reals$. + \begin{subproof} + Fix $x \in \dom{G}$. + It suffices to show that $g(x) \in \reals$. + + %There exist $k \in \reals$ such that for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(n)}{x} - k} < \epsilon$ and $g(x)= k$. + + + + \end{subproof} + + We show that for all $x \in \dom{G}$ we have $\zero \leq G(x) \leq 1$. + \begin{subproof} Omitted. - - %It suffices to show that $\dom{F} = \carrier[X]$ and - %$F \in \rels{\carrier[X]}{\intervalclosed{\zero}{1}}$ and $F$ is right-unique. - % - %We show that $F \in \rels{\carrier[X]}{\intervalclosed{\zero}{1}}$. - %\begin{subproof} - % It suffices to show that $F \in \pow{\carrier[X] \times \intervalclosed{\zero}{1}}$. - % It suffices to show that for all $w \in F$ we have $w \in (\carrier[X] \times \intervalclosed{\zero}{1})$. -% - % Fix $w \in F$. -% - % %Take $x$ such that there exist $k \in \intervalclosed{\zero}{1}$ such that $w = (x,k)$. -% -% - %\end{subproof} - % -% -% - %Trivial. \end{subproof} - We show that $F(A) = \zero$. + + We show that $G \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$. + \begin{subproof} + It suffices to show that $\ran{G} \subseteq \intervalclosed{\zero}{1}$ by \cref{fun_ran_iff,funs_intro,funs_weaken_codom}. + It suffices to show that for all $x \in \dom{G}$ we have $G(x) \in \intervalclosed{\zero}{1}$. + Fix $x \in \dom{G}$. + Then $x \in \carrier[X]$. + $g(x) = G(x)$. + We have $G(x) \in \reals$. + $\zero \leq G(x) \leq 1$. + We have $G(x) \in \intervalclosed{\zero}{1}$ . + \end{subproof} + + We show that $G(A) = \zero$. \begin{subproof} Omitted. \end{subproof} - We show that $F(B) = 1$. + We show that $G(B) = 1$. \begin{subproof} Omitted. \end{subproof} - We show that $F$ is continuous. + We show that $G$ is continuous. \begin{subproof} Omitted. \end{subproof} diff --git a/source/CommandLine.hs b/source/CommandLine.hs index 711f7f0..b8c170e 100644 --- a/source/CommandLine.hs +++ b/source/CommandLine.hs @@ -43,10 +43,12 @@ run = do case withDump opts of WithoutDump -> skip WithDump dir -> do + liftIO (Text.putStrLn "\ESC[1;36mCreating Dumpfiles.\ESC[0m") let serials = [dir show n <.> "p" | n :: Int <- [1..]] tasks <- zip serials <$> encodeTasks (inputPath opts) createDirectoryIfMissing True dir forM_ tasks (uncurry dumpTask) + liftIO (Text.putStrLn "\ESC[35mDump ready.\ESC[0m") case (withParseOnly opts, withMegalodon opts) of (WithParseOnly, _) -> do ast <- parse (inputPath opts) @@ -60,6 +62,7 @@ run = do -- A custom E executable can be configured using environment variables. -- If the environment variable is undefined we fall back to the -- a globally installed E executable. + liftIO (Text.putStrLn "\ESC[1;96mStart of verification.\ESC[0m") vampirePathPath <- (?? "vampire") <$> lookupEnv "NAPROCHE_VAMPIRE" eproverPath <- (?? "eprover") <$> lookupEnv "NAPROCHE_EPROVER" let prover = case withProver opts of -- cgit v1.2.3