如果两个列表是排列的，那么写一个prooving的策略

Question

我是一个初学者，我想写一个策略来证明两个列表是否是排列。

例如，我想用来检查策略

Goal (Permutation (1::3::4::2::nil) (2::4::1::3::nil))

我已经编写了一个函数来对列表进行排序，并检查两个列表是否相等，但我在编写策略时遇到了一些麻烦。

你能帮我吗？

Answer 1

哦。我认为写一个策略是指写一个决策程序来自动化你的证明。我以为你指的是Coq.Sorting.Permutation中定义的Permutation关系。

如果你只是想证明你的列表是相互排列的，你可以这样做：

Definition Permutation : list nat -> list nat -> Prop :=
  fun l1 l2 => EqualS (sortL l1) (sortL l2).
Goal Permutation (1 :: 3 :: 4 :: 2 :: nil) (2 :: 4 :: 1 :: 3 :: nil).
Proof. lazy. tauto. Qed.

True的定义是

Inductive True : Prop :=
  | I : True.

如果你想证明一些更通用的东西，比如

forall n1 n2 n3 n4, Permutation (n1 :: n2 :: n3 :: n4 :: nil) (n4 :: n3 :: n2 :: n1 :: nil)

你必须首先证明一些关于你的函数的事实，比如

forall n1 n2 l1, sortL (n1 :: n2 :: l1) = sortL (n2 :: n1 :: l1)
forall n1 l1 l2, EqualS (n1 :: l1) (n1 :: l2) <-> EqualS l1 l2

你必须用这些重写。