zohaze (Jan 02 2022 at 07:50): 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.
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 *)
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 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).
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.
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:
byis 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".
*)
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: Oct 13 2024 at 01:02 UTC