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. destruct l; simpl; tauto. Qed.

Lemma sorted_first_two (a b : nat) (l : list nat) :
  sorted (a :: b :: l) -> a <= b.
Proof. simpl; tauto. Qed.

Lemma sorted_less_than_all (a : nat) (l : list nat) :
  sorted l /\ (forall b, In b l -> a <= b) <-> sorted (a :: l).
Proof.
  revert a; induction l as [|b l IHl].
  - simpl. tauto.
  - intros a.
    split.
    + intros Hbl.
      destruct Hbl as [Hbl Hble].
      simpl.
      simpl in Hbl.
      split.
      * apply Hble.
        simpl. tauto.
      * trivial.
    + intros Habl.
      split.
      * eapply sorted_tail; eauto.
      * intros c Hc.
        simpl in Hc.
        destruct Habl as [Hab Hbl].
        destruct Hc as [Hc|Hc].
        -- rewrite <- Hc. trivial.
        -- apply IHl in Hbl.
           destruct Hbl as [Hl Hble].
           transitivity b.
           ++ trivial.
           ++ apply Hble. trivial.
Qed.

Lemma in_insert (n : nat) (l : list nat) :
  forall a, In a (insert n l) <-> a = n \/ In a l.
Proof.
  revert n; induction l as [|b l IHl].
  - simpl. firstorder.
  - intros n a.
    split.
    + simpl.
      destruct le_lt_dec.
      * simpl. firstorder.
      * simpl. intros Hl.
        firstorder.
    + intros Habl.
      simpl in Habl.
      simpl.
      destruct le_lt_dec.
      * simpl. firstorder.
      * simpl. firstorder.
Qed.

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.

From Coq.Sorting Require Import Permutation.

Print Permutation.

Lemma insert_perm a l : Permutation (a :: l) (insert a l).
Proof.
  revert a; induction l as [|b l IHl].
  - simpl.
    intros a.
    apply Permutation_refl.
  - intros a.
    simpl.
    destruct le_lt_dec.
    + apply Permutation_refl.
    + eapply (@perm_trans _ _ (b :: a :: l)).
      * apply perm_swap.
      * apply perm_skip.
        apply IHl.
Qed.

Theorem insertion_sort_perm l : Permutation l (insertion_sort l).
Proof.
  induction l as [|a l IHl].
  - simpl.
    apply perm_nil.
  - simpl.
    apply (@perm_trans _ _ (a :: insertion_sort l)).
    + apply perm_skip.
      trivial.
    + apply insert_perm.
Qed.
Search nat "dec".