The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

What kind of syntax "match" has if placing random garbage in it does not 
generate an error message?

V.



On Aug 3, 2014, at 7:44 PM, Cédric 
<sedrikov AT gmail.com>
 wrote:

> 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

Attachment: signature.asc
Description: Message signed with OpenPGP using GPGMail