Reducing code in hypothesis

Stream: new members

[duck]

Hi all, I am relatively new to lean and I’ve been doing some math with it

I have written this hypothesis

  have pow_a_b_eq_mod_g : a ≡ a^N [MOD g] ∨ b ≡ b^N [MOD g]:= by
    obtain h0 | h1 := Nat.le_total b a
    left
    . have : a * b ≤ a * a := by rel [h0]
      have dvd_a_sub_b : g ∣ a - b := by
        rw [← Nat.sub_sub_self le_mul_a,
              Nat.sub_right_comm,
              ← mul_sub_one,
              mul_comm,
              ← mul_sub_one]
        apply dvd_sub _ dvd_b_a dvd_a_b
        repeat rw [mul_sub_one]
        rw [mul_comm]
        rel [h0]
      have dvd_a_sq_a : g ∣ a^2 - a := by
        rw [pow_two, ← Nat.sub_add_cancel this, Nat.add_sub_assoc le_mul_a,
          ← mul_sub_one, ← Nat.mul_sub_left_distrib, add_comm]
        refine dvd_add dvd_a_b ?_
        exact dvd_mul_of_dvd_right dvd_a_sub_b a
      have : a ≤ a^2 := by nlinarith
      have a_eq_a_sq := dvd_a_sq_a
      rw [← Nat.modEq_iff_dvd' this] at a_eq_a_sq
      exact m_eq_pow_k_mod_n a_eq_a_sq N hn
    right
    . have : b*a ≤ b * b := by rel [h1]

      have dvd_b_sub_a : g ∣ b - a := by
        rw [← Nat.sub_sub_self le_mul_b,
              Nat.sub_right_comm,
              ← mul_sub_one,
              mul_comm,
              ← mul_sub_one]
        apply Nat.dvd_sub _ dvd_a_b dvd_b_a
        repeat rw [mul_sub_one]
        rw [mul_comm]
        rel [h1]
      have dvd_b_sq_b : g ∣ b^2 - b := by
        rw [pow_two, ← Nat.sub_add_cancel this, Nat.add_sub_assoc le_mul_b,
          ← mul_sub_one, ← Nat.mul_sub_left_distrib, add_comm]
        refine dvd_add dvd_b_a ?_
        exact dvd_mul_of_dvd_right dvd_b_sub_a b
      have : b ≤ b^2 := by nlinarith
      have b_eq_b_sq := dvd_b_sq_b
      rw [← Nat.modEq_iff_dvd' this] at b_eq_b_sq
      exact m_eq_pow_k_mod_n b_eq_b_sq N hn

And I was hoping since the two constructors are so similar that I could possibly reduce the amount of code duplication from it. Thanks!

[Julian Berman]

Hi! Can you make that into an #mwe (that's a link), so that it's easier for someone to play with.

[Martin Dvořák]

Please make a working example out of it #mwe (emphasis on "working") – imports, main theorem statement.

[duck]

import Mathlib.Data.Nat.ModEq
import Mathlib.Algebra.Group.Defs
import Mathlib.FieldTheory.Finite.Basic
import Mathlib.Tactic.GCongr

open Nat

lemma m_eq_pow_k_mod_n (h: m ≡ m^2 [MOD n]): ∀k ≥ 1, m ≡ m^k [MOD n] := by sorry

lemma g_eq_gcd_or_two_times {a b g N : ℕ} (ha: 0 < a) (hb: 0 < b) (hn: 0 < N)
  (h : ∀ n ≥ N, Nat.gcd (a^n + b) (b^n + a) = g) : g = Nat.gcd 2*(Nat.gcd a b) ∨ g = Nat.gcd a b := by
  have le_mul_a := Nat.le_mul_of_pos_right a hb
  have le_mul_b := Nat.le_mul_of_pos_right b ha

  have dvd_a_n : ∀ n ≥ N, g ∣ a^n + b := by sorry
  have dvd_b_a: g ∣ b*(a - 1) := by sorry
  have dvd_b_n: ∀ n ≥ N, g ∣ b^n + a := by sorry
  have dvd_a_b: g ∣ a*(b - 1) := by sorry
  have pow_a_b_eq_mod_g : a ≡ a^N [MOD g] ∨ b ≡ b^N [MOD g]:= by
    obtain h0 | h1 := le_total b a
    left
    . have : a * b ≤ a * a := by rel [h0]
      have dvd_a_sub_b : g ∣ a - b := by
        rw [← Nat.sub_sub_self le_mul_a,
              Nat.sub_right_comm,
              ← mul_sub_one,
              mul_comm,
              ← mul_sub_one]
        apply dvd_sub _ dvd_b_a dvd_a_b
        repeat rw [mul_sub_one]
        rw [mul_comm]
        rel [h0]
      have dvd_a_sq_a : g ∣ a^2 - a := by
        rw [pow_two, ← Nat.sub_add_cancel this, Nat.add_sub_assoc le_mul_a,
          ← mul_sub_one, ← Nat.mul_sub_left_distrib, add_comm]
        refine dvd_add dvd_a_b ?_
        exact dvd_mul_of_dvd_right dvd_a_sub_b a
      have : a ≤ a^2 := by nlinarith
      have a_eq_a_sq := dvd_a_sq_a
      rw [← Nat.modEq_iff_dvd' this] at a_eq_a_sq
      exact m_eq_pow_k_mod_n a_eq_a_sq N hn
    right
    . have : b*a ≤ b * b := by rel [h1]

      have dvd_b_sub_a : g ∣ b - a := by
        rw [← Nat.sub_sub_self le_mul_b,
              Nat.sub_right_comm,
              ← mul_sub_one,
              mul_comm,
              ← mul_sub_one]
        apply Nat.dvd_sub _ dvd_a_b dvd_b_a
        repeat rw [mul_sub_one]
        rw [mul_comm]
        rel [h1]
      have dvd_b_sq_b : g ∣ b^2 - b := by
        rw [pow_two, ← Nat.sub_add_cancel this, Nat.add_sub_assoc le_mul_b,
          ← mul_sub_one, ← Nat.mul_sub_left_distrib, add_comm]
        refine dvd_add dvd_b_a ?_
        exact dvd_mul_of_dvd_right dvd_b_sub_a b
      have : b ≤ b^2 := by nlinarith
      have b_eq_b_sq := dvd_b_sq_b
      rw [← Nat.modEq_iff_dvd' this] at b_eq_b_sq
      exact m_eq_pow_k_mod_n b_eq_b_sq N hn

Hi, sorry for that. I have attached the mwe here. A lot of the code is replicated due to the symmetric nature of the problem, often just substituting b for an and vice versa. I was really hoping I could reduce the amount of code for each variable if the core logic is very similar.

[Ruben Van de Velde]

Are you asking "is it possible to reduce the size of each individual branch" or "can I keep just one of the branches and argue by symmetry for the other one"?

[Derek Rhodes]

Hi duck, I pulled some of the have blocks out to named lemmas which reduced code duplication and nesting. It would be really nice if editors supported this refactoring automatically. Not sure if that's practical given Lean's exotic syntax.

import Mathlib.Data.Nat.ModEq
import Mathlib.Algebra.Group.Defs
import Mathlib.FieldTheory.Finite.Basic
import Mathlib.Tactic.GCongr

open Nat

lemma dvd_v_n {v w g N : ℕ} : ∀ n ≥ N, g ∣ v^n + w := by sorry
lemma dvd_w_n {v w g N : ℕ} : ∀ n ≥ N, g ∣ w^n + v := by sorry

lemma dvd_mul_sub (v w g N : ℕ) : g ∣ v * (w - 1) := by sorry
lemma dvd_pow_add (v w g N : ℕ) : ∀ n ≥ N, g ∣ v^n + w := by sorry

lemma m_eq_pow_k_mod_n (h: m ≡ m^2 [MOD n]): ∀k ≥ 1, m ≡ m^k [MOD n] := by sorry

lemma dvd_sub' (v w g N : ℕ) {hw: 0 < w} {h0 : w ≤ v} : g ∣ v - w := by
  have le_mul_v := Nat.le_mul_of_pos_right v hw
  rw [← Nat.sub_sub_self le_mul_v,
        Nat.sub_right_comm,
        ← mul_sub_one,
        mul_comm,
        ← mul_sub_one]
  apply dvd_sub _ (dvd_mul_sub w v g N) (dvd_mul_sub v w g N)
  repeat rw [mul_sub_one]
  rw [mul_comm]
  rel [h0]

lemma mod_congr_pow {a b g N : ℕ} (hb: 0 < b) (hn: 0 < N) (h0 : b ≤ a) : a ≡ a ^ N [MOD g] := by
  have le_mul_a := Nat.le_mul_of_pos_right a hb
  have : a * b ≤ a * a := by rel [h0]
  have dvd_a_sub_b : g ∣ a - b := @dvd_sub' a b g N hb h0
  have dvd_a_sq_a : g ∣ a^2 - a := by
    rw [pow_two, ← Nat.sub_add_cancel this, Nat.add_sub_assoc le_mul_a,
      ← mul_sub_one, ← Nat.mul_sub_left_distrib, add_comm]
    refine dvd_add (@dvd_mul_sub a b g N) ?_
    exact dvd_mul_of_dvd_right dvd_a_sub_b a
  have : a ≤ a^2 := by nlinarith
  have a_eq_a_sq := dvd_a_sq_a
  rw [← Nat.modEq_iff_dvd' this] at a_eq_a_sq
  exact m_eq_pow_k_mod_n a_eq_a_sq N hn

lemma g_eq_gcd_or_two_times {a b g N : ℕ} (ha: 0 < a) (hb: 0 < b) (hn: 0 < N)
  (h : ∀ n ≥ N, Nat.gcd (a^n + b) (b^n + a) = g) : g = Nat.gcd 2*(Nat.gcd a b) ∨ g = Nat.gcd a b := by
  have le_mul_a := Nat.le_mul_of_pos_right a hb
  have le_mul_b := Nat.le_mul_of_pos_right b ha

  have pow_a_b_eq_mod_g : a ≡ a^N [MOD g] ∨ b ≡ b^N [MOD g]:= by
    obtain h0 | h1 := le_total b a
    left
    apply mod_congr_pow hb hn h0
    right
    apply mod_congr_pow ha hn h1

[duck]

That looks kind of what I’m looking for, thanks so much!