(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)
(*i 	$Id: Lsort.v,v 1.1.2.1 2004/07/16 19:31:27 herbelin Exp $	 i*)

Require Bool.
Require Sumbool.
Require Arith.
Require ZArith.
Require Addr.
Require Adist.
Require Addec.
Require Map.
Require PolyList.
Require Mapiter.

Section LSort.

  Variable A : Set.

  Fixpoint ad_less_1 [a,a':ad; p:positive] : bool :=
    Cases p of
        (xO p') => (ad_less_1 (ad_div_2 a) (ad_div_2 a') p')
      | _ => (andb (negb (ad_bit_0 a)) (ad_bit_0 a'))
    end.

  Definition ad_less := [a,a':ad] Cases (ad_xor a a') of
      	                              ad_z => false
				    | (ad_x p) => (ad_less_1 a a' p)
				  end.

  Lemma ad_bit_0_less : (a,a':ad) (ad_bit_0 a)=false -> (ad_bit_0 a')=true -> 
      (ad_less a a')=true.
  Proof.
    Intros. Elim (ad_sum (ad_xor a a')). Intro H1. Elim H1. Intros p H2. Unfold ad_less.
    Rewrite H2. Generalize H2. Elim p. Intros. Simpl. Rewrite H. Rewrite H0. Reflexivity.
    Intros. Cut (ad_bit_0 (ad_xor a a'))=false. Intro. Rewrite (ad_xor_bit_0 a a') in H5.
    Rewrite H in H5. Rewrite H0 in H5. Discriminate H5.
    Rewrite H4. Reflexivity.
    Intro. Simpl. Rewrite H. Rewrite H0. Reflexivity.
    Intro H1. Cut (ad_bit_0 (ad_xor a a'))=false. Intro. Rewrite (ad_xor_bit_0 a a') in H2.
    Rewrite H in H2. Rewrite H0 in H2. Discriminate H2.
    Rewrite H1. Reflexivity.
  Qed.

  Lemma ad_bit_0_gt : (a,a':ad) (ad_bit_0 a)=true -> (ad_bit_0 a')=false -> 
      (ad_less a a')=false.
  Proof.
    Intros. Elim (ad_sum (ad_xor a a')). Intro H1. Elim H1. Intros p H2. Unfold ad_less.
    Rewrite H2. Generalize H2. Elim p. Intros. Simpl. Rewrite H. Rewrite H0. Reflexivity.
    Intros. Cut (ad_bit_0 (ad_xor a a'))=false. Intro. Rewrite (ad_xor_bit_0 a a') in H5.
    Rewrite H in H5. Rewrite H0 in H5. Discriminate H5.
    Rewrite H4. Reflexivity.
    Intro. Simpl. Rewrite H. Rewrite H0. Reflexivity.
    Intro H1. Unfold ad_less. Rewrite H1. Reflexivity.
  Qed.

  Lemma ad_less_not_refl : (a:ad) (ad_less a a)=false.
  Proof.
    Intro. Unfold ad_less. Rewrite (ad_xor_nilpotent a). Reflexivity.
  Qed.

  Lemma ad_ind_double : 
      (a:ad)(P:ad->Prop) (P ad_z) ->
      	((a:ad) (P a) -> (P (ad_double a))) ->
      	((a:ad) (P a) -> (P (ad_double_plus_un a))) -> (P a).
  Proof.
    Intros; Elim a. Trivial.
    Induction p. Intros. 
    Apply (H1 (ad_x p0)); Trivial.
    Intros; Apply (H0 (ad_x p0)); Trivial.
    Intros; Apply (H1 ad_z); Assumption.
  Qed.

  Lemma ad_rec_double : 
      (a:ad)(P:ad->Set) (P ad_z) ->
      	((a:ad) (P a) -> (P (ad_double a))) ->
      	((a:ad) (P a) -> (P (ad_double_plus_un a))) -> (P a).
  Proof.
    Intros; Elim a. Trivial.
    Induction p. Intros. 
    Apply (H1 (ad_x p0)); Trivial.
    Intros; Apply (H0 (ad_x p0)); Trivial.
    Intros; Apply (H1 ad_z); Assumption.
  Qed.

  Lemma ad_less_def_1 : (a,a':ad) (ad_less (ad_double a) (ad_double a'))=(ad_less a a').
  Proof.
    Induction a. Induction a'. Reflexivity.
    Trivial.
    Induction a'. Unfold ad_less. Simpl. (Elim p; Trivial).
    Unfold ad_less. Simpl. Intro. Case (p_xor p p0). Reflexivity.
    Trivial.
  Qed.

  Lemma ad_less_def_2 : (a,a':ad)
      (ad_less (ad_double_plus_un a) (ad_double_plus_un a'))=(ad_less a a').
  Proof.
    Induction a. Induction a'. Reflexivity.
    Trivial.
    Induction a'. Unfold ad_less. Simpl. (Elim p; Trivial).
    Unfold ad_less. Simpl. Intro. Case (p_xor p p0). Reflexivity.
    Trivial.
  Qed.

  Lemma ad_less_def_3 : (a,a':ad) (ad_less (ad_double a) (ad_double_plus_un a'))=true.
  Proof.
    Intros. Apply ad_bit_0_less. Apply ad_double_bit_0.
    Apply ad_double_plus_un_bit_0.
  Qed.

  Lemma ad_less_def_4 : (a,a':ad) (ad_less (ad_double_plus_un a) (ad_double a'))=false.
  Proof.
    Intros. Apply ad_bit_0_gt. Apply ad_double_plus_un_bit_0.
    Apply ad_double_bit_0.
  Qed.

  Lemma ad_less_z : (a:ad) (ad_less a ad_z)=false.
  Proof.
    Induction a. Reflexivity.
    Unfold ad_less. Intro. Rewrite (ad_xor_neutral_right (ad_x p)). (Elim p; Trivial).
  Qed.

  Lemma ad_z_less_1 : (a:ad) (ad_less ad_z a)=true -> {p:positive | a=(ad_x p)}.
  Proof.
    Induction a. Intro. Discriminate H.
    Intros. Split with p. Reflexivity.
  Qed.

  Lemma ad_z_less_2 : (a:ad) (ad_less ad_z a)=false -> a=ad_z.
  Proof.
    Induction a. Trivial.
    Unfold ad_less. Simpl. Cut (p:positive)(ad_less_1 ad_z (ad_x p) p)=false->False.
    Intros. Elim (H p H0).
    Induction p. Intros. Discriminate H0.
    Intros. Exact (H H0).
    Intro. Discriminate H.
  Qed.

  Lemma ad_less_trans : (a,a',a'':ad)
      (ad_less a a')=true -> (ad_less a' a'')=true -> (ad_less a a'')=true.
  Proof.
    Intro a. Apply ad_ind_double with P:=[a:ad]
          (a',a'':ad)
           (ad_less a a')=true
            ->(ad_less a' a'')=true->(ad_less a a'')=true.
    Intros. Elim (sumbool_of_bool (ad_less ad_z a'')). Trivial.
    Intro H1. Rewrite (ad_z_less_2 a'' H1) in H0. Rewrite (ad_less_z a') in H0. Discriminate H0.
    Intros a0 H a'. Apply ad_ind_double with P:=[a':ad]
          (a'':ad)
           (ad_less (ad_double a0) a')=true
            ->(ad_less a' a'')=true->(ad_less (ad_double a0) a'')=true.
    Intros. Rewrite (ad_less_z (ad_double a0)) in H0. Discriminate H0.
    Intros a1 H0 a'' H1. Rewrite (ad_less_def_1 a0 a1) in H1.
    Apply ad_ind_double with P:=[a'':ad]
          (ad_less (ad_double a1) a'')=true
           ->(ad_less (ad_double a0) a'')=true.
    Intro. Rewrite (ad_less_z (ad_double a1)) in H2. Discriminate H2.
    Intros. Rewrite (ad_less_def_1 a1 a2) in H3. Rewrite (ad_less_def_1 a0 a2).
    Exact (H a1 a2 H1 H3).
    Intros. Apply ad_less_def_3.
    Intros a1 H0 a'' H1. Apply ad_ind_double with P:=[a'':ad]
          (ad_less (ad_double_plus_un a1) a'')=true
           ->(ad_less (ad_double a0) a'')=true.
    Intro. Rewrite (ad_less_z (ad_double_plus_un a1)) in H2. Discriminate H2.
    Intros. Rewrite (ad_less_def_4 a1 a2) in H3. Discriminate H3.
    Intros. Apply ad_less_def_3.
    Intros a0 H a'. Apply ad_ind_double with P:=[a':ad]
          (a'':ad)
           (ad_less (ad_double_plus_un a0) a')=true
            ->(ad_less a' a'')=true
               ->(ad_less (ad_double_plus_un a0) a'')=true.
    Intros. Rewrite (ad_less_z (ad_double_plus_un a0)) in H0. Discriminate H0.
    Intros. Rewrite (ad_less_def_4 a0 a1) in H1. Discriminate H1.
    Intros a1 H0 a'' H1. Apply ad_ind_double with P:=[a'':ad]
          (ad_less (ad_double_plus_un a1) a'')=true
           ->(ad_less (ad_double_plus_un a0) a'')=true.
    Intro. Rewrite (ad_less_z (ad_double_plus_un a1)) in H2. Discriminate H2.
    Intros. Rewrite (ad_less_def_4 a1 a2) in H3. Discriminate H3.
    Rewrite (ad_less_def_2 a0 a1) in H1. Intros. Rewrite (ad_less_def_2 a1 a2) in H3.
    Rewrite (ad_less_def_2 a0 a2). Exact (H a1 a2 H1 H3).
  Qed.

  Fixpoint alist_sorted [l:(alist A)] : bool :=
    Cases l of
      	nil => true
      | (cons (a, _) l') => Cases l' of
                                nil => true
			      | (cons (a', y') l'') => (andb (ad_less a a')
			                                     (alist_sorted l'))
			    end
    end.

  Fixpoint alist_nth_ad [n:nat; l:(alist A)] : ad :=
    Cases l of
      	nil => ad_z (* dummy *)
      | (cons (a, y) l') => Cases n of
                                O => a
			      | (S n') => (alist_nth_ad n' l')
			    end
    end.

  Definition alist_sorted_1 := [l:(alist A)]
      (n:nat) (le (S (S n)) (length l)) ->
      	(ad_less (alist_nth_ad n l) (alist_nth_ad (S n) l))=true.

  Lemma alist_sorted_imp_1 : (l:(alist A)) (alist_sorted l)=true -> (alist_sorted_1 l).
  Proof.
    Unfold alist_sorted_1. Induction l. Intros. Elim (le_Sn_O (S n) H0).
    Intro r. Elim r. Intros a y. Induction l0. Intros. Simpl in H1.
    Elim (le_Sn_O n (le_S_n (S n) O H1)).
    Intro r0. Elim r0. Intros a0 y0. Induction n. Intros. Simpl. Simpl in H1.
    Exact (proj1 ? ? (andb_prop ? ? H1)).
    Intros. Change (ad_less (alist_nth_ad n0 (cons (a0,y0) l1))
      	                    (alist_nth_ad (S n0) (cons (a0,y0) l1)))=true.
    Apply H0. Exact (proj2 ? ? (andb_prop ? ? H1)).
    Apply le_S_n. Exact H3.
  Qed.

  Definition alist_sorted_2 := [l:(alist A)]
    (m,n:nat) (lt m n) -> (le (S n) (length l)) ->
      	(ad_less (alist_nth_ad m l) (alist_nth_ad n l))=true.

  Lemma alist_sorted_1_imp_2 : (l:(alist A)) (alist_sorted_1 l) -> (alist_sorted_2 l).
  Proof.
    Unfold alist_sorted_1 alist_sorted_2 lt. Intros l H m n H0. Elim H0. Exact (H m).
    Intros. Apply ad_less_trans with a':=(alist_nth_ad m0 l). Apply H2. Apply le_trans_S.
    Assumption.
    Apply H. Assumption.
  Qed.

  Lemma alist_sorted_2_imp : (l:(alist A)) (alist_sorted_2 l) -> (alist_sorted l)=true.
  Proof.
    Unfold alist_sorted_2 lt. Induction l. Trivial.
    Intro r. Elim r. Intros a y. Induction l0. Trivial.
    Intro r0. Elim r0. Intros a0 y0. Intros.
    Change (andb (ad_less a a0) (alist_sorted (cons (a0,y0) l1)))=true.
    Apply andb_true_intro. Split. Apply (H1 (0) (1)). Apply le_n.
    Simpl. Apply le_n_S. Apply le_n_S. Apply le_O_n.
    Apply H0. Intros. Apply (H1 (S m) (S n)). Apply le_n_S. Assumption.
    Exact (le_n_S ? ? H3).
  Qed.

  Lemma app_length : (C:Set) (l,l':(list C)) (length (app l l'))=(plus (length l) (length l')).
  Proof.
    Induction l. Trivial.
    Intros. Simpl. Rewrite (H l'). Reflexivity.
  Qed.

  Lemma aapp_length : (l,l':(alist A)) (length (aapp A l l'))=(plus (length l) (length l')).
  Proof.
    Exact (app_length ad*A).
  Qed.

  Lemma alist_nth_ad_aapp_1 : (l,l':(alist A)) (n:nat)
      (le (S n) (length l)) -> (alist_nth_ad n (aapp A l l'))=(alist_nth_ad n l).
  Proof.
    Induction l. Intros. Elim (le_Sn_O n H).
    Intro r. Elim r. Intros a y l' H l''. Induction n. Trivial.
    Intros. Simpl. Apply H. Apply le_S_n. Exact H1.
  Qed.

  Lemma alist_nth_ad_aapp_2 : (l,l':(alist A)) (n:nat)
      (le (S n) (length l')) ->
      	(alist_nth_ad (plus (length l) n) (aapp A l l'))=(alist_nth_ad n l').
  Proof.
    Induction l. Trivial.
    Intro r. Elim r. Intros a y l' H l'' n H0. Simpl. Apply H. Exact H0.
  Qed.

  Lemma interval_split : (p,q,n:nat) (le (S n) (plus p q)) ->
      {n' : nat | (le (S n') q) /\ n=(plus p n')}+{(le (S n) p)}.
  Proof.
    Induction p. Simpl. Intros. Left . Split with n. (Split; [ Assumption | Reflexivity ]).
    Intros p' H q. Induction n. Intros. Right . Apply le_n_S. Apply le_O_n.
    Intros. Elim (H ? ? (le_S_n ? ? H1)). Intro H2. Left . Elim H2. Intros n' H3.
    Elim H3. Intros H4 H5. Split with n'. (Split; [ Assumption | Rewrite H5; Reflexivity ]).
    Intro H2. Right . Apply le_n_S. Assumption.
  Qed.

  Lemma alist_conc_sorted : (l,l':(alist A)) (alist_sorted_2 l) -> (alist_sorted_2 l') ->
      ((n,n':nat) (le (S n) (length l)) -> (le (S n') (length l')) ->
      	  (ad_less (alist_nth_ad n l) (alist_nth_ad n' l'))=true) ->
      	(alist_sorted_2 (aapp A l l')).
  Proof.
    Unfold alist_sorted_2 lt. Intros. Rewrite (aapp_length l l') in H3.
    Elim (interval_split (length l) (length l') m
            (le_trans ? ? ? (le_n_S ? ? (lt_le_weak m n H2)) H3)).
    Intro H4. Elim H4. Intros m' H5. Elim H5. Intros. Rewrite H7.
    Rewrite (alist_nth_ad_aapp_2 l l' m' H6). Elim (interval_split (length l) (length l') n H3).
    Intro H8. Elim H8. Intros n' H9. Elim H9. Intros. Rewrite H11.
    Rewrite (alist_nth_ad_aapp_2 l l' n' H10). Apply H0. Rewrite H7 in H2. Rewrite H11 in H2.
    Change (le (plus (S (length l)) m') (plus (length l) n')) in H2.
    Rewrite (plus_Snm_nSm (length l) m') in H2. Exact (simpl_le_plus_l (length l) (S m') n' H2).
    Exact H10.
    Intro H8. Rewrite H7 in H2. Cut (le (S (length l)) (length l)). Intros. Elim (le_Sn_n ? H9).
    Apply le_trans with m:=(S n). Apply le_n_S. Apply le_trans with m:=(S (plus (length l) m')).
    Apply le_trans with m:=(plus (length l) m'). Apply le_plus_l.
    Apply le_n_Sn.
    Exact H2.
    Exact H8.
    Intro H4. Rewrite (alist_nth_ad_aapp_1 l l' m H4).
    Elim (interval_split (length l) (length l') n H3). Intro H5. Elim H5. Intros n' H6. Elim H6.
    Intros. Rewrite H8. Rewrite (alist_nth_ad_aapp_2 l l' n' H7). Exact (H1 m n' H4 H7).
    Intro H5. Rewrite (alist_nth_ad_aapp_1 l l' n H5). Exact (H m n H2 H5).
  Qed.

  Lemma alist_nth_ad_semantics : (l:(alist A)) (n:nat) (le (S n) (length l)) ->
      {y:A | (alist_semantics A l (alist_nth_ad n l))=(SOME A y)}.
  Proof.
    Induction l. Intros. Elim (le_Sn_O ? H).
    Intro r. Elim r. Intros a y l0 H. Induction n. Simpl. Intro. Split with y.
    Rewrite (ad_eq_correct a). Reflexivity.
    Intros. Elim (H ? (le_S_n ? ? H1)). Intros y0 H2.
    Elim (sumbool_of_bool (ad_eq a (alist_nth_ad n0 l0))). Intro H3. Split with y.
    Rewrite (ad_eq_complete ? ? H3). Simpl. Rewrite (ad_eq_correct (alist_nth_ad n0 l0)).
    Reflexivity.
    Intro H3. Split with y0. Simpl. Rewrite H3. Assumption.
  Qed.

  Lemma alist_of_Map_nth_ad : (m:(Map A)) (pf:ad->ad)
      (l:(alist A)) l=(MapFold1 A (alist A) (anil A) (aapp A)
                                [a0:ad][y:A](acons A (a0,y) (anil A)) pf m) ->
      	(n:nat) (le (S n) (length l)) -> {a':ad | (alist_nth_ad n l)=(pf a')}.
  Proof.
    Intros. Elim (alist_nth_ad_semantics l n H0). Intros y H1.
    Apply (alist_of_Map_semantics_1_1 A m pf (alist_nth_ad n l) y).
    Rewrite <- H. Assumption.
  Qed.

  Definition ad_monotonic := [pf:ad->ad] (a,a':ad)
      (ad_less a a')=true -> (ad_less (pf a) (pf a'))=true.

  Lemma ad_double_monotonic : (ad_monotonic ad_double).
  Proof.
    Unfold ad_monotonic. Intros. Rewrite ad_less_def_1. Assumption.
  Qed.

  Lemma ad_double_plus_un_monotonic : (ad_monotonic ad_double_plus_un).
  Proof.
    Unfold ad_monotonic. Intros. Rewrite ad_less_def_2. Assumption.
  Qed.

  Lemma ad_comp_monotonic : (pf,pf':ad->ad) (ad_monotonic pf) -> (ad_monotonic pf') ->
      (ad_monotonic [a0:ad] (pf (pf' a0))).
  Proof.
    Unfold ad_monotonic. Intros. Apply H. Apply H0. Exact H1.
  Qed.

  Lemma ad_comp_double_monotonic : (pf:ad->ad) (ad_monotonic pf) ->
      (ad_monotonic [a0:ad] (pf (ad_double a0))).
  Proof.
    Intros. Apply ad_comp_monotonic. Assumption.
    Exact ad_double_monotonic.
  Qed.

  Lemma ad_comp_double_plus_un_monotonic : (pf:ad->ad) (ad_monotonic pf) ->
      (ad_monotonic [a0:ad] (pf (ad_double_plus_un a0))).
  Proof.
    Intros. Apply ad_comp_monotonic. Assumption.
    Exact ad_double_plus_un_monotonic.
  Qed.

  Lemma alist_of_Map_sorts_1 : (m:(Map A)) (pf:ad->ad) (ad_monotonic pf) ->
      (alist_sorted_2 (MapFold1 A (alist A) (anil A) (aapp A)
                                [a:ad][y:A](acons A (a,y) (anil A)) pf m)).
  Proof.
    Induction m. Simpl. Intros. Apply alist_sorted_1_imp_2. Apply alist_sorted_imp_1. Reflexivity.
    Intros. Simpl. Apply alist_sorted_1_imp_2. Apply alist_sorted_imp_1. Reflexivity.
    Intros. Simpl. Apply alist_conc_sorted.
    Exact (H [a0:ad](pf (ad_double a0)) (ad_comp_double_monotonic pf H1)).
    Exact (H0 [a0:ad](pf (ad_double_plus_un a0)) (ad_comp_double_plus_un_monotonic pf H1)).
    Intros. Elim (alist_of_Map_nth_ad m0 [a0:ad](pf (ad_double a0))
       (MapFold1 A (alist A) (anil A) (aapp A)
         [a0:ad][y:A](acons A (a0,y) (anil A))
         [a0:ad](pf (ad_double a0)) m0) (refl_equal ? ?) n H2).
    Intros a H4. Rewrite H4. Elim (alist_of_Map_nth_ad m1 [a0:ad](pf (ad_double_plus_un a0))
       (MapFold1 A (alist A) (anil A) (aapp A)
         [a0:ad][y:A](acons A (a0,y) (anil A))
         [a0:ad](pf (ad_double_plus_un a0)) m1) (refl_equal ? ?) n' H3).
    Intros a' H5. Rewrite H5. Unfold ad_monotonic in H1. Apply H1. Apply ad_less_def_3.
  Qed.

  Lemma alist_of_Map_sorts : (m:(Map A)) (alist_sorted (alist_of_Map A m))=true.
  Proof.
    Intro. Apply alist_sorted_2_imp.
    Exact (alist_of_Map_sorts_1 m [a0:ad]a0 [a,a':ad][p:(ad_less a a')=true]p).
  Qed.

  Lemma alist_of_Map_sorts1 : (m:(Map A)) (alist_sorted_1 (alist_of_Map A m)).
  Proof.
    Intro. Apply alist_sorted_imp_1. Apply alist_of_Map_sorts.
  Qed.
 
  Lemma alist_of_Map_sorts2 : (m:(Map A)) (alist_sorted_2 (alist_of_Map A m)).
  Proof.
    Intro. Apply alist_sorted_1_imp_2. Apply alist_of_Map_sorts1.
  Qed.
 
  Lemma ad_less_total : (a,a':ad) {(ad_less a a')=true}+{(ad_less a' a)=true}+{a=a'}.
  Proof.
    Intro a. Refine (ad_rec_double a [a:ad] (a':ad){(ad_less a a')=true}+{(ad_less a' a)=true}+{a=a'}
                            ? ? ?).
    Intro. Elim (sumbool_of_bool (ad_less ad_z a')). Intro H. Left . Left . Assumption.
    Intro H. Right . Rewrite (ad_z_less_2 a' H). Reflexivity.
    Intros a0 H a'. Refine (ad_rec_double a' [a':ad] {(ad_less (ad_double a0) a')=true}
                                 +{(ad_less a' (ad_double a0))=true}+{(ad_double a0)=a'} ? ? ?).
    Elim (sumbool_of_bool (ad_less ad_z (ad_double a0))). Intro H0. Left . Right . Assumption.
    Intro H0. Right . Exact (ad_z_less_2 ? H0).
    Intros a1 H0. Rewrite ad_less_def_1. Rewrite ad_less_def_1. Elim (H a1). Intro H1.
    Left . Assumption.
    Intro H1. Right . Rewrite H1. Reflexivity.
    Intros a1 H0. Left . Left . Apply ad_less_def_3.
    Intros a0 H a'. Refine (ad_rec_double a' [a':ad] {(ad_less (ad_double_plus_un a0) a')=true}
                                 +{(ad_less a' (ad_double_plus_un a0))=true}
                                 +{(ad_double_plus_un a0)=a'} ? ? ?).
    Left . Right . (Case a0; Reflexivity).
    Intros a1 H0. Left . Right . Apply ad_less_def_3.
    Intros a1 H0. Rewrite ad_less_def_2. Rewrite ad_less_def_2. Elim (H a1). Intro H1.
    Left . Assumption.
    Intro H1. Right . Rewrite H1. Reflexivity.
  Qed.

  Lemma alist_too_low : (l:(alist A)) (a,a':ad) (y:A)
      (ad_less a a')=true -> (alist_sorted_2 (cons (a',y) l)) ->
      	(alist_semantics A (cons (a',y) l) a)=(NONE A).
  Proof.
    Induction l. Intros. Simpl. Elim (sumbool_of_bool (ad_eq a' a)). Intro H1.
    Rewrite (ad_eq_complete ? ? H1) in H. Rewrite (ad_less_not_refl a) in H. Discriminate H.
    Intro H1. Rewrite H1. Reflexivity.
    Intro r. Elim r. Intros a y l0 H a0 a1 y0 H0 H1.
    Change (Case (ad_eq a1 a0) of
               (SOME A y0)
               (alist_semantics A (cons (a,y) l0) a0)
               end)=(NONE A).
    Elim (sumbool_of_bool (ad_eq a1 a0)). Intro H2. Rewrite (ad_eq_complete ? ? H2) in H0.
    Rewrite (ad_less_not_refl a0) in H0. Discriminate H0.
    Intro H2. Rewrite H2. Apply H. Apply ad_less_trans with a':=a1. Assumption.
    Unfold alist_sorted_2 in H1. Apply (H1 (0) (1)). Apply lt_n_Sn.
    Simpl. Apply le_n_S. Apply le_n_S. Apply le_O_n.
    Apply alist_sorted_1_imp_2. Apply alist_sorted_imp_1.
    Cut (alist_sorted (cons (a1,y0) (cons (a,y) l0)))=true. Intro H3.
    Exact (proj2 ? ? (andb_prop ? ? H3)).
    Apply alist_sorted_2_imp. Assumption.
  Qed.

  Lemma alist_semantics_nth_ad : (l:(alist A)) (a:ad) (y:A)
      (alist_semantics A l a)=(SOME A y) ->
      	{n:nat | (le (S n) (length l)) /\ (alist_nth_ad n l)=a}.
  Proof.
    Induction l. Intros. Discriminate H.
    Intro r. Elim r. Intros a y l0 H a0 y0 H0. Simpl in H0. Elim (sumbool_of_bool (ad_eq a a0)).
    Intro H1. Rewrite H1 in H0. Split with O. Split. Simpl. Apply le_n_S. Apply le_O_n.
    Simpl. Exact (ad_eq_complete ? ? H1).
    Intro H1. Rewrite H1 in H0. Elim (H a0 y0 H0). Intros n' H2. Split with (S n'). Split.
    Simpl. Apply le_n_S. Exact (proj1 ? ? H2).
    Exact (proj2 ? ? H2).
  Qed.

  Lemma alist_semantics_tail : (l:(alist A)) (a:ad) (y:A)
      (alist_sorted_2 (cons (a,y) l)) ->
      	(eqm A (alist_semantics A l) [a0:ad] if (ad_eq a a0)
                                             then (NONE A)
					     else (alist_semantics A (cons (a,y) l) a0)).
  Proof.
    Unfold eqm. Intros. Elim (sumbool_of_bool (ad_eq a a0)). Intro H0. Rewrite H0.
    Rewrite <- (ad_eq_complete ? ? H0). Unfold alist_sorted_2 in H.
    Elim (option_sum A (alist_semantics A l a)). Intro H1. Elim H1. Intros y0 H2.
    Elim (alist_semantics_nth_ad l a y0 H2). Intros n H3. Elim H3. Intros.
    Cut (ad_less (alist_nth_ad (0) (cons (a,y) l)) (alist_nth_ad (S n) (cons (a,y) l)))=true.
    Intro. Simpl in H6. Rewrite H5 in H6. Rewrite (ad_less_not_refl a) in H6. Discriminate H6.
    Apply H. Apply lt_O_Sn.
    Simpl. Apply le_n_S. Assumption.
    Trivial.
    Intro H0. Simpl. Rewrite H0. Reflexivity.
  Qed.

  Lemma alist_semantics_same_tail : (l,l':(alist A)) (a:ad) (y:A)
      (alist_sorted_2 (cons (a,y) l)) -> (alist_sorted_2 (cons (a,y) l')) ->
      	(eqm A (alist_semantics A (cons (a,y) l)) (alist_semantics A (cons (a,y) l'))) ->
	  (eqm A (alist_semantics A l) (alist_semantics A l')).
  Proof.
    Unfold eqm. Intros. Rewrite (alist_semantics_tail ? ? ? H a0).
    Rewrite (alist_semantics_tail ? ? ? H0 a0). Case (ad_eq a a0). Reflexivity.
    Exact (H1 a0).
  Qed.

  Lemma alist_sorted_tail : (l:(alist A)) (a:ad) (y:A)
      (alist_sorted_2 (cons (a,y) l)) -> (alist_sorted_2 l).
  Proof.
    Unfold alist_sorted_2. Intros. Apply (H (S m) (S n)). Apply lt_n_S. Assumption.
    Simpl. Apply le_n_S. Assumption.
  Qed.

  Lemma alist_canonical : (l,l':(alist A))
      (eqm A (alist_semantics A l) (alist_semantics A l')) ->
      	(alist_sorted_2 l) -> (alist_sorted_2 l') -> l=l'.
  Proof.
    Unfold eqm. Induction l. Induction l'. Trivial.
    Intro r. Elim r. Intros a y l0 H H0 H1 H2. Simpl in H0.
    Cut (NONE A)=(Case (ad_eq a a) of (SOME A y)
                           (alist_semantics A l0 a)
                           end).
    Rewrite (ad_eq_correct a). Intro. Discriminate H3.
    Exact (H0 a).
    Intro r. Elim r. Intros a y l0 H. Induction l'. Intros. Simpl in H0.
    Cut (Case (ad_eq a a) of (SOME A y)
                         (alist_semantics A l0 a)
                         end)=(NONE A).
    Rewrite (ad_eq_correct a). Intro. Discriminate H3.
    Exact (H0 a).
    Intro r'. Elim r'. Intros a' y' l'0 H0 H1 H2 H3. Elim (ad_less_total a a'). Intro H4.
    Elim H4. Intro H5.
    Cut (alist_semantics A (cons (a,y) l0) a)=(alist_semantics A (cons (a',y') l'0) a).
    Intro. Rewrite (alist_too_low l'0 a a' y' H5 H3) in H6. Simpl in H6.
    Rewrite (ad_eq_correct a) in H6. Discriminate H6.
    Exact (H1 a).
    Intro H5. Cut (alist_semantics A (cons (a,y) l0) a')=(alist_semantics A (cons (a',y') l'0) a').
    Intro. Rewrite (alist_too_low l0 a' a y H5 H2) in H6. Simpl in H6.
    Rewrite (ad_eq_correct a') in H6. Discriminate H6.
    Exact (H1 a').
    Intro H4. Rewrite H4.
    Cut (alist_semantics A (cons (a,y) l0) a)=(alist_semantics A (cons (a',y') l'0) a).
    Intro. Simpl in H5. Rewrite H4 in H5. Rewrite (ad_eq_correct a') in H5. Inversion H5.
    Rewrite H4 in H1. Rewrite H7 in H1. Cut l0=l'0. Intro. Rewrite H6. Reflexivity.
    Apply H. Rewrite H4 in H2. Rewrite H7 in H2.
    Exact (alist_semantics_same_tail l0 l'0 a' y' H2 H3 H1).
    Exact (alist_sorted_tail ? ? ? H2).
    Exact (alist_sorted_tail ? ? ? H3).
    Exact (H1 a).
  Qed.

End LSort.