CODEWITHSUNDEEP
coq
Robert
Robert

Reputation: 31

How can I match on a specific value in Coq?

I'm trying to implement a function that simply counts the number of occurrences of some nat in a bag (just a synonym for a list).

This is what I want to do, but it doesn't work:

Require Import Coq.Lists.List.
Import ListNotations.

Definition bag := list nat.

Fixpoint count (v:nat) (s:bag) : nat :=
  match s with
  | nil    => O
  | v :: t => S (count v t) 
  | _ :: t => count v t
  end.

Coq says that the final clause is redundant, i.e., it just treats v as a name for the head instead of the specific v that is passed to the call of count. Is there any way to pattern match on values passed as function arguments? If not, how should I instead write the function?

I got this to work:

Fixpoint count (v:nat) (s:bag) : nat :=
match s with
| nil    => O
| h :: t => if (beq_nat v h) then S (count v t) else count v t
end.

But I don't like it. I'd rather pattern match if possible.

Upvotes: 3

Views: 958

Answers (3)

Eduardo Pascual Aseff
Eduardo Pascual Aseff

Reputation: 1166

Well, as v doesn't work in the match, I thought that maybe I could ask whether the head of the list was equal to v. And yes, it worked. This is the code:

Fixpoint count (v : nat) (s : bag) : nat :=
  match s with
  |  nil => 0
  |  x :: t => 
    match x =? v with 
    | true => S ( count v t )
    | false => count v t
    end
  end.

Upvotes: 1

Konrad Lorenz
Konrad Lorenz

Reputation: 1

I found in another exercise that it's OK to open up a match clause on the output of a function. In that case, it was "evenb" from "Basics". In this case, try "eqb".

Upvotes: 0

ejgallego
ejgallego

Reputation: 6852

Pattern matching is a different construction from equality, meant to discriminate data encoded in form of "inductives", as standard in functional programming.

In particular, pattern matching falls short in many cases, such as when you need potentially infinite patterns.

That being said, a more sensible type for count is the one available in the math-comp library:

count : forall T : Type, pred T -> seq T -> nat
Fixpoint count s := if s is x :: s' then a x + count s' else 0.

You can then build your function as count (pred1 x) where pred1 : forall T : eqType, T -> pred T , that is to say, the unary equality predicate for a fixed element of a type with decidable (computable) equality; pred1 x y <-> x = y.

Upvotes: 4

Related Questions