The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Matt,

did you try the zify tactic which converts nat in your context into Z? The 
tactic is not really documented but mentioned in a footnote in the Micromega 
section.

Best regards,

Michael

> -----Original Message-----
> From: 
> coq-club-request AT inria.fr
>  
> [mailto:coq-club-request AT inria.fr]
>  On Behalf
> Of Matt Quinn
> Sent: Saturday, December 1, 2018 7:12 AM
> To: Coq-Club Club 
> <coq-club AT inria.fr>
> Subject: [Coq-Club] Proof Involving Arith in Both Z and Nat
> 
> 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
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928