The Coq mailing list

["Matthew Brecknell" <matthew AT brecknell.net>]

Hi Paul,

paul.tarau AT gmail.com
 wrote:
> 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'm not sure what the best approach is here, but since no-one else has
answered, I'll have a go.

I doubt that nested recursion (one technique for defining the Ackermann
function) is applicable, since there's still no obvious way to make
these functions structurally recursive. The first branch of s0 and the
third of p0 are the troublesome ones.

So as you suggest, you'll need to establish well-foundedness to define
these as functions in Coq. Function may help you to do this, but one
other approach you might want to consider is to first define these as
inductive relations:

Inductive s_rel: T -> T -> Prop :=
  | s_rel_E: s_rel E (A E E)
  | s_rel_AE: forall x sx y z, s_rel y (A x z) -> s_rel x sx -> s_rel (A
  E y) (A sx z)
  | s_rel_AA: (* etc *)
with p0_rel: T -> T -> T -> Prop :=
  | (* etc *).

Note that s0 may as well be inlined into s, and that p need not be
mutually recursive with the others.

I have not tested this, and I have no idea whether inductive relations
will actually help in this case (*), but it might help to consider
proofs of existence and uniqueness separately, and this might be easier
with relational reasoning. Perhaps you can use the inductive relations
to establish well-foundedness, and then use this to define the
corresponding functions. Perhaps relational reasoning would be
sufficient for the theorems you're interested in, and you don't even
need the functions at all.

Of course, the inductive relation is a non-trivial transformation of the
Haskell code, so you'd have to convince yourself that it amounts to the
same thing as the corresponding function (perhaps by doing some proofs).

I hope you'll report back to the list if you figure this out.

Regards,
Matthew

(*) If someone on the list with more experience than me (it wouldn't
take much!) knows that this would be a waste of time, hopefully they'll
say so.