Add quantified calcs and relax tokenization

Use an `\iff`-calc to speed up `union_as_unions`. Also remove `in_implies_neq` which seems to interact badly with the choice axiom used by superposition-based proofs like Vampire in cut-down problems.

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