dependent_sort.v

(* Free category on a quiver *)
Inductive Free {ob} (Q : ob -> ob -> Type) : ob -> ob -> Type :=
  | Id : forall {X}, Free Q X X
  | Circ : forall {X Y Z}, Q Y Z -> Free Q X Y -> Free Q X Z.
Arguments Id {_ _ _}.
Arguments Circ {_ _ _ _ _}.

Fixpoint append {ob} {Q : ob -> ob -> Type} {X Y Z} (xs : Free Q Y Z) (ys : Free Q X Y)
  : Free Q X Z
  := match xs, ys with
     | Id, ys => ys
     | Circ x xs, ys => Circ x (append xs ys)
     end.

Theorem append_assoc {ob} {Q : ob -> ob -> Type} {X Y Z W} (xs : Free Q Z W) (ys : Free Q Y Z) (zs : Free Q X Y)
  : append xs (append ys zs) = append (append xs ys) zs.
Proof.
  induction xs as [ | ? ? ? x xs IH]; simpl; auto.
  now rewrite IH.
Qed. 

Section InsertionSort.

Variable ob : Type.
Variable Q : ob -> ob -> Type.

Inductive SwapResult : ob -> ob -> Type :=
  | NoSwap : forall {X Y}, SwapResult X Y
  | Swap : forall {X Y Z}, Free Q Y Z -> Q X Y -> SwapResult X Z
  | Erase : forall {X}, SwapResult X X.
  
Variable swap : forall {X Y Z}, Q Y Z -> Q X Y -> SwapResult X Z.

Fixpoint sortedAfter {X Y Z} (x : Q Y Z) (ys : Free Q X Y) : Prop
  := match ys, x with
     | Id, _ => True
     | Circ y ys, x => swap x y = NoSwap /\ sortedAfter y ys
     end.

Definition sorted {X Y} (xs : Free Q X Y) : Prop
  := match xs with
     | Id => True
     | Circ x xs => sortedAfter x xs
     end.

