The Coq mailing list

[Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>]

Hi Jake,

I didn't look deep into your problem, but I guess I can try to explain why this proof cannot work.

Consider the following list, [x, y]. For the sake of it, let's forget about setoids and just work with propositional equality. Let x != y in this case.

I can definitely conclude [x, y] is both a permutation and a stable permutation of itself.

Now consider use of transtivity, which goes like this,

[x, y] => [y, x] => [x, y]

Clearly, [x, y] and [y, x] are not stable. The fact that you can apply a stable filter to the end results doesn't prevent the internal structure of permutation from violating it, so the theorem is simply not closed under transitivity and you cannot prove such fixpoint exists.

Hope that makes sense. I have no idea how to prove your particular theorem without looking into it. Sorry about that. My wild guess is StableFilter is a too shallow restriction on the lists, and therefore something stronger might help.

Sincerely Yours,

Jason Hu

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Jake <jake.waksbaum AT gmail.com>
Sent: March 14, 2019 8:32 PM
To: coq-club AT inria.fr
Subject: [Coq-Club] Induction on Permutation

 

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.