From 73a21e6e23bf56a92b76682ec0c2c01512359026 Mon Sep 17 00:00:00 2001 From: Convindix Date: Thu, 30 Jul 2026 02:05:12 -0500 Subject: [PATCH 1/2] Fix some types and add a few docstrings --- Foundation/FirstOrder/Basic/Semantics/Semantics.lean | 6 +++--- Foundation/FirstOrder/Basic/Syntax/Formula.lean | 8 ++++---- Foundation/FirstOrder/SetTheory/Recursion.lean | 2 +- Foundation/FirstOrder/SetTheory/Z.lean | 2 +- Foundation/FirstOrder/SetTheory/ZF.lean | 2 +- Foundation/Syntax/Predicate/Rew.lean | 6 +++++- Foundation/Syntax/Predicate/Term.lean | 8 ++++---- Foundation/Vorspiel/List/Basic.lean | 2 +- 8 files changed, 20 insertions(+), 16 deletions(-) diff --git a/Foundation/FirstOrder/Basic/Semantics/Semantics.lean b/Foundation/FirstOrder/Basic/Semantics/Semantics.lean index 4e7aaf5a7..62ccec0cb 100644 --- a/Foundation/FirstOrder/Basic/Semantics/Semantics.lean +++ b/Foundation/FirstOrder/Basic/Semantics/Semantics.lean @@ -453,10 +453,10 @@ lemma eval_toEmpty [DecidableEq ξ] {n} {φ : Semiformula L ξ n} (hp : φ.freeV haveI : Inhabited M := Classical.inhabited_of_nonempty inferInstance simp [Semiformula.univCl, ←eval_toEmpty (f := default)] -@[simp] lemma eval_enumarateFVar_idxOfFVar_eq_id [DecidableEq M] [Inhabited M] (φ : Semiformula L M n) (v) : - φ.Eval v (fun x ↦ φ.enumarateFVar (φ.idxOfFVar x)) ↔ φ.Eval v id := +@[simp] lemma eval_enumerateFVar_idxOfFVar_eq_id [DecidableEq M] [Inhabited M] (φ : Semiformula L M n) (v) : + φ.Eval v (fun x ↦ φ.enumerateFVar (φ.idxOfFVar x)) ↔ φ.Eval v id := Semiformula.eval_iff_of_funEqOn _ <| by - intro x hx; simp [Semiformula.enumarateFVar_idxOfFVar (Semiformula.mem_fvarList_iff_fvar?.mpr hx)] + intro x hx; simp [Semiformula.enumerateFVar_idxOfFVar (Semiformula.mem_fvarList_iff_fvar?.mpr hx)] end rew diff --git a/Foundation/FirstOrder/Basic/Syntax/Formula.lean b/Foundation/FirstOrder/Basic/Syntax/Formula.lean index 065d079e9..18742233d 100644 --- a/Foundation/FirstOrder/Basic/Syntax/Formula.lean +++ b/Foundation/FirstOrder/Basic/Syntax/Formula.lean @@ -555,12 +555,12 @@ def fvarList {n : ℕ} : Semiformula L ξ n → List ξ def idxOfFVar [DecidableEq ξ] (φ : Semiformula L ξ n) : ξ → ℕ := φ.fvarList.idxOf -def enumarateFVar [Inhabited ξ] (φ : Semiformula L ξ n) : ℕ → ξ := +def enumerateFVar [Inhabited ξ] (φ : Semiformula L ξ n) : ℕ → ξ := fun i ↦ if hi : i < φ.fvarList.length then φ.fvarList.get ⟨i, hi⟩ else default -lemma enumarateFVar_idxOfFVar [DecidableEq ξ] [Inhabited ξ] {φ : Semiformula L ξ n} {x : ξ} (hx : x ∈ φ.fvarList) : - enumarateFVar φ (idxOfFVar φ x) = x := by - simpa [enumarateFVar, idxOfFVar] +lemma enumerateFVar_idxOfFVar [DecidableEq ξ] [Inhabited ξ] {φ : Semiformula L ξ n} {x : ξ} (hx : x ∈ φ.fvarList) : + enumerateFVar φ (idxOfFVar φ x) = x := by + simpa [enumerateFVar, idxOfFVar] using fun h ↦ False.elim <| not_le.mpr (List.idxOf_lt_length_iff.mpr hx) h lemma mem_fvarList_iff_fvar? [DecidableEq ξ] {φ : Semiformula L ξ n} : x ∈ φ.fvarList ↔ φ.FVar? x := by diff --git a/Foundation/FirstOrder/SetTheory/Recursion.lean b/Foundation/FirstOrder/SetTheory/Recursion.lean index 42a68f885..2f4bc5f2d 100644 --- a/Foundation/FirstOrder/SetTheory/Recursion.lean +++ b/Foundation/FirstOrder/SetTheory/Recursion.lean @@ -116,7 +116,7 @@ lemma attempt_function_restrict_eq_of_lt intro γ hγβ y have hγα : γ ∈ α.val := by aesop have : IsOrdinal γ := of_mem hγβ - have hγsusbetβ : γ ⊆ β.val := by grind + have hγsubsetβ : γ ⊆ β.val := by grind simp_all [mem_restrict_iff] /-- Any two attempt functions agree on overlapping inputs. -/ diff --git a/Foundation/FirstOrder/SetTheory/Z.lean b/Foundation/FirstOrder/SetTheory/Z.lean index b4007829a..29a53c506 100644 --- a/Foundation/FirstOrder/SetTheory/Z.lean +++ b/Foundation/FirstOrder/SetTheory/Z.lean @@ -282,7 +282,7 @@ instance power.definable : ℒₛₑₜ-function₁[V] power := power.defined.to lemma separation_exists_eval (x : V) (φ : SetTheorySemiformula V 1) : ∃ y : V, ∀ z : V, z ∈ y ↔ z ∈ x ∧ φ.Eval ![z] id := by -- have : Inhabited V := inhabited_of_nonempty inferInstance - let f := φ.enumarateFVar + let f := φ.enumerateFVar let ψ := (Rew.rewriteMap φ.idxOfFVar) ▹ φ have := by simpa [models_iff, Semiformula.eval_univCl, Axiom.separationSchema] using Theory.models V 𝗭 (Zermelo.axiom_of_separation ψ) simpa [ψ, f, Semiformula.eval_rewriteMap, Matrix.constant_eq_singleton] using this f x diff --git a/Foundation/FirstOrder/SetTheory/ZF.lean b/Foundation/FirstOrder/SetTheory/ZF.lean index 965d230d5..5afb484b9 100644 --- a/Foundation/FirstOrder/SetTheory/ZF.lean +++ b/Foundation/FirstOrder/SetTheory/ZF.lean @@ -16,7 +16,7 @@ lemma replacement_exists_eval (φ : SetTheorySemiformula V 2) (X : V) (h : (∀ ∃ Y : V, ∀ y : V, y ∈ Y ↔ ∃ x ∈ X, φ.Eval ![x, y] id := by /- `φ` can have finitely many free variables of type `V`, these are interpreted by `id : V → V` as finitely many parameters in `V`. `f` enumerates the parameters of `φ`. -/ - let f := φ.enumarateFVar + let f := φ.enumerateFVar /- While `φ` has free variables of type `V`, `ψ` has free variables of type `ℕ`. Since `f` enumerates the parameters, it is intended to be the valuation of the free variables of `ψ`. -/ let ψ := (Rew.rewriteMap φ.idxOfFVar) ▹ φ diff --git a/Foundation/Syntax/Predicate/Rew.lean b/Foundation/Syntax/Predicate/Rew.lean index c266756da..fe35bd2eb 100644 --- a/Foundation/Syntax/Predicate/Rew.lean +++ b/Foundation/Syntax/Predicate/Rew.lean @@ -26,7 +26,9 @@ namespace FirstOrder /-- A structure for maps which rewrite the semiterms occurring in a term. + toFun - A function from `Semiterm L ξ₁ n₁` to `Semiterm L ξ₂ n₂`. + func'' - A proof that `toFun` respects the function symbols of `L`. -/ structure Rew (L : Language) (ξ₁ : Type*) (n₁ : ℕ) (ξ₂ : Type*) (n₂ : ℕ) where @@ -95,7 +97,7 @@ def rewriteMap (e : ξ₁ → ξ₂) : Rew L ξ₁ n ξ₂ n := rewrite (fun m = def map (b : Fin n₁ → Fin n₂) (e : ξ₁ → ξ₂) : Rew L ξ₁ n₁ ξ₂ n₂ := bind (fun n => #(b n)) (fun m => &(e m)) -/-- `LO.FirstOrder.Rew.subst v` is a substitution of the bounded variables occurring in a term by `v : Fin n → Semiterm L ξ n'`. -/ +/-- `LO.FirstOrder.Rew.subst v` is a substitution of the bound variables occurring in a term by `v : Fin n → Semiterm L ξ n'`. -/ def subst {n'} (v : Fin n → Semiterm L ξ n') : Rew L ξ n ξ n' := bind v fvar @@ -119,6 +121,8 @@ def cast {n n' : ℕ} (h : n = n') : Rew L ξ n ξ n' := def castLE {n n' : ℕ} (h : n ≤ n') : Rew L ξ n ξ n' := map (Fin.castLE h) id +/-- `LO.FirstOrder.Rew.embSubsts v` is a substitution of the bound variables occurring in a term with no free variables by `v : Fin n → Semiterm L ξ n'`. +This closely resembles `LO.FirstOrder.Rew.subst`, however the term is required to have free variables of type `Empty`. -/ def embSubsts (v : Fin k → Semiterm L ξ n) : Rew L Empty k ξ n := Rew.bind v Empty.elim protected def q (ω : Rew L ξ₁ n₁ ξ₂ n₂) : Rew L ξ₁ (n₁ + 1) ξ₂ (n₂ + 1) := diff --git a/Foundation/Syntax/Predicate/Term.lean b/Foundation/Syntax/Predicate/Term.lean index 5e8e8044c..9e0c2e659 100644 --- a/Foundation/Syntax/Predicate/Term.lean +++ b/Foundation/Syntax/Predicate/Term.lean @@ -232,12 +232,12 @@ def fvarList : Semiterm L ξ n → List ξ def idxOfFVar [DecidableEq ξ] (t : Semiterm L ξ n) : ξ → ℕ := t.fvarList.idxOf -def enumarateFVar [Inhabited ξ] (t : Semiterm L ξ n) : ℕ → ξ := +def enumerateFVar [Inhabited ξ] (t : Semiterm L ξ n) : ℕ → ξ := fun i ↦ if hi : i < t.fvarList.length then t.fvarList.get ⟨i, hi⟩ else default -lemma enumarateFVar_idxOfFVar [DecidableEq ξ] [Inhabited ξ] {t : Semiterm L ξ n} {x : ξ} (hx : x ∈ t.fvarList) : - enumarateFVar t (idxOfFVar t x) = x := by - simpa [enumarateFVar, idxOfFVar] +lemma enumerateFVar_idxOfFVar [DecidableEq ξ] [Inhabited ξ] {t : Semiterm L ξ n} {x : ξ} (hx : x ∈ t.fvarList) : + enumerateFVar t (idxOfFVar t x) = x := by + simpa [enumerateFVar, idxOfFVar] using fun h ↦ False.elim <| not_le.mpr (List.idxOf_lt_length_iff.mpr $ hx) h lemma mem_fvarList_iff_fvar? [DecidableEq ξ] {t : Semiterm L ξ n} : x ∈ t.fvarList ↔ t.FVar? x:= by diff --git a/Foundation/Vorspiel/List/Basic.lean b/Foundation/Vorspiel/List/Basic.lean index 98b206346..d837e8cb9 100644 --- a/Foundation/Vorspiel/List/Basic.lean +++ b/Foundation/Vorspiel/List/Basic.lean @@ -152,7 +152,7 @@ lemma remove_cons_subset_cons_remove (a b) (l : List α) : simp only [mem_remove_iff, mem_cons, ne_eq, and_imp] rintro (rfl | hx) nex <;> simp [*] -lemma remove_map_substet_map_remove [DecidableEq β] (f : α → β) (l : List α) (a) : +lemma remove_map_subset_map_remove [DecidableEq β] (f : α → β) (l : List α) (a) : (l.map f).remove (f a) ⊆ (l.remove a).map f := by simp only [subset_def, mem_remove_iff, mem_map, ne_eq, and_imp, forall_exists_index, forall_apply_eq_imp_iff₂] From 7988dc394b754f96dedb86e646b4e7882c7ad395 Mon Sep 17 00:00:00 2001 From: Convindix Date: Thu, 30 Jul 2026 02:21:22 -0500 Subject: [PATCH 2/2] Occurrences that I didn't catch --- Foundation/FirstOrder/Arithmetic/IOpen/Basic.lean | 4 ++-- Foundation/FirstOrder/Arithmetic/Schemata.lean | 2 +- Foundation/FirstOrder/Basic/Syntax/Formula.lean | 4 ++-- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/Foundation/FirstOrder/Arithmetic/IOpen/Basic.lean b/Foundation/FirstOrder/Arithmetic/IOpen/Basic.lean index 4d81c33e0..7644af8da 100644 --- a/Foundation/FirstOrder/Arithmetic/IOpen/Basic.lean +++ b/Foundation/FirstOrder/Arithmetic/IOpen/Basic.lean @@ -31,12 +31,12 @@ lemma succ_induction {P : V → Prop} InductionScheme.succ_induction (C := Semiformula.Open) (by rcases hP with ⟨φ, hp, hhp⟩ haveI : Inhabited V := Classical.inhabited_of_nonempty' - refine ⟨φ.enumarateFVar, Rew.rewriteMap φ.idxOfFVar ▹ φ, by simp [hp], ?_⟩ + refine ⟨φ.enumerateFVar, Rew.rewriteMap φ.idxOfFVar ▹ φ, by simp [hp], ?_⟩ intro x simp only [hhp, Nat.succ_eq_add_one, Nat.reduceAdd, Semiformula.eval_rewriteMap] exact Semiformula.eval_iff_of_funEqOn φ (by intro z hz - simp [Semiformula.enumarateFVar_idxOfFVar (Semiformula.mem_fvarList_iff_fvar?.mpr hz)])) + simp [Semiformula.enumerateFVar_idxOfFVar (Semiformula.mem_fvarList_iff_fvar?.mpr hz)])) zero succ lemma least_number {P : V → Prop} diff --git a/Foundation/FirstOrder/Arithmetic/Schemata.lean b/Foundation/FirstOrder/Arithmetic/Schemata.lean index ca3c1ab4a..2ab9b4334 100644 --- a/Foundation/FirstOrder/Arithmetic/Schemata.lean +++ b/Foundation/FirstOrder/Arithmetic/Schemata.lean @@ -141,7 +141,7 @@ lemma succ_induction {P : V → Prop} (hP : Γ-[m].DefinablePred P) InductionScheme.succ_induction (P := P) (C := Hierarchy Γ m) (by rcases hP with ⟨φ, hp⟩ haveI : Inhabited V := Classical.inhabited_of_nonempty' - exact ⟨φ.val.enumarateFVar, (Rew.rewriteMap φ.val.idxOfFVar) ▹ φ.val, by simp, + exact ⟨φ.val.enumerateFVar, (Rew.rewriteMap φ.val.idxOfFVar) ▹ φ.val, by simp, by intro x; simp [Semiformula.eval_rewriteMap, hp.df.iff]⟩) zero succ diff --git a/Foundation/FirstOrder/Basic/Syntax/Formula.lean b/Foundation/FirstOrder/Basic/Syntax/Formula.lean index 18742233d..437a2d511 100644 --- a/Foundation/FirstOrder/Basic/Syntax/Formula.lean +++ b/Foundation/FirstOrder/Basic/Syntax/Formula.lean @@ -541,7 +541,7 @@ def lMap (Φ : L₁ →ᵥ L₂) {n} : Semiformula L₁ ξ n →ˡᶜ Semiformul (Semiformula.lMap Φ φ).freeVariables = φ.freeVariables := by induction φ using Semiformula.rec' <;> try simp [lMap_rel, lMap_nrel, freeVariables_rel, freeVariables_nrel, *] -section enumarateFVar +section enumerateFVar def fvarList {n : ℕ} : Semiformula L ξ n → List ξ | ⊤ => [] @@ -566,7 +566,7 @@ lemma enumerateFVar_idxOfFVar [DecidableEq ξ] [Inhabited ξ] {φ : Semiformula lemma mem_fvarList_iff_fvar? [DecidableEq ξ] {φ : Semiformula L ξ n} : x ∈ φ.fvarList ↔ φ.FVar? x := by induction φ using rec' <;> simp [fvarList, Semiterm.mem_fvarList_iff_fvar?, *] -end enumarateFVar +end enumerateFVar end Semiformula