From Coq.micromega Require Import Lia.
From Coq.Arith Require Import PeanoNat.
Import Compare_dec.
From Coq.Lists Require Import List.
Import ListNotations.

Fixpoint insert (n : nat) (l : list nat) : list nat :=
match l with
| [] => [n]
| a :: l' => if le_lt_dec n a then n :: l else a :: (insert n l')
end.

Fixpoint insertion_sort (l : list nat) : list nat :=
match l with
| [] => []
| a :: l' => insert a (insertion_sort l')
end.

Fixpoint sorted (l : list nat) : Prop :=
match l with
| nil => True
| cons a l' =>
  match l' with
  | [] => True
  | b :: l'' => a <= b /\ sorted l'
  end
end.

Lemma sorted_tail (a : nat) (l : list nat) : sorted (a :: l) -> sorted l.
Proof.
Admitted.

Lemma sorted_first_two (a b : nat) (l : list nat) :
  sorted (a :: b :: l) -> a <= b.
Proof.
  simpl.
  intros Habl.
  destruct Habl as [Habl1 Habl2].
  trivial.
Qed.

Lemma sorted_less_than_all (a : nat) (l : list nat) :
  sorted l /\ (forall b, In b l -> a <= b) <-> sorted (a :: l).
Proof.
Admitted.

Lemma in_insert (n : nat) (l : list nat) :
  forall a, In a (insert n l) <-> a = n \/ In a l.
Proof.
Admitted.

Lemma insert_sorted (n : nat) (l : list nat) : sorted l -> sorted (insert n l).
Proof.
  revert n.
  induction l as [|a l IHl].
  - intros n. simpl. trivial.
  - intros n Hl. simpl.
    destruct le_lt_dec.
    + simpl.
      split.
      * trivial.
      * destruct l as [|b l].
        -- trivial.
        -- split.
           ++ eapply sorted_first_two; eauto.
           ++ eapply sorted_tail; eauto.
    + apply sorted_less_than_all.
      split.
      * apply IHl. eapply sorted_tail; eauto.
      * apply sorted_less_than_all in Hl.
        destruct Hl as [Hl1 Hl2].
        intros b Hb.
        apply in_insert in Hb.
        destruct Hb as [Hb1|Hb2].
        -- rewrite Hb1. lia.
        -- auto.
Qed.

Theorem insertion_sort_sorted (l : list nat) : sorted (insertion_sort l).
Proof.
  induction l as [|a l IHl].
  - simpl. trivial.
  - simpl.
    apply insert_sorted; trivial.
Qed.