The Coq mailing list

[Matt Quinn <matt AT mattjquinn.com>]

Hello all,

I would appreciate some advice on a proof I'm stuck on involving both 
naturals and integers. I have defined this Record with t and r represented in 
Z:

Record netstate := NetState {t : Z; r : Z; c1 : channel; c2 : channel}.

And I can successfully prove this lemma stating that t and r are always >= 0 
in the context of a simple evaluation relation:

Definition safety1 (st' : netstate) : Prop := st'.(t) >= 0 /\ st'.(r) >= 0.
Lemma safety1_holds: forall st st' : netstate, (netEvalR st st') -> safety1 
st'.

However, when I attempt to prove another lemma stating that t, r, and the 
length of both channels always sums to 10:

Definition safety2 (st' : netstate) : Prop :=
    List.length st'.(c1) + List.length st'.(c2) + st'.(t) + st'.(r) = 10.
Lemma safety2_holds : forall st st' : netstate, (netEvalR st st') -> safety2 
st'.

I of course cannot proceed because list lengths are naturals, while t and r 
are in Z.

I can prove safety2_holds if I represent t and r as nat instead of Z, but I 
want to keep them in Z. What then is the best way to proceed? Should I use 
Z.of_nat on the list lengths or Z.to_nat on variables t and r? I've played 
with both paths but don't see a clear way forward through the subsequent 
match case destructions. Or is there some corollary I should set up given 
that I've already proven that t and r are always effectively natural 
themselves?

Matt