Library listaux

Require Export List.
Require Import Omega.
Require Import Permutation.

Fixpoint set {A:Type} (n:nat) (l:list A) (val:A) {struct l} : list A :=
    match n, l with
      | O, x :: l' => val::l'
      | O, nil => nil
      | S m, nil => nil
      | S m, x :: t => x::(set m t val)
    end.

Lemma set_nth_same: forall (A:Type) (n:nat) (l:list A) (val d:A),
n<length l-> nth n (set n l val) d=val.
Proof.
intros.
revert n H.
induction l.
intros.
simpl in H. inversion H.
intros.
destruct n.
auto.
simpl.
apply IHl.
simpl in H.
omega.
Qed.

Lemma set_nth_different: forall (A:Type) (m n:nat) (l:list A) (val d:A),
 m<>n -> nth n (set m l val) d=nth n l d.
Proof.
intros.
revert m n H.
induction l.
intros.
destruct m;auto.
destruct m;simpl in *.
destruct n;simpl in *;auto.
intros. exfalso. apply H. auto.
intros.
destruct n;simpl in *;auto.
Qed.

Lemma nth_set_same: forall (A:Type) (n:nat) (l:list A) (d:A),
set n l (nth n l d)=l.
Proof.
intros. revert n. induction l.
- intros. destruct n;auto.
- intros. destruct n;auto. simpl. rewrite IHl. auto.
Qed.

Fixpoint setandraise {A:Type} (n:nat) (l:list A) (val def:A) {struct n} : list A :=
    match n, l with
      | O, x :: l' => val::l'
      | O, nil => val::nil
      | S m, nil => def::(setandraise m nil val def)
      | S m, x :: t => x::(setandraise m t val def)
    end.

Lemma setandraise_set: forall (A:Type) (n:nat) (l:list A) (val d:A),
n<length l-> setandraise n l val d=set n l val.
Proof.
intros. revert n H. induction l.
- intros. simpl in H. inversion H.
- intros. destruct n. auto.
simpl. rewrite IHl;auto.
simpl in H. omega.
Qed.

Theorem setandraise_longer: forall (l:list nat) (n val def:nat),
length l<=length (setandraise n l val def).
Proof.
intros. revert n. induction l.
-intros. simpl. destruct n. simpl. auto. simpl. omega.
-intros. simpl. destruct n.
simpl. auto. simpl. specialize(IHl n).
omega.
Qed.

Theorem setandraise_equallength: forall (l:list nat) (n val def:nat),
n<length l -> length l=length (setandraise n l val def).
Proof.
intros. revert n H. induction l.
-intros. simpl in H|-*. inversion H.
-intros. simpl in H|-*. destruct n.
simpl. auto. simpl. f_equal. apply IHl. omega.
Qed.


Inductive issorted : list nat-> Prop :=
|issorted_nil : issorted nil
|issorted_single : forall x:nat, issorted (x::nil)
|issorted_cons : forall (x y:nat) (l':list nat),
  x<=y -> issorted (y::l') -> issorted(x::y::l').

Theorem issorted_12345: issorted (1::2::3::4::5::nil).
Proof.
repeat (constructor;auto).
Qed.

Hint Resolve issorted_nil issorted_single issorted_cons.

Theorem issorted_skip: forall (l:list nat) (n:nat),
issorted (n::l) -> issorted l.
Proof.
destruct l. auto. intros. inversion H. assumption.
Qed.

Lemma issorted_firstn_S: forall (l:list nat) (n:nat),
 issorted (firstn (S n) l) -> issorted (firstn n l).
Proof.
intros l n. revert l. induction n;auto.
intros.
destruct l;simpl;auto.
specialize(IHn l).
simpl in H. inversion H. destruct l;simpl;auto.
destruct n;simpl;auto. inversion H2.
destruct l;simpl;auto. inversion H1.
inversion H1. rewrite H5 in H2, H3. clear y H1 H5 x H0.
rewrite H6 in H3. clear l' H6.
destruct n;simpl;auto.
Qed.

Theorem firstn_issorted: forall l:list nat,
issorted (firstn (length l) l) -> issorted l.
Proof.
induction l.
- auto.
- intros. destruct l. auto. simpl in *. inversion H.
constructor;auto.
Qed.


Theorem permutation12345: Permutation (1::2::3::4::5::nil) (1::4::5::3::2::nil).
Proof.
apply perm_skip;auto.
eapply perm_trans.
apply Permutation_rev. simpl.
apply perm_swap.
Qed.

Theorem Permutation_nil_l: forall {A:Type} (l:list A), Permutation nil l->l=nil.
Proof.
intros A l.
assert(forall m:list A, m=nil -> Permutation m l -> l = m).
- intros m Hm Hlm. induction Hlm.
+ auto.
+ inversion Hm.
+ inversion Hm.
+ rewrite Hm in *;clear l Hm. specialize(IHHlm1 (eq_refl _)).
rewrite IHHlm1 in *;clear l' IHHlm1. apply IHHlm2. auto.
- intros. apply H. auto. assumption.
Qed.

Theorem Permutation_nil_r: forall {A:Type} (l:list A), Permutation l nil->l=nil.
Proof.
intros.
apply Permutation_nil_l.
apply Permutation_sym.
auto.
Qed.


Theorem Permutation_set_displacement: forall {A:Type} (l:list A)
 (i:nat) (val def:A),
S i < length l ->
Permutation (set (S i) l val) (set i (set (S i) l (nth i l def)) val).
Proof.
intros. revert l H. induction i.
- intros. destruct l. inversion H. destruct l. inversion H. inversion H1.
simpl. apply perm_swap.
- intros. destruct l. inversion H.
destruct i. destruct l. inversion H. inversion H1.
simpl. apply perm_skip. destruct l. inversion H. inversion H1. inversion H3.
simpl. apply perm_swap. simpl in H.
assert(Hlength:S (S i) < length l). omega.
specialize(IHi l Hlength).
simpl. apply perm_skip. exact IHi.
Qed.