Idiomatic way to use Ord Typeclass to get Bools?

Stream: new members

[Agnishom Chattopadhyay]

I have written the following code:

def quicksort {a : Type}
  [LT a] [forall (x y : a), Decidable (x < y)]
  [LE a] [forall (x y : a), Decidable (x ≤ y)]
  : List a → List a
  | [] => []
  | x :: xs =>
      (
      have : List.length (xs.filter (fun y => decide (y < x))) < List.length (x :: xs) := by {
        simp [List.length]
        apply Nat.lt_succ_of_le
        apply List.length_filter_le
      }
      quicksort (xs.filter (fun y => decide (y < x)))
      )
      ++ [x] ++
      (
      have : List.length (xs.filter (fun y => decide (x ≤ y))) < List.length (x :: xs) := by {
        simp [List.length]
        apply Nat.lt_succ_of_le
        apply List.length_filter_le
      }
      quicksort (xs.filter (fun y => decide (x ≤ y)))
      )
  termination_by
    quicksort xs => xs.length
  decreasing_by
    simp_wf
    simp_all

#eval quicksort [3, 4, 2, 1]
-- prints [1, 2, 3, 4]

Is there a way to write the {a : Type} [LT a] [forall (x y : a), Decidable (x < y)] [LE a] [forall (x y : a), Decidable (x ≤ y)] declaration in a more idiomatic way? I know that there is a Ord a typeclass, but it is not clear to me why it doesn't automatically inherit LT or LE

[Agnishom Chattopadhyay]

Does anyone have any suggestions on improving this code?

[Eric Wieser]

You could use docs#LinearOrder, which inherits from LT and LE and Ord simultaneously.

[Eric Wieser]

Quick sort only makes sense on linear orders anyway, IIRC.

[Alex J. Best]

You could have distinct elements that compare to equal and sensibly run quicksort perhaps?

[Alex J. Best]

You could also use (x ≤ ·) in place of fun y => decide (...) it should turn out to be the same thing

[Alex J. Best]

Also we try to avoid non-terminal simp calls, as they are liable to break when the library you are using is changed, so we replace them with the output of simp?

[Agnishom Chattopadhyay]

Eric Wieser said:

You could use docs#LinearOrder, which inherits from LT and LE and Ord simultaneously.

Thanks. That seems to be the right typeclass that I am looking for

def quicksort2 {a : Type} [LinearOrder a] : List a → List a
  | [] => []
  | x :: xs =>
      (
      have : List.length (xs.filter (. < x)) < List.length (x :: xs) := by {
        simp [List.length]
        apply Nat.lt_succ_of_le
        apply List.length_filter_le
      }
      quicksort2 (xs.filter (. < x))
      )
      ++ [x] ++
      (
      have : List.length (xs.filter (x ≤ .)) < List.length (x :: xs) := by {
        simp [List.length]
        apply Nat.lt_succ_of_le
        apply List.length_filter_le
      }
      quicksort2 (xs.filter (x ≤ .))
      )
  termination_by
    quicksort2 xs => xs.length
  decreasing_by
    simp_wf
    simp_all

[Agnishom Chattopadhyay]

Alex J. Best said:

You could have distinct elements that compare to equal and sensibly run quicksort perhaps?

Yes, true. Is there a way to refer to this kind of equality?

Another way to have this kind of a function would be to modify the signature of quicksort to

quicksort_by {a b : Type} (f : b -> a) [LinearOrder a] : List b -> List b

[Agnishom Chattopadhyay]

Alex J. Best said:

Also we try to avoid non-terminal simp calls, as they are liable to break when the library you are using is changed, so we replace them with the output of simp?

Thanks, that is a great point. How do I do this?

The output of simp [List.length] seems to be

List.length (List.filter (fun x_1 => decide (x_1 < x)) xs) < List.length xs + 1

[Alex J. Best]

Well I think your original version already allowed for that, by not assuming antisymmetry of LE the LE relation could be weaker than in a linear order and hence be something like (a,b) \le (c,d) \iff a \le c or some such, allowing to sort on a key without comparing the elements for equality

[Alex J. Best]

All you really need it rw [List.length_cons] not simp [List.length] btw

[Eric Wieser]

Agnishom Chattopadhyay said:

The output of simp [List.length] seems to be

List.length (List.filter (fun x_1 => decide (x_1 < x)) xs) < List.length xs + 1

You should be looking at the output of simp? [List.length], not the goal state afterwards