Stream: Coq users

Topic: patteren matching


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

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

view this post on Zulip 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: Mar 29 2024 at 05:40 UTC