模式与奇偶案例匹配

假设我写勒柯克一个已知点的算法，总结了一个号码的所有“半”：模式与奇偶案例匹配

Fixpoint sum_of_halves (a : nat) : nat := 
    match a with 
    | 0 => 0 
    | 2 * k => a + (sum_of_halves k) 
    | S (2 * k) => a + (sum_of_halves k) 
    end.

试图评估该算法将得到：Error: Invalid notation for pattern.

我如何让Coq识别a是偶数还是奇数，并与2 * k或S (2 * k)匹配？

来源

2017-09-23 MoronicAcid

有很多讨论这个问题，使用搜索功能！ – ejgallego

我搜索偶数，奇数或两者的模式匹配。我找不到任何足够的答案来回答我的问题。 – MoronicAcid

Coq只能在构造函数上使用match。 nat有两个构造函数O和S，所以不能匹配2 * k。您将不得不使用非match结构或非nat类型或不同的算法。

来源

2017-09-24 03:59:25 jbapple

您需要证明给定自然数a只有三种情况。任一a为0，无论是a是另一数目k和k < a双，或a是双k + 1和k < a，即这三种情况是独占（这是重要的，否则使得模式匹配可能会导致一个inconistency）。

幸运的是，所有这些都可以完成。这是一个先进的Coq编程，但它已在ZArith中完成。这是一个解决方案。

首先注意到另一个数字已经由Coq库中的一个函数div2提供。

Require Import Arith Nat. 

Definition cases_div2 (a : nat) : 
    {k : nat | a = 2 * k /\ k < a}+{k : nat | a = S (2 * k) /\ k < a}+{a=0}. 
destruct a as [ | a']. 
    right; reflexivity. 
case_eq (odd (S a')); intros odd_a. 
    left; right; exists (div2 (S a')); rewrite (div2_odd (S a')) at 1. 
    split. 
    rewrite odd_a; simpl b2n; ring. 
    apply lt_div2; auto with arith. 
left; left; exists (div2 (S a')); rewrite (div2_odd (S a')) at 1. 
split. 
    rewrite odd_a; simpl b2n; ring. 
apply lt_div2; auto with arith. 
Defined.

现在，你可以在你的电话号码模式匹配一个使用cases_div2，但仍不足以定义函数，因为递归使用Fixpoint依靠递归调用发生在前作，这里k不能写作为前任模式，可用于任何输入a。你需要更强大的递归。我通常依靠Function或Fix进行这种强递归。这里是Fix

Definition sum_of_halves : nat -> nat := 
    Fix Arith.Wf_nat.lt_wf (fun _ => nat) 
    (fun a (sum_of_halves' : forall y, y < a -> nat) => 
    match cases_div2 a with 
    | inright h => 0 
    | inleft (inl (exist _ k (conj keq klt))) => 
     a + sum_of_halves' k klt 
    | inleft (inr (exist _ k (conj keq klt))) => 
     a + sum_of_halves' k klt 
    end).

一个例子然后来思考sum_of_halves你需要充分的理由归纳推理的，并使用Fix_eq。

这是一种可能性。

来源

2017-09-25 07:56:52 Yves

模式与奇偶案例匹配

回答

相关问题