Email Gateway (Aug 23 2022 at 08:20): Email Gateway (Aug 23 2022 at 08:20):From: "John F. Hughes" <jfh@cs.brown.edu>
I'm having trouble with quotients, and I suspect that I'm trying to use a
tool in the wrong place, but I'm not sure what tool I *should *be using.
Here's the setup:
In synthetic projective geometry, you can define an affine plane to be a
pair of sets ("points" and "lines") and a function "meets P k" which is
true when the point P "is on" the line k; the "meets" function has to
satisfy certain properties ("two points determine a line", etc.) to make
this an affine plane. (Alternatively, one could define the "lines" to be
certain subsets of "points", and "meets" gets replaced by "element of";
that makes it more difficult to prove duality theorems later, though). In
Isabelle, I've represented this with a locale:
theory QuoExample
imports Complex_Main
begin
locale affine_plane_data =
fixes meets :: "'point ⇒ 'line ⇒ bool"
begin
definition parallel:: "'line ⇒ 'line ⇒ bool" (infix "||" 50)
where "l || m ⟷ (l = m ∨ ¬ (∃ P. meets P l ∧ meets P m))"
definition collinear :: "'point ⇒ 'point ⇒ 'point ⇒ bool"
where "collinear A B C ⟷ (∃ l. meets A l ∧ meets B l ∧ meets C l)"
end
value "affine_plane_data"
locale affine_plane =
affine_plane_data meets
for meets :: "'point ⇒ 'line ⇒ bool" +
assumes
a1: "P ≠ Q ⟹ ∃!l. meets P l ∧ meets Q l" and
a2: "¬ meets P l ⟹ ∃!m. l || m ∧ meets P m" and
a3: "∃P Q R. P ≠ Q ∧ P ≠ R ∧ Q ≠ R ∧ ¬ collinear P Q R"
begin
lemma symmetric_parallel: "l || m ⟹ m || l"
using parallel_def by auto
lemma reflexive_parallel: "l || l"
by (simp add: parallel_def)
lemma transitive_parallel: "⟦l || m ; m || n⟧ ⟹ l || n"
by (metis a2 parallel_def)
================
At this point, I want to "complete" the affine plane. For the ordinary
Euclidean plane, this consists of adding a "point at infinity" to each
line, with the rules that two parallel lines have the same point at
infinity added to them, and then tossing all these newly added points into
a new line (the line at infinity). So the "points" of my new space (which
is a PROJECTIVE geometry rather than an affine one) are (1) all the old
points, and (2) all the new "points at infinity", one for each set of
parallel lines in the Euclidean plane.
The same idea works for any affine geometry: for each "family of parallel
lines", you create a new point, and you then use these new points in
building a projective plane. The general idea here is that given a function
"meets: 'point -> 'line -> bool", we can build a function
"meets2 : 'newpoint -> 'newline -> bool", where the type "newpoint"
consists of all original points, plus all the "points at infinity." It's
natural to define something like
quotient_type pencil = "'line" / "parallel"
type ('point 'line) newpoints = OriginalPoint 'point | InfinitePoint 'pencil
type ('point 'line) newline = OriginalLine 'line | InfiniteLine
and then carefully define the meets2 function on these things. (I'm sure
I've got the syntax on the second and third lines wrong, but it doesn't
matter because the very first line of this construction fails: I can't
construct the type "pencil"; trying to do so gives me
"pencil": extra type variable(s) on the lhs: "'line"
"pencil": extra type variable(s) in the relation: "'line", "'point"
"pencil": illegal variable(s) in the relation: "meets"
=================
Is there a way to do this in Isabelle? The general idea --- you have
something that satisfies some axioms, based on items of some fixed but
unknown type -- and want to construct associated quotients, certainly
happens often enough in mathematics. A group, for instance, might
consist of matrices, or real-to-real functions, or permutations, or ...
lots of things. But in all cases, we can have a notion of a normal subgroup
and quotient groups. I looked at the HOL/HOL-Algebra/Coset.html entry,
thinking I'd see there exactly how to use quotients but ... there are no
quotients there, which made me suspect that quotients in Isabelle aren't
quite what I think they might be.
Advice, anyone?
Email Gateway (Aug 23 2022 at 08:20):From: "John F. Hughes" <jfh@cs.brown.edu>
By the way, even if I parameterize that quotient definition, writing
quotient_type ('point, 'line) pencil = "'line" / "parallel"
I still get
"pencil": illegal variable(s) in the relation: "meets"
Closer, but not close enough!
Last updated: Apr 16 2024 at 12:28 UTC