Library Lsort

Require Import Bool.
Require Import Sumbool.
Require Import Arith.
Require Import NArith.
Require Import Ndigits.
Require Import Ndec.
Require Import Map.
Require Import List.
Require Import Mapiter.

Section LSort.

  Variable A : Type.

  Fixpoint alist_sorted (l:alist A) : bool :=
    match l with
    | nil => true
    | (a, _) :: l' =>
        match l' with
        | nil => true
        | (a', y') :: l'' => andb (Nless a a') (alist_sorted l')
        end
    end.

  Fixpoint alist_nth_ad (n:nat) (l:alist A) {struct l} : ad :=
    match l with
    | nil => N0
    | (a, y) :: l' => match n with
                      | O => a
                      | S n' => alist_nth_ad n' l'
                      end
    end.

  Definition alist_sorted_1 (l:alist A) :=
    forall n:nat,
      S (S n) <= length l ->
      Nless (alist_nth_ad n l) (alist_nth_ad (S n) l) = true.

  Lemma alist_sorted_imp_1 :
   forall l:alist A, alist_sorted l = true -> alist_sorted_1 l.

  Definition alist_sorted_2 (l:alist A) :=
    forall m n:nat,
      m < n ->
      S n <= length l -> Nless (alist_nth_ad m l) (alist_nth_ad n l) = true.

  Lemma alist_sorted_1_imp_2 :
   forall l:alist A, alist_sorted_1 l -> alist_sorted_2 l.

  Lemma alist_sorted_2_imp :
   forall l:alist A, alist_sorted_2 l -> alist_sorted l = true.

  Lemma app_length :
   forall (C:Type) (l l':list C), length (l ++ l') = length l + length l'.

  Lemma aapp_length :
   forall l l':alist A, length (aapp A l l') = length l + length l'.

  Lemma alist_nth_ad_aapp_1 :
   forall (l l':alist A) (n:nat),
     S n <= length l -> alist_nth_ad n (aapp A l l') = alist_nth_ad n l.

  Lemma alist_nth_ad_aapp_2 :
   forall (l l':alist A) (n:nat),
     S n <= length l' ->
     alist_nth_ad (length l + n) (aapp A l l') = alist_nth_ad n l'.

  Lemma interval_split :
   forall p q n:nat,
     S n <= p + q -> {n' : nat | S n' <= q /\ n = p + n'} + {S n <= p}.

  Lemma alist_conc_sorted :
   forall l l':alist A,
     alist_sorted_2 l ->
     alist_sorted_2 l' ->
     (forall n n':nat,
        S n <= length l ->
        S n' <= length l' ->
        Nless (alist_nth_ad n l) (alist_nth_ad n' l') = true) ->
     alist_sorted_2 (aapp A l l').

  Lemma alist_nth_ad_semantics :
   forall (l:alist A) (n:nat),
     S n <= length l ->
     {y : A | alist_semantics A l (alist_nth_ad n l) = Some y}.

  Lemma alist_of_Map_nth_ad :
   forall (m:Map A) (pf:ad -> ad) (l:alist A),
     l =
     MapFold1 A (alist A) (anil A) (aapp A)
       (fun (a0:ad) (y:A) => acons A (a0, y) (anil A)) pf m ->
     forall n:nat, S n <= length l -> {a' : ad | alist_nth_ad n l = pf a'}.

  Definition ad_monotonic (pf:ad -> ad) :=
    forall a a':ad, Nless a a' = true -> Nless (pf a) (pf a') = true.

  Lemma Ndouble_monotonic : ad_monotonic Ndouble.

  Lemma Ndouble_plus_one_monotonic : ad_monotonic Ndouble_plus_one.

  Lemma ad_comp_monotonic :
   forall pf pf':ad -> ad,
     ad_monotonic pf ->
     ad_monotonic pf' -> ad_monotonic (fun a0:ad => pf (pf' a0)).

  Lemma ad_comp_double_monotonic :
   forall pf:ad -> ad,
     ad_monotonic pf -> ad_monotonic (fun a0:ad => pf (Ndouble a0)).

  Lemma ad_comp_double_plus_un_monotonic :
   forall pf:ad -> ad,
     ad_monotonic pf -> ad_monotonic (fun a0:ad => pf (Ndouble_plus_one a0)).

  Lemma alist_of_Map_sorts_1 :
   forall (m:Map A) (pf:ad -> ad),
     ad_monotonic pf ->
     alist_sorted_2
       (MapFold1 A (alist A) (anil A) (aapp A)
          (fun (a:ad) (y:A) => acons A (a, y) (anil A)) pf m).

  Lemma alist_of_Map_sorts :
   forall m:Map A, alist_sorted (alist_of_Map A m) = true.

  Lemma alist_of_Map_sorts1 :
   forall m:Map A, alist_sorted_1 (alist_of_Map A m).

  Lemma alist_of_Map_sorts2 :
   forall m:Map A, alist_sorted_2 (alist_of_Map A m).

  Lemma alist_too_low :
   forall (l:alist A) (a a':ad) (y:A),
     Nless a a' = true ->
     alist_sorted_2 ((a', y) :: l) ->
     alist_semantics A ((a', y) :: l) a = None.

  Lemma alist_semantics_nth_ad :
   forall (l:alist A) (a:ad) (y:A),
     alist_semantics A l a = Some y ->
     {n : nat | S n <= length l /\ alist_nth_ad n l = a}.

  Lemma alist_semantics_tail :
   forall (l:alist A) (a:ad) (y:A),
     alist_sorted_2 ((a, y) :: l) ->
     eqm A (alist_semantics A l)
       (fun a0:ad =>
          if Neqb a a0 then None else alist_semantics A ((a, y) :: l) a0).

  Lemma alist_semantics_same_tail :
   forall (l l':alist A) (a:ad) (y:A),
     alist_sorted_2 ((a, y) :: l) ->
     alist_sorted_2 ((a, y) :: l') ->
     eqm A (alist_semantics A ((a, y) :: l))
       (alist_semantics A ((a, y) :: l')) ->
     eqm A (alist_semantics A l) (alist_semantics A l').

  Lemma alist_sorted_tail :
   forall (l:alist A) (a:ad) (y:A),
     alist_sorted_2 ((a, y) :: l) -> alist_sorted_2 l.

  Lemma alist_canonical :
   forall l l':alist A,
     eqm A (alist_semantics A l) (alist_semantics A l') ->
     alist_sorted_2 l -> alist_sorted_2 l' -> l = l'.

End LSort.