On Well Founded sets and the Axiom of Choice
First, build a context with classical logic and assume the Axiom of
Functional Choice:
Require Import Classical.
Axiom functional_choice : forall (A:Set)(S:A->A->Prop),
(forall x, exists y, S x y )->
exists f, forall x, S x (f x).
Prove the following theorem:
notWellFounded_seq
: forall (A : Set) (R : A -> A -> Prop),
~ well_founded R ->
exists f : nat -> A, (forall n : nat, R (f (S n)) (f n))
Remarks
Look also at that exercise
The Axiom of Functional Choice is presented on Coq's FAQ
(in Coq's documentation ).
Look at the section "The Logic of Coq : Axioms".
Solution
Look at this file .
Going home