Agda

Haskell based proof assistant.

Tips

• If you leave out a parameter to a module, that parameter becomes an argument to all top-level signatures.¹
  • useful for universe levels?
• If you’ve got a hole in your program, you can put the cursor in it and press C-c C-a, and Agda will try and find the automatic solution to the problem. For a while, I didn’t think much of this feature, as rare was the program which Agda could figure out. Turns out I was just using it wrong! Into the hole you should type the options for the proof search: enabling case-splitting (-c), enabling the use of available definitions (-r), and listing possible solutions (-l). ¹
• Well-Founded Recursion the order can be passed as a parameter to function. ¹
  • Another technique is using something like this: https://gallais.github.io/agdarsec/Induction.Nat.Strong.html
• Unification error solutions: ¹

What do you mean you’re not sure if there’s a case for the constructor proof: it’s the only case! The problem is that Agda is trying to unify two types who both have calls to user-defined functions in them, which is a hard problem. As phrased by Conor McBride:

When combining prescriptive and descriptive indices, ensure both are in constructor form. Exclude defined functions which yield difficult unification problems.

So if you ever get the “I’m not sure if…” error, try either to:

1. Redefine the indices so they use constructors, not functions.
2. Remove the index, instead having a proof inside the type of equality. What does that mean? Basically, transform the definition of ≤ above into the one in Data.Nat

• inspect is like with but gives a proof of equality as well as the value. ¹

f-is-the-same-as-g : ∀ x → f x ≡ g x
f-is-the-same-as-g x with f x | inspect f x
f-is-the-same-as-g x | y | [ fx≡y ] = {!!}

• Bindings:
  • SPC G G in spacemacs - go to definition
  • C-c C-n - normalize
• Irrelevance in Agda is difference to Coq, Haskell, and Idris.
  • In all cases it means a value doesn’t need to be arround at runtime.
  • In Idris it represents a values that doesn’t need to be stored, since they can be elided from other values, eg storing the length of a list.
  • In Agda, it means values where the actual value doesn’t need to be stored, eg. in storing proofs.
  • The agda irrelevance means it can’t be used in the Idris sense ¹

Footnotes

1. https://doisinkidney.com/posts/2018-09-20-agda-tips.html ↩ ↩² ↩³ ↩⁴ ↩⁵ ↩⁶