open import 1Lab.Type.Pi.Currying
open import 1Lab.Prelude

open import Data.List.Quantifiers
open import Data.List.Membership
open import Data.Fin.Finite
open import Data.Bool.Base
open import Data.List.Base
open import Data.Dec.Base

module Data.Fin.CaseBash where

The case bash tacticπŸ”—

In the 1Lab, we try to strive for the most elegant proofs possible. Unfortunately, sometimes the most elegant proof really is a giant proof-by-cases. These proofs are enlightening to read and tedious to write, and are a prime candidate for proof automation.

Enter case-bash!. This tactic walks down a goal like and repeatedly case splits on each listable type in the domain, and which point it gathers all of the resulting goals into a dependent list.

Somewhat surprisingly, this can be implemented entirely using instance arguments! We first use the Curried typeclass to gather all of the arguments into a big Ξ£ type. We then use instance resolution to try and find a Listing of that Ξ£-type, which will attempt to resolve Listing instances for all of the components. We then require proofs of the curried codomain for every single element in the listing of the curried codomain.

case-bash!
  : βˆ€ {β„“ β„“d β„“f} {Goal : Type β„“}
  β†’ ⦃ C : Curried Goal β„“d β„“f ⦄
  β†’ ⦃ ds : Listing (Curried.Dom C) ⦄
  β†’ All (Curried.Cod C) (Listing.univ ds)
  β†’ Goal

The type of the function is honestly more complicated then it’s implementation, which just curries and then looks up proofs in a list.

case-bash! ⦃ C ⦄ ⦃ ds ⦄ proofs =
  Equiv.to (Curried.eqv C) (Ξ» ix β†’ all-∈ proofs (Listing.find ds ix))

ExamplesπŸ”—

Now that we have our tactic, let’s see some examples. The following bit of code proves commutativity of and via case-bash!.

private
  and-comm-via-case-bash : βˆ€ (x y : Bool) β†’ and x y ≑ and y x
  and-comm-via-case-bash = case-bash! (refl ∷ refl ∷ refl ∷ refl ∷ [])

We can avoid writing a giant list of refl by using even more proof automation. The decide! tactic lets us use Dec instances to prove goals, and All has a Dec instance that tries to decide some predicate for every element of the list. This means that we can combine case-bash! and decide! to discharge the entire list of goals in one go, provided that every goal is decidable.

private
  and-assoc-via-case-bash : βˆ€ (x y z : Bool) β†’ and x (and y z) ≑ and (and x y) z
  and-assoc-via-case-bash = case-bash! decide!