Accessibility and extraction of infinite decending chains

acc_idc.v

From Equations Require Import Equations.
From Coq Require Import ssreflect.

Section Defs.
  Context {A : Type} (R : A -> A -> Prop).

  Definition entire := forall x, exists y, R y x.

  Definition idc_from a0 :=
    exists f : nat -> A, f 0 = a0 /\ forall n, R (f (S n)) (f n).

  Definition idc := exists f : nat -> A, forall n, R (f (S n)) (f n).
End Defs.

Definition dc_statement := forall A (R : A -> A -> Prop), entire R -> forall a0, idc_from R a0.


Lemma wf_not_idc {A : Type} (R : A -> A -> Prop) : well_founded R -> ~(idc R).
Proof.
  move=> wfR [f hf].
  apply (Fix (measure_wf wfR f)); last constructor.
  move=> n h; apply: (h (S n)); apply: hf.
Qed.

Module not_wf_idc.
  Context (em : forall (P : Prop), P \/ ~ P).
  Context (dc : dc_statement).

  Lemma dne : forall P, ~~P -> P.
  Proof. move=> P; case: (em P)=> //. Qed.

  Lemma neg_exists (A : Type) (P : A -> Prop) : ~ (exists a, P a) -> forall a, ~ P a.
  Proof. move=> h a p; apply: h; exists a=> //. Qed.

  Lemma em_forall (A : Type) (P : A -> Prop) : (forall a, P a) \/ exists a, ~ (P a).
  Proof.
    case: (em (forall a, P a)); [now left|right].
    apply: dne=> /neg_exists h; apply: b=> x; exact (dne _ (h x)).
  Qed.

  Context (A : Type) R (h : ~(well_founded (A:=A) R)).

  Lemma non_acc_pt : exists a, ~(Acc R a).
  Proof. case: (em_forall A (Acc R))=> // /h []. Qed.

  Definition Rstar := (Relation_Operators.clos_refl_trans A R).

  Section LocalDef.
    Context (a : A) (ha : ~(Acc R a)).
    Definition B := { x : A | Rstar x a /\ ~(Acc R x) }.

    Definition RB (x y : B) := R (proj1_sig x) (proj1_sig y).

    Lemma entire_RB : entire RB.
    Proof.
      move=> [x [xa hx]].
      case: (em_forall A (fun y => ~ (R y x) \/ Acc R y)).
      - move=> h0; exfalso; apply hx; constructor=> z accz.
        case: (h0 z)=> // /(_ accz) [].
      - move=> [y0] /Decidable.not_or [/dne desc hy0].
        unshelve eexists (exist _ y0 _).
        1: split=> //; eapply Relation_Operators.rt_trans; last eassumption;
          by constructor.
        assumption.
    Qed.
  End LocalDef.

  Lemma inf_desc_chain : idc R.
  Proof.
    case: non_acc_pt=> [a ha].
    have a' : B a by exists a; split=> //; constructor.
    move: (dc (B a) (RB a) (entire_RB a) a') => [f [_ hf]].
    exists (fun n => proj1_sig (f n)) => //.
  Qed.

End not_wf_idc.


Module not_wf_idc_dc.
  Context (not_wf_idc : forall A (R : A -> A -> Prop), ~(well_founded R) -> idc R).
  Context A (R : A -> A -> Prop) (eR : entire R).

  Section Local.
    Context (a0 : A).
    Definition Rstar := (Relation_Operators.clos_refl_trans A R).
    Definition B := { x : A | Rstar x a0 }.
    Definition RB (x y : B) := R (proj1_sig x) (proj1_sig y).

    Lemma not_acc (b : B) : ~(Acc RB b).
    Proof.
      elim=> -[x hx] h ih; move: (eR x)=> [y hy].
      refine (ih (exist _ y _) hy).
      eapply Relation_Operators.rt_trans; last eassumption; by constructor. 
    Qed.

    Lemma not_wf : ~(well_founded RB).
    Proof.
      have a1 : B by exists a0; by constructor.
      move=> /(_ a1); apply: not_acc.
    Qed.
  End Local.

  Lemma reduce_idc_from a0 (b : B a0) : (idc_from (RB a0) b) -> (idc_from R a0).
  Proof.
    move: b=> [? h].
    move=> [g [geq0 hg]].
    have h' := (Operators_Properties.clos_rt_rt1n _ _ _ _ h).
    move: {geq0}g (f_equal (@proj1_sig _ _) geq0) hg => /= {h}. 
    induction h'.
    + move=> g geq0 hg; exists (fun n => proj1_sig (g n))=> //.
    + move=> gx geqx hgx.
      unshelve apply: IHh'.
      * case=>[|n]; [| exact (gx n)].
        exists y; by apply: Operators_Properties.clos_rt1n_rt.
      * reflexivity.
      * case=>[|n] /=; last apply: hgx.
        rewrite /RB geqx //=.
  Qed.

  Lemma dc : forall a0, exists f : nat -> A, f 0 = a0 /\ forall n, R (f (S n)) (f n).
  Proof.
    move=> a0.
    move: (not_wf_idc (B a0) (RB a0) (not_wf a0))=> [g hg].
    apply: (reduce_idc_from a0 (g 0)); exists g; split=> //.
  Qed.

End not_wf_idc_dc.


Module not_wf_idc_dne.
  Context (not_wf_idc : forall A (R : A -> A -> Prop), ~(well_founded R) -> idc R).

  Context (P : Prop).
  Definition RP (x y : unit) := P.
  Lemma not_wf_RP : ~~P -> ~(well_founded RP).
  Proof.
    move=> nnp wfRP; apply: nnp=> p.
    induction (wfRP tt). exact (H0 tt p).
  Qed.

  Lemma dne : ~~P -> P.
  Proof.
    move=> /not_wf_RP /not_wf_idc [? hf].
    exact (hf 0).
  Qed.
End not_wf_idc_dne.