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(-)

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