modp setoid

Stream: general

[Johan Commelin]

Can something like this be made to work?

namespace modp
variables (α : Type*) [comm_ring α] (p : ℕ) (hp : nat.prime p)

def rel : setoid α := submodule.quotient_rel (ideal.span ({p} : set α))

local attribute [instance] rel

variables {α p}
lemma pow_add (a b : α) : (a + b)^p ≈ a^p + b^p :=
_

end modp

[Chris Hughes]

Look at add_pow_char in algebra.char_p

[Chris Hughes]

and use quotient_ring.quotient instead of submodule.quotient

[Chris Hughes]

Or ideal.quotient. I forget the name.

[Johan Commelin]

I guess I should clarify (-;

[Johan Commelin]

I want to use the relation.

[Johan Commelin]

Point is that I want to do some computations with mv_polynomials over the integers, modulo p.

[Johan Commelin]

And using this relation would make for readable calc proofs

[Reid Barton]

Can you use mv_polynomials over the integers modulo p?

[Chris Hughes]

But isn't it easier to map everything into the quotient and use equality?

[Johan Commelin]

Otherwise you'll have ideal.quotient.mk (ideal.span ({p} : set (mv_polynomial int _)) all over the place...

[Chris Hughes]

use notation

[Johan Commelin]

I guess I could define a local notation for that... but then the proof state is still ugly

[Chris Hughes]

I don't like the fact that we can't quotient mod p without things being ugly.

[Reid Barton]

I was hoping you could use parameter but it doesn't seem to help

[Johan Commelin]

I would like to write

calc [mod p] foo = bar : blah
  ... = xyzzy : etc

[Johan Commelin]

And then coercions should take care of the rest

[Reid Barton]

You should at least be able to write calc foo =[p]= bar : blah ... = xyzzy : etc using notation

[Reid Barton]

though at that point I guess you should just define notation which depends on p

[Johan Commelin]

Isn't that what you are doing in your example?

[Johan Commelin]

Is interactive calc in core or in mathlib? I couldn't find it easily

[Kevin Buzzard]

Must be in core because it's in TPIL

[Johan Commelin]

Is that interactive calc or term-mode calc?

[Reid Barton]

I mean in a section you can define local notation which depends on a variable, so you don't need to write this funny =[p]= stuff.

[Johan Commelin]

I am currently experimenting with

notation x ` modᵢ ` I := ideal.quotient.mk I x
notation x ` modₛ ` s := ideal.quotient.mk (ideal.span s) x
notation x ` modₑ ` a := ideal.quotient.mk (ideal.span ({a})) x

[Johan Commelin]

This can probably be improved quite a bit, using priorities etc... but I've no idea what would be sensible.

[Johan Commelin]

namespace modp
variables {α : Type*} [comm_ring α] {p : ℕ} (hp : nat.prime p)

notation x ` modᵢ ` I := ideal.quotient.mk I x
notation x ` modₛ ` s := ideal.quotient.mk (ideal.span s) x
notation x ` modₑ ` a := ideal.quotient.mk (ideal.span ({a})) x

include hp
instance (h : ¬ is_unit (p : α)) : char_p (ideal.span ({p} : set α)).quotient p :=
⟨begin
  intro n,
  have helper : ∀ m : ℕ, (m : (ideal.span ({p} : set α)).quotient) =
    ideal.quotient.mk (ideal.span ({p} : set α)) (m : α),
  { intro m, induction m with m ih, {refl}, simp [ih] },
  split,
  { intro H,
    rw [helper, ideal.quotient.eq_zero_iff_mem, ideal.mem_span_singleton] at H,
    rcases H with ⟨c, hc⟩,
    cases nat.coprime_or_dvd_of_prime hp n with hn hn,
    swap, {exact hn},
    have key := nat.gcd_eq_gcd_ab p n,
    delta nat.coprime at hn, rw hn at key,
    replace key := congr_arg (λ k : ℤ, (k : α)) key,
    simp only [int.cast_coe_nat, int.cast_add, int.coe_nat_zero, int.cast_mul, int.cast_one,
      int.coe_nat_succ, zero_add, hc] at key,
    rw [mul_assoc, ← mul_add] at key,
    exfalso, apply h,
    rw is_unit_iff_exists_inv,
    exact ⟨_, key.symm⟩ },
  { rintro ⟨c, rfl⟩,
    apply eq_zero_of_zero_dvd,
    use p,
    rw [zero_mul, helper (p*c), ideal.quotient.eq_zero_iff_mem, nat.cast_mul],
    exact ideal.mul_mem_right _ (ideal.subset_span $ set.mem_singleton p) }
end⟩
.

example (a b : α) : ((a + b)^p modₑ (p : α)) = (a^p modₑ (p : α)) + (b^p modₑ (p : α)) :=
begin
  sorry
end

end modp

[Johan Commelin]

Does simp see through notation?

[Reid Barton]

Everything sees through notation