Definitions
Examples of every mathematical definition mechanism
1-- Examples of every mathematical definition mechanism.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module DefinitionExamples8import Grace.Cumulus.Set.Choice9import Grace.Cumulus.Set10import Grace.Cumulus.Real.Metric11open Grace.Cumulus.Set.Foundation1213-- Give a reusable construction a name.14def duplicate (x : Set) : Set := {x, x}1516-- duplicate(a) is definitionally {a}1718-- Define a bounded function graph from a codomain proof.19defgraph inclusionMap (A B : Set) (x ∈ A) : B := x20requires subset : A ⊆ B21proof22 unfold Subset at subset23 exact subset with x, member2425-- inclusionMap.function and inclusionMap.value are checked laws.2627-- Choose a witness from a bounded predicate, justified by existence.28defchoose selected (A : Set) (x ∈ A) := x ∈ A29requires inhabited : ∃ x, x ∈ A30proof31 obtain ⟨x, member⟩ := inhabited32 witness x33 refine ⟨member, member⟩3435-- Extract a uniquely determined value without Choice.36defunique identityValue (A : Set) (x ∈ {A}) := x = A37proof38 witness A39 refine ⟨singleton.self at A, rfl⟩40uniqueness41 intro x42 intro xMember43 intro xValue44 intro y45 intro yMember46 intro yValue47 cc4849-- Name a proposition or a mathematical collection.50predicate FixedBy (f x : Set) := f(x) = x51class Natural (x : Set) := Nat(x)5253-- Define executable functions by checked structural recursion.54def copies (x : Set, n : Nat) → Set55 | x, zero => empty56 | x, succ(k) => {x, copies(x, k)}5758-- Introduce a set-encoded inductive datatype.59datatype Branches(A : Set)60 | leaf(value : A)61 | fork(left : self, right : self)6263-- Form a bounded subset by Separation.64def fixedPoints (A f : Set) : Set := {x ∈ A | f(x) = x}6566-- Form the image of a set by bounded Replacement.67def singletons (A : Set) : Set := {{x} | x ∈ A}6869-- Define an ordinal-indexed construction by transfinite recursion.70noncomputable transfinite def stages (α : Ordinal) : Set71 | 0 => empty72 | succ β => 𝒫(stages β)73 | limit λ => ⋃ { stages β | β < λ }7475-- Recurse through set membership using a checked history graph.76noncomputable foundation def memberLayers (x : Set) : Set77 | x using history => 𝒫(history)7879-- Recurse over a set with a certified well-founded relation.80noncomputable well-founded def rankOn (A x : Set) : Set81 over A ordered by membershipOn(A)82 certified by membershipOn.wellFounded83 | x using history => 𝒫(history)8485-- The graph is a set-valued object, and its application has a proved value.86theorem inclusion_value (A B x : Set)87 requires subset : A ⊆ B88 requires member : x ∈ A89 shows inclusionMap(A, B)(x) = x90proof91 exact inclusionMap.value with subset, member9293-- Selection is justified under the same existence hypothesis.94theorem selected_member (A : Set)95 requires inhabited : ∃ x ∈ A, x = x96 shows selected(A) ∈ A97proof98 have exists : ∃ x, x ∈ A99 rcases inhabited with ⟨x, member, equal⟩100 refine ⟨x, member⟩101 have chosen := selected.selected with exists102 tauto103