Certainty by Construction Progress Report 1

The following is a progress report for Certainty by Construction, a new book I’m writing on learning and effectively wielding Agda. Writing a book is a tedious and demoralizing process, so if this is the sort of thing you’re excited about, please do let me know!

As part of a new ~quarterly goal, I’m going to be publishing updates to Certainty by Construction every Friday. This is for a few reasons: one, things get done much more quickly when you’re not doing them in private; two, relatedly, it’s good to get some exposure here and keep myself accountable.

Anyway, there are 26 new pages since last week, although a good deal of that is code without any prose around it yet. I’m in the process of cannibalizing the sections on relations and setoids into a single chapter. It’s a discussion of mathematical relations, their properties, an several examples. We explore different pre-orders, partial orders and total orders, and have a length digression about effectively designing indices for data types.

This last point arose from me spending a few hours trying to work out under which circumstances exactly Agda gets confused about whether or not a computing index will give rise to a constructor. My findings are that it’s not really about computing indices, so much as it is about Agda running out of variables in which it can pack constraints. I suspect this knowledge can be exploited to make more interesting constructors than I thought possible, but I haven’t worked out how to do it yet.

I’ve also been working on how to simplify some bigger setoid proofs, where you have a bunch of equational reasoning you’d like to do under congruence. The folklore on this is generally to introduce a lemma somewhere else, but this has always struck me as a disappointing solution. Modulo the concrete syntax, this seems to work pretty well:

_≈nested_[_]_
    : A
    → {f : A → A}
    → (cong : {x y : A} → x ≈ y → f x ≈ f y)
    → {x y z : A}
    → x IsRelatedTo y
    → f y IsRelatedTo z
    → f x IsRelatedTo z
_ ≈nested cong [ relTo x=y ] (relTo fy=z)
    = relTo (trans (cong x=y) fy=z)
infixr 2 _≈nested_[_]_

which lets you focus in on a particular sub-expression, and use a new equational reasoning block to rewrite that, before popping your results back to the full expression. As an example:

  ⌊ ((a *H c) *x+ 0#) +H b *S c +H d *S a ⌋ * x + b * d
≈nested (+-congʳ ∘ *-congʳ) [  -- focus on subexpr
  ⌊ ((a *H c) *x+ 0#) +H b *S c +H d *S a ⌋
≈⟨ +H-+-hom (((a *H c) *x+ 0#) +H b *S c) (d *S a) x ⟩
  ⌊((a *H c) *x+ 0#) +H b *S c ⌋ + ⟦ d *S a ⌋
≈⟨ +-congʳ (+H-+-hom ((a *H c) *x+ 0#) (b *S c) x) ⟩
  ⌊ a *H c ⌋ * x + 0# + ⌊ b *S c ⌋ + ⌊ d *S a ⌋
≈⟨ …via… *S-*-hom ⟩
  ⌊ a *H c ⌋ * x + (b * ⌊ c ⌋) + (d * ⌊ a ⌋)
≈⟨ +-congʳ (+-congʳ (*-congʳ (*H-*-hom a c x))) ⟩
  ⌊ a ⌋ * ⌊ c ⌋ * x + b * ⌊ c ⌋ + d * ⌊ a ⌋
∎ ]                            -- pop back
  (⌊ a ⌋ * ⌊ c ⌋ * x + b * ⌊ c ⌋ + d * ⌊ a ⌋) * x + (b * d)

The attentive reader here will notice that I have also clearly been improving the chapter on ring solving. Maybe I’m just better at proofs these days, but the whole thing feels much less challenging than my first few times looking at it.

Anyway, that’s all for today. If you’ve already bought the book, you can get the updates for free on Leanpub. If you haven’t, might I suggest doing so? Your early support and feedback helps inspire me and ensure the book is as good as it can possibly be.