<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div>Dear All,<br class=""><br class="">Some of you may have seen my talk at S-REPLS earlier this month, entitled<br class="">“Improving Agda’s equational reasoning with reflection”. This is a public<br class="">release of the development that the talk was based on.<br class=""><br class="">--------------------------------</div><div><br class=""></div><div><a href="https://github.com/bch29/agda-holes" class="">https://github.com/bch29/agda-holes</a><br class=""><font color="#5856d6" class=""><br class=""></font>Holes is an Agda library that uses reflection to make writing and reading<br class="">equational reasoning proofs easier.<br class=""><font color="#5856d6" class=""><br class=""></font>It can turn proofs like this:<br class=""><font color="#5856d6" class=""><br class=""></font> *-distrib-+₁ : ∀ a b c → a * (b + c) ≡ a * b + a * c<br class=""> *-distrib-+₁ zero b c = refl<br class=""> *-distrib-+₁ (suc a) b c =<br class=""> b + c + a * (b + c)<br class=""> ≡⟨ cong (λ h → b + c + h) (*-distrib-+₁ a b c) ⟩<br class=""> (b + c) + (a * b + a * c)<br class=""> ≡⟨ sym (+-assoc (b + c) (a * b) (a * c)) ⟩<br class=""> ((b + c) + a * b) + a * c<br class=""> ≡⟨ cong (λ h → h + a * c) (+-assoc b c (a * b)) ⟩<br class=""> (b + (c + a * b)) + a * c<br class=""> ≡⟨ cong (λ h → (b + h) + a * c) (+-comm c (a * b)) ⟩<br class=""> (b + (a * b + c)) + a * c<br class=""> ≡⟨ cong (λ h → h + a * c) (sym (+-assoc b (a * b) c)) ⟩<br class=""> ((b + a * b) + c) + a * c<br class=""> ≡⟨ +-assoc (b + a * b) c (a * c) ⟩<br class=""> (b + a * b) + (c + a * c)<br class=""> ∎<br class=""><font color="#5856d6" class=""><br class=""></font>... into proofs like this:<br class=""><font color="#5856d6" class=""><br class=""></font> *-distrib-+ : ∀ a b c → a * (b + c) ≡ a * b + a * c<br class=""> *-distrib-+ zero b c = refl<br class=""> *-distrib-+ (suc a) b c =<br class=""> b + c + ⌞ a * (b + c) ⌟<br class=""> ≡⟨ cong! (*-distrib-+ a b c) ⟩<br class=""> ⌞ (b + c) + (a * b + a * c) ⌟<br class=""> ≡⟨ cong! (+-assoc (b + c) (a * b) (a * c)) ⟩<br class=""> ⌞ (b + c) + a * b ⌟ + a * c<br class=""> ≡⟨ cong! (+-assoc b c (a * b)) ⟩<br class=""> (b + ⌞ c + a * b ⌟) + a * c<br class=""> ≡⟨ cong! (+-comm c (a * b)) ⟩<br class=""> ⌞ b + (a * b + c) ⌟ + a * c<br class=""> ≡⟨ cong! (+-assoc b (a * b) c) ⟩<br class=""> ⌞ ((b + a * b) + c) + a * c ⌟<br class=""> ≡⟨ cong! (+-assoc (b + a * b) c (a * c)) ⟩<br class=""> (b + a * b) + (c + a * c)<br class=""> ∎<br class=""><font color="#5856d6" class=""><br class=""></font>This works by using reflection to inspect the left hand side of an 'equality'<br class="">type. The 'holes', i.e. expressions within the `⌞_⌟` (identity) function are<br class="">found, and a path to the holes is found. This path is then combined with the<br class="">user's proof to prove the goal. The `cong!` macro works to prove any goal that<br class="">expects an equality, not just those within equational reasoning.<br class=""><font color="#5856d6" class=""><br class=""></font>It is easiest to use with propositional equality, because there is a general<br class="">congruence function available. The path can be converted to a simple lambda that<br class="">is used as the argument to `cong`. There is also work in progress support<br class="">for relations that do not have general congruence, by providing a database of<br class="">congruences for the macro to use.<br class=""><font color="#5856d6" class=""><br class=""></font>Please see the README in the linked git repository for more information and<br class="">examples.<font color="#5856d6" class=""><br class=""></font></div><div><br class=""></div><div>--------------------------------</div><div><br class=""></div><div>Bradley Hardy</div></body></html>