[Agda] Eta for Bool

[Ulf Norell]

Hi Wouter,

I think your best bet here is using reflection. Something like

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.Reflection
open import Agda.Builtin.Unit
open import Agda.Builtin.List

id : Bool → Bool
id false = false
id true  = true

the-hammer : Term → TC ⊤
the-hammer hole = unify hole (con (quote refl) [])

smash-bool : (tac : Term → TC ⊤) {P : Bool → Set}
             {@(tactic tac) f : P false}
             {@(tactic tac) t : P true} →
             ∀ b → P b
smash-bool tac {f = f} {t = t} false = f
smash-bool tac {f = f} {t = t} true  = t

id-id : ∀ b → id b ≡ b
id-id = smash-bool the-hammer

/ Ulf

On Thu, Jun 3, 2021 at 11:04 AM Swierstra, W.S. (Wouter) <
W.S.Swierstra at uu.nl> wrote:

> Dear all,
>
> Suppose I have the following (silly) identity function:
>
>    id : Bool -> Bool
>    id True  = True
>    id False = False
>
> It's easy enough to show that this really is the identity function by
> proving:
>
>   id-id : (b : Bool) -> id b ≡ b
>   id-id True  = refl
>   id-id False = refl
>
> This is all easy enough -- but I've been writing a program where there
> are quite a few pattern matches of this form, often with the same (up to
> implicit arguments) right hand sides. Is there some idiom or eliminator
> that can reduce the amount of pattern matching required? I could write
> 'id-id' using the usual eliminator for booleans, but I still need to
> pass in two copies of refl. What are my options for keeping the number
> of cases in check? Thanks in advance,
>
>    Wouter
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210603/7a7e2761/attachment.html>