функции в Coq

Я должен доказать некоторые формализованные вещи. Есть две функции: получает несколько строк и массив строк, сравнивает, если есть совпадение, и возвращает 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, которая должна быть верной, если обе функции вернут истину и докажут это. как

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.

Спасибо,

Вилаят


string function coq definitions
person Khan    schedule 08.06.2012    source источник
comment
Этот вопрос, особенно с учетом того, что вы пишете большое количество Java, выглядит крайне ошибочным. Возможно, вам стоит пересмотреть основы использования Coq, прежде чем пытаться это сделать. Однако вы должны отметить, что Coq имеет поддержку (или, по крайней мере, в стандартной библиотеке) для работы с подмножествами.   -  person Kristopher Micinski    schedule 11.06.2012

Ответы (1)


arrow_upward
1
arrow_downward

Coq имеет строки и устанавливает в своей стандартной библиотеке.

Ваш function1 на самом деле просто оболочка вокруг mem, которая возвращает истину, когда 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. Может, есть какие-то. В противном случае ... просто сделайте это (и, возможно, внесите свой вклад).

Очевидно, есть способы сделать это лучше. Я не уверен, есть ли более быстрый / грязный способ. Может быть, есть реализация с медленным набором, где вам где-то нужно только разрешимое равенство.

Удачи.

person Ptival    schedule 11.06.2012