coq - 如何使用 coq 证明列表连接不可交换？

Question

抱歉，我是 coq 的新手。我想知道如何使用 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.