1. Lab 01: Setup (30/1/2023).
  2. Lab02: Selection Sort (part 1) and `≤` on `Answer` (6/2/2023).
  3. Lab03 Selection Sort (part 2) (13/2/2023).
  4. Vectors: Equivalence of definitions (20/3/2023).

Lab03 Selection Sort (part 2)

due by Monday, Feb 13, 2023

Before doing this assignment you will need to pull from the upstream repository, i.e., the course repository. Please complete the definitions/proofs in the file PnP2023/Labs/Lab03/SelectionSort.lean. When you are done please commit and push your changes to your forked private repository and alert me on Zulip.

  1. Complete the proof of selectionSort_mem_of_mem in PnP2023/Labs/Lab03/SelectionSort.lean.

  2. Complete the proof of selectionSort_mem_mem in PnP2023/Labs/Lab03/SelectionSort.lean.

  3. Complete the proof of selectionSort_sorted in PnP2023/Labs/Lab03/SelectionSort.lean.