The Coq mailing list

[Cédric <sedrikov AT gmail.com>]

Le Sun, 03 Aug 2014 13:17:26 +0200, Matej Kosik  
<5764c029b688c1c0d24a2e97cd764f AT gmail.com> a écrit:

> 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?

Probably because you mistyped "February" in "Feburary", thus "Feburary" is  
considered as a variable matching all other cases. Then April, June,  
September and November are considered already treated by "Feburary"

> 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?

Because you continue to mistype February, and it is considered a variable  
matching all other cases.

> ──────────────────────────────────────────────────────────────────────────────────
>
> <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>


--
---
Cédric AUGER