pianke (Apr 09 2023 at 06:26): 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...
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.
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: Oct 13 2024 at 01:02 UTC