Stream: Coq users

Topic: less values

zohaze (Jan 02 2022 at 07:50):

I want to establish less than relation between two natural numbers. Therefore defined inductive type with two constructors less and not less. Then compare two values ,if one is less than other then true else false. But get invalid pattern message
Inductive less_1 : Type :=
|lt (r c :nat)
|nlt (r c :nat).

``````Definition less(n1 n2:nat) : bool :=
match n1 ,n2 with
| n1 < n2 =>true
| n2 < n1 =>false
end.
``````

Julin S (Jan 02 2022 at 08:59):

Should `lt` and `nlt` be used in the definition of `less`?

Maybe you can use `Nat.ltb`.

Julin S (Jan 02 2022 at 09:12):

I'm not sure if this correct (I hope others will correct me), but we can't just do `2 < 3` as it would be a value of `Prop` type ( a proposition). For that matter we could even say `3 < 2`.

``````Compute (2 < 3).
Compute (3 < 2).
``````

without error.

What you may be need could be

``````Compute Nat.ltb 2 3. (* true : bool *)
Compute Nat.ltb 3 2. (* false : bool *)
``````

zohaze (Jan 02 2022 at 14:00):

In x,y plane , I have two points a(x1,y1) & b(x2,y2). In order to find smaller value point (a< b), I have to write x1<x2 & y1<y2. Formally can I write like above and use above command? Like (and (Nat.ltb x1 x2)(Nat.ltb y1 y2)=true)

Pierre Castéran (Jan 02 2022 at 15:31):

You may represent points as records.
Here is a possible definition of a boolean function. Note that it uses the `andb` boolean function and not the logical `and`connective.

``````Require Import Arith Bool.

Record point: Set :=
mkPoint{pointX :nat; pointY:nat}.

Definition smallerb (a b : point):=
andb (Nat.ltb (pointX a) (pointX b))
(Nat.ltb (pointY a) (pointY b)).

Compute smallerb (mkPoint 2 4) (mkPoint 4 5).
``````

By the way, are you sure of your definition ? There are a lot of pairs of incomparable points.

``````Compute smallerb (mkPoint 4 6) (mkPoint 4 2).
Compute smallerb (mkPoint 4 2) (mkPoint 4 6).
Compute smallerb (mkPoint 2 4) (mkPoint 4 2).
Compute smallerb (mkPoint 4 2) (mkPoint 2 4).
``````

zohaze (Jan 02 2022 at 16:53):

Actually ,I want to subtract two natural numbers (points). It is only possible when one number is less than other. Any suggestion for testing the two numbers so that they become suitable for subtraction? x2-x1, y2-y1

Julin S (Jan 03 2022 at 04:14):

zohaze said:

I want to subtract two natural numbers (points).

But a point consists of two natural numbers, right? Could you give a complete example as to how it would look like to make it clearer?

Which numbers would you need to compare for two points (x1, y1) and (x2, y2)?

zohaze (Jan 03 2022 at 15:05):

At location (x1,y1) 4 is present and at (x2,y2) 9 is present. I want to subtract 4 from 9. Therefore,first check that value at (x1,y1) is less than value at (x2,y2),so that subtraction is possible. (4<9).In case first value is smaller then function gives the x,y of smaller value at the output.
Some thing like this

``````Definition co_ordinates (n1 n2: points) : points  :=
match n1,n2 with
c{x,y}, c{x',y'} =>
if (smallerb {x,x'} {y,y'}) then {x,y} else {0,0}
end.
``````

zohaze (Jan 03 2022 at 15:14):

How I can record points (x1,y1) & (x2,y2) in following
Record point: Set :=
mkPoint{pointX :nat; pointY:nat}? Like (2 ,1) & (3,2). Is it possible to directly pass x1,y1,x2,y2 as input arguments to above smallerb function?

Julin S (Jan 03 2022 at 16:30):

Okay, so there are three values associated with each point? x,y coordinates and the value?

Julin S (Jan 03 2022 at 16:30):

If that's the case, we can use one more field in the record type.

Julin S (Jan 03 2022 at 16:40):

Something like

``````Record point : Set := mkPoint {
x : nat;
y : nat;
val : nat
}.

Definition smaller (a b : point) : point :=
if (Nat.ltb a.(val) b.(val)) then a else b.

