zmod bit golf

Stream: general

[Johan Commelin]

Some of the proofs below look like they are twice as long as they should be. Golfing challenge!

import tactic.basic
import data.zmod.basic
import field_theory.finite.basic
import algebra.invertible

namespace nat

variables (n : ℕ)

@[simp] lemma bit0_mod_two : bit0 n % 2 = 0 :=
show (n + n) % 2 = 0, by rw [← two_mul, mul_mod, mod_self, zero_mul, zero_mod]

@[simp] lemma bit1_mod_two : bit1 n % 2 = 1 :=
by rw [bit1, add_mod, bit0_mod_two, zero_add, mod_mod, one_mod]

end nat

namespace zmod
variables (n : ℕ)

@[simp] lemma pow_bit0 [fact (bit1 n).prime] (k : zmod (bit1 n)) (hk : k ≠ 0) :
  k ^ (bit0 n) = 1 :=
zmod.pow_card_sub_one_eq_one hk

lemma two_mul_gcd_a_self_bit1 (n : ℕ) : 2 * (nat.gcd_a 2 (bit1 n) : zmod (bit1 n)) = 1 :=
begin
  have aux := nat.gcd_eq_gcd_ab 2 (bit1 n),
  apply_fun (coe : ℤ → zmod (bit1 n)) at aux,
  simp only [int.cast_add, int.cast_mul, int.cast_coe_nat, zmod.cast_self, zero_mul, add_zero,
    nat.cast_bit0, nat.cast_one] at aux,
  suffices : nat.gcd 2 (bit1 n) = 1,
  { rw [← aux, this, nat.cast_one] },
  simp only [nat.gcd_succ, nat.gcd_one_left, eq_self_iff_true, nat.bit1_mod_two]
end

instance invertible_two : invertible (2 : zmod (bit1 n)) :=
{ inv_of := nat.gcd_a 2 (bit1 n),
  inv_of_mul_self := by rw [mul_comm, two_mul_gcd_a_self_bit1],
  mul_inv_of_self := two_mul_gcd_a_self_bit1 _ }

@[simp] lemma bit0_ne_zero (k : zmod (bit1 n)) (hk : k ≠ 0) : (bit0 k) ≠ 0 :=
begin
  apply mt _ hk,
  haveI : fact (0 < bit1 n) := nat.pos_of_ne_zero (nat.bit1_ne_zero _),
  rw [bit0, ← two_mul],
  intro H,
  apply_fun (*) (⅟2 : zmod (bit1 n)) at H,
  simpa only [←mul_assoc, one_mul, inv_of_mul_self, mul_zero] using H
end

@[simp] lemma bit1_ne_zero (k : zmod (bit0 n)) : (bit1 k) ≠ 0 :=
begin
  intro H,
  cases n,
  { change ℤ at k,
    apply_fun (coe : ℤ → zmod 2) at H,
    simp only [int.cast_bit1, cast_zero] at H,
    revert H,
    generalize : (k : zmod 2) = i,
    dec_trivial! },
  { apply_fun (*) n.succ at H,
    simp only [bit1, bit0, mul_add, ←add_mul, mul_one, mul_zero, ← nat.cast_add] at H,
    rw [zmod.cast_self, zero_mul, zero_add, nat_coe_zmod_eq_zero_iff_dvd] at H,
    apply not_le_of_lt _ (nat.le_of_dvd (n.succ_pos) H),
    rw [bit0],
    exact nat.lt_add_of_pos_left n.succ_pos }
end

end zmod