coq中的歸納數據類型的通用摺疊

Question

我發現自己一遍又一遍地重複一個模式，我想抽象它。我相當有信心coq足夠表達捕捉模式，但我在設法解決這個問題時遇到了一些麻煩。我定義編程語言，它具有代表句法方面相互遞歸感應數據類型：

Inductive Expr : Set := 
    | eLambda (x:TermVar) (e:Expr) 
    | eVar  (x:TermVar) 
    | eAscribe (e:Expr) (t:IFType) 
    | ePlus (e1:Expr) (e2:Expr) 

    | ... many other forms ... 

with DType : Set := 
    | tArrow (x:TermVar) (t:DType) (c:Constraint) (t':DType) 
    | tInt 

    | ... many other forms ... 

with Constraint : Set := 
    | cEq (e1:Expr) (e2:Expr) 
    | ... 

現在，有一些的，我需要定義在這些類型的功能。例如，我想要一個函數來查找所有的自由變量，一個執行替換的函數，以及一個抽取所有約束集合的函數。這些功能都具有以下形式：

Fixpoint doExpr (e:Expr) := match e with 
    (* one or two Interesting cases *) 
    | ... 

    (* lots and lots of boring cases, 
    ** all of which just recurse on the subterms 
    ** and then combine the results in the same way 
    *) 
    | .... 

with doIFType (t:IFType) := match t with 
    (* same structure as above *) 

with doConstraint (c:Constraint) := match c with 
    (* ditto *) 

例如，要查找免費的變量，我需要做的事情在變量的情況下，並且做結合的情況下有趣的，但一切我只是遞歸找到所有的子表達式的自由變量，然後將這些列表結合在一起。對於生成所有約束列表的函數也是如此。替代的情況下是更加棘手一點點，因爲結果類型的三個功能是不同的，以及用於將子表達式組合構造也不同：

Variable x:TermVar, v:Expr. 
Fixpoint substInExpr (e:Expr) : **Expr** := match e with 
    (* interesting cases *) 
    | eLambda y e' => 
     if x = y then eLambda y e' else eLambda y (substInExpr e') 
    | eVar y => 
     if x = y then v else y 

    (* boring cases *) 
    | eAscribe e' t => **eAscribe** (substInExpr e') (substInType t) 
    | ePlus e1 e2 => **ePlus** (substInExpr e1) (substInExpr e2) 
    | ... 

with substInType  (t:Type)  : **Type** := match t with ... 
with substInConstraint (c:Constraint) : **Constraint** := ... 
. 

編寫這些功能是乏味的且容易出錯的，因爲我必須爲每個函數寫出所有不感興趣的案例，並且我需要確保對所有子項遞歸。我想寫的是像下面這樣：

Fixpoint freeVars X:syntax := match X with 
    | syntaxExpr eVar x   => [x] 
    | syntaxExpr eLambda x e  => remove x (freeVars e) 
    | syntaxType tArrow x t1 c t2 => remove x (freeVars t1)++(freeVars c)++(freeVars t2) 
    | _   _  args  => fold (++) (map freeVars args) 
end. 

Variable x:TermVar, v:Expr. 
Fixpoint subst X:syntax := match X with 
    | syntaxExpr eVar y  => if y = x then v else eVar y 
    | syntaxExpr eLambda y e => eLambda y (if y = x then e else (subst e)) 
    | syntaxType tArrow ... 

    | _ cons args => cons (map subst args) 
end. 

這種想法的關鍵是構造一般適用於一些數量的參數，並且有某種的「地圖」，即，保留的能力參數的類型和數量。

很明顯，這個僞碼不起作用，因爲_ cases只是不正確。所以我的問題是，是否有可能編寫以這種方式組織的代碼，或者我註定要手動列出所有無聊的情況？

Answer 1

這是一條路要走，但它不給很可讀的代碼：使用戰術。

比方說，我有一個帶有許多構造函數的語言，並且我想將特定的目標僅應用於構造函數aaa給出的情況，並且我想要遍歷所有其他構造函數，以瞭解aaa的可能會出現在他們的下面。我可以執行以下操作：

假設你想定義一個函數A→B，你將需要跟蹤你處於什麼情況，所以你應該在A上定義一個幻像類型，減少到B.

