## Stream: Coq users

### Topic: constructor

#### pianke (Mar 03 2023 at 17:00):

``````Fixpoint check ( x y :nat)(l : list nat):bool :=
| nil => false
| x ::nil=> true
|a1::a2::t=> if.....then check a1 a2 t else false
``````

Out put bool value should be false when there exist one element. If i do that then it give false for all the cases because of recursive function. How i can solve it ,so that it gives false incase of one element not for the case where list goes to its end .

#### Laurent Théry (Mar 03 2023 at 18:35):

using 2 functions ?

``````Fixpoint check1 ( x y :nat)(l : list nat):bool :=
| nil => false
| x ::nil=> true
|a1::a2::t=> if.....then check1 a1 a2 t else false

Definition  check ( x y :nat)(l : list nat):bool :=
match l with
| nil => false
| x ::nil=> false
|_::_:: _ =>  check1 x y l
end
``````

#### pianke (Mar 04 2023 at 08:34):

Only problem in check1 is that it gives true in case of single element, but i want to have false in that case. If i replace second constructor with false then it give false in case of third constructor,when it reaches the end of list. As a result i get one correct statement at a time.

#### Laurent Théry (Mar 04 2023 at 09:56):

no `check1` returns true in the case of the recursion of a list of more than one element. `check`returns false in the case of a list of one element. The final function is `check` not `check1`

#### pianke (Mar 05 2023 at 06:32):

Ok, thank you. Problem of single element get solved. If multiple elements lie in the list then it works properly. Even when two elements left then it works. But when list have two elements it gives true but i need false here (in this situation only). When modify a1::a2::nil=> false then every thing goes wrong. May i bring this change at this particular point?

``````Fixpoint  check3 (x y  : nat)( l  : list nat) : bool :=
match  l   with
| nil => false
| [c] =>false
| a1::a2::nil=> true
| a1::((a2::t) as t2)  =>
if (.....)  check3 x y t2  else false
end.
``````

#### Pierre Castéran (Mar 05 2023 at 08:58):

You may use the pattern we discussed recently in the following conversations:

• Define a helper function which is OK for almost all lists (here lists of more than two elements)
• Then a main function which gives a correct result in particular cases (here lists of 0,1, or 2 elements) and calls the helper otherwise.
``````Fixpoint helper (p : nat -> nat -> bool) (l: list nat)
:= match l with
[] | [_] => true
| x::((y::l) as tl) => (p x y && helper p tl)
end.

Definition main p l :=
match l with
nil | [_ ] | [_ ;  _] => false
|  _ => helper p l
end.
Compute main (fun x y => Nat.eqb y (3 + x)) [5;8].
Compute main (fun x y => Nat.eqb y (3 + x)) [5;8;11].
``````

Last updated: Oct 04 2023 at 23:01 UTC