The Coq mailing list

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

> Definition nonsense ( x : un ) := match x with y => 0 end .
>
> Is this supposed to make sense?

This makes perfect sense.

> If so then what is "y" in the term "match x with y => 0 end "? Is it a 
> variable? Is it a free variable or a bound variable?

"y" is a variable in binding position. I would call
"bound variable" the uses under a binder; this is not a use but a
definition.


Some beginners find this awkward. In particular if you write:

  Definition y := 0.
  Definition awkward x := match x with y => true | _ => false.

They would expect the 'y' in a pattern to correspond to an equality
test to the existing 'y' variable, while it in fact is a binder that
catches all case (so the "| _" is an error). I've seen enough
beginners make this confusion to conclude that this syntax is maybe a
bit too clever for its own good, at least when the binder shadows an
existing variable. I know of no better alternative, though.

Furthermore, in a dependently typed language, the interpretation of
pattern-y as an equality test would be a dubious design choice,
because equality is not an easy notion.

On Sun, Aug 3, 2014 at 2:55 PM, Vladimir Voevodsky 
<vladimir AT ias.edu>
 wrote:
> Ok. Here is less complex code:
>
> Inductive un : Type :=  .
>
> Definition nonsense ( x : un ) := match x with y => 0 end .
>
> Is this supposed to make sense?
>
> If so then what is "y" in the term "match x with y => 0 end "? Is it a 
> variable? Is it a free variable or a bound variable?
>
> PS ... and if I write this:
>
> Definition nonsense ( x : un ) := match x with y + 2 => 0 end .
>
> I get this:
>
>> Toplevel input, characters 20-83:
>> Anomaly: Uncaught exception Not_found(_). Please report.
>
>
> (I am running trunk).
>
>
>
>
>
>
> On Aug 3, 2014, at 8:12 PM, Michel Levy 
> <michel.levy1948 AT gmail.com>
>  wrote:
>
>> On 03/08/2014 13:44, Cédric 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.
>>>
>>>
>> I confirm the diagnostic of Cédric : Feburary is a variable matching all
>> other cases.
>> A good way to verify this is to print the  definition of
>> month_with_even_number_of_days''' with
>> Print month_with_even_number_of_days'''.
>>
>> --
>> email : 
>> michel.levy1948 AT gmail.com
>> http://membres-liglab.imag.fr/michel.levy
>>
>