CODEWITHSUNDEEP
coqcoq-tactic
Breno
Breno

Reputation: 165

How to deal with division in COQ?

How to deal with with the division in a goal? Because I have a goal which is clearly true... However I cannot use lia and I think that this is related to the division.

2 ^ k / 2 ≤ 2 ^ k

Bellow is my COQ screen:

enter image description here

Upvotes: 0

Views: 411

Answers (2)

M Soegtrop
M Soegtrop

Reputation: 1456

There is no automation for division on naturals - they don't even form a field. But the corresponding lemmas are not hard to find with Search:

Require Import Lia.

Goal forall k:N, 2 ^ k / 2 <= 2 ^ k.
Proof.
  intros k.
  Search (?a/?b <= ?a/?c).
  Search (_/1).
  rewrite <- N.div_1_r.
  apply N.div_le_compat_l.
  lia.
Qed.

If you have really complicated terms, you can embed the goal into reals using floor (a/b) for integer a/b and then use coq-interval. The embedding is easy to automate and coq-interval is quite powerful for proving real inequalities, but it might choke if you have more than a few floors. You can combine it with coq-gappa then to get rid of the floors. It gets quite involved then, but still fully automated. But be aware that it might not be able to prove very tight inequalities, since it uses real analysis.

Nia (Require Import Psatz), as suggested by Ana, can't solve this (and I honestly stopped trying it).

Upvotes: 1

Pierre Jouvelot
Pierre Jouvelot

Reputation: 923

Division on natural numbers is not as easy to manage as on rationals or reals (think 1 / 3). One way out of this could be to try to reframe your constraints with multiplication instead; for instance, n < m / p can sometimes be handled as n * p < m. Otherwise, using a library for rationals could be a solution.

Upvotes: 0

Related Questions