I am trying to prove the following basic theorem about the existence of the inverse function of a bijective function (to learn theorem-proving with Isabelle/HOL):
For any set S and its identity map 1_S, α:S→T is bijective iff there exists a map β: T→S such that βα=1_S and αβ=1_S.
Below is what I have so far after some attempts to define relevant things including functions and their inverses. But I am pretty stuck and couldn't make much progress due to my lack of understanding of Isabelle and/or Isar.
theory Test
imports Main
"HOL.Relation"
begin
lemma bij_iff_ex_identity : "bij_betw f A B ⟷ (∃ g. g∘f = restrict id B ∧ f∘g = restrict id A)"
unfolding bij_betw_def inj_on_def restrict_def iffI
proof
let ?g = "restrict (λ y. (if f x = y then x else undefined)) B"
assume "(∀x∈A. ∀y∈A. f x = f y ⟶ x = y)"
have "?g∘f = restrict id B"
proof
(* cannot prove this *)
end
In above, I try to give an explicit existential witness (i.e. the inverse function g
of the original function f
). I have several issues about the proof.
whether the concepts are defined right (functions, inverse functions etc.) in Isabelle terms.
how to expand the relevant definitions and then simplify them with function applications. I have followed some Isabelle (2021) examples/tutorials about both the apply-style simp, and structured style Isar proof but couldn't use the Isar proof fluently. Once I started the proof command, I don't know how to simp or move any further.
Isar has the new way of
assumes ... shows ...
for stating the theorem. Is there similar support for proving iff's (⟷
) like the example above? Without it, there is no access toassms
etc., and is it necessary toassume
everything except the conclusion during the proof.
Can someone help explain how the above existential proof about inverse function can be accomplished?
I agree with the insightful remarks provided by Dominique Unruh. However, I would like to mention that a theorem that captures the idea underlying the theorem that you are trying to prove already exists in the source code of the main library of Isabelle/HOL. In fact, it exists in at least two different formats: let me name them the traditional Isabelle/HOL format and the canonical
FuncSet
format. For the former one, see the theorembij_betw_iff_bijections
:The situation is a little bit more complicated with
FuncSet
. There does not seem to exist a single theorem that captures the idea. However, together, the theoremsbij_betwI
,bij_betw_imp_funcset
andinv_into_funcset
are nearly equivalent to the theorem that you are trying to state. Let me provide a sketch of how one could express this theorem in a manner that would be considered reasonably canonical in theFuncSet
sense (try to prove it yourself):I would also like to repeat the advice given by Dominique Unruh and provide several side remarks:
Indeed, this is a very good idea. In general, by trying to restrict the problem to explicitly defined sets
A
andB
, instead of working directly with types, you touched upon a topic that is known as relativization in logic. For a mild layman's introduction see, for example, https://leanprover.github.io/logic_and_proof/first_order_logic.html [1], for a slightly more thorough introduction in the context of set theory see [2, chapter 12]. As you have probably noticed by now, it is not that easy to relativize theorems in Isabelle/HOL and requires additional proof effort. However, there exists an extension of Isabelle/HOL that allows for the automation of the process of the relativization of theorems. For more information about this extension see the article From Types to Sets by Local Type Definition in Higher-Order Logic by Ondřej Kunčar and Andrei Popescu [3]. There also exists a large scale application example of the framework [4]. Independently, I am working on making this extension more user-friendly and very slowly approaching the final stages in my efforts: see https://gitlab.com/user9716869/tts_extension. Thus, in principle, if you know how to use Types-To-Sets and you accept its axioms, then it is sufficient to prove the theorem withbij
, e.g.,"bij f ⟷ (∃g. (∀x. g (f x) = x) ∧ (∀y. f (g y) = y))"
,Then, the theorems like
bij_betw_iff_bijections
andbij_betw_iff
can be synthesized automatically for free upon a click of a button (almost...).Finally, for completeness, let me offer my own advice with regard to your queries (although, as I mentioned, I agree with everything stated by Dominique Unruh)
I believe that the best way to learn what you are trying to learn is by following through the exercises in the book Concrete Semantics by Tobias Nipkow and Gerwin Klein [5]. Additionally, I would also look through A Proof Assistant for Higher-Order Logic by Tobias Nipkow et al [6](it is slightly outdated, but I found it to be useful specifically for learning
apply
-style scripting/direct rule application). By the way, I have mostly self-taught myself Isabelle from these books without any prior experience in formal methods.I will make the advice given by Dominique Unruh more explicit: use
rule iffI
orintro iffI
for this.Edit. When you use
rule iffI
(or similar) to start your structured Isar proof, you need to state your assumptions explicitly for every subgoal (using theassume ... show ...
paradigm). However, there is a tool that can generate such boilerplate Isar code automatically. It is called Sketch-and-Explore and you can find it in the directoryHOL/ex
of the main library of Isabelle/HOL. In this case, all you need to do is to typesketch(rule iffI)
and theassume
/show
paradigm will be generated automatically for every subgoal.References