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

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.

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.

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

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

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

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

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

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?

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

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.

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

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

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

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

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

file) ?

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

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

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|}

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

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?

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

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.

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.

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

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

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.

.

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

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

@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.
- admit. (* Here *)
- intro; subst.
admit. (* Here *)
Admitted.
<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.

I have modified my post.

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

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.

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

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

.

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.

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.

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?

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.

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)

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?

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.
destruct H, H'; try contradiction.
(*
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`

.

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.

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

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`

?

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)

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

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?

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`

.

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?

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

.

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?

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`

.

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?

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

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

error "The reference x was not found in the current environment."

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

Sorry for the typo :oh_no: please replace `=>`

with `:=`

in `Pr`

's definition.

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 )

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

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

Just try to use `injection`

as follows. `injection H1; intros; subst. `

Then, your goal is impossible to solve, because it would imply `1=2`

.

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

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

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

Please post a snippet with all your definitions and goal, so we could replay your example.

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

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?

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

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

Sorry for typing error.

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

In this situation what general statement i should have ? How i should proceed?

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

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

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?

Think it will rather become

`... -> b = S b -> S b <= 0`

.

This is tautology because the *assumption* is wrong.

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)

Remove H1 in this case?

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.

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 occur and how to remove it .What is the missing information that will help me in coming out.

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

I have list of points and notation of point is PX (P x y) val). I am adding 3 in x and y co-ordinates of each point recursively.Only problem is that i am passing Px as argument to function then by using its notations, i am adding 2 to its coordinates like Px(P x+2 y+2) .But during recursive call function require Px not Px(P x+2 y+2).How to adjust it?

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

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?

l= Some [P(2 1 37), P(4 2 37)....P(10 9 37).

```
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 l) with
nil =>true
| h::t=> match h with
| P(x y val) => if (x>0) then incrs_x P(2+2 1 37) t else false
end
end.
```

It shows an error message.

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.

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.

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 37) f t else false

end

end.

This definition of `incrs_x`

contains several errors (syntax, type). Was this function really defined and tested with Coq before posting this definition ?

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 computes
`false`

.

Looks like you need to define a recursive function which 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.

Last updated: Feb 01 2023 at 13:03 UTC