Insertion sort and its properties. A bug in MergeSort.agda is fixed. #2723
Conversation
|
So the |
Luckily, the diffs are the only modification to fix the bug mentioned. The bug is: mergesort used a DecTotalOrder to sort, whose underlying equality is not propositional. Before modification, the permutation property only works for a DecTotalOrder with propositional equality, but now any setoid equivalence. |
Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
| } | ||
|
|
||
| ------------------------------------------------------------------------ | ||
| -- Congruence properties |
There was a problem hiding this comment.
Hmm, now I notice that usually such things would be in Data.List.Sort.InsertionSort.Properties rather than directly in the main file.
There was a problem hiding this comment.
Yes, I agree. Same prolem with Mergesort. Ideally, all properties goes to the "*.Properties" file, such as "Sorted properties" and "Permutation properties" , not only the "Congruence properties". Should we split them? On the other hand, InsertionSort only has less than 200 loc, it seems kinda too dogmatic to split such a small file.
There was a problem hiding this comment.
There are properties needed to define Algorithm that can stay here, and then the ones after, which should move. But I'm fine with all of them moving.
The file is currently short. But these things have a way of continually expanding. May as well set a good example as early as possible.
There was a problem hiding this comment.
agreed and done for two sorting algorithms.
|
|
|
|
||
| -- But the induction over xs ↭ ys is hard to do for the "transitive" | ||
| -- constructor. So instead we have a similar property that depends on | ||
| -- the particular sorting algorithm used. |
There was a problem hiding this comment.
As you say in the comment, this isn't really the form of the two lemmas we want to prove. Yes, the transitive constructor makes the proof hard, but its not impossible to do.
I'd really prefer to have the correct lemma in the library, rather than the "wrong" one that we have to go to the faff of removing later...
If the full lemma is too hard to prove, then I suggest we simply remove these two lemmas.
There was a problem hiding this comment.
I have tried to prove the full lemma using the current permutation definition, but failed. Issue #2311 started one year ago was trying to fix the definition, but not ready yet.
Ignore the comment for a moment, the property sort-cong-↭ is just a congruence for sort, which itself as a property for sort should be there, but it is implied by the full lemma. Can we change the proof of sort-cong-↭ later and keep this property now? I also have subsequent developement depending on the decidability of permutation. If not, I have no problem removing them.
There was a problem hiding this comment.
@onestruggler I've proved the general lemma
↗↭↗⇒≋ : ∀ {xs ys} → Sorted O xs → Sorted O ys → xs ↭ ys → xs ≋ ysin the branch sorting-perm-equality2. A PR will be incoming in the next few days, so can you remove these lemmas from your PR. You can then add any extra results you need based on the new lemma in a new PR?
There was a problem hiding this comment.
The "property1 : ∀ {xs ys} → xs ~ ys → Sorted xs → Sorted ys → xs ≋ ys" is still hard to prove using the new definition in #2726 . Induction over ⋎ cannot go through, becasue I need "b ∷ cs" to be sorted in order to call IH on it. It is unreasonable to ask "b ∷ cs" to be sorted.
There was a problem hiding this comment.
If you squint at the following line in the new def of permuation in #2726
⋎ : as ∼ b ∷ cs → a ∷ cs ∼ bs → a ∷ as ∼ b ∷ bs
this line is essentially transitivity (plus swap): as ~ cs -> cs ~ bs -> as ~ bs.
The reason we cannot get rid of transitivity is that transitivity is composition of permutations. We cannot list all N! permutations in our inductive data type, we can only choose some generators, e.g. right now all swaps (transpositions) (we know transpositions generates all permuations) , so we have to compose generators to get all permutations. So transitivity is non-elimable. So induction proof can never avoid transivity, hence hard to go through.
This suggests the "full lemma" as called by Matt is hard to prove using whatever defs of permutations. Hence the not-so-full lemma depending on a particular sorting algorithm seems the only way to do it.
There was a problem hiding this comment.
@onestruggler I've proved the general lemma
↗↭↗⇒≋ : ∀ {xs ys} → Sorted O xs → Sorted O ys → xs ↭ ys → xs ≋ ysin the branch
sorting-perm-equality2. A PR will be incoming in the next few days, so can you remove these lemmas from your PR. You can then add any extra results you need based on the new lemma in a new PR?
Yes, I am going to make a new PR later. Your proof is impressive! Thanks.
There was a problem hiding this comment.
@onestruggler thanks for the comments on #2726 suggest we move the discussion there? But yes, the merge constructor indeed incorporates some transitivity, but in a more constrained way, moreover list cs is shorter than as or bs (which drives the proof of full transitivity)
There was a problem hiding this comment.
Hi @jamesmckinna , sure, let's move to #2726 after this post. Matt has a proof that avoids induction over transitivity, so different defs for permutation is no longer urgent for proving the "full lemma". But simple defs is definitely preferable.
|
Also needs a CHANGELOG entry. |
There was a problem hiding this comment.
Ah also I've just realised a really crucial point! The permutations were propositional based because that is actually the stronger result than them being setoid based permutations!
Please can you revert the changes back so that they are propositional permutations! (and of course remove that statement from the CHANGELOG!)
|
It might be good to add a comment as well explaining why the proofs are propositional based. Note that it is very easy to convert from propositional permutation to setoid-based permutation (but not the other way around!) |
I must misundertand something. I think setoid-based sorting is more general (stronger) than propositional based. If you want to sort propositionally you just use a DecTotalOrder whose underlying equivalence is propositional. Then you use the following to get to the "real propsitional": But if you only have propositional sorting, you cannot sort setoidly. Every propositional equality is a setoid. You can always turn propostional equaltiy into a setoid equivalence by refl but not visa vera, that is setoid is more general. |
The crucial thing is that sorting should preserve the elements in the list right? Even if you are using a setoid based For example, imagine sorting unnormalised rationals quotiented over by the setoid in the obvious way (e.g. 1/2 = 2/4 in the setoid). If you say that sorting only needs to return a setoid-based permutation then legally Crucially, it's actually impossible for the sorting algorithm to do that as the way we have created the interface, it is impossible to mutate the elements of the list at all as the interface is entirely generic as to the carrier set being passed in. |
|
Very interesting discussions... who knew insertion sort still had things to teach us!? |
Yes, it should preserve elements. But if I used a setoid based
In a setoid, 1/3 is 123/369, the return looks good to me. Also, at least for insertion sort, it does not change the elements whatsoever: it compares and puts everything back. The old interface cannot sort unnormalised rationals (because the underlying equivalence is non-propositional equivalence), but can sort normalised rationals (because the underlying equivalence is propositional equality), while the new sort can sort both. When the new one sorts normalised rationals, it behaves the same as the old one (guarantted by ↭ₛ⇒↭ : ↭ₛ ⇒ ↭ ). That is the new one is stronger. I need to hear more voices on this: @JacquesCarette @jamesmckinna @larrytheliquid |
|
I'm now in meetings for the rest of the day, but lots of food for thought regarding |
This is beside the point.
Really, a sorting algorithm that magically changes 1/3 to 123/369 looks good to you?
Yes, exactly! That's my point! It's impossible to write a generic sorting algorithm that changes the elements. Hence this should be reflected in the type signature.
This is not true. With the current interface you can pass in the total order over unnormalised rationals which uses the setoid-based equality and then derive both the setoid and the non-setoid permutation result: open import Data.Rational.Unnormalised
open import Data.Rational.Unnormalised.Properties
open import Data.List
open import Data.List.Sort ≤-decTotalOrder
import Data.List.Relation.Binary.Permutation.Homogeneous as Homo
import Data.List.Relation.Binary.Permutation.Setoid ≃-setoid as Setoid
import Data.List.Relation.Binary.Permutation.Propositional as Prop
l : List ℚᵘ
l = 1ℚᵘ ∷ 0ℚᵘ ∷ []
sl : List ℚᵘ
sl = sort l
sorted-prop-↭ : sl Prop.↭ l
sorted-prop-↭ = sort-↭ l
sorted-setoid-↭ : sl Setoid.↭ l
sorted-setoid-↭ = Homo.map ≃-reflexive (Prop.↭⇒↭ₛ (sorted-prop-↭))So challenge for you. Can you derive |
I finally see your point. Thanks for the clarification. I indeed misunderstood it. I apologize for being stupid. In some sense, for sorting, the setoid equivalence in a DecTotalOrder is never used, in other words, in some sense, in the eyes of sorting, any DecTotalOrder is always propostional-based. (the sentence before is just a vague idea, please do not take it literally). So restricting to propostional permutation loses nothing and is indeed stronger than setoid permutation (as the challenge shows, you can never recover propostional equality from setoid equivalence). This should be documented in case of someone like me misunderstand it again. |
|
Glad it was sorted (ahem) out. Yes, this is super subtle. Happy to help document -- but where? I guess it doesn't matter as much as to where we put pointers to such documentation, so that you might have seen it while doing this work. |
Besides the sorted and permutation peroperties, we also proved a congruence between permutation relation and pointwise relation on lists. And then we prove permuation relation is decidable.