Instantly share code, notes, and snippets.

# MaiaVictor/equality.md Created Oct 30, 2019

syntax description
`a == b` A type asserting that `a` is equal to `b`
`refl(~x)` A proof that `x == x`
`sym(~e)` Given `e : a == b`, proves `b == a`
`cong(~f, ~e)` For any `f`, given `e : a == b`, proves `f(a) == f(b)`
`t :: rewrite x in P(x) with e` Given `e : a == b` and `t : P(a)`, proves `P(b)`

Here, `a == b` is a type specifying that `a` is equal to `b`. It is not a proof, it is merely "a question". To prove it, you must construct a term `x` of type `a == b`. The only way to do it directly is with `refl(~t)`, which proves that a term is equal to itself. That is, for any `t`, proves `t == t`. So, for example:

```main : 1 == 1
refl(~1)```

That means `refl(~1)` is a proof that `1 == 1`. As you can see, we can have values inside types: that's perfectly normal in Formality.

Equalities are useful to, among other things, restrict the domain of a function. For example:

```mul_small : {x : Word, y : Word, ~e : (x + y) == 10} -> Word
x * y

main : Word
mul_small(3, 7, ~refl(~10))```

This "small multiplication" function can only be called if its first two arguments add to `10`. This is enforced by the presence of the third argument, `e`, which is erased (due to the `~`). In other words, differently than a classic "assert", this restriction is checked statically and has no runtime costs. As an exercise, try changing the arguments of `mul_small` on the program above and see what happens.

Equality can be used and manipuled with 3 primitives. The `sym` primitive just flips the sides of an equality. The `cong` primitive just appends a function to both sides. The `rewrite` primitive allows us to substitute equal terms in arbitrary types. It consists of a term to be casted (`t`), a variable (`x`), a template (`P(x)`) and an equality proof (`e`), and performs the following operation:

``````// Step 1: assert that `e`'s type is an equality.
// Step 2: replace the template's variable by the left-side of the equality.
// Step 3: assert that the type of `a` matches the type above.
// Step 4: replace the template's variable by the right-side of the equality.
// Step 5: cast `t` to the type above.
``````

For example, suppose that we had a function that received a `x : Word` and a `y : Word` that added to `9`, and we wanted to call `small_mul` with them. We could try this:

```main : {x : Word, y : Word, ~e : (x + y) == 9} -> Word
mul_small(x + y, 1, ~e)```

But we'd have the following error:

```Type mismatch.
- Found type... x + y == 9
- Instead of... (x + y) + 1 == 10```

That's because `e` is a proof that `x + y == 9`, not that `(x + y) + 1 == 10`. But since `9` is smaller than `10`, we should be able to call `mul_small` on `x + y`. With `rewrite`, we can do that as follows:

```main : {x : Word, y : Word, ~xy_is_9 : (x + y) == 9} -> Word
// The term to be casted.
let t = refl(~10)

// The rewrite equality.
let e = sym(~xy_is_9)

//  Step 1: asserted `e`'s type is an equality (`9 == x + y`).
//  Step 2: replacing `k` on the template by `9`, we get `(9 + 1) == 10`.
//  Step 3: asserted that `t : 10 == 10` matches the type above (by reduction).
//  Step 4: replacing `k` on the template by `x + y`, we get `((x + y) + 1) == 10`.
//  Step 5: `t` is casted to the type above.
let t = t :: rewrite k in (k + 1) == 10 with e

//Since `T : ((x + y) + 1) == 10`, we can call `mul_small` with `(x + y)` and `1`.
mul_small(x + y, 1, ~t)```

In short, it allowed us to replace `9` by `x + y` on `t : (9 + 1) == 10` by exploiting the `e : 9 == x + y` argument. Note that, here, `t` is an equality too, but that's not mandatory; it could have been any type that had a `9` inside it.