Zulip Chat Archive

Stream: general

Topic: modp setoid


view this post on Zulip Johan Commelin (Jun 06 2019 at 00:58):

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

view this post on Zulip Chris Hughes (Jun 06 2019 at 01:04):

Look at add_pow_char in algebra.char_p

view this post on Zulip Chris Hughes (Jun 06 2019 at 01:05):

and use quotient_ring.quotient instead of submodule.quotient

view this post on Zulip Chris Hughes (Jun 06 2019 at 01:06):

Or ideal.quotient. I forget the name.

view this post on Zulip Johan Commelin (Jun 06 2019 at 01:06):

I guess I should clarify (-;

view this post on Zulip Johan Commelin (Jun 06 2019 at 01:06):

I want to use the relation.

view this post on Zulip Johan Commelin (Jun 06 2019 at 01:06):

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

view this post on Zulip Johan Commelin (Jun 06 2019 at 01:06):

And using this relation would make for readable calc proofs

view this post on Zulip Reid Barton (Jun 06 2019 at 01:07):

Can you use mv_polynomials over the integers modulo p?

view this post on Zulip Chris Hughes (Jun 06 2019 at 01:07):

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

view this post on Zulip Johan Commelin (Jun 06 2019 at 01:07):

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

view this post on Zulip Chris Hughes (Jun 06 2019 at 01:07):

use notation

view this post on Zulip Johan Commelin (Jun 06 2019 at 01:08):

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

view this post on Zulip Chris Hughes (Jun 06 2019 at 01:08):

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

view this post on Zulip Reid Barton (Jun 06 2019 at 01:12):

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

view this post on Zulip Johan Commelin (Jun 06 2019 at 01:12):

I would like to write

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

view this post on Zulip Johan Commelin (Jun 06 2019 at 01:12):

And then coercions should take care of the rest

view this post on Zulip Reid Barton (Jun 06 2019 at 01:13):

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

view this post on Zulip Reid Barton (Jun 06 2019 at 01:14):

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

view this post on Zulip Johan Commelin (Jun 06 2019 at 01:16):

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

view this post on Zulip Johan Commelin (Jun 06 2019 at 06:33):

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

view this post on Zulip Kevin Buzzard (Jun 06 2019 at 06:35):

Must be in core because it's in TPIL

view this post on Zulip Johan Commelin (Jun 06 2019 at 06:40):

Is that interactive calc or term-mode calc?

view this post on Zulip Reid Barton (Jun 06 2019 at 07:29):

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.

view this post on Zulip Johan Commelin (Jun 06 2019 at 07:33):

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

view this post on Zulip Johan Commelin (Jun 06 2019 at 07:34):

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

view this post on Zulip Johan Commelin (Jun 06 2019 at 07:40):

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

view this post on Zulip Johan Commelin (Jun 06 2019 at 07:42):

Does simp see through notation?

view this post on Zulip Reid Barton (Jun 06 2019 at 07:47):

Everything sees through notation


Last updated: May 14 2021 at 12:18 UTC