## Stream: Coq users

### Topic: list of points

#### zohaze (Jan 18 2022 at 17:33):

I have two points
let (xa, ya, vala) := a in
let (xb, yb, valb) := b in
In order to confirm the presence of point in the list, i have to prove In (point) l. For this purpose I have defined
In function but it has error

``````Fixpoint In (point :pixel) (l:list points) : Prop :=
match l with
| [] => False
| point1:: t => match point1 , point with
(xa, ya, vala), (xb, yb, valb) =>
(xa, ya, vala):: t => eqpoints ((xa, ya, vala) (xb, yb, valb) )
\/ In (xb, yb, valb) t
end
end.
``````

#### Pierre Castéran (Jan 18 2022 at 19:45):

The `In`predicate of standard library has the following type:

``````In
: forall A : Type, A -> list A -> Prop
``````

In your definition, you check if some point of type `pixel` belongs to a list of `points`. You got probably a typing error.

#### zohaze (Jan 19 2022 at 12:59):

I want to use In function from standard library. I want to ask that if I have to prove In (point)(list points) then what I should do? Give some proof that point lies in the list.

#### Pierre Castéran (Jan 19 2022 at 15:59):

`In` is defined in terms of equality, `or`and False (look at the answer to the `Compute`command).
So, you have to work with propositions of the form "a1 = x \/ a2 = x \/ ... \/ an = x \/ False".

``````Require Import List.
Import ListNotations.
Record point := mkpoint{pointX:nat; pointY:nat}.

Compute In (mkpoint 1 0)   [mkpoint 2 0 ; mkpoint 5 8; mkpoint 1 0 ; mkpoint 3 6].

Goal In (mkpoint 1 0)   [mkpoint 2 0 ; mkpoint 5 8; mkpoint 1 0 ; mkpoint 3 6].
Proof. repeat ((left; reflexivity) || right).
Qed.

Goal ~ In (mkpoint 21 0)   [mkpoint 2 0 ; mkpoint 5 8; mkpoint 1 0 ; mkpoint 3 6].
Proof.  intro H; now repeat ( destruct H as [? | H]; [discriminate| ] ).
Qed.
``````

#### zohaze (Jan 20 2022 at 17:49):

Thank you. Actually I want to compare the elements of list with input element in form of boolean.

``````Lemma eq_points: forall points1 points2,
points1=? points2 = true .

