2

我已经写了这个归纳谓词和它的（强）规范的部分证明：

Inductive SumPairs : (nat*nat) -> list (nat*nat) -> Prop :=
| sp_base : SumPairs (0,0) nil
| sp_step : forall (l0:list (nat*nat)) (n0 n1: nat) (y:(nat*nat)), SumPairs (n0,n1) l0 -> SumPairs ((n0+(fst y)),(n1+(snd y))) (cons y l0).

Theorem sumPairs_correct : forall (l:list (nat*nat)), { n: nat | SumPairs (n,n) l }.
Proof.
...

问题是我认为这个定理不正确，因为 Coq 不接受类似{n0 n1: nat | ...}. 有没有办法解决这个问题还是我想错了？

我认为谓词SumPairs是正确的，但由于我不确定，这里有一个它应该如何工作的例子： input [(1,2),(3,4)], expected output[3,7]

4

1 回答 1

2

您可以在结果中放入一对，例如：

Inductive SumPairs : (nat*nat) -> list (nat*nat) -> Prop :=
| sp_base : SumPairs (0,0) nil
| sp_step : forall (l0:list (nat*nat)) (n0 n1: nat) (y:(nat*nat)), SumPairs (n0,n1) l0 -> SumPairs ((n0+(fst y)),(n1+(snd y))) (cons y l0).

Theorem sumPairs_correct : forall (l:list (nat*nat)), { p: nat * nat | SumPairs p l }.
Proof.
intros l.
induction l as [|p l [[x y] IH]].
- exists (0, 0); constructor.
- now exists (x + fst p, y + snd p); constructor.
Qed.

然而，对于这个特定的任务，实际上最好只使用一个普通的函数式程序：

Require Import Coq.Lists.List.

Definition sum_list l := fold_left Nat.add l 0.

Definition sum_pairs l := (sum_list (map fst l), sum_list (map snd l)).

这个定义比第一个版本更容易阅读、理解和修改。请注意，您仍然可以使用 Coq 来推理该函数：

Lemma sum_list_cat l1 l2 : 
  sum_pairs (l1 ++ l2) = 
  (fst (sum_pairs l1) + fst (sum_pairs l2),
   snd (sum_pairs l1) + snd (sum_pairs l2)).
(* Exercise! *)
于 2021-05-24T02:51:24.583 回答