wellfounded.v

(** Well-founded relations in intuitionistic type theory *)
(** last updated : 5 of April, 2017. email: dfrumin [at] cs.ru.nl *)
Definition relation A := A -> A -> Prop.

Section wf.
  Variable A : Type.
  Variable R : relation A.
  Notation "x '<' y" := (R x y).

  (** * Intuitionistic well-foundedness criteria *)

  (** A set is <-inductive if the membership [a ∈ P] if decided
  completely by the predecessors of [a]. *)
  Definition inductive (P : A -> Prop) : Prop := forall a, (forall b, b < a -> P b) -> P a.

  (** The smallest <-inductive subset of A is the accessibility relation [Acc] *)
  Inductive Acc (x : A) : Prop :=
  | Acc_intro : (forall y : A, y < x -> Acc y) -> Acc x.
  (** The way [Acc] is defined is with a single constructor
  [Acc_intro]. This allows Coq to generate a recursion principle for
  [Acc], even though [Acc] is (family of) inductive proposition. *)
  Lemma Acc_inductive : inductive Acc.
  Proof. intros ??. constructor. auto. Qed.

  Lemma Acc_inductive_min P : inductive P -> (forall a, Acc a -> P a).
  Proof. intros ?? HAcc. induction HAcc. auto. Qed.

  Definition well_founded := forall a, Acc a.

  (** We can prove the principle of well-founded recursion and use it
  to prove that every well-founded relation is irreflexive *)
  Theorem well_founded_induction :
    well_founded -> forall (P : A -> Prop),
      inductive P ->
      forall (a:A), P a.
  Proof.
    intros WF P IP a.
    pose (AccA:=WF a).
    induction AccA as [a Ha HaP].
    specialize (IP a). apply IP.
    assumption.
  Defined.

  Theorem wf_irrefl : well_founded -> forall (x:A), ~ (x < x).
  Proof.
    (** By well-founded induction it is sufficient to show that [{ x | ~ (x < x) }] is inductive. *)
    intros WF. eapply well_founded_induction; auto.
    intros a IH Haa. apply (IH a); auto.
  Qed.
  
  (** * Classical well-foundedness *)
  (** Clasically, a relation is well-founded if every inhabited subset
  of [A] has a <-minimal element. *)
  Definition inhab P := exists (x:A), P x.
  Definition minelem P := { x : A | P x /\ ~ exists y, y < x /\ P y }.
  Definition classical_wf := forall P, inhab P -> minelem P.

  (** Clasically, of course, a well-founded relation is also irreflexive. This proof is from Guillaume Allais. *)
  Lemma classical_wf_irrefl : classical_wf -> forall x, ~ (x < x).
  Proof.
    intros cwf x.
    pose (P := fun y => x < y \/ x = y).
    assert (px : P x) by (cbv; auto).
    destruct (cwf P) as [y [Py miny]].
    - exists x; assumption.
    - destruct Py as [ltyx | eqxy]; subst; intros ?;
        apply miny; eexists; eauto.
  Qed.

End wf.

Arguments Acc {_}.
Arguments well_founded {_}.
Arguments inhab {_}.
Arguments classical_wf {_}.

(** * Relations between the different notions *)
(** ** Classical well-foundedness enforces classical logic *)
(** We can show that if a two-element type is clasically well-founded, then we have a full LEM *)
Definition lt : bool -> bool -> Prop := fun b1 b2 =>
  match b1, b2 with
  | false,true => True
  | _,_ => False
  end.

Theorem classical_bool_wf : classical_wf lt -> (forall Q, Q \/ ~ Q).
Proof.
  unfold classical_wf. intros C Q.
  (** Consider a set [P = { true } ∪ { false | Q }]. *)
  pose (P:=(fun (x : bool) => if x then True else Q)).
  (** It is inhabited. *)
  assert (inhab P) as Pin.
  { exists true. unfold P. auto. }
  (** Therefore, it must contain a minimal element [x]. *)
  specialize (C P Pin).
  destruct C as [x [Px Pxmin]].
  (** [x] is either [true] or [false]. If [x = false], then 
      [false ∈ P] and Q must hold. Otherwise we can prove that 
      [~Q] holds. For suppose [Q] holds; then [false ∈ P] and 
      hence [x = true] is not a minimal element of [P]. *)
  destruct x; compute in Px.
  - right. intro HQ. apply Pxmin.
    exists false. tauto. 
  - left; auto.
Qed.    

(** However, we can show that [bool] is well-founded
intuitionistically, just by case analysis on every element. *)

Theorem intuit_bool_wf : well_founded lt.
Proof.
  intro x.  
  destruct x; constructor; intuition; constructor; destruct y; intuition;
    try (match goal with
    | [H : lt ?x ?y |- _ ] => inversion H
    end).  
  destruct y; constructor; intuition;
    try (match goal with
    | [H : lt ?x ?y |- _ ] => inversion H
    end).      
