Require Import Prelude.

Section WFR.
  Variable X : Type.
  Variable R : X -> X -> Prop.
  Variable XM : forall P, P \/ ~ P.

  Implicit Types (x y z : X) (p q r : X -> Prop).

  Definition serial p := ex p /\ forall x, p x -> exists y, p y /\ R y x.

  Definition minel p x := p x /\ forall y, p y -> ~ R y x.

  Definition regular p := ex p -> ex (minel p).

  Lemma serial_not_has_min p :
    serial p -> ~ ex (minel p).
  Proof.
    intros (_&H1) (x&H2&H3).
    specialize (H1 x H2) as (y&H4&H5).
    apply (H3 y H4 H5).
  Qed.

  Fact all_regular_not_ex_serial :
    all regular <-> ~ ex serial.
  Proof.
    split.
    - intros H1 [p H2].
      enough (~ ex (minel p)) as H3 by apply H3, H1, H2.
      apply serial_not_has_min, H2.
    - intros H1 p H2. contra XM H3.
      apply H1. exists p. split. exact H2.
      intros x H4. contra XM H5.
      apply H3. exists x. split. exact H4.
      intros y H6. contradict H5. now exists y.
  Qed.

  Inductive Acc : X -> Prop :=
  | AccI x : (forall y, R y x -> Acc y) -> Acc x.

  Fact all_Acc_all_regular :
    all Acc -> all regular.
  Proof.
    intros H p (x&H1).
    induction (H x) as [x _ IH].
    destruct (XM (exists y, p y /\ R y x)) as [(y&H2&H3)|H2].
    - now apply (IH y).
    - exists x. split. exact H1.
      intros y H3. contradict H2. now exists y.
  Qed.

  Fact not_ex_serial_all_Acc :
    ~ ex serial -> all Acc.
  Proof.
    intros H. intros x. contra XM H1.
    apply H. exists (fun z => ~ Acc z).
    split. now exists x. clear x H H1.
    intros x H. contra XM H1.
    apply H. constructor. intros y H2.
    contra XM H3. apply H1. now exists y.
  Qed.

  Definition inductive p := (forall x, (forall y, R y x -> p y) -> p x) -> all p.

  Fact all_Acc_all_inductive :
    all Acc <-> all inductive.
  Proof.
    split.
    - intros H p H1 x. apply Acc_ind; auto.
    - intros H. apply H. apply AccI.
  Qed.

End WFR.