Prove a relation is not well-founded

3
votes

Recall the definition of a well-founded relation from Coq's library :

Inductive Acc (A : Set) (R : A -> A -> Prop) (x : A) : Prop :=
  Acc_intro : (forall y : A, R y x -> Acc A R y) -> Acc A R x.

Definition well_founded (A : Set) (R : A -> A -> Prop) :=
  forall x : A, Acc A R x.

In other words, if all the predecessors y of an element x are accessible, then x is accessible too. This Coq definition accepts all usual mathematical well-founded relations, for example the strict order < on the natural numbers.

However, how can we prove that the strict order on the signed integers is not well-founded in this Coq sense ? As a constructive proof of a negation, we would start by assuming by contradiction that the order on signed integers is well-founded. That means all signed integers are accessible. Where is the contradiction in that ? Acc_intro looks happy with it.

But if we axiomatize that the order on signed integers is well-founded, we will be able to define a function recursively on them. The computation of this function will be an infinite loop, which seems to break the consistency of Coq's logic.

Did I make a mistake somewhere ?

1
coq

1 Answers

3
votes

If < were well-founded on the integers, the following function would terminate:

f : Z -> False
f x = f (x - 1)

Thus, f 0 would yield a proof of False. We can formalize this argument in Coq as follows:

Require Import Coq.ZArith.ZArith.

Lemma Z_lt_not_well_founded : ~ well_founded Z.lt.
Proof.
intros Hwf.
exact (Fix Hwf (fun _ => False) (fun x IH => IH (Z.pred x) (Z.lt_pred_l x)) 0%Z).
Qed.