Grace/Cumulus/List/Sorted.g17

Open in Workbench Download source

Imports

Prefix

Declarations

Source

1-- Sorted lists of natural numbers: the head bounds the tail, sortedness2-- survives prefixes, suffixes, filters, and ordered concatenation,3-- insertion sort produces a sorted permutation, and a sorted arrangement4-- of given entries is unique5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.List.Sorted11import Prefix1213-- Entries are nondecreasing along positions.14predicate ListSorted (xs : Set) :=15  ∀ i, ∀ j, Nat(i) → Nat(j) → i < j → j < length{ℕ}(xs) → listCoefficient{ℕ}(0, xs, i) ≤ listCoefficient{ℕ}(0, xs, j)1617theorem ListSorted.nil18  shows ListSorted([])19proof20  unfold ListSorted21  intros i j iNat jNat below bound22  rw length.nil at bound23  exfalso24  arith2526theorem ListSorted.singleton (x : Nat)27  shows ListSorted(x :: [])28proof29  unfold ListSorted30  intros i j iNat jNat below bound31  have xIn : x ∈ ℕ := nat.omega.forward with *32  rw length.singleton at bound33  exfalso34  arith3536theorem ListSorted.head_le (a : Nat) (xs : List(ℕ))37  requires sorted : ListSorted(a :: xs)38  shows ∀ y ∈ listSupport{ℕ}(xs), a ≤ y39proof40  intros y hy41  have aIn : a ∈ ℕ := nat.omega.forward with *42  obtain ⟨k, kNat, bound, value⟩ := listSupport.mem_iff_index.forward at ℕ, 0, y, xs with hy43  have kSucc : Nat(succ(k)) by typecheck44  have positive : 0 < succ(k) by arith45  have inside : succ(k) < length{ℕ}(a :: xs)46    rw length.cons47    arith48  unfold ListSorted at sorted49  have step := sorted with 0, succ(k), Naturals.constructor.zero, kSucc, positive, inside50  rw [listCoefficient.zero, listCoefficient.succ, value] at step51  exact step5253theorem ListSorted.tail (a : Nat) (xs : List(ℕ))54  requires sorted : ListSorted(a :: xs)55  shows ListSorted(xs)56proof57  unfold ListSorted58  intros i j iNat jNat below bound59  have aIn : a ∈ ℕ := nat.omega.forward with *60  have iSucc : Nat(succ(i)) by typecheck61  have jSucc : Nat(succ(j)) by typecheck62  have belowSucc : succ(i) < succ(j) by arith63  have inside : succ(j) < length{ℕ}(a :: xs)64    rw length.cons65    arith66  unfold ListSorted at sorted67  have step := sorted with succ(i), succ(j), iSucc, jSucc, belowSucc, inside68  rw [listCoefficient.succ, listCoefficient.succ] at step69  exact step7071theorem ListSorted.cons (a : Nat) (xs : List(ℕ))72  requires head : ∀ y ∈ listSupport{ℕ}(xs), a ≤ y73  requires sorted : ListSorted(xs)74  shows ListSorted(a :: xs)75proof76  unfold ListSorted77  intros i j iNat jNat below bound78  have aIn : a ∈ ℕ := nat.omega.forward with *79  rw length.cons at bound80  have shapeJ := natural.zero_or_successor at j with jNat81  cases shapeJ with zeroJ | successorJ82  . rw zeroJ at below83    exfalso84    arith85  . obtain ⟨q, qNat, equalJ⟩ := successorJ86    rw equalJ at bound87    have insideQ : q < length{ℕ}(xs) by arith88    have memberQ := listCoefficient.mem_support at ℕ, 0, xs, q with insideQ89    have shapeI := natural.zero_or_successor at i with iNat90    cases shapeI with zeroI | successorI91    . rw [zeroI, equalJ, listCoefficient.zero, listCoefficient.succ]92      exact head with listCoefficient{ℕ}(0, xs, q), memberQ93    . obtain ⟨p, pNat, equalI⟩ := successorI94      rw [equalI, equalJ] at below95      have belowPQ : p < q by arith96      unfold ListSorted at sorted97      have step := sorted with p, q, pNat, qNat, belowPQ, insideQ98      rw [equalI, equalJ, listCoefficient.succ, listCoefficient.succ]99      exact step100101theorem ListSorted.cons_iff (a : Nat) (xs : List(ℕ))102  shows ListSorted(a :: xs) ↔ ((∀ y ∈ listSupport{ℕ}(xs), a ≤ y) ∧ ListSorted(xs))103proof104  constructor105  . intro sorted106    have head := ListSorted.head_le with sorted107    have tail := ListSorted.tail with sorted108    exact ⟨head, tail⟩109  . intro both110    obtain ⟨head, tail⟩ := both111    exact ListSorted.cons with head, tail112113theorem ListSorted.cons_cons_le (a b : Nat) (xs : List(ℕ))114  requires sorted : ListSorted(a :: b :: xs)115  shows a ≤ b116proof117  have bIn : b ∈ ℕ := nat.omega.forward with *118  have head := ListSorted.head_le with sorted119  have member := listSupport.mem_cons_self at ℕ, b, xs with bIn120  exact head with b, member121122theorem ListSorted.min_head (a : Nat) (xs : List(ℕ))123  requires sorted : ListSorted(a :: xs)124  shows ∀ y ∈ listSupport{ℕ}(a :: xs), a ≤ y125proof126  intros y hy127  have aIn : a ∈ ℕ := nat.omega.forward with *128  have head := ListSorted.head_le with sorted129  have split := listSupport.mem_cons_iff.forward with aIn, hy130  cases split with same | rest131  . rw same132    exact LessEqual.reflexive at a133  . exact head with y, rest134135theorem ListSorted.replicate (x : Nat) (n : Nat)136  shows ListSorted(listReplicate(n, x))137proof138  induction n139  | zero =>140    rw listReplicate.zero141    exact ListSorted.nil142  | succ(k) using ih =>143    have xIn : x ∈ ℕ := nat.omega.forward with *144    have list := listReplicate.closed at ℕ, x, k with xIn145    have head : ∀ y ∈ listSupport{ℕ}(listReplicate(k, x)), x ≤ y146      intros y hy147      have equal := listReplicate.mem_support with xIn, hy148      rw equal149      exact LessEqual.reflexive at x150    rw listReplicate.succ151    exact ListSorted.cons with head, ih152153theorem ListSorted.take (xs : List(ℕ)) (n : Nat)154  requires sorted : ListSorted(xs)155  shows ListSorted(listTake{ℕ}(n, xs))156proof157  induction xs generalizing n158  | List.nil =>159    intros n nNat sorted160    rw listTake.nil161    exact ListSorted.nil162  | List.cons(a, tail) using ih =>163    intros n nNat sorted164    have aIn : a ∈ ℕ by assumption165    have aNat := nat.omega.backward with aIn166    have shape := natural.zero_or_successor at n with nNat167    cases shape with zero | successor168    . have whole : List(ℕ, a :: tail) by typecheck169      rw [zero, listTake.zero]170      exact ListSorted.nil171    . obtain ⟨k, kNat, equal⟩ := successor172      have headAll := ListSorted.head_le with sorted173      have tailSorted := ListSorted.tail with sorted174      have inner := ih with k, kNat, tailSorted175      have taken := listTake.closed at ℕ, tail, k with *176      have subset := listTake.support_subset at ℕ, tail, k with *177      have head : ∀ y ∈ listSupport{ℕ}(listTake{ℕ}(k, tail)), a ≤ y178        intros y hy179        have member := subset with y, hy180        exact headAll with y, member181      rw [equal, listTake.succ_cons]182      exact ListSorted.cons with head, inner183184theorem ListSorted.drop (xs : List(ℕ)) (n : Nat)185  requires sorted : ListSorted(xs)186  shows ListSorted(listDrop{ℕ}(n, xs))187proof188  induction xs generalizing n189  | List.nil =>190    intros n nNat sorted191    rw listDrop.nil192    exact ListSorted.nil193  | List.cons(a, tail) using ih =>194    intros n nNat sorted195    have aIn : a ∈ ℕ by assumption196    have aNat := nat.omega.backward with aIn197    have shape := natural.zero_or_successor at n with nNat198    cases shape with zero | successor199    . have whole : List(ℕ, a :: tail) by typecheck200      rw [zero, listDrop.zero]201      exact sorted202    . obtain ⟨k, kNat, equal⟩ := successor203      have tailSorted := ListSorted.tail with sorted204      rw [equal, listDrop.succ_cons]205      exact ih with k, kNat, tailSorted206207theorem ListSorted.filter (S : Set) (xs : List(ℕ))208  requires sorted : ListSorted(xs)209  shows ListSorted(listFilter{ℕ}(S, xs))210proof211  induction xs212  | List.nil =>213    intro sorted214    rw listFilter.nil215    exact ListSorted.nil216  | List.cons(a, tail) using ih =>217    intro sorted218    have aIn : a ∈ ℕ by assumption219    have aNat := nat.omega.backward with aIn220    have headAll := ListSorted.head_le with sorted221    have tailSorted := ListSorted.tail with sorted222    have inner := ih with tailSorted223    have filtered := listFilter.closed at ℕ, S, tail with *224    have alternatives : a ∈ S ∨ ¬(a ∈ S) by tauto225    cases alternatives with member | absent226    . have subset := listFilter.support_subset at ℕ, S, tail with *227      have head : ∀ y ∈ listSupport{ℕ}(listFilter{ℕ}(S, tail)), a ≤ y228        intros y hy229        have inTail := subset with y, hy230        exact headAll with y, inTail231      rw listFilter.cons_member232      exact ListSorted.cons with head, inner233    . rw listFilter.cons_other234      exact inner235236theorem ListSorted.append (xs ys : List(ℕ))237  requires first : ListSorted(xs)238  requires second : ListSorted(ys)239  requires between : ∀ x ∈ listSupport{ℕ}(xs), ∀ y ∈ listSupport{ℕ}(ys), x ≤ y240  shows ListSorted(append(ys, xs))241proof242  induction xs243  | List.nil =>244    intros first between245    have ysList : List(ℕ, ys) by typecheck246    rw append.nil247    exact second248  | List.cons(a, tail) using ih =>249    intros first between250    have aIn : a ∈ ℕ by assumption251    have aNat := nat.omega.backward with aIn252    have headAll := ListSorted.head_le with first253    have tailSorted := ListSorted.tail with first254    have headIn := listSupport.mem_cons_self at ℕ, a, tail with aIn255    have restBetween : ∀ x ∈ listSupport{ℕ}(tail), ∀ y ∈ listSupport{ℕ}(ys), x ≤ y256      intros x hx y hy257      have outer := listSupport.mem_cons_of_mem with aIn, hx258      exact between with x, outer, y, hy259    have inner := ih with tailSorted, restBetween260    have appended := append.closed at ℕ, tail, ys with *261    have head : ∀ y ∈ listSupport{ℕ}(append(ys, tail)), a ≤ y262      intros y hy263      have split := listSupport.mem_append_iff.forward at ℕ, y, tail, ys with hy264      cases split with inTail | inYs265      . exact headAll with y, inTail266      . exact between with a, headIn, y, inYs267    rw append.cons268    exact ListSorted.cons with head, inner269270-- A sorted arrangement of given entries is unique.271theorem ListSorted.permutation_unique (xs ys : List(ℕ))272  requires first : ListSorted(xs)273  requires second : ListSorted(ys)274  requires permutation : ListPermutation(ℕ, xs, ys)275  shows xs = ys276proof277  induction xs generalizing ys278  | List.nil =>279    intros ys ysList first second permutation280    have back := ListPermutation.symmetric with permutation281    have empty := ListPermutation.nil with back282    rw empty283    rfl284  | List.cons(a, tail) using ih =>285    intros ys ysList first second permutation286    have aIn : a ∈ ℕ by assumption287    have aNat := nat.omega.backward with aIn288    have shape := List.cases with ysList289    cases shape with nil | cons290    . rw nil at permutation291      have empty := ListPermutation.nil with permutation292      have distinct := List.cons_ne_nil at ℕ, a, tail with aIn293      exfalso294      exact distinct with empty295    . obtain ⟨b, bIn, rest, restList, equal⟩ := cons296      have bNat := nat.omega.backward with bIn297      rw equal at permutation298      rw equal at second299      have headIn := listSupport.mem_cons_self at ℕ, a, tail with aIn300      have aInYs := ListPermutation.mem_support with permutation, headIn301      have back := ListPermutation.symmetric with permutation302      have headInYs := listSupport.mem_cons_self at ℕ, b, rest with bIn303      have bInXs := ListPermutation.mem_support with back, headInYs304      have minA := ListSorted.min_head with first305      have minB := ListSorted.min_head with second306      have aLeB := minA with b, bInXs307      have bLeA := minB with a, aInYs308      have same := LessEqual.antisymmetric with aLeB, bLeA309      rw ← same at permutation310      have tails := ListPermutation.cons_cancel with aIn, permutation311      have tailSorted := ListSorted.tail with first312      rw ← same at second313      have restSorted := ListSorted.tail with second314      have inner := ih with rest, restList, tailSorted, restSorted, tails315      rw [equal, ← same, inner]316      rfl317318-- Insertion into a sorted list, and insertion sort.319theorem memberTest.successor_le (x y : Nat)320  requires le : x ≤ y321  shows memberTest(succ(y), x) = Bool.true322proof323  have below : x < succ(y) by arith324  have member := membership.of_Less at x, succ(y) with *, below325  exact memberTest.true with member326327theorem memberTest.successor_gt (x y : Nat)328  requires gt : y < x329  shows memberTest(succ(y), x) = Bool.false330proof331  have absent : ¬(x ∈ succ(y))332    intro member333    have below := Less.of_membership at x, succ(y) with *, member334    have le := Less.successor_upper with below335    have strict : x < x by arith336    exact Less.irreflexive with *, strict337  exact memberTest.false with absent338339def listInsert (x : Nat, xs : List(ℕ)) → Set340  | x, [] => x :: []341  | x, y :: rest =>342    boolChoice(memberTest(succ(y), x), x :: y :: rest, y :: listInsert(x, rest))343344theorem listInsert.nil (x : Nat)345  shows listInsert(x, []) = x :: []346proof347  simp [listInsert]348349theorem listInsert.cons_le (x y : Nat) (rest : List(ℕ))350  requires le : x ≤ y351  shows listInsert(x, y :: rest) = x :: y :: rest352proof353  have test := memberTest.successor_le with le354  simp [listInsert, test, boolChoice]355356theorem listInsert.cons_gt (x y : Nat) (rest : List(ℕ))357  requires gt : y < x358  shows listInsert(x, y :: rest) = y :: listInsert(x, rest)359proof360  have test := memberTest.successor_gt with gt361  simp [listInsert, test, boolChoice]362363theorem listInsert.closed (x : Nat) (xs : List(ℕ))364  shows List(ℕ, listInsert(x, xs))365proof366  induction xs367  | List.nil =>368    have xIn : x ∈ ℕ := nat.omega.forward with *369    rw listInsert.nil370    typecheck371  | List.cons(y, rest) using ih =>372    have xIn : x ∈ ℕ := nat.omega.forward with *373    have yIn : y ∈ ℕ by assumption374    have yNat := nat.omega.backward with yIn375    have alternatives : x ≤ y ∨ ¬(x ≤ y) by tauto376    cases alternatives with le | notLe377    . rw listInsert.cons_le378      typecheck379    . have gt := Less.of_not_LessEqual at x, y with notLe380      rw listInsert.cons_gt381      typecheck382383theorem listInsert.permutation (x : Nat) (xs : List(ℕ))384  shows ListPermutation(ℕ, listInsert(x, xs), x :: xs)385proof386  induction xs387  | List.nil =>388    have xIn : x ∈ ℕ := nat.omega.forward with *389    rw listInsert.nil390    exact ListPermutation.reflexive at ℕ, x :: [] with *391  | List.cons(y, rest) using ih =>392    have xIn : x ∈ ℕ := nat.omega.forward with *393    have yIn : y ∈ ℕ by assumption394    have yNat := nat.omega.backward with yIn395    have inserted := listInsert.closed at x, rest with *396    have whole : List(ℕ, y :: rest) by typecheck397    have alternatives : x ≤ y ∨ ¬(x ≤ y) by tauto398    cases alternatives with le | notLe399    . rw listInsert.cons_le400      exact ListPermutation.reflexive at ℕ, x :: y :: rest with *401    . have gt := Less.of_not_LessEqual at x, y with notLe402      rw listInsert.cons_gt403      have step := ListPermutation.cons at ℕ, y, listInsert(x, rest), x :: rest with yIn, ih404      have swap := ListPermutation.swap at ℕ, y, x, rest with yIn, xIn405      exact ListPermutation.transitive with step, swap406407theorem listInsert.length (x : Nat) (xs : List(ℕ))408  shows length{ℕ}(listInsert(x, xs)) = succ(length{ℕ}(xs))409proof410  have xIn : x ∈ ℕ := nat.omega.forward with *411  have inserted := listInsert.closed at x, xs with *412  have whole : List(ℕ, x :: xs) by typecheck413  have permutation := listInsert.permutation at x, xs with *414  have lengths := ListPermutation.length with permutation415  rw [lengths, length.cons]416  rfl417418theorem listInsert.count (x z : Nat) (xs : List(ℕ))419  shows listCount{ℕ}(z, listInsert(x, xs)) = listCount{ℕ}(z, x :: xs)420proof421  have xIn : x ∈ ℕ := nat.omega.forward with *422  have inserted := listInsert.closed at x, xs with *423  have whole : List(ℕ, x :: xs) by typecheck424  have permutation := listInsert.permutation at x, xs with *425  exact ListPermutation.count with permutation426427theorem listInsert.support (x : Nat) (xs : List(ℕ))428  shows listSupport{ℕ}(listInsert(x, xs)) = insert(x, listSupport{ℕ}(xs))429proof430  have xIn : x ∈ ℕ := nat.omega.forward with *431  have inserted := listInsert.closed at x, xs with *432  have whole : List(ℕ, x :: xs) by typecheck433  have permutation := listInsert.permutation at x, xs with *434  have support := ListPermutation.support with permutation435  rw [support, listSupport.cons]436  rfl437438theorem listInsert.sorted (x : Nat) (xs : List(ℕ))439  requires sorted : ListSorted(xs)440  shows ListSorted(listInsert(x, xs))441proof442  induction xs443  | List.nil =>444    intro sorted445    rw listInsert.nil446    exact ListSorted.singleton at x with *447  | List.cons(y, rest) using ih =>448    intro sorted449    have xIn : x ∈ ℕ := nat.omega.forward with *450    have yIn : y ∈ ℕ by assumption451    have yNat := nat.omega.backward with yIn452    have inserted := listInsert.closed at x, rest with *453    have whole : List(ℕ, y :: rest) by typecheck454    have headAll := ListSorted.head_le with sorted455    have restSorted := ListSorted.tail with sorted456    have alternatives : x ≤ y ∨ ¬(x ≤ y) by tauto457    cases alternatives with le | notLe458    . rw listInsert.cons_le459      have head : ∀ z ∈ listSupport{ℕ}(y :: rest), x ≤ z460        intros z hz461        have split := listSupport.mem_cons_iff.forward with yIn, hz462        cases split with same | inRest463        . rw same464          exact le465        . have subset := listSupport.subset at ℕ, rest with *466          have zIn := subset with z, inRest467          have zNat := nat.omega.backward with zIn468          have yz := headAll with z, inRest469          exact LessEqual.transitive with le, yz470      exact ListSorted.cons with head, sorted471    . have gt := Less.of_not_LessEqual at x, y with notLe472      have inner := ih with restSorted473      rw listInsert.cons_gt474      have head : ∀ z ∈ listSupport{ℕ}(listInsert(x, rest)), y ≤ z475        intros z hz476        rw listInsert.support at hz477        have split := insert.membership.forward with hz478        cases split with same | inRest479        . rw same480          exact Less.implies_LessEqual with gt481        . exact headAll with z, inRest482      exact ListSorted.cons with head, inner483484def listInsertionSort (xs : List(ℕ)) → Set485  | [] => []486  | x :: rest => listInsert(x, listInsertionSort(rest))487488theorem listInsertionSort.nil489  shows listInsertionSort([]) = []490proof491  simp [listInsertionSort]492493theorem listInsertionSort.cons (x : Nat) (rest : List(ℕ))494  shows listInsertionSort(x :: rest) = listInsert(x, listInsertionSort(rest))495proof496  simp [listInsertionSort]497498theorem listInsertionSort.closed (xs : List(ℕ))499  shows List(ℕ, listInsertionSort(xs))500proof501  induction xs502  | List.nil =>503    rw listInsertionSort.nil504    typecheck505  | List.cons(x, rest) using ih =>506    have xIn : x ∈ ℕ by assumption507    have xNat := nat.omega.backward with xIn508    rw listInsertionSort.cons509    exact listInsert.closed at x, listInsertionSort(rest) with *510511theorem listInsertionSort.permutation (xs : List(ℕ))512  shows ListPermutation(ℕ, listInsertionSort(xs), xs)513proof514  induction xs515  | List.nil =>516    rw listInsertionSort.nil517    exact ListPermutation.reflexive at ℕ, [] with *518  | List.cons(x, rest) using ih =>519    have xIn : x ∈ ℕ by assumption520    have xNat := nat.omega.backward with xIn521    have sortedRest := listInsertionSort.closed at rest with *522    have inserted := listInsert.closed at x, listInsertionSort(rest) with *523    have consSorted : List(ℕ, x :: listInsertionSort(rest)) by typecheck524    rw listInsertionSort.cons525    have step := listInsert.permutation at x, listInsertionSort(rest) with *526    have consStep := ListPermutation.cons at ℕ, x, listInsertionSort(rest), rest with xIn, ih527    exact ListPermutation.transitive with step, consStep528529theorem listInsertionSort.sorted (xs : List(ℕ))530  shows ListSorted(listInsertionSort(xs))531proof532  induction xs533  | List.nil =>534    rw listInsertionSort.nil535    exact ListSorted.nil536  | List.cons(x, rest) using ih =>537    have xIn : x ∈ ℕ by assumption538    have xNat := nat.omega.backward with xIn539    have sortedRest := listInsertionSort.closed at rest with *540    rw listInsertionSort.cons541    exact listInsert.sorted with ih542543theorem listInsertionSort.length (xs : List(ℕ))544  shows length{ℕ}(listInsertionSort(xs)) = length{ℕ}(xs)545proof546  have sorted := listInsertionSort.closed at xs with *547  have permutation := listInsertionSort.permutation at xs with *548  exact ListPermutation.length with permutation549550theorem listInsertionSort.support (xs : List(ℕ))551  shows listSupport{ℕ}(listInsertionSort(xs)) = listSupport{ℕ}(xs)552proof553  have sorted := listInsertionSort.closed at xs with *554  have permutation := listInsertionSort.permutation at xs with *555  exact ListPermutation.support with permutation556557theorem listInsertionSort.count (x : Set) (xs : List(ℕ))558  shows listCount{ℕ}(x, listInsertionSort(xs)) = listCount{ℕ}(x, xs)559proof560  have sorted := listInsertionSort.closed at xs with *561  have permutation := listInsertionSort.permutation at xs with *562  exact ListPermutation.count with permutation563564theorem listInsertionSort.of_sorted (xs : List(ℕ))565  requires sorted : ListSorted(xs)566  shows listInsertionSort(xs) = xs567proof568  have list := listInsertionSort.closed at xs with *569  have resultSorted := listInsertionSort.sorted at xs with *570  have permutation := listInsertionSort.permutation at xs with *571  exact ListSorted.permutation_unique with resultSorted, sorted, permutation572573theorem listInsertionSort.idempotent (xs : List(ℕ))574  shows listInsertionSort(listInsertionSort(xs)) = listInsertionSort(xs)575proof576  have list := listInsertionSort.closed at xs with *577  have resultSorted := listInsertionSort.sorted at xs with *578  exact listInsertionSort.of_sorted with resultSorted579580theorem listInsertionSort.of_permutation (xs ys : List(ℕ))581  requires permutation : ListPermutation(ℕ, xs, ys)582  shows listInsertionSort(xs) = listInsertionSort(ys)583proof584  have leftList := listInsertionSort.closed at xs with *585  have rightList := listInsertionSort.closed at ys with *586  have leftSorted := listInsertionSort.sorted at xs with *587  have rightSorted := listInsertionSort.sorted at ys with *588  have left := listInsertionSort.permutation at xs with *589  have right := listInsertionSort.permutation at ys with *590  have rightBack := ListPermutation.symmetric with right591  have middle := ListPermutation.transitive with left, permutation592  have whole := ListPermutation.transitive with middle, rightBack593  exact ListSorted.permutation_unique with leftSorted, rightSorted, whole594