Inductive List : Set :=
nil : List
| cons : nat -> List -> List.

Fixpoint comp (m n:nat) {struct m}:bool :=
match (m,n) with
(0,_) => true
| (S p,S q)=> comp p q
| _ => false
end. 

Theorem total: forall n aux :nat, comp n aux=false-> comp aux n=true.
intro.
induction n.
intros.
unfold comp in H.
discriminate H.
intro.
induction aux.
unfold comp.
intro.
reflexivity.
unfold comp.
fold comp.
apply IHn.
Defined.

Fixpoint iseq (m n:nat) {struct m}:bool :=
match (m,n) with
(0,0) => true
| (S p,S q)=> iseq p q
| _ => false
end. 

Lemma iseq_refl:forall n, iseq n n=true.
induction n.
unfold iseq.
reflexivity.
unfold iseq.
fold iseq.
exact IHn.
Defined.

Lemma iseq_ref:forall n m, iseq n m=true-> n=m.
induction n.
induction m.
intros.
reflexivity.
unfold iseq.
intro H.
discriminate H.
intros m.
induction m.
unfold iseq.
intro H.
discriminate H.
unfold iseq.
fold iseq.
intro.
assert (n=m).
apply IHn.
exact H.
rewrite H0.
reflexivity.
Defined.

Lemma iseq_sym:forall m n, iseq m n= iseq n m.
induction m.
induction n.
reflexivity.
unfold iseq.
reflexivity.
induction n.
unfold iseq.
reflexivity.
unfold iseq.
fold iseq.
rewrite (IHm n).
reflexivity.
Defined.


Lemma comp_trans:forall m n p, (comp m n)=true->comp n p=true->comp m p=true.
induction m.
intros.
unfold comp.
reflexivity.
induction n.
intros.
discriminate H.
intro.
induction p.
intros.
discriminate H0.
unfold comp.
fold comp.
intros.
apply (IHm n).
exact H.
exact H0.
Defined.

Fixpoint Comp (l:List):= fun n=>
match l with 
nil => true
| cons m l' => if (comp m n) then Comp l' n else false
end.

Lemma Ccomp: forall l, forall m n,
(Comp l m=true)->(comp m n=true)-> Comp l n=true.
induction l.
simpl.
auto.
simpl.
intros.
assert (comp n m=true).
induction (comp n m).
reflexivity.
discriminate H.
rewrite H1 in H.
assert (comp n n0=true).
apply (comp_trans n m).
exact H1.
exact H0.
rewrite H2.
apply (IHl m n0).
exact H.
exact H0.
Defined.

