## Tuesday, 27 May 2008

`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:))`
`(* * 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 inH0 (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? *)`
`%% 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`