Grace/Cumulus/Set/Foundation.g17

Open in Workbench Download source

Imports

Relation

Declarations

• layer def
• layers def
• closure def
• membershipOn def
• layer.zero theorem derivation
• layer.next theorem derivation
• omega.natural theorem derivation
• omega.successor theorem derivation
• closure.contains theorem derivation
• closure.transitive theorem derivation
• membershipOn.relates theorem derivation
• membershipOn.relation theorem derivation
• membershipOn.wellFounded theorem derivation
• membership.induction_reflexive theorem derivation
• membership.irreflexive theorem derivation

Source

1-- Derived consequences of Foundation2-- 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.Foundation8import Relation910-- The nth downward membership layer starting from {x}.11def layer (x : Set, n : Nat) → Set12  | x, zero => {x}13  | x, succ(n) => ⋃(layer(x, n))1415-- Replacement collects all finite layers; their union is the16-- transitive closure containing x.17def layers (x : Set) : Set := { layer(x, n) | n ∈ ℕ }18def closure (x : Set) : Set := ⋃(layers(x))1920-- Membership restricted to a set, represented as a relation set.21def membershipOn (A : Set) : Set := { p ∈ A × A | ∃ x ∈ A, ∃ y ∈ A, x ∈ y ∧ p = (x, y) }2223theorem layer.zero (x : Set)24  shows layer(x, 0) = {x}25proof26  simp [layer, nat.zero]2728theorem layer.next (x : Set, n : Nat)29  shows layer(x, succ(n)) = ⋃(layer(x, n))30proof31  simp [layer]3233theorem omega.natural (n : Set)34  requires hn : n ∈ ℕ35  shows Nat(n)36proof37  simp [nat.omega]3839theorem omega.successor (n : Set)40  requires hn : n ∈ ℕ41  shows succ(n) ∈ ℕ42proof43  have hnat := omega.natural with hn44  have infinity := set.infinity45  cases infinity with hzeroIn ∧ hsuccessor46  specialize hsuccessor with n, hn47  have hsucc := nat.succ with hnat48  rwa hsucc4950theorem closure.contains (x : Set)51  shows x ∈ closure(x)52proof53  unfold closure54  apply set.union.backward55  witness layer(x, 0)56  constructor57  apply layers.membership.backward58  witness 059  constructor60  have infinity := set.infinity61  cases infinity with hzeroIn ∧ hsuccessor62  rwa nat.zero63  rfl64  have hzero := layer.zero at x65  rw hzero66  exact singleton.self6768theorem closure.transitive (x : Set)69  shows ∀ y ∈ closure(x), ∀ z ∈ y, z ∈ closure(x)70proof71  intros y hy z hz72  unfold closure at hy73  simp [set.union] at hy74  obtain ⟨L, hLy⟩ := hy75  cases hLy with hL ∧ hyL76  simp [layers] at hL77  obtain ⟨n, hnLayer⟩ := hL78  cases hnLayer with hn ∧ hLayer79  unfold closure80  apply set.union.backward81  witness layer(x, succ(n))82  constructor83  apply layers.membership.backward84  witness succ(n)85  constructor86  exact omega.successor with hn87  rfl88  have hnext := layer.next at x, n89  rw [hnext, hLayer]90  exact set.union.backward with ⟨y, hyL, hz⟩9192theorem membershipOn.relates (a b A : Set)93  requires ha : a ∈ A94  requires hb : b ∈ A95  shows relates(membershipOn(A), a, b) ↔ a ∈ b96proof97  constructor98  . intro h99    unfold relates at h100    simp [membershipOn] at h101    obtain ⟨hproduct, x, hxA, y, hyA, hxy, hpair⟩ := h102    obtain ⟨hax, hby⟩ := orderedPair.injective with hpair103    rw hax104    rwa hby105  . intro h106    unfold relates107    exact membershipOn.backward with ⟨(product.pair with ha, hb), a, ha, b, hb, h, rfl⟩108109theorem membershipOn.relation (A : Set)110  shows RelationBetween(membershipOn(A), A, A)111proof112  simp [RelationBetween, Subset]113114theorem membershipOn.wellFounded (A : Set)115  shows wellFoundedOn(membershipOn(A), A)116proof117  intros s hs118  cases hs with hsubset ∧ hnonempty119  obtain ⟨m, hmMinimal⟩ := set.foundation with hnonempty120  cases hmMinimal with hm ∧ hminimal121  witness m122  constructor123  exact hm124  intros y hy hrel125  have hmA := hsubset with hm126  have hyA := hsubset with hy127  have relation := membershipOn.relates with hyA, hmA128  simp [relation] at hrel129  exact hminimal with y, hrel, hy130131-- This tiny theorem is a regression test for the derived induction tactic.132theorem membership.induction_reflexive (x : Set)133  shows x = x134proof135  simp136137theorem membership.irreflexive (x : Set)138  shows ¬x ∈ x139proof140  induction x using membership141  intros current ih hSelf142  exact ih with hSelf, hSelf143