Stream: Coq users

Topic: less values


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 *)

view this post on Zulip 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)

view this post on Zulip 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 andconnective.

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

view this post on Zulip 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

view this post on Zulip 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)?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Julin S (Jan 03 2022 at 16:30):

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

view this post on Zulip Julin S (Jan 03 2022 at 16:30):

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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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))

view this post on Zulip Gaëtan Gilbert (Jan 03 2022 at 16:58):

by is a keyword

view this post on Zulip 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?

view this post on Zulip Julin S (Jan 03 2022 at 16:59):

Gaëtan Gilbert said:

by is a keyword

Ah.. that was it..

view this post on Zulip 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".
*)

view this post on Zulip Gaëtan Gilbert (Jan 03 2022 at 17:05):

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

view this post on Zulip 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).

view this post on Zulip 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".

view this post on Zulip Julin S (Jan 03 2022 at 17:18):

How is loc defined?

view this post on Zulip Gaëtan Gilbert (Jan 03 2022 at 17:19):

use andb instead of and

view this post on Zulip zohaze (Jan 03 2022 at 17:21):

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

view this post on Zulip 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..

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Julin S (Jan 03 2022 at 17:36):

Thanks!


Last updated: Jan 27 2023 at 01:03 UTC