編寫一個策略，如果兩個列表是排列

我是一個初學者，我想寫一個策略來證明兩個列表是否是排列組合。編寫一個策略，如果兩個列表是排列

例如，我想與檢查策略：

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

我寫一個函數來排序列表，並檢查是否2所列出是平等的，但我有一些麻煩寫策略。

請問您能幫我嗎？

來源

2013-12-14 user3101909

請添加你的函數的代碼，以便人們可以幫助你 –

你不需要看代碼，我只是想知道如果兩個列表是排列組合，如何編寫一個策略來推動。我剛剛寫了2個函數： - listS列表返回排序列表l - 如果list1和list2相等，則相等list1 list2返回true else否false – user3101909

對於您的特定示例，您不需要策略。只需證明'to_prop（EqualL（listS l1）（listS l2）） - > Permutation l1 l2'，將其應用於目標，簡化並應用'I'。 'to_prop：bool - > Prop'。如果你的列表有變量，那是完全不同的故事。 – 2013-12-15 15:52:44

哦。通過寫一個策略，我認爲你的意思是寫一個決策程序來自動化你的證明。我想你是指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

，你就會有這些重寫。

來源

2013-12-16 13:33:23

非常感謝，這是我需要的！ ;） – user3101909

編寫一個策略，如果兩個列表是排列

回答

相關問題