Library Coq.Wellfounded.Well_Ordering

Author: Cristina Cornes. From: Constructing Recursion Operators in Type Theory L. Paulson JSC (1986) 2, 325-355

Require Import Eqdep.

#[universes(template)]
Inductive WO (A : Type) (B : A -> Type) : Type :=
  sup : forall (a:A) (f:B a -> WO A B), WO A B.

Section WellOrdering.
  Variable A : Type.
  Variable B : A -> Type.

  Notation WO := (WO A B).

  Inductive le_WO : WO -> WO -> Prop :=
    le_sup : forall (a:A) (f:B a -> WO) (v:B a), le_WO (f v) (sup _ _ a f).

  Theorem wf_WO : well_founded le_WO.

End WellOrdering.

Section Characterisation_wf_relations.

Wellfounded relations are the inverse image of wellordering types

  Variable A : Type.
  Variable leA : A -> A -> Prop.

  Definition B (a:A) := {x : A | leA x a }.

  Definition wof : well_founded leA -> A -> WO A B.

End Characterisation_wf_relations.

Navigation