The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

One man's random garbage is another's perfectly valid variable name.
Matej was, however, getting an error message, highlighting the extra
cases after the free variable.

> Error: this clause is redundant.

It's delicate to design languages with pattern-matching that never
behave confusingly. In OCaml, variables may not start with an
uppercase, precisely to avoid this problem. In some other languages,
variables are not patterns by themselves, you have to use some
explicit marker to turn a variable in a binder pattern. That's also
rather heavy.

On Sun, Aug 3, 2014 at 1:49 PM, Vladimir Voevodsky 
<vladimir AT ias.edu>
 wrote:
> 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
>