George

Theory of Arithmetic

Main note: Theory of Natural Number Arithmetic

Induction

Example

#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

Summation

Example

Prove:

|- forall n . n >= 1 => sum(i, 1, n, (2 * i) - 1) = n^2

which is:

proof:

#check ND

|- forall n . n >= 1 => sum(i, 1, n, (2 * i) - 1) = n^2

1) assume 0 >= 1 {
    1) !(0 >= 1) by arith
    2) sum (i, 1, 0, (2 * i) - 1) = 0^2 by not_e on 1, 2
}
bc) 0 >= 1 => sum(i, 1, 0, (2 * i) - 1) = 0^2 by imp_i on 1-3

ih) inductionstep ng >= 1 => sum(i, 1, ng, (2 * i) - 1) = ng^2 {
    4) assume ng + 1 >= 1 {
        5) ng = 0 | ng >= 1 by arith on 4
        6) case ng = 0 {
            7) sum (i, 1, 0 + 1, (2 * i) - 1) = 2 * 1 - 1 by arith // defn of sum
            9) sum (i, 1, 0 + 1, (2 * i) - 1) = (0 + 1)^2 by arith on 7
            11) sum (i, 1, ng + 1, (2 * i) - 1) = (ng + 1

{ #2}
by eq_e on 6, 9

}
12) case ng >= 1 {
13) sum(i, 1, ng, (2 * i) - 1) = ng^2 by imp_e on i h , 1 2
14) sum(i, 1, ng + 1, (2 * i) - 1) = 2 * (ng + 1) - 1 + sum (i, 1, ng, (2 * i) - 1) by arith // defn of sum
16) sum(i, 1, ng + 1, (2 * i) - 1) = 2 * (ng + 1) - 1 + (ng^2) by eq_e on 13, 14
17) sum(i, 1, ng + 1, (2 * i) - 1) = ng^2 + 2 * ng + 1 by artih on 16
18) sum(i, 1, ng + 1, (2 * i) - 1) = (ng + 1)^2 by artih on 17
}
20) sum(i, 1, ng + 1, (2 * i) - 1 ) = (ng + 1)^2 by cases on 5, 6-11, 12-18
}
21) ng + 1 >= 1 => sum(i, 1, ng + 1, (2 * i) - 1) = (ng + 1)^2 by imp_i on 4-20
}
22) forall n . n >= 1 => sum(i, 1, n, (2 * i) - 1) = n^2 by induction on bc, ih-21

Set Theory

Table

Concept Symbol George
Set Membership in
Empty Set empty
Universal Set , univ univ
Set Equality =
Subset sube
Proper Subset sub
Cardinality card(S)
Power Set pow(S)

Set Comprehension

Main note: Set Builder Notation

Example

Q = { x + y for x: nat, y: nat if x <= 2 & y <= 1 }

is equivalent to

Subset

Proof at Subsets#^f65b37

Example

# check ND

B sube C,
C sube D
| -
B sube D

1) B sube C premise
2) C sube D premise
3) for every xg {
    4) assume xg in B {
        5) forall x . x in B => x in C by set on 1 // subset
        6) xg in B => xg in C by forall_e on 5
        7) xg in C by imp_e on 4 ,6
        8) forall x . x in C => x in D by set on 2 // subset
        9) xg in C => xg in D by forall_e on 8
        10) xg in D by imp_e on 7 ,9
    }
    11) xg in B => xg in D by imp_i on 4 -10
}
12) forall x . x in B => x in D by forall_i on 3 -11
13) B sube D by set on 12 // subset

Relations

Main note: Relations

Table

Concept Symbol George
Domain dom(A)
Range ran(A)
Inverse R~
Identity id(R)
Domain Restriction

<|

| > | Range Restriction | $\triangleright$ |

|>

| > | Domain Subtraction | $\op{\mathrlap{\triangleleft}\textendash}$ |

<-|

| > | Range Subtraction | $\op{\mathrlap{\triangleright}\textendash}$ |

|->

| > | Relational Override | $\oplus$ | `(+)` | > | Relational Image | $R(\vert S \vert)$ |

R(|S|)

| > | Relational Composition | $R \op{;} S$ | `R ; S` |

<|

|>

<-|

|->

R(|S|)

Z Schemas

Example

In George:

schema MySystem begin
    X, Y: nat
pred
    X < Y;;
end
Example

In George:

schema Inc begin
    Delta MySystem
pred
    X' = X + 1;;
    Y' = Y + 1;;
end

Program Correctness

Example

Prove the partial correctness of the program:

assert(x >= 5 & y >= 0);
z := x;
z := z + y;
u := z;
assert(u >= 5) by asn;

Original: Floyd-Hoare Logic#Implied Proof Rule

George:

#check PC

fun main() {
    assert(X >= 5 & Y >= 0);
    assert(X + Y >= 5) by implied on VC1;
    Z := X;
    assert(Z + Y >= 5) by asn;
    Z := Z + Y;
    assert(Z >= 4) by asn;
    U := Z;
    assert(U >= 5) by asn;
}

/* VC 1 */

#check ND

X >= 5 & Y >= 0 |- X + Y >= 5

1) X >= 5 & Y >= 0 premise
2) X + Y >= 5 by arith on 1

Functions

Example

// NOTE: this is not complete
fun inc(x) {
    assert(true);
    ret := x + 1;
    assert(ret = x + 1);

    return ret;
}

fun main() {
    assert(i = i0);
    assert(inc(inc(i) + 1) = i0 + 3) by implied on VC1;
    y :+ inc(i);
    assert(inc(y + 1) = i0 + 3) by asn;
    i := y + 1;
    assert(inc(i) = ...)
}

Original: Floyd-Hoare Logic#Functions

From function rule, we have:

  • lem1:
  • lem2:

VC1:

#check ND

i = i0, inc(i) = i + 1, inc(i + 2) = i + 2 + 1 |- inc(inc(i) + 1) = 10 + 3

1) i = i0 premise
lem1) inc(i) = i + 1 premise
lem2) inc(i + 2) = i + 2 + 1 premise
4) inc(inc(i) + 1) = inc(inc(i) + 1) by eq_i
5) inc(inc(i) + 1) = inc(i + 1 + 1) by eq_e on lem1, 4
6) inc(inc(i) + 1) = inc(i + 2) by arith on 5
7) inc(inc(i) + 1) = i + 2 + 1 by eq_e on lem2, 6
8) inc(inc(i) + 1) = i + 3 by arith on 7
9) inc(inc(i) + 1) = i0 + 3 by eq_e on 1, 8