Email Gateway (Aug 19 2022 at 12:33): Email Gateway (Aug 19 2022 at 12:33):From: Filip Marić <filipmatfbgacrs@gmail.com>
Hello,
I am using the quotient package in Isabelle 2013 and I get an error
when I try to use the descending method and the type real is involved
in the quotient_definition. Here is a (simlified) example.
(* Homogeneous coordinates in the complex plane *)
fun homo_coords_eq :: "complex \<times> complex \<Rightarrow> complex
\<times> complex \<Rightarrow> bool" where
"homo_coords_eq (z1, z2) (w1, w2) \<longleftrightarrow> (\<exists>
k::complex. k \<noteq> 0 \<and> w1 = k * z1 \<and> w2 = k * z2)"
quotient_type
complex_homo_coords = "complex \<times> complex" / homo_coords_eq
proof (rule equivpI)
show "reflp homo_coords_eq" unfolding reflp_def by (auto, rule_tac
x=1 in exI, simp)
next
show "symp homo_coords_eq" unfolding symp_def by (auto, rule_tac
x="1/k" in exI, simp)
next
show "transp homo_coords_eq" unfolding transp_def by (auto, rule_tac
x="k*ka" in exI, simp)
qed
(* Zero *)
definition zero_rep :: "complex \<times> complex" where "zero_rep = (0, 1)"
quotient_definition zero where "zero :: complex_homo_coords" is zero_rep
done
(* Coercion of complex number - everything is OK *)
definition of_complex_rep :: "complex \<Rightarrow> complex \<times>
complex" where "of_complex_rep x = (x, 1)"
quotient_definition of_complex where "of_complex :: complex
\<Rightarrow> complex_homo_coords" is of_complex_rep
done
lemma "of_complex 0 = zero"
by (descending) (auto simp add: zero_rep_def of_complex_rep_def)
(* Coercion of real number - descending raises an error *)
definition of_real_rep :: "real \<Rightarrow> complex \<times>
complex" where "of_real_rep x = (complex_of_real x, 1)"
quotient_definition of_real where "of_real :: real \<Rightarrow>
complex_homo_coords" is of_real_rep
done
lemma "of_real 0 = zero"
apply (descending)
*** [regularize (constant mismatch)
*** tmp.of_real::(nat \<Rightarrow> (nat \<times> nat) \<times> nat
\<times> nat) \<Rightarrow> complex \<times> complex
*** tmp.of_real::real \<Rightarrow> complex_homo_coords]
*** The quotient theorem
*** tmp.of_real 0 = zero
*** does not match with original theorem
*** homo_coords_eq (tmp.of_real 0) zero_rep
*** At command "apply" (line 40 of "/home/filip/Dropbox/moebius/tmp.thy")
The same behavior occurs with every quotient definition where the type
real is involved - it seems that instead of real the system expects
(nat \<Rightarrow> (nat \<times> nat) \<times> nat \<times> nat) - I
suppose that is because real type itself is defined as a quotient? Is
there a way to make the given example work and to use the type real in
quotient definitions as any other type?
Thank you!
Filip
Email Gateway (Aug 19 2022 at 12:33):From: Dmitriy Traytel <traytel@in.tum.de>
Hello Filip,
I cannot say anything about the descending method, but your example
works fine with Lifting and Transfer in Isabelle 2013 (see below). And
since there are plans to eventually remove the Quotient package
(https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-March/msg00026.html),
I would recommend to use these more recent tools.
Dmitriy
(* Homogeneous coordinates in the complex plane *)
fun homo_coords_eq :: "complex × complex ⇒ complex
× complex ⇒ bool" where
"homo_coords_eq (z1, z2) (w1, w2) ⟷ (∃
k::complex. k ≠ 0 ∧ w1 = k * z1 ∧ w2 = k * z2)"
quotient_type
complex_homo_coords = "complex × complex" / homo_coords_eq
proof (rule equivpI)
show "reflp homo_coords_eq" unfolding reflp_def by (auto, rule_tac
x=1 in exI, simp)
next
show "symp homo_coords_eq" unfolding symp_def by (auto, rule_tac
x="1/k" in exI, simp)
next
show "transp homo_coords_eq" unfolding transp_def by (auto, rule_tac
x="k*ka" in exI, simp)
qed
(* Zero *)
definition zero_rep :: "complex × complex" where "zero_rep = (0, 1)"
lift_definition zero :: "complex_homo_coords" is zero_rep
unfolding zero_rep_def by simp
definition of_complex_rep :: "complex ⇒ complex × complex" where
"of_complex_rep x = (x, 1)"
lift_definition of_complex :: "complex ⇒ complex_homo_coords" is
of_complex_rep
unfolding of_complex_rep_def by simp
lemma "of_complex 0 = zero"
by transfer (auto simp add: zero_rep_def of_complex_rep_def)
definition of_real_rep :: "real ⇒ complex ×
complex" where "of_real_rep x = (complex_of_real x, 1)"
lift_definition of_real :: "real ⇒ complex_homo_coords" is of_real_rep
unfolding of_real_rep_def by simp
lemma "of_real 0 = zero"
by transfer (auto simp add: zero_rep_def of_real_rep_def)
Email Gateway (Aug 19 2022 at 12:34):From: Filip Marić <filipmatfbgacrs@gmail.com>
Dmitriy,
I have successfully migrated my formalization - it was quite easy to
do, and everything works fine now. Thank you very much for your
advice!
Filip!
Last updated: Nov 21 2024 at 12:39 UTC