Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
import data.int.modeq
open nat
inductive pf {p : ℕ}
| of_int : ℤ → pf
namespace pf
variables {p : ℕ}
protected def eq : (@pf p) → (@pf p) → Prop
| (of_int m) (of_int n) := m ≡ n [ZMOD p]
notation a `≡` b := pf.eq a b
@[refl] protected theorem eq.refl {α : @pf p} : α ≡ α := by cases α; unfold pf.eq
@[symm] protected theorem eq.symm {α β : @pf p} : α ≡ β → β ≡ α :=
begin
intro h,
cases α, cases β,
unfold pf.eq at *,
exact int.modeq.symm h
end
@[trans] protected theorem eq.trans {α β γ : @pf p} : α ≡ β → β ≡ γ → α ≡ γ :=
begin
intros h1 h2,
cases α, cases β, cases γ,
unfold pf.eq at *,
exact int.modeq.trans h1 h2
end
protected theorem equiv.is_equivalence : equivalence (@pf.eq p) :=
mk_equivalence (@pf.eq p) (@eq.refl p) (@eq.symm p) (@eq.trans p)
instance : has_equiv (@pf p) := ⟨pf.eq⟩
instance decidable_eq (α β : @pf p) : decidable (α ≡ β) :=
by cases α; cases β; apply int.decidable_eq
protected def add : @pf p → @pf p → @pf p
| (of_int m) (of_int n) := of_int ((m + n) % p)
instance : has_add (@pf p) := ⟨pf.add⟩
lemma eq_lem (n : ℤ) : @of_int p n ≡ @of_int p (n % p) :=
begin
unfold pf.eq at *,
apply int.modeq.symm,
apply int.modeq.mod_modeq n p
end
@[simp] lemma of_int_add (n m : ℤ) : @of_int p n + @of_int p m ≡ @of_int p (n + m) := eq.symm (eq_lem _)
theorem pf_add {α β γ η: @pf p} (h₁ : α ≡ β) (h₂ : γ ≡ η) : α + γ ≡ β + η :=
begin
cases α, cases β, cases γ, cases η,
transitivity, apply of_int_add, symmetry,
transitivity, apply of_int_add, symmetry,
apply int.modeq.modeq_add h₁ h₂
end
end pf
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment