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

Link:: https://stackoverflow.com/q/71083370

Display all goals and responses

Question

I need to prove that a secondary definition of permutation is equivalent to the default definition of permutation in Coq:

Down bellow is the default Permutation definition in 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''.

I need to prove that the above mentioned definition is equivalent to the following definition:

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

Which as you have noticed uses the definition occurences_number down bellow:

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.

What I need to prove indeed is the following:

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

Down bellow is my incomplete proof

Proof.forall l l' : list A, Permutation l l' -> perm l l'
  induction l.forall l' : list A, Permutation [] l' -> perm [] l'
a: A
l: list A
IHl: forall l' : list A, Permutation l l' -> perm l l'
forall l' : list A,
Permutation (a :: l) l' -> perm (a :: l) l'
  -forall l' : list A, Permutation [] l' -> perm [] l' admit.
  -a: A
l: list A
IHl: forall l' : list A, Permutation l l' -> perm l l'
forall l' : list A,
Permutation (a :: l) l' -> perm (a :: l) l' intros l' Hequiv.a: A
l: list A
IHl: forall l' : list A, Permutation l l' -> perm l l'
l': list A
Hequiv: Permutation (a :: l) l'
perm (a :: l) l'
    generalize dependent a.l: list A
IHl: forall l' : list A,
Permutation l l' -> perm l l'
l': list A
forall a : A,
Permutation (a :: l) l' -> perm (a :: l) l'
    generalize dependent l.l': list A
forall l : list A,
(forall l' : list A, Permutation l l' -> perm l l') ->
forall a : A,
Permutation (a :: l) l' -> perm (a :: l) l'
    case l'.l': list A
forall l : list A,
(forall l' : list A, Permutation l l' -> perm l l') ->
forall a : A,
Permutation (a :: l) [] -> perm (a :: l) []
l': list A
forall (a : A) (l l0 : list A),
(forall l' : list A, Permutation l0 l' -> perm l0 l') ->
forall a0 : A,
Permutation (a0 :: l0) (a :: l) ->
perm (a0 :: l0) (a :: l)
    +l': list A
forall l : list A,
(forall l' : list A, Permutation l l' -> perm l l') ->
forall a : A,
Permutation (a :: l) [] -> perm (a :: l) [] Admitted.

A (Arthur Azevedo De Amorim): It is probably easier to do induction on the hypothesis Permutation l l' instead of l.

Q: What do you mean @ArthurAzevedoDeAmorim?

A (Arthur Azevedo De Amorim): In Coq, you can do induction not only on data structures, but also on hypotheses that state inductively defined propositions. If you are not familiar with this concept, I recommend having a look at the Software Foundations book: https://softwarefoundations.cis.upenn.edu/lf-current/IndProp.html#lab216

Answer (Arthur Azevedo De Amorim)

Here is a proof that follows the strategy I outlined above:

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