## Stream: Coq users

### Topic: patteren matching

#### pianke (Apr 09 2023 at 06:26):

``````match  l with
|  nil => false
| l' =>  if (eqb_nat a b) then true else
match(f3 a b l')  with
|  nil =>false
``````

In above (eqb_nat a b) is being applied on non empty case. Therefore it is applied on one element and more than one element.But i want to apply true case on single element and false case on two or more element. I introduced new matching pattern but get error message non exhaustive pattern matching.
I am modifying like this

``````match l with
| nil => false
| l' =>  match l' with
|[c]=>  if (eqb_nat a b) then true else
|c1::c2::t=> (eqb_nat a b)=false then
match(f3 a b l') with
| nil =>false...
``````

#### Laurent Théry (Apr 09 2023 at 07:38):

Here are two ways to check with pattern matching that a list has exactly two elements

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

Definition has_exactly_two_elements1 (l : list nat) :=
match l with
| nil => false (* zero element *)
| a :: nil => false  (* one element *)
| a :: b :: nil => true   (* exactly two *)
| a :: b :: c :: l  => false  (* at least three  *)
end.

Definition has_exactly_two_elements2 (l : list nat) :=
match l with
| nil => false (* zero element *)
| a :: l1 =>      (* at least one *)
match l1 with
| nil => false  (* one element *)
| b :: l2 => match l2 with   (* at least two  *)
|  nil => true  (* two elements *)
| c :: l3 => false (* at leas three *)
end
end
end.
``````

#### Laurent Théry (Apr 09 2023 at 08:02):

in your second match, Coq does not recall that `l'` is non-empty. You should write

``````match l with
| nil => false
| c1::  l' =>  match l' with
|nil =>  if (eqb_nat a b) then true else
|c2::t=> (eqb_nat a b)=false then
match(f3 a b l') with
``````

Last updated: Jun 20 2024 at 11:02 UTC