Search code examples
isabelleproofisar

Proving basic properties of recursive "less than" definition for naturals in Isabelle

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:

  1. Non-reflexivity: ~ (a < a)
  2. Non-symmetry: a < b ⟹ ~ (b < a)
  3. 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:

  1. Is my definition wrong (i.e. it does not accurately represent < and lacks the desired properties)? If so, how may I fix it?
  2. 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
Solution

  • After some tips from user9716869, it's clear that my main problem was the lack of knowledge about the arbitrary option in induction. 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) and Zero ≠ 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')
    lemma greater_not_Zero [simp]: "a < b ⟹ b ≠ Zero"
  (*by clarsimp*)
proof
  assume "a < b" "b = Zero"
  then have "a < Zero" by simp
  then show "False" by simp
qed

lemma not_Zero_is_Succ: "b ≠ Zero ⟷ (∃ b'. b = Succ b')"
  (*by (standard, cases b) auto*)
proof
  show "b ≠ Zero ⟹ ∃ b'. b = Succ b'"
  proof (cases b)
    case Zero
    assume ‹b ≠ Zero› 
    moreover note ‹b = Zero›
    ultimately show "∃b'. b = Succ b'" by contradiction
  next
    case (Succ b')
    assume ‹b ≠ Zero› 
    note ‹b = Succ b'› 
    then show "∃b'. b = Succ b'" by simp
  qed
next
  assume "∃ b'. b = Succ b'"
  then obtain b'::natt where "b = Succ b'" by clarsimp
  then show "b ≠ Zero" by simp
qed

    Armed with these, we can prove the 3 main statements:

    • Non-reflexivity: ~ (a < a)
    • Non-symmetry: a < b ⟹ ~ (b < a)
    • Transitivity: a < b ⟹ b < c ⟹ a < c
    lemma less_not_refl [simp]: "¬ a < a"
  (*by (induction a) auto*)
proof (induction a)
  case Zero
  show "¬ Zero < Zero" by simp
next
  case (Succ a)
  note IH = ‹¬ a < a›
  show "¬ Succ a < Succ a" 
  proof
    assume "Succ a < Succ a"
    then have "a < a" by simp
    then show "False" using IH by contradiction
  qed
qed

lemma less_not_sym: "a < b ⟹ ¬ b < a"
proof (induction a arbitrary: b)
  case Zero
  then show "¬ b < Zero" by simp
next
  case (Succ a)
  note IH = ‹⋀b. a < b ⟹ ¬ b < a› 
    and IH_prems = ‹Succ a < b›
  show "¬ b < Succ a"
  proof
    assume asm:"b < Succ a"

    have "b ≠ Zero" using IH_prems by simp
    then obtain b'::natt where eq: "b = Succ (b')" 
      using not_Zero_is_Succ by clarsimp
    then have "b' < a" using asm by simp
    then have "¬ a < b'" using IH by clarsimp
    moreover have "a < b'" using IH_prems eq by simp
    ultimately show "False" by contradiction
  qed
qed

lemma less_trans [trans]: "a < b ⟹ b < c ⟹ a < c"
proof (induction c arbitrary: a b)
  case Zero
  note ‹b < Zero›
  then have "False" by simp
  then show ?case by simp
next 
  case (Succ c)
  note IH = ‹⋀a b. a < b ⟹ b < c ⟹ a < c› 
    and IH_prems = ‹a < b› ‹b < Succ c›
  show "a < Succ c"
  proof (cases a)
    case Zero
    note ‹a = Zero›
    then show "a < Succ c" by simp 
  next 
    case (Succ a')
    note cs_prem = ‹a = Succ a'›

    have "b ≠ Zero" using IH_prems by simp
    then obtain b' where b_eq: "b = Succ b'" 
      using not_Zero_is_Succ by clarsimp
    then have "a' < b'" using IH_prems cs_prem b_eq by simp
    moreover have "b' < c" using IH_prems b_eq by simp
    ultimately have "a' < c" using IH by simp
    then show "a < Succ c" using cs_prem by simp
  qed
qed