Quotient Basics and warnings · Beginner Questions

With the goal of eventually defining PGL(3, R) (3x3 invertible matrices over the reals, where two matrices are 'the same' if one is a nonzero scalar multiple of the other), we ran into troubles almost immediately, and have distilled them down to this minimal example (replacing "3" with "2" for simplicity). The example was produced in analogy with the definition of rationals (i.e., I didn't completely understand what I was doing):

theory Quo
  imports Main "HOL-Analysis.Finite_Cartesian_Product"
begin

type_synonym t = "(real,2) vec"

definition rel::"t ⇒ t ⇒ bool" where
"rel x y = (x$1 = y$1)"

quotient_type q = "t" / "rel"
  morphisms Abs_rel Rep_rel
  by (metis equivpI reflpI rel_def sympI transpI)
end

which generates No map function defined for Finite_Cartesian_Product.vec. This will cause problems later on. and

Generation of a parametrized correspondence relation failed.
Reason:  No relator for the type "Numeral_Type.bit0" found.

When I changed to (real, 3) vec, the second error turned into .bit1; when I changed to (real, 4) vec it changed back to .bit0, at which point I realized I was beyond my depth.

The corresponding theory using ordered pairs (and a proof discovered by sledgehammer) actually works without errors/warnings:

theory Quo
  imports Main "HOL-Analysis.Finite_Cartesian_Product"
begin

type_synonym t = "real × real"

definition rel::"t ⇒ t ⇒ bool" where
"rel ≡ %(a,b)  . %(x, y) .   (x=a)"

quotient_type q = "t" / "rel"
  morphisms Abs_rel Rep_rel
  by (metis (mono_tags, lifting) equivp_def rel_def split_beta)
end

but since I'll actually need the vec stuff for defining my matrices, and don't want to rederive all imaginable linear algebra stuff (determinants!), I'd really like to get the first version to work if that's possible. Googling for the error messages didn't yield a lot of insight, unfortunately: two were pointers to source code, and one (https://groups.google.com/g/fa.isabelle/c/IOc9mYXxxFo) includes a note from Ondřej Kunčar that suggests that the two errors can be ignored, an idea that always worries me.

irvin (Jul 14 2025 at 12:10):

The issue is that vec is not registered as a BNF and thus your quotient type fails to register as a BNF. I do not understand BNF's enough to know whether you can register vec as a BNF but I would agree that you can ignore those warning unless you fail to define a new datatype depending on q

John Hughes (Jul 14 2025 at 12:50):

datatype junk = Junk "q"

in the first example, and then never use the datatype junk again, I should be OK?

(BTW, I tried to read about BNFs a while back, and can confidently say that I also do not understand them well enough!)

irvin (Jul 14 2025 at 14:27):

I'm saying that if you encounter failure when trying to define a new datatype that uses q, then I would bother figuring out whether I can fix this problem. Otherwise I would just ignore it.

John Hughes (Jul 14 2025 at 15:17):

Of course!...that's a much more reasonable interpretation of the sentence you wrote! Thanks for the clarification.

irvin (Jul 14 2025 at 15:19):

Wait I might be completely wrong. I just looked at the code behind quotient_type and it does not seem to be related to bnfs at all.

irvin (Jul 14 2025 at 17:34):

definition map_vec where
"map_vec f g v = vec_lambda (map_fun g f (vec_nth v))"
functor map_vec
  unfolding map_vec_def
   apply fastforce
  using eq_id_iff by fastforce

Stream: Beginner Questions

Topic: Quotient Basics and warnings