在定义中使用函数 [英] Using functions in definitions

问题描述

我正在建模一个程序，用户可以在其中选择不同的运算符和函数来为系统编写查询（即公式）。为了显示这些运算符，在这里我定义了 add 和 mul 函数并使用了nat数据类型，而不是程序的函数和数据类型。我应该如何定义 formula ，使我能够在定义 compute_formula 中使用它。我有点想解决这个问题。

I'm modeling a program in which users can choose from different operators and functions for writing queries (i.e. formulas) for the system. For showing these operators, here I defined add and mul functions and used nat datatype, instead of my program's functions and datatypes. How should I define formula that enables me to use it in definition compute_formula. I'm a bit stuck at solving this issue. Thank you.

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.

推荐答案

首先，用于定义数据类型的语法不是非常正确：您需要使用 Inductive 关键字：

First, your syntax for defining a data type is not quite right: you need to use the Inductive keyword:

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

仍有待弄清楚公式构造函数应该是。 Coq函数类型-> 与其他类型一样，我们可以将其用作第三个参数：

It remains to figure out what the arguments to the Formula constructor should be. The Coq function type -> is a type like any other, and we can use it as the third argument:

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

定义此数据类型后，可以编写类似于 Formula 3 5的表达式add ，表示3和5的加法。要检查公式数据类型，您需要使用 match >公式构造函数：

After defining this data type, you can write an expression like Formula 3 5 add, which denotes the addition of 3 and 5. To inspect the formula data type, you need to write match using the Formula constructor:

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

这篇关于在定义中使用函数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！