From d5b31ee7dc5992687f214d77e795bab53d5fe65d Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Wed, 14 Aug 2024 12:53:47 +0200
Subject: some wishes for NaprocheZF

---
 library/wunschzettel.tex | 99 ++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 99 insertions(+)
 create mode 100644 library/wunschzettel.tex

(limited to 'library/wunschzettel.tex')

diff --git a/library/wunschzettel.tex b/library/wunschzettel.tex
new file mode 100644
index 0000000..b2681fd
--- /dev/null
+++ b/library/wunschzettel.tex
@@ -0,0 +1,99 @@
+%This is just a .tex file with a wishlist of functionalitys 
+
+
+Tupel struct
+
+\newtheorem{struct2}[theoremcount]{Struct2}
+
+\begin{theorem}
+    %Some Theorem.
+\end{theorem}
+\begin{proof}
+    %Wish for nice Function definition. --------------------- 
+
+    %Some Proof where we need a Function.
+    %Privisuly defined.
+    $n \in \naturals$.
+    There is a Set $A = \{A_{0}, ..., A_{n}\}$.
+    For all $i$ we have $A_{i} \subseteq X$.
+
+    Define function $f: X \to Y$,
+    \begin{align}
+        &x \mapsto \rfrac{y}{n} &; if \exists k \in \{1, ... n\}. x \in A_{k} \\
+        &x \mapsto 0 &; if x  \phi(x) \\ 
+        %phi is some fol formula
+
+        &x \mapsto \eta &; for \phi(x) and \psi(\eta) 
+
+        &x \mapsto \some_term(x)(u)(v)(w) &; \exist.u,v,w \psi(x)(u)(v)(w) \\ 
+        % here i see the real need of varibles that can be useds in the define term
+
+        &x \mapsto \some_else_term(x)   &; else 
+        % the else term would be great 
+
+        % the following axioms should be automaticly added.
+        % \dom{f} = X
+        % \ran{f} \subseteq Y
+        % f is function
+
+        % therefor we should add the prompt for a proof that f is well defined
+    \end{align}
+    \begin{proof_well_defined}
+        % we need to proof that f allways maps X to Y
+    \end{proof_well_defined}
+
+    % more proof but now i can use the function f
+
+    % --------------------------------------------------------
+
+
+\end{proof}
+
+
+%------------------------------------------
+% My wish for a new struct 
+% I think this could be just get implemented along with the old struct
+
+
+% If take we only take tupels,
+% then just a list of defining fol formulas should be enougth. 
+\begin{struct2}
+    We say $(X,O)$ is a topological space if
+    \begin{enumerate}
+        \item $X$ is a set. % or X = \{...\mid .. \} or X = \naturals ... or ...
+        \item $O \subseteq \pow X$.
+        \item $\forall x,y \in O. x \union y \in O$ 
+        \item %another formula
+        \item %....
+    \end{enumerate} 
+\end{struct2}
+
+
+% Then the proof of some thing is a structure is more easy.
+% Since if we have just a tupel and some formulas which has to be fufilled,
+% then we can make a proof as follows.
+
+\begin{struct2}
+    We say $(A,i,N)$ is a indexed set if
+    \begin{enumerate}
+        \item $f$ is a bijection from $N$ to $A$
+        \item $N \subseteq \naturals$
+    \end{enumerate}
+\end{struct2}
+
+
+\begin{theorem}
+    Let $A = \{ \{n\} \mid n \in \naturals \}$.
+    Let function $f: \naturals \to \pow{\naturals}$ such that,
+    \begin{algin}
+        \item x \mapsto \{x\} ; x \in \naturals
+    \end{algin}
+    Then $(A, f, \naturals)$ is a indexed set.
+\end{theorem}
+\begin{proof}
+    % Then we only need to proof that:
+    % \ran{f} = A
+    % \dom{f} = \naturals
+    % f is a bijection between $\naturals$ to $A$.
+\end{proof}
+
-- 
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 'library/wunschzettel.tex')

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

