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. --- source/Syntax/Lexicon.hs | 1 + 1 file changed, 1 insertion(+) (limited to 'source') 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') 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 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 --- library/numbers.tex | 131 ++++++++++--------- library/topology/continuous.tex | 14 +- library/topology/urysohn.tex | 274 ++++++++++++++++++++++++++++++++++++++++ source/Api.hs | 17 +++ source/CommandLine.hs | 60 ++++++--- source/Provers.hs | 4 +- source/Test/Golden.hs | 1 + 7 files changed, 422 insertions(+), 79 deletions(-) create mode 100644 library/topology/urysohn.tex (limited to 'source') diff --git a/library/numbers.tex b/library/numbers.tex index 0bfae2d..7d1b058 100644 --- a/library/numbers.tex +++ b/library/numbers.tex @@ -348,6 +348,9 @@ 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. + + +The operations Multiplication and addition is closed in the reals \begin{axiom}\label{reals_rmul} For all $n,m \in \reals$ we have $(n \rmul m) \in \reals$. \end{axiom} @@ -358,10 +361,16 @@ Such that we can introduce the integers and raitionals as smooth as possible. + +Commutivatiy of the standart operations \begin{axiom}\label{reals_axiom_kommu} For all $x,y \in \reals$ $x + y = y + x$ and $x \rmul y = y \rmul x$. \end{axiom} + + + +Existence of one and Zero \begin{axiom}\label{reals_axiom_zero} For all $x \in \reals$ $x + \zero = x$. \end{axiom} @@ -370,6 +379,9 @@ Such that we can introduce the integers and raitionals as smooth as possible. For all $x \in \reals$ we have $x \rmul 1 = x$. \end{axiom} + + +The Existence of Inverse of both operations \begin{axiom}\label{reals_axiom_add_invers} For all $x \in \reals$ there exist $y \in \reals$ such that $x + y = \zero$. \end{axiom} @@ -378,6 +390,9 @@ Such that we can introduce the integers and raitionals as smooth as possible. For all $x \in \reals$ such that $x \neq \zero$ there exist $y \in \reals$ such that $x \rmul y = 1$. \end{axiom} + + +Disstrubitiv Laws of the reals \begin{axiom}\label{reals_axiom_disstro1} For all $x,y,z \in \reals$ $x \rmul (y + z) = (x \rmul y) + (x \rmul z)$. \end{axiom} @@ -386,10 +401,9 @@ Such that we can introduce the integers and raitionals as smooth as possible. For all $x,y,z \in \reals$ $(y + z) \rmul x = (y \rmul x) + (z \rmul x)$. \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} + +Definition of the order symbols \begin{abbreviation}\label{rless} $x < y$ iff $x \rless y$. \end{abbreviation} @@ -406,50 +420,50 @@ Such that we can introduce the integers and raitionals as smooth as possible. $x \geq y$ iff it is wrong that $x < y$. \end{abbreviation} + + +Laws of the order on the reals \begin{abbreviation}\label{is_positiv} $x$ is positiv iff $x > \zero$. \end{abbreviation} - - - - -\begin{axiom}\label{tarski1} +\begin{axiom}\label{reals_order} For all $x,y \in \reals$ we have if $x < y$ then $\lnot y < x$. \end{axiom} -\begin{axiom}\label{tarski2} +\begin{axiom}\label{reals_dense} For all $x,y \in \reals$ if $x < y$ then there exist $z \in \reals$ such that $x < z$ and $z < y$. \end{axiom} -\begin{axiom}\label{tarski3} +\begin{axiom}\label{reals_is_eta_zero_set} For all $X,Y,x,y$ such that $X,Y \subseteq \reals$ and $x \in X$ and $y \in Y$ and $x < y$ we have there exist $z \in \reals$ such that $x < z < y$. \end{axiom} -\begin{axiom}\label{tarski4} - For all $x,y,z \in \reals$ $(x + y) + z = x + (y + z)$ and $(x \rmul y) \rmul z = x \rmul (y \rmul z)$. +\begin{axiom}\label{reals_one_bigger_zero} + $\zero < 1$. \end{axiom} -\begin{axiom}\label{tarski5} - For all $x,y \in \reals$ we have there exist $z \in \reals$ such that $x + z = y$. +\begin{axiom}\label{reals_order_behavior_with_addition} + For all $x,y \in \reals$ such that $x < y$ we have for all $z \in \reals$ $x + z < y + z$. \end{axiom} - -\begin{axiom}\label{tarski8} - $\zero < 1$. +\begin{axiom}\label{reals_postiv_mul_is_positiv} + For all $x,y \in \reals$ such that $\zero < x,y$ we have $\zero < (x \rmul y)$. \end{axiom} -\begin{axiom}\label{labelordersossss} - For all $x,y \in \reals$ such that $x < y$ we have for all $z \in \reals$ $x + z < y + z$. +\begin{axiom}\label{reals_postiv_mul_negativ_is_negativ} + For all $x,y \in \reals$ such that $x < \zero < y$ we have $(x \rmul y) < \zero$. \end{axiom} -\begin{axiom}\label{nocheinschoeneslabel} - For all $x,y \in \reals$ such that $\zero < x,y$ we have $\zero < (x \rmul y)$. +\begin{axiom}\label{reals_negativ_mul_is_negativ} + For all $x,y \in \reals$ such that $x,y < \zero$ we have $\zero < (x \rmul y)$. \end{axiom} + + \subsection{The Intergers} @@ -480,10 +494,11 @@ Such that we can introduce the integers and raitionals as smooth as possible. For all $r \in \reals$ we have $\neg{\neg{r}} = r$. \end{proposition} \begin{proof} - 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}. + Omitted. +% Fix $r \in \reals$. +% $r + \neg{r} = \zero$. +% $\neg{r} + \neg{\neg{r}} = \zero$. +% Follows by \cref{neg,reals_axiom_kommu}. \end{proof} \begin{definition}\label{integers} @@ -511,22 +526,6 @@ Such that we can introduce the integers and raitionals as smooth as possible. -\begin{proposition}\label{integers_negativ_times_negativ_is_positiv} - Suppose $n,m \in \integers$. - Suppose $n < \zero$ and $m < \zero$. - Then $n \rmul m > \zero$. -\end{proposition} -\begin{proof} - Omitted. - %$n \neq \zero$ and $m \neq \zero$. - %For all $k \in \naturals$ we have $k = \zero \lor k > \zero$. - %There exists $n' \in \reals$ such that $n' + n = \zero$. - %There exists $m' \in \reals$ such that $m' + m = \zero$. -\end{proof} - -%TODO: negativ * negativ = positiv. - - \subsection{The Rationals} \begin{axiom}\label{invers_reals} @@ -542,7 +541,7 @@ Such that we can introduce the integers and raitionals as smooth as possible. \end{abbreviation} \begin{definition}\label{rationals} %TODO: Vielleicht ist hier die definition das alle inversen von den ganzenzahlen und die ganzenzahlen selbst die rationalen zahlen erzeugen - $\rationals = \{ q \in \reals \mid \exists z \in \integers. \exists n \in \naturalsPlus. q = \rfrac{z}{n} \}$. + $\rationals = \{ q \in \reals \mid \exists z \in \integers. \exists n \in (\integers \setminus \{\zero\}). q = \rfrac{z}{n} \}$. \end{definition} \begin{abbreviation}\label{nominator} @@ -553,23 +552,41 @@ Such that we can introduce the integers and raitionals as smooth as possible. $n$ is denominator of $q$ iff there exists $z \in \integers$ such that $q = \rfrac{z}{n}$. \end{abbreviation} -%\begin{proposition}\label{q_is_less_then_p_if_denominator_is_bigger_and_nominator_is_equal} -% Suppose $p,q \in \rationals$. -% Suppose $z \in \naturals$. -% Suppose $p$ is positiv. -% Suppose $q$ is positiv. -% Suppose $z$ is nominator of $p$. -% Suppose $z$ is nominator of $p$. -% Suppose $p'$ is denominator of $p$. -% Suppose $q'$ is denominator of $q$. -% Then $p \leq q$ iff $p' \geq q'$. -%\end{proposition} +\begin{theorem}\label{one_divided_by_n_is_in_zero_to_one} + For all $n \in \naturalsPlus$ we have $\zero < \rfrac{1}{n} \leq 1$. +\end{theorem} +\begin{proof} + Omitted. +\end{proof} +\begin{lemma}\label{fraction_kuerzung} %TODO: Englischen namen rausfinden + For all $n,m,k \in \reals$ we have $\rfrac{n \rmul k}{m \rmul k} = \rfrac{n}{m}$. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} -%\begin{theorem}\label{one_divided_by_n_is_in_zero_to_one} -% For all $n \in \naturalsPlus$ we have $\zero < \rfrac{1}{n} \leq 1$. -%\end{theorem} +\begin{lemma}\label{fraction_swap} + For all $n,m,k,l \in \reals$ we have $\rfrac{\rfrac{n}{m}}{\rfrac{k}{l}}=\rfrac{n \rmul l}{m \rmul k}$. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} +\begin{definition}\label{divisor} + $g$ is a integral divisor of $a$ iff $g \in \naturals$ and there exist $b \in \integers$ such that $g \rmul b = a$. +\end{definition} + + + + +%\begin{abbreviation}\label{gcd} +% $g$ is greatest common divisor of $\{a,b\}$ iff +% $g$ is a integral divisor of $a$ +% and $g$ is a integral divisor of $b$ +% and for all $g'$ such that $g'$ is a integral divisor of $a$ +% and $g'$ is a integral divisor of $b$ we have $g' \leq g$. +%\end{abbreviation} % TODO: Was man noch so beweisen könnte: bruch kürzung, kehrbruch eigenschaften, bruch in bruch vereinfachung, @@ -652,7 +669,7 @@ Such that we can introduce the integers and raitionals as smooth as possible. \begin{lemma}\label{order_reals_lemma3} Let $x,y,z \in \reals$. - Suppose $\zero < x$. + Suppose $\zero > x$. Suppose $y < z$. Then $(x \rmul z) < (x \rmul y)$. \end{lemma} diff --git a/library/topology/continuous.tex b/library/topology/continuous.tex index 6a32353..a9bc58e 100644 --- a/library/topology/continuous.tex +++ b/library/topology/continuous.tex @@ -1,5 +1,7 @@ \import{topology/topological-space.tex} \import{relation.tex} +\import{function.tex} +\import{set.tex} \begin{definition}\label{continuous} $f$ is continuous iff for all $U \in \opens[Y]$ we have $\preimg{f}{U} \in \opens[X]$. @@ -8,18 +10,25 @@ \begin{proposition}\label{continuous_definition_by_closeds} Let $X$ be a topological space. Let $Y$ be a topological space. + Let $f \in \funs{X}{Y}$. Then $f$ is continuous iff for all $U \in \closeds{Y}$ we have $\preimg{f}{U} \in \closeds{X}$. \end{proposition} \begin{proof} Omitted. - %We show that if $f$ is continuous then for all $U \in \closeds{Y}$ we have $\preimg{f}{U} \in \closeds{X}$. + %We show that if $f$ is continuous then for all $U \in \closeds{Y}$ such that $U \neq \emptyset$ we have $\preimg{f}{U} \in \closeds{X}$. %\begin{subproof} % Suppose $f$ is continuous. % Fix $U \in \closeds{Y}$. % $\carrier[Y] \setminus U$ is open in $Y$. % Then $\preimg{f}{(\carrier[Y] \setminus U)}$ is open in $X$. % Therefore $\carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)}$ is closed in $X$. - % $\carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)} \subseteq \preimg{f}{U}$. + % We show that $\carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)} \subseteq \preimg{f}{U}$. + % \begin{subproof} + % It suffices to show that for all $x \in \carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)}$ we have $x \in \preimg{f}{U}$. + % Fix $x \in \carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)}$. + % Take $y \in \carrier[Y]$ such that $f(x)=y$. + % It suffices to show that $y \in U$. + % \end{subproof} % $\preimg{f}{U} \subseteq \carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)}$. %\end{subproof} %We show that if for all $U \in \closeds{Y}$ we have $\preimg{f}{U} \in \closeds{X}$ then $f$ is continuous. @@ -27,3 +36,4 @@ % Omitted. %\end{subproof} \end{proof} + diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex new file mode 100644 index 0000000..65457ea --- /dev/null +++ b/library/topology/urysohn.tex @@ -0,0 +1,274 @@ +\import{topology/topological-space.tex} +\import{topology/separation.tex} +\import{topology/continuous.tex} +\import{numbers.tex} +\import{function.tex} +\import{set.tex} +\import{cardinal.tex} + +\section{Urysohns Lemma} +% In this section we want to proof Urysohns lemma. +% We try to follow the proof of Klaus Jänich in his book. TODO: Book reference +% The Idea is to construct staircase functions as a chain. +% The limit of our chain turns out to be our desired continuous function from a topological space $X$ to $[0,1]$. +% With the property that \[f\mid_{A}=1 \land f\mid_{B}=0\] for \[A,B\] closed sets. + +%Chains of sets. + +The first tept will be a formalisation of chain constructions. + +\subsection{Chains of sets} +% Assume $A,B$ are subsets of a topological space $X$. + +% As Jänich propose we want a special property on chains of subsets. +% We need a rising chain of subsets $\mathfrak{A} = (A_{0}, ... ,A_{r})$ of $A$, i.e. +% \begin{align} +% A = A_{0} \subset A_{1} \subset ... \subset A_{r} \subset X\setminus B +% \end{align} +% such that for all elements in this chain following holds, +% $\overline{A_{i-1}} \subset \interior{A_{i}}$. +% In this case we call the chain legal. + +\begin{definition}\label{one_to_n_set} + $\seq{m}{n} = \{x \in \naturals \mid m \leq x \leq n\}$. +\end{definition} + +\begin{definition}\label{cardinality} + $X$ has cardinality of $n$ iff + $n \in \naturals$ and there exists $b$ such that $b$ is a bijection from $\seq{1}{n}$ to $X$. +\end{definition} + + + +\begin{struct}\label{sequence} + A sequence $X$ is a onesorted structure equipped with + \begin{enumerate} + \item $\index$ + \item $\indexset$ + \end{enumerate} + such that + \begin{enumerate} + \item\label{indexset_is_subset_naturals} $\indexset[X] \subseteq \naturals$. + \item\label{index_is_bijection} $\index[X]$ is a bijection from $\indexset[X]$ to $\carrier[X]$. + \end{enumerate} +\end{struct} + +\begin{definition}\label{cahin_of_subsets} + $C$ is a chain of subsets iff + $C$ is a sequence and for all $n,m \in \indexset[C]$ such that $n < m$ we have $\index[C](n) \subseteq \index[C](m)$. +\end{definition} + +\begin{definition}\label{chain_of_n_subsets} + $C$ is a chain of $n$ subsets iff + $C$ is a chain of subsets and $n \in \indexset[C]$ + and for all $m \in \naturals$ such that $m \leq n$ we have $m \in \indexset[C]$. +\end{definition} + + + +% TODO: The Notion above should be generalised to sequences since we need them as well for our limit +% and also for the subproof of continuity of the limit. + + +% \begin{definition}\label{legal_chain} +% $C$ is a legal chain of subsets of $X$ iff +% $C \subseteq \pow{X}$. %and +% %there exist $f \in \funs{C}{\naturals}$ such that +% %for all $x,y \in C$ we have if $f(x) < f(y)$ then $x \subset y \land \closure{x} \subset \interior{y}$. +% \end{definition} + +% TODO: We need a notion for declarinf new properties to existing thing. +% +% The following gives a example and a wish want would be nice to have: +% "A (structure) is called (adjectiv of property), if" +% +% This should then be use als follows: +% Let $X$ be a (adjectiv_1) ... (adjectiv_n) (structure_word). +% Which should be translated to fol like this: +% ?[X]: is_structure(X) & is_adjectiv_1(X) & ... & is_adjectiv_n(X) +% --------------------------------------------------------------- + + + +\subsection{staircase function} + +\begin{definition}\label{intervalclosed} + $\intervalclosed{a}{b} = \{x \in \reals \mid a \leq x \leq b\}$. +\end{definition} + + +\begin{struct}\label{staircase_function} + A staircase function $f$ is a onesorted structure equipped with + \begin{enumerate} + \item $\chain$ + \end{enumerate} + such that + \begin{enumerate} + \item \label{staircase_is_function} $f$ is a function to $\intervalclosed{\zero}{1}$. + \item \label{staircase_domain} $\dom{f}$ is a topological space. + \item \label{staricase_def_chain} $C$ is a chain of subsets. + \item \label{staircase_chain_is_in_domain} for all $x \in C$ we have $x \subseteq \dom{f}$. + \item \label{staircase_behavoir_index_zero} $f(\index[C](1))= 1$. + \item \label{staircase_behavoir_index_n} $f(\dom{f}\setminus \unions{C}) = \zero$. + \end{enumerate} +\end{struct} + +\begin{definition}\label{legal_staircase} + $f$ is a legal staircase function iff + $f$ is a staircase function and + for all $n,m \in \indexset[\chain[f]]$ such that $n \leq m$ we have $f(\index[\chain[f]](n)) \leq f(\index[\chain[f]](m))$. +\end{definition} + +\begin{abbreviation}\label{urysohnspace} + $X$ is a urysohn space iff + $X$ is a topological space and + for all $A,B \in \closeds{X}$ such that $A \inter B = \emptyset$ + we have there exist $A',B' \in \opens[X]$ + such that $A \subseteq A'$ and $B \subseteq B'$ and $A' \inter B' = \emptyset$. +\end{abbreviation} + +\begin{definition}\label{urysohnchain} + $C$ is a urysohnchain in $X$ of cardinality $k$ iff %<---- TODO: cardinality unused! + $C$ is a chain of subsets and + for all $A \in C$ we have $A \subseteq X$ and + for all $n,m \in \indexset[C]$ such that $n < m$ we have $\closure{\index[C](n)}{X} \subseteq \interior{\index[C](m)}{X}$. +\end{definition} + +\begin{abbreviation}\label{infinte_sequence} + $S$ is a infinite sequence iff $S$ is a sequence and $\indexset[S]$ is infinite. +\end{abbreviation} + +\begin{definition}\label{infinite_product} + $X$ is the infinite product of $Y$ iff + $X$ is a infinite sequence and for all $i \in \indexset[X]$ we have $\index[X](i) = Y$. +\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$ + and for all $g \in C$ such that $g \neq c$ we have not $y \subset g \subset x$. +\end{definition} + + +% The next thing we need to define is the uniform staircase function. +% This function has it's domain in $X$ and maps to the closed interval $[0,1]$. +% These functions should behave als follows, +% \begin{align} +% &f(A_{0}) = 1 &\text{consant} \\ +% &f(A_{k} \setminus A_{k+1}) = 1-\frac{k}{r} &\text{constant.} +% \end{align} + +% We then prove that for any given $r$ we find a repolished chain, +% which contains the $A_{i}$ and this replished chain is also legal. +% +% The proof will be finished by taking the limit on $f_{n}$ with $f_{n}$ +% be a staircase function with $n$ many refinemants. +% This limit will be continuous and we would be done. + + +% TODO: Since we want to prove that $f$ is continus, we have to formalize that +% \reals with the usual topology is a topological space. +% ------------------------------------------------------------- + +\begin{theorem}\label{urysohn} + Let $X$ be a urysohn space. + Suppose $A,B \subseteq \closeds{X}$. + Suppose $A \inter B$ is empty. + There exist $f$ such that $f \in \funs{X}{\intervalclosed{\zero}{1}}$ + and $f(A) = 1$ and $f(B)= 0$ and $f$ is continuous. +\end{theorem} +\begin{proof} + We show that for all $n \in \naturals$ we have + if there exist $C$ such that $C$ is a urysohnchain in $X$ of cardinality $n$ + then there exist $C'$ such that $C'$ is a urysohnchain in $X$ of cardinality $n+1$ + and $C'$ is a refinmant of $C$. + \begin{subproof} + Omitted. + \end{subproof} + + + + Take $P$ such that $P$ is a infinite sequence and $\indexset[P] = \naturals$ and for all $i \in \indexset[P]$ we have $\index[P](i) = \pow{X}$. + + We show that there exist $\zeta$ such that $\zeta$ is a infinite sequence + and for all $i \in \indexset[\zeta]$ we have + $\index[\zeta](i)$ is a urysohnchain in $X$ of cardinality $i$ + and $A \subseteq \index[\zeta](i)$ + and $\index[\zeta](i) \subseteq (X \setminus B)$ + and for all $j \in \indexset[\zeta]$ such that + $j < i$ we have for all $x \in \index[\zeta](j)$ we have $x \in \index[\zeta](i)$. + \begin{subproof} + Omitted. + \end{subproof} + + + + + + + + + We show that there exist $g \in \funs{X}{\intervalclosed{\zero}{1}}$ such that $g(A)=1$ and $g(X\setminus A) = \zero$. + \begin{subproof} + Omitted. + \end{subproof} + $g$ is a staircase function and $\chain[g] = C$. + $g$ is a legal staircase function. + + + We show that there exist $f$ such that $f \in \funs{X}{\intervalclosed{\zero}{1}}$ + and $f(A) = 1$ and $f(B)= 0$ and $f$ is continuous. + \begin{subproof} + Omitted. + \end{subproof} + + + %We show that for all $n \in \nautrals$ we have $C_{n}$ a legal chain of subsets of $X$. + %\begin{subproof} + % Omitted. + %\end{subproof} + + %Proof Sheme Idea: + % -We proof for n=1 that C_{n} is a chain and legal + % -Then by induction with P(n+1) is refinmant of P(n) + % -Therefore we have a increing refinmant of these Chains such that our limit could even apply + % --------------------------------------------------------- + + %We show that there exist $f \in \funs{\naturals}{\funs{X}{\intervalclosed{0}{1}}}$ such that $f(n)$ is a staircase function. %TODO: Define Staircase function + %\begin{subproof} + % Omitted. + %\end{subproof} + + + % Formalization idea of enumarted sequences: + % - Define a enumarted sequnecs as a set A with a bijection between A and E \in \pow{\naturals} + % - This should give all finite and infinte enumarable sequences + % - Introduce a notion for the indexing of these enumarable sequences. + % - Then we can define the limit of a enumarted sequence of functions. + % --------------------------------------------------------- + % + % Here we need a limit definition for sequences of functions + %We show that there exist $F \in \funs{X}{\intervalclosed{0}{1}}$ such that $F = \limit{set of the staircase functions}$ + %\begin{subproof} + % Omitted. + %\end{subproof} + % + %We show that $F(A) = 1$. + %\begin{subproof} + % Omitted. + %\end{subproof} + % + %We show that $F(B) = 0$. + %\begin{subproof} + % Omitted. + %\end{subproof} + % + %We show that $F$ is continuous. + %\begin{subproof} + % Omitted. + %\end{subproof} +\end{proof} + +%\begin{theorem}\label{safe} +% Contradiction. +%\end{theorem} diff --git a/source/Api.hs b/source/Api.hs index 95d5c8c..f597153 100644 --- a/source/Api.hs +++ b/source/Api.hs @@ -17,6 +17,7 @@ module Api , dumpTask , verify, ProverAnswer(..), VerificationResult(..) , exportMegalodon + , showFailedTask , WithCache(..) , WithFilter(..) , WithOmissions(..) @@ -29,6 +30,7 @@ module Api , WithParseOnly(..) , Options(..) , WithDumpPremselTraining(..) + , WithFailList(..) ) where @@ -65,6 +67,7 @@ import Text.Megaparsec hiding (parse, Token) import UnliftIO import UnliftIO.Directory import UnliftIO.Environment +import Syntax.Abstract (Formula) -- | Follow all @\\import@ statements recursively and build a theory graph from them. -- The @\\import@ statements should be on their own separate line and precede all @@ -285,6 +288,17 @@ exportMegalodon file = do pure (Megalodon.encodeBlocks lexicon blocks) + +-- | 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 (_, _) = Text.putStrLn "Error!" + + -- | Should we use caching? data WithCache = WithoutCache | WithCache deriving (Show, Eq) @@ -312,6 +326,8 @@ pattern WithoutDump = WithDump "" data WithParseOnly = WithoutParseOnly | WithParseOnly deriving (Show, Eq) +data WithFailList = WithoutFailList | WithFailList deriving (Show, Eq) + data Options = Options { inputPath :: FilePath @@ -327,4 +343,5 @@ data Options = Options , withVersion :: WithVersion , withMegalodon :: WithMegalodon , withDumpPremselTraining :: WithDumpPremselTraining + , withFailList :: WithFailList } 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 diff --git a/source/Provers.hs b/source/Provers.hs index 203ee82..37e02ca 100644 --- a/source/Provers.hs +++ b/source/Provers.hs @@ -110,7 +110,7 @@ data ProverAnswer | No Text | ContradictoryAxioms Text | Uncertain Text - | Error Text + | Error Text Text Text deriving (Show, Eq) nominalDiffTimeToText :: NominalDiffTime -> Text @@ -163,4 +163,4 @@ recognizeAnswer Prover{..} task tptp answer answerErr = | saidNo -> No tptp | doesNotKnow -> Uncertain tptp | warned -> ContradictoryAxioms tptp - | otherwise -> Error (answer <> answerErr) + | otherwise -> Error (answer <> answerErr) tptp (Text.pack(show (taskConjectureLabel task))) diff --git a/source/Test/Golden.hs b/source/Test/Golden.hs index 705aaa5..c01c249 100644 --- a/source/Test/Golden.hs +++ b/source/Test/Golden.hs @@ -39,6 +39,7 @@ testOptions = Api.Options , withTimeLimit = Provers.defaultTimeLimit , withVersion = Api.WithoutVersion , withMegalodon = Api.WithoutMegalodon + , withFailList = Api.WithoutFailList } goldenTests :: IO TestTree -- 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') 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') 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 From 98ba67c72d4959d0a22cedfd5ac6d4b37ed47658 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Sat, 24 Aug 2024 11:44:10 +0200 Subject: Added/Fixed comments --- source/TheoryGraph.hs | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'source') diff --git a/source/TheoryGraph.hs b/source/TheoryGraph.hs index c4887ea..e49bc1f 100644 --- a/source/TheoryGraph.hs +++ b/source/TheoryGraph.hs @@ -67,12 +67,12 @@ member :: FilePath -> TheoryGraph -> Bool member n (TheoryGraph g) = Map.member n g --- | Add a node to the TheoryGraph. This is a noop if the node is already present in the graph. +-- | Add a node to the TheoryGraph. addNode :: FilePath -> TheoryGraph -> TheoryGraph addNode a (TheoryGraph g) = TheoryGraph (Map.insertWith Set.union a Set.empty g) --- | Add an edge to the TheoryGraph. This is a noop if the edge is already present in the graph. +-- | Add an edge to the TheoryGraph. This is a loop if the edge is already present in the graph. addPrecedes :: Precedes FilePath -> TheoryGraph -> TheoryGraph addPrecedes e@(Precedes _ a') (TheoryGraph g) = addNode a' (TheoryGraph (insertTail e g)) where @@ -85,7 +85,9 @@ addPrecedes e@(Precedes _ a') (TheoryGraph g) = addNode a' (TheoryGraph (insertT singleton :: FilePath -> TheoryGraph singleton a = TheoryGraph (Map.singleton a Set.empty) - +-- | Construct a graph, from a list of nodes and edges. +-- It takes all nodes a and add the pair (a, emptyset) to the Theorygraph, +-- afterwards it add all edges between the nodes. makeTheoryGraph :: [Precedes FilePath] -> [FilePath] -> TheoryGraph makeTheoryGraph es as = List.foldl' (flip addPrecedes) (TheoryGraph trivial) es where @@ -94,6 +96,8 @@ makeTheoryGraph es as = List.foldl' (flip addPrecedes) (TheoryGraph trivial) es {-# INLINE makeTheoryGraph #-} +-- | Construct a graph, from a list @x:xs@, +-- where @x@ is a pair of theorys @(a,b)@ with @a@ gets imported in @b@. fromList :: [Precedes FilePath] -> TheoryGraph fromList es = TheoryGraph (Map.fromListWith Set.union es') where -- cgit v1.2.3 From 32424a1efbd774e6beb06212dbaec6e55e92fcd5 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Sat, 24 Aug 2024 11:44:27 +0200 Subject: hlint suggestion --- source/Syntax/Adapt.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'source') diff --git a/source/Syntax/Adapt.hs b/source/Syntax/Adapt.hs index 3a8b3d6..622946a 100644 --- a/source/Syntax/Adapt.hs +++ b/source/Syntax/Adapt.hs @@ -27,7 +27,7 @@ scanChunk ltoks = matchOrErr re env pos = match re toks ?? error ("could not find lexical pattern in " <> env <> " at " <> sourcePosPretty pos) in case ltoks of Located{startPos = pos, unLocated = BeginEnv "definition"} : _ -> - matchOrErr definition "definition" (pos) + matchOrErr definition "definition" pos Located{startPos = pos, unLocated = BeginEnv "abbreviation"} : _ -> matchOrErr abbreviation "abbreviation" pos Located{startPos = pos, unLocated = (BeginEnv "struct")} :_ -> -- cgit v1.2.3 From ce03d33eaa7e9d37935f225d48459223a4004a50 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Sat, 24 Aug 2024 19:30:46 +0200 Subject: First atemped to write a new way of local function defintion --- library/wunschzettel.tex | 9 +++++++++ source/Api.hs | 4 +++- source/Syntax/Abstract.hs | 7 +++++++ source/Syntax/Adapt.hs | 14 ++++++++++++++ source/Syntax/Concrete.hs | 27 ++++++++++++++++++++++++++- source/Syntax/Concrete/Keywords.hs | 10 ++++++++-- 6 files changed, 67 insertions(+), 4 deletions(-) (limited to 'source') diff --git a/library/wunschzettel.tex b/library/wunschzettel.tex index b2681fd..74ea899 100644 --- a/library/wunschzettel.tex +++ b/library/wunschzettel.tex @@ -45,6 +45,15 @@ Tupel struct % more proof but now i can use the function f % -------------------------------------------------------- + \begin{equation} + X= + \begin{cases} + 0, & \text{if}\ a=1 \\ + 1, & \text{otherwise} + \end{cases} + \end{equation} + + \end{proof} diff --git a/source/Api.hs b/source/Api.hs index 3fb0ca2..1bdf615 100644 --- a/source/Api.hs +++ b/source/Api.hs @@ -203,7 +203,9 @@ describeToken = \case EndEnv _ -> "end of environment" _ -> "delimiter" - +-- | gloss generates internal represantation of the LaTeX files. +-- First the file will be parsed and therefore checkt for grammer. +-- 'meaning' then transfer the raw parsed grammer to the internal semantics. gloss :: MonadIO io => FilePath -> io ([Internal.Block], Lexicon) gloss file = do (blocks, lexicon) <- parse file diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs index 4aa8623..f775b69 100644 --- a/source/Syntax/Abstract.hs +++ b/source/Syntax/Abstract.hs @@ -369,6 +369,13 @@ data Proof -- ^ Local function definition, e.g. /@Let $f(x) = e$ for $x\\in d$@/. -- The first 'VarSymbol' is the newly defined symbol, the second one is the argument. -- The first 'Expr' is the value, the final variable and expr specify a bound (the domain of the function). + + + + + | DefineFunctionMathy VarSymbol VarSymbol VarSymbol [VarSymbol Expr [VarSymbol] Expr ] Proof + -- ^ Local function definition, but in this case we give the domain and target an the rules for $xs$ in some sub domains. + -- deriving (Show, Eq, Ord) -- | An inline justification. diff --git a/source/Syntax/Adapt.hs b/source/Syntax/Adapt.hs index 622946a..96fd76d 100644 --- a/source/Syntax/Adapt.hs +++ b/source/Syntax/Adapt.hs @@ -34,6 +34,8 @@ scanChunk ltoks = matchOrErr struct "struct definition" pos Located{startPos = pos, unLocated = (BeginEnv "inductive")} :_ -> matchOrErr inductive "inductive definition" pos + Located{startPos = pos, unLocated = (BeginEnv "signature")} :_ -> + matchOrErr signature "signature" pos _ -> [] adaptChunks :: [[Located Token]] -> Lexicon -> Lexicon @@ -85,6 +87,18 @@ abbreviation = do skipUntilNextLexicalEnv pure [lexicalItem m] +signatureIntro :: RE Token [ScannedLexicalItem] --since signiture is a used word of haskell we have to name it diffrentliy +signatureIntro = do + sym (BeginEnv "signature") + few notEndOfLexicalEnvToken + m <- label + few anySym + lexicalItem <- head + few anySym + sym (EndEnv "signature") + skipUntilNextLexicalEnv + pure [lexicalItem m] + label :: RE Token Marker label = msym \case Label m -> Just (Marker m) diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs index b51b738..51cc013 100644 --- a/source/Syntax/Concrete.hs +++ b/source/Syntax/Concrete.hs @@ -351,8 +351,23 @@ grammar lexicon@Lexicon{..} = mdo define <- rule $ Define <$> (_let *> beginMath *> varSymbol <* _eq) <*> expr <* endMath <* _dot <*> proof defineFunction <- rule $ DefineFunction <$> (_let *> beginMath *> varSymbol) <*> paren varSymbol <* _eq <*> expr <* endMath <* _for <* beginMath <*> varSymbol <* _in <*> expr <* endMath <* _dot <*> proof + - proof <- rule $ asum [byContradiction, byCases, bySetInduction, byOrdInduction, calc, subclaim, assume, fix, take, have, suffices, define, defineFunction, qed] + + -- Define $f $\fromTo{X}{Y} such that, + -- Define function $f: X \to Y$, + -- \begin{align} + -- &x \mapsto 3*x &, + -- &x \mapsto 4*k+x &, + -- \end{align} + -- + defineFunctionMathy <- rule $ DefineFunctionMathy + <$> (_define *> beginMath *> varSymbol) -- Define $ f + <*> _colon *> varSymbol <*> _to *> varSymbol -- : 'var' \to 'var' + <*> localFunctionDefinitionAlign + + + proof <- rule $ asum [byContradiction, byCases, bySetInduction, byOrdInduction, calc, subclaim, assume, fix, take, have, suffices, define, defineFunction, defineFunctionMathy, qed] blockAxiom <- rule $ uncurry3 BlockAxiom <$> envPos "axiom" axiom @@ -435,7 +450,17 @@ enumeratedMarked1 :: Prod r Text (Located Token) a -> Prod r Text (Located Token enumeratedMarked1 p = begin "enumerate" *> many1 ((,) <$> (command "item" *> label) <*> p) <* end "enumerate" "\"\\begin{enumerate}\\item\\label{...}...\"" +-- &x \mapsto 'someexpr' &, for x +localFunctionDefinitionAlign :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (Marker, a) +localFunctionDefinitionAlign p = begin "align" *> many1 funDefExp <* end "align" + "\"\\begin{algin} &x \\mapsto x+2 , x \\in X \\ \\end{algin}\"" + + +funDefExp :: Prod r Text (Located Token) a -> Prod r Text (Located Token) [(Marker, a)] +funDefExp p = NonEmpty.toList <$> ( _ampersand *> varSymbol <*> funDefExpRange <*> (_ampersand *> varSymbol <* _in) <*> varSymbol) -- the last var should be a expression +funDefRange :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (NonEmpty (Marker, a)) +funDefRange p = _mapsto *> varSymbol -- TODO: this Var has to be changed to a expression -- This function could be rewritten, so that it can be used directly in the grammar, -- instead of with specialized variants. diff --git a/source/Syntax/Concrete/Keywords.hs b/source/Syntax/Concrete/Keywords.hs index 135cdac..b507e7e 100644 --- a/source/Syntax/Concrete/Keywords.hs +++ b/source/Syntax/Concrete/Keywords.hs @@ -108,7 +108,7 @@ _either = word "either" ? "either" _equipped :: Prod r Text (Located Token) SourcePos _equipped = (word "equipped" <|> word "together") <* word "with" ? "equipped with" _every :: Prod r Text (Located Token) SourcePos -_every = (word "every") ? "every" +_every = word "every" ? "every" _exist :: Prod r Text (Located Token) SourcePos _exist = word "there" <* word "exist" ? "there exist" _exists :: Prod r Text (Located Token) SourcePos @@ -124,7 +124,7 @@ _for = word "for" ? "for" _forAll :: Prod r Text (Located Token) SourcePos _forAll = (word "for" <* word "all") <|> word "all" ? "all" _forEvery :: Prod r Text (Located Token) SourcePos -_forEvery = (word "for" <* word "every") <|> (word "every") ? "for every" +_forEvery = (word "for" <* word "every") <|> word "every" ? "for every" _have :: Prod r Text (Located Token) SourcePos _have = word "we" <* word "have" <* optional (word "that") ? "we have" _if :: Prod r Text (Located Token) SourcePos @@ -220,3 +220,9 @@ _in :: Prod r Text (Located Token) SourcePos _in = symbol "∈" <|> command "in" ? "\\in" _subseteq :: Prod r Text (Located Token) SourcePos _subseteq = command "subseteq" ? "\\subseteq" +_to :: Prod r Text (Located Token) SourcePos +_to = command "to" ? "\\to" +_mapsto :: Prod r Text (Located Token) SourcePos +_mapsto = command "mapsto" ? "\\mapsto" +_ampersand :: Prod r Text (Located Token) SourcePos +_ampersand = symbol "&" ? "&" \ No newline at end of file -- cgit v1.2.3 From d79c85d70fc907858e3af5715bb94e8fdc202155 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Mon, 26 Aug 2024 15:33:04 +0200 Subject: I implemented a parsing rule in concrete.hs for local functions and a abstract type in abstract.hs for the proof data structure. --- source/Syntax/Abstract.hs | 2 +- source/Syntax/Concrete.hs | 36 ++++++++++++++++++++++-------------- 2 files changed, 23 insertions(+), 15 deletions(-) (limited to 'source') diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs index f775b69..6457d42 100644 --- a/source/Syntax/Abstract.hs +++ b/source/Syntax/Abstract.hs @@ -373,7 +373,7 @@ data Proof - | DefineFunctionMathy VarSymbol VarSymbol VarSymbol [VarSymbol Expr [VarSymbol] Expr ] Proof + | DefineFunctionMathy VarSymbol VarSymbol VarSymbol VarSymbol VarSymbol (NonEmpty [(Expr, Formula)]) Proof -- ^ Local function definition, but in this case we give the domain and target an the rules for $xs$ in some sub domains. -- deriving (Show, Eq, Ord) diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs index 51cc013..f414ea6 100644 --- a/source/Syntax/Concrete.hs +++ b/source/Syntax/Concrete.hs @@ -354,17 +354,36 @@ grammar lexicon@Lexicon{..} = mdo + + + -- Define $f $\fromTo{X}{Y} such that, -- Define function $f: X \to Y$, -- \begin{align} -- &x \mapsto 3*x &, - -- &x \mapsto 4*k+x &, + -- &x \mapsto 4*k &, \forall k \in \N. x \in \Set{k} -- \end{align} -- + + -- Follwing is the definition right now. + -- Define function $f: X \to Y$ such that, + -- \begin{cases} + -- 1 & \text{if } x \in \mathbb{Q}\\ + -- 0 & \text{if } x \in \mathbb{R}\setminus\mathbb{Q} + -- 3 & \text{else} + -- \end{cases} + + functionDefineCase <- rule $ (:[]) <$> ((,) <$> expr <*> (_ampersand *> formula)) defineFunctionMathy <- rule $ DefineFunctionMathy <$> (_define *> beginMath *> varSymbol) -- Define $ f - <*> _colon *> varSymbol <*> _to *> varSymbol -- : 'var' \to 'var' - <*> localFunctionDefinitionAlign + <*> (_colon *> varSymbol) -- : 'var' \to 'var' + <*> (_to *> varSymbol <* endMath <* _suchThat) + -- <*> (_suchThat *> align (many1 ((_ampersand *> varSymbol <* _mapsto) <*> exprApp <*> (_ampersand *> formula)))) + -- <*> (_suchThat *> align (many1 (varSymbol <* exprApp <* formula))) + <*> varSymbol <*> varSymbol <* symbol "=" + <*> many1 functionDefineCase + <*> proof + proof <- rule $ asum [byContradiction, byCases, bySetInduction, byOrdInduction, calc, subclaim, assume, fix, take, have, suffices, define, defineFunction, defineFunctionMathy, qed] @@ -450,17 +469,6 @@ enumeratedMarked1 :: Prod r Text (Located Token) a -> Prod r Text (Located Token enumeratedMarked1 p = begin "enumerate" *> many1 ((,) <$> (command "item" *> label) <*> p) <* end "enumerate" "\"\\begin{enumerate}\\item\\label{...}...\"" --- &x \mapsto 'someexpr' &, for x -localFunctionDefinitionAlign :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (Marker, a) -localFunctionDefinitionAlign p = begin "align" *> many1 funDefExp <* end "align" - "\"\\begin{algin} &x \\mapsto x+2 , x \\in X \\ \\end{algin}\"" - - -funDefExp :: Prod r Text (Located Token) a -> Prod r Text (Located Token) [(Marker, a)] -funDefExp p = NonEmpty.toList <$> ( _ampersand *> varSymbol <*> funDefExpRange <*> (_ampersand *> varSymbol <* _in) <*> varSymbol) -- the last var should be a expression - -funDefRange :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (NonEmpty (Marker, a)) -funDefRange p = _mapsto *> varSymbol -- TODO: this Var has to be changed to a expression -- This function could be rewritten, so that it can be used directly in the grammar, -- instead of with specialized variants. -- cgit v1.2.3 From a253d06a0755c41dd321fc2e235c3332de63a8c7 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Mon, 26 Aug 2024 16:55:39 +0200 Subject: Non finished attemped to translate a local function defintion from abstract to internal --- source/Meaning.hs | 15 +++++++++++++++ source/Syntax/Internal.hs | 2 ++ 2 files changed, 17 insertions(+) (limited to 'source') diff --git a/source/Meaning.hs b/source/Meaning.hs index 834d8a6..30e13f8 100644 --- a/source/Meaning.hs +++ b/source/Meaning.hs @@ -605,9 +605,24 @@ glossProof = \case if domVar == argVar then Sem.DefineFunction funVar argVar <$> glossExpr valueExpr <*> glossExpr domExpr <*> glossProof proof else error "mismatched variables in function definition." + + Raw.DefineFunctionMathy funVar domVar ranVar funVar2 argVar definitions proof -> do + if funVar /= funVar2 + then error "missmatched function names" + else Sem.DefineFunctionMathy funVar domVar ranVar argVar <*> glossLocalFunctionExprEach definitions <*> glossProof proof Raw.Calc calc proof -> Sem.Calc <$> glossCalc calc <*> glossProof proof +glossLocalFunctionExprEach :: NonEmpty [(Raw.Expr, Raw.Formula)]-> Gloss [(Sem.Term, Sem.Formula)] +glossLocalFunctionExprEach def = pure ( glossLocalFunctionExpr `each` def ) + +glossLocalFunctionExpr :: (Raw.Expr, Raw.Formula) -> Gloss (Sem.Term, Sem.Formula) +glossLocalFunctionExpr (definingExpression, localDomain) = do + e <- glossExpr definingExpression + d <- glossFormula localDomain + pure (e,d) + + glossCase :: Raw.Case -> Gloss Sem.Case glossCase (Raw.Case caseOf proof) = Sem.Case <$> glossStmt caseOf <*> glossProof proof diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs index 44603ad..872ae06 100644 --- a/source/Syntax/Internal.hs +++ b/source/Syntax/Internal.hs @@ -436,6 +436,8 @@ data Proof | Define VarSymbol Term Proof | DefineFunction VarSymbol VarSymbol Term Term Proof + | DefineFunctionMathy VarSymbol VarSymbol VarSymbol VarSymbol [(Term, Formula)] Proof + deriving instance Show Proof deriving instance Eq Proof deriving instance Ord Proof -- cgit v1.2.3 From 76ea8e11d943b123d28dfbe2f354838f80fb8dba Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Mon, 26 Aug 2024 20:14:18 +0200 Subject: Implemented the checking for local functions. --- source/Checking.hs | 39 ++++++++++++++++++++++++++++++++++++++- source/Meaning.hs | 12 +++++------- source/Syntax/Abstract.hs | 2 +- source/Syntax/Adapt.hs | 2 +- source/Syntax/Concrete.hs | 2 +- source/Syntax/Internal.hs | 2 +- 6 files changed, 47 insertions(+), 12 deletions(-) (limited to 'source') diff --git a/source/Checking.hs b/source/Checking.hs index dc90264..817c477 100644 --- a/source/Checking.hs +++ b/source/Checking.hs @@ -28,6 +28,7 @@ import Data.HashSet qualified as HS import Data.InsOrdMap (InsOrdMap) import Data.InsOrdMap qualified as InsOrdMap import Data.List qualified as List +import Data.List.NonEmpty qualified as NonEmpty import Data.Set qualified as Set import Data.Text qualified as Text import Data.Text.IO qualified as Text @@ -149,7 +150,7 @@ assume asms = traverse_ go asms go :: Asm -> Checking go = \case Asm phi -> do - phi' <- (canonicalize phi) + phi' <- canonicalize phi modify \st -> st{ checkingAssumptions = phi' : checkingAssumptions st , fixedVars = freeVars phi' <> fixedVars st @@ -542,6 +543,42 @@ checkProof = \case checkCalc calc assume [Asm (calcResult calc)] checkProof continue + DefineFunctionMathy funVar domVar ranVar argVar definitions continue -> do + -- We have f: X \to Y and x \mapsto ... + -- definition is a nonempty list of (expresssion e, formula phi) + -- such that f(x) = e if phi(x) + -- since we do a case deduction in the definition there has to be a check that, + -- our domains in the case are a disjunct union of dom(f) + assume + [Asm (TermOp DomSymbol [TermVar funVar] `Equals` TermVar domVar) + ,Asm (rightUniqueAdj (TermVar funVar)) + ,Asm (relationNoun (TermVar funVar))] + + goals <- gets checkingGoals + setGoals [makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Iff` subdomainConjuctionLocalFunction argVar definitions )] -- check the disjunct union + tellTasks + + assume [Asm (makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Implies` (TermOp ApplySymbol [TermVar funVar, TermVar argVar] `IsElementOf` TermVar ranVar)))] -- function f from \dom(f) \to \ran(f) + assume (functionSubdomianExpression funVar argVar definitions) --behavior on the subdomians + setGoals goals + checkProof continue + + +-- | Makes a conjunction of all the subdomain statments +subdomainConjuctionLocalFunction :: VarSymbol -> NonEmpty (Term, Formula) -> Formula +subdomainConjuctionLocalFunction argVar defintions = + let stmts = [snd x | x <- NonEmpty.toList defintions] + in TermVar argVar `IsElementOf` makeConjunction stmts + + +functionSubdomianExpression :: VarSymbol -> VarSymbol -> NonEmpty (Term, Formula) -> [Asm] +functionSubdomianExpression f a nxs = case nxs of + x:|xs -> singleFunctionSubdomianExpression f a x : functionSubdomianExpression f a (NonEmpty.fromList xs) + + +singleFunctionSubdomianExpression :: VarSymbol -> VarSymbol -> (Term, Formula) -> Asm +singleFunctionSubdomianExpression funVar argVar x = Asm (makeForall [argVar] ((TermVar argVar `IsElementOf` snd x) `Implies` (TermOp ApplySymbol [TermVar funVar, TermVar argVar] `Equals` fst x))) + checkCalc :: Calc -> Checking checkCalc calc = locally do diff --git a/source/Meaning.hs b/source/Meaning.hs index 30e13f8..ab98c9a 100644 --- a/source/Meaning.hs +++ b/source/Meaning.hs @@ -607,17 +607,15 @@ glossProof = \case else error "mismatched variables in function definition." Raw.DefineFunctionMathy funVar domVar ranVar funVar2 argVar definitions proof -> do - if funVar /= funVar2 - then error "missmatched function names" - else Sem.DefineFunctionMathy funVar domVar ranVar argVar <*> glossLocalFunctionExprEach definitions <*> glossProof proof + if funVar == funVar2 + then Sem.DefineFunctionMathy funVar domVar ranVar argVar <$> (glossLocalFunctionExprDef `each` definitions) <*> glossProof proof + else error "missmatched function names" Raw.Calc calc proof -> Sem.Calc <$> glossCalc calc <*> glossProof proof -glossLocalFunctionExprEach :: NonEmpty [(Raw.Expr, Raw.Formula)]-> Gloss [(Sem.Term, Sem.Formula)] -glossLocalFunctionExprEach def = pure ( glossLocalFunctionExpr `each` def ) -glossLocalFunctionExpr :: (Raw.Expr, Raw.Formula) -> Gloss (Sem.Term, Sem.Formula) -glossLocalFunctionExpr (definingExpression, localDomain) = do +glossLocalFunctionExprDef :: (Raw.Expr, Raw.Formula) -> Gloss (Sem.Term, Sem.Formula) +glossLocalFunctionExprDef (definingExpression, localDomain) = do e <- glossExpr definingExpression d <- glossFormula localDomain pure (e,d) diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs index 6457d42..6372c87 100644 --- a/source/Syntax/Abstract.hs +++ b/source/Syntax/Abstract.hs @@ -373,7 +373,7 @@ data Proof - | DefineFunctionMathy VarSymbol VarSymbol VarSymbol VarSymbol VarSymbol (NonEmpty [(Expr, Formula)]) Proof + | DefineFunctionMathy VarSymbol VarSymbol VarSymbol VarSymbol VarSymbol (NonEmpty (Expr, Formula)) Proof -- ^ Local function definition, but in this case we give the domain and target an the rules for $xs$ in some sub domains. -- deriving (Show, Eq, Ord) diff --git a/source/Syntax/Adapt.hs b/source/Syntax/Adapt.hs index 96fd76d..3cff497 100644 --- a/source/Syntax/Adapt.hs +++ b/source/Syntax/Adapt.hs @@ -35,7 +35,7 @@ scanChunk ltoks = Located{startPos = pos, unLocated = (BeginEnv "inductive")} :_ -> matchOrErr inductive "inductive definition" pos Located{startPos = pos, unLocated = (BeginEnv "signature")} :_ -> - matchOrErr signature "signature" pos + matchOrErr signatureIntro "signature" pos _ -> [] adaptChunks :: [[Located Token]] -> Lexicon -> Lexicon diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs index f414ea6..69280c1 100644 --- a/source/Syntax/Concrete.hs +++ b/source/Syntax/Concrete.hs @@ -373,7 +373,7 @@ grammar lexicon@Lexicon{..} = mdo -- 3 & \text{else} -- \end{cases} - functionDefineCase <- rule $ (:[]) <$> ((,) <$> expr <*> (_ampersand *> formula)) + functionDefineCase <- rule $ (,) <$> expr <*> (_ampersand *> formula) defineFunctionMathy <- rule $ DefineFunctionMathy <$> (_define *> beginMath *> varSymbol) -- Define $ f <*> (_colon *> varSymbol) -- : 'var' \to 'var' diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs index 872ae06..0e3361d 100644 --- a/source/Syntax/Internal.hs +++ b/source/Syntax/Internal.hs @@ -436,7 +436,7 @@ data Proof | Define VarSymbol Term Proof | DefineFunction VarSymbol VarSymbol Term Term Proof - | DefineFunctionMathy VarSymbol VarSymbol VarSymbol VarSymbol [(Term, Formula)] Proof + | DefineFunctionMathy VarSymbol VarSymbol VarSymbol VarSymbol (NonEmpty (Term, Formula)) Proof deriving instance Show Proof deriving instance Eq Proof -- cgit v1.2.3 From 30f7c63ce566c993816607f3368c357233693aae Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Tue, 27 Aug 2024 01:44:45 +0200 Subject: Experimental working commit, programm will compile But the Proof that the domain of the local function is not right. Also if in the definition of our local function we just use f(x) = x then we get a technical ambigus parse --- library/topology/urysohn2.tex | 8 ++++++-- source/Checking.hs | 13 +++++++------ source/Meaning.hs | 4 ++-- source/Syntax/Abstract.hs | 2 +- source/Syntax/Adapt.hs | 4 ++-- source/Syntax/Concrete.hs | 13 ++++++++----- source/Syntax/Internal.hs | 2 +- source/Syntax/Token.hs | 17 +++++++++++++++-- 8 files changed, 42 insertions(+), 21 deletions(-) (limited to 'source') diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex index 8e5261e..05ea180 100644 --- a/library/topology/urysohn2.tex +++ b/library/topology/urysohn2.tex @@ -44,10 +44,14 @@ \begin{proof} + Define $f : X \to \reals$ such that $f(x) = $ + \begin{cases} + &(x + x) , x \in X + % & x ,x \in X <- will result in technicly ambigus parse + \end{cases} - + Trivial. - Contradiction. \end{proof} diff --git a/source/Checking.hs b/source/Checking.hs index 817c477..6d55ee1 100644 --- a/source/Checking.hs +++ b/source/Checking.hs @@ -543,7 +543,7 @@ checkProof = \case checkCalc calc assume [Asm (calcResult calc)] checkProof continue - DefineFunctionMathy funVar domVar ranVar argVar definitions continue -> do + DefineFunctionMathy funVar argVar domVar ranExpr definitions continue -> do -- We have f: X \to Y and x \mapsto ... -- definition is a nonempty list of (expresssion e, formula phi) -- such that f(x) = e if phi(x) @@ -558,8 +558,8 @@ checkProof = \case setGoals [makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Iff` subdomainConjuctionLocalFunction argVar definitions )] -- check the disjunct union tellTasks - assume [Asm (makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Implies` (TermOp ApplySymbol [TermVar funVar, TermVar argVar] `IsElementOf` TermVar ranVar)))] -- function f from \dom(f) \to \ran(f) - assume (functionSubdomianExpression funVar argVar definitions) --behavior on the subdomians + assume [Asm (makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Implies` (TermOp ApplySymbol [TermVar funVar, TermVar argVar] `IsElementOf` ranExpr)))] -- function f from \dom(f) \to \ran(f) + assume (functionSubdomianExpression funVar argVar (NonEmpty.toList definitions)) --behavior on the subdomians setGoals goals checkProof continue @@ -571,9 +571,10 @@ subdomainConjuctionLocalFunction argVar defintions = in TermVar argVar `IsElementOf` makeConjunction stmts -functionSubdomianExpression :: VarSymbol -> VarSymbol -> NonEmpty (Term, Formula) -> [Asm] -functionSubdomianExpression f a nxs = case nxs of - x:|xs -> singleFunctionSubdomianExpression f a x : functionSubdomianExpression f a (NonEmpty.fromList xs) +functionSubdomianExpression :: VarSymbol -> VarSymbol -> [(Term, Formula)] -> [Asm] +functionSubdomianExpression f a (x:xs) = singleFunctionSubdomianExpression f a x : functionSubdomianExpression f a xs +functionSubdomianExpression _ _ [] = [] + singleFunctionSubdomianExpression :: VarSymbol -> VarSymbol -> (Term, Formula) -> Asm diff --git a/source/Meaning.hs b/source/Meaning.hs index ab98c9a..4a21fa3 100644 --- a/source/Meaning.hs +++ b/source/Meaning.hs @@ -606,9 +606,9 @@ glossProof = \case then Sem.DefineFunction funVar argVar <$> glossExpr valueExpr <*> glossExpr domExpr <*> glossProof proof else error "mismatched variables in function definition." - Raw.DefineFunctionMathy funVar domVar ranVar funVar2 argVar definitions proof -> do + Raw.DefineFunctionMathy funVar domVar ranExpr funVar2 argVar definitions proof -> do if funVar == funVar2 - then Sem.DefineFunctionMathy funVar domVar ranVar argVar <$> (glossLocalFunctionExprDef `each` definitions) <*> glossProof proof + then Sem.DefineFunctionMathy funVar argVar domVar <$> glossExpr ranExpr <*> (glossLocalFunctionExprDef `each` definitions) <*> glossProof proof else error "missmatched function names" Raw.Calc calc proof -> Sem.Calc <$> glossCalc calc <*> glossProof proof diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs index 6372c87..13691e7 100644 --- a/source/Syntax/Abstract.hs +++ b/source/Syntax/Abstract.hs @@ -373,7 +373,7 @@ data Proof - | DefineFunctionMathy VarSymbol VarSymbol VarSymbol VarSymbol VarSymbol (NonEmpty (Expr, Formula)) Proof + | DefineFunctionMathy VarSymbol VarSymbol Expr VarSymbol VarSymbol (NonEmpty (Expr, Formula)) Proof -- ^ Local function definition, but in this case we give the domain and target an the rules for $xs$ in some sub domains. -- deriving (Show, Eq, Ord) diff --git a/source/Syntax/Adapt.hs b/source/Syntax/Adapt.hs index 3cff497..4b43bc6 100644 --- a/source/Syntax/Adapt.hs +++ b/source/Syntax/Adapt.hs @@ -34,8 +34,8 @@ scanChunk ltoks = matchOrErr struct "struct definition" pos Located{startPos = pos, unLocated = (BeginEnv "inductive")} :_ -> matchOrErr inductive "inductive definition" pos - Located{startPos = pos, unLocated = (BeginEnv "signature")} :_ -> - matchOrErr signatureIntro "signature" pos + --Located{startPos = pos, unLocated = (BeginEnv "signature")} :_ -> + -- matchOrErr signatureIntro "signature" pos _ -> [] adaptChunks :: [[Located Token]] -> Lexicon -> Lexicon diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs index 69280c1..fe08fec 100644 --- a/source/Syntax/Concrete.hs +++ b/source/Syntax/Concrete.hs @@ -373,16 +373,16 @@ grammar lexicon@Lexicon{..} = mdo -- 3 & \text{else} -- \end{cases} - functionDefineCase <- rule $ (,) <$> expr <*> (_ampersand *> formula) + functionDefineCase <- rule $ (,) <$> (_ampersand *> (expr <|> exprVar )) <*> (_comma *> formula) defineFunctionMathy <- rule $ DefineFunctionMathy <$> (_define *> beginMath *> varSymbol) -- Define $ f <*> (_colon *> varSymbol) -- : 'var' \to 'var' - <*> (_to *> varSymbol <* endMath <* _suchThat) + <*> (_to *> expr <* endMath <* _suchThat) -- <*> (_suchThat *> align (many1 ((_ampersand *> varSymbol <* _mapsto) <*> exprApp <*> (_ampersand *> formula)))) -- <*> (_suchThat *> align (many1 (varSymbol <* exprApp <* formula))) - <*> varSymbol <*> varSymbol <* symbol "=" - <*> many1 functionDefineCase - <*> proof + <*> (beginMath *> varSymbol) <*> (paren varSymbol <* _eq <* endMath) + <*> cases (many1 functionDefineCase) + <*> proof @@ -644,6 +644,9 @@ group body = token InvisibleBraceL *> body <* token InvisibleBraceR "\"{...} align :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a align body = begin "align*" *> body <* end "align*" +cases :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a +cases body = begin "cases" *> body <* end "cases" + maybeVarToken :: Located Token -> Maybe VarSymbol maybeVarToken ltok = case unLocated ltok of diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs index 0e3361d..7046161 100644 --- a/source/Syntax/Internal.hs +++ b/source/Syntax/Internal.hs @@ -436,7 +436,7 @@ data Proof | Define VarSymbol Term Proof | DefineFunction VarSymbol VarSymbol Term Term Proof - | DefineFunctionMathy VarSymbol VarSymbol VarSymbol VarSymbol (NonEmpty (Term, Formula)) Proof + | DefineFunctionMathy VarSymbol VarSymbol VarSymbol Term (NonEmpty (Term, Formula)) Proof deriving instance Show Proof deriving instance Eq Proof diff --git a/source/Syntax/Token.hs b/source/Syntax/Token.hs index cb3f4cb..52da86a 100644 --- a/source/Syntax/Token.hs +++ b/source/Syntax/Token.hs @@ -189,6 +189,7 @@ toks = whitespace *> goNormal id <* eof Nothing -> pure (f []) Just t@Located{unLocated = BeginEnv "math"} -> goMath (f . (t:)) Just t@Located{unLocated = BeginEnv "align*"} -> goMath (f . (t:)) + Just t@Located{unLocated = BeginEnv "cases"} -> goMath (f . (t:)) Just t -> goNormal (f . (t:)) goText f = do r <- optional textToken @@ -204,6 +205,7 @@ toks = whitespace *> goNormal id <* eof Nothing -> pure (f []) Just t@Located{unLocated = EndEnv "math"} -> goNormal (f . (t:)) Just t@Located{unLocated = EndEnv "align*"} -> goNormal (f . (t:)) + Just t@Located{unLocated = EndEnv "cases"} -> goNormal (f . (t:)) Just t@Located{unLocated = BeginEnv "text"} -> goText (f . (t:)) Just t@Located{unLocated = BeginEnv "explanation"} -> goText (f . (t:)) Just t -> goMath (f . (t:)) @@ -219,12 +221,12 @@ toks = whitespace *> goNormal id <* eof -- | Parses a single normal mode token. tok :: Lexer (Located Token) tok = - word <|> var <|> symbol <|> mathBegin <|> alignBegin <|> begin <|> end <|> opening <|> closing <|> label <|> ref <|> command + word <|> var <|> symbol <|> mathBegin <|> alignBegin <|> casesBegin <|> begin <|> end <|> opening <|> closing <|> label <|> ref <|> command -- | Parses a single math mode token. mathToken :: Lexer (Located Token) mathToken = - var <|> symbol <|> number <|> begin <|> alignEnd <|> end <|> opening <|> closing <|> beginText <|> beginExplanation <|> mathEnd <|> command + var <|> symbol <|> number <|> begin <|> alignEnd <|> casesEnd <|> end <|> opening <|> closing <|> beginText <|> beginExplanation <|> mathEnd <|> command beginText :: Lexer (Located Token) beginText = lexeme do @@ -277,6 +279,11 @@ alignBegin = guardM isTextMode *> lexeme do setMathMode pure (BeginEnv "align*") +casesBegin :: Lexer (Located Token) +casesBegin = guardM isTextMode *> lexeme do + Char.string "\\begin{cases}" + setMathMode + pure (BeginEnv "cases") -- | Parses a single end math token. mathEnd :: Lexer (Located Token) @@ -291,6 +298,12 @@ alignEnd = guardM isMathMode *> lexeme do setTextMode pure (EndEnv "align*") +casesEnd :: Lexer (Located Token) +casesEnd = guardM isMathMode *> lexeme do + Char.string "\\end{cases}" + setTextMode + pure (EndEnv "cases") + -- | Parses a word. Words are returned casefolded, since we want to ignore their case later on. word :: Lexer (Located Token) -- cgit v1.2.3 From 604d7a87b4c45ab13ef03e3c7a611ad4f9342f23 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Tue, 27 Aug 2024 02:13:29 +0200 Subject: ambigus parse fix. The proof goal must be changed, since now some could define a function with overlapping and worng subdomains --- library/topology/urysohn2.tex | 4 +++- source/Checking.hs | 6 +++--- source/Syntax/Concrete.hs | 2 +- 3 files changed, 7 insertions(+), 5 deletions(-) (limited to 'source') diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex index 05ea180..f2f6ef3 100644 --- a/library/topology/urysohn2.tex +++ b/library/topology/urysohn2.tex @@ -46,7 +46,9 @@ Define $f : X \to \reals$ such that $f(x) = $ \begin{cases} - &(x + x) , x \in X + &(x + x) &\text{if} x \in X + & x &\text{if} x \neq \zero + & \zero & \text{if} x = \zero % & x ,x \in X <- will result in technicly ambigus parse \end{cases} diff --git a/source/Checking.hs b/source/Checking.hs index 6d55ee1..7362c93 100644 --- a/source/Checking.hs +++ b/source/Checking.hs @@ -564,11 +564,11 @@ checkProof = \case checkProof continue --- | Makes a conjunction of all the subdomain statments +-- | Makes a conjunction of all the subdomain statments <- this has to be checked!!!! TODO!!!!!! subdomainConjuctionLocalFunction :: VarSymbol -> NonEmpty (Term, Formula) -> Formula -subdomainConjuctionLocalFunction argVar defintions = +subdomainConjuctionLocalFunction _ defintions = let stmts = [snd x | x <- NonEmpty.toList defintions] - in TermVar argVar `IsElementOf` makeConjunction stmts + in makeDisjunction stmts functionSubdomianExpression :: VarSymbol -> VarSymbol -> [(Term, Formula)] -> [Asm] diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs index fe08fec..9d52995 100644 --- a/source/Syntax/Concrete.hs +++ b/source/Syntax/Concrete.hs @@ -373,7 +373,7 @@ grammar lexicon@Lexicon{..} = mdo -- 3 & \text{else} -- \end{cases} - functionDefineCase <- rule $ (,) <$> (_ampersand *> (expr <|> exprVar )) <*> (_comma *> formula) + functionDefineCase <- rule $ (,) <$> (_ampersand *> expr) <*> (_ampersand *> text _if *> formula) defineFunctionMathy <- rule $ DefineFunctionMathy <$> (_define *> beginMath *> varSymbol) -- Define $ f <*> (_colon *> varSymbol) -- : 'var' \to 'var' -- cgit v1.2.3 From 6acc5654f1702f2466006564a415546a3def16e3 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Tue, 27 Aug 2024 17:19:02 +0200 Subject: Feature Complete Finalised the proof output and goals. The Local Function definition now producces a Function f with the right domain and range, together with the rules presented in cases. Then proof goal of this local definition is set to for all x we have x is element of dom(f) if and only if x is in exactly one of the subdomains. This suffices as welldefindness check on f, besides the right range. Further checks that should be implemented are the correct range of the function. And optional subproof such that the presented goal can be check easily. --- library/topology/urysohn2.tex | 2 +- source/Checking.hs | 37 ++++++++++++++++++++++++------------- source/Syntax/Internal.hs | 10 ++++++++++ 3 files changed, 35 insertions(+), 14 deletions(-) (limited to 'source') diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex index f2f6ef3..ea49a6c 100644 --- a/library/topology/urysohn2.tex +++ b/library/topology/urysohn2.tex @@ -46,7 +46,7 @@ Define $f : X \to \reals$ such that $f(x) = $ \begin{cases} - &(x + x) &\text{if} x \in X + &(x + k) &\text{if} x \in X \land k \in \naturals & x &\text{if} x \neq \zero & \zero & \text{if} x = \zero % & x ,x \in X <- will result in technicly ambigus parse diff --git a/source/Checking.hs b/source/Checking.hs index 7362c93..b43923c 100644 --- a/source/Checking.hs +++ b/source/Checking.hs @@ -555,30 +555,41 @@ checkProof = \case ,Asm (relationNoun (TermVar funVar))] goals <- gets checkingGoals - setGoals [makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Iff` subdomainConjuctionLocalFunction argVar definitions )] -- check the disjunct union + setGoals [makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Iff` localFunctionGoal definitions)] tellTasks assume [Asm (makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Implies` (TermOp ApplySymbol [TermVar funVar, TermVar argVar] `IsElementOf` ranExpr)))] -- function f from \dom(f) \to \ran(f) - assume (functionSubdomianExpression funVar argVar (NonEmpty.toList definitions)) --behavior on the subdomians + assume (functionSubdomianExpression funVar argVar domVar (NonEmpty.toList definitions)) --behavior on the subdomians setGoals goals checkProof continue +-- |Creats the Goal \forall x. x \in dom{f} \iff (phi_{1}(x) \xor (\phi_{2}(x) \xor (... \xor (\phi_{n}) ..))) +-- where the phi_{i} are the subdomain statments +localFunctionGoal :: NonEmpty (Term,Formula) -> Formula +localFunctionGoal xs = makeXor $ map snd $ NonEmpty.toList xs --- | Makes a conjunction of all the subdomain statments <- this has to be checked!!!! TODO!!!!!! -subdomainConjuctionLocalFunction :: VarSymbol -> NonEmpty (Term, Formula) -> Formula -subdomainConjuctionLocalFunction _ defintions = - let stmts = [snd x | x <- NonEmpty.toList defintions] - in makeDisjunction stmts +-- We have our list of expr and forumlas, in this case normaly someone would write +-- f(x) = ....cases +-- & (\frac{1}{k} \cdot x) &\text{if} x \in \[k, k+1\) +-- +-- So therefore we have to check that all free varibels in lhs are free on rhs, +-- since its an expression all varibals from the lhs has to be free on rhs. +-- +-- so we take (exp, frm) -> binding all free in exp +-- -> make forall [x, bound vars] x \in \dom(f) & frm => exp -functionSubdomianExpression :: VarSymbol -> VarSymbol -> [(Term, Formula)] -> [Asm] -functionSubdomianExpression f a (x:xs) = singleFunctionSubdomianExpression f a x : functionSubdomianExpression f a xs -functionSubdomianExpression _ _ [] = [] - +functionSubdomianExpression :: VarSymbol -> VarSymbol -> VarSymbol -> [(Term, Formula)] -> [Asm] +functionSubdomianExpression f a d (x:xs) = singleFunctionSubdomianExpression f a d x : functionSubdomianExpression f a d xs +functionSubdomianExpression _ _ _ [] = [] -singleFunctionSubdomianExpression :: VarSymbol -> VarSymbol -> (Term, Formula) -> Asm -singleFunctionSubdomianExpression funVar argVar x = Asm (makeForall [argVar] ((TermVar argVar `IsElementOf` snd x) `Implies` (TermOp ApplySymbol [TermVar funVar, TermVar argVar] `Equals` fst x))) +singleFunctionSubdomianExpression :: VarSymbol -> VarSymbol -> VarSymbol -> (Term, Formula) -> Asm +singleFunctionSubdomianExpression funVar argVar domVar (expr, frm) = let + boundVar = Set.toList (freeVars expr) in + let def = makeForall (argVar:boundVar) (((TermVar argVar `IsElementOf` TermVar domVar) `And` frm) `Implies` TermOp ApplySymbol [TermVar funVar, TermVar argVar] `Equals` expr) + in Asm def + checkCalc :: Calc -> Checking diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs index 7046161..e83126d 100644 --- a/source/Syntax/Internal.hs +++ b/source/Syntax/Internal.hs @@ -324,6 +324,16 @@ makeDisjunction = \case [] -> Bottom es -> List.foldl1' Or es +makeIff :: [ExprOf a] -> ExprOf a +makeIff = \case + [] -> Bottom + es -> List.foldl1' Iff es + +makeXor :: [ExprOf a] -> ExprOf a +makeXor = \case + [] -> Bottom + es -> List.foldl1' Xor es + finiteSet :: NonEmpty (ExprOf a) -> ExprOf a finiteSet = foldr cons EmptySet where -- cgit v1.2.3 From 454a89d6683a80d93c1be89a6321350cb8656b19 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Tue, 3 Sep 2024 02:28:06 +0200 Subject: Hot fix Hot Fix for the wrong Asumtion creation. Now the function will have a image. --- source/Checking.hs | 32 +++++++++++++++++--------------- 1 file changed, 17 insertions(+), 15 deletions(-) (limited to 'source') diff --git a/source/Checking.hs b/source/Checking.hs index b43923c..766c327 100644 --- a/source/Checking.hs +++ b/source/Checking.hs @@ -558,8 +558,9 @@ checkProof = \case setGoals [makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Iff` localFunctionGoal definitions)] tellTasks + fixed <- gets fixedVars assume [Asm (makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Implies` (TermOp ApplySymbol [TermVar funVar, TermVar argVar] `IsElementOf` ranExpr)))] -- function f from \dom(f) \to \ran(f) - assume (functionSubdomianExpression funVar argVar domVar (NonEmpty.toList definitions)) --behavior on the subdomians + assume (functionSubdomianExpression funVar argVar domVar fixed (NonEmpty.toList definitions)) --behavior on the subdomians setGoals goals checkProof continue @@ -573,21 +574,22 @@ localFunctionGoal xs = makeXor $ map snd $ NonEmpty.toList xs -- f(x) = ....cases -- & (\frac{1}{k} \cdot x) &\text{if} x \in \[k, k+1\) -- --- So therefore we have to check that all free varibels in lhs are free on rhs, --- since its an expression all varibals from the lhs has to be free on rhs. +-- since we have to bind all globaly free Varibels we generate following asumptions. -- --- so we take (exp, frm) -> binding all free in exp --- -> make forall [x, bound vars] x \in \dom(f) & frm => exp - - -functionSubdomianExpression :: VarSymbol -> VarSymbol -> VarSymbol -> [(Term, Formula)] -> [Asm] -functionSubdomianExpression f a d (x:xs) = singleFunctionSubdomianExpression f a d x : functionSubdomianExpression f a d xs -functionSubdomianExpression _ _ _ [] = [] - -singleFunctionSubdomianExpression :: VarSymbol -> VarSymbol -> VarSymbol -> (Term, Formula) -> Asm -singleFunctionSubdomianExpression funVar argVar domVar (expr, frm) = let - boundVar = Set.toList (freeVars expr) in - let def = makeForall (argVar:boundVar) (((TermVar argVar `IsElementOf` TermVar domVar) `And` frm) `Implies` TermOp ApplySymbol [TermVar funVar, TermVar argVar] `Equals` expr) +-- For x \mapsto expr(x,ys,cs) , if formula(x,ys) ; here cs are just global constants +-- -> \forall x,ys: ( formula(x,ys) => expr(x,ys,cs)) + + +functionSubdomianExpression :: VarSymbol -> VarSymbol -> VarSymbol -> Set VarSymbol -> [(Term, Formula)] -> [Asm] +functionSubdomianExpression f a d s (x:xs) = singleFunctionSubdomianExpression f a d s x : functionSubdomianExpression f a d s xs +functionSubdomianExpression _ _ _ _ [] = [] + +singleFunctionSubdomianExpression :: VarSymbol -> VarSymbol -> VarSymbol -> Set VarSymbol -> (Term, Formula) -> Asm +singleFunctionSubdomianExpression funVar argVar domVar fixedV (expr, frm) = let + -- boundVar = Set.toList (freeVars expr) in + -- let def = makeForall (argVar:boundVar) (((TermVar argVar `IsElementOf` TermVar domVar) `And` frm) `Implies` TermOp ApplySymbol [TermVar funVar, TermVar argVar] `Equals` expr) + boundVar = fixedV in + let def = forallClosure boundVar (((TermVar argVar `IsElementOf` TermVar domVar) `And` frm) `Implies` (TermOp ApplySymbol [TermVar funVar, TermVar argVar] `Equals` expr)) in Asm def -- cgit v1.2.3 From 5362771c14eccd80fd1a3ab6521c3a6ad9bb7838 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Tue, 17 Sep 2024 00:36:24 +0200 Subject: Corrected Math Env Parsing Since Latex has a really specify syntax for \begin{cases} ... \end{cases} The math mode in tokenizing had to be setup correctly. --- library/numbers.tex | 3 +++ library/topology/real-topological-space.tex | 27 +++++++++++++++------------ source/Syntax/Concrete.hs | 6 +++--- source/Syntax/Token.hs | 8 ++++---- 4 files changed, 25 insertions(+), 19 deletions(-) (limited to 'source') diff --git a/library/numbers.tex b/library/numbers.tex index 406553e..ac0a683 100644 --- a/library/numbers.tex +++ b/library/numbers.tex @@ -613,6 +613,9 @@ Laws of the order on the reals \subsection{Order on the reals} +\begin{axiom}\label{reals_order_is_transitive} + For all $x,y,z \in \reals$ such that $x < y$ and $y < z$ we have $x < z$. +\end{axiom} \begin{lemma}\label{plus_one_order} diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex index e5e17ef..d9790aa 100644 --- a/library/topology/real-topological-space.tex +++ b/library/topology/real-topological-space.tex @@ -70,7 +70,7 @@ Then $\epsBall{x}{\epsilon}$ is inhabited. \end{lemma} \begin{proof} - $x < x + \epsilon$. + $x < x + \epsilon$ by \cref{reals_order_behavior_with_addition,realsplus,reals_axiom_zero_in_reals,reals_axiom_kommu,reals_axiom_zero}. $x - \epsilon < x$. $x \in \epsBall{x}{\epsilon}$. \end{proof} @@ -104,12 +104,8 @@ Omitted. \end{proof} -\begin{lemma}\label{reals_order_is_transitive} - For all $x,y,z \in \reals$ such that $x < y$ and $y < z$ we have $x < z$. -\end{lemma} -\begin{proof} - Omitted. -\end{proof} + + \begin{lemma}\label{reals_order_plus_minus} Suppose $a,b \in \reals$. @@ -207,12 +203,16 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have Then there exists $a,b \in \reals$ such that $a < b$ and $\intervalopen{a}{b} = \epsBall{x}{\epsilon}$. \end{lemma} +\begin{lemma}\label{one_in_realsplus} + $1 \in \realsplus$. +\end{lemma} + \begin{lemma}\label{reals_existence_addition_reverse} For all $\delta \in \reals$ there exists $\epsilon \in \reals$ such that $\epsilon + \epsilon = \delta$. \end{lemma} \begin{proof} Fix $\delta \in \reals$. - Follows by \cref{reals_disstro2,reals_axiom_disstro1,reals_rmul,suc_eq_plus_one,reals_axiom_mul_invers,suc,suc_neq_emptyset,realsplus_in_reals_plus,naturals_addition_axiom_2,naturals_1_kommu,reals_axiom_zero,naturals_inductive_set,one_is_suc_zero,realsplus,reals_one_bigger_zero,one_in_reals,reals_axiom_one,minus_in_reals}. + Follows by \cref{one_in_realsplus,reals_disstro2,reals_axiom_disstro1,reals_rmul,suc_eq_plus_one,reals_axiom_mul_invers,suc,suc_neq_emptyset,realsplus_in_reals_plus,naturals_addition_axiom_2,naturals_1_kommu,reals_axiom_zero,naturals_inductive_set,one_is_suc_zero,realsplus,reals_one_bigger_zero,one_in_reals,reals_axiom_one,minus_in_reals}. \end{proof} \begin{lemma}\label{reals_addition_minus_behavior1} @@ -260,7 +260,7 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have \end{subproof} We show that $\epsBall{x}{\epsilon} \subseteq \intervalopen{a}{b}$. \begin{subproof} - It suffices to show that for all $y \in \epsBall{x}{\epsilon}$ we have $y \in \intervalopen{a}{b}$. + It suffices to show that for all $y \in \epsBall{x}{\epsilon}$ we have $y \in \intervalopen{a}{b}$ by \cref{subseteq}. Fix $y \in \epsBall{x}{\epsilon}$. \end{subproof} @@ -270,7 +270,8 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have Suppose $a,b,x,y \in \reals$. Suppose $a < b$. Suppose $x < y$. - If $a \leq x < y \leq b$ then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{x}{y}$. + Suppose $a \leq x < y \leq b$. + Then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{x}{y}$. \end{lemma} \begin{proof} Omitted. @@ -280,7 +281,8 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have Suppose $a,b,x,y \in \reals$. Suppose $a < b$. Suppose $x < y$. - If $a = x$ and $b \leq y$ then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{a}{b}$. + Suppose $a = x$ and $b \leq y$. + Then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{a}{b}$. \end{lemma} \begin{proof} Omitted. @@ -290,7 +292,8 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have Suppose $a,b,x,y \in \reals$. Suppose $a < b$. Suppose $x < y$. - If $a \leq x$ and $b = y$ then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{x}{y}$. + Suppose $a \leq x$ and $b = y$. + Then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{x}{y}$. \end{lemma} \begin{proof} Omitted. diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs index 9d52995..7a89bea 100644 --- a/source/Syntax/Concrete.hs +++ b/source/Syntax/Concrete.hs @@ -373,15 +373,15 @@ grammar lexicon@Lexicon{..} = mdo -- 3 & \text{else} -- \end{cases} - functionDefineCase <- rule $ (,) <$> (_ampersand *> expr) <*> (_ampersand *> text _if *> formula) + functionDefineCase <- rule $ (,) <$> (optional _ampersand *> expr) <*> (_ampersand *> text _if *> formula) defineFunctionMathy <- rule $ DefineFunctionMathy <$> (_define *> beginMath *> varSymbol) -- Define $ f <*> (_colon *> varSymbol) -- : 'var' \to 'var' <*> (_to *> expr <* endMath <* _suchThat) -- <*> (_suchThat *> align (many1 ((_ampersand *> varSymbol <* _mapsto) <*> exprApp <*> (_ampersand *> formula)))) -- <*> (_suchThat *> align (many1 (varSymbol <* exprApp <* formula))) - <*> (beginMath *> varSymbol) <*> (paren varSymbol <* _eq <* endMath) - <*> cases (many1 functionDefineCase) + <*> (beginMath *> varSymbol) <*> (paren varSymbol <* _eq ) + <*> cases (many1 functionDefineCase) <* endMath <* optional _dot <*> proof diff --git a/source/Syntax/Token.hs b/source/Syntax/Token.hs index 52da86a..53e1e6a 100644 --- a/source/Syntax/Token.hs +++ b/source/Syntax/Token.hs @@ -189,7 +189,7 @@ toks = whitespace *> goNormal id <* eof Nothing -> pure (f []) Just t@Located{unLocated = BeginEnv "math"} -> goMath (f . (t:)) Just t@Located{unLocated = BeginEnv "align*"} -> goMath (f . (t:)) - Just t@Located{unLocated = BeginEnv "cases"} -> goMath (f . (t:)) + --Just t@Located{unLocated = BeginEnv "cases"} -> goMath (f . (t:)) Just t -> goNormal (f . (t:)) goText f = do r <- optional textToken @@ -205,7 +205,7 @@ toks = whitespace *> goNormal id <* eof Nothing -> pure (f []) Just t@Located{unLocated = EndEnv "math"} -> goNormal (f . (t:)) Just t@Located{unLocated = EndEnv "align*"} -> goNormal (f . (t:)) - Just t@Located{unLocated = EndEnv "cases"} -> goNormal (f . (t:)) + --Just t@Located{unLocated = EndEnv "cases"} -> goNormal (f . (t:)) Just t@Located{unLocated = BeginEnv "text"} -> goText (f . (t:)) Just t@Located{unLocated = BeginEnv "explanation"} -> goText (f . (t:)) Just t -> goMath (f . (t:)) @@ -282,7 +282,7 @@ alignBegin = guardM isTextMode *> lexeme do casesBegin :: Lexer (Located Token) casesBegin = guardM isTextMode *> lexeme do Char.string "\\begin{cases}" - setMathMode + --setMathMode pure (BeginEnv "cases") -- | Parses a single end math token. @@ -301,7 +301,7 @@ alignEnd = guardM isMathMode *> lexeme do casesEnd :: Lexer (Located Token) casesEnd = guardM isMathMode *> lexeme do Char.string "\\end{cases}" - setTextMode + --setTextMode pure (EndEnv "cases") -- cgit v1.2.3 From c943ca6441e9118bc9caee1c11f697da89bc06b7 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Wed, 18 Sep 2024 00:01:42 +0200 Subject: working commit --- library/set/equinumerosity.tex | 2 +- library/topology/urysohn2.tex | 260 ++++++++++++++++++++++++++++++++++++++--- source/Checking.hs | 2 +- source/Meaning.hs | 4 +- source/Syntax/Abstract.hs | 2 +- source/Syntax/Concrete.hs | 4 +- source/Syntax/Internal.hs | 2 +- 7 files changed, 250 insertions(+), 26 deletions(-) (limited to 'source') diff --git a/library/set/equinumerosity.tex b/library/set/equinumerosity.tex index a846b78..a922052 100644 --- a/library/set/equinumerosity.tex +++ b/library/set/equinumerosity.tex @@ -15,7 +15,7 @@ $A\approx A$. \end{proposition} \begin{proof} - $\identity{A}$ is a bijection from $A$ to $A$ by \cref{id_is_bijection}. + $\identity{A}$ is a bijection from $A$ to $A$. %by \cref{id_is_bijection}. Follows by \cref{equinum}. \end{proof} diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex index 9990199..97bbc70 100644 --- a/library/topology/urysohn2.tex +++ b/library/topology/urysohn2.tex @@ -13,6 +13,7 @@ \import{set/fixpoint.tex} \import{set/product.tex} \import{topology/real-topological-space.tex} +\import{set/equinumerosity.tex} \section{Urysohns Lemma} @@ -251,6 +252,7 @@ + \begin{proposition}\label{naturals_leq_on_suc} For all $n,m \in \naturals$ such that $m < \suc{n}$ we have $m \leq n$. \end{proposition} @@ -358,6 +360,218 @@ Omitted. \end{proof} +\begin{lemma}\label{naturals_suc_injective} + Suppose $n,m \in \naturals$. + $n = m$ iff $\suc{n} = \suc{m}$. +\end{lemma} + +\begin{lemma}\label{naturals_rless_implies_not_eq} + Suppose $n,m \in \naturals$. + Suppose $n < m$. + Then $n \neq m$. +\end{lemma} + +\begin{lemma}\label{cardinality_of_singleton} + For all $x$ such that $x \neq \emptyset$ we have $\{x\}$ has cardinality $1$. +\end{lemma} +\begin{proof} + Omitted. + %Fix $x$. + %Suppose $x \neq \emptyset$. + %Let $X = \{x\}$. + %$\seq{\zero}{\zero}=1$. + %$\seq{\zero}{\zero}$ has cardinality $1$. + %$X \setminus \{x\} = \emptyset$. + %$1 = \{\emptyset\}$. + %Let $F = \{(x,\emptyset)\}$. + %$F$ is a relation. + %$\dom{F} = X$. + %$\emptyset \in \ran{F}$. + %for all $x \in 1$ we have $x = \emptyset$. + %$\ran{F} = 1$. + %$F$ is injective. + %$F \in \surj{X}{1}$. + %$F$ is a bijection from $X$ to $1$. +\end{proof} + +\begin{lemma}\label{cardinality_n_plus_1} + For all $n \in \naturals$ we have $n+1$ has cardinality $n+1$. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + +\begin{lemma}\label{cardinality_n_m_plus} + For all $n,m \in \naturals$ we have $n+m$ has cardinality $n+m$. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + +\begin{lemma}\label{cardinality_plus_disjoint} + Suppose $X \inter Y = \emptyset$. + Suppose $X$ is finite. + Suppose $Y$ is finite. + Suppose $X$ has cardinality $n$. + Suppose $Y$ has cardinality $m$. + Then $X \union Y$ has cardinality $m+n$. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + + + + +\begin{lemma}\label{injective_functions_is_bijection_if_bijection_there_is_other_bijection_1} + Suppose $f$ is a bijection from $X$ to $Y$. + Suppose $g$ is a function from $X$ to $Y$. + Suppose $g$ is injective. + Suppose $X$ is finite and $Y$ is finite. + For all $n \in \naturals$ such that $Y$ has cardinality $n$ we have $g$ is a bijection from $X$ to $Y$. +\end{lemma} +\begin{proof}[Proof by \in-induction on $n$] + Assume $n \in \naturals$. + Suppose $Y$ has cardinality $n$. + $X$ has cardinality $n$ by \cref{bijection_converse_is_bijection,bijection_circ,regularity,cardinality,foundation,empty_eq,notin_emptyset}. + \begin{byCase} + \caseOf{$n = \zero$.} + Follows by \cref{converse_converse_eq,injective_converse_is_function,converse_is_relation,dom_converse,id_is_function_to,id_ran,ran_circ_exact,circ,ran_converse,emptyset_is_function_on_emptyset,bijective_converse_are_funs,relext,function_member_elim,bijection_is_function,cardinality,bijections_dom,in_irrefl,codom_of_emptyset_can_be_anything,converse_emptyset,funs_elim,neq_witness,id}. + \caseOf{$n \neq \zero$.} + %Take $n' \in n$ such that $n = \suc{n'}$. + %$n' \in \naturals$. + %$n' + 1 = n$. + %Take $y$ such that $y \in Y$ by \cref{funs_type_apply,apply,bijections_to_funs,cardinality,foundation}. + %Let $Y' = Y \setminus \{y\}$. + %$Y' \subseteq Y$. + %$Y'$ is finite. + %There exist $m \in \naturals$ such that $Y'$ has cardinality $m$. + %Take $m \in \naturals$ such that $Y'$ has cardinality $m$. + %Then $Y'$ has cardinality $n'$. + %Let $x' = \apply{\converse{f}}{y'}$. + %$x' \in X$. + %Let $X' = X \setminus \{x'\}$. + %$X' \subseteq X$. + %$X'$ is finite. + %There exist $m' \in \naturals$ such that $X'$ has cardinality $m'$. + %Take $m' \in \naturals$ such that $X''$ has cardinality $m'$. + %Then $X'$ has cardinality $n'$. + %Let $f'(z)=f(z)$ for $z \in X'$. + %$\dom{f'} = X'$. + %$\ran{f'} = Y'$. + %$f'$ is a bijection from $X'$ to $Y'$. + %Let $g'(z) = g(z)$ for $z \in X'$. + %Then $g'$ is injective. + %Then $g'$ is a bijection from $X'$ to $Y'$ by \cref{rels,id_elem_rels,times_empty_right,powerset_emptyset,double_complement_union,unions_cons,union_eq_cons,union_as_unions,unions_pow,cons_absorb,setminus_self,bijections_dom,ran_converse,id_apply,apply,unions_emptyset,img_emptyset,zero_is_empty}. + %Define $G : X \to Y$ such that $G(z)= + %\begin{cases} + % g'(z) & \text{if} z \in X' \\ + % y' & \text{if} z = x' + %\end{cases}$ + %$G = g$. + %Follows by \cref{double_relative_complement,fun_to_surj,bijections,funs_surj_iff,bijections_to_funs,neq_witness,surj,funs_elim,setminus_self,cons_subseteq_iff,cardinality,ordinal_empty_or_emptyset_elem,naturals_inductive_set,natural_number_is_ordinal_for_all,foundation,inter_eq_left_implies_subseteq,inter_emptyset,cons_subseteq_intro,emptyset_subseteq}. + Omitted. + \end{byCase} + %$\converse{f}$ is a bijection from $Y$ to $X$. + %Let $h = g \circ \converse{f}$. + %It suffices to show that $\ran{g} = Y$ by \cref{fun_to_surj,dom_converse,bijections}. + %It suffices to show that for all $y \in Y$ we have there exist $x \in X$ such that $g(x)=y$ by \cref{funs_ran,subseteq_antisymmetric,fun_ran_iff,apply,funs_elim,ran_converse,subseteq}. +% + %Fix $y \in Y$. + %Take $x \in X$ such that $\apply{\converse{f}}{y} = x$. + +\end{proof} + +\begin{lemma}\label{injective_functions_is_bijection_if_bijection_there_is_other_bijection} + Suppose $f$ is a bijection from $X$ to $Y$. + Suppose $g$ is a function from $X$ to $Y$. + Suppose $g$ is injective. + Suppose $Y$ is finite. + Then $g$ is a bijection from $X$ to $Y$. +\end{lemma} +\begin{proof} + There exist $n \in \naturals$ such that $Y$ has cardinality $n$ by \cref{cardinality,injective_functions_is_bijection_if_bijection_there_is_other_bijection_1,finite}. + Follows by \cref{injective_functions_is_bijection_if_bijection_there_is_other_bijection_1,cardinality,equinum_tran,equinum_sym,equinum,finite}. +\end{proof} + + + +\begin{lemma}\label{naturals_bijection_implies_eq} + Suppose $n,m \in \naturals$. + Suppose $f$ is a bijection from $n$ to $m$. + Then $n = m$. +\end{lemma} +\begin{proof} + $n$ is finite. + $m$ is finite. + Suppose not. + Then $n < m$ or $m < n$. + \begin{byCase} + \caseOf{$n < m$.} + Then $n \in m$. + There exist $x \in m$ such that $x \notin n$. + $\identity{n}$ is a function from $n$ to $m$. + $\identity{n}$ is injective. + $\apply{\identity{n}}{n} = n$ by \cref{id_ran,ran_of_surj,bijections,injective_functions_is_bijection_if_bijection_there_is_other_bijection}. + Follows by \cref{inhabited,regularity,function_apply_default,apply,id_dom,in_irrefl,function_member_elim,bijections_dom,zero_is_empty,bijection_is_function,foundation,bijections,ran_of_surj,dom_converse,converse_emptyset,dom_emptyset}. + \caseOf{$m < n$.} + Then $m \in n$. + There exist $x \in n$ such that $x \notin m$. + $\converse{f}$ is a bijection from $m$ to $n$. + $\identity{m}$ is a function from $m$ to $n$. + $\identity{m}$ is injective. + $\apply{\identity{m}}{m} = m$ by \cref{id_ran,ran_of_surj,bijections,injective_functions_is_bijection_if_bijection_there_is_other_bijection}. + Follows by \cref{inhabited,regularity,function_apply_default,apply,id_dom,in_irrefl,function_member_elim,bijections_dom,zero_is_empty,bijection_is_function,foundation,bijections,ran_of_surj,dom_converse,converse_emptyset,dom_emptyset}. + \end{byCase} +\end{proof} + +\begin{lemma}\label{naturals_eq_iff_bijection} + Suppose $n,m \in \naturals$. + $n = m$ iff there exist $f$ such that $f$ is a bijection from $n$ to $m$. +\end{lemma} +\begin{proof} + We show that if $n = m$ then there exist $f$ such that $f$ is a bijection from $n$ to $m$. + \begin{subproof} + Trivial. + \end{subproof} + We show that for all $k \in \naturals$ we have if there exist $f$ such that $f$ is a bijection from $k$ to $m$ then $k = m$. + \begin{subproof}%[Proof by \in-induction on $k$] + %Assume $k \in \naturals$. + %\begin{byCase} + % \caseOf{$k = \zero$.} + % Trivial. + % \caseOf{$k \neq \zero$.} + % \begin{byCase} + % \caseOf{$m = \zero$.} + % Trivial. + % \caseOf{$m \neq \zero$.} + % Take $k' \in \naturals$ such that $\suc{k'} = k$. + % Then $k' \in k$. + % Take $m' \in \naturals$ such that $m = \suc{m'}$. + % Then $m' \in m$. + % + % \end{byCase} + %\end{byCase} + \end{subproof} +\end{proof} + +\begin{lemma}\label{seq_from_zero_suc_cardinality_eq_upper_border} + Suppose $n,m \in \naturals$. + Suppose $\seq{\zero}{n}$ has cardinality $\suc{m}$. + Then $n = m$. +\end{lemma} +\begin{proof} + We have $\seq{\zero}{n} = \suc{n}$. + Take $f$ such that $f$ is a bijection from $\seq{\zero}{n}$ to $\suc{m}$. + Therefore $n=m$ by \cref{suc_injective,naturals_inductive_set,cardinality,naturals_eq_iff_bijection}. +\end{proof} + +\begin{lemma}\label{seq_from_zero_cardinality_eq_upper_border_set_eq} + Suppose $n,m \in \naturals$. + Suppose $\seq{\zero}{n}$ has cardinality $\suc{m}$. + Then $\seq{\zero}{n} = \seq{\zero}{m}$. +\end{lemma} + \begin{proposition}\label{existence_normal_ordered_urysohn} Let $X$ be a urysohn space. Suppose $U$ is a urysohnchain of $X$. @@ -384,23 +598,24 @@ Take $f$ such that there exist $k'$ such that $f$ is a bijection from $\seq{\zero}{k'}$ to $\dom{U}$ and $\dom{U}$ has cardinality $\suc{k'}$ and for all $n',m' \in \seq{\zero}{k'}$ such that $n' < m'$ we have $f(n') < f(m')$. Take $k'$ such that $f$ is a bijection from $\seq{\zero}{k'}$ to $\dom{U}$ and $\dom{U}$ has cardinality $\suc{k'}$ and for all $n',m' \in \seq{\zero}{k'}$ such that $n' < m'$ we have $f(n') < f(m')$. $\seq{\zero}{k'}$ has cardinality $\suc{k}$ by \cref{omega_is_an_ordinal,suc,ordinal_transitivity,bijection_converse_is_bijection,seq_zero_to_n_eq_to_suc_n,cardinality,bijections_dom,bijection_circ}. - We show that $\seq{\zero}{k'} = \seq{\zero}{k}$. - \begin{subproof} - We show that $\seq{\zero}{k'} \subseteq \seq{\zero}{k}$. - \begin{subproof} - It suffices to show that for all $y \in \seq{\zero}{k'}$ we have $y \in \seq{\zero}{k}$. - Fix $y \in \seq{\emptyset}{k'}$. - Then $y \leq k'$. - Therefore $y \in k'$ or $y = k'$ by \cref{omega_is_an_ordinal,suc_intro_self,ordinal_transitivity,cardinality,rless_eq_in_for_naturals,m_to_n_set}. - %Then $\seq{\emptyset}{k'} \in \suc{k}$. - Therefore $y \in \suc{k}$. - Therefore $y \in \seq{\emptyset}{k}$. - \end{subproof} - We show that for all $y \in \seq{\zero}{k}$ we have $y \in \seq{\zero}{k'}$. - \begin{subproof} - Fix $y \in \seq{\emptyset}{k}$. - \end{subproof} - \end{subproof} + $\seq{\zero}{k'} = \seq{\zero}{k}$ by \cref{omega_is_an_ordinal,seq_from_zero_cardinality_eq_upper_border_set_eq,suc_subseteq_implies_in,suc_subseteq_elim,ordinal_suc_subseteq,cardinality}. + %We show that $\seq{\zero}{k'} = \seq{\zero}{k}$. + %\begin{subproof} + % We show that $\seq{\zero}{k'} \subseteq \seq{\zero}{k}$. + % \begin{subproof} + % It suffices to show that for all $y \in \seq{\zero}{k'}$ we have $y \in \seq{\zero}{k}$. + % Fix $y \in \seq{\emptyset}{k'}$. + % Then $y \leq k'$. + % Therefore $y \in k'$ or $y = k'$ by \cref{omega_is_an_ordinal,suc_intro_self,ordinal_transitivity,cardinality,rless_eq_in_for_naturals,m_to_n_set}. + % + % Therefore $y \in \suc{k}$. + % Therefore $y \in \seq{\emptyset}{k}$. + % \end{subproof} + % We show that for all $y \in \seq{\zero}{k}$ we have $y \in \seq{\zero}{k'}$. + % \begin{subproof} + % Fix $y \in \seq{\emptyset}{k}$. + % \end{subproof} + %\end{subproof} \end{subproof} Take $F$ such that $F$ is a bijection from $\seq{\zero}{k}$ to $\dom{U}$ and for all $n',m' \in \seq{\zero}{k}$ such that $n' < m'$ we have $F(n') < F(m')$. Let $N = \seq{\zero}{k}$. @@ -452,7 +667,9 @@ $f$ is staircase sequence of $U$ iff $f$ is a sequence and $U$ is a lifted urysohnchain of $X$ and $\dom{U} = \dom{f}$ and for all $n \in \dom{U}$ we have $\at{f}{n}$ is a staircase function adapted to $\at{U}{n}$ in $U$. \end{definition} - +\begin{definition} + +\end{definition} @@ -565,8 +782,15 @@ \end{subproof} Take $U$ such that $U$ is a lifted urysohnchain of $X$ and $\at{U}{\zero} = U_0$. + We show that there exist $S$ such that $S$ is staircase sequence of $U$. + \begin{subproof} + Omitted. + \end{subproof} + Take $S$ such that $S$ is staircase sequence of $U$. + For all $x \in \carrier[X]$ we have there exist $r,R$ such that $r \in \reals$ and $R$ is a sequence of reals and $\dom{R} = \naturals$ and $R$ converge to $r$ and for all $n \in \naturals$ we have $\at{R}{n} = \apply{\at{S}{n}}{x}$. + We show that for all $x \in \carrier[X]$ there exists $r \in \intervalclosed{a}{b}$ such that for . diff --git a/source/Checking.hs b/source/Checking.hs index 766c327..8bc38a4 100644 --- a/source/Checking.hs +++ b/source/Checking.hs @@ -543,7 +543,7 @@ checkProof = \case checkCalc calc assume [Asm (calcResult calc)] checkProof continue - DefineFunctionMathy funVar argVar domVar ranExpr definitions continue -> do + DefineFunctionLocal funVar argVar domVar ranExpr definitions continue -> do -- We have f: X \to Y and x \mapsto ... -- definition is a nonempty list of (expresssion e, formula phi) -- such that f(x) = e if phi(x) diff --git a/source/Meaning.hs b/source/Meaning.hs index 4a21fa3..00a944f 100644 --- a/source/Meaning.hs +++ b/source/Meaning.hs @@ -606,9 +606,9 @@ glossProof = \case then Sem.DefineFunction funVar argVar <$> glossExpr valueExpr <*> glossExpr domExpr <*> glossProof proof else error "mismatched variables in function definition." - Raw.DefineFunctionMathy funVar domVar ranExpr funVar2 argVar definitions proof -> do + Raw.DefineFunctionLocal funVar domVar ranExpr funVar2 argVar definitions proof -> do if funVar == funVar2 - then Sem.DefineFunctionMathy funVar argVar domVar <$> glossExpr ranExpr <*> (glossLocalFunctionExprDef `each` definitions) <*> glossProof proof + then Sem.DefineFunctionLocal funVar argVar domVar <$> glossExpr ranExpr <*> (glossLocalFunctionExprDef `each` definitions) <*> glossProof proof else error "missmatched function names" Raw.Calc calc proof -> Sem.Calc <$> glossCalc calc <*> glossProof proof diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs index 13691e7..c8022c7 100644 --- a/source/Syntax/Abstract.hs +++ b/source/Syntax/Abstract.hs @@ -373,7 +373,7 @@ data Proof - | DefineFunctionMathy VarSymbol VarSymbol Expr VarSymbol VarSymbol (NonEmpty (Expr, Formula)) Proof + | DefineFunctionLocal VarSymbol VarSymbol Expr VarSymbol VarSymbol (NonEmpty (Expr, Formula)) Proof -- ^ Local function definition, but in this case we give the domain and target an the rules for $xs$ in some sub domains. -- deriving (Show, Eq, Ord) diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs index 7a89bea..9b947b0 100644 --- a/source/Syntax/Concrete.hs +++ b/source/Syntax/Concrete.hs @@ -374,7 +374,7 @@ grammar lexicon@Lexicon{..} = mdo -- \end{cases} functionDefineCase <- rule $ (,) <$> (optional _ampersand *> expr) <*> (_ampersand *> text _if *> formula) - defineFunctionMathy <- rule $ DefineFunctionMathy + defineFunctionLocal <- rule $ DefineFunctionLocal <$> (_define *> beginMath *> varSymbol) -- Define $ f <*> (_colon *> varSymbol) -- : 'var' \to 'var' <*> (_to *> expr <* endMath <* _suchThat) @@ -386,7 +386,7 @@ grammar lexicon@Lexicon{..} = mdo - proof <- rule $ asum [byContradiction, byCases, bySetInduction, byOrdInduction, calc, subclaim, assume, fix, take, have, suffices, define, defineFunction, defineFunctionMathy, qed] + proof <- rule $ asum [byContradiction, byCases, bySetInduction, byOrdInduction, calc, subclaim, assume, fix, take, have, suffices, define, defineFunction, defineFunctionLocal, qed] blockAxiom <- rule $ uncurry3 BlockAxiom <$> envPos "axiom" axiom diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs index e83126d..c098380 100644 --- a/source/Syntax/Internal.hs +++ b/source/Syntax/Internal.hs @@ -446,7 +446,7 @@ data Proof | Define VarSymbol Term Proof | DefineFunction VarSymbol VarSymbol Term Term Proof - | DefineFunctionMathy VarSymbol VarSymbol VarSymbol Term (NonEmpty (Term, Formula)) Proof + | DefineFunctionLocal VarSymbol VarSymbol VarSymbol Term (NonEmpty (Term, Formula)) Proof deriving instance Show Proof deriving instance Eq Proof -- cgit v1.2.3