Fixpoint isOrd (l:List):bool :=
match l with
nil => true
| cons a l' => match l' with
                            nil => true
                            | cons b l'' => if (comp b a) then (isOrd l') else false

                       end 
end.

Lemma isOrd_pre:  forall l:List,forall n:nat,
 (isOrd (cons n l) = true)-> isOrd l = true.
intro.
induction l.
intro.
unfold isOrd.
intro.
reflexivity.
intro.
unfold isOrd.
fold isOrd.
induction (comp n n0).
intro.
exact H.
intro.
discriminate H.
Defined.


Lemma OC: forall l, forall n, 
isOrd (cons n l)=true <-> (Comp l n=true /\ isOrd l=true).
induction l.
split.
unfold isOrd.
intros.
unfold Comp.
split.
reflexivity.
reflexivity.
unfold isOrd.
intro.
reflexivity.
intro.
split.
intro.
assert (isOrd (cons n l)=true).
apply (isOrd_pre (cons n l) n0).
exact H.
split;[idtac|exact H0].
elim (IHl n).
clear IHl.
intros.
elim H1;[idtac|exact H0].
clear H1.
intros.
clear H2.
unfold isOrd in H. fold isOrd in H.
unfold Comp. fold Comp.
assert (comp n n0=true).
induction(comp n n0).
reflexivity.
exact H.
clear H.
rewrite H2.
apply (Ccomp  l n n0).
exact H1.
exact H2.
unfold Comp.
fold Comp.
intro.
elim H.
clear H.
intros.
assert (comp n n0=true).
induction (comp n n0).
reflexivity.
exact H.
rewrite H1 in H.
unfold isOrd.
fold isOrd.
rewrite H1.
unfold isOrd in H0.
fold isOrd in H0.
exact H0.
Defined.

Inductive exList :Set:=
error : exList
| cast : List -> exList.

Fixpoint remove (n:nat) (l:List) {struct l} :=
match l with 
nil => error
| cons m l' => if (iseq n m) then cast l' else 
                              match (remove n l') with
                              error => error
                              | cast l'' => cast (cons m l'')
                              end
end.

Lemma rem_lem: forall n n0 l, 
iseq n n0=false
-> (exists x0,remove n0 l=cast x0
/\ exists x1,remove n x0=cast x1)
->exists l', remove n l=cast l'.
intros.
induction l.
elim H0;clear H0;intros.
elim H0;clear H0;intros.
simpl in H0;discriminate H0.
elim H0;clear H0;intros.
elim H0;clear H0;intros.
elim H1;clear H1;intros.
simpl.
assert (iseq n n1=true\/iseq n n1=false).
induction (iseq n n1).
left;reflexivity.
right;reflexivity.
elim H2.
clear H2;intros.
rewrite H2.
exists l.
reflexivity.
clear H2;intros.
rewrite H2.
assert (exists l0, remove n l=cast l0).
assert (iseq n0 n1=true\/iseq n0 n1=false).
induction (iseq n0 n1).
left;reflexivity.
right;reflexivity.
elim H3.
clear H3;intros.
simpl in H0.
rewrite H3 in H0.
injection H0;clear H0;intros.
rewrite H0.
exists x0.
exact H1.
simpl in H0.
clear H3;intros;rewrite H3 in H0.
assert (exists l5, remove n0 l=cast l5).
induction (remove n0 l).
discriminate H0.
exists l0.
reflexivity.
elim H4;clear H4;intros.
rewrite H4 in H0.
injection H0;clear H0;intros.
rewrite <- H0 in H1.
simpl in H1.
rewrite H2 in H1.
apply IHl.
exists x1.
split.
exact H4.
induction (remove n x1).
discriminate H1.
exists l0.
reflexivity.
elim H3;clear H3;intros.
rewrite H3.
exists (cons n1 x1).
reflexivity.
Defined.

Lemma remComp: forall l,forall n m, 
forall l', Comp l m =true ->  remove n l = cast l' -> comp n m=true/\Comp l' m=true.
induction l.
simpl.
intros.
discriminate H0.
simpl.
intros.
assert (comp n m=true).
induction (comp n m);[idtac|discriminate H].
reflexivity.
rewrite H1 in H.
assert (iseq n0 n=true \/ iseq n0 n=false).
induction (iseq n0 n).
left; reflexivity.
right;reflexivity.
elim H2.
clear H2.
intro.
rewrite H2 in H0.
assert (n0=n).
apply iseq_ref.
exact H2.
rewrite H3.
split.
exact H1.
injection H0;clear H0;intro.
rewrite H0 in H.
exact H.
clear H2.
intro.
rewrite H2 in H0.
assert (exists l'', remove n0 l=cast l'').
induction (remove n0 l).
discriminate H0.
exists l0.
reflexivity.
elim H3;clear H3;intros.
rewrite H3 in H0.
injection H0;clear H0;intro.
rewrite <- H0.
simpl.
rewrite H1.
apply IHl.
exact H.
exact H3.
Defined.



Lemma rem_com: forall n m l l' l'',
iseq n m=false->
remove m l=cast l'->
remove n l=cast l''->
remove n l'=remove m l''/\(exists l0,remove n l'=cast l0).
induction l.
simpl.
intros.
discriminate H0.
simpl.
intros.
assert (iseq m n0=true\/iseq m n0=false).
induction (iseq m n0).
left;reflexivity.
right;reflexivity.
assert (iseq n n0=true\/iseq n n0=false).
induction (iseq n n0).
left;reflexivity.
right;reflexivity.
elim H2.
clear H2.
intros.
rewrite H2 in H0.
injection H0.
clear H0.
intros.
rewrite <- H0.
elim H3.
clear H3.
intros.
assert (m=n0).
apply iseq_ref.
exact H2.
assert (n=n0).
apply iseq_ref.
exact H3.
assert (iseq n m=true).
rewrite H4.
rewrite H5.
apply (iseq_refl).
rewrite H6 in H.
discriminate H.
clear H3.
intros.
rewrite H3 in H1.
induction (remove n l).
discriminate H1.
injection H1.
clear H1.
intros.
rewrite <- H1.
simpl.
rewrite H2.
split.
reflexivity.
exists l0.
reflexivity.
clear H2.
intros.
rewrite H2 in H0.
elim H3.
clear H3;intros.
rewrite H3 in H1.
injection H1.
clear H1;intro.
rewrite <- H1.
induction (remove m l).
discriminate H0.
injection H0;clear H0;intro.
rewrite <- H0.
simpl.
rewrite H3.
split.
reflexivity.
exists l0.
reflexivity.
clear H3;intros.
rewrite H3 in H1.
induction (remove m l).
discriminate H0.
induction (remove n l).
discriminate H1.
injection H0;clear H0;intros.
injection H1;clear H1;intros.
rewrite <- H0.
rewrite <- H1.
assert (remove n l0=remove m l1/\exists l3,remove n l0=cast l3).
apply IHl.
exact H.
reflexivity.
reflexivity.
simpl.
rewrite H3.
rewrite H2.
elim H4;clear H4;intros.
split.
rewrite H4.
reflexivity.
elim H5.
clear H5;intros.
rewrite H5.
exists (cons n0 x).
reflexivity.
Defined.




Fixpoint inc (l l':List) {struct l} :=
match l with
nil => match l' with nil => true | _ => false end
| cons n l1 => match (remove n l') with
         error => false
         | cast l2 => inc l1 l2
         end
end.


Lemma inc_rem2: forall n l l' l0, 
inc l l'=true 
-> remove n l=cast l0
-> (exists l1,remove n l'=cast l1/\ inc l0 l1=true).
intro.
induction l.
simpl.
intros.
discriminate H0.
intros.
assert (iseq n n0=true\/iseq n n0=false).
induction (iseq n n0).
left;reflexivity.
right;reflexivity.
elim H1.
clear H1;intros.
simpl in H0.
rewrite H1 in H0.
assert (n=n0).
apply iseq_ref.
exact H1.
simpl in H.
rewrite <- H2 in H.
induction (remove n l').
discriminate H.
exists l1.
split.
reflexivity.
injection H0;clear H0;intros.
rewrite H0 in H.
exact H.
clear H1;intros.
simpl in H0.
rewrite H1 in H0.
assert (exists l2,remove n l=cast l2).
induction (remove n l).
discriminate H0.
exists (l1).
reflexivity.
elim H2.
clear H2;intros.
rewrite H2 in H0.
rewrite H2 in IHl.
injection H0.
clear H0;intros.
rewrite <- H0.
simpl in H.
simpl.
assert (exists l2, remove n0 l'=cast l2).
induction (remove n0 l').
discriminate H.
exists l1.
reflexivity.
elim H3.
clear H3;intros.
assert (exists l6, remove n x0 = cast l6 /\ inc x l6=true).
apply IHl.
rewrite H3 in H.
exact H.
reflexivity.
clear IHl.
elim H4;clear H4;intros.
elim H4;clear H4;intros.
rewrite H3 in H.
assert (exists l3,remove n l'=cast l3).
apply (rem_lem n n0 l').
exact H1.
exists x0.
split.
exact H3.
exists x1.
exact H4.
elim H6;clear H6;intros.
exists x2.
split.
exact H6.
assert (remove n0 x2=remove n x0/\exists l3,remove n0 x2=cast l3).
apply (rem_com n0 n l').
rewrite (iseq_sym n0 n).
exact H1.
exact H6.
exact H3.
elim H7;clear H7;intros.
rewrite H7.
rewrite H4.
exact H5.
Defined.

Lemma inc_refl: forall l, inc l l=true.
induction l.
unfold inc.
reflexivity.
unfold inc.
fold inc.
unfold remove.
fold remove.
rewrite (iseq_refl n).
exact IHl.
Defined.



Lemma inc_trans: forall l l' l'', (inc l l'=true)->(inc l' l''=true)->(inc l l''=true).
induction l.
simpl;intros.
induction l'.
induction l''.
reflexivity.
simpl in H0.
exact H0.
discriminate H.
simpl.
intros.
assert (exists l2, remove n l'=cast l2).
induction (remove n l').
discriminate H.
exists l0.
reflexivity.
elim H1;clear H1;intros.
rewrite H1 in H.
assert (exists l1,remove n l''=cast l1/\ inc x l1=true).
apply (inc_rem2 n l' l'' x).
exact H0.
exact  H1.
elim H2;clear H2;intros.
elim H2;clear H2;intros.
rewrite H2.
apply (IHl x x0).
exact H.
exact H3.
Defined.


Lemma incComp: forall l' l, forall n, 
(Comp l n =true) -> (inc l' l=true) -> (Comp l' n =true).
induction l'.
simpl.
reflexivity.
intros.
unfold inc in H0.
fold inc in H0.
assert (exists l2, remove n l=cast l2).
induction (remove n l).
discriminate H0.
exists l0.
reflexivity.
elim H1;clear H1;intros.
rewrite H1 in H0.
assert (comp n n0=true).
elim (remComp l n n0 x H H1).
intros.
exact H2.
simpl.
rewrite H2.
apply (IHl' x).
elim (remComp l n n0 x).
intros.
exact H4.
exact H.
exact H1.
exact H0.
Defined.

Lemma insert :forall n l,
(isOrd l=true)->exists l', inc l' (cons n l) =true/\ isOrd l'=true.
induction l.
intros.
exists (cons n nil).
split.
apply inc_refl.
simpl.
reflexivity.
assert (comp n0 n=true\/comp n0 n=false).
induction (comp n0 n).
left; reflexivity.
right;reflexivity.
elim H.
clear H;intros.
exists (cons n (cons n0 l)).
split.
apply inc_refl.
simpl.
rewrite H.
simpl in H0.
exact H0.
clear H;intros.
assert (comp n n0=true).
apply (total n0 n).
exact H.
clear H.
assert (exists l0,inc l0 (cons n l)=true/\isOrd l0=true).
apply IHl.
apply (isOrd_pre l n0).
exact H0.
elim H;clear H;intros.
elim H;clear H;intros.
exists (cons n0 x).
split.
simpl.
rewrite (iseq_refl).
assert (iseq n0 n=true\/iseq n0 n=false).
induction (iseq n0 n).
left; reflexivity.
right;reflexivity.
elim H3.
clear H3;intros.
rewrite H3.
rewrite (iseq_ref n0 n H3).
exact H.
clear H3;intro.
rewrite H3.
exact H.
elim (OC x n0).
intros.
clear H3.
apply H4.
clear H4.
split.
apply (incComp x (cons n l)).
simpl.
rewrite H1.
elim (OC l n0).
intros.
clear H4.
elim H3;clear H3.
intros.
exact H3.
exact H0.
exact H.
exact H2.
Defined.


Lemma sort: forall l:List,exists l':List, ((isOrd l'=true) /\ (inc l' l=true)).
induction l.
exists (nil).
simpl.
split.
reflexivity.
reflexivity.
elim IHl.
clear IHl.
intros.
elim H;clear H;intros.
assert (exists l':List, inc l' (cons n x) =true /\  isOrd l'=true).
apply (insert n x).
exact H.
elim H1;clear H1;intros.
elim H1;clear H1;intros.
exists x0.
split.
exact H2.
assert (inc (cons n x) (cons n l)=true).
simpl.
rewrite (iseq_refl).
exact H0.
apply (inc_trans x0 (cons n x) (cons n l)).
exact H1.
exact H3.
Defined.

Corollary forget: forall l:List, exists l':List, True.
intros.
assert (exists l':List, ((isOrd l'=true) /\ (inc l' l=true))).
apply sort.
elim H;clear H; intros.
exists x.
auto.
Defined.

Notation "x ; y" := (cons x y) (at level 34, right associativity) :type_scope.

Eval compute in (sort (1 ; 4 ; 4; 5 ; 7 ; 3 ; 2 ; 9 ; nil)).