A nice case bash tactic

CaseBash.lagda.md

description
Case bash tactic.

module CaseBash where

Displayed Lists

data ListP {ℓ ℓ'} {A : Type ℓ} (B : A → Type ℓ') : List A → Type (ℓ ⊔ ℓ') where
  [] : ListP B []
  _∷_ : ∀ {x xs} → B x → ListP B xs → ListP B (x ∷ xs)

private variable
  ℓ ℓ' : Level
  A X : Type ℓ
  B : A → Type ℓ
  C : (a : A) (b : B a) → Type ℓ

memberp
  : ∀ {a : A} {as : List A}
  → a ∈ₗ as
  → ListP B as
  → B a
memberp (here reflᵢ) (b ∷ _) = b
memberp (there p) (_ ∷ bs) = memberp p bs

instance
  ListP-[] : ListP B []
  ListP-[] = []

  ListP-∷
    : ∀ {x xs}
    → ⦃ _ : B x ⦄
    → ⦃ _ : ListP B xs ⦄
    → ListP B (x ∷ xs)
  ListP-∷ ⦃ bx ⦄ ⦃ bxs ⦄ = bx ∷ bxs

  Dec-ListP
    : ∀ {xs : List A}
    → ⦃ _ : ∀ {x} → Dec (B x) ⦄
    → Dec (ListP B xs)
  Dec-ListP {B = B} {xs = []} = yes []
  Dec-ListP {B = B} {xs = x ∷ xs} with holds? (B x) | holds? (ListP B xs)
  ... | yes bx | yes bxs = yes (bx ∷ bxs)
  ... | yes bx | no ¬bxs = no λ { (_ ∷ bxs) → ¬bxs bxs }
  ... | no ¬bx | _ = no λ { (bx ∷ _) → ¬bx bx }

Currying via classes

record Curried {ℓ} (A : Type ℓ) (ℓd : Level) (ℓf : Level) : Type (ℓ ⊔ lsuc ℓd ⊔ lsuc ℓf) where
  no-eta-equality
  field
    Dom : Type ℓd
    Fam : Dom → Type ℓf
    eqv : ((d : Dom) → Fam d) ≃ A

instance
  Curry-Π
    : ∀ {ℓ ℓ' ℓ'' ℓd ℓf} {A : Type ℓ} {B : A → Type ℓ'} {C : (a : A) → B a → Type ℓ''}
    → ⦃ _ : ∀ {a} → Curried ((b : B a) → C a b) ℓd ℓf ⦄
    → Curried ((a : A) (b : B a) → C a b) (ℓd ⊔ ℓ) ℓf
  Curry-Π {A = A} ⦃ c ⦄ .Curried.Dom = Σ[ a ∈ A ] (Curried.Dom (c {a}))
  Curry-Π {A = A} ⦃ c ⦄ .Curried.Fam (a , d) = Curried.Fam c d
  Curry-Π {A = A} ⦃ c ⦄ .Curried.eqv = curry≃ ∙e Π-ap-cod λ a → Curried.eqv c

  Curried-default
    : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'}
    → Curried ((a : A) → B a) ℓ ℓ'
  Curried-default {A = A} {B = B} .Curried.Dom = A
  Curried-default {A = A} {B = B} .Curried.Fam = B
  Curried-default {A = A} {B = B} .Curried.eqv = id≃
  {-# INCOHERENT Curried-default #-}

Case Bash

case-bash!
  : ∀ {ℓ ℓd ℓf} {Goal : Type ℓ}
  → ⦃ C : Curried Goal ℓd ℓf ⦄
  → ⦃ ds : Listing (Curried.Dom C) ⦄
  → ListP (Curried.Fam C) (Listing.univ ds)
  → Goal
case-bash! ⦃ C ⦄ ⦃ ds ⦄ proofs =
  Equiv.to (Curried.eqv C) (λ d → memberp (Listing.find ds d) proofs)

test : ∀ (x y z : Bool) → and x (and y z) ≡ and (and x y) z
test = case-bash! decide!