The Coq mailing list

[paul.tarau AT gmail.com]

I am new to Coq and trying to use it to prove some theorems (like theorem1)
about the following Haskell program:

data T = E|A T T deriving (Eq,Read,Show)

-- successor
s E = A E E
s (A x y) = s0 x y

s0 E y = A (s x) z where A x z = s y
s0 (A a b) y = A E (A (p0 a b) y) 

p0 E E = E
p0 E (A x y) = A (s x) y
p0 (A a b) y = A E (p0 (p0 a b) y)

-- predecessor
p (A x y) = p0 x y

-- empirically true for the first 1000 trees, E, s E, s (s E) ...
theorem1 x = p (s x) == x && (x==E || s (p x) == x) 

I tried to port it to Coq as:

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

Delimit Scope t_scope with T.

Fixpoint
  s (k:T) {struct k} :T := match k with
  | E => A E E
  | A x y => s0 x y
  end
with (* the problem seems to originate here *)
  s0 (x y : T) : T := match x with
  | E => A (s (src (s y))) (tgt (s y))
  | A a b => A E (A (p0 a b) y) 
  end   
with
  p0 (x y : T) {struct x} : T  := match x,y with
  | E,E => E
  | E, A x y => A (s x) y
  | A a b, y => A E (p0 (p0 a b) y)
  end
with 
  p (z : T) {struct z} : T := match z with
  | A x y => p0 x y
  | E => E (* should never happen *)  
  end
with src (x : T) {struct x} : T := 
  match x with
  | A a _ => a
  | E => E (* should never happen *)
  end
with tgt (x : T) {struct x} : T := 
  match x with
  | A _ b => b
  | E => E (* should never happen *)
  end.  

I got in trouble with the relatively complex induction pattern that
seem to be required in either Fixpoint or Function to express the
fact that while s0 is likely to be well founded in x and y,
their decreases are interleaved in a non-trivial way.

I have seen some examples handling Ackermann's function so my guess is that 
Coq
should be able to handle such definitions.

Thanks for any hints,

Paul