Module Qcert.Utils.SortingAdd


This module defines a simple (inefficient) insert sort, used in various parts of the specification.

Require Export Sorting.
Require Import EquivDec.
Require Import List.
Require Import CoqLibAdd.
Require Import ListAdd.
Require Import Permutation.
Require Import Eqdep_dec.
Require Import RelationClasses.

Section SortingAdd.

Insertion sort

  Section InsertionSort.
    Context {A:Type}.
    Context {R:A->A->Prop}.
    Context (R_dec : forall a a', {R a a'} + {~R a a'}).

    Fixpoint insertion_sort_insert a l
      := match l with
         | nil => a :: nil
         | b::xs => if (R_dec a b)
                    then a::b::xs
                    else if (R_dec b a) then
                           b::insertion_sort_insert a xs
                         else b::xs
         end.

    Fixpoint insertion_sort (l:list A)
      := match l with
         | nil => nil
         | a::xs => insertion_sort_insert a (insertion_sort xs)
         end.

    Local Hint Constructors LocallySorted : qcert.

    Lemma insertion_sort_insert_Sorted a (l:list A) :
      Sorted R l -> Sorted R (insertion_sort_insert a l).
Proof.
      repeat rewrite Sorted_LocallySorted_iff.
      induction l; inversion 1; subst; simpl in *;
        repeat match goal with
               | [|- context [R_dec ?x ?y]] => destruct (R_dec x y)
               end; eauto with qcert.
    Qed.

    Local Hint Resolve insertion_sort_insert_Sorted : qcert.

    Lemma insertion_sort_Sorted (l:list A) : Sorted R (insertion_sort l).
Proof.
      induction l; simpl; eauto with qcert.
    Qed.

    Fixpoint is_list_sorted (l:list A) :=
      match l with
      | nil => true
      | x::xs => match xs with
                 | nil => true
                 | y::ls => if R_dec x y then is_list_sorted xs else false
                 end
      end.

    Theorem is_list_sorted_Sorted_iff l:
      is_list_sorted l = true <-> Sorted R l.
Proof.
      induction l; simpl; intuition.
      - destruct l; simpl; eauto.
        destruct (R_dec a a0); simpl; intuition; try discriminate.
      - inversion H1; subst. rewrite H0; auto.
        destruct l; auto.
        inversion H5; subst.
        destruct (R_dec a a0); eauto.
    Qed.

    Corollary insertion_sort_is_list_sorted:
      forall l, is_list_sorted (insertion_sort l) = true.
Proof.
      intros.
      rewrite is_list_sorted_Sorted_iff.
      apply insertion_sort_Sorted.
    Qed.

    Lemma is_list_sorted_ext : forall l (p1 p2:is_list_sorted l = true), p1 = p2.
Proof.
      intros. apply eq_proofs_unicity. decide equality.
    Qed.

    Theorem is_list_sorted_StronglySorted `{Transitive A R}:
      forall l, is_list_sorted l = true <-> StronglySorted R l.
Proof.
      intros.
      rewrite is_list_sorted_Sorted_iff.
      split.
      apply Sorted_StronglySorted.
      red. apply transitivity.
      apply StronglySorted_Sorted.
    Qed.

    Corollary insertion_sort_StronglySorted `{Transitive A R}:
      forall l, StronglySorted R (insertion_sort l).
Proof.
      intros.
      rewrite <- is_list_sorted_StronglySorted.
      apply insertion_sort_is_list_sorted.
    Qed.

    Lemma Forall_nin_irr `{Irreflexive A R}:
      forall a l, Forall (R a) l -> ~ In a l.
Proof.
      induction l; [auto|intros].
      inversion H0; subst; intro.
      inversion H1; subst.
      eapply irreflexivity; eauto.
      elim IHl; auto.
    Qed.

    Lemma StronglySorted_NoDup `{Irreflexive A R}:
      forall l, StronglySorted R l -> NoDup l.
Proof.
      induction l; intros.
      constructor.
      inversion H0; subst.
      constructor; auto. eapply Forall_nin_irr; eauto.
    Qed.

    Lemma Sorted_NoDup `{StrictOrder A R}:
      forall l, Sorted R l -> NoDup l.
Proof.
      intros.
      apply StronglySorted_NoDup; eauto.
      apply Sorted_StronglySorted; eauto.
      red; intros; etransitivity; eauto.
    Qed.

    Lemma is_list_sorted_NoDup `{StrictOrder A R} :
      forall l, is_list_sorted l = true -> NoDup l.
Proof.
      intros.
      eapply Sorted_NoDup; eapply is_list_sorted_Sorted_iff; eauto.
    Defined.

    Lemma is_list_sorted_cons a r :
      is_list_sorted (a::r) = true
      <->
      (is_list_sorted r = true
       /\ match r with
          | nil => True
          | y::_ => R a y
          end).
Proof.
      simpl; destruct r; intuition;
        destruct (R_dec a a0); intuition congruence.
    Qed.

    Lemma is_list_sorted_cons_inv {a r} :
      is_list_sorted (a::r) = true ->
      is_list_sorted r = true.
Proof.
      rewrite is_list_sorted_cons. intuition.
    Qed.

    Lemma StronglySorted_cons_in {x a l} :
      StronglySorted R (a::l) ->
      In x l ->
      R a x.
Proof.
      inversion 1; subst; intros iin.
      rewrite Forall_forall in H3.
      auto.
    Qed.

    Lemma in_insertion_sort_insert {x l a} :
      In x (insertion_sort_insert a l) -> a = x \/ In x l.
Proof.
      revert x a. induction l; simpl; [intuition | ].
      intros x a0.
      case_eq (R_dec a0 a); simpl; intros; trivial.
      revert H0.
      case_eq (R_dec a a0); simpl; intros; intuition.
      destruct (IHl _ _ H2); intuition.
    Qed.

    Lemma in_insertion_sort {x l} :
      In x (insertion_sort l) -> In x l.
Proof.
      induction l; simpl; trivial.
      intros inn. apply in_insertion_sort_insert in inn.
      intuition.
    Qed.

    Lemma is_list_sorted_cons_Forall_lt `{Transitive A R} (a:A) :
      forall l,
        is_list_sorted (a :: l) = true ->
        Forall (fun x => R a x) (insertion_sort l).
Proof.
      intros.
      rewrite Forall_forall; intros.
      rewrite is_list_sorted_StronglySorted in H0.
      inversion H0.
      subst.
      apply (StronglySorted_cons_in H0).
      apply in_insertion_sort; assumption.
    Qed.

    Lemma Forall_insertion_sort {P} l :
      Forall P l -> Forall P (insertion_sort l).
Proof.
      repeat rewrite Forall_forall.
      intros fp x inx.
      apply in_insertion_sort in inx.
      auto.
    Qed.

    Lemma insertion_sort_sorted_is_id l :
      is_list_sorted l = true ->
      insertion_sort l = l.
Proof.
      induction l; intros; simpl in *.
      - reflexivity.
      - assert (is_list_sorted l = true).
        destruct l; simpl in *; try reflexivity.
        destruct (R_dec a a0); congruence.
        specialize (IHl H0).
        rewrite IHl; clear IHl.
        destruct l; simpl in *; try reflexivity.
        revert H.
        destruct (R_dec a a0); intros; trivial.
        destruct (R_dec a0 a); congruence.
    Qed.

    Lemma is_list_sorted_insert_sorted `{Transitive A R} a l:
          is_list_sorted l = true -> is_list_sorted (insertion_sort_insert a l) = true.
Proof.
      revert a.
      induction l; intros.
      - reflexivity.
      - simpl.
        case_eq (R_dec a0 a); intros.
        + rewrite is_list_sorted_cons; split; assumption.
        + case_eq (R_dec a a0); intros; [|congruence].
          rewrite is_list_sorted_cons.
          split.
          * apply IHl; apply (is_list_sorted_cons_inv H0).
          * assert (Forall (fun x => R a x) (insertion_sort l))
              by (apply is_list_sorted_cons_Forall_lt; assumption).
            assert (is_list_sorted l = true) by
                apply (is_list_sorted_cons_inv H0); clear H0.
            specialize (IHl a H4); clear IHl.
            case_eq (insertion_sort_insert a0 l); intros; [trivial|].
            assert (a0 = a1 \/ In a1 l)
              by (apply (@in_insertion_sort_insert a1 l a0);
                  rewrite H0; left; reflexivity).
            rewrite Forall_forall in H3.
            elim H5; intros; [subst; assumption|]; clear H5.
            apply H3.
            rewrite insertion_sort_sorted_is_id; assumption.
    Qed.
    
    Theorem insertion_sort_sorted `{Transitive A R}:
      forall l, is_list_sorted (insertion_sort l) = true.
Proof.
      induction l; intros.
      - reflexivity.
      - simpl.
        apply is_list_sorted_insert_sorted.
        assumption.
    Qed.

    Lemma insertion_sort_idempotent l :
      insertion_sort (insertion_sort l) =
      insertion_sort l.
Proof.
      apply insertion_sort_sorted_is_id.
      apply is_list_sorted_Sorted_iff.
      apply insertion_sort_Sorted.
    Qed.

    Lemma insertion_sort_insert_not_nil a l :
      insertion_sort_insert a l <> nil.
Proof.
      induction l; simpl; intuition; try discriminate.
      destruct (R_dec a a0); simpl in *; try discriminate.
      destruct (R_dec a0 a); simpl in *; try discriminate.
    Qed.
    
    Lemma insertion_sort_nil l :
      insertion_sort l = nil -> l = nil.
Proof.
      induction l; simpl; intuition.
      apply insertion_sort_insert_not_nil in H; intuition.
    Qed.

    Lemma insertion_sort_insert_swap a a0 l `{StrictOrder A R}:
      R a a0 ->
      insertion_sort_insert a (insertion_sort_insert a0 l) =
      insertion_sort_insert a0 (insertion_sort_insert a l).
Proof.
      revert a a0.
      induction l; simpl; intros.
      - destruct (R_dec a a0); simpl; intuition.
        destruct (R_dec a0 a); simpl; intuition.
        rewrite r0 in r. eelim irreflexivity; eauto.
      - destruct (R_dec a1 a).
        + destruct (R_dec a0 a).
          * simpl.
            destruct (R_dec a0 a1); intuition.
            destruct (R_dec a1 a); intuition.
            destruct (R_dec a1 a0); intuition.
            rewrite r3 in H0; eelim irreflexivity; eauto.
          * rewrite r in H0; intuition.
        + destruct (R_dec a0 a); simpl.
          * destruct (R_dec a1 a); intuition.
            destruct (R_dec a0 a1); intuition.
            destruct (R_dec a1 a0).
            rewrite r1 in r0; eelim irreflexivity; eauto.
            destruct (R_dec a a1); simpl;
              destruct (R_dec a0 a); intuition.
          * destruct (R_dec a a1); destruct (R_dec a a0); simpl.
            destruct (R_dec a0 a).
            rewrite r1 in r0; eelim irreflexivity; eauto.
            destruct (R_dec a a0); intuition.
            destruct (R_dec a1 a).
            rewrite r2 in r; eelim irreflexivity; eauto.
            destruct (R_dec a a1); intuition.
            f_equal; eauto.
            destruct (R_dec a a0); intuition.
            destruct (R_dec a1 a).
            rewrite r0 in r; eelim irreflexivity; eauto.
            destruct (R_dec a0 a); intuition.
            destruct (R_dec a a1); intuition.
            rewrite H0 in r; intuition.
            destruct (R_dec a0 a); intuition.
            destruct (R_dec a a0); intuition.
            destruct (R_dec a1 a); intuition.
            destruct (R_dec a a1); intuition.
    Qed.

  End InsertionSort.

Properties of filter on sorted lists

  
  Section Filter.
    Lemma StronglySorted_filter {A} {R} f {l} :
      @StronglySorted A R l -> StronglySorted R (filter f l).
Proof.
      induction l; simpl; trivial.
      inversion 1; simpl; subst.
      destruct (f a); auto.
      constructor; auto.
      apply Forall_filter; trivial.
    Qed.
  End Filter.

Properties of In on sorted lists

  
  Section In.
    Local Hint Resolve asymmetric_over_cons_inv : qcert.
    
    Lemma insertion_sort_insert_in_strong {A R R_dec} {x l a}
          (contr:asymmetric_over R (a::l)) :
      a = x \/ In x l -> In x (@insertion_sort_insert A R R_dec a l).
Proof.
      revert x a contr. induction l; simpl; [intuition | ].
      intros x a0.
      case_eq (R_dec a0 a); simpl; intros; trivial.
      revert H0.
      case_eq (R_dec a a0); simpl; intros; intuition; subst; intuition.
      - right; apply (IHl x x); intuition.
        apply asymmetric_over_swap in contr. eauto with qcert.
      - right. apply (IHl x a0); intuition.
        apply asymmetric_over_swap in contr. eauto with qcert.
    Qed.

    Lemma insertion_sort_insert_in {A R R_dec} {x l a}
          (contr:forall x y, ~R x y -> ~R y x -> x = y) :
      a = x \/ In x l -> In x (@insertion_sort_insert A R R_dec a l).
Proof.
      apply insertion_sort_insert_in_strong.
      apply asymmetric_asymmetric_over; eauto.
    Qed.

    Lemma insertion_sort_in_strong {A R R_dec} {x l}
          (contr:asymmetric_over R l) :
      In x l -> In x (@insertion_sort A R R_dec l).
Proof.
      revert x.
      induction l; simpl; trivial; intros.
      specialize (IHl (asymmetric_over_cons_inv contr)).
      apply insertion_sort_insert_in_strong; trivial.
      - apply (asymmetric_over_incl contr). clear. simpl; intuition.
        apply in_insertion_sort in H0; eauto.
      - intuition.
    Qed.

    Local Hint Resolve asymmetric_asymmetric_over : qcert.

    Lemma insertion_sort_in {A R R_dec} {x l}
          (contr:forall x y, ~R x y -> ~R y x -> x = y) :
      In x l -> In x (@insertion_sort A R R_dec l).
Proof.
      apply insertion_sort_in_strong; intuition.
    Qed.

    Lemma equivlist_insertion_sort_strong {A R} R_dec {l l'}
          (contr:asymmetric_over R l) :
      equivlist l l' ->
      equivlist (@insertion_sort A R R_dec l) (@insertion_sort A R R_dec l').
Proof.
      cut (forall l l', (asymmetric_over R l) -> equivlist l l' ->
                        (forall x, In x (@insertion_sort A R R_dec l) -> In x (@insertion_sort A R R_dec l'))).
      - intros C eq x. split; intros inn.
        + specialize (C _ _ contr eq); intuition.
        + eapply C; try eapply inn.
          rewrite <- (asymmetric_over_equivlist eq); trivial.
          symmetry; trivial.
      - clear l l' contr. intros l l' asym incl x inn.
        apply in_insertion_sort in inn. apply incl in inn.
        apply insertion_sort_in_strong; trivial.
        eapply asymmetric_over_equivlist; eauto.
        symmetry. trivial.
    Qed.

    Lemma equivlist_insertion_sort {A R} R_dec {l l'}
          (contr:forall x y, ~R x y -> ~R y x -> x = y) :
      equivlist l l' ->
      equivlist (@insertion_sort A R R_dec l) (@insertion_sort A R R_dec l').
Proof.
      intros.
      eapply equivlist_insertion_sort_strong; trivial.
      apply asymmetric_asymmetric_over; trivial.
    Qed.

    Lemma insertion_sort_insert_insertion_nin {A:Type} lt dec
          `{StrictOrder A lt}
          (trich:forall a b, {lt a b} + {eq a b} + {lt b a})
          (a:A) a0 l :
      ~ lt a0 a ->
      ~ lt a a0 ->
      insertion_sort_insert dec a0
                            (insertion_sort_insert dec a l)
      = @insertion_sort_insert A lt dec a l.
Proof.
      revert a a0. induction l; simpl; intros.
      - repeat (match_destr; try congruence).
      - repeat (match_destr; try congruence);
          simpl; repeat (match_destr; try congruence); trivial.
        + rewrite l0 in l1. intuition.
        + rewrite IHl; trivial.
        + destruct (trich a a0) as [[?|?]|?];
            try congruence.
        + destruct (trich a a0) as [[?|?]|?];
            try congruence.
    Qed.

    Lemma insertion_sort_insert_cons_app {A:Type} lt dec
          `{StrictOrder A lt}
          (trich:forall a b, {lt a b} + {eq a b} + {lt b a}) a l l2 :
      insertion_sort dec (insertion_sort_insert dec a l ++ l2) = @insertion_sort A lt dec (a::l ++ l2).
Proof.
      revert a l2.
      induction l; simpl; trivial; intros.
      destruct (dec a0 a); simpl; trivial.
      destruct (dec a a0); simpl; trivial.
      - rewrite IHl; simpl. apply insertion_sort_insert_swap; eauto.
      - rewrite insertion_sort_insert_insertion_nin; eauto.
    Qed.

    Lemma insertion_sort_insertion_sort_app1 {A} lt dec `{StrictOrder A lt}
          (trich:forall a b, {lt a b} + {eq a b} + {lt b a}) l1 l2 :
      insertion_sort dec (insertion_sort dec l1 ++ l2) =
      @insertion_sort A lt dec (l1 ++ l2).
Proof.
      revert l2.
      induction l1; simpl; trivial; intros.
      rewrite insertion_sort_insert_cons_app; trivial.
      simpl.
      rewrite IHl1; trivial.
    Qed.

    
    Lemma insertion_sort_trich_equiv {A:Type} lt dec
          (trich:forall a b, {lt a b} + {eq a b} + {lt b a}) (l:list A)
      : equivlist (@insertion_sort A lt dec l) l.
Proof.
      intros; split; intros.
      - apply in_insertion_sort in H; trivial.
      - eapply insertion_sort_in in H; eauto.
        intros.
        destruct (trich x0 y) as [[?|?]|?]; intuition.
    Qed.

    Lemma insertion_sort_insert_forall_lt
          {A:Type} lt dec (a:A) (l:list A) :
      Forall (lt a) l ->
      @insertion_sort_insert A lt dec a l = a :: l.
Proof.
      destruct l; simpl; trivial.
      inversion 1; subst.
      match_destr; intuition.
    Qed.

    Lemma sort_insert_filter_true {A:Type} f lt dec `{StrictOrder A lt}
          (trich:forall a b, {lt a b} + {eq a b} + {lt b a})
          (a:A) (l:list A) :
      StronglySorted lt l ->
      f a = true ->
      filter f (@insertion_sort_insert A lt dec a l)
      = insertion_sort_insert dec a (filter f l).
Proof.
      revert a.
      induction l; simpl; intros b lsort fb.
      - rewrite fb; trivial.
      - inversion lsort; subst.
        case_eq (f a); simpl; intros fa.
        + destruct (dec b a); simpl.
           * rewrite fb.
             simpl. match_destr.
           * rewrite <- IHl; trivial.
             match_destr; simpl; rewrite fa; trivial.
        + match_destr.
          * simpl. rewrite fb, fa.
            rewrite insertion_sort_insert_forall_lt; trivial.
            apply Forall_filter.
            revert H3.
            apply Forall_impl_in; intros.
            etransitivity; eauto.
          * rewrite <- IHl; trivial.
            match_destr; simpl; rewrite fa; trivial.
            destruct (trich a b) as [[?|?]|?]; try congruence.
    Qed.
    
    Lemma sort_insert_filter_false {A:Type} f lt dec (a:A) (l:list A) :
      f a = false ->
      filter f (@insertion_sort_insert A lt dec a l) =
      filter f l.
Proof.
      revert a.
      induction l; simpl; intros ? fa.
      - rewrite fa; trivial.
      - match_destr; simpl.
        + rewrite fa; trivial.
        + match_destr; simpl.
          rewrite IHl; trivial.
    Qed.
    
    Lemma sort_filter_commute {A:Type} f lt dec
          `{StrictOrder A lt}
          (trich:forall a b, {lt a b} + {eq a b} + {lt b a})
          (l:list A) :
      filter f (@insertion_sort A lt dec l)
      = insertion_sort dec (filter f l).
Proof.
      induction l; simpl; trivial.
      case_eq (f a); intros fa; simpl.
      - rewrite <- IHl, sort_insert_filter_true; trivial.
        eapply Sorted_StronglySorted.
        + apply StrictOrder_Transitive.
        + eapply insertion_sort_Sorted.
      - rewrite <- IHl, sort_insert_filter_false; trivial.
    Qed.

  End In.

Properties of map on sorted lists

  
  Section Map.

    Lemma map_insertion_sort_insert {A B}
          {R1 R2}
          (R1_dec : forall a a' : A, {R1 a a'} + {~ R1 a a'})
          (R2_dec : forall b b' : B, {R2 b b'} + {~ R2 b b'})
          (f:A->B)
          (consistent:forall x y, R1 x y <->
                                  R2 (f x) (f y)) a l :
      map f (insertion_sort_insert R1_dec a l) =
      insertion_sort_insert R2_dec (f a) (map f l).
Proof.
      induction l; simpl; trivial.
      rewrite <- IHl.
      destruct (consistent a a0); destruct (consistent a0 a).
      repeat match_destr; simpl; try tauto.
    Qed.
    
    Lemma map_insertion_sort {A B}
          {R1 R2}
          (R1_dec : forall a a' : A, {R1 a a'} + {~ R1 a a'})
          (R2_dec : forall b b' : B, {R2 b b'} + {~ R2 b b'})
          (f:A->B)
          (consistent:forall x y, R1 x y <->
                                  R2 (f x) (f y)) l :
      map f (insertion_sort R1_dec l) =
      insertion_sort R2_dec (map f l).
Proof.
      induction l; simpl; trivial.
      rewrite <- IHl.
      erewrite map_insertion_sort_insert; eauto.
    Qed.

  End Map.

  Lemma insertion_sort_insert_nin_eq_inv {A R} dec (a:A) ll₂ :
    insertion_sort_insert (R:=R) dec a l₁ = insertion_sort_insert dec a l₂ ->
    ~ In a l₁ ->
    ~ In a l₂ ->
    l₁ = l₂.
Proof.
    revert l₂.
    induction l₁; destruct l₂; simpl; intros eqq; trivial.
    - intuition.
      destruct (dec a a0); simpl in *.
      + invcs eqq.
      + destruct (dec a0 a); invcs eqq; tauto.
    - intuition.
      destruct (dec a a0); simpl in *.
      + invcs eqq.
      + destruct (dec a0 a); invcs eqq; tauto.
    - intuition.
      destruct (dec a a0); simpl in *.
      + invcs eqq.
        destruct (dec a a1); simpl.
        * invcs H4; trivial.
        * destruct (dec a1 a); invcs H4; tauto.
      + destruct (dec a0 a).
        * destruct (dec a a1); invcs eqq; try tauto.
          destruct (dec a1 a); invcs H4; try tauto.
          f_equal; eauto.
        * { destruct (dec a a1).
            - invcs eqq; tauto.
            - destruct (dec a1 a); invcs eqq; try tauto.
          }
  Qed.

End SortingAdd.