sort_compl.v

(**
This file is part of the Elfic library

Copyright (C) Boldo, Clément, Faissole, Martin, Mayero

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)

From Coq Require Import ClassicalDescription.
From Coq Require Import Lia Reals List Sorted Permutation.

Require Import logic_compl. (* For strong_induction. *)
Require Import list_compl.
Require Import R_compl.

Open Scope list_scope.


Section Insertion_sort.

(** Insertion sort. *)

Context {A : Set}.
Variable ord : A -> A -> Prop.

Lemma Permutation_ex :
  forall (a : A) l l',
    Permutation (a :: l) l' ->
    exists l1 l2,
      l' = l1 ++ (cons a l2) /\ Permutation l (l1 ++ l2).
Proof.
intros a l l' Hl.
assert (H:In a l').
apply Permutation_in with (a::l); try easy.
apply in_eq.
destruct (in_split _ _ H) as (l1,(l2, H1)).
exists l1; exists l2; split; try easy.
apply Permutation_cons_inv with a.
rewrite H1 in Hl.
apply Permutation_trans with (1:=Hl).
rewrite Permutation_app_comm.
simpl.
apply perm_skip.
apply Permutation_app_comm.
Qed.

Definition leqb : A -> A -> bool :=
  fun x y => match excluded_middle_informative (ord x y) with
    | left _ => true
    | right _  => false
    end.

Lemma leqb_true : forall a b, leqb a b = true -> ord a b.
Proof.
intros a b H.
unfold leqb in H.
destruct (excluded_middle_informative (ord a b));auto.
exfalso;auto.
Qed.

Lemma leqb_false : forall a b, leqb a b = false -> ~ord a b.
Proof.
intros a b H.
unfold leqb in H.
destruct (excluded_middle_informative (ord a b));auto.
Qed.

Fixpoint insert (x : A) (l : list A) {struct l} : list A :=
  match l with
  | nil => x :: nil
  | y :: tl => if leqb x y then x :: l else y :: insert x tl
  end.

Fixpoint sort (l : list A) : list A :=
  match l with
  | nil => nil
  | x :: tl => insert x (sort tl)
  end.

Lemma corr_insert : forall (x : A) l, Permutation (x :: l) (insert x l).
Proof.
intros x.
induction l;intros.
simpl;apply perm_skip.
apply perm_nil.
simpl.
case (leqb x a).
apply Permutation_refl.
assert (Permutation (a::x::l) (a:: insert x l)).
now apply perm_skip.
apply perm_trans with (l':=(a::x::l));auto.
apply perm_swap.
Qed.

Lemma corr_sort : forall l, Permutation l (sort l).
Proof.
induction l;intros.
simpl;apply perm_nil.
apply perm_trans with (l':=(a::(sort l)));auto.
simpl;apply corr_insert.
Qed.

Lemma LocallySorted_0_1 :
  forall P l (a0 a : A),
    l <> nil -> LocallySorted P l -> LocallySorted P (a0 :: l) ->
    P a0 (nth 0 l a).
Proof.
intros P; induction l;intros.
exfalso;now apply H.
inversion H1.
now simpl.
Qed.

(* Useful?
Lemma LocallySorted_0_1_nil :
  forall P l (a0 : A),
    l <> nil -> LocallySorted P l -> LocallySorted P (a0 :: l) ->
    P a0 (nth 0 l a0).
Proof.
intros; now apply LocallySorted_0_1.
Qed.
*)

Lemma LocallySorted_cons :
  forall P (a : A) l,
    LocallySorted P (a :: l) ->
    LocallySorted P l.
Proof.
induction l;simpl;intros.
apply LSorted_nil.
now inversion H.
Qed.

Lemma LocallySorted_0_1_alt :
  forall P (a : A) l,
    LocallySorted P l -> (1 < length l)%nat ->
    P (nth 0 l a) (nth (S 0) l a).
Proof.
induction l.
simpl;intros.
contradict H0; easy.
intros.
simpl.
case_eq l; try easy.
intros H1; contradict H0; rewrite H1; simpl; auto with arith.
intros a1 l0 H1; rewrite H1 in H.
apply LocallySorted_0_1; try discriminate; auto.
now apply LocallySorted_cons with a0.
Qed.

Lemma LocallySorted_nth :
  forall P (a : A) l,
    (forall i, (i < length l - 1)%nat ->
    LocallySorted P l ->
    P (nth i l a) (nth (S i) l a)).
Proof.
intros P; induction l;intros.
inversion H.
destruct (eq_nat_dec i 0).
(*i=0*)
rewrite e;simpl;apply LocallySorted_0_1;auto.
red;intro;rewrite H1 in H;simpl in H.
inversion H.
now apply LocallySorted_cons with a0.
(*i<>0*)
assert ((i-1<length l - 1)%nat).
rewrite length_cons_1 in H.
assert ((length l + 1 - 1)=length l)%nat.
lia.
rewrite H1 in H;lia.
assert (LocallySorted P l).
now apply LocallySorted_cons with a0.
generalize (IHl (i-1)%nat H1 H2);clear IHl;intro IHl.
rewrite (nth_cons a0 a l (i-1)%nat) in IHl.
assert (S (i - 1)=i)%nat.
lia.
rewrite H3 in IHl;now rewrite <-(nth_cons a0 a l).
Qed.

Lemma insert_hd_dec :
  forall (a r : A) l, {hd a (insert r l) = r} + {hd a (insert r l) = hd a l}.
Proof.
intros n r l;induction l.
left;simpl;reflexivity.
simpl;destruct (leqb r a).
left;simpl;reflexivity.
right;simpl;reflexivity.
Qed.

Lemma LocallySorted_insert :
  forall l a,
    (forall x y, ~ ord x y -> ord y x) ->
    LocallySorted ord l ->
    LocallySorted ord (insert a l).
Proof.
intros l a Hord Hl; simpl;induction l;simpl.
apply LSorted_cons1.
case_eq (leqb a a0).
intros;apply LSorted_consn;auto.
now apply leqb_true.
intros;case_eq (insert a l).
intros H0;apply LSorted_cons1;auto.
intros r l0 H0;
  destruct (insert_hd_dec a0 a l) as [H1 | H2].
case_eq (leqb a0 r);intro H2.
apply LSorted_consn;auto.
rewrite <- H0;apply IHl.
now apply LocallySorted_cons with a0.
now apply leqb_true.
apply LSorted_consn;auto.
rewrite <- H0;apply IHl;
  now apply LocallySorted_cons with a0.
rewrite H0 in H1;simpl in H1;rewrite <- H1 in H;
  generalize (leqb_false r a0 H).
intro H3;apply Hord; easy.
case_eq (leqb a0 r);intro H3.
apply LSorted_consn;auto.
rewrite <- H0;apply IHl.
now apply LocallySorted_cons with a0.
now apply leqb_true.
apply LSorted_consn;auto.
rewrite <- H0;apply IHl.
now apply LocallySorted_cons with a0.
rewrite H0 in H2;simpl in H2;rewrite H2; simpl.
inversion Hl; simpl.
destruct (excluded_middle_informative (ord a0 a0));auto.
easy.
Qed.

Lemma LocallySorted_sort :
  forall l,
    (forall x y, ~ ord x y -> ord y x) ->
    LocallySorted ord (sort l).
Proof.
intros l Hord; induction l.
apply LSorted_nil.
simpl; now apply (LocallySorted_insert (sort l) a).
Qed.

Lemma LocallySorted_impl :
  forall (P1 P2 P3 : A -> A -> Prop) l,
    (forall a b, P1 a b -> P2 a b -> P3 a b) ->
    LocallySorted P1 l -> LocallySorted P2 l -> LocallySorted P3 l.
Proof.
intros P1 P2 P3; intros l; case l.
intros; apply LSorted_nil.
clear l; intros r1 l; generalize r1; clear r1.
induction l.
intros; apply LSorted_cons1.
intros r1 H0 H1 H2.
apply LSorted_consn.
apply IHl; try easy.
now apply LocallySorted_cons with r1.
now apply LocallySorted_cons with r1.
apply H0.
now inversion H1.
now inversion H2.
Qed.

Lemma LocallySorted_neq :
  forall l, NoDup l -> LocallySorted (fun x y : A => x <> y) l.
Proof.
intros l; case l.
intros; apply LSorted_nil.
clear l; intros a l; generalize a; clear a.
induction l.
intros; apply LSorted_cons1.
intros b H1.
apply LSorted_consn.
apply IHl; try easy.
now apply (NoDup_cons_iff b (a::l)).
assert (~(In b (a::l))).
now apply (NoDup_cons_iff b (a::l)).
intros H2; apply H; rewrite H2.
apply in_eq.
Qed.

Lemma LocallySorted_extends :
  forall l (a x : A),
    (forall x y z, ord x y -> ord y z -> ord x z) ->
    LocallySorted ord (a :: l) ->
    In x l -> ord a x.
Proof.
intros l a x Ho Hl.
apply Forall_forall.
apply Sorted_extends; try assumption.
now apply Sorted_LocallySorted_iff.
Qed.

Lemma LocallySorted_cons2 :
  forall (a b : A) l,
    (forall x y z, ord x y -> ord y z -> ord x z) ->
    LocallySorted ord (a :: b :: l) -> LocallySorted ord (a :: l).
Proof.
intros a b l Ho Hl.
inversion Hl; inversion H1.
apply LSorted_cons1.
apply LSorted_consn; try easy.
now apply Ho with b.
Qed.

Lemma LocallySorted_select :
  forall P l,
    (forall x y z, ord x y -> ord y z -> ord x z) ->
    LocallySorted ord l ->
    LocallySorted ord (select P l).
Proof.
induction l.
intros;apply LSorted_nil.
intros Ho H1.
generalize (LocallySorted_cons ord a l H1);intro H2.
simpl;case (excluded_middle_informative (P a));intro H.
2: now apply IHl.
generalize (IHl Ho H2);intro H0.
case_eq (select P l).
intros _; apply LSorted_cons1.
intros b l' H3.
apply LSorted_consn.
rewrite <- H3; easy.
apply LocallySorted_extends with l; try easy.
apply In_select_In with P.
rewrite H3; apply in_eq.
Qed.

End Insertion_sort.


Open Scope R_scope.


Section Sort_R.

(** Sorting lists on R. **)

Lemma LocallySorted_sort_Rle : forall l, LocallySorted Rle (sort Rle l).
Proof.
intros l; apply LocallySorted_sort.
intros x y H; auto with real.
Qed.

Lemma LocallySorted_map :
  forall (P : R -> R -> Prop) f l,
    (forall x y, P x y -> P (f x) (f y)) ->
    LocallySorted P l ->
    LocallySorted P (map f l).
Proof.
intros P f l; case l.
intros H1 H2; simpl.
apply LSorted_nil.
clear l; intros a l; generalize a; clear a.
induction l.
intros a H1 H2; simpl.
apply LSorted_cons1.
intros b H1 H2; simpl.
apply LSorted_consn.
apply IHl; try easy.
inversion H2; easy.
apply H1.
inversion H2; easy.
Qed.

Lemma LocallySorted_Rlt_inj :
  forall l i j,
    LocallySorted Rlt l ->
    (i < length l)%nat -> (j < length l)%nat ->
    nth i l 0 = nth j l 0 -> i = j.
Proof.
assert (forall l i j,
    LocallySorted Rlt l ->
    (i < length l)%nat -> (j < length l)%nat ->
    nth i l 0 = nth j l 0 -> (i < j)%nat -> False).
intros l i j H1 Hi Hj H2 H3.
absurd ((nth i l 0) < (nth j l 0)).
rewrite H2; auto with real.
generalize (LocallySorted_nth Rlt 0%R l); intros H4.
apply Rlt_le_trans with (nth (S i) l 0).
apply H4; auto with arith.
case (le_lt_or_eq 0 (length l)); auto with zarith.
apply Rlt_increasing with (u:=fun n=> nth n l 0)
  (N:=(length l-1)%nat); try easy.
intros; apply H4; easy.
split; auto with zarith.
intros l i j H1 H2 H3 H4.
case (le_or_lt i j); intros H5.
case (le_lt_or_eq i j H5); intros H6; try easy.
exfalso; apply H with l i j; auto.
exfalso; apply H with l j i; auto.
Qed.

End Sort_R.


Section Sorted_In_eq_eq_Sec.

Lemma Sorted_In_eq_eq_aux1:
  forall (l1 l2 : list R),
    (forall x, In x l1 <-> In x l2) ->
    (LocallySorted Rlt l1) -> (LocallySorted Rlt l2) ->
    l1 <> nil -> l2 <> nil ->
    forall i,
      (i < min (length l1) (length l2))%nat ->
      Rle (nth i l1 0) (nth i l2 0).
Proof.
intros l1 l2 H V1 V2 Z1 Z2 i.
apply (strong_induction (fun i => (i < min (length l1) (length l2))%nat
    -> Rle (nth i l1 0) (nth i l2 0))).
intros n Hn1 Hn2.
case_eq n.
(* u1 0 <= u2 0 *)
intros Hn3.
assert (T: In (nth 0 l2 0) l1).
apply H.
apply nth_In.
case (le_lt_or_eq 0 (length l2)); auto with arith.
intros V; absurd (l2 = nil); try easy.
apply length_zero_iff_nil; auto.
destruct (In_nth l1 _ 0 T) as (m,(Hm1,Hm2)).
rewrite <- Hm2.
apply Rlt_increasing with (u:=fun i => nth i l1 0) (N:=(length l1-1)%nat); try assumption.
intros j Hj; apply LocallySorted_nth; assumption.
split; lia.
(* u1 (S m) <= u2 (S m) *)
intros nn Hnn.
rewrite <- Hnn.
assert (T: In (nth n l2 0) l1).
apply H.
apply nth_In.
apply le_trans with (1:=Hn2).
auto with arith.
destruct (In_nth l1 _ 0 T) as (m,(Hm1,Hm2)).
case (le_or_lt n m); intros M.
rewrite <- Hm2.
apply Rlt_increasing with  (u:=fun i => nth i l1 0) (N:=(length l1-1)%nat); try assumption.
intros j Hj; apply LocallySorted_nth; assumption.
split; auto with zarith.
absurd (nth m l1 0 = nth n l2 0).
2: now rewrite Hm2.
apply Rlt_not_eq.
apply Rle_lt_trans with (nth m l2 0).
apply Hn1; auto with zarith.
apply Rlt_le_trans with (nth (S m) l2 0).
apply LocallySorted_nth; try assumption.
apply lt_le_trans with (1:=M).
generalize (Nat.le_min_r (length l1) (length l2)); lia.
apply Rlt_increasing with (u:=fun i => nth i l2 0) (N:=(length l2-1)%nat); try assumption.
intros j Hj; apply LocallySorted_nth; assumption.
split; auto with arith.
generalize (Nat.le_min_r (length l1) (length l2)); lia.
Qed.

Lemma Sorted_In_eq_eq_aux2 :
  forall (l1 l2 : list R),
    (forall x, In x l1 <-> In x l2) ->
    (LocallySorted Rlt l1) -> (LocallySorted Rlt l2) ->
    l1 <> nil -> l2 <> nil ->
    forall i,
      (i < min (length l1) (length l2))%nat ->
      (nth i l1 0 = nth i l2 0).
Proof.
intros l1 l2 H V1 V2 Z1 Z2 i Hi.
apply Rle_antisym.
apply Sorted_In_eq_eq_aux1; assumption.
apply Sorted_In_eq_eq_aux1; try assumption.
intros x; split; apply H.
now rewrite Min.min_comm.
Qed.

Lemma Sorted_In_eq_eq_aux3:
  forall (l1 l2 : list R),
    (forall x, In x l1 <-> In x l2) ->
    (LocallySorted Rlt l1) -> (LocallySorted Rlt l2) ->
    l1 <> nil -> l2 <> nil ->
    length l1 = length l2.
Proof.
assert (H: forall (l1 l2 : list R),
    (forall x, In x l1 <-> In x l2) ->
     (LocallySorted Rlt l1) -> (LocallySorted Rlt l2) ->
     l1 <> nil -> l2 <> nil ->
       (length l1 <= length l2)%nat).
intros l1 l2 H V1 V2 Z1 Z2.
case (le_or_lt (length l1) (length l2)); try easy; intros H3.
exfalso.
assert (T: In (nth (length l2) l1 0) l1).
apply nth_In; try easy.
apply H in T.
destruct (In_nth _ _ 0 T) as (m,(Hm1,Hm2)).
absurd (nth m l1 0 = nth (length l2) l1 0).
apply Rlt_not_eq.
apply Rle_lt_trans with (nth (length l2-1) l1 0).
apply Rlt_increasing with  (u:=fun i => nth i l1 0) (N:=(length l1-1)%nat); try assumption.
intros j Hj; apply LocallySorted_nth; assumption.
split; auto with zarith.
replace (length l2) with (S (length l2-1)) at 2.
apply LocallySorted_nth; try assumption.
lia.
assert (length l2 <> 0)%nat; try lia.
rewrite <- Hm2.
apply Sorted_In_eq_eq_aux2; auto; try (split;easy).
rewrite Min.min_r; lia.
intros l1 l2 H0 V1 V2 Z1 Z2.
apply le_antisym.
apply H; assumption.
apply H; try assumption.
intros x; split; apply H0; easy.
Qed.

Lemma Sorted_In_eq_eq_aux4 :
  forall (l1 l2 : list R),
    (forall x, In x l1 <-> In x l2) ->
    (LocallySorted Rlt l1) -> (LocallySorted Rlt l2) ->
    l1 <> nil -> l2 <> nil ->
    l1 = l2.
Proof.
intros l1 l2 H V1 V2 Z1 Z2.
generalize (Sorted_In_eq_eq_aux3 l1 l2 H V1 V2 Z1 Z2).
generalize (Sorted_In_eq_eq_aux2 l1 l2 H V1 V2 Z1 Z2).
intros H3 H4.
rewrite H4 in H3.
rewrite Min.min_r in H3; try lia.
generalize H3 H4; clear V1 V2 H H3 H4 Z1 Z2; generalize l1 l2; clear l1 l2.
induction l1.
intros l2 H1 H2.
apply sym_eq, length_zero_iff_nil.
rewrite <- H2; easy.
intros l2; case l2.
intros H1 H2.
contradict H2; easy.
clear l2; intros r l2 H1 H2.
rewrite IHl1 with l2.
specialize (H1 0%nat); simpl in H1.
rewrite H1; try easy; lia.
intros i Hi.
change (nth i l1 0) with (nth (S i) (a :: l1) 0).
change (nth i l2 0) with (nth (S i) (r :: l2) 0).
apply H1.
simpl; lia.
simpl in H2; lia.
Qed.

Lemma Sorted_In_eq_eq :
  forall (l1 l2 : list R),
    (forall x, In x l1 <-> In x l2) ->
    (LocallySorted Rlt l1) -> (LocallySorted Rlt l2) ->
    l1 = l2.
Proof.
intros l1 l2 H V1 V2.
case_eq l1; case_eq l2.
easy.
intros r2 ll2 J1 J2.
absurd (In r2 l1).
rewrite J2; apply in_nil.
apply H; rewrite J1.
apply in_eq.
intros J2 r1 ll1 J1.
absurd (In r1 l2).
rewrite J2; apply in_nil.
apply H; rewrite J1.
apply in_eq.
intros r2 ll2 J2 r1 ll1 J1; rewrite <- J1, <- J2.
apply Sorted_In_eq_eq_aux4; try easy.
rewrite J1; easy.
rewrite J2; easy.
Qed.

Lemma LocallySorted_Rlt_NoDup : forall l, LocallySorted Rlt l -> NoDup l.
Proof.
intros l Hl.
rewrite (NoDup_nth l 0).
intros i j Y1 Y2 K1.
apply LocallySorted_Rlt_inj with l; easy.
Qed.

End Sorted_In_eq_eq_Sec.