rw for modeq?

Stream: general

[Fabian Glöckle]

I am formalizing an easy IMO problem on modular arithmetic:

import data.pnat.basic
import tactic.norm_num
import tactic.interval_cases
import tactic.ring
import data.nat.modeq

theorem imo_1964_p1_1
  -- (n : ℤ)
  (n : ℕ)
  (h₀ : 7 ∣ (2^n - 1)) :
  3 ∣ n :=
begin
  have hupper := (@nat.mod_lt n 3) (by norm_num),
  interval_cases (n % 3),
  { exact nat.dvd_of_mod_eq_zero h },
  { -- Case: n % 3 = 1
    have hn := nat.div_add_mod n 3,
    rw h at hn,
    rw ←hn at h₀,
    have H : 2 ^ (3 * (n / 3) + 1) = 2 * (2 ^ 3) ^ (n / 3),
    simp only [pow_succ, pow_mul],
    rw H at h₀,
    ring_nf at h₀,

    have H₇ : (2 * 8 ^ (n / 3) - 1) ≡ 0 [MOD 7] := nat.mod_eq_zero_of_dvd h₀,
    have H₇ : 2 * 8 ^ (n / 3) - 1 + 1 ≡ 1 [MOD 7] := nat.modeq.add_right 1 H₇,
    rw nat.sub_add_cancel at H₇,

    have h₈ : 8 ≡ 1 [MOD 7] := @nat.add_modeq_left 1 7,
    have h₈' := nat.modeq.pow (n/3) h₈,
    simp at h₈',
    have h₈'' := nat.modeq.mul_left 2 h₈',
    simp at h₈'',
    have contra := nat.modeq.trans (nat.modeq.comm.1 h₈'') H₇,
    dsimp [nat.modeq] at contra,
    rw nat.mod_def at contra,
    simp at contra,
    contradiction,

    have hle₁ := nat.one_le_pow (n / 3) 8 (by simp),
    have hle₂ := @nat.le_mul_of_pos_left (8^(n/3)) 2 (by simp),
    exact trans hle₁ hle₂
  },
  { -- Case: n % 3 = 2
    -- similarly
    sorry
  }
end

nat.modeq provides all the lemmas needed to perform such computations. However, working with modeq did not come very natural to me because I couldn't use simps and rws like I could with equalities. Does rw support rewriting along equivalence relations? Or is it better to work in the quotients? What would you recommend / are there any best practices?

[Kevin Buzzard]

No, rw only works for = and <->. If you want to use = then I can recommend the zmod n type (which is the quotient, with API). You can't in general rewrite along equivalence relations because if X ~ Y and P X is true then in general there's no reason for P Y to be true.

[Joachim Breitner]

