對Coq中的記錄構造中的模式匹配感到困惑

我一直在使用Coq很短的時間，並且仍然碰到牆上有些東西。我用Record結構定義了一個集合。現在我需要做一些模式匹配來使用它，但我有問題正確使用它。首先，這些是我的元素。對Coq中的記錄構造中的模式匹配感到困惑

Inductive element : Set := 
| empty : element 
. 
. 
. 
| fun_m : element -> element -> element 
| n_fun : nat -> element -> element 
.

我挑選具有一定特色的元素，使它們的一個子集的下一個方法：

Inductive esp_char : elements -> Prop := 
| esp1 : esp_char empty 
| esp2 : forall (n : nat)(E : element), esp_char E -> esp_char (n_fun n E). 

Record especial : Set := mk_esp{ E : element ; C : (esp_char E)}.

現在，我需要使用的定義和對「特殊」的元素固定點，只是兩個我選擇。我已閱讀記錄的文件和我所得到的是，我需要做這樣的事情：

Fixpoint Size (E : especial): nat := 
match E with 
|{|E := empty |}  => 0 
|{|E := n_fun n E0|} => (Size E0) + 1 
end.

當然，這告訴我，我缺少的元素的電感部分，所以我加的一切{|E := _ |}=> 0，或任何東西，只是爲了使感應器充滿。即使這樣做，然後我發現這個問題：

|{|E := n_fun n E0|} => (Size E0) + 1 

Error: 
In environment 
Size : especial -> nat 
E : especial 
f : element 
i : esp_char f 
n : nat 
E0 : element 
The term "E0" has type "element" while it is expected to have type "especial".

我已經無法做的是修復過去的事情，我有一個引理證明如果n_fun n E0是「特殊」，那麼E0是特殊的，但我可以在Fixpoint內部不會這樣構建。我還定義了「所有元素」的大小，然後在一個定義中選擇了「特殊」元素，但我希望能夠直接在集合「特殊」上進行直接模式匹配。謝謝您的意見。

編輯：忘了提，我也有一個強制總是發送特別元素。

編輯：這是我的方法，然後再發布過：

Fixpoint ElementSize (E : element): nat := 
match E with 
| n_fun n E0 => (ElementSize E0) + 1 
| _ => 0 
end. 

Definition Size (E : especial) := ElementSize E.

來源

2016-03-28 Sara

當然這裏的東西不排隊，類型錯了（提示，嘗試'關於C'。我建議你先在'element'上定義尺寸函數，然後用記錄訪問器編寫尺寸函數來獲得'especial'（sic）的尺寸。 – ejgallego

我完全按照你的建議做了，似乎是最自然的方式，但我被要求只用一個單一的Fixpoint來完成，這就是我卡住的地方。我編輯修復了一些錯別字，並添加了一些細節。 – Sara

哦，那好像是一個奇怪的需求，看到答案，因爲我不能在這裏複製完整的代碼。 – ejgallego

我試圖做：

Lemma mk_especial_proof n E : esp_char (n_fun n E) -> esp_char E. 
Proof. now intros U; inversion U. Qed. 

Fixpoint Size (E : especial): nat := 
match E with 
|{|E := empty    |} => 0 
|{|E := n_fun n E0; C := P |} => (Size (mk_esp E0 (mk_especial_proof _ _ P))) + 1 
|{|E := fun_m E1 E2  |} => 0 
end.

然而，這將失敗終止檢查。我不熟悉如何用記錄來克服這個問題。我會明確地遵循我在評論中提到的方法（對基礎數據類型使用固定點）。

編輯：增加了單一的fixpoint解決方案。

Fixpoint size_e e := 
    match e with 
    | empty  => 0 
    | fun_m e1 e2 => 0 
    | n_fun _ e => 1 + size_e e 
    end. 

Definition size_esp e := size_e (E e).

來源

2016-03-28 17:41:24 ejgallego

謝謝，我同意另一種方法，可惜我需要這個方法（我不明白它背後的基本原理）。我試過這個，我得到一個錯誤：對Size的遞歸調用的主參數等於「{| E：= E0; C：= mk_especial_proof n E0 P0 |}」而不是子項「E」。你知道這意味着什麼，或者我錯了哪裏？ – Sara

只需注意一點，另一種方法可以讓您以單個固定點*執行此任務*。錯誤信息意味着Coq無法弄清楚「mk_esp ...」是比輸入項「E」更小的項。 – ejgallego

我已經編輯了我的文章，以我原來的解決方案，我有一個Fixpoint和一個定義，你能指出我要改變什麼來讓Fixpoint吸收定義嗎？也謝謝你的解釋。 – Sara

我將你的例子簡化爲此，但你可以輕鬆地回到你的定義。我們有一個集合和一個由歸納謂詞定義的子集。通常使用西格馬類型的這種方法，其符號爲{b | Small b}，但它實際上與您示例中使用的Record定義相同，所以不要介意:-)。

Inductive Big : Set := (* a big set *) 
| A 
| B (b0 b1:Big) 
| C (b: Big). 

Inductive Small : Big -> Prop := (* a subset *) 
| A' : Small A 
| C' (b:Big) : Small b -> Small (C b). 

Record small := mk_small { b:Big ; P:Small b }.

這是一個解決方案。

Lemma Small_lemma: forall b, Small (C b) -> Small b. 
Proof. intros b H; now inversion H. Qed. 

Fixpoint size (b : Big) : Small b -> nat := 
    match b with 
     | A => fun _ => 0 
     | B _ _ => fun _ => 0 
     | C b' => fun H => 1 + size b' (Small_lemma _ H) 
    end. 

Definition Size (s:small) : nat := 
    let (b,H) := s in size b H.

爲了能夠使用假設H在match -branches，它被送入分支作爲函數參數。否則，b的銷燬不會在H期限內執行，並且Coq無法證明我們在H上執行了結構遞歸。

來源

2016-03-30 07:44:18 larsr

對Coq中的記錄構造中的模式匹配感到困惑

回答

相關問題