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