2
$\begingroup$

When I saw this question asking what is the "Hello, World!" for proof assistants I immediately thought of that exercise. Not a long time after this answer by Couchy was proposed.

Therefore, I am asking this question: How do I canonically define lists, append and prove its associativity in your favourite theorem prover?


Of course, you are encouraged to provide additional theorems which you think highlights an interesting feature/quirk of that particular theorem prover!

$\endgroup$
11
  • 2
    $\begingroup$ I think this is not a good question, but it does bring up something important: we need a proof assistants Rosetta stone. $\endgroup$ Feb 15, 2022 at 22:06
  • 1
    $\begingroup$ @AndrejBauer I agree about the latter, but that would make an even worse question. You may edit the question to open it up some more, but my fear is that it'll quickly gets subjective. $\endgroup$
    – Wno-all
    Feb 15, 2022 at 22:11
  • 2
    $\begingroup$ If we do allow questions like this, I would be inclined to make them community wiki. I'm not sure we should have them at all, though. $\endgroup$ Feb 16, 2022 at 1:08
  • 3
    $\begingroup$ I made a meta question for this issue. $\endgroup$ Feb 16, 2022 at 1:40
  • 5
    $\begingroup$ I’m voting to close this question because StackExchange sites are not the right format for such information. Note I do not say questions. See Meta question with my answer. In short consider GitHub pages or similar. $\endgroup$
    – Guy Coder
    Feb 16, 2022 at 8:53

1 Answer 1

3
$\begingroup$

Here's a little list module written in Adga. To do this we are going to need cong -rule, and it resides in PropositionalEquality -module.

module lists where
open import Relation.Binary.PropositionalEquality

Agda uses GADT-like syntax for its inductive types.

data List (a : Set) : Set where
  nil : List a
  cons : a → List a → List a

Here's the append, implemented by matching on the first argument. I defined it for an infix symbol to make it bit more convenient to describe associativity of append.

_++_ : {a : Set} → List a → List a → List a
_++_ nil ys = ys
_++_ (cons x xs) ys = cons x (xs ++ ys)

And here's the associativity property for append.

appendAssociative : {a : Set} → (xs ys zs : List a)
                  → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
appendAssociative nil ys zs = refl
appendAssociative (cons x xs) ys zs = cong (cons x) (appendAssociative xs ys zs)
$\endgroup$
4
  • 1
    $\begingroup$ Using the rewrite construct you can avoid importing the standard library just for one little cong. $\endgroup$
    – Trebor
    Feb 16, 2022 at 18:11
  • 1
    $\begingroup$ If you get into the habit of using rewrite a lot (and with too), you're setting yourself up for a lot of pain in the future. They both work, but don't scale all that well, at least in my experience. $\endgroup$ Feb 16, 2022 at 18:21
  • $\begingroup$ The standard library is also being used for _≡_. If you didn't import that, you'd have to define your own and bind it to the relevant builtin in order to use rewrite. You could alternatively avoid the builtin pragma by manually desugaring the rewrite to a with. $\endgroup$
    – James Wood
    Feb 16, 2022 at 22:49
  • $\begingroup$ @mudri _≡_ is builtin. If you look at stdlib closely, you will see that it merely re-exports Agda.Builtin.Equality. PS. if you don't include the @ sign I won't be notified. $\endgroup$
    – Trebor
    Feb 18, 2022 at 15:39

Not the answer you're looking for? Browse other questions tagged or ask your own question.