Grace/Cumulus/Set/Order.g17

Open in Workbench Download source

Imports

Cumulus.Relation · Set · Function

Declarations

Source

1-- Order theory2-- 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.Order8import Cumulus.Relation9import Set10import Function1112predicate IsLinearOrder (A r : Set) := IsPartialOrder(A, r) ∧ (∀ x ∈ A, ∀ y ∈ A, relates(r, x, y) ∨ relates(r, y, x))13predicate StrictOrder (A r : Set) := RelationBetween(r, A, A) ∧ (IrreflexiveOn(A, r) ∧ TransitiveOn(A, r))14predicate StrictLinearOrder (A r : Set) := StrictOrder(A, r) ∧ ConnectedOn(A, r)15predicate LowerBound (A r S a : Set) := a ∈ A ∧ (S ⊆ A) ∧ (∀ x ∈ S, relates(r, a, x))16predicate UpperBound (A r S a : Set) := a ∈ A ∧ (S ⊆ A) ∧ (∀ x ∈ S, relates(r, x, a))17predicate Least (A r S a : Set) := a ∈ S ∧ LowerBound(A, r, S, a)18predicate Greatest (A r S a : Set) := a ∈ S ∧ UpperBound(A, r, S, a)19predicate Comparable (r x y : Set) := relates(r, x, y) ∨ relates(r, y, x)20predicate Chain (A r C : Set) :=21  (C ⊆ A) ∧ (∀ x ∈ C, ∀ y ∈ C, Comparable(r, x, y))22predicate ChainOfChains (A r S : Set) :=23  (∀ C ∈ S, Chain(A, r, C)) ∧24  (∀ C ∈ S, ∀ D ∈ S, ((C ⊆ D) ∨ (D ⊆ C)))25predicate Maximal (A r m : Set) :=26  m ∈ A ∧ (∀ x ∈ A, relates(r, m, x) → x = m)27predicate ZornCondition (A r : Set) :=28  IsPartialOrder(A, r) ∧29  (∀ C, Chain(A, r, C) → ∃ u, UpperBound(A, r, C, u))30predicate WellOrder (A r : Set) := StrictLinearOrder(A, r) ∧ wellFoundedOn(r, A)31predicate InitialSegment (A r I : Set) :=32  (I ⊆ A) ∧33  (∀ x ∈ I, ∀ y ∈ A, relates(r, y, x) → y ∈ I)34predicate ProperInitialSegment (A r I : Set) := InitialSegment(A, r, I) ∧ I ≠ A35predicate OrderEmbedding (f A r B s : Set) :=36  InjectiveBetween(f, A, B) ∧37  (∀ x ∈ A, ∀ y ∈ A, ∀ u ∈ B, ∀ v ∈ B,38    relates(f, x, u) → relates(f, y, v) → (relates(r, x, y) ↔ relates(s, u, v)))39predicate OrderIsomorphism (f A r B s : Set) :=40  BijectiveBetween(f, A, B) ∧41  (∀ x ∈ A, ∀ y ∈ A, ∀ u ∈ B, ∀ v ∈ B,42    relates(f, x, u) → relates(f, y, v) → (relates(r, x, y) ↔ relates(s, u, v)))4344theorem WellOrder.strict_linear (A r : Set)45  requires h : WellOrder(A, r)46  shows StrictLinearOrder(A, r)47proof48  simp [WellOrder]4950theorem WellOrder.well_founded (A r : Set)51  requires h : WellOrder(A, r)52  shows wellFoundedOn(r, A)53proof54  simp [WellOrder]5556theorem InitialSegment.subset (A r I : Set)57  requires h : InitialSegment(A, r, I)58  shows (I ⊆ A)59proof60  simp [InitialSegment]6162theorem InitialSegment.empty (A r : Set)63  shows InitialSegment(A, r, empty)64proof65  simp [InitialSegment, Subset, set.empty]6667theorem InitialSegment.full (A r : Set)68  shows InitialSegment(A, r, A)69proof70  simp [InitialSegment, Subset]7172theorem ProperInitialSegment.initial (A r I : Set)73  requires h : ProperInitialSegment(A, r, I)74  shows InitialSegment(A, r, I)75proof76  simp [ProperInitialSegment]7778theorem OrderIsomorphism.bijective (f A r B s : Set)79  requires h : OrderIsomorphism(f, A, r, B, s)80  shows BijectiveBetween(f, A, B)81proof82  simp [OrderIsomorphism]8384theorem OrderIsomorphism.embedding (f A r B s : Set)85  requires h : OrderIsomorphism(f, A, r, B, s)86  shows OrderEmbedding(f, A, r, B, s)87proof88  rcases h with ⟨bijective, ordered⟩89  constructor90  . have injective := Bijective.injective at f, A, B91    exact injective with bijective92  . exact ordered9394theorem IsLinearOrder.partial (A r : Set)95  requires h : IsLinearOrder(A, r)96  shows IsPartialOrder(A, r)97proof98  rcases h with ⟨partial, total⟩99  exact partial100101theorem IsPartialOrder.reflexive (A r : Set)102  requires h : IsPartialOrder(A, r)103  shows ReflexiveOn(A, r)104proof105  simp [IsPartialOrder, IsPreorder]106107theorem IsPartialOrder.transitive (A r : Set)108  requires h : IsPartialOrder(A, r)109  shows TransitiveOn(A, r)110proof111  simp [IsPartialOrder, IsPreorder]112113theorem IsPartialOrder.antisymmetric (A r : Set)114  requires h : IsPartialOrder(A, r)115  shows AntisymmetricOn(A, r)116proof117  simp [IsPartialOrder]118119theorem Chain.subset (A r C : Set)120  requires h : Chain(A, r, C)121  shows (C ⊆ A)122proof123  simp [Chain]124125theorem Chain.empty (A r : Set)126  shows Chain(A, r, empty)127proof128  simp [Chain, Subset, set.empty]129130theorem Chain.singleton (A r x : Set)131  requires order : IsPartialOrder(A, r)132  requires hx : x ∈ A133  shows Chain(A, r, {x})134proof135  constructor136    intros y hy137    have equal := singleton.membership.forward with hy138    rwa equal139  . intros y hy z hz140    have equalY := singleton.membership.forward with hy141    have equalZ := singleton.membership.forward with hz142    rw [equalY, equalZ]143    left144    have reflexive := IsPartialOrder.reflexive with order145    exact reflexive with x, hx146147theorem Chain.union (A r S : Set)148  requires family : ChainOfChains(A, r, S)149  shows Chain(A, r, ⋃(S))150proof151  rcases family with ⟨chains, nested⟩152  constructor153  . apply union.subset154    intros C0 hC0S155    exact Chain.subset with (chains with C0, hC0S)156  . intros x hx y hy157    simp [set.union] at hx158    obtain ⟨C1, hC1S, hxC1⟩ := hx159    simp [set.union] at hy160    obtain ⟨D1, hD1S, hyD1⟩ := hy161    have alternatives := nested with C1, hC1S, D1, hD1S162    cases alternatives with subsetCD | subsetDC163    . obtain ⟨subsetD, comparableD⟩ := chains with D1, hD1S164      exact comparableD with x, (subsetCD with x, hxC1), y, hyD1165    . obtain ⟨subsetC, comparableC⟩ := chains with C1, hC1S166      exact comparableC with x, hxC1, y, (subsetDC with y, hyD1)167168theorem ZornCondition.order (A r : Set)169  requires h : ZornCondition(A, r)170  shows IsPartialOrder(A, r)171proof172  simp [ZornCondition]173174theorem ZornCondition.upper_bound (A r C : Set)175  requires h : ZornCondition(A, r)176  requires chain : Chain(A, r, C)177  shows ∃ u, UpperBound(A, r, C, u)178proof179  rcases h with ⟨order, bounded⟩180  exact bounded with C, chain181182theorem ZornCondition.nonempty (A r : Set)183  requires h : ZornCondition(A, r)184  shows Nonempty(A)185proof186  have emptyChain := Chain.empty at A, r187  obtain ⟨u, huA, _, _⟩ := ZornCondition.upper_bound with h, emptyChain188  refine ⟨u, huA⟩189190theorem StrictOrder.irreflexive (A r : Set)191  requires h : StrictOrder(A, r)192  shows IrreflexiveOn(A, r)193proof194  simp [StrictOrder]195196theorem StrictOrder.transitive (A r : Set)197  requires h : StrictOrder(A, r)198  shows TransitiveOn(A, r)199proof200  simp [StrictOrder]201202theorem StrictLinearOrder.strict (A r : Set)203  requires h : StrictLinearOrder(A, r)204  shows StrictOrder(A, r)205proof206  simp [StrictLinearOrder]207208theorem StrictLinearOrder.connected (A r : Set)209  requires h : StrictLinearOrder(A, r)210  shows ConnectedOn(A, r)211proof212  simp [StrictLinearOrder]213214theorem StrictLinearOrder.relation (A r : Set)215  requires h : StrictLinearOrder(A, r)216  shows RelationBetween(r, A, A)217proof218  simp [StrictLinearOrder, StrictOrder]219220theorem StrictLinearOrder.irreflexive (A r : Set)221  requires h : StrictLinearOrder(A, r)222  shows IrreflexiveOn(A, r)223proof224  simp [StrictLinearOrder, StrictOrder]225226theorem StrictLinearOrder.transitive (A r : Set)227  requires h : StrictLinearOrder(A, r)228  shows TransitiveOn(A, r)229proof230  simp [StrictLinearOrder, StrictOrder]231232theorem Ordinal.membership_irreflexive (α : Set)233  requires ordinal : α ∈ Ordinal234  shows IrreflexiveOn(α, membershipOn(α))235proof236  intros x hx related237  have member := membershipOn.relates with hx, hx238  apply membership.irreflexive at x239  apply member.forward240  exact related241242theorem Ordinal.membership_transitive (α : Set)243  requires ordinal : α ∈ Ordinal244  shows TransitiveOn(α, membershipOn(α))245proof246  intros x hx y hy z hz xyRelated yzRelated247  have xy := membershipOn.relates with hx, hy248  have xInY := xy.forward with xyRelated249  have yz := membershipOn.relates with hy, hz250  have yInZ := yz.forward with yzRelated251  have zOrdinal := Ordinal.member with ordinal, hz252  have zTransitive := Ordinal.transitive with zOrdinal, y, yInZ253  have xInZ := zTransitive with xInY254  have xz := membershipOn.relates with hx, hz255  apply xz.backward256  exact xInZ257258theorem Ordinal.membership_connected (α : Set)259  requires ordinal : α ∈ Ordinal260  shows ConnectedOn(α, membershipOn(α))261proof262  intros x hx y hy unequal263  have xOrdinal := Ordinal.member with ordinal, hx264  have yOrdinal := Ordinal.member with ordinal, hy265  have comparison := Ordinal.trichotomy with xOrdinal, y, yOrdinal266  cases comparison with xInY | rest267  . left268    have related := membershipOn.relates with hx, hy269    apply related.backward270    exact xInY271  . cases rest with equal | yInX272    . exfalso273      apply unequal274      exact equal275    . right276      have related := membershipOn.relates with hy, hx277      apply related.backward278      exact yInX279280theorem Ordinal.membership_strict_linear (α : Set)281  requires ordinal : α ∈ Ordinal282  shows StrictLinearOrder(α, membershipOn(α))283proof284  constructor285    constructor286    . exact membershipOn.relation at α287    . constructor288      . exact Ordinal.membership_irreflexive at α289      . exact Ordinal.membership_transitive at α290  . exact Ordinal.membership_connected at α291292theorem Ordinal.well_order (α : Set)293  requires ordinal : α ∈ Ordinal294  shows WellOrder(α, membershipOn(α))295proof296  simp [WellOrder, Ordinal.membership_strict_linear, membershipOn.wellFounded]297298theorem Ordinal.member_initial_segment (α β : Set)299  requires ordinal : α ∈ Ordinal300  requires member : β ∈ α301  shows InitialSegment(α, membershipOn(α), β)302proof303  constructor304  . have transitive := Ordinal.transitive with ordinal305    exact transitive with β, member306  . intros x hx y hy related307    have alphaTransitive := Ordinal.transitive with ordinal, β, member308    have xInAlpha := alphaTransitive with hx309    have yx := membershipOn.relates with hy, xInAlpha310    have yInX := yx.forward with related311    have betaOrdinal := Ordinal.member with ordinal, member312    have betaTransitive := Ordinal.transitive with betaOrdinal, x, hx313    exact betaTransitive with y, yInX314315theorem Ordinal.member_proper_initial_segment (α β : Set)316  requires ordinal : α ∈ Ordinal317  requires member : β ∈ α318  shows ProperInitialSegment(α, membershipOn(α), β)319proof320  constructor321  . have initial := Ordinal.member_initial_segment at α, β322    exact initial with member323  . intro equal324    rw equal at member325    exact membership.irreflexive with member326327theorem Least.unique (A r S a b : Set)328  requires order : IsPartialOrder(A, r)329  requires ha : Least(A, r, S, a)330  requires hb : Least(A, r, S, b)331  shows a = b332proof333  rcases order with ⟨preorder, antisymmetric⟩334  rcases ha with ⟨haS, haA, hSA, haLe⟩335  rcases hb with ⟨hbS, hbA, hSB, hbLe⟩336  specialize haLe with b, hbS337  specialize hbLe with a, haS338  exact antisymmetric with a, haA, b, hbA, haLe, hbLe339340theorem Greatest.unique (A r S a b : Set)341  requires order : IsPartialOrder(A, r)342  requires ha : Greatest(A, r, S, a)343  requires hb : Greatest(A, r, S, b)344  shows a = b345proof346  rcases order with ⟨preorder, antisymmetric⟩347  rcases ha with ⟨haS, haA, hSA, haGe⟩348  rcases hb with ⟨hbS, hbA, hSB, hbGe⟩349  specialize haGe with b, hbS350  specialize hbGe with a, haS351  exact antisymmetric with a, haA, b, hbA, hbGe, haGe352353-- Inclusion is a partial order on any family of sets.354def inclusionOrder (F : Set) : Set :=355  {p ∈ F × F | ∃ C ∈ F, ∃ D ∈ F, p = (C, D) ∧ C ⊆ D}356357theorem inclusionOrder.relates (F C D : Set)358  requires hC : C ∈ F359  requires hD : D ∈ F360  shows relates(inclusionOrder(F), C, D) ↔ C ⊆ D361proof362  constructor363  . intro related364    unfold relates at related365    obtain ⟨bounded, U, hU, V, hV, equal, subset⟩ := inclusionOrder.membership.forward with related366    obtain ⟨sameC, sameD⟩ := orderedPair.injective with equal367    rw sameC368    rwa sameD369  . intro subsetCD370    have pair := product.pair with hC, hD371    unfold relates372    exact inclusionOrder.membership.backward with ⟨pair, C, hC, D, hD, rfl, subsetCD⟩373374theorem inclusionOrder.partial (F : Set)375  shows IsPartialOrder(F, inclusionOrder(F))376proof377  constructor378    constructor379    . settle with RelationBetween, Subset, inclusionOrder380    . constructor381        intros C hC382        exact inclusionOrder.relates.backward with hC, hC, (Subset.reflexive at C)383        intros C hC D hD E hE cd de384        have subsetCD := inclusionOrder.relates.forward with hC, hD, cd385        have subsetDE := inclusionOrder.relates.forward with hD, hE, de386        exact inclusionOrder.relates.backward with hC, hE, (Subset.transitive with subsetCD, subsetDE)387    intros C hC D hD cd dc388    have subsetCD := inclusionOrder.relates.forward with hC, hD, cd389    have subsetDC := inclusionOrder.relates.forward with hD, hC, dc390    exact Subset.antisymmetric with subsetCD, subsetDC391392theorem Chain.adjoin_upper (A r C u : Set)393  requires order : IsPartialOrder(A, r)394  requires chain : Chain(A, r, C)395  requires bound : UpperBound(A, r, C, u)396  shows Chain(A, r, C ∪ {u})397proof398  have reflexive := IsPartialOrder.reflexive with order399  rcases chain with ⟨subsetC, comparable⟩400  rcases bound with ⟨uInA, boundedC, upper⟩401  have singletonSubset : {u} ⊆ A by simp402  have bounded := union2.subset with subsetC, singletonSubset403  constructor404  . exact bounded405  . intros x hx y hy406    have xCases := union2.membership.forward with hx407    have yCases := union2.membership.forward with hy408    cases xCases with xC | xu409    . cases yCases with yC | yu410      . exact comparable with x, xC, y, yC411      . obtain rfl := singleton.membership.forward with yu412        left413        exact upper with x, xC414    . obtain rfl := singleton.membership.forward with xu415      cases yCases with yC | yu416        right417        exact upper with y, yC418      . obtain rfl := singleton.membership.forward with yu419        left420        exact reflexive with u, uInA421