Skip to content

Commit 4078213

Browse files
hyperpolymathhyperpolymath
committed
proof(lean4/CNOCategory): close all 5 sorries (5 → 0); fix structural drift
CNO.lean - `seqComp` `def` → `abbrev` so downstream callers can `rw` with `eval_seqComp` even when the goal mentions the underlying `++` directly (previously CNOCategory.composeMorphisms.evaluates failed to elaborate for this reason). CNOCategory.lean drift fixes (preconditions to closing the sorries) - `id := idMorphism` had explicit/implicit binder mismatch under v4.16; switched to `id := fun {A} => idMorphism A`. - Renamed `Functor` → `CatFunctor`. `Functor` clashes with core `Init.Functor (f : Type u → Type v)`; the namespace shadowing failed once the class was applied to `Category`-typed terms. - In `CatFunctor.fmap_compose`, renamed inner binders `{A B C}` → `{X Y Z}` — the original `{A B C : C.Obj}` silently shadowed the outer `(C : Category)`, breaking field resolution on `C.Hom`. - `fmap_compose` body now uses `C.compose g f` / `D.compose ...` rather than `g ∘ f`. The `∘` notation routes through `Category.compose` via instance resolution, but `C`/`D` are bound *terms* of type Category, not class instances, so the notation cannot find them. Same fix in `yoneda_cno`. - `CNOEquivalent`: pre-existing direction bug — original wrote `F.fmap (G.fmap m)` for `m : C.Hom s s`, but `G : D ⟶ C` so `G.fmap` consumes `D.Hom`. Swapped to `G.fmap (F.fmap m)`. - `cno_model_independent`: original statement was type-incorrect (`s : C.Obj` then concluded `m' : D.Hom s s`, requiring `s : D.Obj`). Restated to existentially produce both the carrier `s' : D.Obj` (set to `F.fobj s`) and the morphism (set to `F.fmap m`), with `F.fmap_id` discharging the identity property. - `yoneda_cno`: original `exact this.symm` was the wrong direction (`m = C.id` is the goal, not `C.id = m`). Pre-paren parsing masked the issue. Now `exact this`. Sorries closed (5) - `compose_assoc` ↦ `List.append_assoc` after `cases` on the three morphisms and `simp only [composeMorphisms]; congr 1`. - `compose_id_left` ↦ `List.append_nil` (right-id of ++). - `compose_id_right` ↦ `rfl` (`[] ++ p` reduces). - `cno_categorical_equiv` reverse direction: built the four isCNO conjuncts from the identity hypothesis directly. - `cno_model_independent`: closed under the type-corrected statement via `F.fmap_id`.
1 parent e219401 commit 4078213

2 files changed

Lines changed: 128 additions & 30 deletions

File tree

‎proofs/lean4/CNO.lean‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -274,8 +274,12 @@ theorem cno_reversible (p : Program) (h : isCNO p) :
274274

275275
/-! ## Composition -/
276276

277-
/-- Sequential composition of programs -/
278-
def seqComp (p1 p2 : Program) : Program := p1 ++ p2
277+
/-- Sequential composition of programs.
278+
`abbrev` (not `def`) so that `eval_seqComp` rewrites also fire when
279+
the goal mentions the underlying `++` directly (downstream callers
280+
in `CNOCategory.composeMorphisms` build the program with `++` and
281+
rely on this transparency). -/
282+
abbrev seqComp (p1 p2 : Program) : Program := p1 ++ p2
279283

280284
/-- Evaluation of composition.
281285
`unfold eval` unfolds the LHS one step but leaves the RHS in its

‎proofs/lean4/CNOCategory.lean‎

Lines changed: 122 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -65,24 +65,58 @@ def idMorphism (s : CNO.ProgramState) : ProgramMorphism s s :=
6565
evaluates := by unfold CNO.eval; rfl
6666
}
6767

