logoalt Hacker News

solomonb • yesterday at 7:19 PM • 1 reply • view on HN

I think a lot of people have never actually tried using a proof checker and are forming hot takes based on their imagined assumptions about how they work.

For anyone reading this, here is a very small example proof that + is associative over Nats in Agda (written using 1lab style equational reasoning syntax):

    +-associative : (x y z : Nat) → x + (y + z) ≡ (x + y) + z
    +-associative zero y z = refl
    +-associative (suc x) y z =
      suc x + (y + z) ≡⟨ ap suc (+-associative x y z) ⟩
      suc (x + y + z) ≡⟨⟩
      (suc x + y) + z ∎
We pattern match on the first nat to get `zero` and `suc x`. In the `zero` case we have `0 + (y + z) = (0 + y) + z`. Both sides compute to `y + z` and thus the equation holds by reflexivity.

In the `suc x` case we need to show that `suc x + (y + z) ≡ (suc x + y) + z`.

`suc x + (y + z)` computes to `suc (x + (y + z))` by the definition of `+`.

By recursively calling `+-associative x y z` we get `x + (y + z) ≡ (x + y) + z`. Then we need to prove that by congruence this is true under `suc`. We get this by passing our proof (from the recursive call to +-associative) into `ap suc`. `ap` says that given `a = b` it is true that `f a = f b`.

Finally, `(suc x + y) + z` computes to `suc ((x + y) + z)`, so the last step holds by computation, which is why it’s just `≡⟨⟩`.

Proof checkers like Lean/Agda/Rocq are literally total functional programming languages with rich type systems.

Everything above comes down to pattern matching and function application. The proof is just a function whose type is the statement we wanted to prove, and the type checker accepting it is what makes it a proof.

This is the Curry-Howard Correspondence in a nutshell. Propositions are types and proofs are programs.

Replies

black_knight • yesterday at 9:09 PM

And here is another short and simple example of some Agda code (Did you know you can open modules in a type signature‽):

    -- An element has at most one two-sided inverse.
    inverse-unique : ∀ (M : Monoid) (open Reasoning M)
                       (x y z : type M)
                   → y ⋆ x ＝ unit M
                   → x ⋆ z ＝ unit M
                   → y ＝ z
    inverse-unique M x y z leftInverse rightInverse =
      begin
        y                ⟪ sym (unitᵣAt y)           ⟫
        y ⋆ unit M       ⟪ mapᵣ (sym rightInverse)   ⟫
        y ⋆ (x ⋆ z)      ⟪ sym (associativeAt y x z) ⟫
        (y ⋆ x) ⋆ z      ⟪ mapₗ leftInverse          ⟫
        unit M ⋆ z       ⟪ unitₗAt z                 ⟫
        z
      ∎
      where open Reasoning M
Not sure if all the unicode characters will render on HN, but the things left of the ⟪ ⟫-brackets is exactly what a text book in mathematics will have. While the things inside the brackets are just a functional-programming way of saying out the argument which would be left for the reader to make in their head for why each step holds.

(If you know Agda, I dare you to look carefully at this example!)