Compute smaller (mkPoint 3 1 4) (mkPoint 1 1 9).
(*
= {| x := 3; y := 1; val := 4 |}
: point
*)
``````

maybe?

Julin S (Jan 03 2022 at 16:42):

I tried doing it with tuples as well. But in the course of doing so, I got an error while 'destructing' the tuples:

``````Definition smaller' (a b : nat * nat * nat) : nat * nat :=
let '(ax, (ay, aval)) := a in
let '(bx, (by, bval)) := b in
(ax, ay).
(*
Syntax error: [constr:pattern level 200] expected after '(' (in [constr:pattern]).
*)
``````

Does anyone know how this can be fixed?

Ana de Almeida Borges (Jan 03 2022 at 16:53):

I think tuples are left associative, so perhaps you want `(a b : nat * (nat * nat))`

Gaëtan Gilbert (Jan 03 2022 at 16:58):

`by` is a keyword

Julin S (Jan 03 2022 at 16:59):

I tried

``````Definition smaller' (a b : nat * (nat * nat)) : nat * nat :=
let '(ax, (ay, aval)) := a in
let '(bx, (by, bval)) := b in
(ax, ay).
``````

but that gave the same error.

Are `(nat * nat * nat)` and `(nat * (nat * nat))` different types?

Julin S (Jan 03 2022 at 16:59):

Gaëtan Gilbert said:

`by` is a keyword

Ah.. that was it..

Julin S (Jan 03 2022 at 17:04):

Are (nat * nat * nat) and (nat * (nat * nat)) different types?

I guess it is.

For

``````Definition smaller' (a b : nat * (nat * nat)) : nat * nat :=
let '(xa, (ya, vala)) := a in
let '(xb, (yb, valb)) := b in
if (Nat.ltb vala valb) then (xa, ya) else (xb, yb).
``````

This worked:

``````Compute smaller' (3,(1,4)) (1,(1,9)).
``````

but this gave error:

``````Compute smaller' (3,1,4) (1,1,9).
(*
The term "(3, 1, 4)" has type "(nat * nat * nat)%type"
while it is expected to have type "(nat * (nat * nat))%type".
*)
``````

Gaëtan Gilbert (Jan 03 2022 at 17:05):

why not do `let '(xa, ya, vala) := ...`?

Julin S (Jan 03 2022 at 17:08):

Yeah that ran without error too:

``````Definition smaller'' (a b : nat * nat * nat) : nat * nat :=
let '(xa, ya, vala) := a in
let '(xb, yb, valb) := b in
if (Nat.ltb vala valb) then (xa, ya) else (xb, yb).

Compute smaller'' (3,1,4) (1,1,9).
Compute smaller'' ((3,1),4) ((1,1),9).
(*
= (3, 1)
: nat * nat
*)
``````

Had thought some default associativity rules would make `nat * nat * nat` same as `nat * (nat * nat)` but it seems that it is `nat * nat * nat` and `(nat * nat) * nat` that are same (left-associative like mentioned earlier).

zohaze (Jan 03 2022 at 17:17):

Whats wrong with this
Definition smaller_coordinates (x1 x2: loc) : bool :=
match x1, x2 with
| { x , y }, { x' , y' } =>
if(and(Nat.ltb x x')(Nat.ltb y y')) then true else false
end.
error: The term "x <?x' " has type "bool" while it is expected to have type "Prop".

Julin S (Jan 03 2022 at 17:18):

How is `loc` defined?

Gaëtan Gilbert (Jan 03 2022 at 17:19):

use andb instead of and

zohaze (Jan 03 2022 at 17:21):

Inductive type with two nat arguments. It works(andb). Thanks to all of you.

Julin S (Jan 03 2022 at 17:26):

This may be a silly question, but what is the `by` keyword used for? Couldn't find with a quick online search..

Li-yao (Jan 03 2022 at 17:35):

The refman is a better place to search keywords: https://coq.inria.fr/refman/search.html?q=by&check_keywords=yes&area=default

Li-yao (Jan 03 2022 at 17:35):

It's also used in `rewrite` https://coq.inria.fr/refman/proofs/writing-proofs/equality.html#coq:tacn.rewrite

Julin S (Jan 03 2022 at 17:36):

Thanks!

Last updated: Jun 25 2024 at 15:02 UTC