Last active
December 25, 2015 15:29
-
-
Save ijp/6998547 to your computer and use it in GitHub Desktop.
Origami Programming in Coq
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* 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. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment