Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Proof Involving Arith in Both Z and Nat

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proof Involving Arith in Both Z and Nat


Chronological Thread 
  • From: Matt Quinn <matt AT mattjquinn.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Proof Involving Arith in Both Z and Nat
  • Date: Sat, 01 Dec 2018 21:51:45 -0800
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=matt AT mattjquinn.com; spf=Pass smtp.mailfrom=matt AT mattjquinn.com; spf=Pass smtp.helo=postmaster AT out4-smtp.messagingengine.com
  • Ironport-phdr: 9a23:jF/LLhUqFLogtk2A6IEIXfMqBn3V8LGtZVwlr6E/grcLSJyIuqrYYxaDt8tkgFKBZ4jH8fUM07OQ7/iwHzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba9xIRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/UisJ+kq1Urh29qBJ4wYHUbpybOvRlc6PBf94XX3ZNU9xNWyFDBI63cosBD/AGPeZdt4TzoEEBrQeiBQKxH+3v1z5Ihnnw3aYn1OkhFBvJ3BA8H98VtXTbtsn1NLsQUeCs0anIzDPDb/VM1Tjh74jIdwksrPeRVrx+dsrRzFMgFwLDjliIqIzlOS+V2foJs2SB8uVvS+SigHMkpQFpujWix8YhhpPUio4I11zI7yp0zJwrKdC7TkNwfMSqH4FKty6AMot7WsMiTH9suCY90rAGvoO7fDQFxZg+3B7fbuCHc5CS7hLmSumROix4i2hqeLK+gRay/lavyuvzVsm11lZFsDBJncXLtnAIzxDT686HReVh/kq52DuC1hrf5vxZLUwpj6bWJIQtzqAzm5YLtETMBC72mEH4jK+McUUk//Cl6+H9bbX6up+RLIp0hRviMqQymMy/GPk4MgkIX2id4+izyLrj/UjhTLVQkvI2irXZsIzdJckDuqG5BBZV3p8/5Ba7Ejepy88VnWIHLVJAYBKIlZLlO1DIIPDiDPewmU6gkDlxx6OOArq0CZLUa3PHjb3JfLBn6kcaxhBg48pY4sdxA60daMvuW0n3/IjdBwMlGwm93/rlEch80IVYUmWKVPzKeJjOuEOFs7p8a9KHY5UY7W6keqoVosX2hHp8omczOKyg3J8Zcne9R6o0JkyFfXj1n9YHFyEBuQ9sFbW22m3HaiZaYjOJZ4x5/isyUdz0CI7fWoK0nb2H2mGwGZgEPjkbWGDJKm/hcsC/Y9lJaC+WJZQ4wDsZSeTkUIo9zVeruRThwrVmKOXZ/CIZs5+l399wtbTe

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



Archive powered by MHonArc 2.6.18.

Top of Page