Coq中的函数

Question

我必须证明一些形式化的东西。有两个函数，获取一些字符串和字符串数组，比较是否有匹配， 并返回布尔值。我想在一个引理中测试它们，并验证它。在编程中，函数如下所示。

 // 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）这四个元素的国家名称，世界，名称，学生的类型应该是什么？

我很想得到一些材料参考，帮助我在Coq中解决此类问题。

谢谢

威拉亚特

Answer 1

Coq的标准库中有字符串和集合。

您的function1实际上只是mem的包装器，当c是空字符串时返回 true。你的function2似乎完全一样，我不确定你为什么一开始就写了第二个函数......这将是一个可能的Coq等价物：

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 中定义的字符串的顺序。也许有一些。否则。。。好吧，就去做（也许贡献它）。

显然，可能有更好的方法可以做到这一点。我不确定是否有更快/更脏的方法。也许有一个缓慢的集合实现，你只需要在某个地方实现可判定的相等。

祝你好运。