functions in Coq

Question

I have to prove some formalised stuff. There are two functions, gets some strings and array of strings, compare if there is a match, and returns bool. I want to test them both in a lemma, and verify it. In programming, the functions would be like the following.

 // Countryname is a country in the set (World) of all countries of the World.
 // Europe, is a subset of the set of all countries of the Wrold.

 function1 ( String Countryname, String[] Europe)   // function1() returns bool.
  {
    boolean result = false;

    if Countryname = = ' '
      result true;
    else 
       {
        for ( int i = 0; i < sizeof(Europe) ; i++) {
            if ( Countryname = = Europe[i] )
                          result true; 
                          break;
        }
       }

    return result1;
  }


 // function2() compares similarly getting a 'Name' of type string, and an array of 'Students' names. If name is empty, or it matchs a name 
    in the list of students, it should return true.


 function2 ()           // function2() returns bool.
{
...

}

I want to state a lemma in Coq which should be true if both functions return true and prove it. like

Lemma Test : function1 /\ function2.

Questions:

1) How can I define these functions? these are not inductive function or recursive functions (I think). should they be like the following or any other option?

Definition function1 ( c e : World ) : bool :=
 match c with 
 | empty => true                    // I dont know how to represent empty.
 | e => true
 end. 

2) How can I deal with subsets? Like how can I deal with set of countries World and Europe? Remember, my requirement is that the function gets a single name and an array of strings.

3) what should be the type of these four elements Countryname, World, Name, Students?

I would love to get a reference to materials helping me sovling such problems in Coq.

Thanks,

Wilayat

Answer 1

Coq has strings and sets in its standard library.

Your function1 is really just a wrapper around mem that returns true when c is the empty string. Your function2 seems to be exactly the same, I'm not sure why you even wrote a second function in the first place... Here would be a possible Coq equivalent:

Definition my_compare (s: string) (set: StringSet.t) :=
  (string_dec s "") || (StringSet.mem s set).

You could use these types:

Module StringOT <: OrderedType.
  Definition t := string.
  Definition eq := @eq t.
  Definition lt : t -> t -> Prop := (* TODO *).
  Definition eq_refl := @refl_equal t.
  Definition eq_sym := @sym_eq t.
  Definition eq_trans := @trans_eq t.
  Theorem lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
  Proof. (* TODO *) Admitted.
  Theorem lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
  Proof. (* TODO *) Admitted.
  Definition compare : forall x y : t, Compare lt eq x y := (* TODO *).
  Definition eq_dec := string_dec.
End StringOT.

Module StringSet := FSetAVL.Make(StringOT)

I couldn't find an order for strings defined in the stdlib. Maybe there's some. Otherwise... well just do it (and maybe contribute it).

Obviously there might be better ways to do it. I'm not sure whether there's a quicker/dirtier way though. Maybe there's a slow set implementation where you only need decidable equality somewhere.

Good luck.