Definition phant (x : A) : Type := B. 

我想，工會功能有B型 - 「乙 - > B和你有B中的默認值，稱爲empty_B

Ltac generic_process f := 
    match goal with 
    |- context [phan (aaa _)] => (* assume aaa has arith 1 *) 
     intros val_of_aaa_component; exact process_this_value val_of_aaa_component 
    | |- intros val_in_A => (* This should be used when the next argument of the current 
          constructor is in type A, you want to process recursively 
          down this argument, using the function f. *) 
     apply (union (f val_in_A)); (* This clause will fail if val_in_A is not in type A *) 
            (* This leaves a goal in B to be solved. *) 
     generic_process f 
    | |- intros val_in_not_A => (* This should be used when the next argument of the current 
           constructor is not in type A, you want to ignore it *) 
     generic_process f 
    | |- _ => (* this rule should be used when intros fails, we have exhausted all arguments 
       to the current constructor. *) 
     exact empty_B 
    end. 

現在，您可以通過一個證明定義函數。假設這個函數叫做process_aaa。

Definition process_aaa (x : A) : phant x. 
fix. (* This adds process_add : forall x:A, phant x. in the context. *) 
intros x; case x; generic_process process_aaa. 
Defined. 

注意generic_process的定義只點名一個構造函數，AAA，所有其他 以系統的方式處理。我們使用類型信息來檢測我們想要執行遞歸下降的那些值子組件。如果你有幾個相互歸納的類型，你可以在generic_process函數中添加參數來指明哪個函數將用於每個類型，並且有更多的子句，每個類型的每個參數一個。

我沒有時間來測試這個想法，但如果你測試它，請告訴我們。

Answer 2

這是另一種方式，雖然不是每個人都會喝杯茶。

這個想法是將遞歸移出類型和評估器，反過來對它進行參數化，並將表達式值轉化爲摺疊。這在某些方面提供了便利，但在其他方面更加努力 - 這實際上是您花費最多時間的地方的問題。好的方面是評估者可以很容易編寫，而且你不必處理相互遞歸的定義。然而，其他方式更簡單的事情可能會以這種風格變成腦筋急轉彎。

Require Import Ssreflect.ssreflect. 
Require Import Ssreflect.ssrbool. 
Require Import Ssreflect.eqtype. 
Require Import Ssreflect.seq. 
Require Import Ssreflect.ssrnat. 

Inductive ExprF (d : (Type -> Type) -> Type -> Type) 
       (c : Type -> Type) (e : Type) : Type := 
    | eLambda (x:nat) (e':e) 
    | eVar  (x:nat) 
    | eAscribe (e':e) (t:d c e) 
    | ePlus (e1:e) (e2:e). 

Inductive DTypeF (c : Type -> Type) (e : Type) : Type := 
    | tArrow (x:nat) (t:e) (c':c e) (t':e) 
    | tInt. 

Inductive ConstraintF (e : Type) : Type := 
    | cEq (e1:e) (e2:e). 

Definition Mu (f : Type -> Type) := forall a, (f a -> a) -> a. 

Definition Constraint := Mu ConstraintF. 
Definition DType  := Mu (DTypeF ConstraintF). 
Definition Expr  := Mu (ExprF DTypeF ConstraintF). 

Definition substInExpr (x:nat) (v:Expr) (e':Expr) : Expr := fun a phi => 
    e' a (fun e => match e return a with 
    (* interesting cases *) 
    | eLambda y e' => 
     if (x == y) then e' else phi e 
    | eVar y => 
     if (x == y) then v _ phi else phi e 

    (* boring cases *) 
    | _ => phi e 
    end). 

Definition varNum (x:ExprF DTypeF ConstraintF nat) : nat := 
    match x with 
    | eLambda _ e => e 
    | eVar y => y 
    | _ => 0 
    end. 

Compute (substInExpr 2 (fun a psi => psi (eVar _ _ _ 3)) 
        (fun _ phi => 
         phi (eLambda _ _ _ 1 (phi (eVar _ _ _ 2))))) 
     nat varNum. 

Compute (substInExpr 1 (fun a psi => psi (eVar _ _ _ 3)) 
        (fun _ phi => 
         phi (eLambda _ _ _ 1 (phi (eVar _ _ _ 2))))) 
     nat varNum.