Как написать определения без аргументов в Coq? - PullRequest
Новая
       8

Как написать определения без аргументов в Coq?

2 голосов
/ 06 сентября 2010

У меня есть следующий индуктивный тип, определенный в Coq . 

Inductive natlist : Type :=
| nil : natlist
| cons : nat -> natlist -> natlist.

Notation "x :: l" := (cons x l) (at level 60, right associativity). 
Notation "[ ]" := nil.
Notation "[ x , .. , y ]" := (cons x .. (cons y  nil) ..).

Natlist - это в основном список натуральных чисел (аналогично спискам в Python).Я пытаюсь найти объединение двух натлистов, используя приведенное ниже определение.

Definition union_of_lists : natlist -> natlist -> natlist

т. Е. Eval simpl in (union_of_lists [1,2,3] [1,4,1]) должен вернуть [1,2,3,1,4,1]

У меня есть следующие сомнения:

  • Поскольку у этого определения нет аргументов, как я могу получить входные данные и обработать их?
  • Что означает определениеunion_of_lists возвращают точно?Это просто natlist?

Любая помощь или советы приветствуются.

1 Ответ

1 голос
/ 07 сентября 2010

Я нашел ответ сам :) Что я сделал, я написал отдельную функцию Fixpoint append, а затем присвоил ей определение union_of_lists. 

Fixpoint append(l1 l2 : natlist) : natlist :=
  match l1 with
  | nil => l2
  | (h :: t) => h :: app t l2
  end.`

, а затем 

Definition union_of_lists : natlist -> natlist -> natlist := append.

Eval simpl in (append [1,2,3] [1,2,3]) (* returns [1,2,3,1,2,3] *)

Определение union_of_lists возвращает функцию, которая принимает natlist в качестве аргумента и возвращает другую функцию типа natlist -> natlist (т.е. функция принимает аргумент natlist и возвращает natlist).

Это определение union_of_lists напоминает функции в Функциональное программирование , которые могут возвращать функцию или значение.

...