The Coq mailing list

[Matt Quinn <matt AT mattjquinn.com>]

Thanks Michael for the suggestion. Didn't know about zify. That led me to 
realize I should be using Zlength for the lists rather than length:

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

After that the proof went through. Thanks again.

Matt

On Fri, Nov 30, 2018, at 11:41 PM, Soegtrop, Michael wrote:
> 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