Proving RLE encoding and decoding in Coq

Require Import List.
Require Import ListPlus.

Set Implicit Arguments.

Notation "y <- x" := (x -> y) (at level 94, left associativity, only parsing).

Definition compose A B C (f : C <- B) (g : B <- A) := fun x => f (g x).
Infix "∘" := compose (at level 30, right associativity).

(*
 * rle = map (length &&& head) ∘ group
 * unrle = concat ∘ map (uncurry replicate)
 *
 * is it always true that (unrle ∘ rle) x = x?
 *
 * notice:
 *  rle = f ∘ f'
 *  unrle = g' ∘ g
 *
 *)

Theorem sandwich : forall I M O
  (f : O <- M) (f' : M <- I)
  (g : O -> M) (g' : M -> I),
  (forall x, (f  ∘ g ) x = x) ->
  (forall x, (f' ∘ g') x = x) ->
  (forall x, (f ∘ f' ∘ g' ∘ g) x = x).
Proof.
  unfold compose; intros.
  rewrite (H0 (g x)).
  apply H.
Qed.

(*
 * so all that must be proved now is
 *    forall x, (concat ∘ group) x = x
 * /\ forall x, (map (uncurry replicate) ∘ map (length &&& head))
 *
 *)

Theorem map_fuse : forall A B C (f : C <- B) (g : B <- A),
  forall x, (map f ∘ map g) x = map (f ∘ g) x.
Proof.
  induction x.
  reflexivity.
  simpl; rewrite <- IHx.
  reflexivity.
Qed.

(*
 * Now we have "only" to prove
 *    forall x, (concat ∘ group) x = x
 * /\ forall x, (uncurry replicate ∘ (length &&& head)) x = x
 *
 * This is actually impossible though,
 * (uncurry replicate ∘ (length &&& head)) "foo" = "fff"
 *
 * The reason rle works is because group segments the list
 * into *homogenous* chunks, if we knew the input to (length && head)
 * was a homogenous list then it would be correct and provable.
 * It needs access to this precondition though
 *
 *)

Theorem sandwich' : forall I M O
  (P : M -> Prop)
  (f : O <- M) (f' : M <- I)
  (g : O -> M) (g' : M -> I),
  (forall x, (f  ∘ g ) x = x) ->
  (forall x, P x -> (f' ∘ g') x = x) ->
  (forall x, P (g x)) ->
  (forall x, (f ∘ f' ∘ g' ∘ g) x = x).
Proof.
  unfold compose; intros.
  rewrite (H0 (g x)).
  apply H.
  apply H1.
Qed.

Inductive Homogenous A : listP A -> Prop :=
| HEnd : forall u, Homogenous (nilP u)
| HOne : forall u, Homogenous (u:~:nilP u)
| HAdd : forall u us, Homogenous (u:~:us) -> Homogenous (u:~:u:~:us).
Hint Constructors Homogenous.

Inductive All X (P : X -> Prop) : list X -> Prop :=
| AllNil : All P nil
| AllCons : forall x xs, P x -> All P xs -> All P (x::xs).
Hint Constructors All.

Section RLE.
  
  Variable A : Type.
  Variable eq_dec : forall x y : A, { x = y } + { x <> y }.
  
  Definition head_consP X (e : X) (l : list (listP X)) :=
    match l with
      | nil => nil
      | x::xs => (e:~:x)::xs
    end.

  Fixpoint group (l : list A) : list (listP A) :=
    match l with
      | nil => nil
      | x::xs =>
        match xs with
          | nil => nilP x::nil
          | y::ys =>
            match eq_dec x y with
              | left equal => head_consP x (group xs)
              | right not_equal => nilP x::group xs
            end
        end
    end.
  Fixpoint concat (l : list (listP A)) : list A :=
    match l with
      | nil => nil
      | x::xs => appP' x (concat xs)
    end.
  
  Definition crush (l : listP A) : (nat * A) := (lengthP l, headP l).
  Definition expand (t : nat * A) : listP A := let (n,e) := t in replicateP n e.
  
  Definition rle := map crush ∘ group.
  Definition unrle := concat ∘ map expand.
  
  Functional Scheme group_ind := Induction for group Sort Prop.
  Lemma concat_group_inv : forall x, (concat ∘ group) x = x.
    unfold compose.
    intro x; functional induction (group x).
    
    reflexivity.
    
    reflexivity.
    
    Lemma cat_cons : forall u v vs, concat (head_consP u (v::vs)) = u :: concat (v::vs).
      destruct vs; reflexivity.
    Qed.
    
    destruct (group (y :: _x)).
    inversion IHl.
    rewrite cat_cons.
    rewrite IHl.
    reflexivity.
    
    simpl in *.
    rewrite IHl.
    reflexivity.
  Qed.
  
  Lemma expand_crush_inv : forall x, Homogenous x -> (expand ∘ crush) x = x.
    unfold compose.
    induction x.
    reflexivity.
    intro; inversion H.
    rewrite <- H2 in IHx.
    reflexivity.
    simpl in *.
    rewrite <- H2 in *.
    rewrite <- IHx.
    reflexivity.
    assumption.
  Qed.
  
  (*
   * some notes I had to write to crack this lemma,
   *
   * group [] = []
   * group [x] = [[x]]
   * group (x:y:ys) = if x == y then headCons x (group (y:ys))
   *                           else [x] : group (y:ys)
   *   where headCons x (y:ys) = (x:y):ys
   *
   * Theorem: forall xs, All Homogenous (group xs)
   * 
   * group [] ~ trivial
   * group [x] ~ trivial
   * group (x:y:ys) = [x] : group (y:ys)
   *            homo   ^          ^ homo by induction
   * 
   * group (x:x:ys) = headCons x (group (x:xs))
   * 
   * (group (x:xs)) = ((x:p):q)
   *          homogenous ^  ^ all homogenous by induction
   *
   * group (x:x:ys) = headCons x ((x:p):q)
   *                = ((x:x:p):q)
   *            homo cons ^
   *)
  
  Lemma group_homo : forall x, All (@Homogenous A) (group x).
    induction x.
    simpl; auto.
    destruct x.
    simpl; auto.
    
    simpl.
    destruct (eq_dec a a0).
    
    rewrite <- e in *.
    
    Lemma paper_plane : forall xs x,
      exists p, exists q,
        group (x::xs) = ((x:~:p)::q) \/ group (x::xs) = ((nilP x)::q).
      induction xs.
      simpl.
      intro x; exists (nilP x); exists nil; auto.
      intro x.
      simpl.
      destruct (eq_dec x a).
      rewrite <- e in *; clear e a.
      
      destruct (IHxs x).
      destruct H.
      destruct H.
      simpl in H.
      rewrite H.
      simpl.
      exists (x :~: x0).
      exists x1.
      left; reflexivity.
      simpl in H.
      rewrite H.
      simpl.
      exists (nilP x).
      exists x1.
      left; reflexivity.
      
      destruct (IHxs a).
      destruct H.
      destruct H.
      simpl in H.
      destruct xs.
      exists (nilP a).
      exists (nilP a :: nil).
      right; reflexivity.
      rewrite H.
      exists (nilP a).
      exists ((a :~: x0) :: x1).
      right; reflexivity.
      simpl in H.
      rewrite H.
      exists (nilP a).
      exists (nilP a :: x1).
      right; reflexivity.
    Qed.
    
    pose (paper_plane x a).
    inversion e0.
    inversion H.
    inversion H0.
    
    rewrite H1 in IHx.
    simpl in H1.
    rewrite H1.
    simpl.
    apply AllCons.
    apply HAdd.
    inversion IHx; auto.
    inversion IHx; auto.
    
    rewrite H1 in IHx.
    simpl in H1.
    rewrite H1.
    simpl.
    apply AllCons.
    apply HOne.
    inversion IHx.
    assumption.
    
    apply AllCons.
    auto.
    apply IHx.
  Qed.
  
  Theorem rle_inv : forall x, unrle (rle x) = x.
    intro; unfold unrle, rle.
    apply sandwich' with (P := All (@Homogenous A)).
    
    exact concat_group_inv.
    
    clear x; intros; rewrite map_fuse; induction x.
    reflexivity.
    simpl.
    inversion H.
    rewrite (IHx H3).
    rewrite (expand_crush_inv H2).
    reflexivity.
  
    exact group_homo.
  Qed.
    
End RLE.

Require Import Arith.

Eval compute in (rle eq_nat_dec (1::2::3::3::3::5::5::5::1::1::1::6::6::6::6::6::nil)).
(*
 *   = (0, 1) :: (0, 2) :: (2, 3) :: (2, 5) :: (2, 1) :: (4, 6) :: nil
 *   : list (nat * nat)
 *)

Eval compute in (unrle (rle eq_nat_dec (1::2::3::3::3::5::5::5::1::1::1::6::6::6::6::6::nil))).
(*   = 1::2::3::3 ::3 ::5 ::5 ::5::1::1::1::6::6::6::6::6::nil
 *   : list nat
 *)