# Different styles of equality reasoning

by

```{-# OPTIONS --cubical --safe #-}
module 2019-4-21-CuttMltt where
import Agda.Builtin.Equality as MLTT
import Cubical.Core.Everything as CUTT
import Agda.Builtin.Nat as MNat
import Cubical.Data.Nat as CNat
private variable A B : Set
```

In dependently-typed programming languages, we do equality proofs.

Type Theory folks formed two groups; one stands for “proofs are not important”, one stands for “proofs are important”. Someone claims that the identity proof between two objects is unique – which is related to the K rule. The other people believe that the proof of identity is significant – the same theorem can have different proofs, where the identity relation on these proofs are also nontrivial and can be proved to be equivalent or not.

# Intuitionistic Logic

First, let’s take a look at the world of unique identity proofs.

```module Intuitionistic where
open MLTT
open MNat
```

In Intuitionistic Logic, we can prove new theorems via pattern matching on existing theorems, because identity proofs are instances of the equality type:

``` trans : {a b c : A} → a ≡ b → b ≡ c → a ≡ c
trans refl refl = refl

sym : {a b : A} → a ≡ b → b ≡ a
sym refl = refl

cong : {a b : A} → (f : A → B) → a ≡ b → f a ≡ f b
cong _ refl = refl
```

or we can use `rewrite`, which is syntactic sugar of pattern matching (and this definition is more Idris style):

``` trans₁ : {a b c : A} → a ≡ b → b ≡ c → a ≡ c
trans₁ p q rewrite p = q

cong₁ : {a b : A} → (f : A → B) → a ≡ b → f a ≡ f b
cong₁ _ p rewrite p = refl
```

These three functions, `trans`, `sym` and `cong` are our equality proof combinators.

Larger and more concrete theorems, such as the plus commutative law:

``` +-comm : ∀ a b → a + b ≡ b + a
```

can be proved by induction – the base case is simply `a ≡ a + 0`, where we can introduce a lemma for it:

``` +-comm zero b = +-zero b
```

… and we prove the lemma by induction as well:

```  where
+-zero : ∀ a → a ≡ a + 0
+-zero zero = refl
+-zero (suc a) = cong suc (+-zero a)
```

Very small theorems can be proved by induction trivially using a recursive call as the induction hypothesis and let the `cong` function to finish the induction step.

Combining induction and our `trans` combinator we get the induction step of the proof of the plus commutative law:

``` +-comm (suc a) b = trans (cong suc (+-comm a b)) (+-suc b a)
where
+-suc : ∀ a b → suc (a + b) ≡ a + suc b
+-suc zero _ = refl
+-suc (suc a) b = cong suc (+-suc a b)
```

On the other hand, even large theorems such as the plus commutative law can also be proved without the help of lemmas.

Here’s an example, by exploiting the `rewrite` functionality:

``` +-comm₁ : ∀ n m → n + m ≡ m + n
+-comm₁ zero zero = refl
+-comm₁ zero (suc m) rewrite sym (+-comm₁ zero m)  = refl
+-comm₁ (suc n) zero rewrite +-comm₁ n zero = refl
+-comm₁ (suc n) (suc m) rewrite +-comm₁ n (suc m)
| sym (+-comm₁ (suc n) m) | +-comm₁ n m = refl
```

What does `rewrite` do? Let’s look at it in detail.

To prove this theorem, whose goal is `a + c ≡ b + d`,

``` step-by-step : ∀ {a b c d} → a ≡ b → c ≡ d → a + c ≡ b + d
step-by-step {b = b} {d = d} p q
```

we first rewrite with `p`, which turns the goal to `b + c ≡ b + d`, then rewrite with `q`, which turns the goal to `b + d ≡ b + d`,

```  rewrite p | q
```

which is a specialized version of `refl`:

```  = refl {x = b + d}
```

It’s like we’re destructing our goal step by step and finally turn it into a specialized `refl`.

For more complicated proofs, we’re not only destructing the goal – we’re also constructing terms that can be used to destruct the goal. `rewrite` is how we use the constructed terms to destruct terms.

Our proof is bidirectional.

# Cubical model

What if the identity proofs are not trivial?

```module Cubical where
open CUTT using (_≡_; I; ~_; hcomp; inS; hfill; i0; i1)
open CNat
```

In the Cubical model, there’s no pattern matching because you can never tell how many proofs there can be (so no case analysis). Instead, there are interval operations that can construct proofs via existing proofs in a more detailed way.

Inverting an interval is `sym`:

``` sym : {a b : A} → a ≡ b → b ≡ a
sym p i = p (~ i)
```

Creating a new interval by combining an old path with an arbitrary function is `cong`:

``` cong : {a b : A} (f : A → B) → a ≡ b → f a ≡ f b
cong f p i = f (p i)
```

`trans` is far more complicated – you’ll need cubical kan operation:

``` trans : {a b c : A} → a ≡ b → b ≡ c → a ≡ c
trans p q i = hfill (λ { j (i = i0) → p i; j (i = i1) → q j}) (inS (p i)) i
```

Although we lose the ability to `rewrite`, we still have our combinators – `sym`, `cong` and `trans`, which means that several existing proofs are still perfectly valid under the Cubical model.

On the other hand, according to the design of `Path` types, some proofs become perfectly natural. For instance, the `step-by-step` theorem shown above can be proved by:

``` step-by-step : ∀ {a b c d} → a ≡ b → c ≡ d → a + c ≡ b + d
step-by-step p q i = p i + q i
```

There can also be equality on functions, which is not even possible in the Intuitionistic type theory:

``` funExt : {f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g
funExt p i a = p a i
```

# Obvious Conclusions

• The Cubical model introduces tons of primitives while it’s fairly more powerful than the Intuitionistic type theory
• Cubical model is harder implementation-wise
• Intuitionistic type theory is more friendly for letting the compiler to solve some unification problems
• Both of these two models are not gonna save Agda

Tweet this Top 