Efficient reasoning in modular arithmetic

Question

I decided to prove the following theorem:

theory Scratch
  imports Main
begin

lemma "(3::int)^k mod 4 = 1 ⟷ even k"
proof (cases "even k")
  case True
    then obtain l where "2*l = k" by auto
    then show ?thesis
      using power_mult [of "(3::int)" 2 l]
      and power_mod [of "(9::int)" 4 l] by auto
next
  case False
    then obtain l where "2*l + 1 = k" using odd_two_times_div_two_succ by blast
    then have "(3::int)^k mod 4 = 3"
      using power_mult [of "(3::int)" 2 l ]
      and mod_mult_right_eq [of "(3::int)" "9^l" 4]
      and power_mod [of "(9::int)" 4 l]
      by auto
    then show ?thesis using `odd k` by auto
qed

end

The proof is accepted by Isabelle, but to my taste, there is way too much trivial detail as to how calculations mod 4 are performed:

    then have "(3::int)^k mod 4 = 3"
      using power_mult [of "(3::int)" 2 l ]
      and mod_mult_right_eq [of "(3::int)" "9^l" 4]
      and power_mod [of "(9::int)" 4 l]
      by auto

Apart from the application of power_mult, this is only application of various rules on what parts of expressions may be safely reduced. Is there a proof method that can infer detail like this automatically?

(I'm also open to any other comments about my proof style - one thing that bothers me is the repetitive ::int)

Answer 1

Following some discussion on IRC and subsequent experimentation, I have learned the following:

Firstly, the a mod c = b mod c is somewhat verbose. HOL-Number_Theory.Cong defines the notation [a = b] (mod c), which is much more pleasant to use.

theory Scratch
  imports
    Main
    "HOL-Number_Theory.Cong" (* or "HOL-Number_Theory.Number_Theory",
                                but that requires some more computation *)
begin

(note that this will make Isabelle compile the theory, which can take some time. You might want to run isabelle jedit -l HOL-Number_Theory, so that this happens only once.)

A one-line proof of the theorem will still require manually instantiating the relevant lemmas. However, it is usually a better idea to spell out the steps some more. This will allow the tactics to infer how the theorems should be instantiated, while leaving more useful detail for the human.

proof (cases "even k")
  case True
  then obtain l where "2*l = k" by auto
  then have "[3^k = (3^2)^l] (mod 4)" (is "cong _ ... _")
    by (auto simp add: power_mult)
  also have "[... = (1::int)^l] (mod 4)" (is "cong _ ... _")
    by (intro cong_pow) (simp add: cong_def)
  also have "[... = 1] (mod 4)" by auto
  finally have "[3^k = 1::int] (mod 4)".
  thus ?thesis using `even k` by blast
next
  case False
  then obtain l where "2*l + 1 = k"
    using oddE by blast
  then have "[3^k = 3^(2*l+1)] (mod 4)" (is "cong _ ... _") by auto
  also have "[... = (3^2)^l * 3] (mod 4)" (is "cong _ ... _")
    by (metis power_mult power_add power_one_right cong_def)
  also have "[... = (1::int)^l * 3] (mod 4)" (is "cong _ ... _")
    by (intro cong_mult cong_pow) (auto simp add: cong_def)
  also have "[... = 3] (mod 4)" by auto
  finally have "[3^k ≠ 1::int] (mod 4)" by (auto simp add: cong_def)
  then show ?thesis using `odd k` by blast
qed

This is a pretty standard calculational proof, where we use ... to refer to the RHS of the previous command. By default, it refers to the last argument of the top-level function application. In this case, that would be the modulus, so we override it with (is "cong _ ... _").

Also note that we can avoid a large part of the work by reusing minus_one_power_iff:

lemma "[3^k = 1::int] (mod 4) ⟷ even k"
proof -
  have "[3^k = (-1::int)^k] (mod 4)"
    by (intro cong_pow) (auto simp: cong_def)
  thus ?thesis
    by (auto simp: cong_def minus_one_power_iff)
qed