Coq 中的函数答案

【问题标题】：functions in CoqCoq 中的函数
【发布时间】：2012-06-08 13:34:37
【问题描述】：

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

 // 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 中解决此类问题的材料的参考。

谢谢，

维拉亚特

【问题讨论】：

这个问题，特别是考虑到你用大量的 Java 编写，看起来非常误导。也许你应该在尝试这样做之前重新审视使用 Coq 的基础知识。但是，您应该注意到 Coq 确实已经支持（或至少在标准库中）处理子集。

标签： string function coq definitions

【解决方案1】：

Coq 在其标准库中有 strings 和 sets。

您的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)

我找不到标准库中定义的字符串的顺序。也许有一些。否则......好吧，就去做（也许贡献它）。

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

祝你好运。

【讨论】：