Defining Lists and Prove Associativity of Append [closed]

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!

• I think this is not a good question, but it does bring up something important: we need a proof assistants Rosetta stone. Commented Feb 15, 2022 at 22:06
• @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. Commented Feb 15, 2022 at 22:11
• 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. Commented Feb 16, 2022 at 1:08
• I made a meta question for this issue. Commented Feb 16, 2022 at 1:40
• 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. Commented Feb 16, 2022 at 8:53

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)

• Using the rewrite construct you can avoid importing the standard library just for one little cong.
– Trebor
Commented Feb 16, 2022 at 18:11
• 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. Commented Feb 16, 2022 at 18:21
• 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. Commented Feb 16, 2022 at 22:49
• @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.
– Trebor
Commented Feb 18, 2022 at 15:39