-- Project: Sorting
--
-- Math 4680/5680, "Topics in Logic and Computation"
-- Fall 2026
--
-- Name: _______________________
--
-- ============================================================
--
-- Projects must be done individually. You may not collaborate with
-- other students, and you may not use AI tools. If you have questions
-- or are stuck, ask the instructor.
--
-- You may use, among other things, `rfl`, the equality rules from
-- Lecture 8 (including `▸` and `calc`), and the basic lemmas in `Nat`
-- about `≤` and `<` (type `Nat.le_` or `Nat.lt_` to explore them).
--
-- In some places, you will need additional lemmas. Some are suggested
-- below. Please state and prove your own lemmas as appropriate.
--
-- For full marks, complete Parts 1-4. Part 5 is a bonus.
--
-- ============================================================

set_option autoImplicit false
set_option linter.unusedVariables false

namespace Project_Sorting

-- ============================================================
-- Introduction
--
-- A sorting algorithm takes a list, such as `[3, 1, 4, 1, 5]`, and
-- rearranges it into increasing order: `[1, 1, 3, 4, 5]`. Sorting
-- algorithms are among the most-used programs in the world, so it is
-- important to know that they work. But what does it mean for a
-- sorting algorithm to be _correct_? Two things:
--
--   (a) the output is sorted, and
--   (b) the output is a rearrangement (a permutation) of the input.
--
-- Note that neither condition alone is enough: the function that
-- always returns `[]` satisfies (a), and the identity function
-- satisfies (b).
--
-- In this project, we define one of the simplest sorting algorithms,
-- insertion sort. We then define "sorted" and "permutation" as
-- inductive predicates, and prove that insertion sort is correct.
-- This is an example of a _verified algorithm_: an algorithm together
-- with a proof that it does what it is supposed to do.

-- ============================================================
-- Insertion sort
--
-- Insertion sort is how many people sort a hand of playing cards:
-- pick up the cards one at a time, and insert each new card into its
-- correct place among the cards already in your hand.
--
-- The basic operation is `insert x l`, which inserts the number `x`
-- into the list `l`. It walks along `l`, and puts `x` in front of the
-- first element that is at least as large as `x`. (If there is no
-- such element, `x` goes at the end.) If `l` is sorted, then so is
-- the result.

def insert (x : Nat) : List Nat → List Nat
  | [] => [x]
  | y :: l => if x ≤ y then x :: y :: l else y :: insert x l

-- Insertion sort sorts the tail of the list, and then inserts the
-- head into the result. For example:
--
--   isort [3, 1, 2] = insert 3 (isort [1, 2])
--                   = insert 3 (insert 1 (isort [2]))
--                   = insert 3 (insert 1 (insert 2 []))
--                   = insert 3 (insert 1 [2])
--                   = insert 3 [1, 2]
--                   = [1, 2, 3]

def isort : List Nat → List Nat
  | [] => []
  | x :: l => insert x (isort l)

#eval isort [3, 1, 4, 1, 5, 9, 2, 6]    --> [1, 1, 2, 3, 4, 5, 6, 9]

-- When proving things about `insert`, there is one complication.
-- For concrete numbers, such as `insert 3 [1, 2]`, Lean can simply
-- compute the answer. But for variables, Lean cannot simplify
-- `insert x (y :: l)`, because it does not know which branch of the
-- `if` is taken: that depends on whether `x ≤ y`, which Lean does not
-- know. So in your proofs, you will have to consider both cases
-- yourself. The following two lemmas tell you how `insert` computes
-- in each case.

theorem insert_of_le {x y : Nat} {l : List Nat} (h : x ≤ y) :
    insert x (y :: l) = x :: y :: l :=
  ite_eq_left h

theorem insert_of_not_le {x y : Nat} {l : List Nat} (h : ¬ x ≤ y) :
    insert x (y :: l) = y :: insert x l :=
  ite_eq_right h

