Email Gateway (Aug 22 2022 at 18:52): Email Gateway (Aug 22 2022 at 18:52):From: "John F. Hughes" <jfh@cs.brown.edu>
[Apologies for previous incomplete message]
Again, I'm trying to work with affine geometries. It seemed that proving
things about general affine geometries might be like proving things about
general groups, or modules, or other things like that...but because I seem
to have two type-parameters, the "class" approach used in
http://isabelle.in.tum.de/library/HOL/HOL-Isar_Examples/Group.html
won't work. So I went back to locales. I wanted to say that in a geometry,
there are "points" and "lines", and that a point may or may not be on a
line. An initial version of this said that Points was an 'a set, and Lines
was an 'a set set, but then when I wanted to define "parallel" as a
predicate on pairs of lines, I ended up with a predicate on pairs of 'a
sets (not all of which are lines). So I backed off and said that point and
line are types, and there's a predicate, "meets P l" that tells whether a
point P is on the line l. That seemed to work OK (see the first part of the
code below).
But then I wanted to extend that to include some of the axioms of an affine
geometry (see the second locale below).
I initially wrote axiom a1b, for which I got a "unification failed" error.
Then I wrote a1a, which worked. My questions are, "Why did Isabelle decide
that the names 'a and 'b were better than the ones that I chose, and can I
prevent this, so that the rest of my work is more readable?"
--John
My minimal example follows.
section ‹Basic affine geometries›
theory Affine1
imports Main
begin
locale affine_plane_basics =
fixes
meets :: "'point ⇒ 'line ⇒ bool"
locale affine_plane = affine_plane_basics +
assumes
a1a: "⟦ (P::'a) ≠ Q ⟧ ⟹ (∃! (l::'b). meets P l ∧ meets Q l)"
(* This version fails:
a1b: "⟦ (P::'point) ≠ Q ⟧ ⟹ (∃! (l::'line). meets P l ∧ meets Q l)"
*)
...
Email Gateway (Aug 22 2022 at 18:56):From: Makarius <makarius@sketis.net>
On 31/12/2018 23:02, John F. Hughes wrote:
So I backed off and said that point and
line are types, and there's a predicate, "meets P l" that tells whether a
point P is on the line l. That seemed to work OK (see the first part of the
code below).
Note that Isabelle sources are formal proof documents, not "code". This
is formal mathematics, not programming. (Our would you call this mail
text "code", because it was processed on a computer in fixed-width font?).
But then I wanted to extend that to include some of the axioms of an affine
geometry (see the second locale below).I initially wrote axiom a1b, for which I got a "unification failed" error.
Then I wrote a1a, which worked. My questions are, "Why did Isabelle decide
that the names 'a and 'b were better than the ones that I chose, and can I
prevent this, so that the rest of my work is more readable?"
This is due to standard policies of Hindley-Milner type inference. There
are certain rules for implicit scopes of type variables: sometimes they
are fixed, sometimes arbitrary. Referring to things with arbitrary types
in a different context produces most general canonical types,
enumeration of fresh variable names like 'a, 'b, 'c, ...
If you want different type names, you can put explicit type constraints
just in the right spot, e.g. like this:
locale affine_plane_basics =
fixes meets :: "'point ⇒ 'line ⇒ bool"
locale affine_plane =
affine_plane_basics meets for meets :: "'point ⇒ 'line ⇒ bool" +
assumes a1b: "P ≠ Q ⟹ ∃!l. meets P l ∧ meets Q l"
Note that I have removed the pointless type-constraints from the a1b
proposition.
Quite often it is better not to want different type variable names, but
let the type inference do its business unhindered.
There is a certain art to work with type-inference such that it does the
right thing most of the time, without further ado.
Makarius
Last updated: Apr 25 2024 at 12:23 UTC