CODEWITHSUNDEEP
coq
Tom And.
Tom And.

Reputation: 125

Using functions in definitions

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.

Upvotes: 1

Views: 166

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23592

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.

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.

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.

Upvotes: 1

Related Questions