chunk n list = case list of { [] -> [] ; (y:ys) -> ch' ys (n-1) (y:) } where

ch' [] _ k = k [] : []

ch' (y:ys) 0 k = k [] : ch' ys (n-1) (y:)

ch' (y:ys) (c+1) k = ch' ys c (k . (y:))

## Tuesday 27 May 2008

### A Haskell Puzzle

### Easy Examples of Pattern Matching in Coq

(*

* A couple of difficulties in Coq or dependently typed programming

* are having to write impossible cases in pattern matches and

* getting at the new information provided by a pattern match.

*)

(* I'll use vectors (lists which have their length as part of the

* type) to explain this since they are very simple objects

*)

Inductive Vec (A : Set) : nat -> Set :=

| VNil : Vec A 0

| VCons : forall n, A -> Vec A n -> Vec A (S n).

(* It's pretty easy to define a total function taking the head

* of any vector using tactics:

*

Definition head (A : Set)(n : nat) :

Vec A (S n) -> A.

intros.

inversion H.

exact H1.

Defined.

* but actually this results in something terrifying:

Print head.

head =

fun (A : Set) (n : nat) (H : Vec A (S n)) =>

let H0 :=

match H in (Vec _ n0) return (n0 = S n -> A) with

| VNil =>

fun H0 : 0 = S n =>

let H1 :=

eq_ind 0 (fun e : nat => match e with

| 0 => True

| S _ => False

end) I (S n) H0 in

False_rec A H1

| VCons n0 H0 H1 =>

fun H2 : S n0 = S n =>

let H3 :=

let H3 :=

f_equal (fun e : nat => match e with

| 0 => n0

| S n1 => n1

end) H2 in

eq_rect n (fun n1 : nat => A -> Vec A n1 -> A)

(fun (H4 : A) (_ : Vec A n) => H4) n0 (sym_eq H3) in

H3 H0 H1

end in

H0 (refl_equal (S n))

: forall (A : Set) (n : nat), Vec A (S n) -> A

*

* It would be much shorter to simple define it by pattern matching

* but there is a problem,

*)

(*

Definition head (A : Set)(n : nat) :

Vec A (S n) -> A :=

fun v =>

match v with

| VCons n a _ => a

end.

*

* it seems ok but what we know (that a vector of length one or more

* cannot ever be VNil) hasn't been made clear to Coq:

*

Error: Non exhaustive pattern-matching:

no clause found for pattern VNil

*)

(* To define head by pattern matching we must cover all cases

* but there is certainly not object of type A to return given

* a VNil object of type Vec A (S _), of course this is absurd.

* So I'll use the solution given here:

* http://pauillac.inria.fr/pipermail/coq-club/2008/003508.html

*)

Definition head (A : Set)(n : nat) :

Vec A (S n) -> A :=

fun v =>

match v in Vec _ m return

match m with

| 0 => True

| _ => A

end

with

| VNil => I

| VCons n a _ => a

end.

(* This is perfect, the trick is very clever!

* the key is that [match m with | 0 => True | _ => A end] is

* convertable to A since m = (S n).

* then VNil is given a trivial case which must be of type True

* (chosen arbitrarily) and VCons gives the actual definition

* we wished for.

*)

(* this is a big hassle, let's avoid going through it again .. *)

Definition tail (A : Set)(n : nat) :

Vec A (S n) -> Vec A n.

intros; inversion H; trivial.

Defined.

(*

Theorem worm (A : Set)(n : nat) :

forall (v : Vec A (S n)),

v = VCons _ _ (head _ _ v) (tail _ _ v).

Proof.

intros.

inversion v.

*)

(*

A : Set

n : nat

v : Vec A (S n)

n0 : nat

H0 : A

H1 : Vec A n

H : n0 = n

============================

v = VCons A n (head A n v) (tail A n v)

*)

(* so now I tried to prove a theorem relating these functions,

* but of course hit a brick wall, there's just not enough information

* relating the terms to prove it

*)

(* before (when defining head), we met trouble due to not giving a

* total coverage of the type, (that is we ignored Vec A 0) so a

* possible lemma to consider would be an identity on all Vectors

* which takes VNil to VNil and VCons _ _ to VCons (head v) (tail v)

* Actually I had some trouble even writing this, so I let Coq do it

* for me

*)

(*

Definition Vid (A : Set)(n : nat) :

Vec A n -> Vec A n.

destruct n.

tauto.

intro v.

exact (VCons _ _ (head _ _ v) (tail _ _ v)).

Qed.

Print Vid.

*

Vid =

fun (A : Set) (n : nat) =>

match n as n0 return (Vec A n0 -> Vec A n0) with

| 0 => fun H : Vec A 0 => H

| S n0 => fun v : Vec A (S n0) => VCons A n0 (head A n0 v) (tail A n0 v)

end

: forall (A : Set) (n : nat), Vec A n -> Vec A n

* but actually I'd like to have the proof term here in a simpler

* form if possible, so I rewrote it in the way it way synthesized:

*)

Definition Vid (A : Set)(n : nat) :

Vec A n -> Vec A n :=

match n return Vec A n -> Vec A n with

| 0 => fun v => v

| S m => fun v => VCons _ _ (head _ _ v) (tail _ _ v)

end.

Lemma Vid_is_id (A : Set)(n : nat) :

forall v : Vec A n,

v = Vid _ _ v.

Proof.

destruct v; reflexivity.

Qed.

Theorem worm (A : Set)(n : nat) :

forall (v : Vec A (S n)),

v = VCons _ _ (head _ _ v) (tail _ _ v).

Proof.

intros; apply Vid_is_id with (v := v).

Qed.

(* What next? *)

## Monday 5 May 2008

### Prolog CHR - Prime Seive One Liner

%% http://www.cs.kuleuven.be/~dtai/projects/CHR/

:- use_module(library(chr)).

:- chr_constraint prime/1.

prime(X) \ prime(Y) <=> 0 is Y mod X | true.

%% This simpagation rules states:

%% given there are clauses prime(X) and prime(Y)

%% such that 0 is Y mod X, remove the clause prime(Y).

%% To try it out:

primes(1). primes(N) :- prime(N), succ(M,N), primes(M).

%% ?- primes(50) % generate all candidates <= 50

%% % the CHR rule seives out those which are not prime

Subscribe to:
Posts (Atom)