Grace/Cumulus/Set/Ordinal.g17

Open in Workbench Download source

Imports

Classes · Foundation

Declarations

• Transitive predicate
• Ordinal class
• next def
• Limit predicate
• membership.wellFounded theorem derivation
• Transitive.empty theorem derivation
• Ordinal.empty theorem derivation
• next.membership theorem derivation
• next.contains theorem derivation
• Ordinal.transitive theorem derivation
• Ordinal.member_transitive theorem derivation
• Ordinal.next theorem derivation
• next.natural theorem derivation
• Ordinal.natural theorem derivation
• Ordinal.member theorem derivation
• Ordinal.union theorem derivation
• Ordinal.trichotomy theorem derivation
• Ordinal.cases theorem derivation
• Ordinal.subset_bound theorem derivation

Source

1-- Ordinals2-- 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 Grace.Cumulus.Set.Ordinal8import Classes9import Foundation1011-- Von Neumann ordinals: transitive sets whose elements are transitive.12predicate Transitive (A : Set) := ∀ x ∈ A, (x ⊆ A)13class Ordinal (α : Set) := { α | Transitive(α) ∧ (∀ β ∈ α, Transitive(β)) }1415def next (α : Set) : Set := α ∪ {α}16predicate Limit (λ : Set) := λ ∈ Ordinal ∧ λ ≠ ∅ ∧ (∀ α ∈ λ, next(α) ∈ λ)1718-- Foundation supplies the well-founded relation used by both bounded and19-- class-sized ordinal recursion.  The subset premise exposes the usual API.20theorem membership.wellFounded (A : Set)21  shows ∀ s, (∀ x ∈ s, x ∈ A) → s ≠ ∅ → ∃ m ∈ s, (∀ y ∈ m, ¬y ∈ s)22proof23  simp [set.foundation]2425theorem Transitive.empty26  shows Transitive(∅)27proof28  simp [Transitive, Subset, set.empty]2930theorem Ordinal.empty31  shows empty ∈ Ordinal32proof33  simp [Ordinal, Transitive, set.empty]3435theorem next.membership (x α : Set)36  shows x ∈ next(α) ↔ (x ∈ α ∨ x = α)37proof38  simp [next, union2.membership, singleton.membership]3940theorem next.contains (α : Set)41  shows α ∈ next(α)42proof43  simp4445theorem Ordinal.transitive (α : Set)46  requires h : α ∈ Ordinal47  shows Transitive(α)48proof49  simp [Ordinal]5051theorem Ordinal.member_transitive (α β : Set)52  requires hAlpha : α ∈ Ordinal53  requires hBeta : β ∈ α54  shows Transitive(β)55proof56  simp [Ordinal]5758theorem Ordinal.next (α : Set)59  requires h : α ∈ Ordinal60  shows next(α) ∈ Ordinal61proof62  simp [Ordinal, Transitive, Subset, next.membership]6364theorem next.natural (n : Nat)65  shows succ(n) = next(n)66proof67  simp [nat.succ, next, union2, singleton]6869theorem Ordinal.natural (n : Nat)70  shows n ∈ Ordinal71proof72  induction n73  | zero => settle with nat.zero, Ordinal.empty74  | succ(k) using ih => settle with next.natural, Ordinal.next7576theorem Ordinal.member (α β : Set)77  requires hAlpha : α ∈ Ordinal78  requires hBeta : β ∈ α79  shows β ∈ Ordinal80proof81  simp [Ordinal, Transitive, Subset]8283theorem Ordinal.union (A : Set)84  requires hOrdinal : ∀ α ∈ A, α ∈ Ordinal85  shows ⋃(A) ∈ Ordinal86proof87  simp [Ordinal, Transitive, Subset, Ordinal.transitive, set.union, Ordinal.member]8889theorem Ordinal.trichotomy (α : Set)90  shows α ∈ Ordinal → ∀ β, β ∈ Ordinal → (α ∈ β ∨ α = β ∨ β ∈ α)91proof92  induction α using membership93  intros a ihA hA β94  induction β using membership95  intros b ihB hB96  by_contra hNotComparable97  apply hNotComparable98  right99  left100  ext z101  constructor102  . intro hzA103    have hzOrdinal := Ordinal.member with hA, hzA104    have hzComparison := ihA with hzA, hzOrdinal, b, hB105    cases hzComparison with hzB | hzRest106    . exact hzB107    . cases hzRest with hzbEqual | hbInZ108      . exfalso109        rw hzbEqual at hzA110        apply hNotComparable111        right112        right113        exact hzA114      . exfalso115        have hATransitive := Ordinal.transitive with hA116        have hzSubset := hATransitive with z, hzA117        apply hNotComparable118        right119        right120        exact hzSubset with b, hbInZ121  . intro hzB122    have hzOrdinal := Ordinal.member with hB, hzB123    have hzComparison := ihB with hzB, hzOrdinal124    cases hzComparison with haInZ | hzRest125    . exfalso126      have hBTransitive := Ordinal.transitive with hB127      have hzSubset := hBTransitive with z, hzB128      apply hNotComparable129      left130      exact hzSubset with a, haInZ131    . cases hzRest with hazEqual | hzA132      . exfalso133        rw ← hazEqual at hzB134        apply hNotComparable135        left136        exact hzB137      . exact hzA138139theorem Ordinal.cases (β : Set)140  requires hBeta : β ∈ Ordinal141  shows β = ∅ ∨ (∃ α ∈ β, next(α) = β) ∨ Limit(β)142proof143  by_contra hNotCases144  apply hNotCases145  right146  right147  unfold Limit148  refine ⟨hBeta, ⟨?_, ?_⟩⟩149  . intro hEmpty150    apply hNotCases151    left152    exact hEmpty153  . intros α hAlpha154    have hAlphaOrdinal := Ordinal.member with hBeta, hAlpha155    have hNextOrdinal := Ordinal.next with hAlphaOrdinal156    have comparison := Ordinal.trichotomy with hNextOrdinal, β, hBeta157    cases comparison with hNextInBeta | hRest158    . exact hNextInBeta159    . cases hRest with hNextEqual | hBetaInNext160      . exfalso161        apply hNotCases162        right163        left164        refine ⟨α, hAlpha, hNextEqual⟩165      . exfalso166        simp [next.membership] at hBetaInNext167        cases hBetaInNext with hBetaInAlpha | hBetaEqual168        . have hTransitive := Ordinal.transitive with hBeta169          have hAlphaSubset := hTransitive with α, hAlpha170          exact membership.irreflexive with (hAlphaSubset with β, hBetaInAlpha)171        . rw hBetaEqual at hAlpha172          exact membership.irreflexive with hAlpha173174theorem Ordinal.subset_bound (α β : Set)175  requires hAlpha : α ∈ Ordinal176  requires hBeta : β ∈ Ordinal177  requires hSubset : α ⊆ β178  shows α ∈ next(β)179proof180  simp [Subset, Ordinal.trichotomy, next.membership, membership.irreflexive]181