[Agda] Holes 0.1.0

[Bradley Hardy]

Dear All,

Some of you may have seen my talk at S-REPLS earlier this month, entitled
“Improving Agda’s equational reasoning with reflection”. This is a public
release of the development that the talk was based on.

--------------------------------

https://github.com/bch29/agda-holes

Holes is an Agda library that uses reflection to make writing and reading
equational reasoning proofs easier.

It can turn proofs like this:

  *-distrib-+₁ : ∀ a b c → a * (b + c) ≡ a * b + a * c
  *-distrib-+₁ zero b c = refl
  *-distrib-+₁ (suc a) b c =
      b + c + a * (b + c)
    ≡⟨ cong (λ h → b + c + h) (*-distrib-+₁ a b c) ⟩
      (b + c) + (a * b + a * c)
    ≡⟨ sym (+-assoc (b + c) (a * b) (a * c)) ⟩
      ((b + c) + a * b) + a * c
    ≡⟨ cong (λ h → h + a * c) (+-assoc b c (a * b)) ⟩
      (b + (c + a * b)) + a * c
    ≡⟨ cong (λ h → (b + h) + a * c) (+-comm c (a * b)) ⟩
      (b + (a * b + c)) + a * c
    ≡⟨ cong (λ h → h + a * c) (sym (+-assoc b (a * b) c)) ⟩
      ((b + a * b) + c) + a * c
    ≡⟨ +-assoc (b + a * b) c (a * c) ⟩
      (b + a * b) + (c + a * c)
    ∎

... into proofs like this:

  *-distrib-+ : ∀ a b c → a * (b + c) ≡ a * b + a * c
  *-distrib-+ zero b c = refl
  *-distrib-+ (suc a) b c =
      b + c + ⌞ a * (b + c) ⌟
    ≡⟨ cong! (*-distrib-+ a b c) ⟩
      ⌞ (b + c) + (a * b + a * c) ⌟
    ≡⟨ cong! (+-assoc (b + c) (a * b) (a * c)) ⟩
      ⌞ (b + c) + a * b ⌟ + a * c
    ≡⟨ cong! (+-assoc b c (a * b)) ⟩
      (b + ⌞ c + a * b ⌟) + a * c
    ≡⟨ cong! (+-comm c (a * b)) ⟩
      ⌞ b + (a * b + c) ⌟ + a * c
    ≡⟨ cong! (+-assoc b (a * b) c) ⟩
      ⌞ ((b + a * b) + c) + a * c ⌟
    ≡⟨ cong! (+-assoc (b + a * b) c (a * c)) ⟩
      (b + a * b) + (c + a * c)
    ∎

This works by using reflection to inspect the left hand side of an 'equality'
type. The 'holes', i.e. expressions within the `⌞_⌟` (identity) function are
found, and a path to the holes is found. This path is then combined with the
user's proof to prove the goal. The `cong!` macro works to prove any goal that
expects an equality, not just those within equational reasoning.

It is easiest to use with propositional equality, because there is a general
congruence function available. The path can be converted to a simple lambda that
is used as the argument to `cong`. There is also work in progress support
for relations that do not have general congruence, by providing a database of
congruences for the macro to use.

Please see the README in the linked git repository for more information and
examples.

--------------------------------

Bradley Hardy
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170127/5841da31/attachment-0001.html>