Stream: Coq users

Topic: list of points


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

view this post on Zulip Pierre Castéran (Jan 18 2022 at 19:45):

The Inpredicate 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.

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

view this post on Zulip Pierre Castéran (Jan 19 2022 at 15:59):

In is defined in terms of equality, orand False (look at the answer to the Computecommand).
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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

view this post on Zulip Pierre Castéran (Jan 27 2022 at 18:21):

Indeed, the trybefore discriminatewas useless. The tactic I wrote can be used only for proving that some xis not in a given list, by proving xis 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 la 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].

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

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

Please note that the In x l proposition means "x is equal to some element of l".
If lis 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.

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

view this post on Zulip 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 discriminateworks.
injection without any arguments works also, but discriminateis more direct.

If your goal is Px (P 2 0) val = Px (P 2 0) val, reflexivityis 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.

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

view this post on Zulip 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 discriminateyou can easily prove its negation (with <>instead of =).

In which context p, p' and b1are 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).

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

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

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

view this post on Zulip 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 admitand/or Admittedor Abortwhere 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.

view this post on Zulip pianke (Jan 31 2022 at 17:20):

I have modified my post.

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

view this post on Zulip Pierre Castéran (Feb 02 2022 at 08:30):

Your goal should not be closed, because your pixels are indeed different (because of the ycoordinate).
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.

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

view this post on Zulip Pierre Castéran (Feb 04 2022 at 18:00):

Hi,
If you want to use In_pxin various situations, the best is to write your definition of In_pxat 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)).

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

view this post on Zulip Pierre Castéran (Feb 05 2022 at 08:10):

You don't tell us what are aand f1. Previously declared variables of respective type pixeland 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 Definitionor locally with pose), you define it for any pixel pxand 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 pxand pxsare just variables, which is not the case of your example.

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

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

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

view this post on Zulip pianke (Feb 06 2022 at 18:33):

(deleted)

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

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

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

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

view this post on Zulip 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 H1and 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 H1and H2come from hypotheses of the form List.In ?p ?l?

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

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

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

view this post on Zulip 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=0and val1=val2=val3). The tactic discriminateis 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.

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

view this post on Zulip Pierre Castéran (Apr 08 2022 at 19:19):

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

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

view this post on Zulip Pierre Castéran (Apr 09 2022 at 16:51):

If you don't want to consider two types pointand 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 pis bound to a pixel, its coordinates are x pand y p; xand y are selectors, i.e. functions of type pixel -> nat.

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

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

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

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

view this post on Zulip Pierre Castéran (Apr 10 2022 at 11:22):

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

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

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

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

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

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

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

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

view this post on Zulip Pierre Castéran (Apr 26 2022 at 15:20):

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

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

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

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

view this post on Zulip Pierre Castéran (Aug 26 2022 at 10:22):

(deleted)

view this post on Zulip sara lee (Aug 27 2022 at 03:30):

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?

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

view this post on Zulip Pierre Castéran (Sep 09 2022 at 19:01):

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

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

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

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

view this post on Zulip sara lee (Sep 10 2022 at 05:17):

Remove H1 in this case?

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

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

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

view this post on Zulip pianke (Jan 27 2023 at 04:05):

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?

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

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

view this post on Zulip pianke (Jan 31 2023 at 15:30):

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.

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

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

view this post on Zulip 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 37) f t else false
end
end.

view this post on Zulip Pierre Castéran (Feb 01 2023 at 07:07):

This definition of incrs_xcontains 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:

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'sListlibrary and functions like map and filtermay help you.


Last updated: Feb 01 2023 at 13:03 UTC