Использование функций в определениях

Question

Я моделирую программу, в которой пользователи могут выбирать из различных операторов и функций для написания запросов (то есть формул) для системы. Чтобы показать эти операторы, здесь я определил функции add и mul и использовал тип данных nat вместо функций и типов данных моей программы. Как я должен определить formula, что позволяет мне использовать его в определении compute_formula. Я немного застрял в решении этой проблемы. Спасибо.

Fixpoint add n m :=
  match n with
  | 0 => m
  | S p => S (p + m)
  end
where "n + m" := (add n m) : nat_scope.


Fixpoint mul n m :=
  match n with
  | 0 => 0
  | S p => m + p * m
  end
where "n * m" := (mul n m) : nat_scope.


Definition formula : Set :=
 nat-> nat -> ?operators_add_mull  ->formula.

Definition compute_formula (f: formula) : nat :=
 match f with
  |firstnumber,secondnumber, ?operators_add_mull => 
              ?operators_add_mull  firstnumber secondnumber

  end.

Answer 1

Во-первых, ваш синтаксис для определения типа данных не совсем верен: вам нужно использовать ключевое слово Inductive:

Inductive formula : Set :=
| Formula : nat -> nat -> ?operators_add_mul -> formula.

Осталось выяснить, какими должны быть аргументы для конструктора Formula. Тип функции Coq -> является типом, подобным любому другому, и мы можем использовать его в качестве третьего аргумента:

Inductive formula : Set :=
| Formula : nat -> nat -> (nat -> nat -> nat) -> formula.

После определения этого типа данных вы можете написать выражение типа Formula 3 5 add, которое обозначает добавление 3 и 5. Чтобы проверить тип данных формулы, вам нужно написать match с помощью конструктора Formula:

Definition compute_formula (f : formula) : nat :=
  match f with
  | Formula n m f => f n m
  end.