Acc (accessibility)

Accessibility is used for expressing strong induction. A relation is well-founded if every element of the underlying type is accessible using that relation.

The Acc predicate is defined among the primitives, but aliased in the Acc module:

Acc : intersect (i : level) . forall (A : U i) (R : A -> A -> U i) . A -> U i

So if A is a type, and R is a relation on A, then Acc A R x means that properties of x can be proven by induction. (Ignoring constructive niceties, it means that there are no infinite chains descending from x.)

For example, well-foundedness of < on natural numbers is expressed by the lemma:

Nat.lt_well_founded : forall (n : nat) . Acc nat n

The main use of accessibility is to invoke induction on an accessibility hypothesis, often obtained from a well-foundness lemma.

Accessibility can also be used directly. The definition is complicated (given below); it is easier to think about in terms of its intro and elim operations:

Acc_intro : forall (i : level) (A : U i) (R : A -> A -> U i) (x : A) .
               (forall (y : A) . R y x -> Acc A R y) -> Acc A R x

Acc_elim : forall (i : level) (A : U i) (R : A -> A -> U i) (x y : A) .
              Acc A R x -> R y x -> Acc A R y

Acc = fn A R x .
         exists (a : mu t . (exists (y : A) . forall (z : A) . R z y -> t)) .
             (fn W b y .
               exists (v : y = b #1 : A) . forall (z : A) (r : R z y) . W (b #2 z r) z)