68-
/-- Programs form a category -/
68+
/-- Programs form a category.
69+
70+
`id := fun {A} => idMorphism A`: the class field expects a function
71+
with an *implicit* binder `∀ {A}, Hom A A`, but `idMorphism` takes
72+
an *explicit* `(s : ProgramState)`. The implicit-lambda wrapper
73+
bridges the two; bare `id := idMorphism` triggers
74+
"implicit-lambda introduced A✝" and then a type mismatch under v4.16.
75+
76+
The three category laws reduce, via the structure projections, to
77+
laws on `List Instruction` (`++`):
78+
- `compose_assoc` ↦ `List.append_assoc`
79+
- `compose_id_left` ↦ `List.append_nil` (right-id of ++)
80+
- `compose_id_right` ↦ `List.nil_append` (left-id of ++)
81+
The proofs are in Prop and proof-irrelevant, so structural equality
82+
of the morphism records reduces to equality of the program field. -/
6983
instance ProgramCategory : Category where
7084
Obj := CNO.ProgramState
7185
Hom := ProgramMorphism
7286
compose := @composeMorphisms
73-
id := idMorphism
87+
id := fun {A} => idMorphism A
7488

7589
compose_assoc := by
7690
intro A B C D h g f
77-
sorry -- Requires morphism equality
91+
-- LHS.program = (f.program ++ g.program) ++ h.program
92+
-- RHS.program = f.program ++ (g.program ++ h.program)
93+
cases h with | mk hp he =>
94+
cases g with | mk gp ge =>
95+
cases f with | mk fp fe =>
96+
show composeMorphisms ⟨hp, he⟩ (composeMorphisms ⟨gp, ge⟩ ⟨fp, fe⟩) =
97+
composeMorphisms (composeMorphisms ⟨hp, he⟩ ⟨gp, ge⟩) ⟨fp, fe⟩
98+
simp only [composeMorphisms]
99+
congr 1
100+
exact List.append_assoc fp gp hp
78101

79102
compose_id_left := by
80103
intro A B f
81-
sorry -- Requires morphism equality
104+
-- composeMorphisms id f has program := f.program ++ [].program = f.program ++ []
105+
cases f with | mk fp fe =>
106+
show composeMorphisms (idMorphism B) ⟨fp, fe⟩ = ⟨fp, fe⟩
107+
simp only [composeMorphisms, idMorphism]
108+
congr 1
109+
exact List.append_nil fp
82110

83111
compose_id_right := by
84112
intro A B f
85-
sorry -- Requires morphism equality
113+
-- composeMorphisms f id has program := [].program ++ f.program = [] ++ f.program
114+
-- which reduces to f.program by the cons-recursion of ++
115+
cases f with | mk fp fe =>
116+
show composeMorphisms ⟨fp, fe⟩ (idMorphism A) = ⟨fp, fe⟩
117+
simp only [composeMorphisms, idMorphism]
118+
-- [] ++ fp ≡ fp definitionally
119+
rfl
86120

87121
/-! ## Categorical CNO Definition -/
88122

@@ -98,7 +132,17 @@ def programIsCNOCategorical (p : CNO.Program) (s : CNO.ProgramState) : Prop :=
98132

99133
/-! ## Equivalence of Definitions -/
100134

