Coq: Подтверждение пары списков

Я написал этот Индуктивный предикат и часть доказательства его (сильной) спецификации:

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 правильный, но, поскольку я не уверен, вот пример того, как он должен работать: вход [(1,2),(3,4)], ожидаемый результат [3,7]


coq coqide
person Cris Teller    schedule 24.05.2021    source источник
comment
Привет, Крис. Разве вы не ожидаете в качестве результата [(4,6)]?   -  person Pierre Jouvelot    schedule 24.05.2021

Ответы (1)


arrow_upward
2
arrow_downward

Вы можете поместить в результат пару, например:

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! *)
person Arthur Azevedo De Amorim    schedule 24.05.2021
comment
Спасибо, сработало! Единственная причина, по которой я не определил ее как простую функциональную программу, состоит в том, что мой учитель не хотел этого, но я все равно сохраню ее. Еще раз спасибо! - person Cris Teller; 24.05.2021