Skip to content

Commit

Permalink
Document Position
Browse files Browse the repository at this point in the history
Signed-off-by: zeramorphic <[email protected]>
  • Loading branch information
zeramorphic committed Dec 8, 2024
1 parent c1d80cc commit c2b07fe
Showing 1 changed file with 9 additions and 5 deletions.
14 changes: 9 additions & 5 deletions ConNF/Position/Position.lean
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,10 @@ import ConNF.Base.Params
/-!
# Position functions
In this file, we define what it means for a type to have a position function.
## Main declarations
* `ConNF.Position`: The typeclass that stores a position function for a type.
In this file, we define what it means for a type to have a *position* function. Various
well-foundedness constraints in our model are enforced by position functions, which are injections
into `μ`. If we can define a relation on a type with a position function such that `r x y` only if
`pos x < pos y`, then `r` must be well-founded; this situation will occur frequently.
-/

universe u
Expand All @@ -18,15 +17,20 @@ namespace ConNF

variable [Params.{u}]

/-- A *position* function on a type `X` is an injection from `X` into `μ`. -/
class Position (X : Type _) where
pos : X ↪ μ

export Position (pos)

/-- If `X` has a position function, then the cardinality of `X` must be at most `#μ`. -/
theorem card_le_of_position {X : Type _} [Position X] :
#X ≤ #μ :=
mk_le_of_injective pos.injective

/-- An induction (or recursion) principle for any type with a position function.
`C` is the *motive* of the recursion. If we can produce `C x` given `C y` for all `y` with position
lower than `x`, we can produce `C x` for all `x`. -/
@[elab_as_elim]
def pos_induction {X : Type _} [Position X] {C : X → Sort _} (x : X)
(h : ∀ x, (∀ y, pos y < pos x → C y) → C x) : C x :=
Expand Down

0 comments on commit c2b07fe

Please sign in to comment.