Grace/Cumulus/Set/Ordinal/Arithmetic.g17
Open in Workbench Download source
Imports
Basic · Relation.Algebra
Declarations
Source
12345678module Grace.Cumulus.Set.Ordinal.Arithmetic9import Basic10import Relation.Algebra1112noncomputable transfinite def ordinalAdd (α : Ordinal, β : Ordinal) : Set13 | 0 => α14 | succ γ => next(ordinalAdd(α, γ))15 | limit λ => ⋃(Relation.range(history))1617noncomputable transfinite def ordinalMul (α : Ordinal, β : Ordinal) : Set18 | 0 => ∅19 | succ γ => ordinalAdd(ordinalMul(α, γ), α)20 | limit λ => ⋃(Relation.range(history))2122noncomputable transfinite def ordinalPow (α : Ordinal, β : Ordinal) : Set23 | 0 => 124 | succ γ => ordinalMul(ordinalPow(α, γ), α)25 | limit λ => ⋃(Relation.range(history))2627notation infixl 60 "+" => ordinalAdd for Ordinal28notation infixl 70 "*" => ordinalMul for Ordinal29notation infixr 80 "^" => ordinalPow for Ordinal30313233theorem ordinalAdd.zero (α : Ordinal)34 shows α + 0 = α35proof36 simp [ordinalAdd, nat.zero]3738theorem ordinalAdd.next (α β : Ordinal)39 shows α + next(β) = next(α + β)40proof41 simp [ordinalAdd.equation.successor]4243theorem ordinalAdd.limit (α λ : Ordinal)44 requires h : Limit(λ)45 shows α + λ = ⋃(Relation.range(ordinalAdd.history(α, λ)))46proof47 simp [ordinalAdd.equation.limit]4849theorem ordinalAdd.history_membership (p α λ : Set)50 shows p ∈ ordinalAdd.history(α, λ) ↔ ∃ β ∈ λ, p = (β ↦ ordinalAdd(α, β))51proof52 simp [ordinalAdd.history.membership]5354theorem ordinalAdd.history_range (y α λ : Set)55 shows y ∈ Relation.range(ordinalAdd.history(α, λ)) ↔ ∃ β ∈ λ, y = ordinalAdd(α, β)56proof57 constructor58 . intro hy59 obtain ⟨β, hpair⟩ := range.membership_iff.forward with hy60 have member : (β, y) ∈ ordinalAdd.history(α, λ) := hpair61 simp [ordinalAdd.history_membership] at member62 obtain ⟨γ, hγ, shape⟩ := member63 have coordinates := orderedPair.injective with shape64 witness γ65 constructor66 . exact hγ67 . exact coordinates.right68 . intro h69 obtain ⟨β, hβ, shape⟩ := h70 have member : (β ↦ ordinalAdd(α, β)) ∈ ordinalAdd.history(α, λ) by simp [ordinalAdd.history_membership]71 rw shape72 exact range.contains at β, ordinalAdd(α, β), ordinalAdd.history(α, λ) with member7374theorem ordinalAdd.limit_membership (x : Set, α λ : Ordinal)75 requires limit : Limit(λ)76 shows x ∈ α + λ ↔ ∃ β ∈ λ, x ∈ ordinalAdd(α, β)77proof78 have equation := ordinalAdd.limit at α, λ with limit79 rw equation80 constructor81 . intro hx82 simp [set.union] at hx83 obtain ⟨stage, hStage, hxStage⟩ := hx84 obtain ⟨β, hβ, shape⟩ := ordinalAdd.history_range.forward with hStage85 witness β86 constructor87 . exact hβ88 . rw ← shape89 exact hxStage90 . intro h91 obtain ⟨β, hβ, hx⟩ := h92 have inRange : ordinalAdd(α, β) ∈ Relation.range(ordinalAdd.history(α, λ))93 apply ordinalAdd.history_range.backward94 exact ⟨β, hβ, rfl⟩95 exact union.contains with inRange, hx9697theorem ordinalAdd.ordinal (α : Ordinal, β : Set)98 shows β ∈ Ordinal → ordinalAdd(α, β) ∈ Ordinal99proof100 induction β using membership101 intros current ih hCurrent102 have cases := Ordinal.cases with hCurrent103 cases cases with zero | rest104 . rw zero105 rw ← nat.zero106 rw ordinalAdd.zero107 assumption108 . cases rest with successor | limit109 . obtain ⟨γ, hγ, shape⟩ := successor110 rw ← shape111 have γOrdinal := Ordinal.member with hCurrent, hγ112 rw ordinalAdd.next113 exact Ordinal.next with (ih with hγ, γOrdinal)114 . have equation := ordinalAdd.limit at α, current with limit115 rw equation116 apply Ordinal.union117 intros y hy118 obtain ⟨stage, hStage, shape⟩ := ordinalAdd.history_range.forward with hy119 rw shape120 exact ih with hStage, (Ordinal.member with hCurrent, hStage)121122theorem ordinalAdd.one (α : Ordinal)123 shows α + 1 = next(α)124proof125 have one : 1 = next(0) by simp [next.natural]126 rw [one, ordinalAdd.next, ordinalAdd.zero]127 rfl128129theorem ordinalAdd.zero_left (β : Set)130 shows β ∈ Ordinal → ordinalAdd(0, β) = β131proof132 induction β using membership133 intros current ih hCurrent134 have cases := Ordinal.cases with hCurrent135 cases cases with zero | rest136 . rw zero137 rw ← nat.zero138 exact ordinalAdd.zero at 0139 . cases rest with successor | limit140 . obtain ⟨γ, hγ, shape⟩ := successor141 rw ← shape142 have γOrdinal := Ordinal.member with hCurrent, hγ143 have step := ih with hγ, γOrdinal144 rw ordinalAdd.next145 rw step146 rfl147 . apply Subset.antisymmetric148 . intros x hx149 obtain ⟨stage, hStage, hxStage⟩ := ordinalAdd.limit_membership.forward at x, 0, current with limit, hx150 have step := ih with hStage, (Ordinal.member with hCurrent, hStage)151 rw step at hxStage152 exact Ordinal.member_subset at stage, current with hCurrent, hStage, x, hxStage153 . intros x hx154 apply ordinalAdd.limit_membership.backward at x, 0, current with limit155 witness next(x)156 have xOrdinal := Ordinal.member with hCurrent, hx157 constructor158 . exact limit.right.right with x, hx159 . have step := ih with (limit.right.right with x, hx), (Ordinal.next with xOrdinal)160 rw step161 exact next.contains at x162163theorem ordinalAdd.subset_left (α : Ordinal, β : Set)164 shows β ∈ Ordinal → α ⊆ ordinalAdd(α, β)165proof166 induction β using membership167 intros current ih hCurrent168 have cases := Ordinal.cases with hCurrent169 cases cases with zero | rest170 . rw zero171 rw ← nat.zero172 rw ordinalAdd.zero173 exact Subset.reflexive at α174 . cases rest with successor | limit175 . obtain ⟨γ, hγ, shape⟩ := successor176 rw ← shape177 have γOrdinal := Ordinal.member with hCurrent, hγ178 rw ordinalAdd.next179 have step := ih with hγ, γOrdinal180 intros x hx181 apply next.membership.backward182 left183 exact step with x, hx184 . intros x hx185 apply ordinalAdd.limit_membership.backward at x, α, current with limit186 have nonempty := Nonempty.of_ne_empty with limit.right.left187 simp [Nonempty] at nonempty188 obtain ⟨stage, hStage⟩ := nonempty189 witness stage190 constructor191 . exact hStage192 . exact ih with hStage, (Ordinal.member with hCurrent, hStage), x, hx193194theorem ordinalAdd.monotone (α β : Ordinal, γ : Set)195 shows γ ∈ Ordinal → β ∈ γ → ordinalAdd(α, β) ∈ ordinalAdd(α, γ)196proof197 induction γ using membership198 intros current ih hCurrent hBelow199 have cases := Ordinal.cases with hCurrent200 cases cases with zero | rest201 . exfalso202 rw zero at hBelow203 exact set.empty at β with hBelow204 . cases rest with successor | limit205 . obtain ⟨δ, hδ, shape⟩ := successor206 rw ← shape207 have δOrdinal := Ordinal.member with hCurrent, hδ208 rw ordinalAdd.next209 rw ← shape at hBelow210 simp [next.membership] at hBelow211 apply next.membership.backward212 cases hBelow with earlier | equal213 . left214 exact ih with hδ, δOrdinal, earlier215 . right216 rw equal217 rfl218 . apply ordinalAdd.limit_membership.backward at ordinalAdd(α, β), α, current with limit219 witness next(β)220 constructor221 . exact limit.right.right with β, hBelow222 . rw ordinalAdd.next223 exact next.contains at α + β224225226227theorem ordinalMul.zero (α : Ordinal)228 shows α * 0 = ∅229proof230 simp [ordinalMul, nat.zero]231232theorem ordinalMul.next (α β : Ordinal)233 shows α * next(β) = α * β + α234proof235 simp [ordinalMul.equation.successor]236237theorem ordinalMul.limit (α λ : Ordinal)238 requires h : Limit(λ)239 shows α * λ = ⋃(Relation.range(ordinalMul.history(α, λ)))240proof241 simp [ordinalMul.equation.limit]242243theorem ordinalMul.history_range (y α λ : Set)244 shows y ∈ Relation.range(ordinalMul.history(α, λ)) ↔ ∃ β ∈ λ, y = ordinalMul(α, β)245proof246 constructor247 . intro hy248 obtain ⟨β, hpair⟩ := range.membership_iff.forward with hy249 have member : (β, y) ∈ ordinalMul.history(α, λ) := hpair250 simp [ordinalMul.history.membership] at member251 obtain ⟨γ, hγ, shape⟩ := member252 have coordinates := orderedPair.injective with shape253 witness γ254 constructor255 . exact hγ256 . exact coordinates.right257 . intro h258 obtain ⟨β, hβ, shape⟩ := h259 have member : (β ↦ ordinalMul(α, β)) ∈ ordinalMul.history(α, λ) by simp [ordinalMul.history.membership]260 rw shape261 exact range.contains at β, ordinalMul(α, β), ordinalMul.history(α, λ) with member262263theorem ordinalMul.ordinal (α : Ordinal, β : Set)264 shows β ∈ Ordinal → ordinalMul(α, β) ∈ Ordinal265proof266 induction β using membership267 intros current ih hCurrent268 have cases := Ordinal.cases with hCurrent269 cases cases with zero | rest270 . rw zero271 rw ← nat.zero272 rw ordinalMul.zero273 exact Ordinal.empty274 . cases rest with successor | limit275 . obtain ⟨γ, hγ, shape⟩ := successor276 rw ← shape277 have γOrdinal := Ordinal.member with hCurrent, hγ278 rw ordinalMul.next279 have product := ih with hγ, γOrdinal280 exact ordinalAdd.ordinal at α * γ, α with product281 . have equation := ordinalMul.limit at α, current with limit282 rw equation283 apply Ordinal.union284 intros y hy285 obtain ⟨stage, hStage, shape⟩ := ordinalMul.history_range.forward with hy286 rw shape287 exact ih with hStage, (Ordinal.member with hCurrent, hStage)288289theorem ordinalMul.one (α : Ordinal)290 shows α * 1 = α291proof292 have one : 1 = next(0) by simp [next.natural]293 rw [one, ordinalMul.next, ordinalMul.zero]294 rw ← nat.zero295 exact ordinalAdd.zero_left at α with assumption296297298299theorem ordinalPow.zero (α : Ordinal)300 shows α ^ 0 = 1301proof302 simp [ordinalPow, nat.zero]303304theorem ordinalPow.next (α β : Ordinal)305 shows α ^ next(β) = α ^ β * α306proof307 simp [ordinalPow.equation.successor]308309theorem ordinalPow.limit (α λ : Ordinal)310 requires h : Limit(λ)311 shows α ^ λ = ⋃(Relation.range(ordinalPow.history(α, λ)))312proof313 simp [ordinalPow.equation.limit]314315theorem ordinalPow.history_range (y α λ : Set)316 shows y ∈ Relation.range(ordinalPow.history(α, λ)) ↔ ∃ β ∈ λ, y = ordinalPow(α, β)317proof318 constructor319 . intro hy320 obtain ⟨β, hpair⟩ := range.membership_iff.forward with hy321 have member : (β, y) ∈ ordinalPow.history(α, λ) := hpair322 simp [ordinalPow.history.membership] at member323 obtain ⟨γ, hγ, shape⟩ := member324 have coordinates := orderedPair.injective with shape325 witness γ326 constructor327 . exact hγ328 . exact coordinates.right329 . intro h330 obtain ⟨β, hβ, shape⟩ := h331 have member : (β ↦ ordinalPow(α, β)) ∈ ordinalPow.history(α, λ) by simp [ordinalPow.history.membership]332 rw shape333 exact range.contains at β, ordinalPow(α, β), ordinalPow.history(α, λ) with member334335theorem ordinalPow.ordinal (α : Ordinal, β : Set)336 shows β ∈ Ordinal → ordinalPow(α, β) ∈ Ordinal337proof338 induction β using membership339 intros current ih hCurrent340 have cases := Ordinal.cases with hCurrent341 cases cases with zero | rest342 . rw zero343 rw ← nat.zero344 rw ordinalPow.zero345 exact Ordinal.natural at 1346 . cases rest with successor | limit347 . obtain ⟨γ, hγ, shape⟩ := successor348 rw ← shape349 have γOrdinal := Ordinal.member with hCurrent, hγ350 rw ordinalPow.next351 have power := ih with hγ, γOrdinal352 exact ordinalMul.ordinal at α ^ γ, α with power353 . have equation := ordinalPow.limit at α, current with limit354 rw equation355 apply Ordinal.union356 intros y hy357 obtain ⟨stage, hStage, shape⟩ := ordinalPow.history_range.forward with hy358 rw shape359 exact ih with hStage, (Ordinal.member with hCurrent, hStage)360361theorem ordinalMul.one_left (β : Set)362 shows β ∈ Ordinal → ordinalMul(1, β) = β363proof364 induction β using membership365 intros current ih hCurrent366 have cases := Ordinal.cases with hCurrent367 cases cases with zero | rest368 . rw zero369 have base := ordinalMul.zero at 1370 rw nat.zero at base371 exact base372 . cases rest with successor | limit373 . obtain ⟨γ, hγ, shape⟩ := successor374 rw ← shape375 have γOrdinal := Ordinal.member with hCurrent, hγ376 have step := ih with hγ, γOrdinal377 rw [ordinalMul.next, step]378 exact ordinalAdd.one at γ379 . have oneOrdinal := Ordinal.natural at 1380 apply Subset.antisymmetric381 . intros x hx382 have equation := ordinalMul.limit at 1, current with limit383 rw equation at hx384 simp [set.union] at hx385 obtain ⟨stage, hStage, hxStage⟩ := hx386 obtain ⟨earlier, hEarlier, shape⟩ := ordinalMul.history_range.forward with hStage387 have step := ih with hEarlier, (Ordinal.member with hCurrent, hEarlier)388 rw [shape, step] at hxStage389 exact Ordinal.member_subset at earlier, current with hCurrent, hEarlier, x, hxStage390 . intros x hx391 have equation := ordinalMul.limit at 1, current with limit392 rw equation393 have xOrdinal := Ordinal.member with hCurrent, hx394 have nextIn := limit.right.right with x, hx395 have step := ih with nextIn, (Ordinal.next with xOrdinal)396 have inRange : ordinalMul(1, next(x)) ∈ Relation.range(ordinalMul.history(1, current))397 apply ordinalMul.history_range.backward398 exact ⟨next(x), nextIn, rfl⟩399 rw step at inRange400 exact union.contains with inRange, (next.contains at x)401402theorem ordinalPow.one (α : Ordinal)403 shows α ^ 1 = α404proof405 have one : 1 = next(0) by simp [next.natural]406 rw [one, ordinalPow.next, ordinalPow.zero]407 exact ordinalMul.one_left at α408