Lemma eq_ponits: forall p(( x, y))  p(( x', y))},
p(( x, y))=? p(( x', y')) = true .
``````

But problem is that I have points in the form of points notation like p((2,3))=p((6,5) in hypothesis. On the basis of this false equality of points I want to close sub goal.
In another way , If I pass these points to eq_ponits and get false. Then on the basis of false I close sub goal (it is possible? As long as I have false equality of points in hypothesis ,i will be able to close sub goal.)

#### Pierre Castéran (Jan 21 2022 at 07:51):

Your lemmas state that all points are equal.

Indeed, do you want to define a function which tests whether a given point belongs to a list of points ?
In this case, the goal is to build a fonction `points_Inb: point -> list point ->bool` or better
`points_In_dec : forall (p:point)(l:list point), {In p l}+{~In p l}`

Here a possible solution (with any type `A` on which equality is decidable, which is the case of `point`).

``````Definition decide (P:Prop) := {P}+{~P}.

Definition In_dec {A:Type}(A_eq_dec : forall a b:A, decide (a=b)):
forall (a:A) l, decide (In  a l).
Proof.
induction l as [|b l IHl].
- right; auto.
-  destruct (A_eq_dec a b) as [Heq | Hneq].
+ subst; left; now left.
+ destruct IHl as [Hin | Hout].
*  left; now right.
*  right. red; destruct 1; [ congruence | contradiction].
Defined.
``````

If you really want booleans:

``````Definition Inb {A:Type}(A_eq_dec : forall a b:A, decide (a=b))
(a:A)(l: list A): bool :=
if In_dec A_eq_dec a l then true else false.
``````

#### zohaze (Jan 21 2022 at 13:49):

Last question, can I apply H on goal 1 statement directly? (I am comparing only co-ordinates,ignore values.If they match then both H & goal 1 statements are same) . Want to apply H on goal 1& 2 and H2 on goal3 (although point does not exist in the list ,but coordinates are same.If we ignore values then both statements are same .Therefore It should be applicable.

``````H:In point((0,1,valu1))[point((0,0,valu3)), point((0,1,valu8))]
Goal 1: In (point((0,1,valu41))) [point((0,0,valu3)), point((0,1,valu5))]
Goal 2: In (point((0,1,valu3))) [point((0,0,valu2)), point((0,2,valu8))]

H2:In point((0,1,valu1))[point((0,0,valu3)), point((0,4,valu3))]
Goal 3: In point((0,1,valu3))[point((0,0,valu1)), point((0,4,valu1))]
``````

#### Pierre Castéran (Jan 21 2022 at 14:12):

The problem is that `point(0,1,2)`is different from `point(0,1,33)`, so `In`won't work as you mention.

You may consider two types: `point` and `pixel` (point with a value, if I understand on what you're working).
Then you can either define a function `pixel2point : pixel -> point`, and consider such statements as
`In (pixel2point p) (map pixel2point l), or consider the relation `px_equiv px1 px2 := pixel2point px1 = pixel2point px2` and statements of the form `Exists (px_equiv px) l`.

#### zohaze (Jan 21 2022 at 17:39):

I have points with values. But I am not considering values. I am comparing only co-ordinates. If co-ordinates matches (with what ever value they have) ,then In n l should return prop. I have function with arguments point ,values and after comparing x ,y it gives true or false. It ignore values. Now I have above H , H2,goal 1 2 and 3 .Can I apply H to close goals in current scenario? In In (pixel2point p) (map pixel2point l), first I have to define function which make this conversion? Secondly for considering the relation (px_equiv px1 px2), I have to consider each and every point?

#### Pierre Castéran (Jan 21 2022 at 18:31):

Here is an example. Is it OK to you ?

``````Record point : Set := P {x: nat; y: nat}.
Record pixel : Set := PX {pixel2point: point; px_value: nat}.

(** Ignores pixel values *)
Definition In_px (px: pixel) (pxs : list pixel):=
In (pixel2point px) (map pixel2point pxs).

Goal In_px (PX (P 2 3) 42)  [PX (P 0 1) 45; PX (P 2 3) 12; PX (P 4 5) 33].
right; left.  reflexivity.
Qed.

Definition px_equiv (px px' : pixel) :=
pixel2point px = pixel2point px'.

Definition In_px' (px:pixel) (ps: list pixel):= Exists (px_equiv px) ps.

Goal In_px' (PX (P 2 3) 42)
[PX (P 0 1) 45; PX (P 2 3) 12; PX (P 4 5) 33].
right;left; reflexivity.
Qed.
``````

#### zohaze (Jan 22 2022 at 12:13):

Yes. Thanks. Above record can be written in the form of list of list? One list for points other for its values,so that both forms are equal? So that replace [ (PX {pixel2point: point; px_value: nat}]. with [Definition PX := [list points[list val]] ]
I have inductive type for points and another for values.

#### Pierre Castéran (Jan 22 2022 at 12:45):

But you would have to assume and/or verify that the list of points and the list of values have the same length !
This would make your specification and proofs longer !
Better to consider lists of pairs (point, values) (type `list (point * value)` or `list pixel` as in the previous message).

#### zohaze (Jan 22 2022 at 13:28):

Ok. Thank you. Its true when element exist in the list. It means if one of the coordinated either x or y does not match with the element of list ,then reflexivity will not work then have to define ~ In n l. (which may exist when x<>y \/ val1<> val2.)

#### pianke (Jan 24 2022 at 14:33):

My problem is more or less same like above. But want to confirm that provided point(n) does not occur in the list. Can I use above function?)

#### pianke (Jan 25 2022 at 17:39):

@Pierre Castéran and zohaze may I get help from your problem statement? (In case n does not exist in l. )

#### Pierre Castéran (Jan 25 2022 at 19:24):

Could you give us examples of propositions you cannot prove (if possible in a small self-contained `.v`file) ?

#### pianke (Jan 26 2022 at 13:25):

Any example,like you have given above
Goal In_px' (PX (P 2 3) 42)
[PX (P 0 1) 45; PX (P 3 3) 42; PX (P 4 5) 33].

#### Pierre Castéran (Jan 26 2022 at 17:24):

This is certainly not the best solution, but it works on these examples.
You may try to remove the tacticals and replay the proofs step by step in order to get simpler but larger scripts.

``````Require Import Arith List Bool.
Import ListNotations.

Record point : Set := P{x: nat; y: nat}.
Record pixel : Set := Px{px_point: point; px_val: nat}.
Definition px_equiv (px1 px2: pixel) := px_point px1 = px_point px2.

Definition In_point px l := In (px_point px) (map px_point l).

Goal ~ In_point (Px (P 2 3) 255)
[Px (P 2 1) 255; Px (P 4 3) 255; Px (P 20 3) 255; Px (P 2 31) 255].
intro H.
repeat ((eapply in_nil; eassumption) ||
( destruct H as [H0| H] ; [try discriminate | ])).
Qed.

Goal  ~ In_point (Px (P 2 3) 255)
[Px (P 2 1) 255; Px (P 4 3) 255; Px (P 2 3) 128; Px (P 2 31) 255].
intro H.
repeat ((eapply in_nil; eassumption) ||
( destruct H as [H0 | H] ; [try discriminate | ])).
Abort.
``````

#### pianke (Jan 27 2022 at 17:06):

Following is sum of multiple commands. Can I split these command for easy understanding especially for new one? repeat ((eapply in_nil; eassumption) || ( destruct H as [H0| H] ; [try discriminate | ])).
Second I have subgoal statement which is wrong . I am closing it by try discriminate,but it is not working
{|p_point := {| x := 0; y := 1 |}; val := 88|} ={| p_point := {| x := 1; y := 0 |}; val := 88|}

#### Pierre Castéran (Jan 27 2022 at 18:21):

Indeed, the `try`before `discriminate`was useless. The tactic I wrote can be used only for proving that some `x`is not in a given list, by proving `x`is different from every element of the list.
But, as I said, it's not the best solution (it was made only for the subgoal you asked for).

A better solution you may try is
a) define a boolean function for checking if there is in the list `l`a pixel equivalent to `p`
b) prove that your function returns `true` if and only if the property above is true.
Indeed there is already a function `existsb` in https://coq.inria.fr/distrib/current/stdlib/Coq.Lists.List.html.

``````Definition point_eqb (p q: point) := andb (Nat.eqb (x p) (x q))
(Nat.eqb (y p) (y q)).
Definition pixel_equivb (px px': pixel):=
point_eqb (px_point px) (px_point px').

Compute existsb (pixel_equivb (Px (P 2 3) 255))
[Px (P 2 1) 255; Px (P 4 3) 255; Px (P 20 3) 255; Px (P 2 31) 255].

Compute existsb (pixel_equivb (Px (P 2 3) 255))
[Px (P 2 1) 255; Px (P 4 3) 255; Px (P 2 3) 128; Px (P 2 31) 255].
``````

#### pianke (Jan 29 2022 at 07:06):

Thanks: H: In [PX (P 3 4) 77 [ PX (P 3 3) 77 ; PX (P 3 4) 77; PX (P 2 2) 77].
goal: (PX (P 3 2) 77)= (PX (P 2 3) 77)
existb checks the presence of an element in the list and give bool type. But goal statement is to prove the equality of two pixels and both pixels do not exist in the list of hypothesis.If I simplify In n l then n will be compare with each element of list.As a result I get list of equality of pixels in H . Now I can compare goal equality with equality in hypothesis. It means it should return false in my case.In this case there is no need of existb function.It may help in goal closing? Secondly, goal statement is related to the equality of two pixels, not their presence
in the list.If I prove both pixels are not equal and get false by pixel_equivb .Can I close the current gaol statement? Which one may be use?

#### Pierre Castéran (Jan 29 2022 at 15:26):

From which initial goal or lemma statement and tactics did you obtain your goal ?

This goal (as it is written in your post), if solved, would imply `2=3`, hence `False`.
You can verify it using tactics like `injection`, `discriminate`or `congruence`.

Please note that the `In x l` proposition means "x is equal to some element of l".
If `l`is a list of points, OK.
But if you consider pixels, are you interested in equality of pixels (same position, same value)
or equivalence (just same position) ?

In the first case `In (Px (P 3 4) 12) [Px (P 1 2) 10;Px (P 3 4) 12]` is provable but not `In (Px (P 3 4) 128) [Px (P 1 2) 10;Px (P 3 4) 12]`

If you consider pixel equivalence, you should consider `List.Exists` instead of `List.In`.

``````Definition px_equiv (px1 px2: pixel) := px_point px1 = px_point px2.
Goal Exists (px_equiv (Px (P 3 4) 12)) [Px (P 1 2) 10; Px (P 3 4) 128].
right;left;reflexivity.
Qed.
``````

#### pianke (Jan 29 2022 at 18:31):

I am comparing only x & y coordinates, values are same and using In x l . Useing map function for conversion into
points. To solve the goal
Px (P 0 1) val:= Px (P 2 0) val. I have applied injection command I get this message
"Not a negated primitive equality". Whats its meaning? Values are same in hypothesis as well as in goal .Only difference lies in x & y of point and both points do not exist in In x l (list of points) .Accept try discriminate command
but do nothing.

#### Pierre Castéran (Jan 29 2022 at 19:03):

Hi, is there a typo in your goal ? the `:=` operator in your goal results in a syntax error.

Dis you mean `Px (P 0 1) val <> Px (P 2 0) val` ? In this case `discriminate`works.
`injection` without any arguments works also, but `discriminate`is more direct.

If your goal is `Px (P 2 0) val = Px (P 2 0) val`, `reflexivity`is OK.

`injection H` works if you have an hypothesis `H: Px p val = Px p' val'` and you want to prove `p=p' /\ val=val'`

In general, it would be better to show a smallest as possible, self-contained `.v` file (Library requirements, and the proof script which fails).
Otherwise, we do not know which could be the issue, and could give irrelevant answers.

#### pianke (Jan 30 2022 at 15:38):

Example you have given against reflexivity ,is working properly. Example against discriminate does not work because of
difference in way of representation(I think). Definition point_eqb requires two points & pixel_equivb requires two pixels. I write input arguments in this way point_eqb ( p p' :points) & point_eqb (p p': pixels).As I said I have goal related to the equality of two pixels.Like below

{|p_point := {| x := 0; y := 1 |}; val := 77|} = {| p_point := {| x := (S b1); y := 0 |}; val := 77|}.
Goal is in expanded form(point = x y; val=77). Now want to pass x y to point_eqb to check their equality.
assert(point_eqb p_point p p' = true)
assert(point_eqb P(0 2)(P (S b1) 1) = true)
assert (pixel_equivb (PX{ P(0 2) ; val:77}) (PX{ P(Sb1) 1) ; val:77}).
In all above ways of representation I have errors ( unknown p p' b1).It does not accept any way of writing.How I should write it.(x y form in functions?)

#### Pierre Castéran (Jan 30 2022 at 17:09):

Hi,
Your equality is false `{|p_point := {| x := 0; y := 1 |}; val := 77|} = {| p_point := {| x := (S b1); y := 0 |}; val := 77|}.` with `discriminate`you can easily prove its negation (with `<>`instead of `=`).

In which context `p`, `p'` and `b1`are declared ? inside a proof script or a section ? Problems with tactics or commands can only be explained in a precise context which we could understand if you gave us a small but self-contained Coq source which leads to the issue (error message or difficulty/impossibility to prove the goal).

#### pianke (Jan 31 2022 at 06:27):

I have below goal statement .There are two p_points with different x & y.( I want to differentiate between them as p p'.)

`````` {|p_point := {| x := 0; y := 1 |}; val := 77|} =
{| p_point := {| x := (S b1); y := 0 |}; val := 77|}.
``````

I get false from below equality finding function. Same statement as above . p-point = x=0 & y=1
and PX ( P 0 1)

``````Compute (pixel_equivb  (PX (P 0 1)  77)  (PX (P (S b1) 0) 77)).
``````

I want to relate both satatements. When have function I should be able to use it to close goal statement. Simply want to get false from first one. but i am facing unknown x y b1 error message. I want to pass parameters of goal statement(x y val) to pixel_equivb to get answer.
.

#### Karl Palmskog (Jan 31 2022 at 06:30):

@pianke when posting snippets of Coq code, please start on a new line and use triple backticks, then newline and the Coq code, then triple backticks:

``````<triple backticks>
<coq code>
<triple backticks>
``````

This makes your code much easier to read for people who might be able to help.

#### Karl Palmskog (Jan 31 2022 at 06:31):

for small snippets of inline code, you can just put the code into single backticks, and then it show up like this: `statement(x y val)`

#### Pierre Castéran (Jan 31 2022 at 07:25):

@pianke Hi,
Karl Palmskog said:

pianke when posting snippets of Coq code, please start on a new line and use triple backticks, then newline and the Coq code, then triple backticks:

``````<triple backticks>
<coq code>
<triple backticks>
``````

This makes your code much easier to read for people who might be able to help.

In order to make it even easier to help, you may give us all information under the form of a mini coq script we could replay, with `admit`and/or `Admitted`or `Abort`where you find it difficult to complete the proof.
For instance:

``````<triple backticks>
Require Import Arith List Bool.
Import ListNotations.

Record point : Set := P{x: nat; y: nat}.
Record pixel : Set := Px{px_point: point; px_val: nat}.

Definition point_eqb (p p': point) :=
Nat.eqb (x p) (x p') && Nat.eqb (y p) (y p').

Lemma point_eqb_true_iff (p p': point) :
point_eqb p p' = true <-> p = p'.
Proof.
split.
- intro; subst.
<triple backticks>
``````

Then, we can copy/paste and run the code and will be able to get easily the context of all problematic commands or tactics, and give you appropriate help.

Of course, this is OK for short snippets. For longer pieces of code, I don't know yet.

#### pianke (Jan 31 2022 at 17:20):

I have modified my post.

#### pianke (Feb 02 2022 at 08:13):

I have function (pixel_equivb) to check their equality. Unable to pass x y and val to this function because of requirement difference.This function requires pix p p', but I have this information in form of x y val. There is no way to close the gaol in current situation?

``````H0:{| p_point := {| x := 0; y := 0 |};val := 77|} =
{| p_point := {| x := 0; y := 0 |};val := 77|}.

goal:{| p_point := {| x := 0; y := 1 |};val := 77|} =
{| p_point := {| x := 1; y := 0 |};val := 77|}.
``````

#### Pierre Castéran (Feb 02 2022 at 08:30):

Your goal should not be closed, because your pixels are indeed different (because of the `y`coordinate).
Does this goal appear as a sub-goal of a bigger proof ? In this case, please post a snippet of the full proof (with the goal statement and all the tactics which led to this goal).
When some unsolvable conclusion appears in a proof, it may happen that either the current hypotheses lead to a contradiction (for instance in a proof by absurd, which is a perfectly usual situation), or that a previous step was mistaken.
In both cases, we will certainly be able to analyse and explain the situation.

#### pianke (Feb 04 2022 at 16:51):

Its a sub goal and it is contra statement. After your reply I reviewed my code and found contra statement.On the basis of this I have closed the sub goal. Thank you. We can assert a lemma statement by assert command in another lemma statement.How I can assert a definition in other lemma statement? Like I have below definition want to apply to another px1 & pxs1 in the goal statement.

``````Definition In_px (px: pixel) (pxs : list pixel):=In (pixel2point px) (map pixel2point pxs).
``````

#### Pierre Castéran (Feb 04 2022 at 18:00):

Hi,
If you want to use `In_px`in various situations, the best is to write your definition of `In_px`at a global level (I mean before your proofs). Putting `Definition ...` commands inside a proof is strongly discouraged.

To answer your question, it is possible to add a local definition inside a proof script, but it will disappear when the current sub-goal is closed. It's useful only for very temporary uses.
The syntax would be in your example `pose (In_px := fun px pxs => In (px_point px) (map px_point pxs))`.

#### pianke (Feb 05 2022 at 07:38):

Actually I have function whose output is list pixel. In a (f1 a). I want to apply In_px on my In n l.But get this error message
Syntax error: [name] or ':' expected (in [closed_binder]).
I have written in this way
pose (In_px := fun a (f1 a) => In (p_point a) (map p_point (f1 a))). where a is pixel.

#### Pierre Castéran (Feb 05 2022 at 08:10):

You don't tell us what are `a`and `f1`. Previously declared variables of respective type `pixel`and `pixel -> list pixel` ?
It's difficult to guess where the errors come from if you post too partial snippets (without the commands which lead to the error).

If you define a function like `In_px` (globally with `Definition`or locally with `pose`), you define it for any pixel `px`and any list of pixels `pxs`. Later, you may apply it with particular values of the right type, for instance `In_px a (f1 a)`.

The correct syntax are either

``````Definition In_px px pxs :=In (pixel2point px) (map pixel2point pxs).
``````

or

``````pose (In_px := fun px pxs => In (px_point px) (map px_point pxs)).
``````

where `px`and `pxs`are just variables, which is not the case of your example.

#### pianke (Feb 05 2022 at 08:54):

Goal : In a(f1 a). Want to apply In_px command to convert it.Now have pixel and list of pixel comes from (f1 a). Then it should execute without error. I have applied this command

``````pose (In_px := fun a (f1 a) => In (p_point a) (map p_point (f1 a))).
``````

where a is pixel f1 requires pixel ->list pixel. I have defined In_px globally. Now one way is to use apply command like apply In_px a (f1 a)(because I have In a (f1 a)). Then error: Unable to unify "Prop" with "In a (f1 a)". Secondly, by pose command want to define locally. But Syntax error: [name] or ':' expected (in [closed_binder]) occurs,how to remove it?

#### pianke (Feb 06 2022 at 14:46):

How to eliminates this error " Unable to unify "Prop" with "In a (f1 a)" ? . Compute In_px (Px (P 2 0)77 ) (f1 Px (P 2 0) 77)) works properly.

#### Pierre Castéran (Feb 06 2022 at 16:56):

Hi @pianke
May I assume you have a file (for instance `foo.v`) on your computer, the use of which (by compilation, or interactive work on CoqIDE or Proof General) causes these errors ?
If it's not too long, would you please share it (by copy/paste into a snippet) ? If nothing (library requirements, definitions, lemmas, goals and tactics) is lacking, we could be able to explain where is the problem (error messages or difficulty to solve some goal).
Otherwise, it would be difficult to guess what you have really typed.

(deleted)

#### pianke (Feb 17 2022 at 16:34):

H1: {| px_point := {| x := 0; y := 0 |}; val := 77 |} = {| px_point := {| x := 0; y := 0 |};val := 77 |} \/ False
H2: {| px_point := {| x := 0; y := 3 |}; val := 77 |} ={| px_point := {| x := 0; y := 3 |}; val := 77|} \/ False
goal: {| px_point := {| x := 0; y := 3 |}; val := 77 |} = {|px_point := {| x := 0; y := 0 |};val := 77 |}
Goal statement is wrong. I have applied command try discriminate and lia. But it does not close the goal. How I can close the goal?

#### Pierre Castéran (Feb 17 2022 at 16:54):

What do you mean by "close the goal" ? If your proposition cannot be proved under your hypotheses, there is no way to complete the proof. If I oversimplify your goal (replacing pixels with natural numbers), I obtain the following interaction (with the same structure as yours) , and give up with `Abort`.

``````Hypothesis H : 2 = 2 \/ False.
Hypothesis H': 3 = 3 \/ False.

Goal 2 = 3.
(*
1 goal (ID 19)

H0 : 2 = 2
H1 : 3 = 3
============================
2 = 3

*)
Abort.
``````

By the way, the `\/ False` are useless, since `P \/ False` is equivalent to `P`.

#### pianke (Feb 17 2022 at 17:11):

Close the goal mean,under these hypotheses proposition may hold or not.So that move toward next statement. Why these two commands are not working? try contradiction. try discriminate.

#### zohaze (Apr 04 2022 at 16:33):

I have two hypothesis H1 & H2. I struck in proving below statement. Please guide me in solving .
H1: {| p_point := {| x := 1; y := S b2 |}; val := val2|} ={| p_point := {| x := x1; y := y1 |}; val := val|} \/
{| p_point := {| x := 0; y := S (b2+1) |}; val := val2|} ={| p_point := {| x := x1; y := y1 |}; val := val1|} \/
{| p_point := {| x := 0; y := b2-0) |}; val := val2|} ={| p_point := {| x := x1; y := y1 val := val1 \/ False

H2 :{|p_point := {| x := 1; y := 0) |}; val := val3|} ={| p_point := {| x := 0; y := S b2 |}; val:= val2 \/
{| p_point := {| x := 0; y := 1) |};val := val3|} ={| p_point := {| x := 0; y := S b2 |};val := val2 \/ False

Goal:{| p_point := {| x := 1; y := 0) |};val := val3|} ={| p_point := {| x := x1; y := y1 |};val := val1 \/
{| p_point := {| x := 0; y := 1) |};val := val3 |} ={|p_point := {| x := x1; y := y1 |};val := val1

#### Pierre Castéran (Apr 04 2022 at 19:02):

I'm not sure your goal is provable: Let's take the assignment ` b2=0, y1=2, val1=val2=val3, x1=0`. It satisfies `H1`and `H2`, but not the conclusion.
But there are typos in your formulas, and all the declarations are missing , so I couldn't verify it formally and be sure it answers your question. I presume `H1`and `H2`come from hypotheses of the form `List.In ?p ?l`?

#### zohaze (Apr 05 2022 at 11:08):

List.In p. p is pixel. val1 val2 val3 are elements of data type val. x1 y1 b2 are nat. l is list of pixels.
I have used List . In p instead of List.Exists p ,because I am interested in position only (x,y).Therefore I have used List.In p l(list pixel). If i replace List.In p with List.Exists p .I get this error - The term "p" has type "pixel" while it is expected to have type "?A -> Prop". How I can remove this error and how i should write it?
To prove the above (asked) question , I want to use List.In p. (list pixel)

#### Pierre Castéran (Apr 05 2022 at 14:02):

If you want to formalize the predicate `Pr px l `: "the list `l` contains some pixel which has the same coordinates as `px`", you may either use `List.In` or `List.Exists`.
Your error comes from the type of `List.Exists`. Its first explicit argument should be a predicate (here of type `pixel->Prop`) and not a pixel.

``````Require Import List.
Import ListNotations.

Record point : Set := P {x: nat; y: nat}.
Record pixel : Set := Px {position: point; value: nat}.

(* solution with List.In and List.map *)
Definition Pr (px: pixel) (l : list pixel):=
In (position px) (map position l).

Goal Pr  (Px (P 3 4) 12) [Px (P 1 2) 10; Px (P 3 4) 4].
right. left. reflexivity. Qed.

(* solution with List.Exists and an equivalence predicate *)
Definition px_equiv (px1 px2:pixel):Prop := position px1 = position px2.

Definition Pr' (px: pixel) (l : list pixel) :=
Exists (px_equiv px) l.

Goal Pr'  (Px (P 3 4) 12) [Px (P 1 2) 10; Px (P 3 4) 4].
right. left. reflexivity. Qed.
``````

#### zohaze (Apr 08 2022 at 12:27):

Thank you for your reply. I am not too much expert in Coq,therefore it is difficult for me to understand your above given answer.
By considering question (4 Apr) give some suggestion to solve above. I have destruct x1 and y1 to simplify.

H1: {| p_point := {| x := 1; y := S b2 |}; val := val2|} = {| p_point := {| x := S x1; y := S y1 |}; val := val1}
H2 :{|p_point := {| x := 1; y := 0) |}; val := val3|} = {| p_point := {| x := 0; y := S b2 |}; val:= val2 \/
{| p_point := {| x := 0; y := 1) |};val := val3|} = {| p_point := {| x := 0; y := S b2 |};val := val2 \/ False
Goal:{| p_point := {| x := 1; y := 0) |};val := val3|} = {| p_point := {| x := S x1; y := S y1 |};val := val1}
It should be solve by discriminate .Because S b2= S y1 in H .But in goal 0= S y1. But this command is not helpful ,why?

#### Pierre Castéran (Apr 08 2022 at 13:25):

You cannot solve your goal, which would imply `0 = S y1`. Please note that your hypotheses are not contradictory, thus you cannot even solve this goal by contradiction (for instance, they are satisfied by the assignment `x1=b2=y1=0`and `val1=val2=val3`). The tactic `discriminate`is useful for solving goals like `0 <> S b2`(and a few other uses in hypotheses) but you tried to use it on a goal `0 = S b2`.

#### zohaze (Apr 08 2022 at 18:11):

It means by contradiction I cannot solve the goal. Without contra there is no way to solve the goal? I have solved few sub goal statements by directly applying hypothesis or by contra. But struck here because both are not applicable here. What you suggest how to come out ? By inversion H1 & H2 i can derive value of b x1 & y1 then by rewrite these values ,i can solve the goal/ it may be helpful?

#### Pierre Castéran (Apr 08 2022 at 19:19):

From `H1`(using `injection`), you have `x1=0`, `y1=b2`and `val1=val2`. From `H2`: `b2=0`and `val2=val3`. Then, by rewriting, your goal becomes `{| p_point := {| x := 1; y := 0) |};val := val3|} = {| p_point := {| x := 1;y := 1|};val := val3}`.

#### zohaze (Apr 09 2022 at 16:14):

You have separately defined point then use its definition in pixel. But I have defined pixel inductively as pixel (x y: nat) (val:values). Now I am writing it in below form (suggested by you).But compiler does not know about x & y
Definition Pr (px: pixel) (l : list pixel):= In ((pixel x y) px) (map (pixel x y) l, instead of Definition Pr (px: pixel) (l : list pixel):=
In (position px) (map position l). How I can remove this?

#### Pierre Castéran (Apr 09 2022 at 16:51):

If you don't want to consider two types `point`and `pixel`, you may write instead:

``````Record pixel := P{x:nat; y:nat; val: nat}.
Definition coordinates (p:pixel):= (x p, y p).
Definition Pr  px l =>  In (coordinates px) (map coordinates l).
``````

Note that, if `p`is bound to a pixel, its coordinates are `x p`and `y p`; `x`and `y` are selectors, i.e. functions of type `pixel -> nat`.

#### zohaze (Apr 09 2022 at 17:02):

After rewriting goal become {| p_point := {| x := 1; y := 0) |};val := val3|} = {| p_point := {| x := 1;y := 1|};val := val3}. (today 12:19)
I am asking above form of goal can be solve by H1 or H2? I need some contra statement to solve the goal but from where it come?

#### Pierre Castéran (Apr 09 2022 at 18:18):

Your hypotheses are not contradictory, and if you could solve your goal, you would infer 0=1. Perhaps your initial lemma statement was wrong.

It's difficult for us to answer questions about goals if we cannot replay a (possibly small) script which includes library requirements, definitions and the problematic goal. If the situation is described with imprecision, or if the sent script results in errors when compiled, it's almost impossible to help you. The best is to send a small as possible snippet (delimited by triple backquotes).

#### zohaze (Apr 10 2022 at 11:07):

Ok. Yesterday ,you have suggested combine form . When run it then have following

``````Record pixel := P{x:nat; y:nat; val: nat}.
Definition coordinates (p:pixel):= (x p, y p).
Definition Pr  px l =>  In (coordinates px) (map coordinates l).
``````

error "Syntax error: ':=' or ':' expected after [binders] (in [def_body]). "

2)

`````` Inductive pixel: Type :=  | PIXEL (x y: nat) (val: value).
Definition coordinates (p:pixel):= (x p, y p).
``````

3)When define in the following way, then 1&2 statements are accepted by compiler ,but 3rd one has following error

``````Inductive pixel := P{x:nat; y:nat; val: value}.
Definition coordinates (p:pixel):= (x p, y p).
Definition Pr  px l =>   In (coordinates px) (map coordinates l).
``````

error "Syntax error: ':=' or ':' expected after [binders] (in [def_body])."

#### Pierre Castéran (Apr 10 2022 at 11:22):

Sorry for the typo :oh_no: please replace `=>`with `:=`in `Pr`'s definition.

#### zohaze (Apr 12 2022 at 17:02):

Thanks it works. Last question what is the difference between two statements
1) Inductive pixel: Type := | PIXEL (x y: nat) (val: value).
2) Inductive pixel := P{x:nat; y:nat; val: value}.
2 is working but 1 is not working. If i want to write / use 1 statement then what I have to do? (don't want to use P in definition
of pixel and separately define coordinates )

#### Pierre Castéran (Apr 12 2022 at 17:42):

With the first definition, you have to define your selectors (which I call `getX`, etc. for instance). `x`, `y`and `val`are just variables.

``````Definition value:= nat.
Inductive pixel: Type := | PIXEL (x y: nat) (val: value).

Definition getX p:= match p with PIXEL x _ _ => x end.

Compute getX (PIXEL 3 0 42).
``````

In your second definition `x`, `y`, and `val` are interpreted as selectors
You may prefer the `Record` command:

``````Record pixel: Type :=
PIXEL { x : nat; y : nat; val: value}.

Compute x  (PIXEL 3 0 42).
``````

#### zohaze (Apr 13 2022 at 07:01):

Because of no contra statement in hypothesis, I am unable to solve the goal statement. Now, I have. But still discriminate does not work. What could be the reason?

``````H1:  PX (P 2 0) val2 = PX (P x1 y1) val1
H2:  PX (P 1 0) val3 = PX (P x2 y2) val2
goal: PX (P 1 0) val2 = PX (P x1 y1) val1
``````

#### Pierre Castéran (Apr 13 2022 at 09:04):

Just try to use `injection` as follows. `injection H1; intros; subst. `
Then, your goal is impossible to solve, because it would imply `1=2`.

#### pianke (Apr 24 2022 at 11:29):

``````H1:  In (PX (P 0 3) val1)   [(PX (P 9 5) val2) ; (PX (P 0 3) val2)]
goal: In (PX (P 0 3) val2)  [(PX (P 9 5) val1) ; (PX (P 0 3) val1)]
``````

I also want to ignore values , just consider coordinates.But how to convert H1 and goal statement so that I can solve the
goal statement by apply Pr, px-eq definitions (suggested by you).

#### Pierre Castéran (Apr 24 2022 at 16:34):

If you want to ignore values, you may use the following definitions:

``````Require Import Arith List Bool.
Import ListNotations.

Record point : Set := P{point_x: nat; point_y: nat}.
Record pixel : Set := PX{coord: point; px_val: nat}.

Definition PX_equiv p1 p2 := coord p1 = coord p2.

Definition In_coord (px: pixel) (pxs : list pixel) :=
In (coord px) (map coord pxs).

(* another equivalent definition *)
Definition In_coord'  (px: pixel) (pxs : list pixel):=
Exists (PX_equiv px) pxs.

Parameters val1 val2: nat.
Goal In_coord (PX (P 0 3) val2)  [(PX (P 9 5) val1) ; (PX (P 0 3) val1)].
right; now left.
Qed.

Goal In_coord' (PX (P 0 3) val2)  [(PX (P 9 5) val1) ; (PX (P 0 3) val1)].
right; now left.
Qed.
``````

Note that in your message, the hypothesis `H1` implies `val1= val2`, which allows you to solve your goal.
Also, there were missing characters in your hypothesis and goal. Please send us questions about goals which we can directly replay on our computers, without having to guess the used libraries, your definitions and initial goals. For instance, a small and error-free copy-pasted script (between triple backquotes).

#### pianke (Apr 26 2022 at 12:36):

First ,thanks. I have defined Px_equiv and In_coord (after your reply). Problem is that you are one step ahead.

``````H1:  In (PX (P 0 3) val1)   [(PX (P 9 5) val2) ; (PX (P 0 3) val2)]
goal: In (PX (P 0 3) val2)  [(PX (P 9 5) val1) ; (PX (P 0 3) val1)]
``````

Currently I have above definitions . These definitions have no relation with my existing goal and hypothesis. I still have In, pixel and list of pixel. In your given example you have used

``````Goal In_coord (PX (P 0 3) val2)  [(PX (P 9 5) val1) ; (PX (P 0 3) val1)].
``````

I am asking how to convert "In" to "In_coord (first). I have both things but in seperate form. How I convert my H and goal so that it match with your Goal's statement.( form ).

#### Pierre Castéran (Apr 26 2022 at 15:20):

Otherwise, we have to guess them, and perhaps give you a useless answer.

Your goal is solvable, because `H1`implies `val1=val2`. But I'm not sure whence this goal (and `H1`) comes from.

``````Hypothesis H1: In (PX (P 0 3) val1)   [(PX (P 9 5) val2) ; (PX (P 0 3) val2)].

Goal In (PX (P 0 3) val2)  [(PX (P 9 5) val1) ; (PX (P 0 3) val1)].
assert (H: val1= val2).
{ case H1.
- injection 1; discriminate.
-  destruct 1 as [H0 | H0].
+ injection H0; auto.
+  destruct H0.
}
rewrite H; right; now left.
Qed.
``````

#### pianke (May 26 2022 at 14:25):

H1: {| px_point := {| x := 0; y := 0 |}; val := 77 |} = {| px_point := {| x := 0; y := 0 |};val := 77 |} \/ False
goal: {| px_point := {| x := 0; y := 3 |}; val := 77 |} = {|px_point := {| x := 0; y := 0 |};val := 77 |}\/
*| px_point := {| x :=1; y := 3 |}; val := 77 |} = {|px_point := {| x := 3; y := 0 |};val := 77 |}
| px_point := {| x :=1 0; y := 37 |}; val := 77 |} = {|px_point := {| x := 10; y := 37 |};val := 77 |}

I have multiple equality statements .In above there are three case.To reach to particular case I write right.right.left.then apply reflexivity. In some case where no of terms are greater i write right.right.... left.Its working
but not looking smart and good. Is there any alternate command which would be very compact?

#### sara lee (Aug 25 2022 at 18:07):

In case , point does not exist in the list (like below). Then how i can prove it is false.

``````H1: In (mkpoint 1 0)   [mkpoint 2 0 ; mkpoint 5 8; mkpoint 1 9 ; mkpoint 3 6].
Goal:False
``````

#### Mukesh Tiwari (Aug 26 2022 at 10:20):

@sara lee 'simpl in H1' should do the job. Since the point you are search in not in the list, it should evaluate to False, and that's what your goal is but from from False you can prove anything.

(deleted)

(deleted)

#### sara lee (Sep 09 2022 at 17:38):

``````H1: (PX (P 0 (S a1)) val2) = (PX (P 0 (S b)) val2)
H2: (PX (P 0 a1) val2) = (PX (P 0 (S b)) val2)-> a1 = S b ->  S b <= 0
``````

Above is false because Succ(b)<=0. How i can prove it false or both statements are contra statements?

#### Pierre Castéran (Sep 09 2022 at 19:01):

No. From `H1`you get `a1=b`. If you replace `a1` with `b`in `H2`, `H2` becomes trivially provable (hence useless as a hypothesis).
From your context, you can just infer `a1=b`.

#### sara lee (Sep 10 2022 at 04:21):

From H1, a1=b . By using a1 in H2 i will get b=S b. Number & its succ both are equal,is it not false?

#### abab9579 (Sep 10 2022 at 04:50):

Think it will rather become
`... -> b = S b -> S b <= 0`.
This is tautology because the assumption is wrong.

#### zohaze (Sep 10 2022 at 05:09):

You are saying H1 is correct and due to wrong assumption H2 is not correct and its presence is useless. But how to come out from above situation (in the presence of H & H2)

#### sara lee (Sep 10 2022 at 05:17):

Remove H1 in this case?

#### Pierre Castéran (Sep 10 2022 at 05:34):

It depends on which theorem you want to prove, and which tactics you called since the beginning of the interactive proof. This information is missing from your posts.

#### sara lee (Sep 10 2022 at 07:51):

Simply i want to prove equality of two points,under H1 & H

``````H1: mkpoint 0 a = mkpoint 0 (S b).
H: b<=x.
Goal: (S b) <= x.
``````

To prove above which information i should add?( Plz explain). Currently, i am using commanad (repeat ((left; reflexivity) || right).)
I have no idea why this situation has occured and how to remove it .What is the missing information that will help me in coming out.

#### Mukesh Tiwari (Sep 11 2022 at 09:25):

@sara lee It's not provable. Assume `b = 0` and `x = 0`, so `H : b <= x` (0 <= 0) holds, but it's not the case that `S b <= x` (1 <= 0).

#### pianke (Jan 27 2023 at 04:05):

I have list of points PX and notation of point is (P x y val). I am passing PX as argument to function and adding 2 to its coordinates like (P x+2 y val) .But during recursive call function require PX not (P x+2 y val).How to adjust it? Is it possible to assign input argument PX a return value in the form of (P x y val)

#### Mukesh Tiwari (Jan 27 2023 at 18:17):

@pianke Can you post some working code? It’s very difficult to understand the what are you after without looking at some code snippet.

#### pianke (Jan 31 2023 at 04:13):

I have list Some [P(x1 y1 val1), P(x2 y2 val)....P(xn yn valn). Want to check equality of x1 and x2 . In case of equality get false
else give increment of 2 in both x1 & x2 then compare x2 &x3 ....
First i have removed Some from list then matched first and second element of list .But don't know how to give increment in recursive call.Please guide me how to do it?

#### pianke (Jan 31 2023 at 15:30):

l= Some [P(2 1 37), P(4 2 37)....P(10 9 37) generated by list_out(c l) .

``````Definition remov-option (def : list point) (o : pointoption) : list point :=
match o with
| None => def
| Some x => x
end.
``````

After applying above function i get [P(2 1 37), P(4 2 37)....P(10 9 37).

``````Fixpoint incrs_x( c:point )(l:list point):bool:=
match ( remov-option nil (list_out c l) with
nil =>true
| h::t=> match h with
| P(x y val) =>  if (0<?x) then incrs_x P(2+2 1 37) t else false
end
end.
``````

It shows an error message.

#### Mukesh Tiwari (Jan 31 2023 at 20:51):

In the if statement, x > 0 is Prop so try to find a Boolean equivalent of x > 0. I am typing this from my phone but try this: if (0 <? x ) then … else … and hopefully it should work.

#### Pierre Castéran (Jan 31 2023 at 22:05):

There is another issue.
In the evaluation of a term like `incrs_x c l`, the recursive call is `incrs_x c' t` where `t` depends on `(list_out c l)`.
We have no information about `list_out`. Does this function allow a definition of `incrs_x` by structural recursion ?
Or, could you prove that the length of `list_out c l`is less or equal than the length of `l`? In which case, a solution like in the https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/how.20to.20modify.20code thread would help.

#### pianke (Feb 01 2023 at 06:16):

Due to problem you have mentioned. I have modified code. I am adding 2 to x coordinate of each and every point of
l till it match with f.
Fixpoint incrs_x( c f:point )(l:list point):bool:=
match l with
nil =>false
| c::t=> false
| c::d::t=> match (c, d) with
| P(x1 y1 val),P(x2 y2 val) => if ((x1<? x2) then incrs_x P(x1+2 y1 val) f t else false
end
end.

#### Pierre Castéran (Feb 01 2023 at 07:07):

This definition of `incrs_x`contains several errors (syntax, type). Was this function really defined and tested with Coq before posting it ?
Please note that, even if we correct these errors, some issues remain:

• the role of `f` is not clear (unused in the code)
• What is the role of the constant `37`?
• If we look at the base cases, we infer that this function simply returns `false`. It has the same effect as if you had defined:
``````  Definition incrs_x  (c f:point )(l:list point):bool := false.
``````

Looks like you need to define a recursive function which builds and returns a list (instead of a boolean), and test your function (with `Compute`). Looking at Coq's`List`library and functions like `map` and `filter`may help you.

#### pianke (Feb 01 2023 at 16:37):

No,i directly type here. Next time i will copy from editor and run before copy.
1) 37 means any constant value (i have corrected above)
2) [] => true (i have corrected above)

(deleted)

#### pianke (Feb 05 2023 at 07:34):

I have list of coordinates and each coordinate is represented as |x0,y0| . I am defining list as
Definition mylist (n : nat) (l: list cordinate):= [|x1,y1|; |x2,y2|; |x3,y3| ...|xn,yn|].
How i can solve it? I want to define in terms of |x,y| .

#### pianke (Feb 07 2023 at 14:56):

when i defined list from these points then there is no issue |2,3| , |3,6|, |6,3| ,|4,2|
But when i make list from these points |x1,y1| , |x2,y2|, |x3,y3| ,|xn,yn| (In term of variables) , then there is error message
How i can solve it? I want to define in terms of |x,y| . Is it possible?

#### zohaze (Feb 18 2023 at 08:39):

I am defining a list on following basis (for time being i am not considering third co-ordinate of point).
Used notation from previous post: = (PX (P 0 3) val1) . I have simplified it as P |0 3|

``````Definition f  (pt: point)  : list point :=
match pt with
|P |x y| =>
match x y with
| 0,0=> [P|0 1|]
|0,y=> [P|0 y+2|, P|0 y+3|, P|0 y+4|]
|x,0=> [P|x+2 0|, P|x+3 0|, P|x+4 0|]
|_,_ => [P|x+3 y+3|, P|x+4 y+4|, P|x+5 y+5|]
end.
``````

For example
maylist1:= [ P|0 0|, P|0 1|,P|0 2|,P|0 4|,P|0 6|,P|3 0|,P|5 0|,P|3 3|,P|7 7|].

1) Want to confirm maylist1 contains points itself and any other point from its allocated list of points
e.g |0,y=> [P|0 y+2|, P|0 y+3|, P|0 y+4|]
0 2 [0 4]

#### Pierre Castéran (Feb 18 2023 at 10:00):

Your function `f`doesn't use its argument `l`.

The snippet you posted causes syntax errors. Perhaps you required some library with notations like in your definitions ?
In which case, could you post a correct and complete enough code (including notations, definitions and `Require`statements ) ?

(deleted)

#### Pierre Castéran (Feb 20 2023 at 07:35):

Do you mean: "given two lists of points `l`and `l'`, check whether each element of `l'` is in the image by `f`of some element of `l`?

As a predicate:

``````Definition P (l l': list point) : Prop :=
Forall (fun p' => Exists (fun p => In p' (f p)) l) l'.
``````

As a boolean function:
Let's assume you defined the function `point_in : point -> list point -> bool.`

``````Definition p_bool (l l': list point) : bool :=
forallb (fun p' => existsb (fun p => point_in p' (f p)) l) l'.
``````

#### zohaze (May 11 2023 at 12:41):

In hypothesis i have
In P | 0, 2, val1| l .
I want to write the val exist in list l at x=0 & y=2 is val1 . This existing val is equal to P | 0, 2, val1|.

#### zohaze (May 11 2023 at 12:43):

In hypothesis i have
In P | 0, 2, val1| l .
I want to write the val exist in list l at x=0 & y=2 is val1 . This existing val is equal to P | 0, 2, val1|.

Last updated: Sep 26 2023 at 13:01 UTC