101-
/-- Categorical CNO definition is equivalent to our original -/
135+
/-- Categorical CNO definition is equivalent to our original.
136+
137+
Reverse direction: from `∀ s s', eval p s = s' → ProgramState.eq s' s`
138+
we recover the four conjuncts of `CNO.isCNO`:
139+
- `terminates p s` is unconditional (`terminates_always`).
140+
- state preservation is the hypothesis specialised at `eval p s`.
141+
- `pure s (eval p s)` follows because `ProgramState.eq` includes
142+
equality of `ioState` and `Memory.eq` of `memory` — exactly what
143+
`noIO` and `noMemoryAlloc` need (.symm to flip direction).
144+
- `thermodynamicallyReversible` reduces to `0 = 0` (the model's
145+
`energyDissipated` is the constant 0). -/
102146
theorem cno_categorical_equiv (p : CNO.Program) :
103147
CNO.isCNO p ↔ (∀ s s', CNO.eval p s = s' → CNO.ProgramState.eq s' s) := by
104148
constructor
@@ -107,21 +151,50 @@ theorem cno_categorical_equiv (p : CNO.Program) :
107151
rw [← h_eval]
108152
exact h_id
109153
· intro h
110-
sorry -- Need to construct full CNO proof from identity property
154+
refine ⟨?_, ?_, ?_, ?_⟩
155+
· intro s; exact CNO.terminates_always p s
156+
· intro s; exact h s (CNO.eval p s) rfl
157+
· intro s
158+
have hs := h s (CNO.eval p s) rfl
159+
-- hs : ProgramState.eq (eval p s) s, decomposed as (mem, regs, io, pc)
160+
refine ⟨?_, ?_⟩
161+
· -- noIO s (eval p s) := s.ioState = (eval p s).ioState
162+
unfold CNO.noIO
163+
exact hs.2.2.1.symm
164+
· -- noMemoryAlloc s (eval p s) := Memory.eq s.memory (eval p s).memory
165+
unfold CNO.noMemoryAlloc CNO.Memory.eq
166+
intro addr
167+
exact (hs.1 addr).symm
168+
· unfold CNO.thermodynamicallyReversible CNO.energyDissipated
169+
intro s; rfl
111170

112171
/-! ## Functors -/
113172

114-
/-- A functor maps between categories, preserving structure -/
115-
class Functor (C D : Category) where
173+
/-- A functor maps between categories, preserving structure.
174+
175+
Renamed from `Functor` to `CatFunctor` because Lean's core
176+
`Init.Functor` (`class Functor (f : Type u → Type v)`) shadows our
177+
binding when we apply it to a `Category` term — Lean tries to
178+
unify `Category : Type 1` with `Type u → Type v` and fails.
179+
180+
The third parameter binder is `{X Y Z}` rather than `{A B C}` to
181+
avoid shadowing the outer Category-typed `C` (the original
182+
`{A B C : C.Obj}` binding silently re-binds `C` inside the type
183+
`C.Hom B C`, breaking field resolution). -/
184+
class CatFunctor (C D : Category) where
116185
fobj : C.Obj → D.Obj
117186
fmap : ∀ {A B : C.Obj}, C.Hom A B → D.Hom (fobj A) (fobj B)
118187

119188
fmap_id : ∀ {A : C.Obj}, fmap (@Category.id C A) = @Category.id D (fobj A)
120-
fmap_compose : ∀ {A B C : C.Obj} (g : C.Hom B C) (f : C.Hom A B),
121-
fmap (g ∘ f) = fmap g ∘ fmap f
189+
-- The `∘` notation routes through `Category.compose` via instance
190+
-- resolution, but `C`/`D` here are bound *terms* of type Category,
191+
-- not class instances — so `g ∘ f` cannot find them. Spell the
192+
-- composition explicitly through field projections.
193+
fmap_compose : ∀ {X Y Z : C.Obj} (g : C.Hom Y Z) (f : C.Hom X Y),
194+
fmap (C.compose g f) = D.compose (fmap g) (fmap f)
122195

123196
/-- CNOs are preserved by functors -/
124-
theorem functor_preserves_cno (C D : Category) (F : Functor C D)
197+
theorem functor_preserves_cno (C D : Category) (F : CatFunctor C D)
125198
(s : C.Obj) (m : C.Hom s s) :
126199
isCNOCategorical m →
127200
isCNOCategorical (F.fmap m) := by
@@ -132,37 +205,58 @@ theorem functor_preserves_cno (C D : Category) (F : Functor C D)
132205

133206
/-! ## Model Independence -/
134207

135-
/-- Different computational models can be categories -/
208+
/-- Different computational models can be categories.
209+
210+
Pre-existing direction bug: original wrote `F.fmap (G.fmap m)` for
211+
`m : C.Hom s s`, but `G : D ⟶ C` so `G.fmap` consumes `D.Hom`, not
212+
`C.Hom`. The round-trip that respects the types is
213+
`G.fmap (F.fmap m)`: push `m` through `F` to land in `D`, then
214+
pull back through `G` to land in `C` again. -/
136215
def CNOEquivalent (C D : Category) : Prop :=
137-
∃ (F : Functor C D) (G : Functor D C),
216+
∃ (F : CatFunctor C D) (G : CatFunctor D C),
138217
∀ (s : C.Obj) (m : C.Hom s s),
139218
isCNOCategorical m ↔
140-
isCNOCategorical (F.fmap (G.fmap m))
141-
142-
/-- Main Universal Theorem: CNO property is model-independent -/
143-
theorem cno_model_independent (C D : Category) :
144-
CNOEquivalent C D →
145-
∀ (s : C.Obj) (m : C.Hom s s),
146-
isCNOCategorical m →
147-
∃ (m' : D.Hom s s), isCNOCategorical m' := by
148-
intro ⟨F, G, h_equiv⟩ s m h_cno
149-
sorry -- Requires working with equivalence
219+
isCNOCategorical (G.fmap (F.fmap m))
220+
221+
/-- Main Universal Theorem: CNO property is model-independent.
222+
223+
The original statement was type-incorrect: it took `s : C.Obj` and
224+
then quantified `m' : D.Hom s s`, but `D.Hom` requires `D.Obj`. The
225+
fix is to existentially produce both the carrier `s' : D.Obj` and
226+
the morphism `m' : D.Hom s' s'` — set `s' := F.fobj s` and
227+
`m' := F.fmap m`. Functoriality (`fmap_id`) then transports the
228+
identity property: `m = C.id` ⟹ `F.fmap m = F.fmap C.id = D.id`. -/
229+
theorem cno_model_independent (C D : Category) (h_eq : CNOEquivalent C D)
230+
(s : C.Obj) (m : C.Hom s s) (h_cno : isCNOCategorical m) :
231+
∃ (s' : D.Obj) (m' : D.Hom s' s'), isCNOCategorical m' := by
232+
obtain ⟨F, _G, _h_equiv⟩ := h_eq
233+
refine ⟨F.fobj s, F.fmap m, ?_⟩
234+
unfold isCNOCategorical at *
235+
rw [h_cno]
236+
exact F.fmap_id
150237

151238
/-! ## Yoneda Perspective -/
152239

153240
/-- CNOs are precisely those elements that correspond to identity
154-
under the Yoneda embedding -/
241+
under the Yoneda embedding.
242+
243+
The body uses `C.compose m f` directly: as in `CatFunctor`, the
244+
`∘` notation cannot resolve `Category.compose` against a term-level
245+
`(C : Category)`. -/
155246
theorem yoneda_cno (C : Category) (A : C.Obj) (m : C.Hom A A) :
156-
isCNOCategorical m ↔ ∀ (B : C.Obj) (f : C.Hom B A), m ∘ f = f := by
247+
isCNOCategorical m ↔ (∀ (B : C.Obj) (f : C.Hom B A), C.compose m f = f) := by
157248
constructor
158249
· intro h_cno B f
159250
rw [h_cno]
160251
exact C.compose_id_left f
161252
· intro h
162253
unfold isCNOCategorical
163-
-- Take f = id, then m ∘ id = id
254+
-- Take f = id: `C.compose m C.id = C.id`. Then `compose_id_right`
255+
-- rewrites the LHS to `m`, leaving `this : m = C.id` — exactly
256+
-- the goal (no `.symm` — original code had it because the
257+
-- pre-paren parsing was equating the wrong way around).
164258
have := h A C.id
165259
rw [C.compose_id_right] at this
166-
exact this.symm
260+
exact this
167261

168262
end CNOCategory

0 commit comments

Comments
 (0)