The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 11/08/2014 12:53 PM, Saulo Araujo wrote:
> Thanks a lot Jonathan! Your suggestion works like a charm! Could you help
> me with some other doubts?
>
> 1) I tried to use the notations [], [x], [x;y] and x :: y but had no luck.
> What kind of preamble (Require Import, Open Scope, etc.) do I have to use
> to be able to use these notations?

Require Import List.
Import ListNotations.

> 2) I tried to define a function that receives a list of classes and a class
> name and returns an option containing the class (if there is a class with
> the same name) like this:
>
> Definition getClass classes name := List.find
> (
>    fun class =>
>      match class with
>        | Class name' attributes => name = name'
>      end
> ) classes.
>
> but the compiler complains "The term "name = name'" has type "Prop" while
> it is expected to have type
>   "bool". I did some research and I believe I understood why. My next
> attempt was:
>
> Definition compareStrings x y := if prefix x y then prefix y x else false.
>
> Definition getClass classes name := List.find
> (
>    fun class =>
>      match class with
>        | Class name' attributes => compareStrings name name'
>      end
> ) classes.
>
> and the compiler is happy about it. My doubt is: is there a more idiomatic
> way to compare strings in Coq?

The term [name = name'] in Coq is not a comparison at all.  It's a type 
(actually, a Prop, which is a kind of Type).  That's probably rather 
confusing for programmers, but it's easy to get used to. It's the type 
of proofs that name is the same as name'.

A better definition of compareStrings would be:

Definition compareStrings x y := if string_dec x y then true else false.

> 3) In SML is possible to do pattern matching directly in the function
> parameters and val assignments. There are useful when the only thing you
> want is to extract the values inside another value. Is this possible in
> Coq? I tried this
>
> Definition getClass classes name := List.find
> (
>    fun (Class name' attributes) => compareStrings name name'
> ) classes.

The closest is to use a destructuring let:

Definition getClass classes name := List.find (fun c := let (name', _) 
:= c in compareStrings name name').

Alternatively, you could define a projection function on a class to get 
its name.  Or, use Record to define a class, which would automatically 
give you the projection functions.

> 4) Is it possible to define local functions in Coq? I am looking for
> something like let clauses in SML.

Yes - let can do that as well.  See ref manual section 1.2.12.

-- Jonathan