Coq的功能

Question

我必須證明一些正式的東西。有兩個函數，獲取一些字符串和字符串數組，比較是否匹配 並返回bool。我想在一個引理中對它們進行測試，並對其進行驗證。在編程中，函數將如下所示。

// 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. 
{ 
... 

} 

我想在Coq中聲明一個引理，如果兩個函數都返回true並證明它的話，這應該是真的。像

Lemma Test : function1 /\ function2. 

問題：

1）我怎麼能確定這些功能呢？這些不是歸納函數或遞歸函數（我認爲）。 他們應該像以下還是其他選項？

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

2）我該如何處理子集？就像我如何處理世界和歐洲的國家？請記住，我的要求是該函數得到一個名字和一個字符串數組。

3）這四個元素應該是什麼類型Countryname，World，Name，Students？

我很想得到一個材料的參考資料，幫助我在Coq中解決這些問題。

感謝，

Wilayat

Answer 1

勒柯克有strings和sets在其標準庫。

您的function1實際上只是一個圍繞mem的包裝，當c是空字符串時返回true。你function2似乎是完全一樣的，我不知道爲什麼你甚至在第一時間寫了第二個功能......這裏將是一個可能的勒柯克相當於：

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

你可以使用這些類型：

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) 

我找不到在stdlib中定義的字符串的順序。也許有一些。否則......就這樣做（也許有助於它）。

很明顯，可能有更好的方法來做到這一點。我不確定是否有更快/更髒的方式。也許有一個緩慢的實現，你只需要可判斷的平等。

祝你好運。