我有一些任务要做,但不知道该怎么做:
reverse, rev :: [a] [a]
reverse [] = []
reverse (x:xs) = reverse xs ++ [x]
rev = aux [] where
aux ys [] = ys
aux ys (x:xs) = aux (x:ys) xs
“证明:reverse=rev”
您的帮助将不胜感激。谢谢你。
PS。我可以用一些例子来做,但我认为那不专业
我有一些任务要做,但不知道该怎么做:
reverse, rev :: [a] [a]
reverse [] = []
reverse (x:xs) = reverse xs ++ [x]
rev = aux [] where
aux ys [] = ys
aux ys (x:xs) = aux (x:ys) xs
“证明:reverse=rev”
您的帮助将不胜感激。谢谢你。
PS。我可以用一些例子来做,但我认为那不专业
你可以通过结构归纳来做一个草率的证明,但如果你想要一个正确处理底部的证明,那就不那么简单了。
就职。基本情况是微不足道的。归纳步骤不应该太难。
我不会尝试直接证明等价性,而是会为每个函数证明(使用归纳法)它实际上反转了列表。如果它们都反转列表,则它们是等效的。
证明草图:
我们想证明 rev 适用于所有列表:
长度为 0 的 基本情况列表:证明 rev [] 计算正确
归纳案例:证明对于任何 n,rev 可以反转任何长度为 n 的列表,假设 rev 可以反转任何长度不超过 n-1 的列表
由于任何列表反转函数只能在给定有限列表的情况下产生任何输出,我们可以将此代码转换为 Coq(其中列表始终是有限的)并在那里证明所需的语句(忽略底部)。
这个证明不是我自己的——它是标准库证明的略微修改版本。
Open Scope list_scope.
Require List.
Require Import FunctionalExtensionality.
Section equivalence.
Variable A : Type.
(* The reverse function is already defined in the standard library as List.rev. *)
Notation reverse := (@List.rev A).
Fixpoint aux (ys l2 : list A) :=
match l2 with
nil => ys
| x :: xs => aux (x :: ys) xs
end.
Definition rev : list A -> list A
:= aux nil.
Lemma aux_rev : forall l l', aux l' l = reverse l ++ l'.
Proof.
induction l; simpl; auto; intros.
rewrite <- List.app_assoc; firstorder.
Qed.
Theorem both_equal : reverse = rev.
extensionality xs.
unfold rev.
rewrite aux_rev.
now rewrite List.app_nil_r.
Qed.
End equivalence.