The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

Hi,

I would like to ask why if I introduce this definition:

  (* CoqArt, Section 6.1.1 (pg 138) *)

  Inductive month : Set :=
  | January : month   | February : month | March : month    | April : month
  | May : month       | June : month     | July : month     | August : month
  | September : month | October : month  | November : month | December : 
month.

and then I try to define a function in the following way:

  (* Exercise 6.5 (pg 144) *)

  Definition month_has_even_number_of_days'' (leap:bool) (m:month) :=
    match m with
    | January | March | May | July | August | October | December => false
    | Feburary => negb leap
    | April | June | September | November => true
    end.

then I am getting a complaint:

  Toplevel input, characters 227-270:
  >   | April | June | September | November => true
  >     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Despite me tring to do fairly simple thing, the output thoroughly surprised 
me.
Is the above response plausible? Why?

A complementary question: why does Coq admit this:

  Definition month_with_even_number_of_days''' (leap:bool) (m:month) :=
    match m with
    | January | March | May | July | August | October | December => false
    | Feburary => negb leap
    end.

instead of rejecting it due to cases that are not covered?

──────────────────────────────────────────────────────────────────────────────────

<SIDENOTE>

This:

  Definition month_has_even_number_of_days (leap:bool) (m:month) :=
    match m with
    | January => false
    | February => negb leap
    | March => false
    | April => true
    | May => false
    | June => true
    | July => false
    | August => false
    | September => true
    | October => false
    | November => true
    | December => false
    end.

as well as this:

  Definition month_has_even_number_of_days' (leap:bool) :=
    month_rec (fun _ => bool)
              false         (* January *)
              (negb leap)   (* February *)
              false         (* March *)
              true          (* April *)
              false         (* May *)
              true          (* June *)
              false         (* July *)
              false         (* August *)
              true          (* September *)
              false         (* October *)
              true          (* November *)
              false.        (* December *)

works as expected.

If I omit some case, Coq correctly identifies it and complains.
If I provide a superfluous case, Coq correctly identifies it and complains.

</SIDENOTE>