Slightly off topic, but a better tactic together with appropriate congruence lemmas _could_ do such rewriting (Isabelle's simplifier can). Maybe one day :-)

(Although I am suddenly not sure if I remember that correctly. Maybe I am spreading fake news. Hmm, I'll do more research.)

[Jannis Limperg]

Coq also has 'generalised rewriting', so it's certainly possible. Lots of work though and it's not so urgent in Lean because of the quotient workaround.

[Joachim Breitner]

Ah, maybe I was misremembering what's in Isabelle and what's in Coq. But good point about quotients, of course.

[Heather Macbeth]

I wrote a small tactic for this kind of thing, for my students. I never PR'd it because I am sure I'm missing a lot of tricks, but it should give an idea of what's possible.

import tactic.interactive
import data.int.modeq

namespace tactic

/-- Congruence lemmas (currently an incomplete list) -/
def mod_lemmas : list name :=
[`int.modeq.add_right, `int.modeq.add_left, `int.modeq.add,
 `int.modeq.sub_right, `int.modeq.sub_left, `int.modeq.sub,
 `int.modeq.mul_left, `int.modeq.mul_right,
 `int.modeq.neg, `int.modeq.pow, `int.modeq.refl]

/-- Append all the congruence lemmas to a list of expressions. -/
meta def append_mod_lemmas : list expr → tactic (list expr)
| [] := (mod_lemmas.mmap resolve_name) >>= (list.mmap i_to_expr_for_apply)
| (h :: t) := do l ← append_mod_lemmas t,
                 return (h :: l)

/-- Run through a list of expressions and, for any of the form `a ≡ b [ZMOD c]`, append the
symemtric expression `b ≡ a [ZMOD c]`. -/
meta def add_symms : list expr → tactic (list expr)
| [] := return []
| (h :: t) :=
    do tail ← add_symms t,
       h_typ ← infer_type h,
       match h_typ with
       | `(int.modeq %%a %%b %%c) := do h_symm ← mk_app `int.modeq.symm [h],
                                        return (h_symm :: h :: tail)
       | _ := return (h :: tail)
       end

meta def foo : list expr → tactic (list (tactic expr))
| [] := return []
| (h :: t) := do l ← foo t,
                 return ((return h) :: l)

meta def mod_substitute (hs : list pexpr) : tactic unit :=
do l₀ ← (hs.mmap i_to_expr_for_apply) >>= add_symms,
   l ← lock_tactic_state $ append_mod_lemmas l₀ >>= foo,
   iterate_at_most_on_subgoals 50 (apply_list_expr {} l)


meta def add_pos_hyp (p : expr) : tactic unit :=
do z ← mk_app `nat.zero [],
   pos ← mk_app `has_lt.lt [z, p],
   assert `h_pos pos, tactic.exact_dec_trivial

setup_tactic_parser

namespace interactive

meta def mod_substitute (hs : parse pexpr_list_or_texpr) : tactic unit :=
tactic.mod_substitute hs

end interactive
end tactic

[Heather Macbeth]

It allows for things like

example (n : ℤ) : 5 * n ^ 2 + 3 * n + 7 ≡ 1 [ZMOD 2] :=
calc 5 * n ^ 2 + 3 * n + 7
        ≡ 5 * 0 ^ 2 + 3 * 0 + 7 [ZMOD 2] : by mod_substitute hn
    ... = 1 + 2 * 3 : by norm_num
    ... ≡ 1 [ZMOD 2] : by apply int.modeq_add_fac',

[Kevin Buzzard]

@Fabian Glöckle here's a zmod 7 proof of the middle case:

  { -- Case: n % 3 = 1
    rw [← nat.div_add_mod n 3, h, pow_add, pow_mul,
      ← zmod.nat_coe_zmod_eq_zero_iff_dvd] at h₀,
    norm_num [show (8 : zmod 7) = 1, by dec_trivial] at h₀,
  },

The first line tidies up the way you tidied up (but more efficiently -- you might want to compare what the first line does with how you did it). But then that last rewrite puts us into Z/7 and then norm_num knows things like 1^(n/3)=1.

[Fabian Glöckle]

Thank you for all your answers.
I guess what I am asking for is a way to rewrite P X to P Y provided that X ~ Y and that P is ~-equivariant in O(1) tactic lines, not in O(depth of P).
To sum up the answers: Both a dedicated rewriting system for equivalence relations which is aware of the equivariance lemmas (as in Coq or @Heather Macbeth 's tactic), and rewriting equalities in the quotient as in @Kevin Buzzard 's solution achieve this. The latter works because norm_num is aware of the "equivariance lemmas for zmod coes".

[Heather Macbeth]

@Jannis Limperg @Joachim Breitner Where can I find out more about this "generalized rewriting"? The tactic I wrote works pretty well for the relation ≡ [ZMOD n], but my attempts at doing something similar for the relation ≤ failed dismally. (Here's the kind of problem I hit.). I'd love to see something more expert there.

[Kyle Miller]

Just to document some poking around in Lean internals: there's an extremely weak version of this in simp, if I understand it correctly, which is the lift_eq option (by default tt). It looks like that when simp is trying to prove R a b when R is a reflexive relation, it will try to prove a = b, which gives it access to all the congruence lemmas, and then construct a proof of the relation if it succeeds.

I've wondered what it would be like if simp were able to pass to a quotient by a relation, so for example go from ZMOD to zmod, in both the goal/target and the hypotheses. It might also have to "zmodify" things to be useful (or maybe @[congr] lemmas are enough? I'm not sure).

[Jannis Limperg]

@Heather Macbeth User-level docs are here. The corresponding paper seems to be this one. Re-implementing this is certainly doable, but it's a significant amount of work. I would guesstimate one or two good MSc theses.

[Heather Macbeth]

Thanks! In any case I guess this wouldn't work for the relation ≤: it looks like it's specific to equivalence relations.

[Jannis Limperg]

No, the Coq implementation also supports asymmetric relations (though maybe the paper version didn't). See this section for a remarkably confusing example.