理解 Coq 中“有根据的”证明

Question

I'm writing a fixpoint that requires an integer to be incremented "towards" zero at every iteration. This is too complicated for Coq to recognize as a decreasing argument automatically and I'm trying prove that my fixpoint will terminate.

I have been copying (what I believe is) an example of a well-foundedness proof for a step function on Z from the standard library. (Here)

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.

which creates the following context:

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

My question is what does this goal actually mean?

I thought that the goal I'd have to prove for this would at least involve the step function that I want to show has the "well founded" property, "Z_increment".

The most useful explanation I have looked at is this but I've never worked with the list type that it uses and it doesn't explain what is meant by terms like "accessible".

Answer 1

Basically, you don't need to do a well founded proof, you just need to prove that your function decreases the (natural number) abs(z). More concretely, you can implement abs (z:Z) : nat := z_to_nat (z * Z.sgn z) (with some appropriate conversion to nat) and then use this as a measure with Function, something like Function foo z {measure abs z} := ....

The well founded business is for showing relations are well-founded: the idea is that you can prove your function terminates by showing it "decreases" some well-founded relation R (think of it as <); that is, the definition of f x makes recursive subcalls f y only when R y x. For this to work R has to be well-founded, which intuitively means it has no infinitely descending chains. CPDT's general recursion chapter as a really good explanation of how this really works.

这与你正在做的事情有什么关系？标准库证明，对于所有下界c，如果另外它仅适用于，x < y则是一个有根据的关系。我认为这不适用于您 - 相反，您会向零移动，因此您可以使用s上的通常关系减少。标准库已经证明了这种关系是有根据的，这就是使用。Zy >= cabs z<natFunction ... {measure ...}