coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Automation for division over nat

From: Gert Smolka <smolka AT ps.uni-saarland.de>
To: "coq-club AT inria.fr Club" <coq-club AT inria.fr>
Subject: [Coq-Club] Automation for division over nat
Date: Sat, 9 Feb 2019 15:43:33 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=smolka AT ps.uni-saarland.de; spf=Pass smtp.mailfrom=smolka AT ps.uni-saarland.de; spf=None smtp.helo=postmaster AT thyone.hiz-saarland.de
Ironport-phdr: 9a23:6xUcCBODJGOvUuNqN2cl6mtUPXoX/o7sNwtQ0KIMzox0Lfr5rarrMEGX3/hxlliBBdydt6oUzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlLiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSkHKzE3/27YhNFzgqxVvhyvoAdyw5LNYIGQKPZ+fr/RcNEcSGFcXshRTStBAoakYoUOEeUBJ/pYpJTgqVsLqhu+AQqsC/nywTJPnX/22Ko60+AiEQ7cxwEgB8kOvG7JrNXzNaceSPu1w7PSwjXZa/NZwzH955XSfh88v/6BRLR9etfSx0k3Dw7Jk1udpIP/Mz6R1+kBqWqW4/B+We+hlWIrsx99riWty8s2iYTFmJgZx1TA+Clj3Yo5Odu1Q1Nhb9G+CptfrSSaOpN2Qsw8R2Fovz43yqEGuZ+7eygKzoooywTfa/yGcomE+wnjW/yLLjdigHJqYrS/iAuo/Ue91OLwTsi00FBUoSpZitTAq34A2hPJ5sWDS/Zx5EWs1SyR2w3d9O1IOUU0mrDaK54lzL4wjJ0TsUHbEy/tnUX2i6uWdkY+9eWz8+Tnea/qpoKaN491kw3+Kb4hldalAeQ8KAcOWXWU9f6h27L95UH5WqlFjuUqkqnFt5DXPdgUpqmgAwNMzokj7wu/ACy93dQDnXgHKUpFdwidg4joPVHOOvH4Au2lj1Siijc4j8zBa/fqBYyIJXzemp/ge6x84ghS0kIYyc1VrdoAAbYYZfn3R0XZtdrCDxZ/PRbikMj9D9Ao+Y4ERSq0B6idM6qa5USN4eYsKsGUf8kIvje4MPEs/frni3N/lVJLLvrh5ocedH3tRqcuGE6ee3e52o5QQ1dPhRI3SanRsHPHVDdSY3ioWKdmvmMjE8S7C4aGXYmkmriI2iv9EpAEPzkaWGDJKm/hcsC/Y9lJcDibeJcziidCSL6gDpQo3AuqvQn2jbZqfLKNp38o8Kn73d0w3NX90BE/8TsuU5aB03CKSWwynmIaAiQ/1bp7qEpxjFuOg/B1

Is there tactic support for proving lemmas involving division over nat, for
instance

a) 1 <= k <= x -> x/k >= 1
b) x <= y -> k >= 1 -> x/k <= y/k.
c) k >= 1 -> (k * x) / k = x.

I'm using the tactics lia and nia but they don’t know about division.

Thanks,
Gert

[Coq-Club] Automation for division over nat, Gert Smolka, 02/09/2019
- Re: [Coq-Club] Automation for division over nat, Laurent Thery, 02/09/2019
  - Re: [Coq-Club] Automation for division over nat, Bas Spitters, 02/09/2019
  - Re: [Coq-Club] Automation for division over nat, Gert Smolka, 02/09/2019