[acl2/acl2] cdb4cb: Extended the set-theory library, motivated by maki...

[MattKaufmann]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: cdb4cbdc58ec313f9e5d84a6e8d9b13610725c2c
https://github.com/acl2/acl2/commit/cdb4cbdc58ec313f9e5d84a6e8d9b13610725c2c
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-06-17 (Wed, 17 Jun 2026)

Changed paths:
M books/projects/hol-in-acl2/acl2/lemmas.lisp
M books/projects/set-theory/base.lisp
R books/projects/set-theory/change-pkg.lisp
M books/projects/set-theory/doc.lisp
A books/projects/set-theory/finite/base.lisp
A books/projects/set-theory/finite/finite-domain.lisp
A books/projects/set-theory/finite/finite-restrict.lisp
A books/projects/set-theory/finite/finite-union2.lisp
A books/projects/set-theory/finite/top.lisp
A books/projects/set-theory/image-plus.lisp
A books/projects/set-theory/intersection.lisp
M books/projects/set-theory/package.lsp
A books/projects/set-theory/phoenix.lisp
M books/projects/set-theory/set-algebra.lisp
M books/projects/set-theory/top.lisp
A books/projects/set-theory/topology/cert.acl2
A books/projects/set-theory/topology/compact.lisp
A books/projects/set-theory/topology/finite-intersection-closure.lisp
A books/projects/set-theory/topology/normal.lisp
A books/projects/set-theory/topology/prelims.lisp
A books/projects/set-theory/topology/subspace.lisp
A books/projects/set-theory/utilities/change-pkg.lisp
A books/projects/set-theory/utilities/remove-hypz.lisp
A books/projects/set-theory/zfns.lisp

Log Message:
-----------
Extended the set-theory library, motivated by making a start on a topology library (in books/projects/set-theory/topology/)

Note: Claude Fable 5 (run by Eric Smith, using the interface provided
by Eric McCarthy) assisted with a proof in
books/projects/set-theory/topology/finite-intersection-closure.lisp,
as noted in comments there. I was impressed.

I removed some lemmas in books/projects/hol-in-acl2/acl2/lemmas.lisp
that were added to the set-theory library to support development of
the topology library.

Regarding this effort:

A lot of this work was driven by a goal of proving the theorem in
topology that every compact Hausdorff space is normal. I haven't done
that yet, but I intend to do so. I'm not going to claim any sort of
grand accomplishment if and when I do, though. Consider for example
Josef Urban's "130k Lines of Formal Topology in Two Weeks: Simple and
Cheap Autoformalization for Everyone"
(https://arxiv.org/pdf/2601.03298), in particular the theorem
paracompact_Hausdorff_normal, which I believe is a formalization that
every paracompact Hausdorff space is normal, which is probably a much
deeper result than that every compact Hausdorff space is normal. I
think that also, John Harrison reported a fully automatic proof, via
AI, of that deeper theorem. I don't know how much library support for
set theory was already in place for those efforts. My main goal in
proving the (again) simpler theorem that compact Hausdorff spaces are
normal (again, not yet done!) is just to show that ACL2 with set
theory, which I'm now calling ACL2(zfc) -- and which, unlike the two
systems mentioned above, is based on first order logic -- can be used
to do such proofs. My secondary goal is to push development of the
set theory library. As that library continues to be fleshed out and
as AI continues to further its reach, perhaps many such proofs can
eventually be done automatically.



To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications

[acl2buildserver]

Branch: refs/heads/testing

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel

Commit: ae74fae4b052451567eebbb667c4409d9305120e
https://github.com/acl2/acl2/commit/ae74fae4b052451567eebbb667c4409d9305120e
Author: Alessandro Coglio <em...@alessandrocoglio.info>

Date: 2026-06-17 (Wed, 17 Jun 2026)

Changed paths:

M books/kestrel/c/syntax/abstract-syntax-trees.lisp

Log Message:
-----------
[C$] Make some doc more precise.


Commit: 18677beeac40b0c20d0359db37c8c6c765ca8fe4
https://github.com/acl2/acl2/commit/18677beeac40b0c20d0359db37c8c6c765ca8fe4
Author: Alessandro Coglio <em...@alessandrocoglio.info>

Date: 2026-06-17 (Wed, 17 Jun 2026)

Changed paths:

M books/kestrel/c/syntax/disambiguator.lisp

Log Message:
-----------
[C$] Fix bug in disambiguator.

There was a missing check for turning function parameter declarators to function
name declarators (in C17).

Thanks to Grant Jurgensen for running the disambiguator on an example that led
to the discovery of the bug.


Commit: a9542c5a8cdb80ba5f46cd8f391cf35555943178
https://github.com/acl2/acl2/commit/a9542c5a8cdb80ba5f46cd8f391cf35555943178
Author: Alessandro Coglio <em...@alessandrocoglio.info>

Date: 2026-06-17 (Wed, 17 Jun 2026)

Changed paths:

M books/kestrel/c/syntax/tests/disambiguator-trans-units.lisp

Log Message:
-----------
[C$] Add a disambiguator test.

This demonstrates the fix in the previous commit.


Commit: 094e32b11c33042bf8cf7682d0d767c9c4d99671
https://github.com/acl2/acl2/commit/094e32b11c33042bf8cf7682d0d767c9c4d99671
Author: Alessandro Coglio <em...@alessandrocoglio.info>

Date: 2026-06-17 (Wed, 17 Jun 2026)

Changed paths:

M books/kestrel/c/syntax/tests/validator.lisp

Log Message:
-----------
[C$] Add a validator test.

This was failing prior to the disambiguator fix in the commit before the
previous one.


Compare: https://github.com/acl2/acl2/compare/1786593535ed...094e32b11c33