Origami Programming in Coq

origami.v

(* Working Through Jeremy Gibbons' article Origami Programming in Coq *)
Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Program.Basics.
Open Scope program_scope.       (* for ∘ composition operator *)

Inductive list (X:Type) : Type :=
  | nil : list X
  | cons : X -> list X -> list X.

Definition is_nil (X:Type) (l:list X) : bool :=
  match l with
    | nil => true
    | cons x xs => false
  end.

Implicit Arguments nil [[X]].
Implicit Arguments cons [[X]].

Definition wrap (X:Type) (x:X) : list X := cons x nil.
Implicit Arguments wrap [[X]].

Fixpoint foldL (A B: Type) (f:A -> B -> B) (e:B) (l:list A) : B :=
  match l with
    | nil => e
    | cons x xs => f x (foldL A B f e xs)
  end.
Implicit Arguments foldL [[A] [B]].

Theorem fold_universal:
  forall (A B : Type) (h: list A -> B) (f:A -> B -> B) (e:B),
    (h = foldL f e) <-> 
    (h nil = e) /\ (forall (x:A) (xs:list A),(h (cons x xs) = f x (h xs))).
Proof.
  intros A B h f e. split.
  (* -> *)
  intros H. split.
    (* h nil = e *)
    subst h. reflexivity.
    (* h (cons x xs) = f x (h xs) *)
    subst h. reflexivity.
  (* <- *)
    intros H. inversion H. apply functional_extensionality.
    intros l. induction l as [| lh lt].
    (* l = nil *)
    simpl. apply H0.
    (* l = cons lh lt *)
    simpl. rewrite -> H1. rewrite -> IHlt. reflexivity. 
Qed.

(* Exercise 3.1 *)
Theorem fold_fusion:
  forall (A B C:Type) (h:B -> C) (f:A -> B -> B) (e:B) (f':A -> C -> C) (e' : C),
    (forall (a:A) (b:B), h (f a b) = f' a (h b)) /\ (h e = e') ->
      h ∘ (foldL f e) = foldL f' e'.
Proof.
  intros A B C h f e f' e' H. inversion H.
  apply fold_universal. split.
  (* (h ∘ foldL A B f e) nil = e' *)
  unfold compose. simpl. apply H1.
  (* (h ∘ foldL A B f e) (cons x xs) = f' x ((h ∘ foldL A B f e) xs) *)
  unfold compose. simpl. intros x xs. apply H0.
Qed.
(* TODO: The law does not hold for strict h, because *)

(* Exercise 3.2 *)
Definition mapL (A B: Type) (f:A->B) (l:list A) : list B :=
  foldL (fun a b => cons (f a) b) nil l.
Implicit Arguments mapL [[A] [B]].

Definition appendL (A : Type) (l1:list A) (l2:list A) : list A :=
  foldL (fun a b => cons a b) l2 l1.
Implicit Arguments appendL [[A]].

Definition concatL (A : Type) (l:list (list A)) : list A :=
  foldL (fun a b => appendL a b) nil l.
Implicit Arguments concatL [[A]].

(* Exercise 3.3 *)
Corollary map_fusion:
  forall (A B C: Type) (f:A -> B -> B) (e:B) (g:C->A),
    foldL f e ∘ mapL g = foldL (f ∘ g) e.
Proof.
  intros A B C f e g.
  apply fold_fusion. split.
  (* foldL f e (cons (g a) b) = (f ∘ g) a (foldL f e b) *)
  simpl. unfold compose. reflexivity.
  (* foldL f e nil = e *)
  reflexivity.
Qed.

(* I should make this use an ordering property; one that actually
requires a proof of ordering *)
(* also ask about coq equivalents to haskell's (++) or `foo` *)
Fixpoint insert (A:Type) (le: A -> A -> bool) (y : A) (l : list A) : list A :=
  match l with
    | nil => wrap y
    | cons x xs => if le y x
                   then cons y l
                   else cons x (insert A le y xs)
  end.
Implicit Arguments insert [[A]].

Definition isort (A:Type) (le: A -> A -> bool) (l : list A) : list A :=
  foldL (insert le) nil l.
Implicit Arguments isort [[A]].

(* Exercise 3.4 *)
Definition insert1 (A:Type) (le: A -> A -> bool) (y : A) (l : list A) : (list A * list A) :=
  foldL (fun a b => match b with
                      | (c,d) => if le y a
                                 then (cons a c, cons y (cons a c))
                                 else (cons a c, cons a d)
                    end)
        (nil,wrap y)
        l.
Implicit Arguments insert1 [[A]].

Theorem insert1_insert_related:
  forall (A:Type) (le: A -> A -> bool) (y : A) (xs : list A),
    insert1 le y xs = (xs, insert le y xs).
Proof.
  intros A le y xs. induction xs as [|h t].
  (* xs = nil *)
  unfold insert1. simpl. reflexivity.
  (* xs = cons h t *)
  unfold insert1. simpl. unfold insert1 in IHt. destruct (le y h).
    (* le y h = true *)
    rewrite IHt. reflexivity.
    (* le y h = false *)
    rewrite IHt. reflexivity.
Qed.


Fixpoint paraL (A B: Type) (f:A -> list A * B -> B) (e:B) (l:list A) : B :=
  match l with
    | nil => e
    | cons x xs => f x (xs, paraL A B f e xs)
  end.
Implicit Arguments paraL [[A] [B]].

Definition insert2 (A:Type) (le: A -> A -> bool) (y : A) (l : list A) : list A :=
  paraL (fun a b => match b with
                      | (c,d) => if le y a
                                 then cons y (cons a c)
                                 else cons a d
                    end)
        (wrap y)
        l.
Implicit Arguments insert2 [[A]].

Theorem insert_insert2_equivalent:
  forall (A:Type) (le: A -> A -> bool) (y : A) (l : list A),
    insert le y l = insert2 le y l.
Proof.
  intros A le y l. induction l as [|h t].
  (* l = nil *)
  reflexivity.
  (* l = cons h t *)
  unfold insert2. simpl.
  destruct (le y h).
    (* le y h = true *)
    reflexivity.
    (* le y h = false *)
    unfold insert2 in IHt. rewrite IHt. reflexivity.
Qed.