Понимание "обоснованных" доказательств в Coq - PullRequest
Новая
       9

Понимание "обоснованных" доказательств в Coq

0 голосов
/ 07 мая 2018

Я пишу точку фиксации, которая требует увеличения целого числа «к нулю» на каждой итерации. Это слишком сложно для Coq, чтобы автоматически распознавать его как убывающий аргумент, и я пытаюсь доказать, что моя точка фиксации прекратит работу.

Я копировал (как я полагаю) пример доказательства обоснованности пошаговой функции на Z из стандартной библиотеки. (Здесь) 

Require Import ZArith.Zwf.

Section wf_proof_wf_inc.
  Variable c : Z.
  Let Z_increment (z:Z) := (z + ((Z.sgn c) * (-1)))%Z.

  Lemma Zwf_wf_inc : well_founded (Zwf c).
  Proof.
    unfold well_founded.
    intros a.
  Qed.

End wf_proof_wf_inc.

, который создает следующий контекст: 

  c : Z
  wf_inc := fun z : Z => (z + Z.sgn c * -1)%Z : Z -> Z
  a : Z
  ============================
  Acc (Zwf c) a

Мой вопрос: что на самом деле означает эта цель?

Я думал, что цель, которую я должен доказать для этого, будет, по крайней мере, включать в себя функцию шага, которую я хочу показать, имеет "обоснованное" свойство "Z_increment".

Самое полезное объяснение, на которое я смотрел, это this , но я никогда не работал с типом списка, который он использует, и он не объясняет, что подразумевается под такими терминами, как "доступные".

1 Ответ

0 голосов
/ 07 мая 2018

По сути, вам не нужно делать обоснованные доказательства, вам просто нужно доказать, что ваша функция уменьшает (натуральное число) abs (z). Более конкретно, вы можете реализовать abs (z:Z) : nat := z_to_nat (z * Z.sgn z) (с некоторым соответствующим преобразованием в nat), а затем использовать это как меру с Function, что-то вроде Function foo z {measure abs z} := ....

Хорошо обоснованный бизнес заключается в том, чтобы показать, что отношения обоснованы: идея состоит в том, что вы можете доказать, что ваша функция заканчивается, показывая, что она "уменьшает" некое обоснованное отношение R (подумайте об этом) как <); то есть определение f x делает рекурсивные подзвоны f y только тогда, когда R y x. Для этого R должен быть обоснованным , что интуитивно означает, что у него нет бесконечно нисходящих цепей. общая рекурсивная глава CPDT как действительно хорошее объяснение того, как это действительно работает.

Как это связано с тем, что вы делаете? Стандартная библиотека доказывает, что для всех нижних границ c, x < y является обоснованным отношением в Z, если дополнительно оно применяется только к y >= c. Я не думаю, что это относится к вам - вместо этого вы двигаетесь к нулю, так что вы можете просто уменьшить abs z с обычным отношением < на nat с. В стандартной библиотеке уже есть доказательство того, что это отношение хорошо обосновано, и именно это Function ... {measure ...} использует.

...