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

[Matt Quinn]

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

[Soegtrop, Michael]

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-----
Of Matt Quinn
Sent: Saturday, December 1, 2018 7:12 AM
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
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
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
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: [phone], www.intel.de
Managing Directors: Christin Eisenschmid
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Registe

[Matt Quinn]

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

Post by Soegtrop, Michael
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-----
Of Matt Quinn
Sent: Saturday, December 1, 2018 7:12 AM
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
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
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
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: [phone], www.intel.de
Managing Directors: Christin Eisenschmid
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928