0

我必须证明一些正式的东西。有两个函数，获取一些字符串和字符串数组，比较是否匹配，并返回 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 并证明它，它应该为 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、Student这四个元素的类型应该是什么？

我很想获得帮助我在 Coq 中解决此类问题的材料的参考。

谢谢，

维拉亚特

4

1 回答 1

1

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

你function1真的只是一个包装器，当是空字符串mem时返回 true 。c你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 中定义的字符串的顺序。也许有一些。否则......好吧，就这样做（也许贡献它）。

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

祝你好运。

于 2012-06-11T12:42:56.710 回答