## Thursday, 19 June 2008

### 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 *)`