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

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

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.

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`

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

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

https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/list.20is.20empty.20or.20not

https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/constructor

- 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: Jun 24 2024 at 13:02 UTC