An analysis of the Bernstein’s theorem for
an
automatedprover
byHidetsune Kobayashi Institute of ComputationalLogic
Yoko Ono
Yokohama City University
abstract
Ouraimis tolet
an
automatedprover
generatea
prooftothe Bernstein’stheorem
on
the settheory. Theprover
can
takesome
propositions out froma
data base at each proof step. However, sincewe
have several propositions applicableto
a
step,we
have toomany
roots to check.But, if
we
havea
rough scenario ofa
proof, thenwe
have only to checksome
conflned routes.This report is
an
analysisofthe Bernstein’s theoremtosee
howa
proof consists and tosee
ifwe
can
givea
scenario to theprover.
1. Introduction
Atfirst,
we
introduce the Bernstein’s theorem:Let$f$be
an
injecUve mapfroma
setAtoa
setB. If there isan
injective map $g$from$B$ to$A$, the two setsAand$B$ have thesame
cardinality.That is,
we
havea
one
toone
onto mapfromAto B.This is
a
famous propositionon
the set theory, andwe
havea
short proof requiring at most 10linestowrite down. But, fora
formal proof,we
require about ten timesmore
lines toexpress
the proof, becauseno
logicalgaps are
allowedandwe use
elementary propositionson
the settheory stored ina
data base. 2. Bernstein’s theoremAtflrst
we
havea
big modification ofthe proposiUon:We
use
thesame
notationsas
in 1. Since, $g$isa
one
toone
map from$B$ to$g(B)$, and $g\circ fis$ a
one
toone
map from Ato $g\circ f(A)$which isa
subset of$g(B)$, ifwe
can
flnda one
toone
map from$g(B)$ to$A$,we
havea one
toone
onto mapfrom$A$to B. Therefor
we
haveonlytoshow:let Al be
a
subset$ofA$, and let$f$bea
one
toone
map fromAintoAl,Ourprover
use
Isabelle/HOLas
the inference engine,we express
the lastproposition
as
$[A1\subseteq A,$ $f:Aarrow$ Al, inj
on
$fA]\Rightarrow\exists\varphi.$$bi|_{-}to\varphi A$Al.3. Existing files in Isabelle/HOL.
Aproofis
a
sequence of proposiUons derived logically correct change fromthe formerproposition. Alogically correct changeis given by applying
an
alreadyproved proposition. Hereafter, to avoid
a
confusion,we
callthe already proved propositionas
a
rule, anda
proposition to be proved is called simplyas a
proposition. InIsabelle/HOL,
a
file containingpropositions and proofs is calleda
theoryfile (it is named
as
$*.thy$)Rules
are
taken from existing thy files and from anew
thyfile “Bernstein.thy”. Existing filesare:
HOL.thy Elementary rules concerninglogical propositions Set.thy Elementary set theory
Fun.thy Elementaryproperties offunctions FuncSet.thy Elementaryproperties offunctions Thenewfile “Bernstein.thy” is writtentoprove the therem.
4. Key
definitions
The proof requires three key definitions. The flrst
one
is given byusingthe primitive recursionas:
primrec $itr::\prime[nat,a*|a]\Rightarrow(a\Leftrightarrow a)^{\dagger/}$ where
$itr_{-}0:\prime\prime itr0f=f"|$ $itr_{-}Suc:\prime\prime itr$(Suc n)$f=f\circ(\dot{\ovalbox{\tt\small REJECT}}trnf)^{\iota\iota}$
The second
one
isa
definition givinga
special subset ofAl: definition $A2set::’/[’a*^{\iota}a$,ta
set,‘a
set] $*’a$set“
where $ltA2setf$A Al $==\{\cross.$ $\cross\in Al\wedge (\exists y\in (A- A1). \exists n. itr nfy=\cross)\}"$The third is
a
map
which is proved to be bijective later. This is the functionwe
looked for:definition Bfunc::$\dagger/[’a\not\subset 3^{1|}a,a$ set,
‘a
set] $c*(’aI*^{t}a)^{t/}$ where‘
Bfunc$f$A Al $==\lambda\cross\in A.$ $|\prime f$$(\cross\in (A- A1)u(A2setf A Al))$ then $f\cross elseX"$
5. Finalprop$0$sitions to prove.
Our goalisto show Bfunc defined above is
a
bijectivemap. Following two propositions implythat Bfuncis bijective. Bydefinition, ifa
functionis injective and also surjective, it is bijective.lemma $Bfunc\lrcorner n|:"[A1\subseteq A;f\in Aarrow$ Al; $In|_{-}$
onfAJ
$\Rightarrow$$in|_{-}on$ (Bfunc$f$A Al) $A”$
lemma $Bfunc_{-}sur|:"[A1\subseteq A;f\in Aarrow Al; in|_{-}onfA]\Rightarrow$ $sur|_{-}to$ (Bfunc $f$AAl) $AA1”$
?he flrstlemmanamed $Bfunc_{-}inj$
means:
LetAl be
a
subset ofa
set$A$, and let$f$bean
injectivemap
fromAtoAl,then Bfunc $f$A Al” isinjective.
The second lemma
means
that Bffinc $fA$Al” isa
surjectivemap
fromA toAl.6. Rules applied to
prove
thelemma $uBfunc$ inj”.We list rules explicitly applied to
prove
the lemma $Bfunc_{-}inj$”:
From HOL.thy balll, impl , $bo\cross_{-}equals$
From Fun.thy $inj_{-}on_{-}defin|_{-}on\lrcorner ff$
From FuncSet.thy funcset mem, Di$ff\lrcorner ff$
From Bernstein.thy $Bfunc_{-}eq,$ $Bfunc_{-}eq1,$ $A2set_{-}as_{-}range$
As
a
prooftechniquewe
use
case-tac
as:
case
$-tac\cross|\in A$ –Al $uA2setfAA1^{\iota/}$case
$-tac’ y\prime\in$ A-Al $uA2setfAA1”$Case-tac
givesa
pair ofpropositionsone
withan
extraassumption given inthequotation, and another
one
withan
extra assumpUonwith negation ofthe assumption given in the quotation. For example, the lastcase-tac
givestwopropositions
one
with $\prime\prime y\in A$ –Al $uA2$set$fAA1”$as
an
extra assumption andanotherproposition with $y\not\in A$ –Al $uA2$set$fAA7”$
We place fllesin
a
order from elementaryone
to complicatedone:
HOL.thy, Set.thy, Fun.thy, FuncSet.thy, Bernstein.thy.7. Rules Bfunc-eq, Bfunc-eql, $A2set_{-}as_{-}range$
proved by explicitly applying rules;
Bfunc-eq
refl, subset$D,$ $Bfunc_{-}def$, lambda$-funA2set_{-}sub$
Bfunc-eql
Bfunc$-def$ $A2set_{-}as_{-}range$
conjl, bexl, exl, funcsetl, conj$E,$ $be\cross E,$ $e\cross E,$ $\arg_{-}cong$ subset$D$, Collectl,
$UnE$, Collect$E,$ $funcset_{-}mem,$ $A2set_{-}def,$ $A2set_{-}sub,$ $itr_{-}O,$ $Itr_{-}Suc$
8. The chain ofrules backward from Bfunc$-$inj
To illustrate howthe proof of $Bfunc\lrcorner nj$” consists,
we
showa
chain oflemmas backward from “Bfunc-inj”.
Bfunc def $\cdots$
Bfunc-eq
lambda-fun
$\cdots$A2 set sub $\cdots$
$Bfunc\lrcorner nj$ Bfunc-eql Bfunc def $\cdots$
A2
set-as range
$A2set_{-}def$ $\cdots$A2 set sub $\cdots$
$Itr_{-}O$,
ltr-Suc
$\cdots$9. How
a
rule changesa
proposition.We give
an
example ofa
part ofa
proofto show how rules changea
givenproposition. $A$propositionto prove is “Bfunc-inj”.
lemma$Bfunc\lrcorner n|:"[A1\subseteq A;f\in Aarrow Al; in|_{-}onfA]\Rightarrow in|_{-}on$(Bfunc $f$A Al) $A”$
apply$($subst $in|_{-}on_{-}def)$
Here, $Bf\lfloor 1nc_{-}inj$” is
a
proposition to prove. The nextline isa
commandwe
aska
prover change the originalproposition. Then the inferenceengine Isabelle/HOL
returns
a
propositionderived by applying the rule subst $inj_{-}on_{-}def$’as
$1.$ $\prime\prime[A1\subseteq A;f\in Aarrow Al; in|_{-}onfA]\Rightarrow$
$\forall\cross\in A.$ $\forall y\in A$
.
Bfunc $f$A Al $x=$ Bfunc $f$A AlIn fact, the deflnition of“inj-on” is substitutedin the conclusionpart. The following command changes by the rule “ball$I$” and subsequently“ball$I$” again.
apply (ruleballl, rule balll)
1. $\Lambda\cross y.$ $[A1\subseteq A,\cdot f\in Aarrow$ Al; $in|_{-}onfA;\cross\in A;y\in AI\Rightarrow$
Bfunc$f$AAl$x=$ Bfunc$f$AAl$yarrow\cross=y$
apply (rule impl)
1. $\Lambda\cross y$
.
[Al $\subseteq A;f\in Aarrow A1;in|_{-}onfA;\cross\in A;y\in A$Bfunc$f$A Al $\cross=$ Bfunc$f$AAl$y$] $\Rightarrow\cross=y$
apply $(case_{-}tac"x\in A- A1 uA2setf A A1^{\iota/})$
1. $\Lambda\cross y.$ $[$ Al $\subseteq A;f\in Aarrow A1;in|_{-}onfA;\cross\in A;y\in A$;
Bfunc$f$A Al$\cross=$ Bfunc$f$AAl $y;\cross\in A$ –Al $uA2$setfA ] $\Rightarrow\cross=y$
2. $\Lambda\cross y$
.
[Al $\subseteq A;f\in Aarrow$Al; $in|_{-}onfA;\cross\in A;y\in A$;Bfunc$f$A Al $\cross=$Bfunc$f$A Al$y;x\not\in A$ –Al $uA2$setfA ] $\Rightarrow x=y$
Weneed apply $(case\lrcorner ac"y\in A$ –Al $uA2$set $fAA1”)$, but itis abbreviatedl
apply$(frule\lrcorner aca=x in Bfunc_{-}eq[of Al A \eta, assumption+)$
1. $\Lambda\cross y.$ $[$ Al $\subseteq A;f\in Aarrow A1;in|_{-}onfA;\cross\in A;y\in A$; Bfunc$f$A Al $x=$
Bfunc$f$A Al$y_{1}\cdot\cross\in A$ –Al $uA2setfA$; Bfunc$f$A Al $x=\cross$] $\Rightarrow\cross=y$
2. abbreviated
Above application of Bfunc-eq shows how rules work. It flxes
a
part ofpath towards the conclusion. Thismeans
thata
rule decidesa
part of proof path.10. Who gives a rule at each proofstep?
Ouraimis to make
an
automatedprover
which choosesproper
rules at each step ofthe proof. Actually, it is quite hard to give definitions“Bfunc“ and $A2_{-}set$knowledge data base.
“case-tac”
isalso difficulttactic touse
unless the proverhas
no
mathematical idea. Thereforwe
have tostore suchknowledgewithinstruction howto
use.
Theformal proofto the Bernstein’s theoremis written by
a
human. Startingfrom the original proposition, it is changedby
a
rule with$a/$some
simplemathematical property/properties. The proofdirection is controled carefully. In
section 8,
we
gave
a
diagram of rules. But, in the diagram,we
listed onlyrules whichare
usedon
the correctway tothe finalproof. Infact, we have muchmore
rules applicable ata
step (and probably, it takesus
toa
wrong
way). Here,we
stressagain, mathematical ideas
are
indispensable to reach thegoal. $A$scenariofor the proof ofthe Bernstein’s theoremis:
1. give
a
simple form of the original proposition.2. prove that
a
proof of the theorem is derived bya
simplifled proposition.3. prove the simplified proposition.
Our proverchoose
an
applicable rule ifthe rule satisfiessome
necessary
conditions. Among those applicable rules,
we
can
throwoutsome unnecessary
rules with
some
mathematical ideas. In the proof of the Bernstein‘s theorem,within scenario 3,
we
needan
instructiontouse
case-tac.
Thereforgivinga
scenario is not enough to generatea
proposition, andwe
needsome
detailed mathematical ideas.References
1. S. Kametani, Set and topoloy, Asakura, (inJapanese)
2. T. Nipkow, L. Paulson, M. Wenzel, $A$proof assistant for higherorderlogic,