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)

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

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

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]`

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`

.

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

@djao best avoid `Load`

@Ende Jin

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

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`

.

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

after `#[local] Open Scope N_scope.`

, ` 20 < 4294967296`

means `(20 < 4294967296)%N`

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?

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.

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