將電感值轉換爲另一種類型的電感值

Question

在數據庫理論中，假設存在兩個含有變量和常量的不相交集合。

我要讓變量和常量的區別在我的值類型級別，使用以下兩種歸納類型：

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

然後我想定義一個函數變量映射到一個常數內部使用相同的字符串。

我可以使用下面的定義達成這一目標：

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進行開發，所以如果你認爲我的方法是錯誤的，請告訴我:-)

祝您有美好的一天！

的Fabian Pijcke

Answer 1

你可以簡單地寫函數的代碼，而不是直接構建它以交互方式使用戰術：

​​

甚至打火機：

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