[Agda] Holes 0.1.0

[Victor Miraldo]

Hello Bradley,

Interesting library, thanks! It is nice to see people are still working
on better equational reasoning! :)

I did some related work in the past
(https://github.com/VictorCMiraldo/agda-rw) but
soon after that Agda changed its reflection API. This rendered our
library unusable for
newer versions of Agda.

Since we had to do our unification from scratch, we could get away
without having to explicitly
mark where we wanted the rewrite or even the parameters to be passed
to the lemma used
to rewrite. How hard would it be to extend your approach for one or
both of these features?

Cheers,
Victor

On Fri, Jan 27, 2017 at 1:42 PM, Bradley Hardy <bch29 at cam.ac.uk> wrote:
> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>