-- To use these lemmas, you will typically do a case distinction on
-- whether `x ≤ y` holds, like this:
--
--   match Decidable.em (x ≤ y) with
--   | .inl h => ...    -- here h : x ≤ y
--   | .inr h => ...    -- here h : ¬ x ≤ y
--
-- (`Decidable.em` is the law of excluded middle for propositions,
-- like `x ≤ y`, whose truth can be decided by a computation.) Then
-- use `insert_of_le h` or `insert_of_not_le h`, together with `▸`,
-- `Eq.subst`, or `calc`, to replace `insert x (y :: l)` by what it
-- computes to. You may also find `Nat.le_of_not_le` useful.
--
-- Here is a complete example, which you can use as a template: the
-- length of `insert x l` is one more than the length of `l`.

theorem length_insert (x : Nat) : ∀ l : List Nat, (insert x l).length = l.length + 1
  | [] => rfl
  | y :: l =>
      match Decidable.em (x ≤ y) with
      | .inl h =>
          calc (insert x (y :: l)).length
            _ = (x :: y :: l).length := congrArg List.length (insert_of_le h)
            _ = (y :: l).length + 1 := rfl
      | .inr h =>
          calc (insert x (y :: l)).length
            _ = (y :: insert x l).length := congrArg List.length (insert_of_not_le h)
            _ = (insert x l).length + 1 := rfl
            _ = (l.length + 1) + 1 := congrArg (· + 1) (length_insert x l)
            _ = (y :: l).length + 1 := rfl

-- ============================================================
-- Part 1: Sorted lists
--
-- A list is _sorted_ if each element is less than or equal to the
-- next one. We define this as an inductive predicate. The empty list
-- and one-element lists are sorted, and `x :: y :: l` is sorted if
-- `x ≤ y` and `y :: l` is sorted. Note that we only ever compare
-- neighbouring elements; it follows (by transitivity of `≤`) that
-- every element is less than or equal to every later one.
--
--                                            x ≤ y    Sorted (y :: l)
--  ──────────── (nil)  ─────────── (single)  ───────────────────────── (cons)
--   Sorted []           Sorted [x]               Sorted (x :: y :: l)

inductive Sorted : List Nat → Prop where
  | nil : Sorted []
  | single (x : Nat) : Sorted [x]
  | cons {x y : Nat} {l : List Nat} : x ≤ y → Sorted (y :: l) → Sorted (x :: y :: l)

section
open Sorted

-- 1.1 (Hint: `Nat.le_of_ble_eq_true rfl` is a convenient way to prove
-- inequalities between concrete numbers, such as `2 ≤ 5`. Can you see
-- why it works?)
example : Sorted [1, 2, 2, 5] :=
  sorry

-- 1.2 (Hint: if there were a proof of `Sorted [2, 1]`, which
-- constructor could it have been built with? What would that tell
-- you?)
theorem not_sorted : ¬ Sorted [2, 1] :=
  sorry

-- 1.3
theorem sorted_tail {x : Nat} {l : List Nat} : Sorted (x :: l) → Sorted l :=
  sorry

-- ============================================================
-- Part 2: Insertion sort produces sorted lists
--
-- The main lemma is that inserting into a sorted list gives a sorted
-- list. If you try to prove this directly by induction, you will get
-- stuck in one of the cases: to show that `y :: insert x l` is
-- sorted, you need to know something about the first element of
-- `insert x l`, and the induction hypothesis does not tell you that.
--
-- The solution is to prove a stronger statement, such as the
-- following. Intuitively, it says: if `y` is allowed to stand in
-- front of `l`, and `y ≤ x`, then `y` is still allowed to stand in
-- front of `insert x l`. This works because the first element of
-- `insert x l` is either `x` or the first element of `l`, and `y` is
-- less than or equal to both. Proving a stronger statement in order
-- to make an induction work is a very common trick.

