Strictly sorted lists are identical if they are equivalent

Require Import Base.

Implicit Types A N : list nat.

Inductive sorted : list nat -> Prop :=
| sortedN : sorted nil
| sortedC x A : (forall z, z el A -> x < z ) -> sorted A -> sorted (x ::A).

Definition sep (A B : list nat) : Prop :=
  exists x, x el A /\ x nel B \/ x nel A /\ x el B.

Lemma sorted_sep A B :
  sorted A -> sorted B -> A <> B -> sep A B.
Proof.
  intros H. revert B.
  induction H as [ |x A H1 _ IH]; intros B H2 H3.
  - destruct B as [|x B]. congruence. exists x. auto.
  - destruct H2 as [ |y B H5 H6].
    + exists x. auto.
    + assert (x<y \/ y<x \/ x=y) as [H7|[H7|<-]] by omega.
      * exists x. left. split. now auto. intros [<-|H8%H5]; omega.
      * exists y. right. split; [|now auto]. intros [->|H8%H1]; omega.
      * destruct (IH B H6) as [y [[H7 H8]|[H7 H8]]].
        -- congruence.
        -- exists y. left. split. now auto.
           apply H1 in H7. contradict H8.
           destruct H8 as [<-|H8]. omega. exact H8.
        -- exists y. right. split; [|now auto].
           apply H5 in H8. contradict H7.
           destruct H7 as [->|H7]. omega. exact H7.
Qed.

Fact sorted_unique A B :
  sorted A -> sorted B -> A === B <-> A = B.
Proof.
  intros H1 H2. split.
  - intros H3. contra_dec H4.
    destruct (sorted_sep H1 H2 H4) as [x [[H5 H6]|[H5 H6]]].
    + apply H3 in H5. auto.
    + apply H3 in H6. auto.
   - intros <-. reflexivity.
Qed.

Insertion sort

Fixpoint insert x A : list nat :=
  match A with
  | nil => [x ]
  | y::A' => if Dec (x <y) then x ::y::A'
            else if Dec (x =y) then y::A' else y::insert x A'
  end.

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

Lemma insert_equiv x A :
  insert x A === x :: A.
Proof.
  induction A as [|y A IH]; cbn.
  - reflexivity.
  - decide (x < y) as [D|D]. reflexivity.
    decide (x = y) as [<-|E]. now auto.
    rewrite IH. apply equi_swap.
Qed.

Lemma sort_equiv A :
  sort A === A.
Proof.
  induction A as [|x A IH]; cbn.
  - reflexivity.
  - now rewrite insert_equiv, IH.
Qed.

Lemma sorted_cons x y A :
  x < y -> sorted (y ::A) -> sorted (x ::y ::A).
Proof.
  intros H1 H2. constructor.
  - intros z [->|H3]. exact H1.
    enough (y<z) by omega.
    inv H2; auto.
  - constructor; inv H2; auto.
Qed.

Lemma insert_sorted x A :
  sorted A -> sorted (insert x A).
Proof.
  induction 1 as [ |y A H1 H IH]; cbn.
  - auto using sorted.
  - decide (x < y) as [H2|H2].
    + apply sorted_cons; auto using sorted.
    + decide (x = y) as [<-|H3]. now auto using sorted.
      constructor; [|exact IH].
      intros z [->|H4] % insert_equiv. omega. auto.
Qed.

Lemma sort_sorted A :
  sorted (sort A).
Proof.
  induction A as [|x A IH]; cbn.
  - constructor.
  - apply insert_sorted, IH.
Qed.

Theorem sort_normalizer A B :
  A === B <-> sort A = sort B.
Proof.
  rewrite <-sorted_unique.
  - now rewrite !sort_equiv.
  - apply sort_sorted.
  - apply sort_sorted.
Qed.

Exercises

Fact equiv_sep A B :
  A === B <-> ~ sep A B.
Proof.
  split.
  - intros H1 [x [[H2 H3]|[H2 H3]]]; firstorder.
  - intros H1. split; intros x H2; contra_dec H3; apply H1; exists x; auto.
Qed.

Fact sorted_sort_fp A :
  sorted A <-> sort A = A.
Proof.
  split; intros H.
  - apply sorted_unique.
    + apply sort_sorted.
    + exact H.
    + apply sort_equiv.
  - rewrite <-H. apply sort_sorted.
Qed.

Fact sorted_dec A :
  dec (sorted A).
Proof.
  apply dec_transfer with (P:= sort A = A).
  - symmetry. apply sorted_sort_fp.
  - auto.
Qed.

Fact sort_idempotent A :
  sort (sort A) = sort A.
Proof.
  apply sorted_sort_fp.
  apply sort_sorted.
Qed.