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