Email Gateway (Aug 18 2022 at 16:34): Email Gateway (Aug 18 2022 at 16:34):From: Victor Porton <porton@narod.ru>
The following lemma fails to verify (in ZF). It is strange because (simp) should do the job.
lemma comp_eq_id_iff2:
"[| g: B->Ag; f: Af->C; Ag<=Af |] ==> (ALL y:B. f(gy) = y) <-> f O g = id(B)"
proof -
assume "g: B->Ag" "f: Af->C" "Ag<=Af"
hence "f O g: B->C" by (rule comp_fun2)
moreover
have "id(B): B->B" by (rule id_type)
ultimately have m: "(ALL y:B. (f O g)y = id(B)y) <-> f O g = id(B)" by (rule fun_extension_iff)
from g: B->Ag have c [simp]: "y:B ==> (f O g)y = f(gy)" by auto
have i [simp]: "y:B ==> id(B)y = y" by auto
from m show "(ALL y:B. f(gy) = y) <-> f O g = id(B)" by simp
qed
What is my error? What is the right way to do this?
Email Gateway (Aug 18 2022 at 16:34):From: Lawrence Paulson <lp15@cam.ac.uk>
Your problem is in the following line:
have c [simp]: "y:B ==> (f O g)
y = f(g`y)" by auto
This theorem refers to y, a free variable. All the variables (y, B, f, g) in this theorem have fixed meanings. But for your final proof, you need a theorem that holds for all elements of B. You can fix your proof by changing the line as follows:
have c [simp]: "!!y. y:B ==> (f O g)
y = f(g`y)" by auto
Larry Paulson
On 19 Dec 2010, at 21:15, Victor Porton wrote:
The following lemma fails to verify (in ZF). It is strange because (simp) should do the job.
lemma comp_eq_id_iff2:
"[| g: B->Ag; f: Af->C; Ag<=Af |] ==> (ALL y:B. f(gy) = y) <-> f O g = id(B)"
proof -
assume "g: B->Ag" "f: Af->C" "Ag<=Af"
hence "f O g: B->C" by (rule comp_fun2)
moreover
have "id(B): B->B" by (rule id_type)
ultimately have m: "(ALL y:B. (f O g)y = id(B)y) <-> f O g = id(B)" by (rule fun_extension_iff)
fromg: B->Aghave c [simp]: "y:B ==> (f O g)y = f(gy)" by auto have i [simp]: "y:B ==> id(B)y = y" by auto
from m show "(ALL y:B. f(gy) = y) <-> f O g = id(B)" by simp
qedWhat is my error? What is the right way to do this?
Last updated: Apr 26 2024 at 04:17 UTC