Well-foundedness of the lexicographic and product orders on DFinsupp and Pi #
The primary results are DFinsupp.Lex.wellFounded and the two variants that follow it,
which essentially say that if (· > ·) is a well order on ι, (· < ·) is well-founded on each
α i, and 0 is a bottom element in α i, then the lexicographic (· < ·) is well-founded
on Π₀ i, α i. The proof is modelled on the proof of WellFounded.cutExpand.
The results are used to prove Pi.Lex.wellFounded and two variants, which say that if
ι is finite and equipped with a linear order and (· < ·) is well-founded on each α i,
then the lexicographic (· < ·) is well-founded on Π i, α i, and the same is true for
Π₀ i, α i (DFinsupp.Lex.wellFounded_of_finite), because DFinsupp is order-isomorphic
to pi when ι is finite.
Finally, we deduce DFinsupp.wellFoundedLT, Pi.wellFoundedLT,
DFinsupp.wellFoundedLT_of_finite and variants, which concern the product order
rather than the lexicographic one. An order on ι is not required in these results,
but we deduce them from the well-foundedness of the lexicographic order by choosing
a well order on ι so that the product order (· < ·) becomes a subrelation
of the lexicographic (· < ·).
All results are provided in two forms whenever possible: a general form where the relations
can be arbitrary (not the (· < ·) of a preorder, or not even transitive, etc.) and a specialized
form provided as WellFoundedLT instances where the (d)Finsupp/pi type (or their Lex
type synonyms) carries a natural (· < ·).
Notice that the definition of DFinsupp.Lex says that x < y according to DFinsupp.Lex r s
iff there exists a coordinate i : ι such that x i < y i according to s i, and at all
r-smaller coordinates j (i.e. satisfying r j i), x remains unchanged relative to y;
in other words, coordinates j such that ¬ r j i and j ≠ i are exactly where changes
can happen arbitrarily. This explains the appearance of rᶜ ⊓ (≠) in
dfinsupp.acc_single and dfinsupp.well_founded. When r is trichotomous (e.g. the (· < ·)
of a linear order), ¬ r j i ∧ j ≠ i implies r i j, so it suffices to require r.swap
to be well-founded.
This key lemma says that if a finitely supported dependent function x₀ is obtained by merging
two such functions x₁ and x₂, and if we evolve x₀ down the DFinsupp.Lex relation one
step and get x, we can always evolve one of x₁ and x₂ down the DFinsupp.Lex relation
one step while keeping the other unchanged, and merge them back (possibly in a different way)
to get back x. In other words, the two parts evolve essentially independently under
DFinsupp.Lex. This is used to show that a function x is accessible if
DFinsupp.single i (x i) is accessible for each i in the (finite) support of x
(DFinsupp.Lex.acc_of_single).
Equations
- (_ : WellFoundedLT (Lex (Π₀ (i : ι), α i))) = (_ : IsWellFounded (Lex (Π₀ (i : ι), α i)) fun (x x_1 : Lex (Π₀ (i : ι), α i)) => x < x_1)
Equations
- (_ : WellFoundedLT (Lex ((i : ι) → α i))) = (_ : IsWellFounded (Lex ((i : ι) → α i)) fun (x x_1 : Lex ((i : ι) → α i)) => x < x_1)
Equations
- (_ : WellFoundedLT (Lex (ι → α))) = (_ : WellFoundedLT (Lex (ι → α)))
Equations
- (_ : WellFoundedLT (Lex (Π₀ (i : ι), α i))) = (_ : IsWellFounded (Lex (Π₀ (i : ι), α i)) fun (x x_1 : Lex (Π₀ (i : ι), α i)) => x < x_1)
Equations
- (_ : WellFoundedLT (Π₀ (i : ι), α i)) = (_ : WellFoundedLT (Π₀ (i : ι), α i))
Equations
- (_ : WellFoundedLT ((i : ι) → α i)) = (_ : IsWellFounded ((i : ι) → α i) fun (x x_1 : (i : ι) → α i) => x < x_1)
Equations
- (_ : WellFoundedLT (ι → α)) = (_ : WellFoundedLT (ι → α))
Equations
- (_ : WellFoundedLT (Π₀ (i : ι), α i)) = (_ : IsWellFounded (Π₀ (i : ι), α i) fun (x x_1 : Π₀ (i : ι), α i) => x < x_1)