I'm trying to build a proof in Coq that two different permutation definitions are equivalent, but the non-inductive side is not working

Question

The two definitions are these:

Inductive perm : list nat -> list nat -> Prop :=

| perm_eq: forall l1, perm l1 l1

| perm_swap: forall x y l1, perm (x :: y :: l1) (y :: x :: l1)

| perm_hd: forall x l1 l2, perm l1 l2 -> perm (x :: l1) (x :: l2)

| perm_trans: forall l1 l2 l3, perm l1 l2 -> perm l2 l3 -> perm l1 l3.

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

Definition equiv l l' := forall n:nat, num_oc n l = num_oc n l'.

The theorem that I'm trying to prove is this:

Theorem perm_equiv: forall l l', equiv l l' <-> perm l l'.

The perm -> equiv direction is ready, but the equiv -> perm direction isn't working. I tried this strategy:

- intro H. unfold equiv in H.
    generalize dependent l'.
    induction l.
    + intros l' H. admit.
    + intros l' H. simpl in H.

      generalize dependent l'.

      intro l'. induction l'.

      * intro H. specialize (H a).

        rewrite <- beq_nat_refl in H.

        simpl in H. Search False.

        inversion H.

        destruct (a =? a0) eqn:Ha.

        ** simpl in H. inversion H.

        ** apply False_ind.

           apply beq_nat_false in Ha.

           apply Ha. reflexivity. 

      * destruct (x =? a). *).

I'm out of ideas for the first branch, so it's admitted for now, but the second one is crashing at the destruct tactic. How do I proceed with this proof?

Answer 1

You should attempt to write a proof on paper before attempting to encode it in Coq. Here is a possible strategy.

Nil case

When l = [], you know that every number in l' occurs zero times because of H. It should be possible to prove an auxiliary lemma that implies that l' = [] in this case. You can conclude with perm_eq.

Cons case

Suppose that l = x :: xs. Let n = num_oc x xs. We know that num_oc x l' = S n by H. You should be able to prove a lemma saying that l' is of the form ys1 ++ x :: ys2 where num_oc x ys1 = 0. This would allow you to show that equiv xs (ys1 ++ ys2). By the induction hypothesis, you find that perm xs (ys1 ++ ys2). Hence, by perm_hd, perm (x :: xs) (x :: ys1 ++ ys2).

You should be able to prove that perm is a transitive relation and that perm (x :: ys1 ++ ys2) (ys1 ++ x :: ys2) holds. Combined with the last assertion, this will yield perm l l'.

---

The main takeaway in this case is that attempting to write every proof with single, direct induction is only going to work for the simplest results. You should start thinking about how to break down your results into simpler intermediate lemmas that you can combine to prove your final result.