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.

4 files changed, 25 insertions, 19 deletions

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