Require Import Arith.
Require Import List.

(** Prédicat: «être triée» *)
Inductive Sorted : (list nat) -> Prop :=
  sorted_nil: (Sorted nil)
| sorted_cons1: forall x:nat, (Sorted (cons x nil))
| sorted_cons2: forall (x1 x2:nat) (xs:(list nat)),
    (le x1 x2) -> (Sorted (cons x2 xs)) 
      -> (Sorted (cons x1 (cons x2 xs))).

(* Lemmes d'inversion *)
Lemma sorted_le : forall (x y:nat) (xs:list nat),
    (Sorted (cons x (cons y xs))) -> (le x y).
Admitted.

Lemma sorted_cons_sorted : forall (x:nat) (xs:list nat),
    (Sorted (cons x xs)) -> (Sorted xs).
Admitted.

  (* Manipulation du début d'une liste triée *)
Lemma sorted_le_sorted : forall (x y:nat) (xs:list nat),
    (Sorted (cons x xs)) -> (le y x) -> (Sorted (cons y xs)).
Admitted.
  
Lemma sorted_push_hd : forall (x y:nat) (xs:list nat),
    (Sorted (cons x (cons y xs))) -> (Sorted (cons x xs)).
Admitted.

(* Elément minorant *)
Lemma sorted_le_list : forall (x:nat) (xs:list nat),
    (Sorted (cons x xs)) -> forall (y:nat), (In y xs) -> (le x y).
Admitted.

(* Tri par insertion *)
Fixpoint insert (x:nat) (xs:list nat) : (list nat) :=
  (cons x xs).

Lemma sorted_insert : forall (x:nat) (xs:list nat),
    (Sorted xs) -> (Sorted (insert x xs)).
Admitted.

Fixpoint sort (xs:list nat) : list nat :=
  xs.

Theorem sorted_sort : forall (xs:list nat), (Sorted (sort xs)).
Admitted.