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 Nat.lt 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)) .
fix
(fn W b y .
exists (v : y = b #1 : A) . forall (z : A) (r : R z y) . W (b #2 z r) z)
a
x