How to prove list concatenation is not commutative using coq?

Question

Sorry I am new to coq. I'm wondering how to prove list concatenation is not commutative using coq?

Answer 1

You just need to exhibit a counterexample. For instance:

Require Import Coq.Lists.List.
Import ListNotations.

Theorem list_app_is_not_commutative :
  ~ (forall A (l1 l2 : list A), l1 ++ l2 = l2 ++ l1).
Proof.
intros H.
specialize (H bool [true] [false]).
simpl in H.
congruence.
Qed.

Answer 2

Like this ?

From Coq Require Import List.

Import ListNotations.

Goal [true] ++ [false] <> [false] ++ [true].
Proof. easy. Qed.