John Hughes (Feb 24 2025 at 13:31): John Hughes (Feb 24 2025 at 13:31):I've got a pair of locales defining something called an affine plane: affine_plane_data, which is then included into affine_plane.
I've got another local defining a projective plane. (this is a little bit like having locals for Groups and Rings, say except that a Group starts with a set and two operations, while an affine plane starts with two sets and three functions, so it's a little messier.
There's a construction for taking an affine plane and building an associated projective plane, and I'm trying to formalize it. As a first step, I need to show that there's a unique something with some property; I have a lemma stating that:
datatype ('point, 'line) projPoint = OrdinaryP 'point | Ideal "'line set"
datatype ('point, 'line) projLine = OrdinaryL 'line | Infty
lemma AB:
fixes Points::"'p set"
fixes Lines::"'l set"
fixes meets :: "'p ⇒ 'l ⇒ bool"
fixes join::"'p ⇒ 'p ⇒ 'l"
fixes find_parallel::"'l ⇒ 'p ⇒ 'l"
assumes ap: "affine_plane Points Lines meets join find_parallel"
fixes lp::"'l ⇒ 'l set"
assumes "lp = affine_plane_data.line_pencil Points Lines meets"
fixes P::'p
assumes "P ∈ Points"
fixes pPoints::"('p, 'l) projPoint set"
assumes pp: "pPoints = {OrdinaryP R | R. (R ∈ Points)} ∪ {Ideal s | s k . (k ∈ Lines) ∧ s = lp k}"
assumes "Ideal t ∈ pPoints"
shows "∃! k ∈ Lines . k ∈ t ∧ meets P k"
whose proof I'll omit. The gist of this is "if, in an affine plane, you have a point (P) and a line-pencil (t), you can produce a unique line k as shown in the last line of code.
I'd now like to define a function, point_pencil_join:: 'p => ('p, 'l projPoint) => 'l which says "Given a point and a line-pencil, produce the line guaranteed by the lemma; given anything else, it's undefined."
I have several problems here:
I realize this is all pretty abstract, so offering help is difficult. But if someone has an example (even in the HOL sources) of something like this being done, I'd love to see it. A kind of simple example would be something like
(a) a theorem showing that for any two integers $x$ and $y$ there are unique Bezout coeffiients $a$ and $b$ with $ax + by = gcd(x,y)$. (Alas, they're not actually unique, but bear with me), and then
(b) using that theorem to write
define bezout_pair:: int => int => int x int where ...
Chelsea Edmonds (Feb 24 2025 at 14:54):Some quick suggestions without looking too closely. In my experience for constructing mathematical objects, the function/definition does the construction, then you prove a seperate lemma(s) showing that given certain assumptions holding on the inputs, the result of the function/definition has the properties you want (e.g. is unique etc). Alternatively, if you don't know how to explicitly construct the object consider using the THE keyword in a definition (i.e. THE x . P x represents a unique value that satisfies some predicate P). There are plenty of examples of the latter in the libraries if you do a quick search (SOME is a weaker keyword, which doesn't imply uniqueness). Similar lemmas are still useful in this approach for simplifying reasoning on the definition.
Chelsea Edmonds (Feb 24 2025 at 14:59):More generally, I have done a lot of work on formalising combinatorial designs - specifically using locales effectively to do so (including constructions which combine several different designs to get a new one etc). Steiner systems and projective planes have the same underlying structure, so this could potentially be useful? Even if just as examples of locale usage in this way. This library is a good starting point: https://www.isa-afp.org/entries/Design_Theory.html (the hypergraph and undirected graph theory libraries also show other extensions using locales to represent the same structures using different terminologies/types etc).
Chelsea Edmonds (Feb 24 2025 at 16:06):Also just saw someone else share this great past message re using THE if you go with that approach:
Last updated: Apr 18 2025 at 20:21 UTC