Pattern Matching and Matching Patterns: This clause is redundant.

I was following along Imp chapter of the Software Foundations textbook (found here at Benjamin Pierce’s webpage) and I got stuck pretty early on.  By follow along, I mean I was retyping everything in the chapter so that I could be an active participant in the “reading along process.”

Here’s what the chapter says to do:

 Inductive bexp : Type := 
  | BTrue : bexp
  | BFalse : bexp
  | BEq : aexp → aexp → bexp
  | BLe : aexp → aexp → bexp
  | BNot : bexp → bexp
  | BAnd : bexp → bexp → bexp.

Here’s what I wrote.

Inductive bexp : Type := 
  | BTrue : bexp
  | BFlase : bexp
  | BEq : aexp → aexp → bexp
  | BLe : aexp → aexp → bexp
  | BNot : bexp → bexp
  | BAnd : bexp → bexp → bexp.

Did you catch the difference? Well I didn’t, and neither did Coq, because frankly, it doesn’t care what you call your constructors – nor, should it.

Fast forward to the first time we tried to use the definition of bexp.

 Fixpoint beval (e : bexp) : bool :=
  match e with 
  | BTrue => true
  | BFalse => false
  | BEq a1 a2 => beq_nat (aeval a1) (aeval a2)   (* Error on this line*)
  | BLe a1 a2 => ble_nat (aeval a1) (aeval a2)
  | BNot b1 => negb (beval b1)
  | BAnd b1 b2 => andb (beval b1) (beval b2)
  end.

And we’re met with the supremely helpful message: Error: This clause is redundant.

Because the definition of bexp had a typo, there is no “BFalse” constructor. Instead, the BFlase in the pattern match of the defintion beval is a pattern match variable matching anything.  So between the BTrue case and the “everything else” case, all patterns are matched making anything below the seemingly correct “BFalse” redundant.

Yes, perhaps it was a careless typo that caused the problem, but a more descriptive error message would have been really helpful.  Having just run into this today, I don’t know if there exists some solution for catching this earlier, but here’s ideas I had.

  1. Warning mode: Warns when a “catch” all pattern is used. (Maybe only warns if the pattern is a variable instead of an underscore)
  2. Enhance the error message with “This clause is redundant because SomeOtherClause already caught this pattern.”

Compile that Buffer

I’ve just started using Coq, a proof assistant, – and a pretty cool one at that. But just like anything else, being new to Coq means I run into some silly problems sometimes (read: often). I’ll post those issues here in the hopes that some other newbie comes across it and doesn’t make my mistakes.

Here’s my setup at the moment:

  • OSX 10.7.5
  • CoqIde version 8.4

If you “Require Export Somelibrary” and you get this error, you may need to compile Somelibrary.

Error: Cannot find library Somelibrary in loadpath

Open Somelibrary into CoqIde and click Compile -> Compile Buffer.