The Coq mailing list

[Jake <jake.waksbaum AT gmail.com>]

When doing induction on Permutation, I often get stuck in the transitive case because my induction hypothesis is not of the correct form. Is there a trick one can use to avoid this issue?

The simplest example I can find that I've encountered recently is proving the following theorem about the equivalence of two definitions of stable permutations:

  Theorem perm_stable_stable_perm {A} `{E : EqDec A} : forall l l' : list A,

      Permutation l l' -> StableFilter l l' -> StablePerm l l'.

This is the form that I often have issues with: there is Permutation and some other information. In the transitive case, that other information isn't available in the right way. In this example, in the transitive case we have the following hypotheses:

  HP1 : Permutation l l'

  HP2 : Permutation l' l''

  IHHP1 : StableFilter l l' -> StablePerm l l'

  IHHP2 : StableFilter l' l'' -> StablePerm l' l''

  HS : StableFilter l l''

  ============================

  StablePerm l l''

From here, we're stuck because we need to know StableFilter l l' and StableFilter l' l'' to apply our induction hypotheses, but we simply cannot conclude that from HP1, HP2, and HS.

I've attached the full file with all the definitions. For this specific theorem, I have worked around this issue by doing induction on the length of the lists. However, this type of issue comes up a lot when I'm working the Permutation and StablePerm because they both have transitive cases. I'm curious if there is a good way of dealing with this this, because otherwise it severely reduces the usefulness of these inductive predicates by making induction on them difficult.

Attachment: Example.v
Description: Binary data