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

Huỳnh Trần Khanh (Dec 12 2023 at 04:38):

(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: Oct 13 2024 at 01:02 UTC