Require Export PolyList.
Require Export Arith.
Require Export Compare_dec.
(* A list is sorted if each element is smaller than the one that follows *)
 
Inductive sorted : (list nat) ->  Prop :=
  sorted_nil: fill_in_the_blank
 | sorted_1: fill_in_the_blank
 | sorted_2: fill_in_blank .
(* A proof that can be done with only the constructors. *)
 
Theorem test1:
 (sorted
  (cons
   (S (S (S O)))
   (cons (S (S (S (S (S O))))) (cons (S (S (S (S (S (S (S O))))))) (nil nat))))).
(* Find the right Hint command so that the following proof goes
   completely automatically *)
 
Theorem test1':
 (sorted
  (cons
   (S (S (S O)))
   (cons (S (S (S (S (S O))))) (cons (S (S (S (S (S (S (S O))))))) (nil nat))))).
Auto 20 with *.
Qed.
(* Lookup the documentation of the Inversion tactic.  *)
 
Theorem test2: ~ (sorted (cons (S (S O)) (cons (S O) (nil nat)))).
(* The interested readers should check the value of le_lt_dec. *)
 
Fixpoint insert [n : nat; l : (list nat)] : (list nat) :=
 Cases l of
   nil => (cons n (nil nat))
  | (cons n1 l1) =>
      Cases (le_lt_dec n n1) of
        (left h) => (cons n (cons n1 l1))
       | (right h) => (cons n1 (insert n l1))
      end
 end.
(* insert produces a sorted list, provided it received a sorted list. *)
 
Theorem isert_sorted:
 (l : (list nat)) (n : nat) (sorted l) ->  (sorted (insert n l)).
(* Construct a function that uses insert to sort a list. *)
 
Fixpoint sort [l : (list nat)] : Fill_in_the_blank :=
 Fill_in_blank.
 
Theorem sort_correct1: (l : (list nat))  (sorted (sort l)).
(* One should also make sure that the result is a permutation of the
   input. *)
 
Inductive permutation : (list nat) -> (list nat) ->  Prop :=
  same_permutation: (l : (list nat))  (permutation l l)
 | transposition_then_permutation:
     (l1, l2, l3, l4 : (list nat))
     (n1, n2 : nat)
     (permutation (app l1 (cons n2 (app l2 (cons n1 l3)))) l4) ->
      (permutation (app l1 (cons n1 (app l2 (cons n2 l3)))) l4) .
 
Theorem permutation_trans: Fill_in_the_blank.
 
Theorem permutation_sym: Fill_in_the_blank.
 
Theorem insert_permutation:
 (l : (list nat)) (n : nat)  (permutation (cons n l) (insert n l)).
 
Theorem sort_permutation: (l : (list nat))  (permutation l (sort l)).