# MathCheck Instructions

This document is as of 2021-11-16. It lacks all more recent features of MathCheck.

In ready-made problems, the use of commands may have been restricted to those relevant for the problem. There are two mechanisms towards this aim. If the textarea has the name “exam”, then many commands are unavailable. Commands may also be banned by some commands mentioned below.

## Arithmetic and Parentheses

 54321 54321 frac(54)(321) 54/321 54 frac(3)(21) 54 3/21 54.321 54.321 pi pi e e
 + + − - * * x/y x/y frac(x+1)(2y) (x+1)/(2y)#/(x+1)(2y) x^y x^y x^(-y z) x^(-y z)
 ( ( ) ) ( #( ) #) [ [ ] ] \ text(div)\  div mod mod n! n!
 sqrt x+1 sqrt x+1 sqrt(x+1) sqrt(x+1) root(n)(x+1) root(n)(x+1) |x+1| |x+1|abs(x+1) |__x+1__| |_x+1_|floor(x+1) |~x+1~| |^x+1^|ceil(x+1) d/(d x) sin 5x DD x sin 5x
 sin sin cos cos tan tan cot cot ln ln log log log_2 log2 sinh sinh cosh cosh tanh tanh

The input symbols ( and ) denote ordinary parentheses and #( and #) denote hard parentheses. MathCheck removes unnecessary ordinary parentheses, but always prints hard parentheses even if they are unnecessary.

A, …, Z, a, …, z, and the Greek letters listed below can be used as variables, excluding e and π. If the problem mode assumes ordinary numbers, then I, …, N and i, …, n hold integer and others hold real values, unless the teacher has specified otherwise.

MathCheck is not good in finding errors if the floor or ceiling function is used.

MathCheck uses precise rational number arithmetic when it can and then reverts to intervals of double-precision values. Also decimal number tokens yield rational values, whenever possible. The functions ddn and dup return the lower and upper bound of the interval.

## Comparisons and Logic

 <= <= < < = = != != >= >= > >
 not !not ^^ /\and^^ vv \/orvv rarr --> harr <-> sf"F" FF sf"U" UU sf"T" TT
 \ sf"&&"\  && \ sf"||"\  || ->> ->> ** * AA x: AA x: AA i; 1 <= i <= n: AA i; 1 <= i <= n: EE x: EE x: EE i; 1 <= i <= n: EE i; 1 <= i <= n:
 rArr ==> lArr <== hArr <=> -= ===

## Reasoning Chains

A reasoning chain may contain ⇐, ⇔, ⇒ and ≡, and the following:

 assume x != 1 /\ y >= x; Set a condition that is assumed to hold throughout the (sub)proof. One may use enda instead of ;. original Refers to the first formula in a reasoning chain. If original is the first formula of a subproof, then it refers to the first formula of the parent proof. subend Ends a subproof. subproof Starts a subproof.

What formulas in a reasoning chain may contain depends on the problem mode. Typically most logical and comparison operators are allowed, but only a small set of arithmetic operators. Variables are automatically of the type needed by the problem mode.

## Greek Letters

 alpha al beta be gamma ga delta de varepsilon ve epsilon ep zeta ze
 eta et theta th vartheta vt iota io kappa ka lambda la mu mu
 nu nu xi xi rho rh sigma si tau ta upsilon up
 phi ph varphi vp chi ch psi ps omega om
 Gamma GaGA Delta DeDE Theta ThTH Lambda LaLA Xi XiXI
 Pi PiPI Sigma SiSI Phi PhPH Psi PsPS Omega OmOM

## Lexical Rules

Spaces and newlines may be freely used between tokens. If a non-numeric token ends and the next one starts with a letter or digit, there must be at least one space or newline in between.

These symbols can also be given as Unicode characters: ¬ ² ³ Γ Δ Θ Λ Ξ Π Σ Φ Ψ Ω α β γ δ ε ζ η θ ι κ λ μ ν ξ π ρ σ τ υ φ χ ψ ω ϑ ϕ ϵ ← → ↔ ↠ ⇐ ⇒ ⇔ ∀ ∃ − √ ∧ ∨ ≠ ≡ ≤ ≥ ⋅ ⌈ ⌉ ⌊ ⌋

## Special Commands

 /**/ Start a new line. A new line may also be started by putting the ⇔, ⇒, etc., to the very beginning of the line. In problem modes that do not support them, put =, >, etc., to the very beginning of the line. /* two to the n is 2^n */ Write a comment and start a new line. Passages surrounded by grave accent characters will be shown as mathematics. assume x != 1 /\ y^2 < sin x; Restrict the range of variables. Any comparisons and propositional operators may be used in the condition. One may use enda instead of ;. Works in the arithmetic and draw function modes, and almost all problem modes that support logical reasoning chains. Unless otherwise stated, this must be next to the problem mode keyword. index x Make the variable of array index type. integer x Make the variable of integer type. prime p Make the variable of prime number type. real k Make the variable of real number type.

## Problem Modes and Related

The versions with capital initial letter do and with small case do not reset most global settings.

 arithmetic Select the arithmetic mode. Checks a chain of arithmetic expressions separated by <, ≤, =, >, and ≥. array_claim A[0...n-1] Select the array claim mode. Checks a chain of predicates on A separated by ⇔ or ≡. The index lower bound must be an integer. The upper bound must be a variable with an optional + or − integer. Does not show the first claim explicitly. Testing is based on trying all small arrays whose elements are in a small range of integers. The smallest tested value is by default 0, but can be set with array_test_min. brief_help Print short typing instructions. CFG_compare Compare the context-free grammars given by the CFG_set and CFG_set2 commands. CFG_in Test whether the string given next is in the language specified earlier by CFG_set. CFG_long Set an upper bound to the length of answer strings. CFG_not_in This one is opposite to CFG_in. CFG_set Set a context-free grammar for future tasks. CFG_set2 Set the latter context-free grammar for CFG_cmp. CFG_short Set a lower bound to the length of answer strings. CFG_start Set the start symbol for the grammar given by CFG_set. (By default, the first non-terminal is used.) CFG_start2 Set the start symbol for the grammar given by CFG_set2. (By default, the first non-terminal is used.) CFG_tree Draw the parse tree of the string given next according to the grammar given by CFG_set, or report that it is not in its language. draw_function -10 10 -5 5;x^2; 1/x; sin x Draw graphs of at most six functions. The numbers are the extreme coordinates: left right bottom top, and they are optional starting from the last. equation x=3 \/ x=-1;x^2 - 2x - 3 = 0 <=> Select the equation mode. In the solution, also ⇒ may be used, but then there must be original ⇔ later on. The teacher-given roots may also be x FF, to indicate that there are no roots; or x, to not give the roots (this last feature does not yet work well). One may use ends instead of ;. The assume clause, if given, must be next to the teacher-given roots. The roots must certainly satisfy the assumption despite rounding errors. help Print this file. mathcheck Print copyright information. The resetting version is written as MathCheck. modulo 17TT <=> EE x: x^2 = -1 Select the modulo mode. Checks a reasoning chain in modular arithmetic. The number must be between 2 and 25 inclusive. expression_tree Draw the expression tree of an expression, etc. This command makes fewer sanity checks than usual. presburger Select the natural number logic mode. Checks a reasoning chain in the logic. prop_logic Select the propositional logic mode without the undefined truth value. Checks a reasoning chain in the logic. prop3_logic Select the propositional logic mode with the undefined truth value. Checks a reasoning chain in the logic. real_logic Select the real number logic mode. Checks a reasoning chain in the logic. tree_compare 1(2+3); Select the expression tree comparison mode. Checks that the expressions have the same expression trees. Does not show the first expression explicitly.

## Local Settings and Related

Local settings only affect the current problem.

 #* This can be used to denote invisible multiplication as a top or banned operator. allow_comp The relation chain may contain <, ≤, >, and ≥ or ⇐ and ⇒. This command is needed to cancel their automatic ban in exam textareas, solve x, solve_all, etc.. b_nodes 48 If the final expression yields at most 48 nodes, a bonus statement is printed. ban_comp The relation chain must not contain <, ≤, >, and ≥ or ⇐ and ⇒. end_of_answer If answers to two or more problems are submitted at the same time, this prevents the next question from being interpreted as part of the previous answer. It thus prevents odd-looking error messages. It should be used in the beginning of the next question. If followed by !, stops reading input. f_allow_U The undefined truth value is by default not allowed in the final answer, but may be allowed with f_allow_U. This currently only works in the array claim mode. f_ban ^ sqrt root; The final expression must not contain the listed operators. When banning *, it may make sense to also ban #*, and vice versa. f_CNF The final expression must be in conjunctional normal form or a product of sums. f_DNF The final expression must be in disjunctional normal form or a sum of products. f_nodes 56 The final expression must not yield more than 56 expression tree nodes. f_polynomial x; The final expression must be in polynomial form with respect to x / all variables. The variable may be omitted. f_range In modular arithmetic mode, the final expression must not contain constants outside the range 0, …, modulus minus 1. f_rational x; The final expression must be in rational or polynomial form with respect to x / all variables. The variable may be omitted. f_req_opr sqrt The final expression must contain √. f_simplify The final expression must be simplified. This command does not yet work very well. f_top_opr sqrt The top operator of the final expression must be √. If the operator is frac(d)(d ...), ∀, or ∃, also the variable must be given. The operator (independently of the variable) may not occur elsewhere in the expression. When using * as the operator, it may make sense to ban #*, and vice versa. hide_expr Print “model-solution” instead of the next expression. solve x The final expression must be solved with respect to x. solve_all The final expression must be solved with respect to all variables. var4 Allow four variables in the arithmetic mode, at the cost of less careful testing of the expressions. (By default, three are allowed.) var5 Allow five variables in the arithmetic mode, at the cost of less careful testing of the expressions. (By default, three are allowed.)

## Global Settings and Related

Global settings are not automatically reset for each new problem. The effect of each xxx_off can be cancelled with xxx_on and vice versa.

 CFG_ambiguous_on Warn about ambiguous grammar. CFG_CR_on Ignore newlines in strings, to facilitate combining CFG items from more than one HTML textarea. debug_on Make MathCheck print mysterious additional information. draw_off Do not draw the graphs of both sides when a relation fails. Do not draw the teacher's expression tree. exam_on Do not give feedback on semantics. fail_text Print the text following this command for each mathematically incorrect answer. The text ends at the next empty line, and # acts as the escape character facilitating writing HTML. ok_text Print the text following this command for each correct answer. The text ends at the next empty line, and # acts as the escape character facilitating writing HTML. only_no_yes_on Do not print the information whose purpose is to help the student find the error. This is useful, for instance, if the correct answer is a number. prove_off Do not attempt to prove relations, etc. reset Reset most global settings (not debug nor exam). verbose_on Print headers, etc., in the feedback.

## Deprecated or Removed Commands

 #D No longer exists. Use DD instead. #xxx No longer exists. Use xxx instead. #(, #), #*, and #/ are not deprecated. f_ban_der Bans the use of derivatives in the final formula. Use f_ban DD; instead. forget_errors Show the link to the next problem page even if the solution contains errors. Chained problem pages proved not so good. funcpar_on No longer exists. Alternative rules for the parentheses cause confusion. Use #( and #) when necessary. lf No longer exists. Use /**/ instead. newproblem No longer exists. Use arithmetic, prop_logic, etc., instead. next_URL https://... If the answer is correct, give the URL of the next problem page in the feedback. Chained problem pages proved not so good. no_next_URL If the answer is correct, tell that this was the last problem in the series. Chained problem pages proved not so good. parse_tree “Parse” refers to a wrong thing. Use expression_tree instead. prop3_on Use the undefined truth value also in the propositional logic mode. Use Prop3_logic instead. skip_error If possible, continue checking even if there is an error. Technically problematic and not very necessary. undef_off This is pedagogically unwise, use the assume mechanism.