[Agda] Path to success with Agda?

[Andrew Pitts]

> On 30 Aug 2022, at 00:02, Ignat Insarov <kindaro at gmail.com> wrote:
> 
> Cool, let us dig in!

Personally, Agda’s implementation of dependent pattern matching was what got me using Adga rather than Coq when I first needed to use one of these systems (Lean was not an option at the time). Stick with it — it’s great, honestly. 

But I sympathise about your problems with “with” (and was interested to read Peter Hancock’s confession). It can be very annoying in the middle of a big proof to try to work around why a particular use of “with” won’t type check.

So I wanted to mention the humble “case” expression, which functional programmers can more easily relate to, maybe. It’s less powerful that “with”, but sometimes works (wrt the not typechecking thing) when “with” won’t.

It’s not a built-in, so one is just disguising “ordinary” Type Theory with some user-defined syntax. For example, defining

open import Agda.Primitive public
case :
  {l m : Level}
  {A : Set l}
  {B : A → Set m}
  (x : A)
  (f : (x : A) → B x)
  → -----------------
  B x
case x f  = f x

then the first example of “with” at <https://agda.readthedocs.io/en/latest/language/with-abstraction.html> becomes

open import Agda.Builtin.Bool public
open import Agda.Builtin.List public
filter : {A : Set} → (A → Bool) → List A → List A
filter p [] = []
filter p (x ∷ xs) = case (p x) \{
  true  → x ∷ filter p xs ;
  false → filter p xs     }

(of course you can write λ rather than \ if you prefer).

Andy