Transforming a inductive value into an inductive value of another type

0
votes

In database theory, one assumes the existence of two disjoint sets containing variables and constants.

I want to make the distinction between variables and constants at the type level of my values, using the two following inductive types:

Inductive variable :=
| var : string -> variable.
Inductive constant :=
| con : string -> constant.

I then would like to define a function mapping a variable to a constant using the same string internally.

I can reach this objective using the following definition:

Definition variable_to_constant : variable -> constant.
  intros.
  destruct H.
  apply (con s).
Defined.

Check test.
test
    : variable -> constant
Eval compute in (variable_to_constant (var "hello")).
    = con "hello"
    : constant

My question is: Is there a more elegant solution to define this function ? (I mean, not using the "Defined." keyword, maybe ...)

This is my first development using Coq, so if you think that my way of achieving this is wrong, please let me know :-)

Have a nice day !

Fabian Pijcke

1
coq

1 Answers

3
votes

You can simply write the code of the function directly rather than building it interactively using tactics:

Definition variable_to_constant : variable -> constant :=
  fun v => match v with var str => con str end.

Or even the lighter:

Definition variable_to_constant (v : variable) : constant :=
  match v with var str => con str end.