CODEWITHSUNDEEP
coq
Charlie Parker
Charlie Parker

Reputation: 5247

How does one do an else statement in Coq's functional programming language?

I am trying to count the # of occurrences of an element v in a natlist/bag in Coq. I tried:

Fixpoint count (v:nat) (s:bag) : nat :=
  match s with
  | nil => 0
  | h :: tl => match h with
               | v => 1 + (count v tl)
               end
  end.

however my proof doesn't work:

Example test_count1:              count 1 [1;2;3;1;4;1] = 3.
Proof. simpl. reflexivity. Qed.

Why doesn't the first piece of code work? What is it doing when v isn't matched?

I also tried:

Fixpoint count (v:nat) (s:bag) : nat :=
  match s with
  | nil => 0
  | h :: tl => match h with
               | v => 1 + (count v tl)
               | _ => count v tl
               end
  end.

but that also gives an error in Coq and I can't even run it.

Functional programming is sort of new to me so I don't know how to actually express this in Coq. I really just want to say if h matches v then do a +1 and recurse else only recurse (i.e. add zero I guess).

Is there a simple way to express this in Coq's functional programming language?

The reason that I ask is because it feels to me that the match thing is very similar to an if else statement in "normal" Python programming. So either I am missing the point of functional programming or something. That is the main issue I am concerned I guess, implicitly.

Upvotes: 0

Views: 457

Answers (2)

SCappella
SCappella

Reputation: 10474

(this is similar to Daniel's answer, but I had already written most of it)

Your problem is that in this code:

match h with
| v => 1 + (count v tl)
end

matching with v binds a new variable v. To test if h is equal to v, you'll have to use some decision procedure for testing equality of natural numbers.

For example, you could use Nat.eqb, which takes two natural numbers and returns a bool indicating whether they're equal.

Require Import Nat.

Fixpoint count (v:nat) (s:bag) : nat :=
  match s with
  | nil => 0
  | h :: tl => if (eqb h v) then (1 + count v t1) else (count v t1)
  end.

Why can't we simply match on the term we want? Pattern matching always matches on constructors of the type. In this piece of code, the outer match statement matches with nil and h :: t1 (which is a notation for cons h t1 or something similar, depending on the precise definition of bag). In a match statement like

match n with
| 0 => (* something *)
| S n => (* something else *)
end.

we match on the constructors for nat: 0 and S _.

In your original code, you try to match on v, which isn't a constructor, so Coq simply binds a new variable and calls it v.

Upvotes: 2

Daniel Schepler
Daniel Schepler

Reputation: 3103

The match statement you tried to write actually just shadows the v variable with a new variable also called v which contains just a copy of h.

In order to test whether two natural numbers are equal, you can use Nat.eqb which returns a bool value which you can then match against:

Require Import Arith.

Fixpoint count (v:nat) (s:bag) : nat :=
  match s with
  | nil => 0
  | h :: tl => match Nat.eqb v h with
               | true => 1 + (count v tl)
               | false => count v tl
               end
  end.

As it happens, for matching of bool values with true or false, Coq also provides syntactic sugar in the form of a functional if/else construct (which is much like the ternary ?: operator from C or C++ if you're familiar with either of those):

Require Import Arith.

Fixpoint count (v:nat) (s:bag) : nat :=
  match s with
  | nil => 0
  | h :: tl => if Nat.eqb v h then
                 1 + (count v tl)
               else
                 count v tl
  end.

(Actually, it happens that if works with any inductive type with exactly two constructors: then the first constructor goes to the if branch and the second constructor goes to the else branch. However, the list type has nil as its first constructor and cons as its second constructor: so even though you could technically write an if statement taking in a list to test for emptiness or nonemptiness, it would end up reversed from the way you would probably expect it to work.)

In general, however, for a generic type there won't necessarily be a way to decide whether two members of that type are equal or not, as there was Nat.eqb in the case of nat. Therefore, if you wanted to write a generalization of count which could work for more general types, you would have to take in an argument specifying the equality decision procedure.

Upvotes: 2

Related Questions