The Coq mailing list

[Saulo Araujo <saulo2 AT gmail.com>]

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?

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?

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.

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

hope I'm not abusing but I could not find the answers to these question in Google. Maybe Coq could benefit from some kind of porting guide from (a subset) of SML (or another functional language) to Coq...

Thanks a lot,

Saulo Medeiros de Araujo

On Sat, Nov 8, 2014 at 1:43 PM, Jonathan <jonikelee AT gmail.com> wrote:

On 11/08/2014 10:53 AM, saulo2 AT gmail.com wrote:

Hi,

I am trying to port a defitional interpreter for a small DSL from Standard ML
to Coq. The first problem I am facing is how to define self referential values
in Coq. Thats what I am trying to do:

Require Import String.
Open Scope string_scope.

Inductive OBJECT : Type := Object : CLASS -> list (string * OBJECT) -> OBJECT
      with CLASS : Type := Class : list (string * CLASS) -> CLASS.

Definition MediaType := Class nil.
Print MediaType.

Definition File := Class (cons ("mediaType", MediaType) nil).
Print File.

Definition User := Class (cons ("picture", File) nil).
Print User.

Definition Message := Class (cons ("sender", User) (
     cons ("recipients", User) (
       cons ("replies", Message) nil
     )
   )
).
Print Message.

but the Coq complier complains "Error: The reference Message was not found in
the current environment."

What you were trying to do with Message is define a self-referential (cyclic) data object, which Coq won't let you do (unless you use codata - but you probably don't want that).

You should probably put a level of indirection between a class's structural definition and its use.  I would suggest defining class tags first, then class structures that reference those tags.  Then define a mapping from class tags to class structures.

This might look something like:

Inductive CLASSTAG : Type := ClassTag : string -> CLASSTAG.

Inductive OBJECT : Type := Object : CLASS -> list (string * OBJECT) -> OBJECT
     with CLASS : Type := Class : list (string * CLASSTAG) -> CLASS.

...
Definition Message := Class (cons ("sender", ClassTag "User") (
    cons ("recipients", ClassTag "User") (
      cons ("replies", ClassTag "Message") nil
    )
  )
).
...
 Definition tag_to_class : CLASSTAG -> CLASS := ...


-- Jonathan