george: User Manual

[ Introduction ] [ File Structure ] [ #check PROP ] [ #check PRED ] [ #check PREDTYPES ] [ #check SEM (etc) ] [ #check TP ]
[ #check ND ] [ #check ST ] [ Arithmetic ] [ Sets ] [ #check Z ] [ #check PC ]
[ Contributions by Students ] [ Credits ] [ Keywords ]

Arithmetic Theory

Thanks to Jane Zeng for some of the documentation below.

Arithmetic theory (a term used generically in SE212) is a theory of predicate logic in which functions and predicates on numbers can be used in predicate logic expressions and proofs. Below is the syntax for these operators, many of which are infix operators. These can be used in any predicate logic formula.

"nat" and "int" are keywords in george for the natural number and integer types respectively. Arithmetic operators are parsed following BEDMAS and are left associative except for exponent which is right associative.

Syntax in george	Meaning	Syntax in george	Meaning
a + b	addition	a - b	subtraction
a * b	multiplication	a / b	division
a^b	exponentiation
a > b	greater than	a < b	less than
a >= b	greater than or equal to	a <= b	less than or equal to
max(a,b)	maximum	min(a,b)	minimum
fact(a)	factorial

These operators can be used in any predicate logic formula. For example:

#check PRED

// Every number that is less than 5 is also less than 10.

forall x. x < 5 => x <10

In proofs, we use the rule by arith on .. to justify any transformations on arithmetic formulas (see below). In addition, in natural deduction we have a special rule by induction on ..., which combines the universal introduction and implication introduction subproofs needed for induction (explained in lecture). Here are two examples that use induction and arithmetic reasoning:

#check ND

|- forall n:nat . 3^n >= 2^n 

bc) 3^0 >= 2^0      by arith 

ih) inductionstep 3^ng >= 2^ng {
    2) 3^ng * 3 >= 2^ng * 2  by arith on ih
    3) 3^(ng+1) >= 2^(ng+1)  by arith on 2
}
4) forall n. 3^n >= 2^n by induction on bc,ih-3

#check ND

f(0) = 0,
f(1) = 1,
forall n:nat . n >= 2 => f(n) = f(n-1) + f(n-2) 
|-
forall n:nat . exists y . n >= 0 & f(3*n) = 2*y

p1) f(0) = 0 premise
p2) f(1) = 1 premise
p3) forall n:nat. n >= 2 => f(n) = f(n-1) + f(n-2) premise
1) f(3*0) = f(0)     by arith 
3) f(3*0) = 0        by arith on 1, p1
4) f(3*0) = 2*0      by arith on 3
5) 0 >= 0 by arith
55) 0 >= 0 & f(3*0) = 2*0 by and_i on 4, 5
bc) exists y:nat . 0 >= 0 & f(3*0) = 2 * y   by exists_i on 55

ih) inductionstep exists y . ng >= 0 & f(3*ng) = 2 * y {
    6) for some yu assume ng >= 0 & f(3*ng) = 2*yu {
        64) ng >= 0 by and_e on 6
        65) f(3*ng) = 2 * yu by and_e on 6
        7) 3*(ng+ 1) >= 2 => f(3*(ng+1)) = f(3*(ng+1)-1) + f(3*(ng+1)-2) by forall_e on p3
        8) 3*(ng + 1) >= 2        by arith on 64
        9) f(3*(ng+1)) = f(3*(ng + 1)-1) + f(3*(ng+1)-2)          by imp_e on 7,8
        10) f(3*(ng+1)) = f(3*ng + 2) + f(3*ng+1) by arith on 9
        

        11) 3*ng +2 >= 2 => f(3*ng+2) = f(3*ng+2-1) + f(3*ng+2-2) by forall_e on p3
        12) 3*ng+2 >= 2        by arith on 64
        13) f(3*ng+2) = f(3*ng+2-1) + f(3*ng+2-2)       by arith on 11, 12
        15) f(3*ng+2) = f(3*ng+1) + f(3*ng)  by arith on 13

        17) f(3*(ng+1)) = f(3*ng+1) + f(3*ng)  + f(3*ng+1)  by eq_e on 10,15
        20) f(3*(ng+1)) = 2*f(3*ng+1) + f(3*ng) by arith on 17
        21) f(3*(ng+1)) = 2*f(3*ng+1) + 2*yu by eq_e on 65, 20

        25) f(3*(ng+1)) = 2*(f(3*ng+1) + yu) by arith on 21

        26) ng+1 >= 0 by arith on 64
        27) ng+1 >= 0 & f(3*(ng+1)) = 2*(f(3*ng+1) + yu) by and_i on 26,25
        30) exists y. ng+1 >= 0 & f(3*(ng+1)) = 2*y by exists_i on 27

    }
    35) exists y . ng+1 >= 0 & f(3*(ng+1)) = 2 * y                  by exists_e on ih, 6-30
}

