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.

4 files changed, 58 insertions, 33 deletions

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