Zulip Chat Archive

Stream: maths

Topic: How to manipulate zmod and its field structure?


view this post on Zulip Ryan Lahfa (May 24 2020 at 08:36):

I'm trying to prove some basic example stuff:

import algebra.group.basic
import algebra.group_power
import data.zmod.basic

def aperiodic_element {M : Type} [monoid M] (a : M) :=
  n : , a^n = a^(n+1)

def aperiodic_monoid (M : Type) [monoid M] :=
  x : M, aperiodic_element x

-- example of multiplicative monoids of Z/(n) rings

example : aperiodic_monoid (zmod 2) := begin
  unfold aperiodic_monoid, intro x,
  unfold aperiodic_element, use 1,
  norm_num, rw pow_two,
  have possible_values :  y : zmod 2, y = 0  y = 1 := dec_trivial,
  cases (possible_values x) with xz xo,
  rw xz, refl,
  rw xo, refl,
end

example : ¬(aperiodic_monoid (zmod 3)) := begin
  unfold aperiodic_monoid,
  push_neg, use 2,
  unfold aperiodic_element, push_neg,
  intros n h,
  rw pow_succ at h,
  rw  mul_one ((2: zmod 3)^n) at h, -- how to do things starting here?
  unfreezeI,
  haveI: fact (nat.prime 3) := sorry,
  haveI := zmod.field 3,
  have: ((2: zmod 3)^n  0) := sorry,
  have := mul_left_cancel' this h,
end

My problem is that for the second example, we are struggling to get a left (or right)-cancellation, because zmod is a field only if 3 is prime, so I try to inject the instance using haveI/unfreezeI, but it prevents me to rewrite the 1 properly.
I don't know if I'm doing something wrong.
set_option pp.all true does not help me as everything is "finite" and produces infinite terms

(code taken from a friend who is trying to formalize some of his work)

view this post on Zulip Kevin Buzzard (May 24 2020 at 09:06):

Do you need letI for the field instance? It's not a Prop I guess.

view this post on Zulip Ryan Lahfa (May 24 2020 at 09:09):

It seems to fix my last step, indeed

view this post on Zulip Kevin Buzzard (May 24 2020 at 09:12):

example : ¬(aperiodic_monoid (zmod 3)) := begin
  unfold aperiodic_monoid,
  push_neg, use 2,
  unfold aperiodic_element, push_neg,
  intros n h,
  rw pow_succ at h,
  rw (show (2 : zmod 3)* 2^n = 2^n + 2^n, by ring) at h,
  have : (2 : zmod 3) ^ n = 0,
  { library_search},
  haveI : fact (nat.prime 3) := by norm_num,
  refine pow_ne_zero n _ this,
  exact dec_trivial,
end

Lazy proving

view this post on Zulip Ryan Lahfa (May 24 2020 at 09:14):

Thanks !

view this post on Zulip Chris Hughes (May 24 2020 at 17:51):

Doing haveI for the field structure will cause problems because have forgets the definitions, so Lean won't know that the new field structure coincides with the old ring structure.


Last updated: May 14 2021 at 20:13 UTC