From f330b3c37f8a21e7ffcae9eecf89d3c0546dcbc0 Mon Sep 17 00:00:00 2001 From: VTrelat Date: Thu, 25 Jun 2026 11:16:43 +0200 Subject: [PATCH 1/4] chore: bump toolchain and mathlib to v4.31.0 --- lake-manifest.json | 29 +++++++++++++++-------------- lakefile.toml | 2 +- lean-toolchain | 2 +- 3 files changed, 17 insertions(+), 16 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 706085d..e560155 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,21 +1,21 @@ -{"version": "1.1.0", +{"version": "1.2.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a3a10db0e9d66acbebf76c5e6a135066525ac900", + "rev": "fabf563a7c95a166b8d7b6efca11c8b4dc9d911f", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.27.0", + "inputRev": "v4.31.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "009dc1e6f2feb2c96c081537d80a0905b2c6498f", + "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28", + "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8f497d55985a189cea8020d9dc51260af1e41ad2", + "rev": "5c7542ed018c78194f1e2b903eaf6a792b74c03d", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,17 +45,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c04225ee7c0585effbd933662b3151f01b600e40", + "rev": "24b0d9dc081c5423f8eec7e866c441e5184f29d9", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.85", + "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "cb837cc26236ada03c81837bebe0acd9c70ced7d", + "rev": "e3cb2f741431ce31bf73549fb52316a57368b06f", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "bd58c9efe2086d56ca361807014141a860ddbf8c", + "rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a", + "rev": "fa08db58b30eb033edcdab331bba000827f9f785", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,11 +85,12 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "55c37290ff6186e2e965d68cf853a57c0702db82", + "rev": "92564e5770e4d09f2d86dfbf8ada1e9c715b384c", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.27.0", + "inputRev": "v4.31.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "ZFLean", - "lakeDir": ".lake"} + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lakefile.toml b/lakefile.toml index 819228d..754564c 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -12,7 +12,7 @@ maxSynthPendingDepth = 3 [[require]] name = "mathlib" scope = "leanprover-community" -rev = "v4.27.0" +rev = "v4.31.0" [[lean_lib]] name = "ZFLean" diff --git a/lean-toolchain b/lean-toolchain index 2bb276a..133a3f7 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.27.0 \ No newline at end of file +leanprover/lean4:v4.31.0 \ No newline at end of file From dff89a25f04a0f06726c3c6ebc92cec8cece17a6 Mon Sep 17 00:00:00 2001 From: VTrelat Date: Thu, 25 Jun 2026 11:19:04 +0200 Subject: [PATCH 2/4] fix: adapt to v4.31.0 breaking changes --- ZFLean/Booleans.lean | 4 ++-- ZFLean/Def.lean | 2 +- ZFLean/Functions.lean | 37 +++++++++++++++++++------------------ ZFLean/Integers.lean | 16 ++++++++-------- ZFLean/Isomorphisms.lean | 37 ++++++++++++++++++------------------- ZFLean/Naturals.lean | 20 +++++++++----------- ZFLean/Sum.lean | 6 +++--- 7 files changed, 60 insertions(+), 62 deletions(-) diff --git a/ZFLean/Booleans.lean b/ZFLean/Booleans.lean index bfeb0f7..5382b5d 100644 --- a/ZFLean/Booleans.lean +++ b/ZFLean/Booleans.lean @@ -33,7 +33,7 @@ infix:70 " Δ " => symmDiff @[simp] theorem mem_symmDiff (x p q : ZFSet) : x ∈ p Δ q ↔ (x ∈ p ∧ x ∉ q) ∨ (x ∈ q ∧ x ∉ p) := by - simp only [symmDiff, mem_union, mem_diff] + simp only [symmDiff, mem_union, mem_sdiff] @[simp] theorem symmDiff_empty (p : ZFSet) : p Δ ∅ = p := by @@ -506,7 +506,7 @@ theorem ofBool_decide_eq_false_iff {P : Prop} [Decidable P] : ofBool (decide P) rw [Bool.decide_iff] at hP contradiction -instance : ZFBool ≃ Bool where +def equivBool : ZFBool ≃ Bool where toFun := toBool invFun := ofBool left_inv := of_Bool_toBool diff --git a/ZFLean/Def.lean b/ZFLean/Def.lean index ff73c42..62948f7 100644 --- a/ZFLean/Def.lean +++ b/ZFLean/Def.lean @@ -111,7 +111,7 @@ infix:70 " Δ " => symmDiff @[simp] theorem mem_symmDiff (x p q : ZFSet) : x ∈ p Δ q ↔ (x ∈ p ∧ x ∉ q) ∨ (x ∈ q ∧ x ∉ p) := by - simp only [symmDiff, mem_union, mem_diff] + simp only [symmDiff, mem_union, mem_sdiff] @[simp] theorem symmDiff_empty (p : ZFSet) : p Δ ∅ = p := by diff --git a/ZFLean/Functions.lean b/ZFLean/Functions.lean index 0abecbc..9313c5e 100644 --- a/ZFLean/Functions.lean +++ b/ZFLean/Functions.lean @@ -1698,9 +1698,10 @@ theorem IsFunc.range_eq_of_surjective {f A B : ZFSet} (hf : IsFunc A B f) · exact ZFSet.mem_dom (is_func_is_pfunc hf) xy · exact xy -attribute [-instance] SetLike.instPartialOrder +attribute [-instance] ZFSet.instPartialOrder -instance instPreorder_mem_Nat {n : ZFSet} (hn : n ∈ Nat) : Preorder {x // x ∈ n} where +@[reducible] +def instPreorder_mem_Nat {n : ZFSet} (hn : n ∈ Nat) : Preorder {x // x ∈ n} where le := fun ⟨a, ha⟩ ⟨b, hb⟩ ↦ (⟨a, ZFNat.mem_Nat_of_mem_mem_Nat hn ha⟩ : ZFNat) ≤ (⟨b, ZFNat.mem_Nat_of_mem_mem_Nat hn hb⟩ : ZFNat) @@ -1986,7 +1987,7 @@ theorem IsFinite.union {A B : ZFSet} (finA : A.IsFinite) (finB : B.IsFinite) : (A ∪ B).IsFinite := by have : A ∪ B = (A \ B) ∪ B := by ext1 z - simp_rw [mem_union, mem_diff] + simp_rw [mem_union, mem_sdiff] constructor · rintro (hA | hB) · by_cases hB : z ∈ B @@ -1999,11 +2000,11 @@ theorem IsFinite.union {A B : ZFSet} (finA : A.IsFinite) (finB : B.IsFinite) : rw [this] have : (A \ B) ∩ B = ∅ := by ext1 z - rw [mem_inter, mem_diff, and_assoc] + rw [mem_inter, mem_sdiff, and_assoc] simp only [not_and_self, and_false, notMem_empty] apply IsFinite.disjoint_union (IsFinite.subset finA ?_) finB this intro z hz - rw [mem_diff] at hz + rw [mem_sdiff] at hz exact hz.1 theorem IsFinite.inter {A B : ZFSet} (fin : A.IsFinite ∨ B.IsFinite) : @@ -2021,7 +2022,7 @@ theorem IsFinite.diff {A B : ZFSet} (finA : A.IsFinite) : (A \ B).IsFinite := by apply IsFinite.subset finA intro z hz - rw [mem_diff] at hz + rw [mem_sdiff] at hz exact hz.1 @[induction_eliminator] @@ -2054,7 +2055,7 @@ def ZFFinSet.inductionOn {P : ZFFinSet → Prop} and_intros · intro z hz unfold fS' at hz - rw [mem_diff, mem_singleton] at hz + rw [mem_sdiff, mem_singleton] at hz obtain ⟨x, xS, y, yS, rfl⟩ := mem_prod.mp <| fS_fun.1 hz.1 rw [pair_inj] at hz rw [pair_mem_prod] @@ -2065,7 +2066,7 @@ def ZFFinSet.inductionOn {P : ZFFinSet → Prop} nomatch hz.2 (pair_inj.mp rfl) · and_intros · unfold S' - rw [mem_diff, mem_singleton] + rw [mem_sdiff, mem_singleton] and_intros · exact xS · rintro rfl @@ -2076,13 +2077,13 @@ def ZFFinSet.inductionOn {P : ZFFinSet → Prop} nomatch mem_irrefl _ yS · exact yS · intro z zS - rw [mem_diff, mem_singleton] at zS + rw [mem_sdiff, mem_singleton] at zS obtain ⟨w, hw, w_unq⟩ := fS_fun.2 z zS.1 exists w and_intros · unfold fS' beta_reduce - rw [mem_diff, mem_singleton, pair_inj] + rw [mem_sdiff, mem_singleton, pair_inj] and_intros · exact hw · rw [not_and_or] @@ -2090,24 +2091,24 @@ def ZFFinSet.inductionOn {P : ZFFinSet → Prop} exact zS.2 · intro w' hw' unfold fS' at hw' - rw [mem_diff, mem_singleton, pair_inj] at hw' + rw [mem_sdiff, mem_singleton, pair_inj] at hw' exact w_unq w' hw'.left have : fS'.IsInjective := by intro x y z xS' yS' zn xy yz apply fS_inj x y z - · exact mem_diff.mp xS' |>.1 - · exact mem_diff.mp yS' |>.1 + · exact mem_sdiff.mp xS' |>.1 + · exact mem_sdiff.mp yS' |>.1 · exact mem_insert_of_mem n zn all_goals unfold fS' at xy - rw [mem_diff, mem_singleton] at xy yz + rw [mem_sdiff, mem_singleton] at xy yz · exact xy.1 · exact yz.1 specialize IH S' fS' (mem_funs.mpr S'_is_func) S'_fin S'_is_func this have : S = Insert.insert a S' := by classical unfold S' ext1 z - simp_rw [mem_insert_iff, mem_diff, mem_singleton, or_and_left, Classical.em, and_true] + simp_rw [mem_insert_iff, mem_sdiff, mem_singleton, or_and_left, Classical.em, and_true] constructor · exact Or.inr · rintro (rfl | hz) @@ -2115,7 +2116,7 @@ def ZFFinSet.inductionOn {P : ZFFinSet → Prop} · exact hz specialize insert _ a IH (by unfold S' - rw [mem_diff, mem_singleton, not_and_or, not_not] + rw [mem_sdiff, mem_singleton, not_and_or, not_not] right; rfl) conv at insert => enter [1,1] @@ -2427,7 +2428,7 @@ theorem IsFinite.powerset {A : ZFSet} (finA : A.IsFinite) : A.powerset.IsFinite specialize IH ⟨S \ ({s} : ZFSet), IsFinite.diff finA⟩ have : S.val = Insert.insert s (S.val \ ({s} : ZFSet)) := by ext - simp only [mem_insert_iff, mem_diff, mem_singleton, or_and_left, + simp only [mem_insert_iff, mem_sdiff, mem_singleton, or_and_left, Classical.em, and_true, iff_or_self] rintro rfl assumption @@ -2439,7 +2440,7 @@ theorem IsFinite.powerset {A : ZFSet} (finA : A.IsFinite) : A.powerset.IsFinite rw [this] at cardS dsimp at cardS have := Card.insert (S := ⟨S.val \ ({s} : ZFSet), IsFinite.diff finA⟩) (x := s) (by - rw [mem_diff, mem_singleton, not_and_or, not_not] + rw [mem_sdiff, mem_singleton, not_and_or, not_not] right; rfl) rw [this, ZFNat.add_right_cancel] at cardS clear this diff --git a/ZFLean/Integers.lean b/ZFLean/Integers.lean index 34cd10e..aae51c6 100644 --- a/ZFLean/Integers.lean +++ b/ZFLean/Integers.lean @@ -634,7 +634,7 @@ lemma induction_pos {P : ZFInt → Prop} (n : ZFInt) (n_pos : 0 ≤ n) induction n using Quotient.ind rename_i n obtain ⟨n, m⟩ := n - rcases ZFNat.instIsStrictTotalOrderLt.trichotomous n m with h | rfl | h + rcases lt_trichotomy n m with h | rfl | h · exfalso rw [ZFInt.lt_zero_iff] at h rcases n_pos with n_pos | eq @@ -689,7 +689,7 @@ lemma induction_neg {P : ZFInt → Prop} (n : ZFInt) (n_neg : n ≤ 0) @[induction_eliminator] theorem induction {P : ZFInt → Prop} (n : ZFInt) (zero : P 0) (pos : ∀ k, P k → P (k + 1)) (neg : ∀ k, P k → P (k - 1)) : P n := by - rcases instIsStrictTotalOrderLt.trichotomous n 0 with h | rfl | h + rcases lt_trichotomy n 0 with h | rfl | h · exact induction_neg n (Or.inl h) zero neg · exact zero · exact induction_pos n (Or.inl h) zero pos @@ -870,7 +870,7 @@ theorem pos_of_mul_pos {a b : ZFInt} (h : 0 < a * b) (ha : 0 < a) : 0 < b := by rcases hb with rfl | hb · rw [mul_zero] at h exact lt_irrefl h - · rcases instIsStrictTotalOrderLt.trichotomous a b with h' | rfl | h' + · rcases lt_trichotomy a b with h' | rfl | h' · nomatch lt_irrefl <| lt_trans (lt_trans ha h') hb · nomatch lt_irrefl <| lt_trans ha hb · nomatch lt_irrefl <| lt_trans h <| mul_pos_neg_neg a b ha hb @@ -921,7 +921,7 @@ theorem mul_eq_zero_iff {a b : ZFInt} : a * b = 0 ↔ a = 0 ∨ b = 0 := by induction b using Quotient.ind rename_i a b simp_rw [mk_eq, mul_eq, zero_eq, eq, ZFSet.zrel, ZFNat.add_zero] at h ⊢ - rcases ZFNat.instIsStrictTotalOrderLt.trichotomous b.1 b.2 with h' | eq | h' + rcases lt_trichotomy b.1 b.2 with h' | eq | h' · have := ZFNat.add_eq_add_sub_eq_sub h.symm rw [←ZFNat.left_distrib_mul_sub, ←ZFNat.left_distrib_mul_sub] at this have b₁b₂_ne_0 : b.2 - b.1 ≠ 0 := by @@ -1106,7 +1106,7 @@ noncomputable def π₂ (x : ZFSet) : ZFSet := @[simp] theorem pair_minus {x y : ZFSet} : x ≠ y → {x, y} \ {x} = ({y} : ZFSet) := by intro x_ne_y ext z - rw [mem_diff, mem_pair, mem_singleton, mem_singleton] + rw [mem_sdiff, mem_pair, mem_singleton, mem_singleton] constructor · rintro ⟨rfl | rfl, r⟩ · contradiction @@ -1123,7 +1123,7 @@ noncomputable def π₂ (x : ZFSet) : ZFSet := rw [sUnion_pair, pair_union, sInter_pair, pair_inter] at h rw [ZFSet.ext_iff] at h specialize h y - simpa only [mem_diff, mem_insert_iff, mem_singleton, eq_self, + simpa only [mem_sdiff, mem_insert_iff, mem_singleton, eq_self, or_true, true_and, notMem_empty, iff_false, not_not, eq_comm] using h · unfold pair at * rw [sUnion_pair, pair_union, sInter_pair, pair_inter] at h ⊢ @@ -1375,7 +1375,7 @@ theorem ZFInt.outof_into (x : ZFInt) : outof (into x) = x := by theorem ZFInt.into_outof (y : {x // x ∈ Int}) : into (outof y) = y := outof_inj _ _ (outof_into _) -attribute [-instance] SetLike.instPartialOrder +attribute [-instance] ZFSet.instPartialOrder /-- Canonical linear order on the set-theoretic integers, defined as the pullback of the linear order @@ -1402,7 +1402,7 @@ equivalence is built directly from `ZFInt.into` and `ZFInt.outof` — no Schröd deterministic in `x`. -/ @[reducible] -noncomputable instance instEquivZFIntInt : ZFInt ≃ {x // x ∈ Int} where +noncomputable def instEquivZFIntInt : ZFInt ≃ {x // x ∈ Int} where toFun := ZFInt.into invFun := ZFInt.outof left_inv := ZFInt.outof_into diff --git a/ZFLean/Isomorphisms.lean b/ZFLean/Isomorphisms.lean index 3a5a71e..c8c4747 100644 --- a/ZFLean/Isomorphisms.lean +++ b/ZFLean/Isomorphisms.lean @@ -62,7 +62,7 @@ theorem bijective_of_injective_on_subset {A B : ZFSet} induction n with | zero => intro x x_mem_C - rw [C, mem_diff] at x_mem_C + rw [C, mem_sdiff] at x_mem_C exact x_mem_C.1 | succ n ih => intro x x_mem_C @@ -83,7 +83,7 @@ theorem bijective_of_injective_on_subset {A B : ZFSet} · apply fapply_mem_range · push_neg at mem_Cn specialize mem_Cn 0 - rw [C, mem_diff, not_and, not_not] at mem_Cn + rw [C, mem_sdiff, not_and, not_not] at mem_Cn exact mem_Cn xA have v_inj : IsInjective v := by intro x y z hx hy hz eq₁ eq₂ @@ -123,7 +123,7 @@ theorem bijective_of_injective_on_subset {A B : ZFSet} · obtain ⟨n, y_mem_Cn⟩ := y_mem_C have : n ≠ 0 := by rintro rfl - rw [C, mem_diff] at y_mem_Cn + rw [C, mem_sdiff] at y_mem_Cn nomatch y_mem_Cn.2 yB obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero this rw [C, mem_sep] at y_mem_Cn @@ -1024,7 +1024,7 @@ theorem ZFNat.iso_eq_iff {n m : ZFNat} : ↑n ≅ᶻ ↑m ↔ n = m where · rw [mem_sep, pair_mem_prod] and_intros · exact zn - · rw [mem_diff, mem_singleton] + · rw [mem_sdiff, mem_singleton] and_intros · exact isfunc.1 hy |> pair_mem_prod.mp |>.2 · rintro ⟨⟩ @@ -1034,12 +1034,12 @@ theorem ZFNat.iso_eq_iff {n m : ZFNat} : ↑n ≅ᶻ ↑m ↔ n = m where exact lt_succ · exact hy · intro w hzw - rw [mem_sep, pair_mem_prod, mem_diff, mem_singleton] at hzw + rw [mem_sep, pair_mem_prod, mem_sdiff, mem_singleton] at hzw exact y_unq w hzw.2 have bij' : IsBijective f' this := by rw [bijective_exists1_iff] intro y hy - rw [mem_diff, add_one_eq_succ, mem_singleton, succ, mem_insert_iff] at hy + rw [mem_sdiff, add_one_eq_succ, mem_singleton, succ, mem_insert_iff] at hy obtain ⟨rfl | y_mem_k, y_ne_ℓ⟩ := hy · rw [bijective_exists1_iff] at bij have := bij k ?_ @@ -1051,7 +1051,7 @@ theorem ZFNat.iso_eq_iff {n m : ZFNat} : ↑n ≅ᶻ ↑m ↔ n = m where rw [add_one_eq_succ]; exact lt_succ) |>.unique x_k_f hℓ · and_intros <;> beta_reduce · exact x_mem_n - · rw [mem_sep, pair_mem_prod, mem_diff, mem_singleton] + · rw [mem_sep, pair_mem_prod, mem_sdiff, mem_singleton] and_intros · exact x_mem_n · rw [add_one_eq_succ] @@ -1059,7 +1059,7 @@ theorem ZFNat.iso_eq_iff {n m : ZFNat} : ↑n ≅ᶻ ↑m ↔ n = m where · exact y_ne_ℓ · exact x_k_f · rintro y ⟨yn, y_k_f⟩ - rw [mem_sep, pair_mem_prod, mem_diff, mem_singleton] at y_k_f + rw [mem_sep, pair_mem_prod, mem_sdiff, mem_singleton] at y_k_f apply bij k (by rw [add_one_eq_succ]; exact lt_succ) |>.unique · and_intros · rw [add_one_eq_succ, succ, mem_insert_iff] @@ -1083,7 +1083,7 @@ theorem ZFNat.iso_eq_iff {n m : ZFNat} : ↑n ≅ᶻ ↑m ↔ n = m where rw [add_one_eq_succ]; exact lt_succ) |>.unique x_k_f hℓ · and_intros <;> beta_reduce · exact x_mem_n - · rw [mem_sep, pair_mem_prod, mem_diff, mem_singleton] + · rw [mem_sep, pair_mem_prod, mem_sdiff, mem_singleton] and_intros · exact x_mem_n · rw [add_one_eq_succ, succ, mem_insert_iff] @@ -1092,7 +1092,7 @@ theorem ZFNat.iso_eq_iff {n m : ZFNat} : ↑n ≅ᶻ ↑m ↔ n = m where · exact y_ne_ℓ · exact x_k_f · rintro z ⟨zn, z_k_f⟩ - rw [mem_sep, pair_mem_prod, mem_diff, mem_singleton] at z_k_f + rw [mem_sep, pair_mem_prod, mem_sdiff, mem_singleton] at z_k_f apply bij y ?_ |>.unique · and_intros · rw [add_one_eq_succ, succ, mem_insert_iff] @@ -1120,7 +1120,7 @@ theorem ZFNat.iso_eq_iff {n m : ZFNat} : ↑n ≅ᶻ ↑m ↔ n = m where · and_intros · intro x y z hz hy hz g_xz g_yz dsimp [g] at g_xz g_yz - simp only [mem_sep, mem_prod, mem_diff, mem_singleton, pair_inj, + simp only [mem_sep, mem_prod, mem_sdiff, mem_singleton, pair_inj, exists_eq_right_right', π₁_pair, π₂_pair] at g_xz g_yz obtain ⟨⟨mem_x_k, mem_z_succ_k, z_ne_ℓ⟩, z_eq⟩ := g_xz obtain ⟨⟨mem_y_k, -, -⟩, z_eq'⟩ := g_yz @@ -1181,14 +1181,13 @@ theorem ZFNat.iso_eq_iff {n m : ZFNat} : ↑n ≅ᶻ ↑m ↔ n = m where -- reason into naturals have y_Nat : y ∈ Nat := by apply mem_Nat_of_mem_mem_Nat (k.succ.prop) - rw [add_one_eq_succ, mem_diff] at hy + rw [add_one_eq_succ, mem_sdiff] at hy exact hy.1 have ℓ_Nat : ℓ ∈ Nat := mem_Nat_of_mem_mem_Nat (k.succ.prop) (by rwa [add_one_eq_succ] at ℓ_mem_m) let Y : ZFNat := ⟨y, y_Nat⟩ let L : ZFNat := ⟨ℓ, ℓ_Nat⟩ - - simp only [add_one_eq_succ, succ, mem_insert_iff, mem_diff, mem_singleton] at hy + simp only [add_one_eq_succ, succ, mem_insert_iff, mem_sdiff, mem_singleton] at hy obtain ⟨rfl | y_mem_k, y_ne_ℓ⟩ := hy · have ℓ_Nat : ℓ ∈ Nat := mem_Nat_of_mem_mem_Nat (k.succ.prop) (by rwa [add_one_eq_succ] at ℓ_mem_m) @@ -1200,7 +1199,7 @@ theorem ZFNat.iso_eq_iff {n m : ZFNat} : ↑n ≅ᶻ ↑m ↔ n = m where · obtain ⟨s, rfl⟩ := this use s, lt_succ unfold g - simp only [mem_sep, pair_mem_prod, mem_diff, mem_singleton, π₁_pair, π₂_pair] + simp only [mem_sep, pair_mem_prod, mem_sdiff, mem_singleton, π₁_pair, π₂_pair] and_intros · exact lt_succ · rw [add_one_eq_succ] @@ -1224,7 +1223,7 @@ theorem ZFNat.iso_eq_iff {n m : ZFNat} : ↑n ≅ᶻ ↑m ↔ n = m where · change Y < L at y_lt_ℓ use y, y_mem_k dsimp [g] - simp only [mem_sep, mem_prod, mem_diff, mem_singleton, pair_inj, + simp only [mem_sep, mem_prod, mem_sdiff, mem_singleton, pair_inj, exists_eq_right_right', π₁_pair, π₂_pair] split_ifs · and_intros @@ -1270,7 +1269,7 @@ theorem ZFNat.iso_eq_iff {n m : ZFNat} : ↑n ≅ᶻ ↑m ↔ n = m where and_intros · change s < k exact lt_of_succ_lt y_mem_k - · rw [mem_diff, mem_singleton] + · rw [mem_sdiff, mem_singleton] and_intros · change s.succ < k + 1 rw [add_one_eq_succ, ←succ_mono] @@ -1291,7 +1290,7 @@ theorem ZFNat.iso_eq_iff {n m : ZFNat} : ↑n ≅ᶻ ↑m ↔ n = m where and_intros · change L < k exact lt_of_succ_lt y_mem_k - · rw [mem_diff, mem_singleton] + · rw [mem_sdiff, mem_singleton] and_intros · change L.succ < k + 1 rw [add_one_eq_succ, ←succ_mono] @@ -1314,7 +1313,7 @@ theorem ZFNat.iso_eq_iff {n m : ZFNat} : ↑n ≅ᶻ ↑m ↔ n = m where and_intros · exact sep_subset_self · intro x x_mem_k - simp only [mem_sep, mem_prod, mem_diff, mem_singleton, pair_inj, + simp only [mem_sep, mem_prod, mem_sdiff, mem_singleton, pair_inj, exists_eq_right_right', π₁_pair, π₂_pair] split_ifs with x_mem_ℓ · use x diff --git a/ZFLean/Naturals.lean b/ZFLean/Naturals.lean index 599aefe..e0c5c45 100644 --- a/ZFLean/Naturals.lean +++ b/ZFLean/Naturals.lean @@ -340,8 +340,7 @@ theorem every_nat_transitive {n : ZFSet} (h : n ∈ Nat) : transitive n := by apply ind _ h · intros _ _ exact False.elim (notMem_empty _ ‹_›) - · intros _ _ ih _ hy - intro _ _ + · intros _ _ ih _ hy _ _ rw [mem_insert_iff] at hy ⊢ rcases hy with rfl | _ · exact Or.inr ‹_› @@ -375,7 +374,6 @@ theorem le_antisymm {x y : ZFNat} : x ≤ y → y ≤ x → x = y := by · trivial theorem lt_le_iff {n m} : n ≤ m ↔ n < succ m := by - dsimp [nat_le, ] apply Iff.intro · rintro (_ | rfl) · exact lt_trans ‹_› lt_succ @@ -383,7 +381,7 @@ theorem lt_le_iff {n m} : n ≤ m ↔ n < succ m := by · intro h let ⟨n, hn⟩ := n let ⟨m, hm⟩ := m - dsimp [nat_lt, succ] at * + dsimp [LT.lt, nat_lt, succ] at * rw [mem_insert_iff] at h rcases h with rfl | _ · right; rfl @@ -490,7 +488,7 @@ theorem lt_iff_le_not_ge {x y : ZFNat} : x < y ↔ x ≤ y ∧ ¬ y ≤ x := by · exact lt_irrefl ‹_› · rintro ⟨h | rfl, h'⟩ · assumption - · simp only [nat_le, or_true] at h' + · simp only [LE.le, or_true] at h' contradiction /-- The (strong) induction principle for natural numbers. -/ @@ -721,11 +719,11 @@ instance : LinearOrder ZFNat where instance : IsStrictTotalOrder ZFNat (·<·) where trichotomous x y := by - rcases @le_total x y with (h | rfl) | h | rfl - · left; assumption - · right; left; rfl - · right; right; assumption - · right; left; rfl + intros h₁ h₂ + rcases @le_total x y with (h | rfl) | h | rfl <;> + first + | contradiction + | rfl irrefl _ := lt_irrefl trans _ _ _ := lt_trans @@ -1552,7 +1550,7 @@ theorem ZFNat.toNat_iff {n m : ZFNat} : n = m ↔ n.toNat = m.toNat where obtain rfl := ih h rfl -instance ZFNat.instEquivZFNat_Nat : ZFNat ≃ ℕ where +def ZFNat.equivZFNat_Nat : ZFNat ≃ ℕ where toFun := toNat invFun := ofNat left_inv := by diff --git a/ZFLean/Sum.lean b/ZFLean/Sum.lean index 9e284fc..799c598 100644 --- a/ZFLean/Sum.lean +++ b/ZFLean/Sum.lean @@ -154,7 +154,7 @@ theorem casesOn_of_inr {A B : ZFSet} {motive : A ⊎ B → Sort*} (a : {x // x · rw [inr, π₁_pair] exact zftrue_ne_zffalse -noncomputable instance {A B : ZFSet} : A ⊎ B ≃ ({x // x ∈ A} ⊕ {x // x ∈ B}) where +noncomputable def equivSum {A B : ZFSet} : A ⊎ B ≃ ({x // x ∈ A} ⊕ {x // x ∈ B}) where toFun x := by cases x with | inl a => exact _root_.Sum.inl a @@ -296,7 +296,7 @@ noncomputable def EmbeddingZFOptionOption {T : ZFSet} : Option T ↪ _root_.Opti toFun := into inj' := into.inj -noncomputable instance instEquivZFOptionOption {T : ZFSet} : +noncomputable def instEquivZFOptionOption {T : ZFSet} : Option T ≃ _root_.Option {x // x ∈ T} where toFun := into invFun := Function.invFun into @@ -354,7 +354,7 @@ def EmbeddingOptionZFOption {T : ZFSet} : _root_.Option {x // x ∈ T} ↪ Optio toFun := outof inj' := outof.inj -noncomputable instance instEquivOptionZFOption {T : ZFSet} : +noncomputable def instEquivOptionZFOption {T : ZFSet} : _root_.Option {x // x ∈ T} ≃ Option T where toFun := outof invFun := Function.invFun outof From 23e63464cc71323b077396a1510a433baa39ebf9 Mon Sep 17 00:00:00 2001 From: VTrelat Date: Thu, 25 Jun 2026 11:19:22 +0200 Subject: [PATCH 3/4] style: add file headers and resolve linter warnings --- ZFLean/Basic.lean | 15 ++++++++- ZFLean/Def.lean | 12 +++++++ ZFLean/Embeddings.lean | 13 ++++++++ ZFLean/Functions.lean | 24 ++++++++++---- ZFLean/Integers.lean | 45 +++++++++++++-------------- ZFLean/Isomorphisms.lean | 67 ++++++++++++++++------------------------ ZFLean/Sum.lean | 14 +++++++++ ZFLean/Tactics.lean | 12 +++++++ 8 files changed, 131 insertions(+), 71 deletions(-) diff --git a/ZFLean/Basic.lean b/ZFLean/Basic.lean index 6e99f16..961605d 100644 --- a/ZFLean/Basic.lean +++ b/ZFLean/Basic.lean @@ -1,4 +1,17 @@ +/- +Copyright (c) 2025 Vincent Trélat. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Vincent Trélat +-/ import Mathlib.SetTheory.ZFC.Basic + +/-! +# Basic ZFSet lemmas + +This file develops elementary lemmas about `ZFSet`, including characterizations of the +empty set, separation, and the behavior of unions and intersections. +-/ + noncomputable section namespace ZFSet @@ -6,7 +19,7 @@ namespace ZFSet theorem nonempty_exists_iff {n : ZFSet} : n ≠ ∅ ↔ ∃ m, m ∈ n := by simp [ZFSet.ext_iff] -@[simp] theorem subset_of_empty {x : ZFSet} (h : x ⊆ ∅) : x = ∅ := by +theorem subset_of_empty {x : ZFSet} (h : x ⊆ ∅) : x = ∅ := by ext1 z constructor · intro hz diff --git a/ZFLean/Def.lean b/ZFLean/Def.lean index 62948f7..4e32077 100644 --- a/ZFLean/Def.lean +++ b/ZFLean/Def.lean @@ -1,3 +1,8 @@ +/- +Copyright (c) 2025 Vincent Trélat. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Vincent Trélat +-/ import ZFLean.Basic import Mathlib.SetTheory.ZFC.Class import Mathlib.Algebra.Ring.Basic @@ -7,6 +12,13 @@ import Mathlib.Tactic.Ring import Mathlib.Data.Finite.Defs -- import Extra.Utils +/-! +# Core definitions for ZFC set theory + +This file develops basic definitions and lemmas over `ZFSet`, including transitive and +inductive sets, the symmetric difference, and assorted membership and monotonicity results. +-/ + noncomputable section namespace ZFSet diff --git a/ZFLean/Embeddings.lean b/ZFLean/Embeddings.lean index 383fc36..113ee26 100644 --- a/ZFLean/Embeddings.lean +++ b/ZFLean/Embeddings.lean @@ -1,5 +1,18 @@ +/- +Copyright (c) 2025 Vincent Trélat. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Vincent Trélat +-/ import ZFLean.Functions +/-! +# Embeddings between ZF sets + +This file defines embeddings between `ZFSet`s as injective functions and establishes +their basic properties: reflexivity, transitivity, and existence of embeddings between +singletons and pairs. +-/ + namespace ZFSet section Embeddings diff --git a/ZFLean/Functions.lean b/ZFLean/Functions.lean index 9313c5e..0bbc724 100644 --- a/ZFLean/Functions.lean +++ b/ZFLean/Functions.lean @@ -1,7 +1,20 @@ +/- +Copyright (c) 2025 Vincent Trélat. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Vincent Trélat +-/ import ZFLean.Rationals import ZFLean.Booleans import ZFLean.Tactics +/-! +# Functions and relations on ZF sets + +This file develops binary relations, partial and total functions, composition, identity, +injectivity/surjectivity/bijectivity, permutations, lambda abstraction and function application +on the encoded `ZFSet` universe, together with order-theoretic notions on subsets. +-/ + namespace ZFSet set_option linter.unusedVariables false @@ -672,6 +685,9 @@ theorem fapply.def {f A B : ZFSet} (hf : f.IsPFunc A B) {x : ZFSet} (hx : x ∈ generalize_proofs y_def exact Classical.choose_spec y_def |>.2 +-- This proof relies on `fapply._proof_1`, the auto-generated existence proof inside `fapply`, +-- to relate the two `Classical.choose` terms; the auxLemma linter is disabled locally for it. +set_option linter.auxLemma false in theorem IsInjective.apply_inj {f A B : ZFSet} (hf : IsFunc A B f) (inj : f.IsInjective) : Function.Injective @ᶻf := by classical rintro ⟨x, x_dom⟩ ⟨y, y_dom⟩ h @@ -1449,6 +1465,7 @@ noncomputable def Max (S : ZFSet) [linord : LinearOrder {x // x ∈ S}] : ZFSet noncomputable def Min (S : ZFSet) [linord : LinearOrder {x // x ∈ S}] : ZFSet := ε (S.sep fun x ↦ (_ : x ∈ S) → ∀ y, (_ : y ∈ S) → linord.le ⟨x, ‹_›⟩ ⟨y, ‹_›⟩) +@[reducible] def LinearOrder.ofSubset {S T : ZFSet} (S_T : S ⊆ T) [linordT : LinearOrder {x // x ∈ T}] : LinearOrder {x // x ∈ S} := LinearOrder.lift' @@ -1534,7 +1551,7 @@ theorem isTuple_pair {a b : ZFSet} : hasArity (ZFSet.pair a b) 2 := by rw [hasArity] · split_ifs with cond · trivial - · push_neg at cond + · push Not at cond nomatch cond a b · rintro ⟨⟩ @@ -2477,7 +2494,6 @@ theorem Min_mem_of_non_empty_finite {S : ZFSet} [inst : LinearOrder {x // x ∈ apply epsilon_spec ?_ (p := fun z ↦ z ∈ S ∧ ∀ (x : z ∈ S) (y : ZFSet.{u_1}) (x_1 : y ∈ S), inst.le ⟨z, x⟩ ⟨y, x_1⟩) |>.1 - beta_reduce obtain ⟨n, f, hn, hf, bij, mono⟩ := IsFinite.exists_bij_mono_iff (inst := inst.toPreorder).mp S_fin have : n ≠ (0 : ZFNat).1 := by @@ -2515,14 +2531,12 @@ theorem Min_mem_of_non_empty_finite {S : ZFSet} [inst : LinearOrder {x // x ∈ have x₀_S : x₀ ∈ S := by rw [mem_sep] at x₀_dom exact x₀_dom.1 - by_contra! contr specialize contr x₀ x₀_S obtain ⟨_, x₁, x₁_S, x₁_lt_x₀⟩ := contr obtain ⟨y₁, y₁_def, -⟩ := hf.2 x₁ x₁_S have := IsPFunc.mem_range_of_mem (is_func_is_pfunc hf) y₁_def rw [IsFunc.range_eq_of_surjective hf bij.2] at this - unfold IsStrictMono at mono have : (⟨y₁, ZFNat.mem_Nat_of_mem_mem_Nat hn this⟩ : ZFNat) < 0 := by specialize mono x₁ x₀ y₁ (0:ZFNat) x₁_S this y₁_def x₀_S _ x₀_def _ @@ -2571,7 +2585,6 @@ theorem fprod_is_func {A B A' B' φ ψ : ZFSet} (hφ : A.IsFunc A' φ) (hψ : B. obtain ⟨rfl, rfl⟩ := eq let φa : ZFSet := @ᶻφ ⟨a, by rwa [is_func_dom_eq hφ]⟩ let ψb : ZFSet := @ᶻψ ⟨b, by rwa [is_func_dom_eq hψ]⟩ - simp only [mem_prod, pair_inj, exists_eq_right_right', π₁_pair, π₂_pair] and_intros · exact aA @@ -2731,7 +2744,6 @@ theorem composition_fprod_Image_bijective {A B A' B' φ ψ : ZFSet} (φ_bij : φ.IsBijective) (ψ_bij : ψ.IsBijective) : let φ_ψ : ZFSet := fprod φ ψ have φ_ψ_bij : φ_ψ.IsBijective := fprod_bijective_of_bijective φ_bij ψ_bij - let Φ : ZFSet := λᶻ : (A.prod B).powerset → (A'.prod B').powerset | S ↦ φ_ψ[S] ∃ (hΦ : (A.prod B).powerset.IsFunc (A'.prod B').powerset Φ), IsBijective Φ hΦ := by diff --git a/ZFLean/Integers.lean b/ZFLean/Integers.lean index aae51c6..48093c6 100644 --- a/ZFLean/Integers.lean +++ b/ZFLean/Integers.lean @@ -82,7 +82,7 @@ theorem one_ne_zero : (1 : ZFInt) ≠ 0 := by rw [zero_eq, one_eq] rintro h rw [ZFInt.eq, ZFSet.zrel] at h - simp at h + simp only [add_zero] at h unfold_projs at h injection h with h rw [ZFSet.ext_iff] at h @@ -198,7 +198,7 @@ theorem neg_add_cancel_right (a b : ZFInt) : a + -b + b = a := by theorem add_left_cancel {a b c : ZFInt} (h : a + b = a + c) : b = c := by have h₁ : -a + (a + b) = -a + (a + c) := by rw [h] - simp [add_assoc, add_left_neg, zero_add] at h₁ + simp only [add_assoc, add_left_neg, zero_add] at h₁ exact h₁ @[simp] @@ -278,24 +278,19 @@ private theorem mul_wf {a b c d s t u v : ZFNat} (h₁ : ZFSet.zrel (a, b) (s, t)) (h₂ : ZFSet.zrel (c, d) (u, v)) : ZFSet.zrel (a * c + b * d, a * d + b * c) (s * u + t * v, s * v + t * u) := by dsimp [ZFSet.zrel] at * - suffices h₃ : t * c + a * c + b * d + s * v + t * u = a * d + b * c + s * u + t * v + t * c by simp_rw [ZFNat.add_comm _ (t*c), ← ZFNat.add_assoc (t*c)] at h₃ apply ZFNat.add_left_cancel.mp at h₃ simp_rw [ZFNat.add_assoc, h₃] - conv in t*c + a*c => rw [← right_distrib, ZFNat.add_comm, h₁, right_distrib] conv in _ + t*v + t*c => rw [← ZFNat.add_assoc, ← left_distrib, ZFNat.add_comm v c, h₂, left_distrib, ZFNat.add_assoc] - apply ZFNat.add_right_cancel.mpr - conv_rhs => rw [ZFNat.add_comm, ZFNat.add_assoc, ZFNat.add_assoc, ← right_distrib, ZFNat.add_comm t a, h₁, right_distrib] rw [ZFNat.add_comm (b * d + s * d), ZFNat.add_assoc, ← ZFNat.add_assoc, ← left_distrib s, ← h₂, left_distrib] - ac_rfl noncomputable abbrev mul (n m : ZFInt) : ZFInt := @@ -512,7 +507,7 @@ theorem lt_iff_le_not_ge {x y : ZFInt} : x < y ↔ x ≤ y ∧ ¬y ≤ x := by · nomatch lt_irrefl ‹_› · rintro ⟨h | rfl, h'⟩ · assumption - · simp only [int_le, or_true] at h' + · simp only [LE.le, or_true] at h' contradiction theorem lt_neg_iff {a b : ZFInt} : a < b ↔ -b < -a := by @@ -1020,11 +1015,11 @@ noncomputable def toZFInt : ℤ → ZFInt example : ofInt 0 = {{∅}} := by dsimp [ofInt, pair] ext x - simp + simp only [Nat.cast_zero, mem_insert_iff, mem_singleton, or_iff_left_iff_imp] intro subst x ext x - simp + simp only [mem_insert_iff, mem_singleton, or_iff_left_iff_imp] exact id section -- could be another definition @@ -1142,7 +1137,7 @@ theorem mem_Int_proj {x : ZFSet} (h : x ∈ Int) : ∃ n ∈ Nat, (x.π₁ = ∅ ∧ x.π₂ = n) ∨ (x.π₁ = n ∧ x.π₂ = ∅) := by simp_rw [mem_union, mem_prod] at h rcases h with ⟨a, ha, b, hb, x_eq⟩ | ⟨b, hb, a, ha, x_eq⟩ - <;> (simp at hb; subst x_eq; rw [π₁_pair, π₂_pair]; exists a) + <;> (simp only [mem_singleton] at hb; subst x_eq; rw [π₁_pair, π₂_pair]; exists a) · exact ⟨ha, .inr ⟨rfl, hb⟩⟩ · exact ⟨ha, .inl ⟨hb, rfl⟩⟩ @@ -1172,7 +1167,7 @@ noncomputable def ZFInt.outof : {x // x ∈ Int} → ZFInt := fun ⟨n, hn⟩ => theorem ZFInt.outof_inj (x y : {x // x ∈ Int}) : outof x = outof y → x = y := by let ⟨x, hx⟩ := x let ⟨y, hy⟩ := y - simp [outof] + simp only [outof, Subtype.mk.injEq] intro outof_eq split_ifs at outof_eq with h₁ h₂ h₂ <;> ( @@ -1184,12 +1179,12 @@ theorem ZFInt.outof_inj (x y : {x // x ∈ Int}) : outof x = outof y → x = y : | obtain ⟨l₂, r₂⟩ := Or.resolve_left (mem_Int_proj' hy) h₂ ) · apply exact at outof_eq - simp [ZFSet.zrel] at outof_eq + simp only [ZFSet.zrel, _root_.zero_add, _root_.add_zero, Subtype.mk.injEq] at outof_eq simp_rw [mem_union, mem_prod] at hx hy rcases hx, hy with ⟨⟨_, _, _, _, rfl⟩|⟨_, _, _, _, rfl⟩,⟨_, _, _, _, rfl⟩|⟨_, _, _, _, rfl⟩⟩ <;> (simp [π₁_pair, π₂_pair] at l₁ r₁ l₂ r₂ outof_eq; subst_eqs; congr) · apply exact at outof_eq - simp [ZFSet.zrel] at outof_eq + simp only [ZFSet.zrel, _root_.add_zero] at outof_eq obtain ⟨l₃, r₃⟩ := ZFNat.eq_zero_of_add_eq_zero outof_eq.symm injection l₃ with l₃ injection r₃ with r₃ @@ -1197,7 +1192,7 @@ theorem ZFInt.outof_inj (x y : {x // x ∈ Int}) : outof x = outof y → x = y : rcases hx, hy with ⟨⟨_, _, _, _, rfl⟩|⟨_, _, _, _, rfl⟩,⟨_, _, _, _, rfl⟩|⟨_, _, _, _, rfl⟩⟩ <;> (simp [π₁_pair, π₂_pair] at l₁ r₁ l₂ r₂ l₃ r₃ outof_eq; subst_eqs; congr) · apply exact at outof_eq - simp [ZFSet.zrel] at outof_eq + simp only [ZFSet.zrel, _root_.add_zero] at outof_eq obtain ⟨l₃, r₃⟩ := ZFNat.eq_zero_of_add_eq_zero outof_eq injection l₃ with l₃ injection r₃ with r₃ @@ -1205,7 +1200,7 @@ theorem ZFInt.outof_inj (x y : {x // x ∈ Int}) : outof x = outof y → x = y : rcases hx, hy with ⟨⟨_, _, _, _, rfl⟩|⟨_, _, _, _, rfl⟩,⟨_, _, _, _, rfl⟩|⟨_, _, _, _, rfl⟩⟩ <;> (simp [π₁_pair, π₂_pair] at l₁ r₁ l₂ r₂ l₃ r₃ outof_eq; subst_eqs; congr) · apply exact at outof_eq - simp [ZFSet.zrel] at outof_eq + simp only [ZFSet.zrel, _root_.add_zero, _root_.zero_add, Subtype.mk.injEq] at outof_eq simp_rw [mem_union, mem_prod] at hx hy rcases hx, hy with ⟨⟨_, _, _, _, rfl⟩|⟨_, _, _, _, rfl⟩,⟨_, _, _, _, rfl⟩|⟨_, _, _, _, rfl⟩⟩ <;> (simp [π₁_pair, π₂_pair] at l₁ r₁ l₂ r₂ outof_eq; subst_eqs; congr) @@ -1242,7 +1237,6 @@ theorem mem_Int_empty_not_mem {x : ZFSet} {h : x ∈ Int} : ∅ ∉ x := by noncomputable section ZFIntEquivInt open Classical in - /-- This function maps `ZFInt` to `Int` by taking the first projection of the pair. -/ @@ -1269,15 +1263,18 @@ theorem ZFInt.into_inj_aux (x y : ZFInt) : into x = into y → x.out ≈ y.out : dsimp [into] obtain ⟨a, b⟩ := Quotient.out x obtain ⟨c, d⟩ := Quotient.out y - split_ifs with h₁ h₂ h₂ <;> (intro eq; simp at *) + split_ifs with h₁ h₂ h₂ <;> + (intro eq; + simp only [not_lt, Subtype.mk.injEq, pair_inj, SetLike.coe_eq_coe, true_and, + and_true] at *) · have := ZFNat.eq_add_of_sub_eq (hle := .inl h₁) (h := eq) rw [ZFNat.add_comm, ← ZFNat.add_sub_assoc (.inl h₂)] at this apply ZFNat.eq_add_of_sub_eq (h := this.symm) rw [ZFNat.add_comm] exact ZFNat.le_trans (.inl h₂) (ZFNat.le_add_right d a) · obtain ⟨eq₁, eq₂⟩ := eq - replace eq₁ : 0 = c - d := Subtype.eq eq₁ - replace eq₂ : b - a = 0 := Subtype.eq eq₂ + replace eq₁ : 0 = c - d := Subtype.ext eq₁ + replace eq₂ : b - a = 0 := Subtype.ext eq₂ have := ZFNat.le_antisymm (ZFNat.sub_eq_zero_imp_le.mp (eq₁.symm)) h₂ subst this rw [eq₁] at eq₂ @@ -1287,8 +1284,8 @@ theorem ZFInt.into_inj_aux (x y : ZFInt) : into x = into y → x.out ≈ y.out : apply ZFNat.eq_add_of_sub_eq (h := eq₂) exact ZFNat.le_add_left c a · obtain ⟨eq₁, eq₂⟩ := eq - replace eq₁ : a - b = 0 := Subtype.eq eq₁ - replace eq₂ : 0 = d - c := Subtype.eq eq₂ + replace eq₁ : a - b = 0 := Subtype.ext eq₁ + replace eq₂ : 0 = d - c := Subtype.ext eq₂ have := ZFNat.le_antisymm (ZFNat.sub_eq_zero_imp_le.mp eq₁) h₁ subst this rw [eq₂] at eq₁ @@ -1352,7 +1349,7 @@ theorem ZFInt.outof_into (x : ZFInt) : outof (into x) = x := by have h_sub_zero : a - b = 0 := Subtype.ext ((π₁_pair (a - b).1 (∅ : ZFSet)).symm.trans hcond.1) have h_le_ab : a ≤ b := ZFNat.sub_eq_zero_imp_le.mp h_sub_zero - have h_le_ba : b ≤ a := by push_neg at hab; exact hab + have h_le_ba : b ≤ a := by push Not at hab; exact hab have ha_eq_b : a = b := ZFNat.le_antisymm h_le_ab h_le_ba subst ha_eq_b refine sound ?_ @@ -1361,7 +1358,7 @@ theorem ZFInt.outof_into (x : ZFInt) : outof (into x) = x := by Subtype.ext (π₂_pair _ _) rw [hπ₂] · rw [dif_neg hcond] - push_neg at hab + push Not at hab -- Rewrite `π₁ (pair (a-b).1 ∅)` to `(a-b).1` via `simp` (which handles the dependent -- proof in the inner ZFNat subtype); then proof irrelevance makes `⟨(a-b).1, _⟩` -- definitionally `a - b`. diff --git a/ZFLean/Isomorphisms.lean b/ZFLean/Isomorphisms.lean index c8c4747..8a2faea 100644 --- a/ZFLean/Isomorphisms.lean +++ b/ZFLean/Isomorphisms.lean @@ -1,5 +1,18 @@ +/- +Copyright (c) 2025 Vincent Trélat. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Vincent Trélat +-/ import ZFLean.Functions +/-! +# Isomorphisms of ZF sets + +This file develops the theory of isomorphisms (bijections) between ZF sets, including the +Cantor–Bernstein theorem, isomorphism stability under products, powersets and function spaces, +and currying/uncurrying. +-/ + namespace ZFSet section Isomorphisms @@ -8,7 +21,7 @@ def isIso (A B : ZFSet) : Prop := ∃ (bij : ZFSet) (is_func : A.IsFunc B bij), bij.IsBijective is_func infix:40 " ≅ᶻ " => ZFSet.isIso -theorem isIso_refl : Reflexive ZFSet.isIso := +theorem isIso_refl : ∀ A, ZFSet.isIso A A := fun A ↦ ⟨A.Id, Id.IsFunc, Id.IsBijective⟩ instance : Trans ZFSet.isIso ZFSet.isIso ZFSet.isIso where @@ -20,16 +33,16 @@ instance : Trans ZFSet.isIso ZFSet.isIso ZFSet.isIso where exists bij'', ZFSet.IsFunc_of_composition_IsFunc is_func' is_func exact ZFSet.IsBijective.composition_of_bijective is_bij is_bij' -theorem isIso_symm : Symmetric ZFSet.isIso := by +theorem isIso_symm : ∀ ⦃x y⦄, ZFSet.isIso x y → ZFSet.isIso y x := by intro x y iso obtain ⟨bij, is_func, is_bij⟩ := iso have := is_func.1 use bij⁻¹, ?_ exact inv_bijective_of_bijective is_bij -instance : IsSymm ZFSet isIso where +instance : Std.Symm isIso where symm := isIso_symm -theorem isIso_trans : Transitive ZFSet.isIso := by +theorem isIso_trans : ∀ ⦃x y z⦄, ZFSet.isIso x y → ZFSet.isIso y z → ZFSet.isIso x z := by intro x y z x_iso_y y_iso_z obtain ⟨bij, is_func, is_bij⟩ := x_iso_y obtain ⟨bij', is_func', is_bij'⟩ := y_iso_z @@ -57,7 +70,6 @@ theorem bijective_of_injective_on_subset {A B : ZFSet} (B_sub : B ⊆ A) {u : ZFSet} {hu : A.IsFunc B u} (u_inj : IsInjective u) : ∃ (v : ZFSet) (hv : A.IsFunc B v), IsBijective v := by let C₀ := A \ B - have C_sub {n} : C A B u n ⊆ A := by induction n with | zero => @@ -68,20 +80,18 @@ theorem bijective_of_injective_on_subset {A B : ZFSet} intro x x_mem_C rw [C, mem_sep] at x_mem_C exact B_sub x_mem_C.1 - let v := λᶻ : A → B | x ↦ if mem_Cn : ∃ n, x ∈ C A B u n then @ᶻu ⟨x, by rw [is_func_dom_eq hu] obtain ⟨_, x_mem_Cn⟩ := mem_Cn apply C_sub x_mem_Cn⟩ else x - have hv : A.IsFunc B v := by apply lambda_isFunc intro x xA split_ifs with mem_Cn · apply fapply_mem_range - · push_neg at mem_Cn + · push Not at mem_Cn specialize mem_Cn 0 rw [C, mem_sdiff, not_and, not_not] at mem_Cn exact mem_Cn xA @@ -98,25 +108,24 @@ theorem bijective_of_injective_on_subset {A B : ZFSet} · generalize_proofs u_pfun u_rel x_dom at eq subst y obtain ⟨n, mem_x⟩ := mem_x - push_neg at mem_y + push Not at mem_y specialize mem_y (n+1) rw [C, mem_sep, not_and] at mem_y specialize mem_y hz - push_neg at mem_y + push Not at mem_y specialize mem_y x mem_x nomatch mem_y <| fapply.def u_pfun x_dom · generalize_proofs u_pfun u_rel y_dom at eq subst z obtain ⟨n, mem_y⟩ := mem_y - push_neg at mem_x + push Not at mem_x specialize mem_x (n+1) rw [C, mem_sep, not_and] at mem_x specialize mem_x hz - push_neg at mem_x + push Not at mem_x specialize mem_x y mem_y nomatch mem_x <| fapply.def u_pfun y_dom · exact eq - have v_surj : IsSurjective v := by classical intro y yB by_cases y_mem_C : ∃ n, y ∈ C A B u n @@ -164,14 +173,11 @@ theorem isIso_of_biembedding {E F f g : ZFSet} {hf : E.IsFunc F f} obtain rfl := g_inj x' y' z hx' hy' (B_sub hz) x'_z_g y'_z_g exact f_inj x y x' hx hy hx' x_x'_f y_y'_f obtain ⟨v, hv, bij⟩ := bijective_of_injective_on_subset B_sub u_inj - have hg' : F.IsFunc B g := IsFunc.is_func_on_range hg have g_bij : IsBijective g hg' := bijective_of_injective hg g_inj have h_v_hinv : E.IsFunc F (composition (inv g hg'.1) v E B F) := IsFunc_of_composition_IsFunc (inv_is_func_of_bijective g_bij) hv - use composition (inv g hg'.1) v E B F, h_v_hinv - exact IsBijective.composition_of_bijective bij (inv_bijective_of_bijective g_bij) alias schroeder_bernstein := isIso_of_biembedding @@ -190,7 +196,6 @@ theorem isIso_of_prod {A B C D : ZFSet} (h : A ≅ᶻ C) (h' : B ≅ᶻ D) : A.p rw [pair_inj] at ab_eq cd_eq rcases ab_eq with ⟨rfl, rfl⟩ rcases cd_eq with ⟨rfl, rfl⟩ - obtain ⟨⟨⟨a', ha', b', hb', rfl⟩, -⟩, _, _, _, _, ⟨a'b'_eq, cd_eq⟩, a'c_f₁, b'd_f₂⟩ := ha'b'cd rw [pair_inj] at a'b'_eq cd_eq rcases a'b'_eq with ⟨rfl, rfl⟩ @@ -250,11 +255,11 @@ theorem inv_Image_of_bijective {f A B : ZFSet} {hf : A.IsFunc B f} f⁻¹[(f[X])] = X := by ext1 x constructor <;> intro hx - · simp [mem_Image, mem_inv] at hx + · simp only [mem_Image, mem_inv] at hx obtain ⟨xA, y, ⟨yB, u, uX, fuy⟩, fxy⟩ := hx obtain rfl := bij.1 u x y (hf.1 fuy |> pair_mem_prod.mp |>.1) xA yB fuy fxy exact uX - · simp [mem_Image, mem_inv] + · simp only [mem_Image, mem_inv] and_intros · exact hX hx · obtain ⟨y, yB, -⟩ := hf.2 x (hX hx) @@ -288,12 +293,10 @@ theorem IsInjective_of_left_inverse {A B : ZFSet} {f : ZFSet} have y_y : y.pair y ∈ g ∘ᶻ f := by rw [left_inv] exact pair_self_mem_Id hy - simp only [composition, mem_sep, mem_prod, pair_inj, exists_eq_right_right', and_self, existsAndEq, and_true, exists_eq_left'] at x_x y_y obtain ⟨-, x', hx', x_x'_f, x'_x_g⟩ := x_x obtain ⟨-, y', hy', y_y'_f, y'_y_g⟩ := y_y - obtain rfl : x' = y' := by trans z · apply hf.2 x hx |>.unique @@ -384,7 +387,6 @@ theorem isIso_powerset {A B : ZFSet} (h : A ≅ᶻ B) : A.powerset ≅ᶻ B.powe exact hy.1 · exact hX · rw [inv_Image_of_bijective bij (mem_powerset.mp hX)] - have right_inv : F ∘ᶻ F' = 𝟙B.powerset := by ext1 X rw [fcomp, composition, mem_sep, mem_prod] @@ -445,7 +447,6 @@ theorem isIso_funs_to_pow_rel {A B : ZFSet} : A.funs B.powerset ≅ᶻ (A.prod B | a ↦ if ha : a ∈ A then B.sep fun b ↦ (a.pair b ∈ R) -- {b ∈ B | (a, b) ∈ R} else ∅ - have hF : (A.funs B.powerset).IsFunc (A.prod B).powerset F := by apply lambda_isFunc intro f hf @@ -462,7 +463,6 @@ theorem isIso_funs_to_pow_rel {A B : ZFSet} : A.funs B.powerset ≅ᶻ (A.prod B rw [dite_cond_eq_true (eq_true ha)] apply sep_mem_powerset rw [mem_powerset] - apply isIso_of_two_sided_inverse (f := F) (g := G) · ext1 f simp only [mem_composition, mem_funs, mem_powerset, mem_Id_iff] @@ -624,7 +624,8 @@ theorem isIso_funs_to_pow_rel {A B : ZFSet} : A.funs B.powerset ≅ᶻ (A.prod B use ⟨ha, hb⟩ rw [fapply] generalize_proofs choose₁ choose₂ - simp [fapp_eq] at * + simp only [fapp_eq, dite_eq_ite, pair_inj, exists_eq_right_right', + π₁_pair, mem_sep, mem_powerset, and_imp] at * clear fapp_eq generalize_proofs choose₃ have choose₃_spec := choose_spec choose₃ @@ -638,7 +639,6 @@ theorem isIso_funs_to_pow_rel {A B : ZFSet} : A.funs B.powerset ≅ᶻ (A.prod B have choose₁_spec := choose_spec choose₁ have choose₂_spec := choose_spec choose₂ have choose₁_eq := choose₁_spec.2 |> lambda_spec.mp |>.2.2 - conv at choose₂_spec => enter [2,1] rw [choose₁_eq] @@ -658,7 +658,6 @@ theorem isIso_funs_to_pow_rel {A B : ZFSet} : A.funs B.powerset ≅ᶻ (A.prod B apply sep_mem_powerset rw [mem_powerset] · rwa [mem_powerset] - · exact hF · exact hG @@ -667,7 +666,6 @@ theorem isIso_of_funs {A B C D : ZFSet} (h : A ≅ᶻ C) (h' : B ≅ᶻ D) : A.f obtain ⟨F, hF, Fbij⟩ := h have : F⁻¹ ⊆ C.prod A := by apply subset_prod_inv obtain ⟨G, hG, Gbij⟩ := h' - let ξ := λᶻ : (A.funs B) → (C.funs D) | f ↦ if hf : f ⊆ A.prod B then λᶻ: C → D @@ -816,7 +814,7 @@ theorem isIso_of_funs {A B C D : ZFSet} (h : A ≅ᶻ C) (h' : B ≅ᶻ D) : A.f rw [←b_def, ←d_def] at db_G have b_eq := fapply.of_pair (is_func_is_pfunc Ginv_isfunc) db_G rw [Subtype.ext_iff] at b_eq - simp [d_eq] at b_eq + simp only [d_eq] at b_eq rw [←fapply_composition Ginv_isfunc hG (fapply_mem_range g'pfunc a_g'dom)] at b_eq conv at b_eq => unfold fapply @@ -996,19 +994,15 @@ theorem ZFNat.iso_eq_iff {n m : ZFNat} : ↑n ≅ᶻ ↑m ↔ n = m where nomatch notMem_empty x contr | succ n ih => obtain ⟨f, isfunc, bij⟩ := iso - obtain ⟨ℓ, hℓ, ℓ_unq⟩ := isfunc.2 ↑n <| add_one_eq_succ ▸ lt_succ have ℓ_mem_m := isfunc.1 hℓ |> pair_mem_prod.mp |>.2 - obtain ⟨k, rfl⟩ : ∃ k, m = k + 1 := by simp_rw [ZFNat.add_one_eq_succ] apply ZFNat.not_zero_imp_succ rintro rfl nomatch notMem_empty _ ℓ_mem_m - rw [add_right_cancel] apply ih - let f' := ZFSet.prod ↑n (↑(k+1) \ {ℓ}) |>.sep (· ∈ f) have : IsFunc ↑n (↑(k+1) \ {ℓ}) f' := by and_intros @@ -1124,7 +1118,6 @@ theorem ZFNat.iso_eq_iff {n m : ZFNat} : ↑n ≅ᶻ ↑m ↔ n = m where exists_eq_right_right', π₁_pair, π₂_pair] at g_xz g_yz obtain ⟨⟨mem_x_k, mem_z_succ_k, z_ne_ℓ⟩, z_eq⟩ := g_xz obtain ⟨⟨mem_y_k, -, -⟩, z_eq'⟩ := g_yz - -- reason into naturals have z_Nat : z ∈ Nat := mem_Nat_of_mem_mem_Nat (k.succ.prop) (by rwa [add_one_eq_succ] at mem_z_succ_k) @@ -1136,7 +1129,6 @@ theorem ZFNat.iso_eq_iff {n m : ZFNat} : ↑n ≅ᶻ ↑m ↔ n = m where let X : ZFNat := ⟨x, x_Nat⟩ let Y : ZFNat := ⟨y, y_Nat⟩ let L : ZFNat := ⟨ℓ, ℓ_Nat⟩ - split_ifs at z_eq z_eq' with x_mem_ℓ y_mem_ℓ y_lt_ℓ · subst x y rfl @@ -1177,7 +1169,6 @@ theorem ZFNat.iso_eq_iff {n m : ZFNat} : ↑n ≅ᶻ ↑m ↔ n = m where · apply succ_inj_aux' rw [←z_eq, ←z_eq'] · intro y hy - -- reason into naturals have y_Nat : y ∈ Nat := by apply mem_Nat_of_mem_mem_Nat (k.succ.prop) @@ -1239,7 +1230,6 @@ theorem ZFNat.iso_eq_iff {n m : ZFNat} : ↑n ≅ᶻ ↑m ↔ n = m where change Y < k at y_mem_k rw [not_lt] at y_lt_ℓ rw [←ne_eq, ne_comm, ne_eq] at y_ne_ℓ - have := ZFNat.not_zero_imp_succ (n := Y) ?_ · obtain ⟨s, Y_eq⟩ := this use s @@ -1514,7 +1504,6 @@ theorem isIso_curry {A B C : ZFSet} : intro g hg rw [dite_cond_eq_true (eq_true hg), mem_funs] apply uncurrify_is_func - have l_inv : (uncurry ∘ᶻ curry) = 𝟙((A.prod B).funs C) := by rw [is_func_ext_iff (IsFunc_of_composition_IsFunc huncurry hcurry) Id.IsFunc] intro f hf @@ -1540,7 +1529,6 @@ theorem isIso_curry {A B C : ZFSet} : ) hf, dite_cond_eq_true (eq_true hf)] rw [uncurrify_of_currify f (mem_funs.mp hf)] - have r_inv : (curry ∘ᶻ uncurry) = 𝟙(A.funs (B.funs C)) := by rw [is_func_ext_iff (IsFunc_of_composition_IsFunc hcurry huncurry) Id.IsFunc] intro g hg @@ -1566,7 +1554,6 @@ theorem isIso_curry {A B C : ZFSet} : ) hg, dite_cond_eq_true (eq_true hg)] rw [currify_of_uncurrify g (mem_funs.mp hg)] - exact isIso_of_two_sided_inverse l_inv r_inv end Lemmas diff --git a/ZFLean/Sum.lean b/ZFLean/Sum.lean index 799c598..8ac4123 100644 --- a/ZFLean/Sum.lean +++ b/ZFLean/Sum.lean @@ -1,8 +1,22 @@ +/- +Copyright (c) 2025 Vincent Trélat. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Vincent Trélat +-/ import ZFLean.Basic import ZFLean.Booleans import ZFLean.Integers import ZFLean.Functions +/-! +# Disjoint sums and options over ZF sets + +This file defines the disjoint sum `A ⊎ B` of two `ZFSet`s as a subtype, with +constructors, eliminators, and an equivalence to the type-level sum. It also develops +`Option S` together with bijections relating it to `_root_.Option` and a lifting of +functions to options. +-/ + namespace ZFSet def Sum (A B : ZFSet) := diff --git a/ZFLean/Tactics.lean b/ZFLean/Tactics.lean index 02e44f6..fcc0519 100644 --- a/ZFLean/Tactics.lean +++ b/ZFLean/Tactics.lean @@ -1,5 +1,17 @@ +/- +Copyright (c) 2025 Vincent Trélat. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Vincent Trélat +-/ import Mathlib.CategoryTheory.Category.Basic +/-! +# Custom tactics for ZF + +This file registers label attributes and defines the `zrel`, `zpfun`, and `zfun` +tactics used to discharge relation, partial-function, and function side goals. +-/ + register_label_attr zrel register_label_attr zpfun register_label_attr zfun From 53c0e8ce51981dcd14b7641d238d80b5ddb3e0d1 Mon Sep 17 00:00:00 2001 From: VTrelat Date: Thu, 25 Jun 2026 11:28:01 +0200 Subject: [PATCH 4/4] ci: pin lean-release-tag to fixed commit (handle new-branch null before) --- .github/workflows/create-release.yml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/.github/workflows/create-release.yml b/.github/workflows/create-release.yml index ba2e44b..d6b44a6 100644 --- a/.github/workflows/create-release.yml +++ b/.github/workflows/create-release.yml @@ -16,7 +16,10 @@ jobs: contents: write steps: - name: lean-release-tag action - uses: leanprover-community/lean-release-tag@v1 + # Pinned to a fixed `main` commit: the `v1` branch lacks the null-`before` guard and + # crashes (`Invalid revision range 000…0..`) on the first push of a new branch, + # where `github.event.before` is the null SHA. + uses: leanprover-community/lean-release-tag@ee8ee743e5a36ff0e75ff51035f6a95a9d1bdf59 with: do-release: true GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}