Qed.

(** Essentially the same argument can be preformed with any inhabited
well-founded relation. The only difference is the choice of the subset
[P]. *)


Section wf0.
  Variable A : Type.
  Variable R : relation A.
  Notation "x '<' y" := (R x y).

  Theorem classical_wf_inhab_lem (y x : A) :
    y < x -> classical_wf R -> (forall Q, Q \/ ~ Q).
  Proof.
    intros Hyx C Q. unfold classical_wf in C.
    (** P = { x } ∪ { a < x | Q } *)
    pose (P:=(fun (a : A) => (a = x) \/ (a < x /\ Q))).
    assert (inhab P) as Pin.
    { exists x. compute. tauto. }
    destruct (C P Pin) as [c [Hc Hcmin]].
    compute in Hc.
    destruct Hc; [subst| tauto ] .
    right. intros HQ. apply Hcmin. exists y. compute. eauto.
  Qed.

  (** ** Classical well-foundedness implies intuitionsitic well-foundness *)
  (** The main trick in the proof is due to Mike Shulman:

      > Hmm, how about this for a sneaky trick? Suppose (A,<)
      > is classically well-founded; we want to show it is
      > well-founded. So let U⊆A be inductive, and let
      > a∈A; we want to show a∈U. Since U is inductive,
      > it suffices to show that every b < a is in U,
      > i.e. we may assume given a b such that b < a and
      > show b∈U. But now < is inhabited, so LEM holds;
      > therefore (A,<) is well-founded by the previous
      > argument, and so U=A and thus b∈U. 
     
   *)
  
  Theorem intuitionistic_wf_classical_wf : classical_wf R -> well_founded R.
  Proof.
    intros C. intro x.
    (** In oreder to show [Acc < x], suffices to prove the accissibility of all [y] for [y < x]. *)
    constructor. intros y Hyx.
    (** But once we have [y < x] we can establish classical logic as per previous lemma *)
    pose (LEM:=(classical_wf_inhab_lem y x Hyx C)).
    (** By classical reasoning it suffices to  show [~~ Acc R y] *)
    destruct (LEM (Acc R y)); auto. exfalso.    
    (** Suppose [y] is *not* accessible. Then the set of in-accessible
    elements is inhabited and thus contains a minimal element [p]. But
    by that token, [p] can not be in-accessible. *)
    pose (P:=fun a => ~ Acc R a).
    assert (inhab P) as Pin.
    { exists y. tauto. }
    destruct (C P Pin) as [p [Hp Hpmin]]. compute in Hp.
    apply Hp.
    { (** In fact, we can show that [p] is accessible. Let [p' < p]. *)
      constructor. intros p' Hp'p.
      (** Suffices to show [~~ Acc R p'], which is possible because if
      [p'] is inaccessible, then [p] is no longer a minimal element.
      *)
      destruct (LEM (Acc R p')) as [?|Hneg_p']; [auto|exfalso].
      apply Hpmin.
      exists p'. tauto.
    }
  Qed.
End wf0.

(** ** The "no infinite descent condition".

The last condition we consider is the one stating that there are no
infinitely descending <-chain.

I will show that the intuitionistic formulation implies the
"no-chains" condition. Currently I am not aware of a relation that
satisfies the "no-chains" condition but does not satisfy the
intuitionistic condition. Something to ponder about.

The proofs below are from Adam Chilipala CPDT book.
*) 

Section descent.
Context {A : Type}.
Variable R : A -> A -> Prop.
Notation "x '<' y" := (R x y).

Definition chain (x : nat -> A) := forall n, (x (S n)) < (x n).

Lemma acc_no_chain x : Acc R x
  -> forall c, chain c -> ~ exists n, c n = x.
Proof. generalize dependent x.
 induction 1; eauto.
 intros c ChainC [n Hcn].
 pose (y:=(c (S n))).
 assert (y < x) as Hyx.
 { subst. unfold y. apply ChainC. }
 specialize (H0 y Hyx c ChainC).
 apply H0. exists (S n); auto.
Qed.

Lemma wf_no_descent : well_founded R -> ~ exists x, chain x.
Proof.
  intros WF [x Chain].
  eapply (acc_no_chain (x 0)); eauto.
Qed.

End descent.

Section topology.
  Context {A : Type}.
  Implicit Types P Q S : A -> Prop.
  Definition dense P := forall (x : A), ~~ P x.
  Definition closed P := forall (x : A), ~~ P x -> P x.

  Definition j_well_founded (R : A -> A -> Prop) :=
    forall P, closed P -> inductive _ R P -> forall (x : A), P x.  
End topology.