The Coq mailing list

[Paul Tarau <paul.tarau AT gmail.com>]

(*
Many thanks to Guillaume, Cedric and Andreas for their help on my
previous postings.

I have succeeded building a bijection between natural
numbers and binary trees. It allows "borrowing" arbitrary
arithmetic operations from "nat" to the domain of
binary trees "T" (see borrowedS and borrowedP).

However, when trying to define sucessor and predecessor operations
directly on the tree domain "T", the execution in
Coq diverges unexpectedly from my expectations.

Note that the code uses artificial "nat" bounds providing
a structurally decreasing argument and I am planning
to show the equivalence with the operations borrowed
from "nat" using the bijection with T.

But I wanted first to see if the code makes sense empirically and
as I seldomly suspect the system itself for unexpected behavior,
I wrote an equivalent Haskell program (attached)
- which works as expected - even for large values of the
"lim" parameter controlling the tests.

So I am wondering if it is something wrong with my Coq program, or
if this is a genuine bug (or an "infelicity":-)) in Coq's "Eval compute".

Here are the symptoms:

Eval compute in "stest" gives:

 = 1 :: 2 :: 3 :: 2 :: 5 :: 12 :: 7 :: 2 :: 9 :: 40 :: 11 :: nil
     : list nat

Eval compute in "pstest" gives:
= 0 :: 1 :: 2 :: 1 :: 4 :: 11 :: 6 :: 1 :: 8 :: 39 :: 10 :: nil
     : list nat

in contrast with the equivalent Haskell program and my expectations:

*CS> stest
[1,2,3,4,5,6,7,8,9,10,11]
*CS> pstest
[0,1,2,3,4,5,6,7,8,9,10]

Note that I placed exceptions in the
Haskell program to catch possible
incorrectness of the artificial nat bounds.
*)

Inductive T : Set :=
| E : T
| C : T -> T -> T.

Delimit Scope T_scope with T.
Bind Scope T_scope with T.
Arguments Scope T [T_scope].

Definition hdT (a:T) : T :=
match a with
| E => E
| C _ y =>y
end.

Definition tlT (a:T) : T :=
match a with
| E => E
| C _ y =>y
end.

(* returns 2x+y *)
Fixpoint twicePlus (x y:nat) :=
match x with
| O => y
| S n => S (S (twicePlus n y))
end.

(* returns 2^x*y *)
Fixpoint exp2times (x y:nat) :=
match x with
| O => y
| S n => twicePlus (exp2times n y) O
end.

(* returns 2^x*(2*y+1) *)
Definition cN (x y:nat) := exp2times x (twicePlus y (S O)).

(* a bijection hdT T tlT nat *)
Fixpoint t2n (t : T) : nat :=
match t with
| E => 0
| C x y => cN (t2n x) (t2n y)
end.

Fixpoint hh (n a b acc:nat) :=
match n,a,b with
| O,   _, _ => acc (* pro forma: should never happen *)
| S _, O,O => acc
| S k, O,a => hh k a O (S acc)
| S _, S O,_ => acc
| S k, S (S n),y => hh k n (S y) acc
end.

(* we know total steps are never more than 2*n *)
Definition hdN (a:nat) := hh (twicePlus a O) a O O.

Fixpoint tt (n a b:nat) :=
match n,a,b with
| O,   _, b => O (* pro forma: should never happen *)
| S _, O,O => O
| S k, O,a => tt k a O
| S _, S O,b => b
| S k, S (S n),y => tt k n (S y)
end.

(* we know total steps are never more than 2*n *)
Definition tlN (a:nat) := tt (twicePlus a O) a O.

Fixpoint kn2t (k n :nat ) : T :=
match k,n with
| O,_ => E (* pro forma *)
| S a,O => E
| S a,x => C (kn2t a (hdN n)) (kn2t a (tlN n))
end.

Definition n2t (n : nat) : T := kn2t n n.

Definition borrowedS (x:T) : T := n2t (S (t2n x)).
Definition borrowedP (x:T) : T := n2t (pred (t2n x)).

Fixpoint s (n : nat) (a:T) :=
match n,a with
| O,_ => E (* pro forma *)
| S _,E => C E E
| S k,C E y => C (s k (hdT (s k y))) (tlT (s k y))
| S k,C x y => C E (C (p k x) y)
end
with p (n : nat) (a:T) : T :=
match n,a with
| O,_ => E (* pro forma *)
| S _,E => E (* pro forma *)
| S _,C E E => E
| S k,C E (C x y) => C (s k x) y
| S k,C x y => C E (p k (C (p k x) y))
end.

Definition sT (a:T) := s (S (t2n a)) a.
Definition pT (a:T) := p (S (t2n a)) a.

Require Import List.

Fixpoint numlist1 (n:nat) (ns:list nat) :=
match n with
| O => ns
| S n => numlist1 n (n::ns)
end.

Definition numlist (n:nat) := numlist1 (S n) nil.

Definition lim := 10.

Definition test :=  map t2n (map n2t (numlist lim)).
Definition btest := map t2n (map borrowedP (map borrowedS (map n2t
(numlist lim)))).

Definition stest :=  map t2n (map sT (map n2t (numlist lim))).
Definition pstest := map t2n (map pT (map sT (map n2t (numlist lim)))).

Eval compute in test.
Eval compute in btest. (* ok with s,p borrowed from nat *)
Eval compute in stest.
Eval compute in pstest.

(* original sT,pT code - needing some help from "nat"
   for structural recursion

Fixpoint sT (a:T) :=
match a with
| E => C E E
| C E y => C (sT (hdT (sT y))) (tlT (sT y))
| C x y => C E (C (pT x) y)
end
with pT (a:T) : T :=
match a with
| E => E
| C E E => E
| C E (C x y) => C (sT x) y
| C x y => C E (pT (C (pT x) y))
end.

Thanks for your help,

Paul
*)

Attachment: CS.hs
Description: Binary data