Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
(** 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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.