格局Coq的單個子句中匹配多個構造

Question

假設我有感應型算術表達式exp

Inductive exp : Type := 
| num : nat -> exp 
| plus : exp -> exp -> exp 
| minus : exp -> exp -> exp 
| mult : exp -> exp -> exp 
| div : exp -> exp -> exp. 

的，我想定義一個函數expsum返回發生在一個exp的所有數字的總和。最明顯的實現是

Fixpoint expsum (e : exp) : nat := 
match e with 
| num n => n 
| plus e1 e2 => expsum e1 + expsum e2 
| minus e1 e2 => expsum e1 + expsum e2 
| mult e1 e2 => expsum e1 + expsum e2 
| div e1 e2 => expsum e1 + expsum e2 
end. 

但對於構造plus，minus，mult，並div，expsum模式匹配後不完全一樣的東西。我想，這樣一個條款需要多個構造函數的照顧它簡化成類似

Fixpoint expsum (e : exp) : nat := 
match e with 
| num n => n 
| [ plus e1 e2 | minus e1 e2 | mult e1 e2 | div e1 e2 ] 
    => expsum e1 + expsum e2 
end. 

。我想我已經看到這在其他功能語言中完成。這可能在Coq中嗎？

Answer 1

這不能在術語語言中完成。 Coq的語言本身非常強大，這要歸功於它的依賴類型，但它不是它自己的元語言;沒有辦法編寫一個操作Coq構造函數的Coq術語（僅用於術語，並且不足以構建模式匹配）。

可能有一種方法可以用白話來做到這一點（用最高級的語言寫出術語的定義，用戰術語言中的證明等等），但我認爲不存在。如果它存在任何地方，我希望它在Program。但是將相同的模式應用於碰巧具有相同類型的構造函數是一個相當專業化的需求。

它可以用證明語言來完成。 Coq中的證明只是術語;有助於重複性證明的策略可以通過重複術語以相同的方式提供幫助。

Inductive exp : Type := 
| num : nat -> exp 
| plus : exp -> exp -> exp 
| minus : exp -> exp -> exp 
| mult : exp -> exp -> exp 
| div : exp -> exp -> exp. 

(* The boring old code *)  
Fixpoint expsum (e : exp) : nat := 
match e with 
| num n => n 
| plus e1 e2 => expsum e1 + expsum e2 
| minus e1 e2 => expsum e1 + expsum e2 
| mult e1 e2 => expsum e1 + expsum e2 
| div e1 e2 => expsum e1 + expsum e2 
end. 

Definition expsum_tactic : exp -> nat. 
    induction 1; 
    (* Figure out the computation automatically based on what arguments are present *) 
    exact n || exact (IHexp1 + IHexp2). 
Defined. (* "Defined" rather than "Qed" to get a transparent definition *) 

(* Show the two definitions in a nice way to visually compare them *) 
Print expsum. 
Eval compute [expsum expsum_tactic exp_rec] in (expsum, expsum_tactic). 

這可以通過使用match goal戰術結構分析每一個構造函數的參數，並相應建立了長期的結果可以推廣到可變參數數量。

雖然這可行，但它很棘手。戰術是針對寫作證明的，其中計算內容是無關緊要的。當你用它們來寫出其實際定義很重要的術語（而不僅僅是類型）時，你需要非常小心以確保你定義了你期望的術語，而不是其他一些恰好具有相同術語的術語類型。正如您現在可能已經想了幾分鐘，該代碼不會贏得可讀性獎項。

我不推薦這種方法，因爲它很容易出錯。 但是，如果您有許多類似的類型和功能，並且在開發過程中類型發生變化，它會很有用。你最終會遇到難以理解的戰術，但是一旦你調試了它們，即使調整了表達式類型，它們也可以工作。

Answer 2

這是可能在勒柯克> = 8.5

Fixpoint expsum (e : exp) : nat := 
match e with 
| num n => n 
| (plus e1 e2 | minus e1 e2 | mult e1 e2 | div e1 e2) => expsum e1 + expsum e2 end. 

Print expsum. (*expsum = 
fix expsum (e : exp) : nat := 
    match e with 
    | num n => n 
    | plus e1 e2 => expsum e1 + expsum e2 
    | minus e1 e2 => expsum e1 + expsum e2 
    | mult e1 e2 => expsum e1 + expsum e2 
    | div e1 e2 => expsum e1 + expsum e2 
    end 
    : exp -> nat*)