# Algebra and subst Rules

In this section, we will learn our first two proof rules for programming logic – `algebra` and `subst`.

## Verifying simple programs

Before we delve into our new proof rules, let’s look at the process for verifying simple Logika programs (ones that include user input, variable initialization, and assignment statements using different operations). Here, the `// -->` lines are pieces of the verification process that you must add (or consider) in order to prove correctness of your program, and the other lines are the code of the program.

``````get user input / set initial variable values

// --> add assume statements to specify what must be true about the input

program statement

// --> add logic block to evaluate what has happened in the program

program statement

// --> add logic block to evaluate what has happened in the program

program statement

// --> add logic block to evaluate what has happened in the program

(...more program statements)

// --> add assert statements to express what our program did``````

We see that if our program involves user input, then we must consider whether our program will only work correctly for certain input values. In that situation, we express our assumptions using `assume` statements.

After each program statement, we must add a logic block to evaluate what changed on that line of code. We will see more details on these logic blocks throughout the rest of this chapter. Recall that the syntax for those logic blocks looks like:

``````l"""{
lineNumber. claim               justification

// ... (more claims/justifications)
}"""``````

Finally, we add one or more `assert` statements to express what our program did. These are usually placed at the end of a program, but sometimes we have assert statements throughout the program to describe the progress up to that point.

## Algebra justification

The `algebra` justification can be used for ANY algebraic manipulation on previous claims. When using this justification, include all relevant proof line numbers in whatever order (you might use as few as zero line numbers or as many as 3+ line numbers).

### Example

Consider this example:

``````import org.sireum.logika._

var x: Z = 6
var y: Z = x

//this assert will not hold yet
assert (y == 6)``````

Following our process from above, we add logic blocks after each program statement. In these logic blocks, we start by listing the previous program statement as a premise:

``````import org.sireum.logika._

var x: Z = 6

l"""{
1. x == 6               premise
}"""

var y: Z = x

l"""{
1. y == x               premise

//need claim "y == 6" for our assert to hold
}"""

//this assert will not hold yet
assert (y == 6)``````

For our assert to hold, we must have EXACTLY that claim in a previous logic block – so we know we want our second logic block to include the claim `y == 6`.

Here is the program with the second logic block completed – the assert statement will now hold.

``````import org.sireum.logika._

var x: Z = 6

l"""{
1. x == 6               premise
}"""

var y: Z = x

l"""{
1. y == x               premise
2. x == 6               premise     //established in a previous logic block, and x is unchanged since then
3. y == 6               algebra 1 2 //we know y is 6 using the claims from lines 1 and 2
}"""

//this assert will hold
assert (y == 6)``````

We could have also deleted the first logic block in this example. We would still be able to claim `x == 6` as a premise in the last logic block, as `x` had not changed since being given that value.

## subst

We have two deduction rules that involve substitution – `subst1` and `subst2`. Both of these rules are similar to the find/replace feature in text editors. They preserve truth by replacing one proposition with an equivalent one.

The `algebra` justification will work for most mathematical manipulation. However, it will not work for any claim involving `∧`, `∨`, `→`, `⊥`, `∀`, `∃` – in those cases, we will be required to use substitution instead.

### subst1 justification

Here is the syntax for the `subst1` rule. In the example below, line `m` must be an equivalence (something equals something else). Line `n` can be anything.

``````l"""{
...
m. LHS_M == RHS_M       (some justification)
...
n. LINE_N               (some justification)
...
p. (claim)              subst1 m n
}"""``````

`(claim1)` rewrites `LINE_N` by substituting all ocurrences of `LHS_M` (the FIRST side of line `m`) with `RHS_M`. Here is an example:

``````l"""{
1. x + 1 == y - 4                       (some justification)
2. x*(x + 1) == (x + 1) + y             (some justification)
3. x*(y - 4) == (y - 4) + y             subst1 1 2
}"""``````

We wrote line 2 by replacing each occurence of `x + 1` with `y - 4`.

### subst2 justification

Here is the syntax for the `subst2` rule. Just as with `subst1`, line `m` must be an equivalence (something equals something else). Line `n` can be anything.

``````l"""{
...
m. LHS_M == RHS_M       (some justification)
...
n. LINE_N               (some justification)
...
p. (claim)              subst2 m n
}"""``````

`(claim1)` rewrites `LINE_N` by substituting all ocurrences of `RHS_M` (the SECOND side of line `m`) with `LHS_M`. Here is an example:

``````l"""{
1. x + 1 == y                               (some justification)
2. y*(x + 1) == (x + 1) + y                 (some justification)
3. (x + 1)*(x + 1) == (x + 1) + (x + 1)     subst2 1 2
}"""``````

We wrote line 2 by replacing each occurence of `y` with `x + 1`. Note that we put parentheses around our first replacement to ensure a product equivalent to the original statement.