Email Gateway (Aug 23 2022 at 08:14): Email Gateway (Aug 23 2022 at 08:14):From: Abel Martin <abel.martin314@gmail.com>
Hello
I am trying to define in a Isabelle theory the property of right
cancellation for function composition but
there are some errors that I can't to fix.
The definition I would like specify in Isabelle is the following:
f : A → B has the property of right cancellation property iff
∀ C : (∀ g, h : B → C ) : g ◦ f = h ◦ f =⇒ g = h
Is it possible? Or more precisely, is it possible to quantify over a type?
Thanks in advance
Email Gateway (Aug 23 2022 at 08:15):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear Martin,
as far as I know, the quantification over types as your ∀ C is not expressible in Isabelle/HOL.
You can provide a polymorphic version though where the type C is given as additional argument.
definition right_cancellation :: "('a ⇒ 'b) ⇒ 'c itself ⇒ bool" where
"right_cancellation f type_argument = (∀ g h :: 'b ⇒ 'c. g o f = h o f --> g = h)”
Moreover, I wondered whether right-cancellation isn’t the same as surjectivity.
If f is not surjective, then it does not have the right-cancellation-property:
Proof: define g and h of type B -> {0,1} as follows:
g(x) = 0
h(x) = if x in image f then 0 else 1
Then clearly g o f = h o f, but g != h since image f != B
On the other hand, let f be surjective and g o f = h o f
and consider an arbitrary x in B. Hence, there must be some y in A such that f(y) = x.
from g o f = h o f conclude g(f(y)) = h(f(y)), so g(x) = h(x) and thus g = h.
Best,
René
Last updated: Apr 18 2024 at 04:17 UTC