Кодирование упорядоченных наборов - PullRequest
Новая
       4

Кодирование упорядоченных наборов

0 голосов
/ 03 ноября 2018

Что касается опыта программирования Coq, Я хотел бы знать, есть ли другие способы кодирования, вместо моего кодирования, отношения предварительного заказа для использования их при проверке функции неубывающей . В коде ниже я заменил типы данных и функции моей программы на простые. mydata - это набор с отношением предварительного заказа (т. Е. С рефлексивным и транзитивным отношением) и является диапазоном функции mappingFunction, которая отображает числа nat в mydata. Я не мог определить отношение предварительного заказа для mydata при теореме кодирования mappingFunction_isIncreasing, поэтому в качестве решения я сопоставил mydata с числами nat через dataparts_toNat, чтобы дать мне возможность определить отношение предварительного заказа между ними. Интересно, есть ли другие способы сделать эту программу, например, без dataparts_toNat. Спасибо. 

 (*defining the datatype*)
Inductive mydata : Set :=
  | part1 : mydata
  | part2 : mydata
  |part3 :mydata.

(* mapping to nats to have
        preorder relation(part1<part2<part3 and part1=part1 and part2=part2 and part3=part3)*)
Definition dataparts_toNat (n:mydata):nat :=
   match n with
          |part1 => 0
          |part2 => 1
          |part3 => 2
    end.

(* a sample function from nat to mydata which is always increasing or not changing*)
Definition mappingFunction
  (a1:nat): mydata :=
        match a1 with 
           |0=> part1
           |S(0) => part2
           |_ => part3
         end.    
Theorem mappingFunction_isIncreasing: forall(a1 a2: nat)(data1 data2: mydata),
   a1<=a2 -> (mappingFunction a1= data1 )/\(mappingFunction a2= 
data2) -> ((dataparts_toNat data1) <= dataparts_toNat(data2)).
Proof.

1 Ответ

0 голосов
/ 04 ноября 2018 
(* The definition of mydata again, for completeness *)
Inductive mydata : Set :=
| part1 : mydata
| part2 : mydata
| part3 : mydata.

Вы можете определить сравнение как логическую функцию mydata -> mydata -> bool: 

Definition le_mydata_dec (d1 d2 : mydata) : bool :=
  match d1, d2 with
  | part1, _ => true
  | part2, (part2 | part3) => true
  | part3, part3 => true
  | _, _ => false
  end.

И из этого получим отношение сравнения mydata -> mydata -> Prop (это только один способ, иногда удобнее определить le_mydata как Inductive предложение). 

Definition le_mydata (d1 d2 : mydata) : Prop :=
  le_mydata_dec d1 d2 = true.

Функция отображения такая же (переименована f для краткости): 

(* a sample function from nat to mydata which is always increasing or not changing*)
Definition f
  (a1:nat): mydata :=
        match a1 with 
           |0=> part1
           |S(0) => part2
           |_ => part3
         end.

Теперь это монотонность: 

Theorem f_isMonotonic: forall(a1 a2: nat),
   a1<=a2 -> le_mydata (f a1) (f a2).
Proof.
Abort.

Вы можете использовать нотации для замены le_mydata на более симпатичный <=. Здесь мы стараемся не скрывать ранее существовавшую нотацию <= для сравнения nat, назначая эту новую нотацию новой области действия mydata_scope, разделенной ключом mydata. 

Infix "<=" := le_mydata : mydata_scope.
Delimit Scope mydata_scope with mydata.
(* now we can write  (x <= y)%mydata  instead of  le_mydata x y *)

Снова теорема о монотонности, используя эти обозначения: 

Theorem f_isMonotonic: forall(a1 a2: nat),
   a1<=a2 -> (f a1 <= f a2)%mydata.
Proof.
Abort.
...