如何证明列表连接是不可交换的使用coq?

Question

对不起，我是新手。我想知道如何证明列表连接是不可交换的使用coq?

Answer 1

您只需要展示一个反例。例如:

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

像这样?

From Coq Require Import List.
Import ListNotations.
Goal [true] ++ [false] <> [false] ++ [true].
Proof. easy. Qed.