0

形式化されたものを証明する必要があります。2 つの関数があり、いくつかの文字列と文字列の配列を取得し、一致するかどうかを比較して、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.
{
...

}

両方の関数が true を返し、それを証明する場合に true になるはずの Coq の補題を述べたいと思います。お気に入り

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 の 4 つの要素の型は何ですか?

Coqでこのような問題を解決するのに役立つ資料への参照を取得したいと思います.

ありがとう、

ウィラヤット

4

1 に答える 1

1

Coqの標準ライブラリには文字列とセットがあります。

あなたfunction1は実際には単なるラッパーであり、が空の文字列のmem場合にtrueを返します。cあなたfunction2はまったく同じように見えますが、そもそもなぜ2番目の関数を書いたのかわかりません...これは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 に答える