Thu 03 Mar 2022

Writing and proving programs correct is generally considered to be much harder than writing them alone. There is quite a bit of evidence to support this position but I will not cover it in this post. Conal Elliott has a hunch about why proving programs correct is so much more difficult. He thinks the main reason is that – most of the time – people attempt to prove properties about existing systems; systems designed in the absence of mathematical constraints.

If “proving at the end” is the main reason for the difficulty of
proof, then it may be the case that an approach where we
*simultaneously* write *and* prove is the solution.

It is a well-recognised principle that composing programs from simpler building blocks is a good way to construct larger programs. Another well-recognised “good thing” is the principle of compositionality which states that when trying to reason about the composition of A and B, it is desirable that the meaning of the composition is determined by the meanings of A, B and the rules used to combine them. It is undesirable (and non-compositional) in the case where reasoning about A and B together either

- can’t be done by reasoning about A and B independently, or
- is significantly more complicated than reasoning about A and B in isolation

What if we were to adopt a discipline where programs *and*
their proofs were composed simultaneously? This style of programming is
well-supported in dependently typed languages such as Agda, Coq, and
Idris. Conal has even coined a name for this technique:
*compositional correctness*.

In this post we will look at an example of *compositional
correctness* in action.

But first, we’ll take a look at constructing a program and then only “proving at the end”.

In my last
post we define a function called `splitPermute`

as
follows:

splitPermute : (m : ℕ) {n : ℕ} → (𝔽 (m + n) → 𝔽 (n + m)) splitPermute m {n} = join n m ∘ swap ∘ splitAt m

We were able to prove that `splitPermute n`

was the
inverse of `splitPermute m`

, for a given
`m + n : ℕ`

as follows:

inverse : {m n : ℕ} → splitPermute n ∘ splitPermute m ≗ id inverse {m} {n} = begin (splitPermute n ∘ splitPermute m) ≡⟨⟩ (join m n ∘ swap ∘ splitAt n) ∘ (join n m ∘ swap ∘ splitAt m) ≡⟨⟩ (join m n ∘ swap ∘ splitAt n ∘ join n m ∘ swap ∘ splitAt m) ≈⟨ cong-[ join m n ∘ swap ]∘⟨ splitAt-join n m ⟩∘[ swap ∘ splitAt m ] ⟩ (join m n ∘ swap ∘ swap ∘ splitAt m) ≈⟨ cong-[ join m n ]∘⟨ swap-involutive ⟩∘[ splitAt m ] ⟩ (join m n ∘ splitAt m) ≈⟨ join-splitAt m n ⟩ id ∎ where open import Relation.Binary.PropositionalEquality open import Relation.Binary.Reasoning.Setoid (𝔽 (m + n) →-setoid 𝔽 (m + n))

We then constructed a bijection – called an `Inverse`

in
Agda – as follows. This packages up a program with proofs of
invertibility.

splitPermute↔ : (m : ℕ) {n : ℕ} → (𝔽 (m + n) ↔ 𝔽 (n + m)) splitPermute↔ m {n} = mk↔′ (splitPermute m) (splitPermute n) (inverse {n} {m}) (inverse {m} {n})

But there is a better way! The beautiful thing about bijections is
that their proofs are bundled together with the program. This is just
what we need for *compositional correctness*.

Let’s see how this is done for `splitPermute`

.

splitPermute↔ : (m : ℕ) {n : ℕ} → 𝔽 (m + n) ↔ 𝔽 (n + m) splitPermute↔ m {n} = (+↔⊎ {m} {n} ∘-↔ swap↔) ∘-↔ sym-↔ +↔⊎

That’s it! The function, its inverse and accompanying proofs of
invertibility have all been defined *in a single line*.

In order to understand this code you will need to study the
definitions of `+↔︎⊎`

and `swap↔︎`

. `+↔︎⊎`

is defined in module `Data.Fin.Properties`

and has the
following definition:

