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

Should `lt`

and `nlt`

be used in the definition of `less`

?

Maybe you can use `Nat.ltb`

.

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 *)
```

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)

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

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

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

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

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?

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

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

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?

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?

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

`by`

is a keyword

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?

Gaëtan Gilbert said:

`by`

is a keyword

Ah.. that was it..

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".
*)
```

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

?

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

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

How is `loc`

defined?

use andb instead of and

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

This may be a silly question, but what is the `by`

keyword used for? Couldn't find with a quick online search..

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

It's also used in `rewrite`

https://coq.inria.fr/refman/proofs/writing-proofs/equality.html#coq:tacn.rewrite

Thanks!

Last updated: Sep 26 2023 at 12:02 UTC