'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

coqcoq-tactic


Solution 1:[1]

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).

Solution 2:[2]

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.

Sources

This article follows the attribution requirements of Stack Overflow and is licensed under CC BY-SA 3.0.

Source: Stack Overflow

Solution Source
Solution 1
Solution 2 Pierre Jouvelot

Related Questions