diff options
| -rw-r--r-- | library/ordinal.tex | 9 | ||||
| -rw-r--r-- | library/set.tex | 26 | ||||
| -rw-r--r-- | library/set/regularity.tex | 4 | ||||
| -rw-r--r-- | source/Api.hs | 1 | ||||
| -rw-r--r-- | source/Checking.hs | 22 | ||||
| -rw-r--r-- | source/CommandLine.hs | 5 | ||||
| -rw-r--r-- | source/Meaning.hs | 14 | ||||
| -rw-r--r-- | source/Syntax/Abstract.hs | 6 | ||||
| -rw-r--r-- | source/Syntax/Concrete.hs | 29 | ||||
| -rw-r--r-- | source/Syntax/Internal.hs | 43 | ||||
| -rw-r--r-- | source/Syntax/Token.hs | 13 | ||||
| -rw-r--r-- | test/golden/calc/glossing.golden | 4 | ||||
| -rw-r--r-- | test/golden/calc/parsing.golden | 4 |
13 files changed, 96 insertions, 84 deletions
diff --git a/library/ordinal.tex b/library/ordinal.tex index c092fa8..f978257 100644 --- a/library/ordinal.tex +++ b/library/ordinal.tex @@ -235,13 +235,6 @@ To show that \in\ is a strict total order it only remains to show that \in\ is c % Goal: ordinal(fgamma)=>(elem(falpha,fgamma)|elem(fgamma,falpha)|falpha=fgamma)) % Assume $\gamma$ is an ordinal. - % Goal: - % elem(falpha,fgamma)|elem(fgamma,falpha)|falpha=fgamma - % - % Original Vampire proof: - % Follows by \cref{setext,transitiveset,ordinal,in_implies_neq,prec_is_ordinal,in_asymmetric}. - % - % Pruned proof: Follows by \cref{setext,transitiveset,ordinal}. \end{subproof} \end{proof} @@ -489,7 +482,7 @@ Then $\alpha\subseteq\beta$. \end{proposition} \begin{proof} % Vampire proof: - Follows by \cref{inters_of_ordinals_is_ordinal,in_implies_neq,inters_iff_forall,ordinal_subseteq_implies_elem_or_eq,inters_subseteq_elem}. + Follows by \cref{inters_of_ordinals_is_ordinal,in_irrefl,inters_iff_forall,ordinal_subseteq_implies_elem_or_eq,inters_subseteq_elem}. \end{proof} \begin{proposition}\label{inters_of_ordinals_is_minimal} diff --git a/library/set.tex b/library/set.tex index 1f7a76a..d964ce7 100644 --- a/library/set.tex +++ b/library/set.tex @@ -124,16 +124,6 @@ which applies it to goals of the form “$A = B$” and “$A \neq B$”. Suppose $A\neq\emptyset$. Then $A$ is inhabited. \end{proposition} -%\begin{proposition}\label{empty_iff_emptyset} -% $A$ is empty iff $A = \emptyset$. -%\end{proposition} - - -\begin{proposition}% -\label{empty_eq} - If $x$ and $y$ are empty, then $x = y$. -\end{proposition} - \begin{proposition}\label{emptyset_subseteq} For all $a$ we have $\emptyset \subseteq a$. \end{proposition} @@ -351,17 +341,19 @@ The $\operatorname{\textsf{cons}}$ operation is determined by the following axio If $c\in B$, then $c\in A\union B$. \end{proposition} -% TODO SLOW \begin{proposition}\label{union_as_unions} $\unions{\{x,y\}} = x\union y$. \end{proposition} \begin{proof} - %For all z we have - %\begin{align*} - % z\in \unions{\{x,y\}} - % &\iff \exists Z\in\{x,y\}. z\in Z - %\end{align*} - Follows by set extensionality. + For all $z$ we have + \begin{align*} + z\in \unions{\{x,y\}} + &\iff \exists Z\in\{x,y\}. z\in Z + &\iff z\in x \lor z\in y + &\iff z\in x\union y. + \end{align*} + Follows by \cref{setext}. + %Follows by set extensionality. \end{proof} \begin{proposition}[Commutativity of union]% diff --git a/library/set/regularity.tex b/library/set/regularity.tex index 068d6a8..10f4a1f 100644 --- a/library/set/regularity.tex +++ b/library/set/regularity.tex @@ -59,10 +59,6 @@ Straightforward. \end{proof} -\begin{proposition}\label{in_implies_neq} - If $a\in A$, then $a\neq A$. -\end{proposition} - \begin{proposition}\label{in_asymmetric} For all sets $a, b$ such that $a\in b$ we have $b\notin a$. \end{proposition} diff --git a/source/Api.hs b/source/Api.hs index 1bdf615..866115d 100644 --- a/source/Api.hs +++ b/source/Api.hs @@ -67,7 +67,6 @@ import Text.Megaparsec hiding (parse, Token) import UnliftIO import UnliftIO.Directory import UnliftIO.Environment -import Syntax.Abstract (Formula) -- | Follow all @\\import@ statements recursively and build a theory graph from them. -- The @\\import@ statements should be on their own separate line and precede all diff --git a/source/Checking.hs b/source/Checking.hs index 8bc38a4..a33edc2 100644 --- a/source/Checking.hs +++ b/source/Checking.hs @@ -539,17 +539,17 @@ checkProof = \case , Asm (relationNoun (TermVar funVar)) ] checkProof continue - Calc calc continue -> do - checkCalc calc - assume [Asm (calcResult calc)] + Calc quant calc continue -> do + checkCalc quant calc + assume [Asm (calcResult quant calc)] checkProof continue DefineFunctionLocal funVar argVar domVar ranExpr definitions continue -> do - -- We have f: X \to Y and x \mapsto ... + -- 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) -- since we do a case deduction in the definition there has to be a check that, -- our domains in the case are a disjunct union of dom(f) - assume + assume [Asm (TermOp DomSymbol [TermVar funVar] `Equals` TermVar domVar) ,Asm (rightUniqueAdj (TermVar funVar)) ,Asm (relationNoun (TermVar funVar))] @@ -578,7 +578,7 @@ localFunctionGoal xs = makeXor $ map snd $ NonEmpty.toList xs -- -- For x \mapsto expr(x,ys,cs) , if formula(x,ys) ; here cs are just global constants -- -> \forall x,ys: ( formula(x,ys) => expr(x,ys,cs)) - + functionSubdomianExpression :: VarSymbol -> VarSymbol -> VarSymbol -> Set VarSymbol -> [(Term, Formula)] -> [Asm] functionSubdomianExpression f a d s (x:xs) = singleFunctionSubdomianExpression f a d s x : functionSubdomianExpression f a d s xs @@ -588,15 +588,15 @@ singleFunctionSubdomianExpression :: VarSymbol -> VarSymbol -> VarSymbol -> Set singleFunctionSubdomianExpression funVar argVar domVar fixedV (expr, frm) = let -- boundVar = Set.toList (freeVars expr) in -- let def = makeForall (argVar:boundVar) (((TermVar argVar `IsElementOf` TermVar domVar) `And` frm) `Implies` TermOp ApplySymbol [TermVar funVar, TermVar argVar] `Equals` expr) - boundVar = fixedV in + boundVar = fixedV in let def = forallClosure boundVar (((TermVar argVar `IsElementOf` TermVar domVar) `And` frm) `Implies` (TermOp ApplySymbol [TermVar funVar, TermVar argVar] `Equals` expr)) in Asm def - -checkCalc :: Calc -> Checking -checkCalc calc = locally do - let tasks = calculation calc + +checkCalc :: CalcQuantifier -> Calc -> Checking +checkCalc quant calc = locally do + let tasks = calculation quant calc forM_ tasks tell where tell = \case diff --git a/source/CommandLine.hs b/source/CommandLine.hs index b8c170e..3502b9a 100644 --- a/source/CommandLine.hs +++ b/source/CommandLine.hs @@ -18,7 +18,6 @@ import UnliftIO import UnliftIO.Directory import UnliftIO.Environment (lookupEnv) import System.FilePath.Posix -import qualified Tptp.UnsortedFirstOrder as Syntax.Internal runCommandLine :: IO () runCommandLine = do @@ -94,7 +93,7 @@ run = do Text.putStrLn task Text.putStrLn err Text.putStrLn tptp - + WithFailList -> liftIO case result of VerificationSuccess -> putStrLn "\ESC[32mVerification successful.\ESC[0m" VerificationFailure [] -> error "Empty verification fail" @@ -187,4 +186,4 @@ withMegalodonParser = flag' WithMegalodon (long "megalodon" <> help "Export to M withFailListParser :: Parser WithFailList withFailListParser = flag' WithFailList (long "list_fails" <> help "Will list all unproven task with possible reason of failure.") - <|> pure WithoutFailList -- Default to using the cache.
\ No newline at end of file + <|> pure WithoutFailList -- Default to using the cache. diff --git a/source/Meaning.hs b/source/Meaning.hs index 9b4bc45..3822221 100644 --- a/source/Meaning.hs +++ b/source/Meaning.hs @@ -605,14 +605,22 @@ glossProof = \case if domVar == argVar then Sem.DefineFunction funVar argVar <$> glossExpr valueExpr <*> glossExpr domExpr <*> glossProof proof else error "mismatched variables in function definition." - + Raw.DefineFunctionLocal funVar domVar ranExpr funVar2 argVar definitions proof -> do if funVar == funVar2 then Sem.DefineFunctionLocal funVar argVar domVar <$> glossExpr ranExpr <*> (glossLocalFunctionExprDef `each` definitions) <*> glossProof proof else error "missmatched function names" - Raw.Calc calc proof -> - Sem.Calc <$> glossCalc calc <*> glossProof proof + Raw.Calc calcQuant calc proof -> + Sem.Calc <$> glossCalcQuantifier calcQuant <*> glossCalc calc <*> glossProof proof +glossCalcQuantifier :: Maybe Raw.CalcQuantifier -> Gloss Sem.CalcQuantifier +glossCalcQuantifier Nothing = pure Sem.CalcUnquantified +glossCalcQuantifier (Just (Raw.CalcQuantifier xs bound maySuchThat)) = do + bound' <- glossBound bound + maySuchThat' <- glossStmt `each` maySuchThat + let maySuchThat'' = case (bound', maySuchThat') of + _ -> Nothing + pure (Sem.CalcForall xs maySuchThat'') glossLocalFunctionExprDef :: (Raw.Expr, Raw.Formula) -> Gloss (Sem.Term, Sem.Formula) glossLocalFunctionExprDef (definingExpression, localDomain) = do diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs index c8d5dac..23da652 100644 --- a/source/Syntax/Abstract.hs +++ b/source/Syntax/Abstract.hs @@ -338,6 +338,10 @@ data Defn | DefnOp SymbolPattern Expr deriving (Show, Eq, Ord) +data CalcQuantifier + = CalcQuantifier (NonEmpty VarSymbol) Bound (Maybe Stmt) + deriving (Show, Eq, Ord) + data Proof = Omitted | Qed Justification @@ -351,7 +355,7 @@ data Proof | Assume Stmt Proof | FixSymbolic (NonEmpty VarSymbol) Bound Proof | FixSuchThat (NonEmpty VarSymbol) Stmt Proof - | Calc Calc Proof + | Calc (Maybe CalcQuantifier) Calc Proof -- ^ Simplify goals that are implications or disjunctions. | TakeVar (NonEmpty VarSymbol) Bound Stmt Justification Proof | TakeNoun (NounPhrase []) Justification Proof diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs index 9b947b0..383f348 100644 --- a/source/Syntax/Concrete.hs +++ b/source/Syntax/Concrete.hs @@ -211,7 +211,6 @@ grammar lexicon@Lexicon{..} = mdo suchStmt <- rule $ _suchThat *> stmt <* optional _comma - -- Symbolic quantifications with or without generalized bounds. symbolicForall <- rule $ SymbolicForall <$> ((_forAll <|> _forEvery) *> beginMath *> varSymbols) @@ -327,9 +326,16 @@ grammar lexicon@Lexicon{..} = mdo let alignedIff = symbol "&" *> command "iff" <?> "\"&\\iff\"" biconditionalItem <- rule $ (,) <$> (alignedIff *> formula) <*> explanation - biconditionals <- rule $ Biconditionals <$> formula <*> (many1 biconditionalItem) + biconditionals <- rule $ Biconditionals <$> formula <*> (many1 biconditionalItem) <* optional _dot + - calc <- rule $ Calc <$> align (equations <|> biconditionals) <*> proof + calcQuantifier <- rule $ CalcQuantifier <$> + ((_forAll <|> _forEvery) *> beginMath *> varSymbols) + <*> maybeBounded <* endMath + <*> optional suchStmt + <* optional _have + + calc <- rule $ Calc <$> optional calcQuantifier <*> align (equations <|> biconditionals) <*> proof caseOf <- rule $ command "caseOf" *> token InvisibleBraceL *> stmt <* _dot <* token InvisibleBraceR byCases <- rule $ ByCase <$> env_ "byCase" (many1_ (Case <$> caseOf <*> proof)) @@ -349,39 +355,40 @@ grammar lexicon@Lexicon{..} = mdo subclaim <- rule $ Subclaim <$> (_show *> stmt <* _dot) <*> env_ "subproof" proof <*> proof have <- rule $ Have <$> optional (_since *> stmt <* _comma <* _have) <* optional _haveIntro <*> stmt <*> justification <* _dot <*> proof + 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 - - -- Define $f $\fromTo{X}{Y} such that, + + -- Define $f $\fromTo{X}{Y} such that, -- Define function $f: X \to Y$, -- \begin{align} - -- &x \mapsto 3*x &, + -- &x \mapsto 3*x &, -- &x \mapsto 4*k &, \forall k \in \N. x \in \Set{k} -- \end{align} - -- + -- -- Follwing is the definition right now. -- Define function $f: X \to Y$ such that, -- \begin{cases} -- 1 & \text{if } x \in \mathbb{Q}\\ -- 0 & \text{if } x \in \mathbb{R}\setminus\mathbb{Q} - -- 3 & \text{else} + -- 3 & \text{else} -- \end{cases} functionDefineCase <- rule $ (,) <$> (optional _ampersand *> expr) <*> (_ampersand *> text _if *> formula) - defineFunctionLocal <- rule $ DefineFunctionLocal + defineFunctionLocal <- rule $ DefineFunctionLocal <$> (_define *> beginMath *> varSymbol) -- Define $ f <*> (_colon *> varSymbol) -- : 'var' \to 'var' - <*> (_to *> expr <* endMath <* _suchThat) + <*> (_to *> expr <* endMath <* _suchThat) -- <*> (_suchThat *> align (many1 ((_ampersand *> varSymbol <* _mapsto) <*> exprApp <*> (_ampersand *> formula)))) -- <*> (_suchThat *> align (many1 (varSymbol <* exprApp <* formula))) <*> (beginMath *> varSymbol) <*> (paren varSymbol <* _eq ) - <*> cases (many1 functionDefineCase) <* endMath <* optional _dot + <*> cases (many1 functionDefineCase) <* endMath <* optional _dot <*> proof diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs index 6a53aa6..f185025 100644 --- a/source/Syntax/Internal.hs +++ b/source/Syntax/Internal.hs @@ -329,7 +329,7 @@ makeIff :: [ExprOf a] -> ExprOf a makeIff = \case [] -> Bottom es -> List.foldl1' Iff es - + makeXor :: [ExprOf a] -> ExprOf a makeXor = \case [] -> Bottom @@ -404,6 +404,10 @@ data IntroRule = IntroRule } deriving (Show, Eq, Ord) +data CalcQuantifier + = CalcForall (NonEmpty VarSymbol) (Maybe Formula) + | CalcUnquantified + deriving (Show, Eq, Ord) data Proof = Omitted @@ -435,7 +439,7 @@ data Proof | Have Formula Justification Proof -- ^ An affirmation, e.g.: /@We have \<stmt\> by \<ref\>@/. -- - | Calc Calc Proof + | Calc CalcQuantifier Calc Proof | Subclaim Formula Proof Proof -- ^ A claim is a sublemma with its own proof: -- @@ -474,25 +478,32 @@ deriving instance Show Calc deriving instance Eq Calc deriving instance Ord Calc -calcResult :: Calc -> ExprOf VarSymbol -calcResult = \case - Equation e eqns -> e `Equals` fst (NonEmpty.last eqns) - Biconditionals phi phis -> phi `Iff` fst (NonEmpty.last phis) +calcQuant :: CalcQuantifier -> (Formula -> Formula) +calcQuant = \case + CalcUnquantified -> id + CalcForall xs maySuchThat -> case maySuchThat of + Nothing -> makeForall xs + Just suchThat -> \phi -> makeForall xs (suchThat `Implies` phi) + +calcResult :: CalcQuantifier -> Calc -> ExprOf VarSymbol +calcResult quant = \case + Equation e eqns -> calcQuant quant (e `Equals` fst (NonEmpty.last eqns)) + Biconditionals phi phis -> calcQuant quant (phi `Iff` fst (NonEmpty.last phis)) -calculation :: Calc -> [(ExprOf VarSymbol, Justification)] -calculation = \case - Equation e1 eqns@((e2, jst) :| _) -> (e1 `Equals` e2, jst) : collectEquations (toList eqns) - Biconditionals p1 ps@((p2, jst) :| _) -> (p1 `Iff` p2, jst) : collectBiconditionals (toList ps) +calculation :: CalcQuantifier -> Calc -> [(ExprOf VarSymbol, Justification)] +calculation quant = \case + Equation e1 eqns@((e2, jst) :| _) -> (calcQuant quant (e1 `Equals` e2), jst) : collectEquations quant (toList eqns) + Biconditionals p1 ps@((p2, jst) :| _) -> (calcQuant quant (p1 `Iff` p2), jst) : collectBiconditionals quant (toList ps) -collectEquations :: [(ExprOf a, b)] -> [(ExprOf a, b)] -collectEquations = \case - (e1, _) : eqns'@((e2, jst) : _) -> (e1 `Equals` e2, jst) : collectEquations eqns' +collectEquations :: CalcQuantifier -> [(Formula, j)] -> [(Formula, j)] +collectEquations quant = \case + (e1, _) : eqns'@((e2, jst) : _) -> (calcQuant quant (e1 `Equals` e2), jst) : collectEquations quant eqns' _ -> [] -collectBiconditionals :: [(ExprOf a, b)] -> [(ExprOf a, b)] -collectBiconditionals = \case - (p1, _) : ps@((p2, jst) : _) -> (p1 `Iff` p2, jst) : collectEquations ps +collectBiconditionals :: CalcQuantifier -> [(Formula, j)] -> [(Formula, j)] +collectBiconditionals quant = \case + (p1, _) : ps@((p2, jst) : _) -> (calcQuant quant (p1 `Iff` p2), jst) : collectBiconditionals quant ps _ -> [] diff --git a/source/Syntax/Token.hs b/source/Syntax/Token.hs index 53e1e6a..2dad049 100644 --- a/source/Syntax/Token.hs +++ b/source/Syntax/Token.hs @@ -321,14 +321,17 @@ var = guardM isMathMode *> lexeme (fmap Variable var') where var' = do alphabeticPart <- letter <|> bb <|> greek - variationPart <- subscriptNumber <|> ticked <|> pure "" + variationPart <- subscript <|> ticked <|> pure "" pure (alphabeticPart <> variationPart) - subscriptNumber :: Lexer Text - subscriptNumber = do + subscript :: Lexer Text + subscript = do Char.char '_' - n <- some Char.digitChar - pure (Text.pack n) + unbraced <|> braced <|> text + where + unbraced = Text.singleton <$> Char.alphaNumChar + braced = Text.pack <$> (Char.char '{' *> many Char.alphaNumChar <* Char.char '}') + text = Char.string "\\text" *> braced -- for rendering the subscript in roman type -- Temporary hack to fit the TPTP format. ticked :: Lexer Text diff --git a/test/golden/calc/glossing.golden b/test/golden/calc/glossing.golden index 96366d4..ed4f3c0 100644 --- a/test/golden/calc/glossing.golden +++ b/test/golden/calc/glossing.golden @@ -71,7 +71,7 @@ , sourceColumn = Pos 1 } ) - ( Calc + ( Calc CalcUnquantified ( Equation ( TermVar ( NamedVar "y" ) @@ -120,7 +120,7 @@ , sourceColumn = Pos 1 } ) - ( Calc + ( Calc CalcUnquantified ( Biconditionals ( TermSymbol ( SymbolPredicate diff --git a/test/golden/calc/parsing.golden b/test/golden/calc/parsing.golden index 3d86683..b6f393a 100644 --- a/test/golden/calc/parsing.golden +++ b/test/golden/calc/parsing.golden @@ -80,7 +80,7 @@ , sourceColumn = Pos 1 } ) - ( Calc + ( Calc Nothing ( Equation ( ExprVar ( NamedVar "y" ) @@ -132,7 +132,7 @@ , sourceColumn = Pos 1 } ) - ( Calc + ( Calc Nothing ( Biconditionals ( FormulaChain ( ChainBase |