The Coq mailing list

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

I guess I didn't wrap my head around fully, but my counterexample should be valid.

Let me fix my premise: consider a setoid S, and x, y are in the same equivalence class, and x != y propositionally.

then the theorem you are trying to prove is not closed under transitivity because [x, y] => [y, x] => [x, y] is an example, so it cannot be established by direct induction.

Sincerely Yours,

Jason Hu

---

From: Jake <jake.waksbaum AT gmail.com>
Sent: March 14, 2019 11:26 PM
To: Jason -Zhong Sheng- Hu
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Induction on Permutation

 

Thanks for your response Jason! I think I wasn't clear about what I meant by stable. In the case you mentioned, because x != y, they can be swapped freely.

The stability I'm talking about is in reference to stable sorts, so we say that a permutation p is stable on a list xs when if i < j and xs[i] = xs[j] for some equivalence relation then p(i) < p(j). For sorts we define the equivalence relation by saying x = y iff x <= y and y <= x. So the fact that x != y means that the stability requirement doesn't care if they're swapped.

In fact, stability only really makes sense if we're using a notion of equivalence that isn't propositional equality because otherwise, even if two equal elements are swapped, we can't tell the difference between them. So under propositional equality every permutation is stable.

Please let me know if I've misunderstood your counterexample or if my explanation is unclear.

Thanks,

Jake

On Thu, Mar 14, 2019, 20:55 Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com> wrote:

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.