coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Any tools or Tactics for reasoning about positives?

From: Jianzhou Zhao <jianzhou AT seas.upenn.edu>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Any tools or Tactics for reasoning about positives?
Date: Wed, 30 May 2012 17:35:03 -0400

Hi List,

I have some goals about properties of BinPos.positive. For example,
p1 + (p2 - p3) = p1 + p2 - p3 when p2 >= p3 ...
I did not find lemmas in Coq libs that can prove the goals like this directly,

Coq has tools to streamline proofs about real and Z. Rather than
proving them from scratch, I was wondering if Coq lib or any Coq
contribution already implemented tools or Tactics for reasoning about
BinPos.positive.

Thanks.
--
Jianzhou

[Coq-Club] Any tools or Tactics for reasoning about positives?, Jianzhou Zhao, 05/30/2012
- Re: [Coq-Club] Any tools or Tactics for reasoning about positives?, Thomas Braibant, 05/30/2012
  - Re: [Coq-Club] Any tools or Tactics for reasoning about positives?, Jianzhou Zhao, 05/31/2012