对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中的记录构造中的模式匹配感到困惑

回答

相关问题