From 1c8a611b4cfc3591a38229ae34842cd2d5289333 Mon Sep 17 00:00:00 2001 From: "A. M. Berns" Date: Fri, 3 Jul 2026 14:59:47 -0400 Subject: [PATCH 1/3] refactor(Vorspiel): rename Matrix.map to Matrix.vecMap to avoid Mathlib clash MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Foundation.Vorspiel.Matrix defined its own Matrix.map, a vector map (Fin k → α) → (Fin k → β), shadowing Mathlib's Matrix.map. Both auto-generate Matrix.map.eq_1, so importing Foundation alongside any Mathlib module that materializes Mathlib's Matrix.map.eq_1 (e.g. Bochner integration, matrix-heavy analysis) fails with an 'environment already contains Matrix.map.eq_1' clash. Because Vorspiel.Matrix sits in Foundation's prelude, this blocks co-importing Foundation with large parts of Mathlib. Rename the def to vecMap. The postfix notation ⨟ and all lemmas are unchanged in behavior; no qualified Matrix.map (vector) references exist elsewhere in the tree. --- Foundation/Vorspiel/Matrix.lean | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/Foundation/Vorspiel/Matrix.lean b/Foundation/Vorspiel/Matrix.lean index cb5472745..916046450 100644 --- a/Foundation/Vorspiel/Matrix.lean +++ b/Foundation/Vorspiel/Matrix.lean @@ -245,11 +245,14 @@ def foldr (f : α → β → β) (init : β) : {k : ℕ} → (Fin k → α) → | 0, _ => init | _ + 1, v => f (vecHead v) (Matrix.foldr f init (vecTail v)) -def map (f : α → β) : (Fin k → α) → (Fin k → β) := fun v ↦ f ∘ v +-- Renamed from `Matrix.map` to `Matrix.vecMap` to avoid clashing with Mathlib's +-- `Matrix.map`: both auto-generate `Matrix.map.eq_1`, which makes Foundation +-- unimportable alongside Mathlib matrix/analysis theory (e.g. Bochner integration). +def vecMap (f : α → β) : (Fin k → α) → (Fin k → β) := fun v ↦ f ∘ v section map -postfix:max "⨟" => map +postfix:max "⨟" => vecMap variable (f : α → β) @@ -257,11 +260,11 @@ variable (f : α → β) @[simp] lemma map_cons (a : α) (v : Fin k → α) : f⨟ (a :> v) = f a :> f⨟ v := by ext i - cases i using Fin.cases <;> simp [map] + cases i using Fin.cases <;> simp [vecMap] @[simp] lemma map_cons' (v : Fin (k + 1) → α) : f⨟ v = f (vecHead v) :> f⨟ (vecTail v) := by ext i - cases i using Fin.cases <;> { simp [map]; rfl } + cases i using Fin.cases <;> { simp [vecMap]; rfl } @[simp] lemma map_app (v : Fin k → α) (i : Fin k) : (f⨟ v) i = f (v i) := rfl From 8292d6639df8658a474861119327c5003db6a0fa Mon Sep 17 00:00:00 2001 From: "A. M. Berns" Date: Fri, 3 Jul 2026 15:34:24 -0400 Subject: [PATCH 2/3] refactor(Vorspiel): also rename Matrix.forall_iff/exists_iff to avoid Mathlib clash Same clash as Matrix.map -> vecMap in this PR: Vorspiel.Matrix's forall_iff and exists_iff collide by name with Mathlib.Data.Matrix.Reflection's Matrix.forall_iff / Matrix.exists_iff, blocking co-import of Foundation with that module (pulled in transitively via EuclideanSpace / InnerProductSpace.PiL2). Rename to vecForall_iff / vecExists_iff and update the 12 call sites in BinderNotation and Semantics. --- Foundation/FirstOrder/Basic/BinderNotation.lean | 16 ++++++++-------- .../FirstOrder/Basic/Semantics/Semantics.lean | 8 ++++---- Foundation/Vorspiel/Matrix.lean | 8 ++++++-- 3 files changed, 18 insertions(+), 14 deletions(-) diff --git a/Foundation/FirstOrder/Basic/BinderNotation.lean b/Foundation/FirstOrder/Basic/BinderNotation.lean index 383777d0b..3d0898d88 100644 --- a/Foundation/FirstOrder/Basic/BinderNotation.lean +++ b/Foundation/FirstOrder/Basic/BinderNotation.lean @@ -45,14 +45,14 @@ lemma eval_nestFormulae {φ : Semiformula L ξ n} {Ψ : Fin n → Semiformula L @[simp] lemma eval_nestFormulae₁ {φ : Semiformula L ξ 1} {ψ : Semiformula L ξ (m + 1)} : Eval e f (φ.nestFormulae ![ψ]) ↔ ∀ x : M, Eval (x :> e) f ψ → Eval ![x] f φ := by - simp [eval_nestFormulae, Matrix.forall_iff, Matrix.empty_eq] + simp [eval_nestFormulae, Matrix.vecForall_iff, Matrix.empty_eq] @[simp] lemma eval_nestFormulae₂ {φ : Semiformula L ξ 2} {ψ₁ ψ₂ : Semiformula L ξ (m + 1)} : Eval e f (φ.nestFormulae ![ψ₁, ψ₂]) ↔ ∀ x₁, Eval (x₁ :> e) f ψ₁ → ∀ x₂, Eval (x₂ :> e) f ψ₂ → Eval ![x₁, x₂] f φ := by suffices (∀ x₁ x₂, Eval (x₁ :> e) f ψ₁ → Eval (x₂ :> e) f ψ₂ → Eval ![x₁, x₂] f φ) ↔ ∀ x₁, Eval (x₁ :> e) f ψ₁ → ∀ x₂, Eval (x₂ :> e) f ψ₂ → Eval ![x₁, x₂] f φ by - simpa [eval_nestFormulae, Matrix.forall_iff, Matrix.empty_eq, Fin.forall_fin_two] + simpa [eval_nestFormulae, Matrix.vecForall_iff, Matrix.empty_eq, Fin.forall_fin_two] grind @[simp] lemma eval_nestFormulae₃ {φ : Semiformula L ξ 3} {ψ₁ ψ₂ ψ₃ : Semiformula L ξ (m + 1)} : @@ -61,7 +61,7 @@ lemma eval_nestFormulae {φ : Semiformula L ξ n} {Ψ : Fin n → Semiformula L suffices (∀ x₁ x₂ x₃, Eval (x₁ :> e) f ψ₁ → Eval (x₂ :> e) f ψ₂ → Eval (x₃ :> e) f ψ₃ → Eval ![x₁, x₂, x₃] f φ) ↔ ∀ x₁, Eval (x₁ :> e) f ψ₁ → ∀ x₂, Eval (x₂ :> e) f ψ₂ → ∀ x₃, Eval (x₃ :> e) f ψ₃ → Eval ![x₁, x₂, x₃] f φ by - simpa [eval_nestFormulae, Matrix.forall_iff, Matrix.empty_eq, Fin.forall_fin_succ] + simpa [eval_nestFormulae, Matrix.vecForall_iff, Matrix.empty_eq, Fin.forall_fin_succ] grind @[simp] lemma eval_nestFormulae₄ {φ : Semiformula L ξ 4} {ψ₁ ψ₂ ψ₃ ψ₄ : Semiformula L ξ (m + 1)} : @@ -83,7 +83,7 @@ lemma eval_nestFormulae {φ : Semiformula L ξ n} {Ψ : Fin n → Semiformula L ∀ x₃, Eval (x₃ :> e) f ψ₃ → ∀ x₄, Eval (x₄ :> e) f ψ₄ → Eval ![x₁, x₂, x₃, x₄] f φ) by - simpa [eval_nestFormulae, Matrix.forall_iff, Matrix.empty_eq, Fin.forall_fin_succ] + simpa [eval_nestFormulae, Matrix.vecForall_iff, Matrix.empty_eq, Fin.forall_fin_succ] grind lemma eval_nestFormulaeFunc {φ : Semiformula L ξ (n + 1)} {Ψ : Fin n → Semiformula L ξ (m + 1)} : @@ -96,14 +96,14 @@ lemma eval_nestFormulaeFunc {φ : Semiformula L ξ (n + 1)} {Ψ : Fin n → Semi @[simp] lemma eval_nestFormulaeFunc₁ {φ : Semiformula L ξ 2} {ψ : Semiformula L ξ (m + 1)} : Eval (z :> e) f (φ.nestFormulaeFunc ![ψ]) ↔ ∀ x, Eval (x :> e) f ψ → Eval ![z, x] f φ := by - simp [eval_nestFormulaeFunc, Matrix.forall_iff, Matrix.empty_eq] + simp [eval_nestFormulaeFunc, Matrix.vecForall_iff, Matrix.empty_eq] @[simp] lemma eval_nestFormulaeFunc₂ {φ : Semiformula L ξ 3} {ψ₁ ψ₂ : Semiformula L ξ (m + 1)} : Eval (z :> e) f (φ.nestFormulaeFunc ![ψ₁, ψ₂]) ↔ ∀ x₁, Eval (x₁ :> e) f ψ₁ → ∀ x₂, Eval (x₂ :> e) f ψ₂ → Eval ![z, x₁, x₂] f φ := by suffices (∀ x₁ x₂, Eval (x₁ :> e) f ψ₁ → Eval (x₂ :> e) f ψ₂ → Eval ![z, x₁, x₂] f φ) ↔ ∀ x₁, Eval (x₁ :> e) f ψ₁ → ∀ x₂, Eval (x₂ :> e) f ψ₂ → Eval ![z, x₁, x₂] f φ by - simpa [eval_nestFormulaeFunc, Matrix.forall_iff, Matrix.empty_eq, Fin.forall_fin_two] + simpa [eval_nestFormulaeFunc, Matrix.vecForall_iff, Matrix.empty_eq, Fin.forall_fin_two] grind @[simp] lemma eval_nestFormulaeFunc₃ {φ : Semiformula L ξ 4} {ψ₁ ψ₂ ψ₃ : Semiformula L ξ (m + 1)} : @@ -112,7 +112,7 @@ lemma eval_nestFormulaeFunc {φ : Semiformula L ξ (n + 1)} {Ψ : Fin n → Semi suffices (∀ x₁ x₂ x₃, Eval (x₁ :> e) f ψ₁ → Eval (x₂ :> e) f ψ₂ → Eval (x₃ :> e) f ψ₃ → Eval ![z, x₁, x₂, x₃] f φ) ↔ ∀ x₁, Eval (x₁ :> e) f ψ₁ → ∀ x₂, Eval (x₂ :> e) f ψ₂ → ∀ x₃, Eval (x₃ :> e) f ψ₃ → Eval ![z, x₁, x₂, x₃] f φ by - simpa [eval_nestFormulaeFunc, Matrix.forall_iff, Matrix.empty_eq, Fin.forall_fin_succ] + simpa [eval_nestFormulaeFunc, Matrix.vecForall_iff, Matrix.empty_eq, Fin.forall_fin_succ] grind @[simp] lemma eval_nestFormulaeFunc₄ {φ : Semiformula L ξ 5} {ψ₁ ψ₂ ψ₃ ψ₄ : Semiformula L ξ (m + 1)} : @@ -134,7 +134,7 @@ lemma eval_nestFormulaeFunc {φ : Semiformula L ξ (n + 1)} {Ψ : Fin n → Semi ∀ x₃, Eval (x₃ :> e) f ψ₃ → ∀ x₄, Eval (x₄ :> e) f ψ₄ → Eval ![z, x₁, x₂, x₃, x₄] f φ) by - simpa [eval_nestFormulaeFunc, Matrix.forall_iff, Matrix.empty_eq, Fin.forall_fin_succ] + simpa [eval_nestFormulaeFunc, Matrix.vecForall_iff, Matrix.empty_eq, Fin.forall_fin_succ] grind end Semiformula diff --git a/Foundation/FirstOrder/Basic/Semantics/Semantics.lean b/Foundation/FirstOrder/Basic/Semantics/Semantics.lean index 40753cb79..3d3e2386b 100644 --- a/Foundation/FirstOrder/Basic/Semantics/Semantics.lean +++ b/Foundation/FirstOrder/Basic/Semantics/Semantics.lean @@ -278,25 +278,25 @@ lemma eval_nrel' {r : L.Rel k} {v} : Eval b f (∀⁰* φ) ↔ ∀ e', Eval e' f φ := match k with | 0 => by simp [eq_finZeroElim] - | k + 1 => by simpa [allClosure_succ, eval_allClosure (k := k), Matrix.forall_iff] using forall_comm + | k + 1 => by simpa [allClosure_succ, eval_allClosure (k := k), Matrix.vecForall_iff] using forall_comm @[simp] lemma eval_exsClosure {b} {φ : Semiformula L ξ k} : Eval b f (∃⁰* φ) ↔ ∃ e', Eval e' f φ := match k with | 0 => by simp [eq_finZeroElim] - | k + 1 => by simpa [exsClosure_succ, eval_exsClosure (k := k), Matrix.exists_iff] using exists_comm + | k + 1 => by simpa [exsClosure_succ, eval_exsClosure (k := k), Matrix.vecExists_iff] using exists_comm @[simp] lemma eval_allItr {b} {φ : Semiformula L ξ (n + k)} : Eval b f (∀⁰^[k] φ) ↔ ∀ e', Eval (Matrix.appendr e' b) f φ := match k with | 0 => by simp [Matrix.empty_eq] - | k + 1 => by simpa [allItr_succ, eval_allItr (k := k), Matrix.forall_iff] using forall_comm + | k + 1 => by simpa [allItr_succ, eval_allItr (k := k), Matrix.vecForall_iff] using forall_comm @[simp] lemma eval_exsItr {b} {φ : Semiformula L ξ (n + k)} : Eval b f (∃⁰^[k] φ) ↔ ∃ e', Eval (Matrix.appendr e' b) f φ := match k with | 0 => by simp [Matrix.empty_eq] - | k + 1 => by simpa [exsItr_succ, eval_exsItr (k := k), Matrix.exists_iff] using exists_comm + | k + 1 => by simpa [exsItr_succ, eval_exsItr (k := k), Matrix.vecExists_iff] using exists_comm section rew diff --git a/Foundation/Vorspiel/Matrix.lean b/Foundation/Vorspiel/Matrix.lean index 916046450..f73e5977c 100644 --- a/Foundation/Vorspiel/Matrix.lean +++ b/Foundation/Vorspiel/Matrix.lean @@ -232,11 +232,15 @@ def appendr {n m} (v : Fin n → α) (w : Fin m → α) : Fin (m + n) → α := @[simp] lemma appendr_cons {m n} (x : α) (v : Fin n → α) (w : Fin m → α) : appendr (x :> v) w = x :> appendr v w := by funext i; simp [appendr] -lemma forall_iff {n : ℕ} (φ : (Fin (n + 1) → α) → Prop) : +-- Renamed from `Matrix.forall_iff` to `Matrix.vecForall_iff` to avoid clashing with +-- Mathlib's `Matrix.forall_iff` (Mathlib.Data.Matrix.Reflection), which otherwise makes +-- Foundation unimportable alongside that module. +lemma vecForall_iff {n : ℕ} (φ : (Fin (n + 1) → α) → Prop) : (∀ v, φ v) ↔ (∀ a, ∀ v, φ (a :> v)) := ⟨fun h a v ↦ h (a :> v), fun h v ↦ by simpa [eq_vecCons v] using h (v 0) (v ∘ Fin.succ)⟩ -lemma exists_iff {n : ℕ} (φ : (Fin (n + 1) → α) → Prop) : +-- Renamed from `Matrix.exists_iff` to `Matrix.vecExists_iff`; see `vecForall_iff` above. +lemma vecExists_iff {n : ℕ} (φ : (Fin (n + 1) → α) → Prop) : (∃ v, φ v) ↔ (∃ a, ∃ v, φ (a :> v)) := ⟨by rintro ⟨v, hv⟩; exact ⟨v 0, v ∘ Fin.succ, by simpa [eq_vecCons] using hv⟩, by rintro ⟨a, v, hv⟩; exact ⟨_, hv⟩⟩ From 85bc80bc9cd067a200856d887b79757b93f10b9d Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Sat, 18 Jul 2026 11:48:09 +0900 Subject: [PATCH 3/3] refactor(Vorspiel): rename map_* lemma family to vecMap_* for consistency Co-Authored-By: Claude --- .../Bootstrapping/DerivabilityCondition/D3.lean | 4 ++-- .../Bootstrapping/Syntax/Formula/Typed.lean | 4 ++-- Foundation/Vorspiel/Matrix.lean | 16 ++++++++-------- 3 files changed, 12 insertions(+), 12 deletions(-) diff --git a/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D3.lean b/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D3.lean index 18619ed39..b9fe56fb0 100644 --- a/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D3.lean +++ b/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/D3.lean @@ -129,7 +129,7 @@ theorem bold_sigma_one_complete {n} {φ : Semisentence ℒₒᵣ n} (hp : Hierar apply ball_intro intro i hi suffices T.internalize V ⊢ (toNumVec (i :> w) ⤔ ⌜φ⌝) by - simpa [Semiformula.substs_substs, Matrix.map_map_comp'] + simpa [Semiformula.substs_substs, Matrix.vecMap_vecMap_comp'] exact ih (h i hi) exact ball_replace T ((toNumVec w).q ⤔ ⌜φ⌝) _ _ ⨀ (eq_comm <| term_complete T t w) ⨀ this case hExs => @@ -139,7 +139,7 @@ theorem bold_sigma_one_complete {n} {φ : Semisentence ℒₒᵣ n} (hp : Hierar suffices T.internalize V ⊢ ∃⁰ ((toNumVec w).q ⤔ ⌜φ⌝) by simpa apply TProof.exs! (𝕹 i) suffices T.internalize V ⊢ (toNumVec (i :> w) ⤔ ⌜φ⌝) by - simpa [Semiformula.substs_substs, Matrix.map_map_comp'] + simpa [Semiformula.substs_substs, Matrix.vecMap_vecMap_comp'] exact ih hφ theorem sigma_one_provable_of_models {σ : Sentence ℒₒᵣ} (hσ : Hierarchy 𝚺 1 σ) : diff --git a/Foundation/FirstOrder/Bootstrapping/Syntax/Formula/Typed.lean b/Foundation/FirstOrder/Bootstrapping/Syntax/Formula/Typed.lean index 0d073f57f..650628945 100644 --- a/Foundation/FirstOrder/Bootstrapping/Syntax/Formula/Typed.lean +++ b/Foundation/FirstOrder/Bootstrapping/Syntax/Formula/Typed.lean @@ -310,11 +310,11 @@ noncomputable def substItrDisj (w : SemitermVec V ℒₒᵣ m n) (φ : Semiformu @[simp] lemma substItrConj_free (w : SemitermVec V ℒₒᵣ m 1) (φ : Semiformula V ℒₒᵣ (m + 1)) (z : V) : (φ.substItrConj w z).free = φ.shift.substItrConj (Semiterm.free⨟ w) z := by - unfold free; simp [Matrix.map_map_comp']; rfl + unfold free; simp [Matrix.vecMap_vecMap_comp']; rfl @[simp] lemma substItrDisj_free (w : SemitermVec V ℒₒᵣ m 1) (φ : Semiformula V ℒₒᵣ (m + 1)) (z : V) : (φ.substItrDisj w z).free = φ.shift.substItrDisj (Semiterm.free⨟ w) z := by - unfold free; simp [Matrix.map_map_comp']; rfl + unfold free; simp [Matrix.vecMap_vecMap_comp']; rfl end Semiformula diff --git a/Foundation/Vorspiel/Matrix.lean b/Foundation/Vorspiel/Matrix.lean index f73e5977c..efadee4a4 100644 --- a/Foundation/Vorspiel/Matrix.lean +++ b/Foundation/Vorspiel/Matrix.lean @@ -254,31 +254,31 @@ def foldr (f : α → β → β) (init : β) : {k : ℕ} → (Fin k → α) → -- unimportable alongside Mathlib matrix/analysis theory (e.g. Bochner integration). def vecMap (f : α → β) : (Fin k → α) → (Fin k → β) := fun v ↦ f ∘ v -section map +section vecMap postfix:max "⨟" => vecMap variable (f : α → β) -@[simp] lemma map_nil (v : Fin 0 → α) : f⨟ v = ![] := empty_eq (f⨟ v) +@[simp] lemma vecMap_nil (v : Fin 0 → α) : f⨟ v = ![] := empty_eq (f⨟ v) -@[simp] lemma map_cons (a : α) (v : Fin k → α) : f⨟ (a :> v) = f a :> f⨟ v := by +@[simp] lemma vecMap_cons (a : α) (v : Fin k → α) : f⨟ (a :> v) = f a :> f⨟ v := by ext i cases i using Fin.cases <;> simp [vecMap] -@[simp] lemma map_cons' (v : Fin (k + 1) → α) : f⨟ v = f (vecHead v) :> f⨟ (vecTail v) := by +@[simp] lemma vecMap_cons' (v : Fin (k + 1) → α) : f⨟ v = f (vecHead v) :> f⨟ (vecTail v) := by ext i cases i using Fin.cases <;> { simp [vecMap]; rfl } -@[simp] lemma map_app (v : Fin k → α) (i : Fin k) : (f⨟ v) i = f (v i) := rfl +@[simp] lemma vecMap_app (v : Fin k → α) (i : Fin k) : (f⨟ v) i = f (v i) := rfl -lemma map_map_comp (g : β → γ) (f : α → β) (v : Fin k → α) : +lemma vecMap_vecMap_comp (g : β → γ) (f : α → β) (v : Fin k → α) : g⨟ (f⨟ v) = (g ∘ f)⨟ v := by ext x; simp -lemma map_map_comp' (g : β → γ) (f : α → β) (v : Fin k → α) : +lemma vecMap_vecMap_comp' (g : β → γ) (f : α → β) (v : Fin k → α) : g⨟ (f⨟ v) = (fun x ↦ g (f x))⨟ v := by ext x; simp -end map +end vecMap section foldr variable (f : α → β → β) (init : β)