proving an obvious statement · Beginner Questions

Usually failing to prove this kind of "obvious" statement involving numerals is because the type of numerals (0, 1, 2, ...) is much more general than one expects. If you fix some type for those numerals, the propositions should become easy to prove, e.g.:

lemma
  "(0 :: nat) ∈ {0..<4}"
  "(1 :: nat) ∈ {0..<4}"
  "(2 :: int) ∈ {0..<4}"
  "(3 :: int) ∈ {0..<4}"
  "finite ({0..<4} :: nat set)"
  by simp_all

depending on what you're after. In general, whenever you find yourself stumped on some trivial lemma like this, it's always a good idea to check which types Isabelle has inferred and/or annotate them yourself.

In fact, we can find a type 'a :: numeral for which the propositions can be falsified. With a little help from a friendly chatbot and sledgehammer:

Counterexample

datatype rev_nat = Rev (unrev: nat)

instantiation rev_nat :: zero begin
definition "0 = Rev 0"
instance ..
end

instantiation rev_nat :: one begin
definition "1 = Rev 1"
instance ..
end

instantiation rev_nat :: plus begin
definition "(x + y) = Rev (unrev x + unrev y)"
instance ..
end

instantiation rev_nat :: times begin
definition "(x * y) = Rev (unrev x * unrev y)"
instance ..
end

instantiation rev_nat :: ord begin
definition "(x ≤ y) ≡ unrev y ≤ unrev x"
definition "(x < y) ≡ unrev y < unrev x"
instance ..
end

instantiation rev_nat :: linorder
begin
instance
  apply standard
  unfolding less_eq_rev_nat_def less_rev_nat_def using rev_nat.expand by auto
end

instantiation rev_nat :: semiring_1
begin
instance
  apply standard
  unfolding
    zero_rev_nat_def one_rev_nat_def plus_rev_nat_def times_rev_nat_def
      less_eq_rev_nat_def less_rev_nat_def using rev_nat.expand
  by (simp_all add: algebra_simps)
end

lemma
  "¬ (0 :: rev_nat) ∈ {0..<4}"
  "¬ (1 :: rev_nat) ∈ {0..<4}"
  "¬ (2 :: rev_nat) ∈ {0..<4}"
  "¬ (3 :: rev_nat) ∈ {0..<4}"
  by (simp_all add: numeral_Bit0 numeral_Bit1 zero_rev_nat_def one_rev_nat_def plus_rev_nat_def less_rev_nat_def)

Also

lemma "¬ finite ({0..<4} :: real set)" by simp

Stream: Beginner Questions

Topic: proving an obvious statement

Craig Alan Feinstein (Nov 09 2025 at 00:23):

Max Lang (Nov 09 2025 at 07:18):

Craig Alan Feinstein (Nov 09 2025 at 20:09):