如何证明另一个排列定义与 COQ 的默认排列库相同

Question

我需要证明置换的二级定义等价于 Coq 中置换的默认定义：

下面是 Coq 中的默认排列定义

Inductive Permutation : list A -> list A -> Prop :=
| perm_nil: Permutation [] []
| perm_skip x l l' : Permutation l l' -> Permutation (x::l) (x::l')
| perm_swap x y l : Permutation (y::x::l) (x::y::l)
| perm_trans l l' l'' :
    Permutation l l' -> Permutation l' l'' -> Permutation l l''.

我需要证明上面定义等价于下面的定义：

Definition perm l l' := forall x, occurences_number x l = occurences_number x l'.

正如您所注意到的，下面使用了定义 occurences_number：

Fixpoint occurences_number x l := match l with
                       | nil => 0
                       | h::tl => if (x =? h) then S(occurences_number x tl) else occurences_number x tl
                       end.

我需要证明的是：

Lemma permutation_to_perm: forall l l', Permutation l l' -> perm l l'.

下面是我不完整的证明

Proof.
 induction l.
 - admit.
 - intros l' Hequiv.
   generalize dependent a.
   generalize dependent l.
   case l'.
   + Admitted.

Answer 1

这是遵循我上面概述的策略的证明：

Lemma Permutation_to_perm l l' : Permutation l l' -> perm l l'.
Proof.
intros H. induction H as [| x l1 l2 _ IH | x y l | l1 l2 l3 _ IH1 _ IH2 ].
- intros ?; reflexivity.
- intros y. simpl. now rewrite IH.
- intros z. simpl. now destruct (z =? y), (z =? x).
- intros ?. now rewrite IH1.
Qed.

如何证明另一个排列定义与 COQ 的默认排列库相同

How to prove that another definition of permutation is the same as the Default Permutation Library for COQ

proof

permutation

coq

induction