## Stream: Coq users

### Topic: How to prove 20 < 4294967296 in Coq?

#### Ende Jin (Dec 12 2023 at 03:48):

Hi everyone. I was trying to prove this but RHS automatically becomes Init.Nat.of_num_uint. I don't know how to proceed...

(deleted)

#### djao (Dec 12 2023 at 04:39):

I think this is why people use N instead of nat.

``````Load NArith.
Goal (20 < 4294967296)%N.
Proof.
reflexivity.
Qed.
``````

#### djao (Dec 12 2023 at 04:40):

I get the following warning if I use nat: `Warning: To avoid stack overflow, large numbers in nat are interpreted as applications of Nat.of_num_uint. [abstract-large-number,numbers,default]`

#### Michael Soegtrop (Dec 12 2023 at 08:59):

I must say I am not a big fan of the fact that < computes in N and Z - there are boolean and Prop comparisons, and if I want things to compute I use bool. The computational < in Z and N easily leads to runaway computation problems in automation.

@Ende Jin : the tactic to prove such things is called `lia`.

#### Ende Jin (Dec 12 2023 at 14:09):

Michael Soegtrop said:

I must say I am not a big fan of the fact that < computes in N and Z - there are boolean and Prop comparisons, and if I want things to compute I use bool. The computational < in Z and N easily leads to runaway computation problems in automation.

Ende Jin : the tactic to prove such things is called `lia`.

Thanks for the suggestion. Actually I don't know how to use lia in this setting. Do you mind be more specific?
image.png

#### Paolo Giarrusso (Dec 12 2023 at 14:47):

@djao best avoid `Load`

#### Paolo Giarrusso (Dec 12 2023 at 14:48):

@Ende Jin

``````From Coq Require Import NArith Lia.
Goal (20 < 4294967296)%N.
Proof.
lia.
Qed.
``````

#### Paolo Giarrusso (Dec 12 2023 at 14:51):

maybe `lia` should learn to reason about `Nat.of_num_uint`, but I'd claim the _goal_ you wrote is bad practice: since `nat` uses unary numbers, processing a large literal `n` in `nat` has complexity _linear_ in the number — `O(n)` steps — which is exponentially bigger than usual processing. You should instead use `N`.

#### Paolo Giarrusso (Dec 12 2023 at 14:52):

if writing `%N` is bothersome, the same snippet can also be written as follows:

``````From Coq Require Import NArith Lia.
#[local] Open Scope N_scope.
Goal 20 < 4294967296.
Proof.
lia.
Qed.
``````

#### Paolo Giarrusso (Dec 12 2023 at 14:53):

after `#[local] Open Scope N_scope.`, ` 20 < 4294967296` means `(20 < 4294967296)%N`

#### Ende Jin (Dec 12 2023 at 17:38):

Paolo Giarrusso said:

maybe `lia` should learn to reason about `Nat.of_num_uint`, but I'd claim the _goal_ you wrote is bad practice: since `nat` uses unary numbers, processing a large literal `n` in `nat` has complexity _linear_ in the number — `O(n)` steps — which is exponentially bigger than usual processing. You should instead use `N`.

Thanks! So the take away is when using large literal it is better to use `N`.
I wonder if I need to use lia in this case? Since `reflexivity` suggested earlier already works?

#### Paolo Giarrusso (Dec 12 2023 at 18:14):

reflexivity on a < b should use reflexivity of <, IMHO, not unfold < and expose its implementation details; using reflexivity makes for a more confusing and fragile proof script. I'd use lia for general arithmetic goals, and something like stdpp's compute_done for computational goals.

#### Yann Leray (Dec 12 2023 at 18:55):

Using `reflexivity` on goal `a < b` is foremost read as "(<) is reflexive and I'm proving `n < n` for some n", neither of which you are doing here (it's better, since (<) is irreflexive). The fact that the definition of (<) is unfolded and the underlying definition happens to end on a `true = true` is implementation details as Paolo said, and I agree that it's confusing and more fragile to use `reflexivity` there.
On the other hand, it is very handy that some definitions are unfolded in general

Last updated: Jun 22 2024 at 16:02 UTC