40) forall n:nat . exists y . n >=0 & f(3*n) = 2*y         by induction on bc, ih-35

When can `by arith` be used?

The `by arith` rule is applicable only to arithmetic reasoning. The following describes the criteria for what constitutes an arithmetic formula (in george). All formulas (premises and conclusion) of a step must be arithmetic formulas to use a `by arith` step in george. A numeric operand is one of type nat or int.

An arithmetic formula is defined as any of the following:

• A formula with one of the following as the outermost operator: <, >, >=, <=. These operators always have numeric operands.
• A formula with one of the following as the outermost operator: =, !=, and numeric operands (determined by typechecking).
• A conjunction, disjunction, iff, or implication of arithmetic formulas
• A negation of an arithmetic formula

In addition, quantifiers are not permitted anywhere in arithmetic formulas, as these can be unsolvable problems.

A logical operator (other than a quantifier) may appear in parameters to functions or predicates (which occurs rarely).

Examples of arithmetic formulas: x b , fact(f(x^2)) = 6 , !(x >= 5 & x <= 5), p(f(2 + 3)) != 4, p(a | b) = 5.

Examples of formulas that are not arithmetic formulas: a & b, forall x . p(x), f(x) = g(x) (if f and g don't return a numeric value).

If all the premises and conclusion of a step are arithmetic formulas, george will attempt to check the correctness of a `by arith` step using an SMT solver. It can determine the step is valid, invalid, or unknown (warning).

George only supports the int and nat types, not reals.

• George performs integer division, so all results are floored. For example, (0 - 1) / 5 = (0 - 1) by arith is valid (negatives round away from 0), 1/5 = 0 by arith is valid (positives round towards 0), 3^4 / 2 = 40 by arith is valid.
• George cannot determine through typechecking that a value is of nat type, therefore, in induction problems which are usually over natural numbers, we often have to add a constraint that a value is >= 0 for `by arith` reasoning steps to pass.

Exponents are indicated by the ^ symbol, such as a ^ b. SMT solvers, however, does not support the rule a^(m + n) = a^m * a^n. The use of exponents in an arithmetic formulas almost always yields unknown.

fact(n) is a built-in function that returns the factorial of integer n. The function is recursively axiomatized as follows:

fact(0) = 1
forall x . x >= 0 => fact(x) >= 0
forall x . x >= 1 => fact(x) = x * fact(x - 1)

Using fact(n) on a negative number will result in an unknown result, as `fact` is not defined for negative integers. However, sometimes even with these axioms SMT solvers cannot solve problems that look obvious to us, such as:

x >= 0, y >= 0, max(x, y) = x|- fact(x) >= fact(y)
1) x >= 0 premise
2) y >= 0 premise 
3) max(x, y) = x premise
4) fact(x) >= fact(y) by arith on 1,2,3

fact(), min(), and max() have their function definitions built into George. But sometimes, we want to declare and axiomatize our own functions. To do this, place the function axioms as premises. Otherwise, George will not know how to interpret the function and the `by arith` steps will get unknown results. A pitfall to watch out for is to ensure function definitions are quantified correctly. For example,

// incorrect version
#check ND

f(x)= 3*x + 6, g(x) = 4*x^2 |- f(5) + g(1) = 25

1) f(x)= 3*x + 6 premise // unquantified x so it thinks x is some value
2) g(x) = 4*x^2  premise 
3) f(5) + g(1) = 25 by arith on 1,2 // George will report this step as invalid

// Correct version
#check ND

forall x . f(x)= 3*x + 6, forall x . g(x) = 4*x^2 |- f(5) + g(1) = 25

1) forall x . f(x)= 3*x + 6 premise
2) forall x . g(x) = 4*x^2  premise 
3) f(5) = 3*5 + 6 by forall_e on 1 
4) g(1) = 4*1^2 by forall_e on 2 
5) f(5) = 21 by arith on 3
6) g(1) = 4 by arith on 4
7) f(5) + g(1) = 25 by arith on 5,6

What does george check?

• Each formula is syntactically correct.
• Each formula typechecks.
• The rule names are correct.
• The non-arith, non-induction rules are correctly applied.
• The format of the proof is correct.

george checks some of the arith rules but if it cannot conclude that the arith steps are correct then it treats them as magic rules. Induction rules are treated as magic rules and does not check the correctness of these, therefore george gives you a warning that these rules have been used and not checked, but for the other TP/ND rules, it checks that they have been used correctly.