Acc
is the accessibility predicate. Given some relation r
(e.g. <
) and a value x
,
Acc r x
means that x
is accessible through r
:
x
is accessible if there exists no infinite sequence ... < y₂ < y₁ < y₀ < x
.
- intro
{α : Sort u}
{r : α → α → Prop}
(x : α)
(h : ∀ (y : α), r y x → Acc r y)
: Acc r x
A value is accessible if for all
y
such thatr y x
,y
is also accessible. Note that if there exists noy
such thatr y x
, thenx
is accessible. Such anx
is called a base case.
Instances For
A relation r
is WellFounded
if all elements of α
are accessible within r
.
If a relation is WellFounded
, it does not allow for an infinite descent along the relation.
If the arguments of the recursive calls in a function definition decrease according to a well founded relation, then the function terminates. Well-founded relations are sometimes called Artinian or said to satisfy the “descending chain condition”.
- intro
{α : Sort u}
{r : α → α → Prop}
(h : ∀ (a : α), Acc r a)
: WellFounded r
If all elements are accessible via
r
, thenr
is well-founded.
Instances For
A type that has a standard well-founded relation.
Instances are used to prove that functions terminate using well-founded recursion by showing that recursive calls reduce some measure according to a well-founded relation. This relation can combine well-founded relations on the recursive function's parameters.
- rel : α → α → Prop
A well-founded relation on
α
. - wf : WellFounded rel
A proof that
rel
is, in fact, well-founded.
Instances
Equations
Instances For
Equations
Instances For
Equations
Instances For
A well-founded fixpoint. If satisfying the motive C
for all values that are smaller according to a
well-founded relation allows it to be satisfied for the current value, then it is satisfied for all
values.
This function is used as part of the elaboration of well-founded recursion.
Equations
Instances For
Equations
Instances For
The inverse image of a well-founded relation is well-founded.
Equations
Instances For
Strong induction on the natural numbers.
The induction hypothesis is that all numbers less than a given number satisfy the motive, which should be demonstrated for the given number.
Equations
Instances For
Equations
Instances For
Equations
A lexicographical order based on the orders ra
and rb
for the elements of pairs.
- left
{α : Type u}
{β : Type v}
{ra : α → α → Prop}
{rb : β → β → Prop}
{a₁ : α}
(b₁ : β)
{a₂ : α}
(b₂ : β)
(h : ra a₁ a₂)
: Prod.Lex ra rb (a₁, b₁) (a₂, b₂)
If the first projections of two pairs are ordered, then they are lexicographically ordered.
- right
{α : Type u}
{β : Type v}
{ra : α → α → Prop}
{rb : β → β → Prop}
(a : α)
{b₁ b₂ : β}
(h : rb b₁ b₂)
: Prod.Lex ra rb (a, b₁) (a, b₂)
If the first projections of two pairs are equal, then they are lexicographically ordered if the second projections are ordered.
Instances For
Equations
Equations
Instances For
Equations
Equations
Instances For
- left {α : Sort u} {β : α → Sort v} {r : α → α → Prop} {s : (a : α) → β a → β a → Prop} {a₁ : α} (b₁ : β a₁) {a₂ : α} (b₂ : β a₂) : r a₁ a₂ → Lex r s ⟨a₁, b₁⟩ ⟨a₂, b₂⟩
- right {α : Sort u} {β : α → Sort v} {r : α → α → Prop} {s : (a : α) → β a → β a → Prop} (a : α) {b₁ b₂ : β a} : s a b₁ b₂ → Lex r s ⟨a, b₁⟩ ⟨a, b₂⟩
Instances For
Equations
Instances For
Equations
- left {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} {a₁ a₂ : α} (b : β) : r a₁ a₂ → RevLex r s ⟨a₁, b⟩ ⟨a₂, b⟩
- right {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} (a₁ : α) {b₁ : β} (a₂ : α) {b₂ : β} : s b₁ b₂ → RevLex r s ⟨a₁, b₁⟩ ⟨a₂, b₂⟩
Instances For
Equations
Instances For
The wfParam
gadget is used internally during the construction of recursive functions by
wellfounded recursion, to keep track of the parameter for which the automatic introduction
of List.attach
(or similar) is plausible.
Equations
Instances For
Reverse direction of dite_eq_ite
. Used by the well-founded definition preprocessor to extend the
context of a termination proof inside if-then-else
with the condition.