diff options
| author | Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> | 2024-08-27 01:44:45 +0200 |
|---|---|---|
| committer | Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> | 2024-08-27 01:44:45 +0200 |
| commit | 30f7c63ce566c993816607f3368c357233693aae (patch) | |
| tree | 9a4cae03dabe28aeda4d2f5537ee04a808b5c49f /source/Checking.hs | |
| parent | 76ea8e11d943b123d28dfbe2f354838f80fb8dba (diff) | |
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
Diffstat (limited to 'source/Checking.hs')
| -rw-r--r-- | source/Checking.hs | 13 |
1 files changed, 7 insertions, 6 deletions
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 |