Add some more builtins to support rendering rules

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

src/Bergamot/Rules.elm

@@ -88,6 +88,13 @@ getUnificationState env ps = Search.pure (ps.unificationState, ps)
 burn : Prover a -> Prover a
 burn p env ps = if ps.gas > 0 then Search.map (\(a, psp) -> (a, { psp | gas = ps.gas })) (p env { ps | gas = ps.gas - 1 }) else Search.fail
 
+try : Prover a -> Prover (Maybe a)
+try p env ps =
+    p env { ps | gas = 30 }
+    |> Search.one
+    |> Maybe.map (Tuple.first << Tuple.first)
+    |> (\mx -> Search.pure (mx, ps))
+
 liftInstantiation : (a -> InstantiationState -> (b, InstantiationState)) -> a -> Prover b
 liftInstantiation f a env ps =
     let
@@ -176,6 +183,16 @@ builtinRules t =
             Call "latexifystring" [StringLit s, Var output] ->
                 liftUnification unify (Var output) (StringLit (encodeLatex s))
                 |> map (\_ -> MkProofTree { name = "BuiltinLatexifyeString", conclusion = t, premises = []})
+            Call "not" [tp] ->
+                try (proveTerm tp)
+                |> andThen (\mp ->
+                    case mp of
+                        Nothing -> pure <| MkProofTree { name = "BuiltinNot", conclusion = t, premises = [] }
+                        Just _ -> fail)
+            Call "symeq" [Call s1 [], Call s2 []] ->
+                if s1 == s2
+                then pure <| MkProofTree { name = "BuiltinSymEq", conclusion = t, premises = [] }
+                else fail
             _ -> fail
 
 provePremises : List (Term UnificationVar) -> Prover (List ProofTree)