-- 2.1
theorem sorted_cons_insert {x : Nat} : ∀ {y : Nat} {l : List Nat},
    y ≤ x → Sorted (y :: l) → Sorted (y :: insert x l) :=
  sorry

-- 2.2
theorem sorted_insert {x : Nat} : ∀ {l : List Nat}, Sorted l → Sorted (insert x l) :=
  sorry

-- 2.3
theorem sorted_isort : ∀ l : List Nat, Sorted (isort l) :=
  sorry

end

-- ============================================================
-- Part 3: Permutations
--
-- Two lists are _permutations_ of each other if they contain the same
-- elements, with the same multiplicities, but possibly in a
-- different order. We define the relation `l ~ l'`, "`l` is a
-- permutation of `l'`", as an inductive predicate. The idea is that
-- any rearrangement can be achieved by repeatedly swapping two
-- adjacent elements:
--
--                          l ~ l'
--  ───────── (nil)  ─────────────────── (cons)
--   [] ~ []          x :: l ~ x :: l'
--
--                                       l ~ l'    l' ~ l''
--  ─────────────────────────── (swap)  ──────────────────── (trans)
--   y :: x :: l ~ x :: y :: l                l ~ l''
--
-- Type `~` as \~ or simply as ~.

inductive Perm : List Nat → List Nat → Prop where
  | nil : Perm [] []
  | cons (x : Nat) {l l' : List Nat} : Perm l l' → Perm (x :: l) (x :: l')
  | swap (x y : Nat) (l : List Nat) : Perm (y :: x :: l) (x :: y :: l)
  | trans {l l' l'' : List Nat} : Perm l l' → Perm l' l'' → Perm l l''

infix:50 " ~ " => Perm

section
open Perm

-- A warning: Lean has another function called `trans`. So when you
-- pattern match on a permutation, you must write the pattern as
-- `.trans p q` (with a dot), or as `Perm.trans p q`, rather than as
-- `trans p q`.

-- 3.1
example : [1, 2, 3] ~ [3, 1, 2] :=
  sorry

-- 3.2 The permutation relation is reflexive.
theorem perm_refl : ∀ l : List Nat, l ~ l :=
  sorry

-- 3.3 The permutation relation is symmetric.
theorem perm_symm {l l' : List Nat} : l ~ l' → l' ~ l :=
  sorry

-- 3.4 Inserting `x` into `l` gives a permutation of `x :: l`.
theorem perm_insert (x : Nat) : ∀ l : List Nat, insert x l ~ x :: l :=
  sorry

-- 3.5 (Hint: use 3.4, and the constructors `cons` and `trans`.)
theorem perm_isort : ∀ l : List Nat, isort l ~ l :=
  sorry

end

-- ============================================================
-- Part 4: Correctness of insertion sort
--
-- Now we can put everything together.

-- 4.1
theorem isort_correct (l : List Nat) : Sorted (isort l) ∧ isort l ~ l :=
  sorry

-- ============================================================
-- Part 5 (bonus)

-- Each bonus question is independent; you may do some, all, or none
-- of them.

-- 5.1 Permutations preserve length.
theorem perm_length {l l' : List Nat} : l ~ l' → l.length = l'.length :=
  sorry

-- 5.2 Sorting a list that is already sorted does nothing. (Hint: you
-- will need a lemma about what `insert x l` computes to when `x` is
-- less than or equal to the first element of `l`.)
theorem isort_of_sorted : ∀ {l : List Nat}, Sorted l → isort l = l :=
  sorry

-- 5.3 (Challenge) There is only one way to sort a list: if two sorted
-- lists are permutations of each other, they are equal. As a
-- consequence, *every* correct sorting algorithm produces the same
-- output as insertion sort. Warning: this is much harder than the
-- other questions. You will need several lemmas of your own, for
-- example about the membership of elements in permuted lists.
theorem sorted_perm_unique {l l' : List Nat} :
    Sorted l → Sorted l' → l ~ l' → l = l' :=
  sorry

end Project_Sorting