+↔⊎ : ∀ {m n} → Fin (m ℕ.+ n) ↔ (Fin m ⊎ Fin n) +↔⊎ {m} {n} = mk↔′ (splitAt m {n}) (join m n) (splitAt-join m n) (join-splitAt m n)

Function `swap↔︎`

is something that I had to write myself
even though all the building blocks were already present in
`Data.Sum`

and `Data.Sum.Properties`

.

swap↔ : ∀ {a b} {A : Set a} {B : Set b} → (A ⊎ B) ↔ (B ⊎ A) swap↔ {a} {b} {A} {B} = mk↔′ swap swap swap-involutive swap-involutive

I submitted a PR to the GitHub `agda-stdlib`

repository
which added this function. It has now been incorporated
and will appear in a future release of the Agda Standard Library.

`∘-↔︎`

The magic of this approach is in the `∘-↔︎`

operator which
is defined in module `Function.Construct.Composition`

. It is
a synonym for function `inverse`

which is defined as:

inverse : Inverse R S → Inverse S T → Inverse R T inverse inv₁ inv₂ = record { f = G.f ∘ F.f ; f⁻¹ = F.f⁻¹ ∘ G.f⁻¹ ; cong₁ = congruent (≈ R) (≈ S) (≈ T) F.cong₁ G.cong₁ ; cong₂ = congruent (≈ T) (≈ S) (≈ R) G.cong₂ F.cong₂ ; inverse = inverseᵇ (≈ R) (≈ S) (≈ T) _ G.f⁻¹ (trans R) (trans T) G.cong₁ F.cong₂ F.inverse G.inverse } where module F = Inverse inv₁; module G = Inverse inv₂

One can further understand this code by looking at:

inverseˡ : Transitive ≈₃ → Congruent ≈₂ ≈₃ g → Inverseˡ ≈₁ ≈₂ f f⁻¹ → Inverseˡ ≈₂ ≈₃ g g⁻¹ → Inverseˡ ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹) inverseˡ trn g-cong f-inv g-inv x = trn (g-cong (f-inv _)) (g-inv x) inverseʳ : Transitive ≈₁ → Congruent ≈₂ ≈₁ f⁻¹ → Inverseʳ ≈₁ ≈₂ f f⁻¹ → Inverseʳ ≈₂ ≈₃ g g⁻¹ → Inverseʳ ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹) inverseʳ trn f⁻¹-cong f-inv g-inv x = trn (f⁻¹-cong (g-inv _)) (f-inv x) inverseᵇ : Transitive ≈₁ → Transitive ≈₃ → Congruent ≈₂ ≈₃ g → Congruent ≈₂ ≈₁ f⁻¹ → Inverseᵇ ≈₁ ≈₂ f f⁻¹ → Inverseᵇ ≈₂ ≈₃ g g⁻¹ → Inverseᵇ ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹) inverseᵇ trn₁ trn₃ g-cong f⁻¹-cong (f-invˡ , f-invʳ) (g-invˡ , g-invʳ) = inverseˡ trn₃ g-cong f-invˡ g-invˡ , inverseʳ trn₁ f⁻¹-cong f-invʳ g-invʳ

As you can see a single, general, proof serves whenever one wants to compose two bijections together.

If we compare the “prove at the end” with the compositional correctness approach, we see that in the “prove at the end” approach we had to carefully apply three different invertibility proofs (in order):

`splitAt-join`

`swap-involutive`

`join-splitAt`

However, by using the approach of compositional correctness, we
actually applied `inverseᵇ`

(under the hood) three times, and
the application was implicitly done with each application of the
`∘-↔︎`

operator.

A style of programming coined by Conal Elliott and called
*compositional correctness* can be used to reduce the cost of
proving one’s programs correct. In the example we considered, “proving
at the end” involved carefully selecting *specific* theorems
while *compositional correctness* used a *general* theorem
(at three specific types) to achieve its goals.

It will remain to be seen whether compositional correctness radically reduces the difficulty of proving program correctness, but it is a very promising candidate.