Dfyjkt

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.

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.