I was trying to recreate a simplified version of the natural numbers, for learning purposes (as it involves inductive definitions, recursive functions, etc...). In that process however, I got stuck in something that I thought would be very trivial.
Basically, I have a definition for natural numbers 'natt
' and a definition for the '<
' relation:
datatype natt = Zero | Succ natt
primrec natt_less :: "natt ⇒ natt ⇒ bool" (infixl "<" 75) where
"natt_less n Zero = False"
| "natt_less n (Succ m') = (case n of Zero ⇒ True | Succ n' ⇒ natt_less n' m')"
and from these, I tried to prove 3 basic properties of the <
relation:
- Non-reflexivity:
~ (a < a)
- Non-symmetry:
a < b ⟹ ~ (b < a)
- Transitivity:
a < b ⟹ b < c ⟹ a < c
I was able to prove the first, but not the others. What took me even more by surprise, is that there are some sub-lemmas that would aid on these, such as Succ a < b ⟹ a < b
, a < b ⟹ a < Succ b
or a < b ∨ a = b ∨ b < a
, which seem even more trivial, but nonetheless I was also not able to prove, even after many attempts. It seems like only one of these (including 2.
and 3.
) is enough to prove the rest, but I wasn't able to prove any of them.
I'm mostly trying to use induction. Together with the fact that I've made the definitions myself, there are two possibilities - Either my definitions are wrong, and do not have the desired properties, or I'm missing some method/argument. So, I have two questions:
- Is my definition wrong (i.e. it does not accurately represent
<
and lacks the desired properties)? If so, how may I fix it? - If not, how can I prove these seemingly trivial properties?
For context, my current attempts are by induction, which I can prove the base case, but always get stuck in the induction case, not really knowing where to go with the assumptions, such as in this example:
lemma less_Succ_1: "Succ a < b ⟹ a < b"
proof (induction b)
case Zero
assume "Succ a < Zero"
then have "False" by simp
then show ?case by simp
next
case (Succ b)
assume "(Succ a < b ⟹ a < b)" "Succ a < Succ b"
then show "a < Succ b" oops
After some tips from user9716869, it's clear that my main problem was the lack of knowledge about the
arbitrary
option ininduction
. Using(induction _ arbitrary: _)
and(cases _)
(see the reference manual for details), the proofs are quite straight forward.Since these are made for educational purposes, the following proofs are not meant to be concise, but to make every step very clear. Most of these could be vastly reduced if more automation is desired, and some can be done in one line (which I left as a comment below the lemma).
Note: In these proofs, we are using an implicit lemma about inductive types, their injectivity (which implies
(Succ a = Succ b) ≡ (a = b)
andZero ≠ Succ a
). Furthermore,(Succ a < Succ b) ≡ (a < b)
by definition.First, we prove 2 useful lemmas:
a < b ⟹ b ≠ Zero
b ≠ Zero ⟷ (∃ b'. b = Succ b')
Armed with these, we can prove the 3 main statements:
~ (a < a)
a < b ⟹ ~ (b < a)
a < b ⟹ b < c ⟹ a < c