Hypothesis swap_swap_sorted
  : forall {X Y Y' Z} (x : Q Y Z) (y : Q X Y) (ys : Free Q Y' Z) (x' : Q X Y'),
  swap x y = Swap ys x' -> sorted (append ys (Circ x' Id))
  /\ forall {W} (z : Q Z W), swap z x = NoSwap -> sortedAfter z (append ys (Circ x' Id)).

(* this is not actually satisfied for Delta ??? *)
Hypothesis swap_erase_sorted
  : forall {X Y Z W} (x : Q Y W) (y : Q Z Y) (z : Q Y Z) (w : Q X Y),
  swap y z = Erase -> swap x y = NoSwap -> swap z w = NoSwap -> swap x w = NoSwap.

Fixpoint insert {X Y Z} (y : Q Y Z) (xs : Free Q X Y) : Free Q X Z
  := match xs, y with
     | Id, y => Circ y Id
     | Circ x xs, y => match swap y x with
                       | NoSwap => fun y x xs => Circ y (Circ x xs)
                       | Swap zs z => fun _ _ xs => append zs (insert z xs)
                       | Erase => fun _ _ xs => xs
                       end y x xs
   end.

Fixpoint sort {X Y} (xs : Free Q X Y) : Free Q X Y
  := match xs with
     | Id => Id
     | Circ x xs => insert x (sort xs)
     end.

Theorem sorted_after_sorted {X Y Z} (x : Q Y Z) (ys : Free Q X Y) 
  : sortedAfter x ys -> sorted ys.
Proof.
  destruct ys; simpl; auto. now intros [].
Qed.

Theorem sorted_append {X Y Z W} (xs : Free Q Z W) (y : Q Y Z) (ys : Free Q X Y)
  : sorted (append xs (Circ y Id)) -> sortedAfter y ys -> sorted (append xs (Circ y ys)).
Proof.
  destruct xs as [ | ? ? ? x xs]; simpl; auto.
  revert Y Z x y ys.
  induction xs as [ | ? ? ? x' xs IH]; simpl.
  - intros ? ? ? ? ? []. auto.
  - intros ? ? ? ? ? [] ?. auto.
Qed.

Theorem insert_sorted_after {X Y Z W} (zs : Free Q Z W) (y : Q Y Z) (xs : Free Q X Y)
  : sorted (append zs (Circ y Id)) -> sorted xs -> sorted (append zs (insert y xs)).
Proof.
  revert Z zs y.
  induction xs as [ | ? ? Z' x xs]; simpl; auto.
  intros Z zs y.
  destruct swap as [ | ? ? ? ws w | ] eqn:e.
  - intros ? ?. apply sorted_append; simpl; auto.
  - intros r ?.
    rewrite append_assoc.
    apply IHxs.
    + apply swap_swap_sorted in e.
      destruct e as [p q].
      destruct zs as [ | ? ? ? z zs]; simpl in *; auto.
      clear IHxs. revert Z z r.
      induction zs as [ | ? ? Z'' z' zs IHzs]; simpl.
      * intros ? ? []. auto.
      * intros Z z []. split; auto.
        eapply IHzs; eauto.
    + eapply sorted_after_sorted; eauto.
  - (* this argument could use a stengthened induction predicate? *)
    destruct zs as [ | ? ? ? z zs]; simpl.
    + intros ?. apply sorted_after_sorted.
    + clear IHxs. revert Z z.
      induction zs as [ | ? ? ? z' zs IHzs]; simpl.
      * intros Z z [q].
        destruct xs as [ | ? ? ? x' xs]; simpl; auto.
        intros [p]. split; auto.
        (* used here: *)
        apply (swap_erase_sorted z y x x' e q p).
      * intros ? ? [] ?. split; auto.
        eapply IHzs; eauto.
Qed.

Theorem sort_sorted {X Y} (xs : Free Q X Y) : sorted (sort xs).
Proof.
  induction xs as [ | ? ? ? x xs IH]; simpl; auto.
  apply (insert_sorted_after Id); simpl; auto.
Qed.

Section Consistency.

Variable Hom : ob -> ob -> Type.
Variable id : forall {X}, Hom X X.
Variable circ : forall {X Y Z}, Hom Y Z -> Hom X Y -> Hom X Z.
Variable id_L : forall {X Y} (f : Hom X Y), circ id f = f.
Variable id_R : forall {X Y} (f : Hom X Y), circ f id = f.
Variable circ_assoc : forall {X Y Z W} (f : Hom Z W) (g : Hom Y Z) (h : Hom X Y),
  circ f (circ g h) = circ (circ f g) h.
Variable embed : forall {X Y}, Q X Y -> Hom X Y.

Fixpoint interpret {X Y} (p : Free Q X Y) : Hom X Y
  := match p with
     | Id => id
     | Circ s f => circ (embed s) (interpret f)
     end.

Theorem interpret_append {X Y Z} (xs : Free Q Y Z) (ys : Free Q X Y)
  : interpret (append xs ys) = circ (interpret xs) (interpret ys).
Proof.
  induction xs as [ | ? ? ? x xs IH]; simpl.
  - symmetry. apply id_L.
  - simpl. rewrite IH. apply circ_assoc.
Qed.

Hypothesis swap_swap_consistent
  : forall {X Y Y' Z} (x : Q Y Z) (y : Q X Y) (ys : Free Q Y' Z) (x' : Q X Y'),
  swap x y = Swap ys x' -> circ (embed x) (embed y) = circ (interpret ys) (embed x').

Hypothesis swap_erase_consistent
  : forall {X Y} (x : Q Y X) (y : Q X Y),
  swap x y = Erase -> circ (embed x) (embed y) = id.

Theorem insert_consistent {X Y Z} (y : Q Y Z) (xs : Free Q X Y)
  : interpret (insert y xs) = circ (embed y) (interpret xs).
Proof.
  revert Z y.
  induction xs as [ | ? ? Z' x xs IH]; simpl; auto.
  intros Z y.
  destruct swap as [ | ? ? ? zs z | ] eqn:e; simpl; auto.
  - apply swap_swap_consistent in e.
    rewrite interpret_append.
    rewrite IH.
    rewrite circ_assoc, circ_assoc.
    rewrite e. auto.
  - apply swap_erase_consistent in e.
    rewrite circ_assoc.
    rewrite e.
    rewrite id_L. auto.
Qed.

Theorem sort_consistent {X Y} (xs : Free Q X Y)
  : interpret (sort xs) = interpret xs.
Proof.
  induction xs as [ | ? ? ? x xs IH]; simpl; auto.
  rewrite insert_consistent.
  rewrite IH. auto.
Qed.

End Consistency.

End InsertionSort.