将归纳值转换为另一种类型的归纳值

Question

在数据库理论中，假设存在两个包含变量和常量的不相交集合。

我想在我的值的类型级别区分变量和常量，使用以下两种归纳类型：

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

然后我想定义一个函数，在内部使用相同的字符串将变量映射到常量。

我可以使用以下定义达到此 objective：

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

我的问题是：有没有更优雅的解决方案来定义这个函数？（我的意思是，不使用 "Defined." 关键字，也许...）

这是我第一次使用 Coq 进行开发，所以如果您认为我的实现方式有误，请告诉我:-)

祝你有愉快的一天！

法比安·派克

Answer 1

您可以直接编写函数的代码，而不是使用策略以交互方式构建它：

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

甚至打火机：

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

将归纳值转换为另一种类型的归纳值

Transforming a inductive value into an inductive value of another type

coq